Commit 3d98a723 authored by charguer's avatar charguer

fix

parent 63b71f6d
......@@ -935,13 +935,13 @@ and cfg_type_record (name,dec) =
(** Auxiliary function to generate stuff for records *)
and record_functions record_name record_constr repr_name params fields_names fields_types =
and record_functions name record_constr repr_name params fields_names fields_types =
let nth i l = List.nth l i in
let n = List.length fields_names in
let indices = list_nat n in
let for_indices f = List.map f indices in
let new_name = record_make_name record_name in
let new_name = record_make_name name in
let get_names = for_indices (fun i -> record_field_get_name (nth i fields_names)) in
let set_names = for_indices (fun i -> record_field_set_name (nth i fields_names)) in
let new_decl = Coqtop_param (new_name, val_type) in
......@@ -985,9 +985,9 @@ and record_functions record_name record_constr repr_name params fields_names fie
let repr_convert_quantif = [tloc] @ tparams @ tlogicals @ treprs @ tabstracts in
let repr_focus_quantif = repr_convert_quantif in
let repr_unfocus_quantif = [tloc] @ tparams @ tconcretes @ tlogicals @ treprs @ tabstracts in
let convert_name = repr_name ^ "_convert" in
let focus_name = repr_name ^ "_focus" in
let unfocus_name = repr_name ^ "_unfocus" in
let convert_name = record_convert_name name in
let focus_name = record_unfocus_name name in
let unfocus_name = record_focus_name name in
let repr_convert = Coqtop_param (convert_name, coq_foralls repr_convert_quantif repr_convert_body) in
let repr_focus = Coqtop_param (focus_name, coq_foralls repr_focus_quantif repr_focus_body) in
let repr_unfocus = Coqtop_param (unfocus_name, coq_foralls repr_unfocus_quantif repr_unfocus_body) in
......@@ -995,9 +995,9 @@ and record_functions record_name record_constr repr_name params fields_names fie
coqtop_noimplicit convert_name; coqtop_noimplicit focus_name; coqtop_noimplicit unfocus_name ] in
let field_convert_focus_unfocus i =
let field_name = nth i fields_names in
let field_convert_name = "_convert" ^ field_name in
let field_focus_name = "_focus" ^ field_name in
let field_unfocus_name = "_unfocus" ^ field_name in
let field_convert_name = record_convert_field_name field_name in
let field_focus_name = record_focus_field_name field_name in
let field_unfocus_name = record_unfocus_field_name field_name in
let tconcretei = nth i tconcretes in
let helemi = nth i helems_items in
let field_folded = hdata vloc (coq_apps (coq_var_at repr_name) (vparams @ vlogicals @ vreprs @ vabstracts)) in
......@@ -1114,15 +1114,16 @@ and record_functions record_name record_constr repr_name params fields_names fie
[ new_decl ]
@ (List.concat (List.map get_set_decl indices))
(* TODO: revive
@ [ repr_def ]
@ repr_convert_focus_unfocus
@ fields_convert_focus_unfocus
(* TODO: revive *)
(*
@ new_spec
@ (List.concat (List.map get_set_spec indices))
@ (List.concat (List.map get_spec_focus indices))
@ (List.concat (List.map set_spec_unfocus indices))
*)
@ (List.concat (List.map set_spec_unfocus indices)) *)
(** Generate the top-level Coq declarations associated with
......
......@@ -322,7 +322,8 @@ let record_make_name name =
(** Convention for naming record field *)
let record_field_name name =
name (* ^ "__" *) (* TODO: modify? *)
name
(* ^ "__" *) (* TODO: modify? *)
(** Convention for naming record accessor function *)
......@@ -334,18 +335,40 @@ let record_field_set_name name =
(** Convention for naming record accessor function specifications *)
let record_get_name_spec name =
let record_get_spec_name name =
name ^ "__get_spec"
let record_set_name_spec name =
let record_set_spec_name name =
name ^ "__set_spec"
(* TODO: use above, and also focus/unfocus etc *)
(** Convention for naming the representation predicate for a record *)
let record_repr_name name =
str_capitalize_1 name
str_capitalize_1 name ^ "_"
(* this should not clash with types because types being with a lowercase *)
let record_convert_name name =
record_repr_name name ^ "_convert"
let record_focus_name name =
record_repr_name name ^ "_focus"
let record_unfocus_name name =
record_repr_name name ^ "_unfocus"
let record_convert_field_name name =
record_field_name name ^ "__convert"
let record_focus_field_name name =
record_field_name name ^ "__focus"
let record_unfocus_field_name name =
record_field_name name ^ "__unfocus"
(*#########################################################################*)
......
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