Commit f44d5ee2 authored by charguer's avatar charguer

polylet

parent e8f2a4c1
......@@ -2,7 +2,19 @@
(*---------polymorphism -----------*)
let test_poly () = let x = [] in x
let poly_top = []
let poly_let_1 () =
let x = [] in x
let poly_let_2 () =
let x = ([], []) in x
let poly_let_2_same () =
let x : ('a list * 'a list) = ([], []) in x
let poly_let_2_partial () =
let x : ('a list * int list) = ([], []) in x
(*---------simple record------------*)
......
......@@ -3,22 +3,54 @@ Set Implicit Arguments.
Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
(*************************************************************************)
(** * Polymorphic let demos *)
(*
let test_poly () = let x = [] in x
*)
Lemma test_poly_spec : forall A,
Spec test_poly () |B>>
B \[] (fun (x:list A) => \[x = @nil A]).
Proof.
intros. xcf.
apply local_erase. intros x Ex.
xret.
hsimpl.
subst x. auto.
Qed.
(** Demo top-level polymorphic let. *)
Lemma poly_top_spec : forall A,
poly_top = @nil A.
Proof using. xcf. Qed.
(** Demo local polymorphic let. *)
Lemma poly_let_1_spec : forall A,
Spec poly_let_1 () |B>>
B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval. subst. xrets. auto. Qed.
(** Demo [xval_st P] *)
Lemma poly_let_1_spec' : forall A,
Spec poly_let_1 () |B>>
B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval_st (fun a => a = @nil). extens~. xrets. subst~. Qed.
(** Demo [xval_st P as x Hx] *)
Lemma poly_let_1_spec'' : forall A,
Spec poly_let_1 () |B>>
B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval_st (fun a => a = @nil) as p Hp. extens~. xrets. subst~. Qed.
(** Demo for partially-polymorphic values. *)
Lemma poly_let_2_spec : forall A1 A2,
Spec poly_let_2 () |B>>
B \[] (fun '(x,y) : list A1 * list A2 => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xvals. xrets. auto. Qed.
Lemma poly_let_2_same_spec : forall A,
Spec poly_let_2_same () |B>>
B \[] (fun '(x,y) : list A * list A => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xvals. xrets. auto. Qed.
Lemma poly_let_2_partial_spec : forall A,
Spec poly_let_2_partial () |B>>
B \[] (fun '(x,y) : list A * list int => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xval as p Hp. subst p. xrets. auto. Qed.
......
......@@ -268,12 +268,30 @@ Notation "'App' f x1 x2 x3 x4 ;" :=
Notation "'AppReturns'" := (@app_1 _ _).
(** Let / Seq / Pay *)
(** LetVal *)
Notation "'LetVal' x ':=' V 'in' F" :=
(!V (fun H Q => forall x, x = V -> F H Q))
(at level 69, x ident) : charac.
Notation "'LetVal' [ A1 ] x ':=' V 'in' F" :=
(!V (fun H Q => forall x, x = (fun (A1:Type) => V) -> F H Q))
(at level 69, x ident, A1 ident) : charac.
Notation "'LetVal' [ A1 A2 ] x ':=' V 'in' F" :=
(!V (fun H Q => forall x, x = (fun (A1 A2:Type) => V) -> F H Q))
(at level 69, x ident, A1 ident, A2 ident) : charac.
Notation "'LetVal' [ A1 A2 A3 ] x ':=' V 'in' F" :=
(!V (fun H Q => forall x, x = (fun (A1 A2 A3:Type) => V) -> F H Q))
(at level 69, x ident, A1 ident, A2 ident, A3 ident) : charac.
Notation "'LetVal' [ A1 A2 A3 A4 ] x ':=' V 'in' F" :=
(!V (fun H Q => forall x, x = (fun (A1 A2 A3 A4:Type) => V) -> F H Q))
(at level 69, x ident, A1 ident, A2 ident, A3 ident, A4 ident) : charac.
(** Let / Seq / Pay *)
Notation "'Let' x ':=' F1 'in' F2" :=
(!T (fun H Q => exists Q1, F1 H Q1 /\ forall x, F2 (Q1 x) Q))
(at level 69, x ident, right associativity,
......
......@@ -626,30 +626,50 @@ Tactic Notation "xseq" "*" constr(H) := xseq H; auto_star.
(** [xval] is used to reason on a let-node binding a value. *)
Tactic Notation "xval" "as" simple_intropattern(x) simple_intropattern(Hx) :=
Ltac xval_impl x Hx :=
apply local_erase; intros x Hx.
Tactic Notation "xval" "as" simple_intropattern(x) simple_intropattern(Hx) :=
xval_impl x Hx.
Tactic Notation "xval" "as" simple_intropattern(x) :=
let Hx := fresh "P" x in xval as x Hx.
let Hx := fresh "P" x in xval_impl x Hx.
Ltac xval_anonymous_impl tt :=
apply local_erase; intro; let x := get_last_hyp tt in revert x;
let Hx := fresh "P" x in intros x Hx.
Tactic Notation "xval" :=
apply local_erase; intro; let x := get_last_hyp tt in revert x; xval as x.
xval_anonymous_impl tt.
(** [xvals] substitutes the bound value right away. *)
Tactic Notation "xvals" :=
Ltac xvals_impl tt :=
apply local_erase; intro; intro_subst.
Tactic Notation "xvals" :=
xvals_impl tt.
(** [xval_st P] is used to assign an abstract specification to the value *)
Ltac xval_st_core P x Hx :=
let E := fresh in intros x E; asserts Hx: (P x); [ subst x | clear E ].
Ltac xval_st_impl P x Hx :=
apply local_erase; xval_st_core P x Hx.
Tactic Notation "xval_st" constr(P) "as" simple_intropattern(x) simple_intropattern(Hx) :=
apply local_erase; intros x; asserts Hx: (P x); [ intro_subst | intros _ ].
xval_st_impl P x Hx.
Tactic Notation "xval_st" constr(P) "as" simple_intropattern(x) :=
let Hx := fresh "P" x in xval_st P as x Hx.
let Hx := fresh "P" x in xval_st_impl P x Hx.
Ltac xval_st_anonymous_impl P :=
apply local_erase; intro; let x := get_last_hyp tt in revert x;
let Hx := fresh "P" x in xval_st_core P x Hx.
Tactic Notation "xval_st" constr(P) :=
apply local_erase; intro; let x := get_last_hyp tt in revert x; xval_st P as x.
xval_st_anonymous_impl P.
(*--------------------------------------------------------*)
......
Set Implicit Arguments.
(********************************************************************)
(** Notation for functions expecting tuples as arguments *)
(** Note: this will later move to TLC *)
Notation "'fun' ''' ( x1 , x2 ) ':' T '=>' E" :=
(fun p : T => let '(x1,x2) := p in E)
(at level 200) : fun_scope.
Notation "'fun' ''' ( x1 , x2 ) '=>' E" :=
(fun p => let '(x1,x2) := p in E)
(at level 200, format "'fun' ''' ( x1 , x2 ) '=>' E") : fun_scope.
Notation "'fun' ''' ( x1 , x2 , x3 ) ':' T '=>' E" :=
(fun p : T => let '(x1,x2,x3) := p in E)
(at level 200) : fun_scope.
Notation "'fun' ''' ( x1 , x2 , x3 ) '=>' E" :=
(fun p => let '(x1,x2,x3) := p in E)
(at level 200, format "'fun' ''' ( x1 , x2 , x3 ) '=>' E") : fun_scope.
(* TODO: coqbug?
Notation "'fun' ''' ( x1 , x2 , x3 , x4) ':' T '=>' E" :=
(fun p : T => let '(x1,x2,x3,x4) := p in E)
(at level 60, E at level 200) : fun_scope.
Notation "'fun' ''' ( x1 , x2 , x3 , x4 ) '=>' E" :=
(fun p => match p with (x1,x2,x3,x4) => E end)
(at level 60, E at level 200, format "'fun' ''' ( x1 , x2 , x3 , x4 ) '=>' E") : fun_scope.
*)
Open Scope fun_scope.
(********************************************************************)
(** Treatment of partially-applied equality *)
......
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