Commit ecbac61a authored by Ralf Jung's avatar Ralf Jung

rename BAnom -> BAnon; avoid overloading notation in the same scope

parent e8ce5b38
......@@ -56,7 +56,7 @@ Section client.
wp_seq. (ewp eapply wp_store); eauto with I. strip_later.
rewrite assoc [(_ y _)%I]comm. apply sep_mono_r, wand_intro_l.
wp_seq. rewrite -signal_spec right_id assoc sep_elim_l comm.
apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", "z" + #42)%L).
apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", "z" + #42)%V).
apply sep_intro_True_r; first done. apply: always_intro.
apply forall_intro=>n. wp_let. wp_op. by apply const_intro. }
(* The two spawned threads, the waiters. *)
......
......@@ -2,12 +2,12 @@ From heap_lang Require Export lifting.
Import uPred.
(** Define some derived forms, and derived lemmas about them. *)
Notation Lam x e := (Rec BAnom x e).
Notation Lam x e := (Rec BAnon x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let BAnom e1 e2).
Notation LamV x e := (RecV BAnom x e).
Notation Seq e1 e2 := (Let BAnon e1 e2).
Notation LamV x e := (RecV BAnon x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx BAnom e2).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
......
......@@ -15,9 +15,14 @@ Inductive un_op : Set :=
Inductive bin_op : Set :=
| PlusOp | MinusOp | LeOp | LtOp | EqOp.
Inductive binder := BAnom | BNamed : string binder.
Inductive binder := BAnon | BNamed : string binder.
Delimit Scope binder_scope with binder.
Bind Scope binder_scope with expr binder.
Bind Scope binder_scope with binder.
Delimit Scope lang_scope with L.
Bind Scope lang_scope with base_lit.
Delimit Scope val_scope with V.
Bind Scope val_scope with base_lit.
Inductive expr :=
(* Base lambda calculus *)
......@@ -54,6 +59,10 @@ Inductive val :=
| InjRV (v : val)
| LocV (l : loc).
Bind Scope binder_scope with expr.
Bind Scope lang_scope with expr base_lit.
Bind Scope val_scope with val base_lit.
Global Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
Proof. solve_decision. Defined.
Global Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
......@@ -67,9 +76,6 @@ Proof. solve_decision. Defined.
Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
Proof. solve_decision. Defined.
Delimit Scope lang_scope with L.
Bind Scope lang_scope with expr val base_lit.
Fixpoint of_val (v : val) : expr :=
match v with
| RecV f x e => Rec f x e
......@@ -144,7 +150,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
(** Substitution *)
(** We have [subst e None v = e] to deal with anonymous binders *)
(** We have [subst' e BAnon v = e] to deal with anonymous binders *)
Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
match e with
| Var y => if decide (x = y) then of_val v else Var y
......@@ -170,7 +176,7 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
| Cas e0 e1 e2 => Cas (subst e0 x v) (subst e1 x v) (subst e2 x v)
end.
Definition subst' (e : expr) (mx : binder) (v : val) : expr :=
match mx with BNamed x => subst e x v | BAnom => e end.
match mx with BNamed x => subst e x v | BAnon => e end.
(** The stepping relation *)
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
......
......@@ -82,8 +82,6 @@ Proof.
rewrite later_sep -(wp_value _ _ (Lit _)) //.
Qed.
(* For the lemmas involving substitution, we only derive a preliminary version.
The final version is defined in substitution.v. *)
Lemma wp_rec E f x e1 e2 v Φ :
to_val e2 = Some v
|| subst' (subst' e1 f (RecV f x e1)) x v @ E {{ Φ }}
......
......@@ -17,7 +17,7 @@ Coercion App : expr >-> Funclass.
Coercion of_val : val >-> expr.
Coercion BNamed : string >-> binder.
Notation "<>" := BAnom : binder_scope.
Notation "<>" := BAnon : binder_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
......@@ -30,9 +30,9 @@ Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : lang_scope.
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1 e1 x2 e2)
(e0, x1, e1, x2, e2 at level 200) : lang_scope.
Notation "()" := LitUnit : lang_scope.
Notation "# l" := (Lit l%Z%L) (at level 8, format "# l").
Notation "# l" := (LitV l%Z%L) (at level 8, format "# l").
Notation "()" := LitUnit : val_scope.
(* No scope, does not conflict and scope is often not inferred properly. *)
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
Notation "! e" := (Load e%L) (at level 9, right associativity) : lang_scope.
Notation "'ref' e" := (Alloc e%L)
(at level 30, right associativity) : lang_scope.
......@@ -51,7 +51,7 @@ Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
Notation "'rec:' f x := e" := (Rec f x e%L)
(at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
Notation "'rec:' f x := e" := (RecV f x e%L)
(at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
(at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
(at level 200, e1, e2, e3 at level 200) : lang_scope.
......@@ -62,29 +62,31 @@ notations are otherwise not pretty printed back accordingly. *)
Notation "λ: x , e" := (Lam x e%L)
(at level 102, x at level 1, e at level 200) : lang_scope.
Notation "λ: x , e" := (LamV x e%L)
(at level 102, x at level 1, e at level 200) : lang_scope.
(at level 102, x at level 1, e at level 200) : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
(at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L)
(at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
Notation "e1 ;; e2" := (Lam BAnom e2%L e1%L)
(at level 100, e2 at level 200, format "e1 ;; e2") : lang_scope.
Notation "e1 ;; e2" := (LamV BAnom e2%L e1%L)
Notation "e1 ;; e2" := (Lam BAnon e2%L e1%L)
(at level 100, e2 at level 200, format "e1 ;; e2") : lang_scope.
(* These are not actually values, but we want them to be pretty-printed. *)
Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L)
(at level 102, x at level 1, e1, e2 at level 200) : val_scope.
Notation "e1 ;; e2" := (LamV BAnon e2%L e1%L)
(at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.
Notation "'rec:' f x y := e" := (Rec f x (Lam y e%L))
(at level 102, f, x, y at level 1, e at level 200) : lang_scope.
Notation "'rec:' f x y := e" := (RecV f x (Lam y e%L))
(at level 102, f, x, y at level 1, e at level 200) : lang_scope.
(at level 102, f, x, y at level 1, e at level 200) : val_scope.
Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%L)))
(at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%L)))
(at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
(at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
Notation "λ: x y , e" := (Lam x (Lam y e%L))
(at level 102, x, y at level 1, e at level 200) : lang_scope.
Notation "λ: x y , e" := (LamV x (Lam y e%L))
(at level 102, x, y at level 1, e at level 200) : lang_scope.
Notation "λ: x y z , e" := (Lam x (LamV y (LamV z e%L)))
(at level 102, x, y, z at level 1, e at level 200) : lang_scope.
Notation "λ: x y z , e" := (LamV x (LamV y (LamV z e%L)))
(at level 102, x, y at level 1, e at level 200) : val_scope.
Notation "λ: x y z , e" := (Lam x (Lam y (Lam z e%L)))
(at level 102, x, y, z at level 1, e at level 200) : lang_scope.
Notation "λ: x y z , e" := (LamV x (Lam y (Lam z e%L)))
(at level 102, x, y, z at level 1, e at level 200) : val_scope.
......@@ -111,7 +111,7 @@ Instance subst_cas e0 e1 e2 x v e0r e1r e2r :
Proof. by intros; red; f_equal/=. Qed.
Definition of_binder (mx : binder) : stringset :=
match mx with BAnom => | BNamed x => {[ x ]} end.
match mx with BAnon => | BNamed x => {[ x ]} end.
Lemma elem_of_of_binder x mx: x of_binder mx mx = BNamed x.
Proof. destruct mx; set_solver. Qed.
Global Instance set_unfold_of_binder (mx : binder) x :
......
......@@ -90,6 +90,4 @@ Section ClosedProofs.
apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
Qed.
Print Assumptions heap_e_closed.
End ClosedProofs.
......@@ -41,7 +41,7 @@ Tactic Notation "wp_lam" ">" :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with
| App (Rec BAnom _ _) _ =>
| App (Rec BAnon _ _) _ =>
wp_bind K; etrans;
[|eapply wp_lam; repeat (reflexivity || rewrite /= to_of_val)];
simpl_subst; wp_finish
......
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