Commit a8c7557d by Dan Frumin

### Notation for MAYBE

parent 04bc3235
 ... @@ -100,3 +100,16 @@ Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E) ... @@ -100,3 +100,16 @@ Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E) 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 "'[' '[' e1 ']' ;; '/' e2 ']'") : expr_scope. format "'[' '[' e1 ']' ;; '/' e2 ']'") : expr_scope. Notation NONE := (InjL #()) (only parsing). Notation SOME x := (InjR x) (only parsing). Notation NONEV := (InjLV #()) (only parsing). Notation SOMEV x := (InjRV x) (only parsing). Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" := (Match e0 BAnon e1 x%bind e2) (e0, e1, x, e2 at level 200, only parsing) : expr_scope. Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" := (Match e0 BAnon e1 x%bind e2) (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
 ... @@ -198,3 +198,6 @@ Proof. ... @@ -198,3 +198,6 @@ Proof. * by eapply IHHt1. * by eapply IHHt1. * eapply IHHt2. by apply map_fmap_mono. * eapply IHHt2. by apply map_fmap_mono. Qed. Qed. (* Type synonyms *) Notation MAYBE τ := (TSum TUnit τ) (only parsing).
 ... @@ -7,8 +7,8 @@ Import uPred. ... @@ -7,8 +7,8 @@ Import uPred. Definition CG_StackType τ := Definition CG_StackType τ := TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))). TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))). Notation Conse h t := (Fold (InjR (Pair h t))). Notation Conse h t := (Fold (SOME (Pair h t))). Notation Nile := (Fold (InjL #())). Notation Nile := (Fold NONE). (* Coarse-grained push *) (* Coarse-grained push *) Program Definition CG_push : val := λ: "st" "x", Program Definition CG_push : val := λ: "st" "x", ... @@ -23,8 +23,8 @@ Definition CG_locked_push : val := λ: "st" "l" "x", ... @@ -23,8 +23,8 @@ Definition CG_locked_push : val := λ: "st" "l" "x", end *) end *) Definition CG_pop : val := λ: "st" <>, Definition CG_pop : val := λ: "st" <>, match: Unfold !"st" with match: Unfold !"st" with InjL <> => InjL #() NONE => NONE | InjR "y" => "st" <- (Snd "y");; InjR (Fst "y") | SOME "y" => "st" <- (Snd "y");; SOME (Fst "y") end. end. ... @@ -41,8 +41,8 @@ Definition CG_snap : val := λ: "st" "l" <>, ... @@ -41,8 +41,8 @@ Definition CG_snap : val := λ: "st" "l" <>, end *) end *) Definition CG_iter : val := rec: "iter" "f" := λ: "s", Definition CG_iter : val := rec: "iter" "f" := λ: "s", match: (Unfold "s") with match: (Unfold "s") with InjL <> => #() NONE => #() | InjR "x" => "f" (Fst "x");; "iter" "f" (Snd "x") | SOME "x" => "f" (Fst "x");; "iter" "f" (Snd "x") end. end. (* snap_iter st l := λ f. iter f (snap st l #()) *) (* snap_iter st l := λ f. iter f (snap st l #()) *) ... @@ -155,7 +155,7 @@ Section CG_Stack. ... @@ -155,7 +155,7 @@ Section CG_Stack. Lemma CG_push_r st' (v w : val) l E1 E2 Δ Γ t K τ : Lemma CG_push_r st' (v w : val) l E1 E2 Δ Γ t K τ : nclose logrelN ⊆ E1 → nclose logrelN ⊆ E1 → st' ↦ₛ v -∗ l ↦ₛ #false -∗ st' ↦ₛ v -∗ l ↦ₛ #false -∗ (st' ↦ₛ FoldV (InjRV (w, v)) -∗ l ↦ₛ #false (st' ↦ₛ FoldV (SOMEV (w, v)) -∗ l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #() : τ) -∗ -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #() : τ) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_push \$/ (LitV (Loc st')) \$/ (LitV (Loc l))) w) : τ. {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_push \$/ (LitV (Loc st')) \$/ (LitV (Loc l))) w) : τ. Proof. Proof. ... @@ -199,10 +199,10 @@ Section CG_Stack. ... @@ -199,10 +199,10 @@ Section CG_Stack. Lemma CG_pop_suc_r st' l (w v : val) E1 E2 Δ Γ t K τ : Lemma CG_pop_suc_r st' l (w v : val) E1 E2 Δ Γ t K τ : nclose logrelN ⊆ E1 → nclose logrelN ⊆ E1 → st' ↦ₛ FoldV (InjRV (w, v)) -∗ st' ↦ₛ FoldV (SOMEV (w, v)) -∗ l ↦ₛ #false -∗ l ↦ₛ #false -∗ (st' ↦ₛ v -∗ l ↦ₛ #false (st' ↦ₛ v -∗ l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (InjR w) : τ) -∗ -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (SOME w) : τ) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_pop \$/ LitV (Loc st') \$/ LitV (Loc l)) #()) : τ. {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_pop \$/ LitV (Loc st') \$/ LitV (Loc l)) #()) : τ. Proof. Proof. iIntros (?) "Hst' Hl Hlog". iIntros (?) "Hst' Hl Hlog". ... @@ -230,10 +230,10 @@ Section CG_Stack. ... @@ -230,10 +230,10 @@ Section CG_Stack. Lemma CG_pop_fail_r st' l E1 E2 Δ Γ t K τ : Lemma CG_pop_fail_r st' l E1 E2 Δ Γ t K τ : nclose logrelN ⊆ E1 → nclose logrelN ⊆ E1 → st' ↦ₛ FoldV (InjLV #()) -∗ st' ↦ₛ FoldV NONEV -∗ l ↦ₛ #false -∗ l ↦ₛ #false -∗ (st' ↦ₛ FoldV (InjLV #()) -∗ l ↦ₛ #false (st' ↦ₛ FoldV NONEV -∗ l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (InjL #()) : τ) -∗ -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K NONE : τ) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_pop \$/ LitV (Loc st') \$/ LitV (Loc l)) #()) : τ. {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_locked_pop \$/ LitV (Loc st') \$/ LitV (Loc l)) #()) : τ. Proof. Proof. iIntros (?) "Hst' Hl Hlog". iIntros (?) "Hst' Hl Hlog". ... ...
 ... @@ -5,8 +5,8 @@ From iris_logrel Require Export logrel examples.stack.mailbox. ... @@ -5,8 +5,8 @@ From iris_logrel Require Export logrel examples.stack.mailbox. Definition LIST τ := Definition LIST τ := TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))). TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))). Notation Conse h t := (Fold (InjR (Pair h t))). Notation Conse h t := (Fold (SOME (Pair h t))). Notation Nile := (Fold (InjL #())). Notation Nile := (Fold NONE). Definition pop_st : val := λ: "r" "get", rec: "pop" <> := Definition pop_st : val := λ: "r" "get", rec: "pop" <> := match: "get" #() with match: "get" #() with ... ...
 ... @@ -2,20 +2,6 @@ From iris.proofmode Require Import tactics. ... @@ -2,20 +2,6 @@ From iris.proofmode Require Import tactics. From iris.algebra Require Import excl. From iris.algebra Require Import excl. From iris_logrel Require Export logrel. From iris_logrel Require Export logrel. Notation MAYBE τ := (TSum TUnit τ) (only parsing). Notation NONE := (InjL #()) (only parsing). Notation SOME x := (InjR x) (only parsing). Notation NONEV := (InjLV #()) (only parsing). Notation SOMEV x := (InjRV x) (only parsing). Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" := (Match e0 BAnon e1 x%bind e2) (e0, e1, x, e2 at level 200, only parsing) : expr_scope. Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" := (Match e0 BAnon e1 x%bind e2) (e0, e1, x, e2 at level 200, only parsing) : expr_scope. Definition mk_offer : val := Definition mk_offer : val := λ: "v", ("v", ref #0). λ: "v", ("v", ref #0). Definition revoke_offer : val := Definition revoke_offer : val := ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!