Commit 9709c97c authored by Robbert Krebbers's avatar Robbert Krebbers

Clean up anonymous binder hack.

We no longer abuse empty strings for anonymous binders. Instead, we
now have a data type for binders: a binder is either named or
anonymous.
parent 0a74ba89
Pipeline #212 passed with stage
From heap_lang Require Export substitution notation.
Definition newbarrier : val := λ: "", ref #0.
Definition newbarrier : val := λ: <>, ref #0.
Definition signal : val := λ: "x", "x" <- #1.
Definition wait : val :=
rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x".
......
......@@ -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 "" x e).
Notation Lam x e := (Rec BAnom x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let "" e1 e2).
Notation LamV x e := (RecV "" x e).
Notation Seq e1 e2 := (Let BAnom e1 e2).
Notation LamV x e := (RecV BAnom x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx "" e2).
Notation SeqCtx e2 := (LetCtx BAnom e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Section derived.
......@@ -18,18 +18,18 @@ Implicit Types Φ : val → iProp heap_lang Σ.
(** Proof rules for the sugar *)
Lemma wp_lam E x ef e v Φ :
to_val e = Some v
|| subst ef x v @ E {{ Φ }} || App (Lam x ef) e @ E {{ Φ }}.
Proof. intros. by rewrite -wp_rec ?subst_empty. Qed.
|| subst' ef x v @ E {{ Φ }} || App (Lam x ef) e @ E {{ Φ }}.
Proof. intros. by rewrite -wp_rec. Qed.
Lemma wp_let E x e1 e2 v Φ :
to_val e1 = Some v
|| subst e2 x v @ E {{ Φ }} || Let x e1 e2 @ E {{ Φ }}.
|| subst' e2 x v @ E {{ Φ }} || Let x e1 e2 @ E {{ Φ }}.
Proof. apply wp_lam. Qed.
Lemma wp_seq E e1 e2 v Φ :
to_val e1 = Some v
|| e2 @ E {{ Φ }} || Seq e1 e2 @ E {{ Φ }}.
Proof. intros ?. rewrite -wp_let // subst_empty //. Qed.
Proof. intros ?. by rewrite -wp_let. Qed.
Lemma wp_skip E Φ : Φ (LitV LitUnit) || Skip @ E {{ Φ }}.
Proof. rewrite -wp_seq // -wp_value //. Qed.
......
......@@ -15,10 +15,14 @@ Inductive un_op : Set :=
Inductive bin_op : Set :=
| PlusOp | MinusOp | LeOp | LtOp | EqOp.
Inductive binder := BAnom | BNamed : string binder.
Delimit Scope binder_scope with binder.
Bind Scope binder_scope with expr binder.
Inductive expr :=
(* Base lambda calculus *)
| Var (x : string)
| Rec (f x : string) (e : expr)
| Rec (f x : binder) (e : expr)
| App (e1 e2 : expr)
(* Base types and their operations *)
| Lit (l : base_lit)
......@@ -32,7 +36,7 @@ Inductive expr :=
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (x1 : string) (e1 : expr) (x2 : string) (e2 : expr)
| Case (e0 : expr) (x1 : binder) (e1 : expr) (x2 : binder) (e2 : expr)
(* Concurrency *)
| Fork (e : expr)
(* Heap *)
......@@ -43,7 +47,7 @@ Inductive expr :=
| Cas (e0 : expr) (e1 : expr) (e2 : expr).
Inductive val :=
| RecV (f x : string) (e : expr) (* e should be closed *)
| RecV (f x : binder) (e : expr) (* e should be closed *)
| LitV (l : base_lit)
| PairV (v1 v2 : val)
| InjLV (v : val)
......@@ -56,6 +60,8 @@ Global Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Global Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Global Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
Proof. solve_decision. Defined.
Global Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Proof. solve_decision. Defined.
Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
......@@ -101,7 +107,7 @@ Inductive ectx_item :=
| SndCtx
| InjLCtx
| InjRCtx
| CaseCtx (x1 : string) (e1 : expr) (x2 : string) (e2 : expr)
| CaseCtx (x1 : binder) (e1 : expr) (x2 : binder) (e2 : expr)
| AllocCtx
| LoadCtx
| StoreLCtx (e2 : expr)
......@@ -138,11 +144,12 @@ 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 "" v = e] to deal with anonymous binders *)
(** We have [subst e None 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 x "") then of_val v else Var y
| Rec f y e => Rec f y (if decide (x f x y) then subst e x v else e)
| Var y => if decide (x = y) then of_val v else Var y
| Rec f y e =>
Rec f y (if decide (BNamed x f BNamed x y) then subst e x v else e)
| App e1 e2 => App (subst e1 x v) (subst e2 x v)
| Lit l => Lit l
| UnOp op e => UnOp op (subst e x v)
......@@ -155,8 +162,8 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
| InjR e => InjR (subst e x v)
| Case e0 x1 e1 x2 e2 =>
Case (subst e0 x v)
x1 (if decide (x x1) then subst e1 x v else e1)
x2 (if decide (x x2) then subst e2 x v else e2)
x1 (if decide (BNamed x x1) then subst e1 x v else e1)
x2 (if decide (BNamed x x2) then subst e2 x v else e2)
| Fork e => Fork (subst e x v)
| Loc l => Loc l
| Alloc e => Alloc (subst e x v)
......@@ -164,6 +171,8 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
| Store e1 e2 => Store (subst e1 x v) (subst e2 x v)
| 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.
(** The stepping relation *)
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
......@@ -187,7 +196,7 @@ Inductive head_step : expr → state → expr → state → option expr → Prop
| BetaS f x e1 e2 v2 σ :
to_val e2 = Some v2
head_step (App (Rec f x e1) e2) σ
(subst (subst e1 f (RecV f x e1)) x v2) σ None
(subst' (subst' e1 f (RecV f x e1)) x v2) σ None
| UnOpS op l l' σ :
un_op_eval op l = Some l'
head_step (UnOp op (Lit l)) σ (Lit l') σ None
......@@ -206,10 +215,10 @@ Inductive head_step : expr → state → expr → state → option expr → Prop
head_step (Snd (Pair e1 e2)) σ e2 σ None
| CaseLS e0 v0 x1 e1 x2 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) x1 e1 x2 e2) σ (subst e1 x1 v0) σ None
head_step (Case (InjL e0) x1 e1 x2 e2) σ (subst' e1 x1 v0) σ None
| CaseRS e0 v0 x1 e1 x2 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) x1 e1 x2 e2) σ (subst e2 x2 v0) σ None
head_step (Case (InjR e0) x1 e1 x2 e2) σ (subst' e2 x2 v0) σ None
| ForkS e σ:
head_step (Fork e) σ (Lit LitUnit) σ (Some e)
| AllocS e v σ l :
......@@ -306,7 +315,7 @@ Lemma atomic_head_step e1 σ1 e2 σ2 ef :
atomic e1 head_step e1 σ1 e2 σ2 ef is_Some (to_val e2).
Proof.
destruct 2; simpl; rewrite ?to_of_val; try by eauto.
repeat (case_match || contradiction || simplify_eq/=); eauto.
unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Qed.
Lemma atomic_step e1 σ1 e2 σ2 ef :
......@@ -351,9 +360,6 @@ Lemma alloc_fresh e v σ :
let l := fresh (dom _ σ) in
to_val e = Some v head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
Lemma subst_empty e v : subst e "" v = e.
Proof. induction e; simpl; repeat case_decide; intuition auto with f_equal. Qed.
End heap_lang.
(** Language *)
......
......@@ -86,18 +86,18 @@ Qed.
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 {{ Φ }}
|| subst' (subst' e1 f (RecV f x e1)) x v @ E {{ Φ }}
|| App (Rec f x e1) e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (App _ _)
(subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
(subst' (subst' e1 f (RecV f x e1)) x v) None) ?right_id //=;
intros; inv_step; eauto.
Qed.
Lemma wp_rec' E f x erec v1 e2 v2 Φ :
v1 = RecV f x erec
to_val e2 = Some v2
|| subst (subst erec f v1) x v2 @ E {{ Φ }}
|| subst' (subst' erec f v1) x v2 @ E {{ Φ }}
|| App (of_val v1) e2 @ E {{ Φ }}.
Proof. intros ->. apply wp_rec. Qed.
......@@ -149,18 +149,18 @@ Qed.
Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0
|| subst e1 x1 v0 @ E {{ Φ }} || Case (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
|| subst' e1 x1 v0 @ E {{ Φ }} || Case (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
(subst e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
(subst' e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
Qed.
Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0
|| subst e2 x2 v0 @ E {{ Φ }} || Case (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
|| subst' e2 x2 v0 @ E {{ Φ }} || Case (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
(subst e2 x2 v0) None) ?right_id //; intros; inv_step; eauto.
(subst' e2 x2 v0) None) ?right_id //; intros; inv_step; eauto.
Qed.
End lifting.
......@@ -16,6 +16,9 @@ Coercion Var : string >-> expr.
Coercion App : expr >-> Funclass.
Coercion of_val : val >-> expr.
Coercion BNamed : string >-> binder.
Notation "<>" := BAnom : binder_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
(* We have overlapping notation for values and expressions, with the expressions
......@@ -64,9 +67,9 @@ 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 "" e2%L e1%L)
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 "" e2%L e1%L)
Notation "e1 ;; e2" := (LamV BAnom e2%L e1%L)
(at level 100, e2 at level 200, format "e1 ;; e2") : lang_scope.
Notation "'rec:' f x y := e" := (Rec f x (Lam y e%L))
......
......@@ -51,22 +51,24 @@ Proof. done. Qed.
Instance loc_closed l : Closed (Loc l).
Proof. done. Qed.
Definition subst_var_eq y x v : (x = y x "") Subst (Var y) x v (of_val v).
Definition subst_var_eq y x v : x = y Subst (Var y) x v (of_val v).
Proof. intros. by red; rewrite /= decide_True. Defined.
Definition subst_var_ne y x v : ¬(x = y x "") Subst (Var y) x v (Var y).
Definition subst_var_ne y x v : x y Subst (Var y) x v (Var y).
Proof. intros. by red; rewrite /= decide_False. Defined.
Hint Extern 0 (Subst (Var ?y) ?x ?v _) =>
match eval vm_compute in (bool_decide (x = y x "")) with
match eval vm_compute in (bool_decide (x = y)) with
| true => apply subst_var_eq; bool_decide_no_check
| false => apply subst_var_ne; bool_decide_no_check
end : typeclass_instances.
Instance subst_rec f y e x v er :
SubstIf (x f x y) e x v er Subst (Rec f y e) x v (Rec f y er).
SubstIf (BNamed x f BNamed x y) e x v er
Subst (Rec f y e) x v (Rec f y er).
Proof. intros [??]; red; f_equal/=; case_decide; auto. Qed.
Instance subst_case e0 x1 e1 x2 e2 x v e0r e1r e2r :
Subst e0 x v e0r SubstIf (x x1) e1 x v e1r SubstIf (x x2) e2 x v e2r
Subst e0 x v e0r
SubstIf (BNamed x x1) e1 x v e1r SubstIf (BNamed x x2) e2 x v e2r
Subst (Case e0 x1 e1 x2 e2) x v (Case e0r x1 e1r x2 e2r).
Proof. intros ? [??] [??]; red; f_equal/=; repeat case_decide; auto. Qed.
......@@ -109,11 +111,19 @@ Instance subst_cas e0 e1 e2 x v e0r e1r e2r :
Subst (Cas e0 e1 e2) x v (Cas e0r e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
Definition of_binder (mx : binder) : stringset :=
match mx with BAnom => | 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 :
SetUnfold (x of_binder mx) (mx = BNamed x).
Proof. constructor; destruct mx; set_solver. Qed.
(** * Solver for [Closed] *)
Fixpoint is_closed (X : stringset) (e : expr) : bool :=
match e with
| Var x => bool_decide (x X)
| Rec f y e => is_closed ({[ f ; y ]} X) e
| Rec f y e => is_closed (of_binder f of_binder y X) e
| App e1 e2 => is_closed X e1 && is_closed X e2
| Lit l => true
| UnOp _ e => is_closed X e
......@@ -125,7 +135,8 @@ Fixpoint is_closed (X : stringset) (e : expr) : bool :=
| InjL e => is_closed X e
| InjR e => is_closed X e
| Case e0 x1 e1 x2 e2 =>
is_closed X e0 && is_closed ({[x1]} X) e1 && is_closed ({[x2]} X) e2
is_closed X e0 &&
is_closed (of_binder x1 X) e1 && is_closed (of_binder x2 X) e2
| Fork e => is_closed X e
| Loc l => true
| Alloc e => is_closed X e
......@@ -147,9 +158,10 @@ Proof.
| _ => case_decide
| _ => f_equal
end; eauto;
match goal with
try match goal with
| H : _, _ _ _ subst _ _ _ = _ |- _ =>
eapply H; first done; rewrite !elem_of_union !elem_of_singleton; tauto
eapply H; first done;
rewrite !elem_of_union !elem_of_of_binder; intuition congruence
end.
Qed.
Ltac solve_closed := apply is_closed_sound; vm_compute; exact I.
......
......@@ -17,7 +17,7 @@ Section LangTests.
Goal σ, prim_step (lam #21)%L σ add σ None.
Proof.
intros. rewrite /lam. (* FIXME: do_step does not work here *)
by eapply (Ectx_step _ _ _ _ _ []), (BetaS "" "x" ("x" + #21) _ #21).
by eapply (Ectx_step _ _ _ _ _ []), (BetaS <> "x" ("x" + #21) _ #21).
Qed.
End LangTests.
......
......@@ -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 "" _ _) _ =>
| App (Rec BAnom _ _) _ =>
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