Commit b2f2d1e6 authored by charguer's avatar charguer

sep

parent 8860950f
......@@ -417,6 +417,9 @@ Notation "'App_' f x1 x2 x3 x4 ;" :=
(** Record contents *)
(* TODO: notation "f1 ':= x1" := record_entry_lifted f1 x1 := (f1,Dyn x1) *)
Notation "`'{ f1 := x1 }" :=
((f1, Dyn x1)::nil)
(at level 0, f1 at level 0)
......
......@@ -114,6 +114,17 @@ Global Opaque MList.
(** Temporary auxiliary specification *)
Parameter rule_get_tl : forall p x p',
triple (trm_app prim_get [val_loc p; val_field tl])
(p ~> record `{ hd := x; tl := p'})
(fun r => \[r = p'] \* p ~> record `{ hd := x; tl := p'}).
(* TODO: this specification will be computed on the fly using a tactic *)
(********************************************************************)
(* * Definition of the list increment program *)
......@@ -141,9 +152,9 @@ Definition mlist_length : val :=
(** Helper for simplifying substitutions *)
Parameter mlist_length_closed : forall E,
Lemma mlist_length_closed : forall E,
subst_val E mlist_length = mlist_length.
(* todo: prove *)
Admitted. (* todo: automate the proof *)
Hint Rewrite mlist_length_closed : rew_subst.
......@@ -151,15 +162,6 @@ Ltac simpl_subst := simpl; autorewrite with rew_subst.
(** Temporary auxiliary specification *)
Parameter rule_get_tl : forall p x p',
triple (trm_app prim_get [val_loc p; val_field tl])
(p ~> record `{ hd := x; tl := p'})
(fun r => \[r = p'] \* p ~> record `{ hd := x; tl := p'}).
(* TODO: this specification will be computed on the fly using a tactic *)
(********************************************************************)
(* * Mutable list increment verification, using triples *)
......@@ -181,12 +183,13 @@ Proof using.
case_if as C1; case_if as C2; tryfalse.
{ inverts C2. xchange MList_null_keep.
xpull. intros EL. applys rule_val. hsimpl. subst~. }
{ xchange (MList_not_null p). { auto. } xpull. intros x p' L' EL.
{ xchange (MList_not_null p). { auto. }
xpull. intros x p' L' EL.
applys rule_let.
{ xapplys rule_get_tl. }
{ simpl_subst. intros p''. xpull. intros E. subst p''.
applys rule_let.
{ xapplys IH. { subst~. } }
{ simpl_subst. xapplys IH. { subst~. } }
{ simpl_subst. intros r. xpull. intros Er. xchange (MList_uncons p).
subst r. xapplys rule_add. subst. rew_length. fequals. math. } } }
Qed.
......@@ -219,7 +222,7 @@ Lemma mlist_incr_spec' : forall L p,
Proof using.
intros L. induction_wf: list_sub_wf L. intros p.
applys cf_sound_app1 20%nat. reflexivity.
simpl; fold mlist_length.
simpl; fold mlist_length.
applys local_erase. esplit. split.
{ applys local_erase. xapplys rule_neq. }
intros X. xpull. intros EX.
......@@ -291,6 +294,8 @@ Open Scope charac.
(** Record contents *)
(* TODO: use MLCFlifted *)
Notation "`'{ f1 := x1 }" :=
((f1, Dyn x1)::nil)
(at level 0, f1 at level 0)
......@@ -403,30 +408,59 @@ Global Opaque MList.
(********************************************************************)
(* TODO: prove spec of primitives *)
Open Scope charac.
Print Visibility.
(** Args contents *)
Notation "`[ x1 x2 ]" :=
((Dyn x1)::(Dyn x2)::nil)
(at level 0, x1 at level 0, x2 at level 0)
: trm_scope.
Notation "`[ x1 ]" :=
((Dyn x1)::nil)
(at level 0, x1 at level 0)
: trm_scope.
(*
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0)
: trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::(f4, Dyn x4)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
: trm_scope.
*)
Open Scope trm_scope.
Parameter Rule_add : forall (n1 n2:int),
App' prim_add n1 n2;
App prim_add `[n1 n2]
\[]
(fun (r:int) => \[r = (n1 + n2)]).
Parameter Rule_neq : forall (v1 v2:loc),
App' prim_neq v1 v2;
App prim_neq `[v1 v2]
\[]
(fun (r:int) => \[r = (If v1 = v2 then 0 else 1)]).
Parameter Rule_get_tl : forall p A `{EA:Enc A} (x:A) (p':loc),
App' prim_get (p:loc) (tl:field);
Parameter Rule_get_tl : forall (p:loc) A `{EA:Enc A} (x:A) (p':loc),
App prim_get `[p (tl:field)]
(p ~> Record `'{ hd := x; tl := p'})
(fun (r:loc) => \[r = p'] \* p ~> Record `'{ hd := x; tl := p'}).
Hint Extern 1 (RegisterSpec (App' (val_prim prim_get) _ tl; _ _)) =>
Hint Extern 1 (RegisterSpec (App (val_prim prim_get) `[_ tl] _ _)) =>
Provide Rule_get_tl.
Hint Extern 1 (RegisterSpec (App' (val_prim prim_neq) _ _; _ _)) =>
Hint Extern 1 (RegisterSpec (App (val_prim prim_neq) `[_ _] _ _)) =>
Provide Rule_neq.
Hint Extern 1 (RegisterSpec (App' (val_prim prim_add) _ _; _ _)) =>
Hint Extern 1 (RegisterSpec (App (val_prim prim_add) `[_ _] _ _)) =>
Provide Rule_add.
......@@ -437,7 +471,7 @@ Hint Extern 1 (RegisterSpec (App' (val_prim prim_add) _ _; _ _)) =>
Lemma mlist_incr_spec : forall A `{EA:Enc A} (L:list A) (p:loc),
App' mlist_length p;
App mlist_length `[p]
(p ~> MList L)
(fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
......
......@@ -409,3 +409,4 @@ Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
: trm_scope.
(* TODO: "f1 := x1" => record_entry f1 x1 := (f1,x1) *)
\ No newline at end of file
......@@ -194,6 +194,9 @@ Ltac hcancel_hook H ::=
(** Representation predicate [r ~> Record L], where [L]
is an association list from fields to values. *)
(* TODO: record_item := field * dyn
record_items := list record_item
*)
Definition record_descr := list (field * dyn).
Fixpoint Record (L:record_descr) (r:loc) : hprop :=
......
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