Commit be24297e authored by Robbert Krebbers's avatar Robbert Krebbers

Do not use [ucmraT]s as argument of inG.

Since [inG] ranges over [cmraT]s, using an [ucmraT]s results in
[ucmra_cmraR] coercions that slow down type checking.

This commit improves the compilation time of thread_local.v by 40%.
parent 121fce4c
......@@ -3,10 +3,10 @@ From iris.prelude Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
Class irisPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
state_inG :> inG Σ (authUR (optionUR (exclR (stateC Λ))));
invariant_inG :> inG Σ (authUR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
enabled_inG :> inG Σ coPset_disjUR;
disabled_inG :> inG Σ (gset_disjUR positive);
state_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
invariant_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
enabled_inG :> inG Σ coPset_disjR;
disabled_inG :> inG Σ (gset_disjR positive);
}.
Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG {
......
......@@ -5,7 +5,7 @@ Import uPred.
Definition thread_id := gname.
Class thread_localG Σ :=
tl_inG :> inG Σ (prodUR coPset_disjUR (gset_disjUR positive)).
tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
Definition tlN : namespace := nroot .@ "tl".
......@@ -47,7 +47,7 @@ Section proofs.
P ={E}=> tl_inv tid N P.
Proof.
iIntros "HP".
iVs (own_empty tid) as "Hempty".
iVs (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
iVs (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
{ apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
apply (gset_alloc_empty_updateP_strong' (λ i, i nclose N)).
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment