Commit 8bdc41ec authored by Armaël Guéneau's avatar Armaël Guéneau

Merge branch 'recursive-records-2' into 'master'

Add support for recursive record definitions

See merge request !3
parents 94fd1a6b a412185c
......@@ -795,6 +795,19 @@ type ('a,'b) recordb =
-- else would need to prefix all fields with the type... *)
(********************************************************************)
(* ** Recursive definitions are supported for heap-allocated records *)
type 'a node = {
mutable data : 'a;
mutable prev : 'a node;
mutable next : 'a node;
}
let create_cyclic_node (data: 'a): 'a node =
let rec node = { data; prev = node; next = node } in
node
(********************************************************************)
(* ** Type mutual *)
......
......@@ -1353,6 +1353,15 @@ Qed.
Definition Sitems A (L:list A) r :=
Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
(********************************************************************)
(* ** Recursive records definitions *)
Lemma create_cyclic_node_spec : forall (A:Type) (data:A),
app create_cyclic_node [data]
PRE \[]
POST (fun (r: loc) => r ~> `{ data' := data; prev' := r; next' := r }).
Proof using. xcf_go~. Qed.
(*
Section ProjLemma.
Variables (B:Type) (A1 : Type).
......
......@@ -700,27 +700,8 @@ let rec cfg_exp env e =
| Texp_construct(p, cstr, args) -> ret e
(* TODO: only in purely function setting: | Texp_record (lbl_expr_list, opt_init_expr) -> ret e*)
| Texp_record (lbl_expr_list, opt_init_expr) ->
if opt_init_expr <> None then unsupported loc "record-with";
let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
let build_arg (name, arg) =
let value = coq_apps coq_dyn_at [coq_typ loc arg; lift arg] in
Coq_tuple [Coq_var (record_field_name name); value]
in
let arg = coq_list (List.map build_arg named_args) in
Cf_record_new (arg)
(* DEPRECATED
let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
let func = Coq_var (pathfront ^ (record_make_name pathend)) in
let fields_names = extract_label_names_scimple e.exp_env e.exp_type in
let args =
try List.map (fun name -> List.assoc name named_args) fields_names
with Not_found -> failwith "some fields are missing in a record construction"
in
let tprod = coq_prod (List.map coq_typ args) in
Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)])
*)
| Texp_record (_, _) ->
cfg_record env e
| Texp_apply (funct, oargs) when (exp_find_inlined_primitive funct oargs <> None) -> ret e
......@@ -734,6 +715,12 @@ let rec cfg_exp env e =
| Texp_constraint ({exp_desc = Texp_function (_,_,_)},_,_) -> true (* todo: generalize *)
| _ -> false in
let is_let_record_new =
match (snd (List.hd pat_expr_list)).exp_desc with
| Texp_record (_,_) -> true
| Texp_constraint ({exp_desc = Texp_record (_,_)},_,_) -> true (* todo: generalize *)
| _ -> false in
(* binding of functions, possibly mutually-recursive *)
if is_let_fun then begin
let env' = match rf with
......@@ -789,7 +776,13 @@ let rec cfg_exp env e =
begin
let cf1 = cfg_exp env bod in
let cf1 =
(* Recursive record term let-binding *)
if is_let_record_new && rf = Recursive then
cfg_record ~record_name:x env bod
else
cfg_exp env bod
in
let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
(* fvs_typ contains all free type variables in the type;
and thus too many w.r.t. to the ones of interest here *)
......@@ -950,6 +943,33 @@ and cfg_func env fvs pat bod =
(* --todo: check if the set of type variables quantified is not too
conservative. Indeed, some type variables may no longer occur. *)
and cfg_record ?(record_name = "_") env e =
let loc = e.exp_loc in
match e.exp_desc with
| Texp_record (lbl_expr_list, opt_init_expr) ->
if opt_init_expr <> None then unsupported loc "record-with";
let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
let build_arg (name, arg) =
let value = coq_apps coq_dyn_at [coq_typ loc arg; lift_val env arg] in
Coq_tuple [Coq_var (record_field_name name); value]
in
let arg =
Coq_fun ((record_name, coq_var "CFHeaps.loc"),
coq_list (List.map build_arg named_args)) in
Cf_record_new (arg)
(* DEPRECATED
let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
let func = Coq_var (pathfront ^ (record_make_name pathend)) in
let fields_names = extract_label_names_scimple e.exp_env e.exp_type in
let args =
try List.map (fun name -> List.assoc name named_args) fields_names
with Not_found -> failwith "some fields are missing in a record construction"
in
let tprod = coq_prod (List.map coq_typ args) in
Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)])
*)
| _ -> assert false
(*#########################################################################*)
(* ** Characteristic formulae for modules *)
......
......@@ -444,10 +444,14 @@ Hint Resolve affine_record_repr : affine.
(* Axiomatic specification of [new] on a list of fields;
[app_record_new L] is a characteristic formula describing
the allocation of a record. *)
the allocation of a record.
Definition app_record_new (L:record_descr) : ~~loc :=
local (fun H Q => (fun r => H \* r ~> record_repr L) ===> Q).
[L] takes the name of the record as an argument: this is useful for records
defined recursively, where fields can point to the record itself. In the
non-recursive case, [L] will be of the form [fun _ => ...]. *)
Definition app_record_new (L:loc -> record_descr) : ~~loc :=
local (fun H Q => (fun r => H \* r ~> record_repr (L r)) ===> Q).
(* Remark: taking the definition below would be a bit of a hack,
and it turns out that Coq rejects the definition for universe
......
......@@ -3009,13 +3009,13 @@ Tactic Notation "xspec" :=
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).
(app_record_new L) H (fun r => H \* r ~> record_repr (L r)).
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 ->
(fun r => H \* r ~> record_repr (L r)) ===> Q \*+ \GC ->
(app_record_new L) H Q.
Proof using.
introv W. unfolds. xgc_post. applys~ local_erase. auto.
......
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