Commit c8ee1439 authored by charguer's avatar charguer

mutual_typedef

parent 440e2396
......@@ -7,10 +7,6 @@ MAJOR TODAY
- loops
- mutual type defs
record generation breaks circularity through use of "loc" systematically for records
MAJOR NEXT
- record single field and array single cell notation
......
......@@ -590,7 +590,7 @@ and 'a typerecd2 =
| Typerecd_2a
| Typerecd_2b of 'a typerecd1
| Typerecd_2c of 'a typerecd3
type 'a typerecd3 = { typerecd3_f : 'a typerecd2 }
and 'a typerecd3 = { typerecd3_f : 'a typerecd2 }
......@@ -604,6 +604,7 @@ module ModFoo = struct
end
(********************************************************************)
(* ** Local module signature *)
......
......@@ -949,7 +949,7 @@ let rec cfg_structure_item s : cftops =
unsupported loc ("mutually-recursive values that are not all functions");
| Tstr_type(decls) -> [ Cftop_coqs (cfg_type_decls decls) ]
| Tstr_type(decls) -> [ Cftop_coqs (cfg_type_decls loc decls) ]
| Tstr_module(id, modl) -> cfg_module id modl
......@@ -987,7 +987,7 @@ and cfg_type_abbrev (name,dec) =
| None -> [Coqtop_param (x, sort)]
| Some t -> [Coqtop_def ((x, sort), coq_fun_types args (lift_typ_exp t));
Coqtop_hint_unfold ([x],"typeclass_instances") ] in
coqs, []
coqs
(** Generate the top-level Coq declarations associated with
a record definition. *)
......@@ -1010,19 +1010,19 @@ and cfg_type_record (name,dec) =
(* todo: assert remaining_params included in declared_params *)
(* TODO: enlever le polymorphisme inutile : list_intersect remaining_params declared_params *)
let params = declared_params in
let top = {
let _top = {
coqind_name = record_structure_name x;
coqind_constructor_name = record_constructor_name x;
coqind_targs = coq_types params;
coqind_ret = Coq_type;
coqind_branches = branches } in
let implicit_decl =
let _implicit_decl =
match params with
| [] -> []
| _ -> List.map (fun field -> Coqtop_implicit (field, List.map (fun p -> p, Coqi_maximal) params)) fields_names
in
let type_abbrev = Coqtop_def ((type_constr_name x, Coq_wild), coq_fun_types params loc_type) in
[ type_abbrev ],
[ type_abbrev ] @
(* DEPRECATED BUT KEEP FOR FUTURE USE
[ Coqtop_record top ]
@ (implicit_decl)
......@@ -1236,7 +1236,7 @@ and record_functions name record_constr repr_name params fields_names fields_typ
(** Generate the top-level Coq declarations associated with
a algebraic data type definition. *)
and cfg_algebraic decls =
and cfg_algebraics decls =
(* -- todo: data constructor type arity may be reduced when types are erased *)
(* -- todo: Caml types often clash with Caml program variables, since in Coq
they get put in the same namespace *)
......@@ -1274,28 +1274,31 @@ and cfg_algebraic decls =
let inds,maxiss = List.split (List.map trans_ind decls) in
[ Coqtop_ind inds ]
@ (List.concat maxiss)
@ [ Coqtop_hint_constructors (List.map (fun i -> i.coqind_name) inds, "typeclass_instances") ],
[]
@ [ Coqtop_hint_constructors (List.map (fun i -> i.coqind_name) inds, "typeclass_instances") ]
(** Generate the top-level Coq declarations associated with
a type definition. *)
and cfg_type_decls (decls : (Ident.t * Typedtree.type_declaration) list) =
let rec aux decls =
if List.length decls = 1 && is_type_abbrev (List.hd decls)
then cfg_type_abbrev (List.hd decls)
else if List.length decls = 1 && is_type_record (List.hd decls)
then cfg_type_record (List.hd decls)
else if (List.for_all is_algebraic decls)
then cfg_algebraic decls
else
(* /todo/ very experimental support: simply break circularity; might stack overflow! *)
and cfg_type_decls loc (decls : (Ident.t * Typedtree.type_declaration) list) =
let has_abbrev = List.exists is_type_abbrev decls in
let all_abbrev = List.for_all is_type_abbrev decls in
let nb_decls = List.length decls in
if has_abbrev then begin
if not (all_abbrev && nb_decls = 1)
then unsupported loc "recursive type definitions that include type abbreviations (try inlining the type abbreviations)";
cfg_type_abbrev (List.hd decls)
end else begin
let decls_records = List.filter is_type_record decls in
let decls_algebraic = List.filter is_algebraic decls in
let records_def = list_concat_map cfg_type_record decls_records in
let algebraics_def = if decls_algebraic = [] then [] else cfg_algebraics decls_algebraic in
records_def @ algebraics_def
end
(* DEPRECATED
experimental support: simply break circularity; might stack overflow!
let (a,b) = List.split (List.map aux (List.map (fun x -> [x]) decls)) in
(List.concat a, List.concat b)
(* unsupported "type definitions must be single abbreviations or mutually-recursive inductive definitions (mixing both is not supported in Coq)" *)
in
let (a,b) = aux decls in
a @ b
(List.concat a, List.concat b) *)
(** Generate the top-level Coq declarations associated with
the content of a module. *)
......@@ -1348,7 +1351,7 @@ and cfg_signature_item s =
[Coqtop_param (x, coq_forall_types fv typ)] @ implicit_decl
| Tsig_type decls ->
cfg_type_decls decls
cfg_type_decls loc decls
(* deprecated
List.iter (fun (id,decl) -> printf "%s\n" (Ident.name id)) decls; print_newline();
assert false
......@@ -1358,7 +1361,7 @@ and cfg_signature_item s =
if rs <> Trec_not then unsupported loc "recursive type definitions in signatures";
begin match td.type_kind with
| Type_abstract -> cfg_type_abbrev (id,td)
| Type_variant _ -> cfg_algebraic [id,td]
| Type_variant _ -> cfg_algebraics [id,td]
| Type_record _ -> unsupported loc "record types"
end
*)
......
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