Commit ee61420a authored by charguer's avatar charguer
Browse files

record_trick

parent 506e9b84
......@@ -5,7 +5,7 @@
URGENT
- record generation breaks circularity through use of "loc" systematically for records
SANITY
......@@ -20,17 +20,32 @@ SANITY
else if name = "exists" then "exists__"
else if name = "forall" then "forall__"
- prevent rebinding of List
- restriction on not binding "min" and "max" might be a bit restrictive..
COMPILATION
- In the makefile.Coq, when building the .vq and obtaining
"Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
=> then delete the .vio file
(useful for compilations interrupted using CTRL+C)
=> even better, wrap "coqc -quick" with an atomic commit of its result.
LATER
- prevent rebinding of List
- restriction on not binding "min" and "max" might be a bit restrictive..
- implement the work around for type abbreviations:
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
=> idea: inline the abbreviation automatically (abbreviation should not be cyclic though)
=> for now, do this encoding by hand.
- add support for pure records
......
......@@ -656,7 +656,7 @@ Lemma order_list_spec :
Proof using. xcf_go*. Qed.
Lemma order_tuple_spec :
app order_tuple [tt] \[] \[= 1::1::nil].
app order_tuple [tt] \[] \[= (1,1)].
Proof using. xcf_go*. Qed.
(* TODO:
......
......@@ -3,6 +3,39 @@ Require Import LibCore LibEpsilon Shared.
Require Import CFHeaps.
Hint Extern 1 (_ ===> _) => apply rel_le_refl.
(* TODO: make this a local hint? xauto should take care of this. *)
(********************************************************************)
(* ** Axioms of CFML *)
(** Note: these axioms could in theory be realized by constructing
a deep embedding of the target programming language.
See Arthur Chargueraud's PhD thesis for full details. *)
(** The type Func, used to represent functions *)
Axiom func : Type.
(** The type Func is inhabited *)
Axiom func_inhab : Inhab func.
Existing Instance func_inhab.
(** The evaluation predicate for functions: [eval f v h v' h'],
asserts that the evaluation of the application of [f] to [v]
in a heap [h] terminates and produces a value [v'] in a heap [h']. *)
Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.
(********************************************************************)
......@@ -36,30 +69,6 @@ Hint Extern 1 (_ ===> _) => apply rel_le_refl.
*)
(********************************************************************)
(* ** Axioms of CFML *)
(** Note: these axioms could in theory be realized by constructing
a deep embedding of the target programming language.
See Arthur Chargueraud's PhD thesis for full details. *)
(** The type Func, used to represent functions *)
Axiom func : Type.
(** The type Func is inhabited *)
Axiom func_inhab : Inhab func.
Existing Instance func_inhab.
(** The evaluation predicate for functions: [eval f v h v' h'],
asserts that the evaluation of the application of [f] to [v]
in a heap [h] terminates and produces a value [v'] in a heap [h']. *)
Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.
(********************************************************************)
(* ** Definition and properties of the primitive app predicate *)
......@@ -118,10 +127,12 @@ Hint Resolve app_basic_local.
(********************************************************************)
(* ** Generic notation for list of dyns *)
(* DEPRECATED
Notation "'Dyn' x" := (@dyn _ x) (at level 0).
*)
Notation "[ x1 ]" := ((dyn x1)::nil)
(at level 0, x1 at level 00) : dynlist.
(at level 0, x1 at level 0) : dynlist.
Notation "[ x1 x2 ]" := ((dyn x1)::(dyn x2)::nil)
(at level 0, x1 at level 0, x2 at level 0) : dynlist.
Notation "[ x1 x2 x3 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::nil)
......@@ -404,3 +415,325 @@ Definition spec (f:func) (n:nat) (P:Prop) :=
Global Opaque app_def curried.
(********************************************************************)
(* ** Xunfold tactics *)
Tactic Notation "ltac_set" "(" ident(X) ":=" constr(E) ")" "at" constr(K) :=
match nat_from_number K with
| 1%nat => set (X := E) at 1
| 2%nat => set (X := E) at 2
| 3%nat => set (X := E) at 3
| 4%nat => set (X := E) at 4
| 5%nat => set (X := E) at 5
| 6%nat => set (X := E) at 6
| 7%nat => set (X := E) at 7
| 8%nat => set (X := E) at 8
| 9%nat => set (X := E) at 9
| 10%nat => set (X := E) at 10
| 11%nat => set (X := E) at 11
| 12%nat => set (X := E) at 12
| 13%nat => set (X := E) at 13
| _ => fail "ltac_set: arity not supported"
end.
(** [Xunfold at n] unfold the definition of the arrow [~>]
at the occurence [n] in the goal. *)
Definition hdata' (A:Type) (S:A->hprop) (x:A) : hprop := S x.
Tactic Notation "Xunfold" "at" constr(n) :=
let h := fresh "temp" in
ltac_set (h := hdata) at n;
change h with hdata';
unfold hdata';
clear h.
(** [Xunfold_clean] simplifies instances of
[p ~> (fun _ => _)] by unfolding the arrow,
but only when the body does not captures
locally-bound variables.
TODO: deprecated *)
Tactic Notation "Xunfold_clean" :=
try match goal with |- context C [?p ~> ?E] =>
match E with (fun _ => _) =>
let E' := eval cbv beta in (E p) in
let G' := context C [E'] in
let G := match goal with |- ?G => G end in
change G with G' end end.
(** [Xunfold E] unfolds all occurences of the representation
predicate [E].
Limitation: won't work if E has more than 12 arguments.
Implementation: converts all occurences of hdata to hdata',
then unfolds these occurences one by one, and considers
them for unfolding. *)
Tactic Notation "Xunfold" constr(E) :=
change hdata with hdata';
let h := fresh "temp" in
set (h := hdata');
repeat (
unfold h at 1;
let ok := match goal with
| |- context [ hdata' (E) _ ] => constr:(true)
| |- context [ hdata' (E _) _ ] => constr:(true)
| |- context [ hdata' (E _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| _ => constr:(false)
end in
match ok with
| true => unfold hdata'
| false => change hdata' with hdata
end);
clear h;
unfold E.
(** [Xunfold E] unfolds a specific occurence of the representation
predicate [E]. TODO: still needs to unfold [E] by hand. *)
Tactic Notation "Xunfold" constr(E) "at" constr(n) :=
let n := nat_from_number n in
change hdata with hdata';
let h := fresh "temp" in
set (h := hdata');
let E' := fresh "tempR" in
set (E' := E);
let rec aux n :=
try (
unfold h at 1;
let ok := match goal with
| |- context [ hdata' (E') _ ] => constr:(true)
| |- context [ hdata' (E' _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| _ => constr:(false)
end in
match ok with
| true =>
match n with
| (S O)%nat =>
unfold hdata'
| (S ?n')%nat => change hdata' with hdata; aux n'
end
| false => change hdata' with hdata; aux n
end)
in
aux n;
unfold h;
clear h;
change hdata' with hdata;
unfold E';
clear E'.
(********************************************************************)
(* Representation of records *)
Definition record_descr := list (nat * dynamic).
(* DEPRECATED
Axiom record_repr : record_descr -> loc -> hprop.
Definition record_repr_one (f:nat) A (v:A) (r:loc) : hprop :=
r ~> record_repr ((f, dyn v)::nil).
*)
Axiom record_repr_one : forall (f:nat) A (v:A) (r:loc), hprop.
Fixpoint record_repr (L:record_descr) (r:loc) : hprop :=
match L with
| nil => \[]
| (f, dyn v)::L' => r ~> record_repr_one f v \* r ~> record_repr L'
end.
(* NOT USED
Definition fields_type := list dynamic.
*)
Notation "`{ f1 := x1 }" := ((f1, dyn x1)::nil)
(at level 0, f1 at level 0) : record_scope.
Notation "`{ f1 := x1 ; f2 := x2 }" := ((f1, dyn x1)::(f2, dyn x2)::nil)
(at level 0, f1 at level 0, f2 at level 0) : record_scope.
Delimit Scope record_scope with record_scope.
Notation "'rec' L" :=
(@record_repr (L)%record_scope) (* (@app_def f (xs)%dynlist _) *)
(at level 69) : charac.
Open Scope charac.
Notation "`{ f1 := x1 }" := (rec `{ f1 := x1 })
(at level 0, f1 at level 0) : charac.
Notation "`{ f1 := x1 ; f2 := x2 }" := (rec `{ f1 := x1 ; f2 := x2 })
(at level 0, f1 at level 0, f2 at level 0) : charac.
(*
Notation "\{ f1 := x1 ; f2 := x2 ; f3 := x3 }" := ((dyn x1)::(dyn x2)::(dyn x3)::nil)
(at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : record_scope.
Notation "[ x1 x2 x3 x4 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::nil)
(at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0) : record_scope.
Notation "[ x1 x2 x3 x4 x5 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::(dyn x5)::nil)
(at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0, x5 at level 0) : record_scope.
*)
(*Bind Scope dynlist with list.*)
(* Axiomatic access in record fields *)
Axiom record_get : func.
Axiom record_get_spec : forall (r:loc) (f:nat) A (v:A),
app_keep record_get [r f] (r ~> record_repr_one f v) \[= v].
Axiom record_set_spec : forall (r:loc) (f:nat) A (v w:A),
app record_get [r f w] (r ~> record_repr_one f v) (# r ~> record_repr_one f w).
Fixpoint record_get_compute_dyn (f:nat) (L:record_descr) : option dynamic :=
match L with
| nil => None
| (f',d')::L' => if Nat.eq_dec f f' then Some d' else record_get_compute_dyn f L'
end.
Definition record_get_compute_spec (f:nat) (L:record_descr) : option Prop :=
match record_get_compute_dyn f L with
| None => None
| Some (dyn v) => Some (forall r,
app_keep record_get [r f] (r ~> record_repr L) \[= v])
end.
Lemma record_get_compute_spec_correct : forall f L (P:Prop),
record_get_compute_spec f L = Some P -> P.
Proof using.
introv M. unfolds record_get_compute_spec.
sets_eq <- do E: (record_get_compute_dyn f L).
destruct do as [[T v]|]; inverts M.
induction L as [|[f' [T' d']] L']; [false|].
simpl in E.
intros r. do 2 Xunfold record_repr at 1. simpl. case_if.
{ inverts E.
eapply local_frame.
{ apply app_local. auto_false. }
{ apply record_get_spec. }
{ hsimpl. }
{ hsimpl~. } }
{ specializes IHL' (rm E).
eapply local_frame.
{ apply app_local. auto_false. }
{ apply IHL'. }
{ hsimpl. }
{ hsimpl~. } }
Qed. (* todo: could use xapply in this proof *)
Lemma record_get_compute_spec_correct' : forall f L,
match record_get_compute_spec f L with
| None => True
| Some P => P
end.
Proof using.
intros. cases (record_get_compute_spec f L).
applys* record_get_compute_spec_correct. auto.
Qed.
Module RecordDemo.
Definition f := 0%nat.
Definition g := 1%nat.
Definition demo1 r :=
r ~> `{ f := 1+1 ; g := 1 }.
Ltac xspec_record_get_compute_for f L :=
let G := fresh in
forwards G: (record_get_compute_spec_correct f L);
[ reflexivity | revert G ].
Ltac xspec_record_get_compute tt :=
match goal with |- app record_get [?r ?f] (?r ~> record_repr ?L) _ =>
xspec_record_get_compute_for f L end.
Lemma demo_get_3 : forall r,
app_keep record_get [r g] (r ~> `{ g := 1 }) \[= 1].
Proof using.
intros.
xspec_record_get_compute tt. intros G. apply G.
Qed.
Lemma demo_get_2 : forall r,
app_keep record_get [r g] (r ~> `{ f := 1+1 ; g := 1 }) \[= 1].
Proof using.
intros.
xspec_record_get_compute tt. intros G. apply G.
Qed.
Lemma demo_get_1 : forall r,
app_keep record_get [r f] (r ~> `{ f := 1+1 ; g := 1 }) \[= 2].
Proof using.
intros.
xspec_record_get_compute tt. intros G. apply G.
Qed.
(* details 1:
match goal with |- app record_get [?r ?f] (?r ~> record_repr ?L) _ =>
pose (demo_L := L); pose (demo_f := f) end.
forwards G: (record_get_compute_spec_correct demo_f demo_L);
[ reflexivity |].
subst demo_f demo_L.
apply G.
*)
(* details 2:
let R := eval hnf in (record_get_compute_spec demo_f demo_L) in
match R with
| None => fail 2 "field not found for record_get"
| Some ?P => pose P
end.
let G := fresh "HP" in assert (G: P).
apply (@record_get_compute_spec_correct demo_f demo_L). reflexivity.
subst P.
subst demo_f demo_L.
apply G.
*)
End RecordDemo.
......@@ -499,7 +499,7 @@ Tactic Notation "xclean" :=
*)
Ltac xok_core cont := (* see [xok] spec further *)
solve [ cbv beta; apply rel_le_refl
solve [ hnf; apply rel_le_refl
| apply pred_le_refl
| apply hsimpl_to_qunit; reflexivity
| hsimpl; cont tt ].
......@@ -1461,11 +1461,6 @@ Tactic Notation "xval_st" constr(P) :=
should take the form [fun f => spec_of_f].
When this tactic fails, try
[xfun_no_simpl P as f Sf. intros. xapp_types. apply Sf.]
- [xfun_no_simpl P] is like the above but does not attempt to
automatically exploit the most general specification for
proving the special specification. Use [xapp] or [apply]
to continue the proof.
- [xfun_ind R P] is a shorthand for proving a recursive function
by well-founded induction on the first argument quantified in [P].
......@@ -1475,12 +1470,23 @@ Tactic Notation "xval_st" constr(P) :=
shown well-founded. Typical relation includes [downto 0]
and [upto n] for induction on the type [int].
- [xfun_no_simpl P] is like [xfun P] but does not attempt to
automatically exploit the most general specification for
proving the special specification. Use [xapp] or [apply]
to continue the proof.
- [xfun_ind_no_simpl R P] is like [xfun_ind R P] but does not
attempt to automatically exploit the most general specification
for proving the special specification. Use [xapp] or [apply]
to continue the proof.
- Also available:
[xfun P as f]
[xfun P as f Hf]
[xfun_no_simpl P as f]
[xfun_no_simpl P as f Hf]
[xfun_ind R P as IH]
[xfun_ind_nos_impl R P as IH]
*)
......@@ -1562,15 +1568,23 @@ Tactic Notation "xfun_no_simpl" constr(P) "as" ident(f) :=
Tactic Notation "xfun_no_simpl" constr(P) "as" ident(f) ident(Hf) :=
xfun_spec_as_2 P f Hf ltac:(fun _ => idtac).
(* TODO: support higher number of mutually recursive functions. *)
(* Internal: [xfun_ind_core_no_simpl_then R P IH cont]
is like [xfun_no_simpl], followed by a call to well-founded
induction on relation [R] with induction principle called [IH],
followed by a call to [cont] on the CF associated with the function. *)
Ltac xfun_ind_core R P IH :=
Ltac xfun_ind_core_no_simpl_then R P IH cont :=
xfun_spec_as_0 P ltac:(fun Hf =>
intro;
let X := get_last_hyp tt in
induction_wf_core_then IH R X ltac:(fun _ =>
intros; apply (proj2 Hf); clear Hf
)).
induction_wf_core_then IH R X ltac:(fun _ => cont Hf)).
Ltac xfun_ind_core_no_simpl R P IH :=
xfun_ind_core_no_simpl_then R P IH ltac:(fun Hf => idtac).
Ltac xfun_ind_core R P IH :=
xfun_ind_core_no_simpl_then R P IH ltac:(fun Hf =>
intros; apply (proj2 Hf); clear Hf).
Tactic Notation "xfun_ind" constr(R) constr(S) "as" ident(IH) :=
xfun_ind_core R S IH.
......@@ -1578,6 +1592,11 @@ Tactic Notation "xfun_ind" constr(R) constr(S) "as" ident(IH) :=
Tactic Notation "xfun_ind" constr(R) constr(S) :=
let IH := fresh "IH" in xfun_ind R S as IH.
Tactic Notation "xfun_ind_no_simpl" constr(R) constr(S) "as" ident(IH) :=
xfun_ind_core_no_simpl R S IH.
Tactic Notation "xfun_ind_no_simpl" constr(R) constr(S) :=
let IH := fresh "IH" in xfun_ind_core_no_simpl R S IH.
(*--------------------------------------------------------*)
......
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