Commit 4bf63199 authored by Armaël Guéneau's avatar Armaël Guéneau

Add support for recursive record definitions

parent 94fd1a6b
......@@ -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 *)
......
......@@ -446,8 +446,8 @@ Hint Resolve affine_record_repr : affine.
[app_record_new L] is a characteristic formula describing
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).
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