Commit a619a4fb authored by charguer's avatar charguer

records

parent c0f46a4f
......@@ -17,16 +17,17 @@ MAJOR NEXT
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
- realize array specification using single-cell array specifications
- partial application
- xabstract => rename as xgen
- xabstract => reimplement and rename as xgen
- record with
- when clauses
- xfocus
- implement the work around for type abbreviations:
type typerecb1 = | Typerecb_1 of typerecb2
......@@ -34,6 +35,7 @@ MAJOR NEXT
- support float
- xfocus
MAJOR POSTPONED
......
......@@ -785,7 +785,7 @@ let rec cfg_exp env e =
| Texp_setfield(arg, p, lbl, newval) ->
let ts1 = coq_typ arg in (* todo: check it is always 'loc' *)
let ts2 = coq_typ newval in
let func = Coq_var "CFML.CFApp.record_get" in
let func = Coq_var "CFML.CFApp.record_set" in
let field = Coq_var (record_field_name lbl.lbl_name) in
Cf_app ([ts1; coq_nat; ts2], coq_unit, func, [lift arg; field; lift newval])
(* DEPRECATED
......
open Mytools
(**
Naming scheme:
TRANSLATION
- var x x
- infix fun (++) infix_plus_plus__
- fresh var x3__
- fresh fun f3__
- fresh pat p3__
- clashing var exists exists__
- clashing var array array__
- var quote x' x'__ // Same rule as clashing var
- var rejected x_ // Cannot end with underscore
- var rejected x_' // (even if a quote follows)
- constructor C C
- rejected cstr C_ // Reject for conflict with A_
- builtin type t t
- type t t_
- type quote t' t'_ // Same rule as above (not special).
- type rejected t_
- type var 'a A_
- field name f f' // Short field names are convienient
- field quote f' f'_'
- rejected field f_
- module M M_ml
INTERPRETATION
M_ml module name (in Coq module scope)
X constructor
X_ type variable
t_ builtin type
f' field name
x__ escaped name for variable x, where x is a keyword
x1__ name for a fresh variable
infix..__ name for infix symbol
x'__ escaped name for variable x' // general rule for escaped name
t'_ escaped name for type t' // general rule for types
f'_' escaped name for field name f' // new rule for escaping field names
// TODO: implement support for variables ending with a quote; currently rejected
*)
(*#########################################################################*)
......@@ -9,13 +63,16 @@ let check_var loc x =
(* Reject program containing variables with a trailing underscore,
as we use such an underscore to disambiguate with type variables *)
let n = String.length x in
if n > 0 && x.[n-1] = '\''
then unsupported loc ("variable name should not end with a quote (not yet supported): " ^ x);
if n > 0 && x.[n-1] = '_'
then unsupported loc ("variables names should not end with an underscore: " ^ x);
then unsupported loc ("variable name should not end with an underscore: " ^ x);
if (not !Clflags.nopervasives)
&& (List.mem x ["mod"; "/"; "&&"; "||"; "="; "<>"; "<="; ">="; "<"; ">"; "min"; "max"])
then unsupported loc ("CFML requires -nopervasives to allow binding of operator: " ^ x)
(* --is this line needed? if loc.loc_ghost then () else *)
(*#########################################################################*)
......@@ -319,6 +376,9 @@ let record_field_name name =
(** Convention for naming record accessor function *)
let record_field_name name =
let n = String.length name in
if n > 0 && name.[n-1] = '\''
then unsupported_noloc ("field name should not end with a quote (not yet supported): " ^ name);
name ^ "'"
(* TODO: avoid names ending with a quote in caml code *)
......
......@@ -428,8 +428,8 @@ Fixpoint record_repr (L:record_descr) (r:loc) : hprop :=
[app_record_new L] is a characteristic formula describing
the allocation of a record. *)
Definition app_record_new (L:record_descr) (H:hprop) (Q:loc->hprop) :=
(fun r => H \* r ~> record_repr L) ===> Q.
Definition app_record_new (L:record_descr) : ~~loc :=
local (fun H Q => (fun r => H \* r ~> record_repr L) ===> Q).
(* Remark: taking the definition below would be a bit of a hack,
and it turns out that Coq rejects the definition for universe
......@@ -658,97 +658,10 @@ Qed. (* todo: could use xapply in this proof *)
Qed.
*)
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.
Global Opaque record_repr.
Ltac xspec_record_set_compute_for f w L :=
let G := fresh in
forwards G: (record_set_compute_spec_correct f w L);
[ reflexivity | revert G ].
Ltac xspec_record_set_compute tt :=
match goal with |- app record_set [?r ?f ?w] (?r ~> record_repr ?L) _ =>
xspec_record_set_compute_for f w L end.
(********************************************************************)
(** DEMOS *)
Definition demo_arglist :=
forall f (xs:list int) (x y:int) B H (Q:B->hprop),
app f [ x y ] H Q.
(* Print demo_arglist. *)
(* TODO: find a way that the parentheses are not printed around "app" *)
Module RecordDemo.
Definition f := 0%nat.
Definition g := 1%nat.
Definition demo1 r :=
r ~> `{ f := 1+1 ; g := 1 }.
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.
*)
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_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_set_1 : forall r,
(forall H',
app record_set [r f 4] (r ~> `{ f := 1+1 ; g := 1 }) (#H') -> True)
-> True.
Proof using.
introv M. applys (rm M).
xspec_record_set_compute tt. intros G. apply G.
Qed.
End RecordDemo.
......
......@@ -323,6 +323,79 @@ Qed.
(********************************************************************)
(** App and Records *)
Require Import CFApp CFTactics.
Definition demo_arglist :=
forall f (xs:list int) (x y:int) B H (Q:B->hprop),
app f [ x y ] H Q.
(* Print demo_arglist. *)
(* TODO: find a way that the parentheses are not printed around "app" *)
Module RecordDemo.
Definition f := 0%nat.
Definition g := 1%nat.
Definition demo1 r :=
r ~> `{ f := 1+1 ; g := 1 }.
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.
*)
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_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_set_1 : forall r,
(forall H',
app record_set [r f 4] (r ~> `{ f := 1+1 ; g := 1 }) (#H') -> True)
-> True.
Proof using.
introv M. applys (rm M).
xspec_record_set_compute tt. intros G. apply G.
Qed.
End RecordDemo.
......
......@@ -2433,6 +2433,38 @@ Tactic Notation "xmatch" constr(Q) :=
(********************************************************************)
(* ** Tactics for Applications *)
(*--------------------------------------------------------*)
(* ** [xspec_record] *)
(* Auxiliary tactics for building specifications for record accesses *)
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_set_compute_for f w L :=
let G := fresh in
forwards G: (record_set_compute_spec_correct f w L);
[ reflexivity | revert G ].
(* extract the record contents *)
Ltac xspec_record_repr_compute H :=
match H with context [ ?r ~> record_repr ?L ] => constr:(L) end.
Ltac xspec_record_get_compute tt :=
match goal with |- app record_get [?r ?f] ?H _ =>
let L := xspec_record_repr_compute H in
xspec_record_get_compute_for f L end.
Ltac xspec_record_set_compute tt :=
match goal with |- app record_set [?r ?f ?w] ?H _ =>
let L := xspec_record_repr_compute H in
xspec_record_set_compute_for f w L end.
(*--------------------------------------------------------*)
(* ** [xspec] *)
......@@ -2479,8 +2511,16 @@ Ltac xspec_app_in_hyps f :=
Ltac xspec_in_core db f :=
ltac_database_get db f.
Ltac xspec_for_record f :=
match f with
| record_get => xspec_record_get_compute tt
| record_set => xspec_record_set_compute tt
end.
(* Note: if [f] is a record function, it needs to be the application visible in the goal *)
Ltac xspec_core f :=
first [ xspec_in_hyps_core f
first [ xspec_for_record f
| xspec_in_hyps_core f
(* FUTURE: | xspec_in database_spec_credits f *)
| xspec_in_core database_spec f
| xspec_app_in_hyps f
......@@ -2497,6 +2537,7 @@ Ltac cfml_apply_xseq_or_xlet_to_reveal_app cont :=
match cfml_get_tag tt with
| tag_let => xlet; [ cont tt | ]
| tag_seq => xseq; [ cont tt | ]
| tag_apply => xuntag tag_apply; cont tt
| tag_none_app => cont tt
| _ => fail 2 "xspec expects the goal to be an application"
end.
......@@ -2516,6 +2557,36 @@ Tactic Notation "xspec" :=
xspec f).
(*--------------------------------------------------------*)
(* ** [xrecord_new] *)
(** [xrecord_new] applies to goals of the form [(AppNew `{ f := v }) H Q].
There is no need to call this tactic directly; prefer using [xapp]. *)
Lemma xrecord_new_lemma_unify : forall L H,
(app_record_new L) H (fun r => H \* r ~> record_repr L).
Proof using.
intros. apply~ local_erase.
Qed.
Lemma xrecord_new_lemma_weaken : forall L H (Q:loc->hprop),
(fun r => H \* r ~> record_repr L) ===> Q \*+ \GC ->
(app_record_new L) H Q.
Proof using.
introv W. unfolds. xgc_post. applys~ local_erase. auto.
Qed.
Ltac xrecord_new_core tt :=
xuntag tag_record_new;
match cfml_postcondition_is_evar tt with
| false => apply xrecord_new_lemma_weaken
| true => apply xrecord_new_lemma_unify
end.
Tactic Notation "xrecord_new" :=
xrecord_new_core tt.
(*--------------------------------------------------------*)
(* ** [xapp] *)
......@@ -2623,11 +2694,17 @@ Ltac xapp_use_or_find H Sf :=
Ltac xapp_prepare_goal cont :=
xextract_check_not_needed tt;
let cont2 tt := instantiate; try xextract in
let inner tt :=
match cfml_get_tag tt with
| tag_apply => xuntag tag_apply; cont tt; xtag_goal
| tag_none_app => cont tt; xtag_goal
| tag_record_new => xrecord_new
end
in
match cfml_get_tag tt with
| tag_let => xlet; [ xuntag tag_apply; cont tt | cont2 tt ]
| tag_seq => xseq; [ xuntag tag_apply; cont tt | cont2 tt ]
| tag_apply => xuntag tag_apply; cont tt; xtag_goal
| tag_none_app => cont tt; xtag_goal
| tag_let => xlet; [ inner tt | cont2 tt ]
| tag_seq => xseq; [ inner tt | cont2 tt ]
| _ => inner tt
end.
Ltac xapp_instantiate Sf args :=
......@@ -2690,14 +2767,20 @@ Ltac xapp_no_simpl_core_no_spec E cont :=
(* [xapps] implementation *)
Ltac xapps_core H E cont :=
Ltac xapps_core H E cont :=
let cont1 tt := xapp_core H E cont in
let cont2 tt := instantiate; try xextract; try intro_subst in
let cont2 tt := instantiate; try xextract; try intro_subst in
let inner tt :=
match cfml_get_tag tt with
| tag_apply => xuntag tag_apply; xapp_core H E cont
| tag_none_app => xapp_core H E cont
| tag_record_new => xrecord_new
end
in
match cfml_get_tag tt with
| tag_let => xlet; [ xuntag tag_apply; cont1 tt | cont2 tt ]
| tag_seq => xseq; [ xuntag tag_apply; cont1 tt | cont2 tt ]
| tag_apply => xuntag tag_apply; xapp_core H E cont
| tag_none_app => xapp_core H E cont
| tag_let => xlet; [ inner tt | cont2 tt ]
| tag_seq => xseq; [ inner tt | cont2 tt ]
| _ => inner tt
end.
(* [xapp as X] implementation *)
......
......@@ -179,62 +179,17 @@ Definition Ref a (v:a) (r:loc) :=
Notation "r '~~>' v" := (hdata (Ref v) r)
(at level 32, no associativity) : heap_scope.
(*
Definition app_record_new (L:record_descr) (H:hprop) (Q:loc->hprop) :=
(fun r => H \* r ~> record_repr L) ===> Q.
*)
Lemma xnew_lemma_unify : forall L H,
local (app_record_new L) H (fun r => H \* r ~> record_repr L).
Proof using.
intros. apply~ local_erase. intros r. hsimpl.
Qed.
(* TODO
Lemma xret_lemma_weaken : forall L H (Q:loc->hprop),
(fun r => H \* r ~> record_repr L) ===> Q \*+ \GC ->
local (app_record_new L) H Q.
Proof using.
introv W. eapply (@local_gc_pre_on (\GC)).
auto.
specializes W r.
apply~ local_erase. intros r. hsimpl.
Qed.
*)
Ltac xnew_core tt :=
xuntag tag_record_new;
match cfml_postcondition_is_evar tt with
| false => xpost; apply xnew_lemma_unify
(* apply xnew_lemma_weaken *)
| true => apply xnew_lemma_unify
end.
Tactic Notation "xnew" :=
xnew_core tt.
Lemma ref_spec : forall a (v:a),
app ref [v] \[] (fun r => r ~~> v).
Proof using.
xcf. xuntag tag_record_new. (* TODO : need local *)
xpost; [ try xlocal | | ]. skip. skip.
(* apply xnew_lemma_unify.
xnew. xapp.
*)
TODO
Qed.
Proof using. xcf_go~. Qed.
Lemma infix_emark__spec : forall a (v:a) r,
app_keep infix_emark_ [r] (r ~~> v) \[= v].
Proof using.
xcf. skip.
Qed.
Proof using. xunfold Ref. xcf_go~. Qed.
Lemma infix_colon_eq__spec : forall a (v w:a) r,
app infix_colon_eq_ [r w] (r ~~> v) (# r ~~> w).
Proof using.
xcf. skip.
Qed.
Proof using. xunfold Ref. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec infix_emark_) => Provide infix_emark__spec.
......@@ -250,15 +205,11 @@ Notation "'App'' r `:= x" := (App infix_colon_eq_ r x;)
Lemma incr_spec : forall (n:int) r,
app incr [r] (r ~~> n) (# r ~~> (n+1)).
Proof using.
xcf. xgo~.
Qed.
Proof using. xcf_go~. Qed.
Lemma decr_spec : forall (n:int) r,
app decr [r] (r ~~> n) (# r ~~> (n-1)).
Proof using.
xcf. xgo~.
Qed.
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.
......@@ -269,15 +220,11 @@ Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.
Lemma fst_spec : forall A B (x:A) (y:B),
app fst [(x,y)] \[] \[= x].
Proof using.
xcf. xgo~.
Qed.
Proof using. xcf_go~. Qed.
Lemma snd_spec : forall A B (x:A) (y:B),
app snd [(x,y)] \[] \[= y].
Proof using.
xcf. xgo~.
Qed.
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec fst) => Provide fst_spec.
Hint Extern 1 (RegisterSpec snd) => Provide snd_spec.
......@@ -288,9 +235,7 @@ Hint Extern 1 (RegisterSpec snd) => Provide snd_spec.
Lemma ignore_spec :
app ignore [tt] \[] \[= tt].
Proof using.
xcf. xgo~.
Qed.
Proof using. xcf_go~. Qed.
Hint Extern 1 (RegisterSpec ignore) => Provide ignore_spec.
......
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