Commit 7347e89e by Ralf Jung

experiment a little with notation for our language

 ... ... @@ -17,6 +17,41 @@ Definition LamV (e : {bind expr}) := RecV e.[ren(+1)]. Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2). Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]). Delimit Scope lang_scope with L. Bind Scope lang_scope with expr. Arguments wp {_ _} _ _%L _. (* TODO: The levels are all random. Also maybe we should not make 'new' a keyword. What about Arguments for hoare triples? Also find better notation for function application. Or maybe we can make "App" a coercion from expr to (expr → expr)? *) (* The colons indicate binders. *) Notation "'rec::' e" := (Rec e) (at level 100) : lang_scope. Notation "'λ:' e" := (Lam e) (at level 100) : lang_scope. Infix "\$" := App : lang_scope. Notation "'let:' e1 'in' e2" := (Let e1 e2) (at level 70) : lang_scope. Notation "e1 ';' e2" := (Seq e1 e2) (at level 70) : lang_scope. Notation "'if' e1 'then' e2 'else' e3" := (If e1 e2 e3) : lang_scope. Notation "'#0'" := (Var 0) (at level 10) : lang_scope. Notation "'#1'" := (Var 1) (at level 10) : lang_scope. Notation "'#2'" := (Var 2) (at level 10) : lang_scope. Notation "'#3'" := (Var 3) (at level 10) : lang_scope. Notation "'#4'" := (Var 4) (at level 10) : lang_scope. Notation "'#5'" := (Var 5) (at level 10) : lang_scope. Notation "'#6'" := (Var 6) (at level 10) : lang_scope. Notation "'#7'" := (Var 7) (at level 10) : lang_scope. Notation "'#8'" := (Var 8) (at level 10) : lang_scope. Notation "'#9'" := (Var 9) (at level 10) : lang_scope. Notation "'★' e" := (Load e) (at level 30) : lang_scope. Notation "e1 '<-' e2" := (Store e1 e2) (at level 60) : lang_scope. Notation "'new' e" := (Alloc e) (at level 60) : lang_scope. Notation "e1 '+' e2" := (Plus e1 e2) : lang_scope. Notation "e1 '≤' e2" := (Le e1 e2) : lang_scope. Notation "e1 '<' e2" := (Lt e1 e2) : lang_scope. Coercion LitNat : nat >-> expr. Coercion Loc : loc >-> expr. Section suger. Context {Σ : iFunctor}. Implicit Types P : iProp heap_lang Σ. ... ...
 ... ... @@ -5,14 +5,15 @@ Import heap_lang. Import uPred. Module LangTests. Definition add := Plus (LitNat 21) (LitNat 21). Goal ∀ σ, prim_step add σ (LitNat 42) σ None. Definition add := (21 + 21)%L. Goal ∀ σ, prim_step add σ 42 σ None. Proof. intros; do_step done. Qed. Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *) Definition rec_app := App rec (LitNat 0). (* FIXME RJ why do I need the %L ? *) Definition rec : expr := (rec:: #0 \$ #1)%L. (* fix f x => f x *) Definition rec_app : expr := rec \$ 0. Goal ∀ σ, prim_step rec_app σ rec_app σ None. Proof. intros; do_step done. Qed. Definition lam := Lam (Plus (Var 0) (LitNat 21)). Proof. Set Printing All. intros; do_step done. Qed. Definition lam : expr := (λ: #0 + 21)%L. Goal ∀ σ, prim_step (App lam (LitNat 21)) σ add σ None. Proof. intros; do_step done. Qed. End LangTests. ... ... @@ -22,10 +23,10 @@ Module LiftingTests. Implicit Types P : iProp heap_lang Σ. Implicit Types Q : val → iProp heap_lang Σ. (* TODO RJ: Some syntactic sugar for language expressions would be nice. *) Definition e3 := Load (Var 0). Definition e2 := Seq (Store (Var 0) (Plus (Load \$ Var 0) (LitNat 1))) e3. Definition e := Let (Alloc (LitNat 1)) e2. Definition e3 : expr := ★ #0. (* FIXME: Fix levels so that we do not need the parenthesis here. *) Definition e2 : expr := (#0 <- ★ #0 + 1) ; e3. Definition e : expr := let: new 1 in e2. Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■(v = LitNatV 2))). Proof. move=> σ E. rewrite /e. ... ... @@ -34,11 +35,13 @@ Module LiftingTests. rewrite -later_intro. apply forall_intro=>l. apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_. rewrite -later_intro. asimpl. (* TODO RJ: If you go here, you can see how the sugar does not print all so nicely. *) rewrite -(wp_bindi (SeqCtx (Load (Loc _)))). rewrite -(wp_bindi (StoreRCtx (LocV _))). rewrite -(wp_bindi (PlusLCtx _)). rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first. { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *) { by rewrite lookup_insert. } (* RJ FIXME: figure out why apply and eapply fail. *) rewrite -later_intro. apply wand_intro_l. rewrite right_id. rewrite -wp_plus -later_intro. rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first. ... ... @@ -52,15 +55,15 @@ Module LiftingTests. by apply const_intro. Qed. Definition FindPred' n1 Sn1 n2 f := If (Lt Sn1 n2) (App f Sn1) n1. Definition FindPred n2 := Rec (Let (Plus (Var 1) (LitNat 1)) (FindPred' (Var 2) (Var 0) n2.[ren(+3)] (Var 1))). Definition Pred := Lam (If (Le (Var 0) (LitNat 0)) (LitNat 0) (App (FindPred (Var 0)) (LitNat 0)) ). Definition FindPred' n1 Sn1 n2 f : expr := if (Sn1 < n2) then f \$ Sn1 else n1. Definition FindPred n2 : expr := Rec (let: (#1 + 1) in (FindPred' (#2) (#0) n2.[ren(+3)] (#1)))%L. Definition Pred : expr := λ: (if #0 ≤ 0 then 0 else (FindPred (#0)) \$ 0 )%L. Lemma FindPred_spec n1 n2 E Q : (■(n1 < n2) ∧ Q (LitNatV \$ pred n2)) ⊑ ... ... @@ -73,7 +76,7 @@ Module LiftingTests. { apply and_mono; first done. by rewrite -later_intro. } apply later_mono. (* Go on. *) rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred \$ LitNat n2))). rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred (LitNat n2)))). rewrite -wp_plus. asimpl. rewrite -(wp_bindi (CaseCtx _ _)). rewrite -!later_intro /=. ... ... @@ -94,7 +97,7 @@ Module LiftingTests. Qed. Lemma Pred_spec n E Q : ▷Q (LitNatV \$ pred n) ⊑ wp E (App Pred (LitNat n)) Q. ▷Q (LitNatV (pred n)) ⊑ wp E (App Pred (LitNat n)) Q. Proof. rewrite -wp_lam //. asimpl. rewrite -(wp_bindi (CaseCtx _ _)). ... ... @@ -109,7 +112,8 @@ Module LiftingTests. Goal ∀ E, True ⊑ wp (Σ:=Σ) E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)). (* FIXME why do we need %L here? *) (let: Pred \$ 42 in Pred \$ #0)%L (λ v, ■(v = LitNatV 40)). Proof. intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro. asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!