Make let a built-in connective of heap_lang.

Now notations are pretty printed in the same way as they are parsed.
Before "let x := e1 in e2" was notation for "(fun x => e2) e1",
resulting in overlapping notations for the same thing.

heap_lang/heap_lang.v

@@ -19,6 +19,8 @@ Inductive expr :=
   | Var (x : string)
   | Rec (f x : string) (e : expr)
   | App (e1 e2 : expr)
+  (* Let *)
+  | Let (x : string) (e1 e2 : expr)
   (* Base types and their operations *)
   | Lit (l : base_lit)
   | UnOp (op : un_op) (e : expr)
@@ -76,6 +78,7 @@ Definition state := gmap loc val.
 Inductive ectx_item :=
   | AppLCtx (e2 : expr)
   | AppRCtx (v1 : val)
+  | LetCtx (x : string) (e2 : expr)
   | UnOpCtx (op : un_op)
   | BinOpLCtx (op : bin_op) (e2 : expr)
   | BinOpRCtx (op : bin_op) (v1 : val)
@@ -101,6 +104,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
   | AppLCtx e2 => App e e2
   | AppRCtx v1 => App (of_val v1) e
+  | LetCtx x e2 => Let x e e2
   | UnOpCtx op => UnOp op e
   | BinOpLCtx op e2 => BinOp op e e2
   | BinOpRCtx op v1 => BinOp op (of_val v1) e
@@ -129,6 +133,8 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
   | 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)
   | App e1 e2 => App (subst e1 x v) (subst e2 x v)
+  | Let y e1 e2 =>
+     Let y (subst e1 x v) (if decide (x ≠ y) then subst e2 x v else e2)
   | Lit l => Lit l
   | UnOp op e => UnOp op (subst e x v)
   | BinOp op e1 e2 => BinOp op (subst e1 x v) (subst e2 x v)
@@ -172,6 +178,9 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
      to_val e2 = Some v2 →
      head_step (App (Rec f x e1) e2) σ
        (subst (subst e1 f (RecV f x e1)) x v2) σ None
+  | DeltaS x e1 e2 v1 σ :
+     to_val e1 = Some v1 →
+     head_step (Let x e1 e2) σ (subst e2 x v1) σ None
   | UnOpS op l l' σ :
      un_op_eval op l = Some l' → 
      head_step (UnOp op (Lit l)) σ (Lit l') σ None

heap_lang/lifting.v

@@ -90,11 +90,19 @@ Proof.
     last by intros; inv_step; eauto.
 Qed.
 
+Lemma wp_let E x e1 e2 v Q :
+  to_val e1 = Some v →
+  ▷ wp E (subst e2 x v) Q ⊑ wp E (Let x e1 e2) Q.
+Proof.
+  intros. rewrite -(wp_lift_pure_det_step (Let _ _ _)
+    (subst e2 x v) None) ?right_id //=; intros; inv_step; eauto.
+Qed.
+
 Lemma wp_un_op E op l l' Q :
   un_op_eval op l = Some l' →
   ▷ Q (LitV l') ⊑ wp E (UnOp op (Lit l)) Q.
 Proof.
-  intros Heval. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
+  intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
     ?right_id //; last by intros; inv_step; eauto.
   by rewrite -wp_value'.
 Qed.

heap_lang/sugar.v

@@ -3,10 +3,8 @@ Import uPred heap_lang.
 
 (** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
 Notation Lam x e := (Rec "" 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 LetCtx x e2 := (AppRCtx (LamV x e2)).
 Notation SeqCtx e2 := (LetCtx "" e2).
 
 Module notations.
@@ -35,6 +33,10 @@ Module notations.
   Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
   (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
   Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
+  Notation "'let:' x := e1 'in' e2" := (Let x e1%L e2%L)
+    (at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope.
+  Notation "e1 ; e2" := (Seq e1%L e2%L)
+    (at level 100, e2 at level 200) : 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 "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
@@ -43,11 +45,6 @@ Module notations.
   (* derived notions, in order of declaration *)
   Notation "λ: x , e" := (Lam x e%L)
     (at level 102, x at level 1, e at level 200) : lang_scope.
-  (* FIXME: the ones below are not being pretty printed *)
-  Notation "'let:' x := e1 'in' e2" := (Let x e1%L e2%L)
-    (at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope.
-  Notation "e1 ; e2" := (Seq e1%L e2%L)
-    (at level 100, e2 at level 200) : lang_scope.
 End notations.
 
 Section suger.
@@ -60,16 +57,12 @@ Lemma wp_lam E x ef e v Q :
   to_val e = Some v → ▷ wp E (subst ef x v) Q ⊑ wp E (App (Lam x ef) e) Q.
 Proof. intros. by rewrite -wp_rec ?subst_empty; eauto. Qed.
 
-Lemma wp_let E x e1 e2 Q :
-  wp E e1 (λ v, ▷ wp E (subst e2 x v) Q) ⊑ wp E (Let x e1 e2) Q.
+Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷ wp E e2 Q) ⊑ wp E (Seq e1 e2) Q.
 Proof.
-  rewrite -(wp_bind [LetCtx x e2]). apply wp_mono=>v.
-  by rewrite -wp_lam //= to_of_val.
+  rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
+  by rewrite -wp_let //= ?subst_empty ?to_of_val.
 Qed.
 
-Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷wp E e2 Q) ⊑ wp E (Seq e1 e2) Q.
-Proof. rewrite -wp_let. apply wp_mono=>v. by rewrite subst_empty. Qed.
-
 Lemma wp_le E (n1 n2 : nat) P Q :
   (n1 ≤ n2 → P ⊑ ▷ Q (LitV true)) →
   (n1 > n2 → P ⊑ ▷ Q (LitV false)) →

heap_lang/tests.v

@@ -31,13 +31,12 @@ Module LiftingTests.
   Goal ∀ σ E, ownP (Σ:=Σ) σ ⊑ wp E e (λ v, v = LitV 2).
   Proof.
     move=> σ E. rewrite /e.
-    rewrite -wp_let /= -wp_alloc_pst //=.
+    rewrite -(wp_bindi (LetCtx _ _)) -wp_alloc_pst //=.
     apply sep_intro_True_r; first done.
     rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l.
     rewrite right_id; apply const_elim_l=> _.
-    rewrite -later_intro.
-    rewrite -(wp_bindi (SeqCtx (Load (Loc _)))) /=.
-    (* FIXME: doing simpl here kills the Seq, turns it all the way into Rec *)
+    rewrite -wp_let //= -later_intro.
+    rewrite -(wp_bindi (SeqCtx (Load (Loc _)))) /=. 
     rewrite -(wp_bindi (StoreRCtx (LocV _))) /=.
     rewrite -(wp_bindi (BinOpLCtx PlusOp _)) /=.
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
@@ -72,7 +71,8 @@ Module LiftingTests.
     rewrite ->(later_intro (Q _)).
     rewrite -!later_and; apply later_mono.
     (* Go on *)
-    rewrite -wp_let -wp_bin_op //= -(wp_bindi (IfCtx _ _)) /= -!later_intro.
+    rewrite -(wp_bindi (LetCtx _ _)) -wp_bin_op //= -wp_let //=.
+    rewrite -(wp_bindi (IfCtx _ _)) /= -!later_intro.
     apply wp_lt=> ?.
     - rewrite -wp_if_true.
       rewrite -!later_intro (forall_elim (n1 + 1)) const_equiv; last omega.
@@ -99,7 +99,8 @@ Module LiftingTests.
     True ⊑ wp (Σ:=Σ) E (let: "x" := Pred (Lit 42) in Pred "x")
                        (λ v, v = LitV 40).
   Proof.
-    intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro /=.
-    rewrite -Pred_spec -later_intro. by apply const_intro.
+    intros E.
+    rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let //=.
+    rewrite -Pred_spec -!later_intro /=. by apply const_intro.
   Qed.
 End LiftingTests.