Commit c8956dab by Robbert Krebbers

### Some notation tweaking.

parent 97896530
 ... @@ -108,7 +108,7 @@ Section proof. ... @@ -108,7 +108,7 @@ Section proof. {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}. {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}. Proof. Proof. iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "[% #?]". iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "[% #?]". iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj. iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj. iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose". iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose". wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_". wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_". { iNext. iExists o, n. by iFrame. } { iNext. iExists o, n. by iFrame. } ... @@ -140,7 +140,7 @@ Section proof. ... @@ -140,7 +140,7 @@ Section proof. Proof. Proof. iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln) "[% #?]"; subst. iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln) "[% #?]"; subst. iDestruct "Hγ" as (o) "Hγo". iDestruct "Hγ" as (o) "Hγo". rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E. wp_let. wp_proj. wp_proj. wp_bind (! _)%E. iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose". iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose". wp_load. wp_load. iDestruct (own_valid_2 with "Hauth Hγo") as iDestruct (own_valid_2 with "Hauth Hγo") as ... ...
 ... @@ -23,13 +23,37 @@ Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope. ... @@ -23,13 +23,37 @@ Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope. first. *) first. *) Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope. Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope. Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope. Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope. (* Using the '[hv' ']' printing box, we make sure that when the notation for match does not fit on a single line, line breaks will be inserted for *each* breaking point '/'. Note that after each breaking point /, one can put n spaces (for example '/ '). That way, when the breaking point is turned into a line break, indentation of n spaces will appear after the line break. As such, when the match does not fit on one line, it will print it like: match: e0 with InjL x1 => e1 | InjR x2 => e2 end Moreover, if the branches do not fit on a single line, it will be printed as: match: e0 with InjL x1 => lots of stuff bla bla bla bla bla bla bla bla | InjR x2 => even more stuff bla bla bla bla bla bla bla bla end *) Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := (Match e0 x1%bind e1 x2%bind e2) (Match e0 x1%bind e1 x2%bind e2) (e0, x1, e1, x2, e2 at level 200, (e0, x1, e1, x2, e2 at level 200, format "'[' 'match:' e0 'with' '/' '[hv' 'InjL' x1 => '[' e1 ']' '/' | 'InjR' x2 => '[' e2 ']' '/' 'end' ']' ']'") : expr_scope. format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope. Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" := Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" := (Match e0 x2%bind e2 x1%bind e1) (Match e0 x2%bind e2 x1%bind e1) (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope. (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope. Notation "()" := LitUnit : val_scope. Notation "()" := LitUnit : val_scope. Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope. Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope. Notation "'ref' e" := (Alloc e%E) Notation "'ref' e" := (Alloc e%E) ... @@ -47,12 +71,15 @@ Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) (at level 70) : expr ... @@ -47,12 +71,15 @@ Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) (at level 70) : expr Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope. Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope. (* The unicode ← is already part of the notation "_ ← _; _" for bind. *) (* The unicode ← is already part of the notation "_ ← _; _" for bind. *) Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. (* The breaking point '/ ' makes sure that the body of the rec is indented by two spaces in case the whole rec does not fit on a single line. *) Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E) Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E) (at level 102, f at level 1, x at level 1, e at level 200, (at level 102, f at level 1, x at level 1, e at level 200, format "'[' '[hv' 'rec:' f x := ']' '/ ' e ']'") : expr_scope. format "'[' 'rec:' f x := '/ ' e ']'") : expr_scope. Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E)) Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E)) (at level 102, f at level 1, x at level 1, e at level 200, (at level 102, f at level 1, x at level 1, e at level 200, format "'[' '[hv' 'rec:' f x := ']' '/ ' e ']'") : val_scope. format "'[' 'rec:' f x := '/ ' e ']'") : val_scope. Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E) Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E) (at level 200, e1, e2, e3 at level 200) : expr_scope. (at level 200, e1, e2, e3 at level 200) : expr_scope. ... @@ -62,40 +89,47 @@ defined above. This is needed because App is now a coercion, and these ... @@ -62,40 +89,47 @@ defined above. This is needed because App is now a coercion, and these notations are otherwise not pretty printed back accordingly. *) notations are otherwise not pretty printed back accordingly. *) Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)) Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)) (at level 102, f, x, y, z at level 1, e at level 200, (at level 102, f, x, y, z at level 1, e at level 200, format "'[' '[hv' 'rec:' f x y .. z := ']' '/ ' e ']'") : expr_scope. format "'[' 'rec:' f x y .. z := '/ ' e ']'") : expr_scope. Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))) Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))) (at level 102, f, x, y, z at level 1, e at level 200, (at level 102, f, x, y, z at level 1, e at level 200, format "'[' '[hv' 'rec:' f x y .. z := ']' '/ ' e ']'") : val_scope. format "'[' 'rec:' f x y .. z := '/ ' e ']'") : val_scope. (* The breaking point '/ ' makes sure that the body of the λ: is indented by two spaces in case the whole λ: does not fit on a single line. *) Notation "λ: x , e" := (Lam x%bind e%E) Notation "λ: x , e" := (Lam x%bind e%E) (at level 102, x at level 1, e at level 200, (at level 102, x at level 1, e at level 200, format "'[' '[hv' 'λ:' x , ']' '/ ' e ']'") : expr_scope. format "'[' 'λ:' x , '/ ' e ']'") : expr_scope. Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..)) Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..)) (at level 102, x, y, z at level 1, e at level 200, (at level 102, x, y, z at level 1, e at level 200, format "'[' '[hv' 'λ:' x y .. z , ']' '/ ' e ']'") : expr_scope. format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope. (* When parsing lambdas, we want them to be locked (so as to avoid needless unfolding by tactics and unification). However, unlocked lambda-values sometimes appear as part of compound expressions, in which case we want them to be pretty printed too. We achieve that by first defining the non-locked notation, and then the locked notation. Both will be used for pretty-printing, but only the last will be used for parsing. *) Notation "λ: x , e" := (LamV x%bind e%E) (at level 102, x at level 1, e at level 200, format "'[' 'λ:' x , '/ ' e ']'") : val_scope. Notation "λ: x , e" := (locked (LamV x%bind e%E)) Notation "λ: x , e" := (locked (LamV x%bind e%E)) (at level 102, x at level 1, e at level 200, (at level 102, x at level 1, e at level 200, format "'[' '[hv' 'λ:' x , ']' '/ ' e ']'") : val_scope. format "'[' 'λ:' x , '/ ' e ']'") : val_scope. Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )) (at level 102, x, y, z at level 1, e at level 200, format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope. Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))) Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))) (at level 102, x, y, z at level 1, e at level 200, (at level 102, x, y, z at level 1, e at level 200, format "'[' '[hv' 'λ:' x y .. z , ']' '/ ' e ']'") : val_scope. format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope. Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E) Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E) (at level 102, x at level 1, e1, e2 at level 200, (at level 102, x at level 1, e1, e2 at level 200, format "'[' '[hv' 'let:' x := '[' e1 ']' 'in' ']' '/' e2 ']'") : expr_scope. format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope. Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E) Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E) (at level 100, e2 at level 200, (at level 100, e2 at level 200, format "'[' '[hv' '[' e1 ']' ;; ']' '/' e2 ']'") : expr_scope. format "'[' '[hv' '[' e1 ']' ;; ']' '/' e2 ']'") : expr_scope. (* These are not actually values, but we want them to be pretty-printed. *) Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%E e1%E) (at level 102, x at level 1, e1, e2 at level 200, format "'[' '[hv' 'let:' x := '[' e1 ']' 'in' ']' '/' e2 ']'") : val_scope. Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E) (at level 100, e2 at level 200, format "'[' '[hv' '[' e1 ']' ;; ']' '/' e2 ']'") : val_scope. (* Shortcircuit Boolean connectives *) (* Shortcircuit Boolean connectives *) Notation "e1 && e2" := Notation "e1 && e2" := (If e1%E e2%E (Lit (LitBool false))) (only parsing) : expr_scope. (If e1%E e2%E (Lit (LitBool false))) (only parsing) : expr_scope. ... ...
 ... @@ -22,7 +22,7 @@ Ltac wp_done := ... @@ -22,7 +22,7 @@ Ltac wp_done := | _ => fast_done | _ => fast_done end. end. Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta. Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; simpl. Ltac wp_seq_head := Ltac wp_seq_head := lazymatch goal with lazymatch goal with ... ...
 ... @@ -56,7 +56,7 @@ Proof. ... @@ -56,7 +56,7 @@ Proof. iNext; iRight; iExists n; by iFrame. iNext; iRight; iExists n; by iFrame. + wp_cas_fail. iMod ("Hclose" with "[-]"); last eauto. + wp_cas_fail. iMod ("Hclose" with "[-]"); last eauto. rewrite /one_shot_inv; eauto 10. rewrite /one_shot_inv; eauto 10. - iIntros "!#". wp_seq. wp_bind (! _)%E. - iIntros "!# /=". wp_seq. wp_bind (! _)%E. iInv N as ">Hγ" "Hclose". iInv N as ">Hγ" "Hclose". iAssert (∃ v, l ↦ v ∗ ((⌜v = NONEV⌝ ∗ own γ Pending) ∨ iAssert (∃ v, l ↦ v ∗ ((⌜v = NONEV⌝ ∗ own γ Pending) ∨ ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv". ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv". ... ...
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