extraction: fixed detection of functors

parent 97934405
......@@ -52,12 +52,11 @@ module ML = struct
| Dlet (Lsym ({rs_name=id}, _, _, _))
| Dlet (Lany ({rs_name=id}, _, _))
| Dexn ({xs_name=id}, _) -> [id]
| Dmodule (_, _, dl) -> List.concat (List.map get_decl_name dl)
| Dclone _ -> [] (* FIXME? *)
| Dmodule (_, dl) -> List.concat (List.map get_decl_name dl)
let rec add_known_decl decl k_map id =
match decl with
| Dmodule (_, _, dl) ->
| Dmodule (_, dl) ->
let add_decl k_map d =
let idl = get_decl_name d in
List.fold_left (add_known_decl d) k_map idl in
......@@ -173,8 +172,7 @@ module ML = struct
| Dlet (Lvar (_, e)) -> iter_deps_expr f e
| Dexn (_, None) -> ()
| Dexn (_, Some ty) -> iter_deps_ty f ty
| Dclone (_, dl) | Dmodule (_, _, dl) -> (* FIXME: functor argument *)
List.iter (iter_deps f) dl
| Dmodule (_, dl) -> List.iter (iter_deps f) dl
let mk_expr e_node e_ity e_effect e_label =
{ e_node = e_node; e_ity = e_ity; e_effect = e_effect; e_label = e_label; }
......@@ -786,21 +784,11 @@ module Translate = struct
let rec mdecl pids info = function
| Udecl pd -> pdecl pids info pd
| Uscope (_, ([Uuse _] | [Uclone _])) -> []
| Uscope (s, dl) -> let dl = List.concat (List.map (mdecl pids info) dl) in
let filter_func_params (dl, params) = function
| Mltree.Dmodule (s, _args, mod_dl) -> dl, (s, mod_dl) :: params
| d -> d :: dl, params in
let dl, params = List.fold_left filter_func_params ([], []) dl in
[Mltree.Dmodule (s, List.rev params, List.rev dl)]
| Uscope (s, dl) ->
let dl = List.concat (List.map (mdecl pids info) dl) in
[Mltree.Dmodule (s, dl)]
| Uuse _ | Uclone _ | Umeta _ -> []
let make_param from mi =
let id = mi.mi_mod.mod_theory.Theory.th_name in
Format.printf "param %s@." id.id_string;
let dl =
List.concat (List.map (mdecl Sid.empty from) mi.mi_mod.mod_units) in
Mltree.Dclone (id, dl)
let ids_of_params pids mi =
Mid.fold (fun id _ pids -> Sid.add id pids) mi.mi_mod.mod_known pids
......@@ -810,7 +798,7 @@ module Translate = struct
let params = find_params m.mod_units in
let pids = List.fold_left ids_of_params Sid.empty params in
let mod_decl = List.concat (List.map (mdecl pids from) m.mod_units) in
let mod_decl = List.map (make_param from) params @ mod_decl in
let mod_decl = mod_decl in
let add_decl known_map decl = let idl = ML.get_decl_name decl in
List.fold_left (ML.add_known_decl decl) known_map idl in
let mod_known = List.fold_left add_decl Mid.empty mod_decl in {
......@@ -952,9 +940,9 @@ module Transform = struct
{ r with rec_exp = rec_exp }, spv
let rec pdecl info = function
| Dtype _ | Dexn _ | Dclone _ as d -> d
| Dmodule (id, args, dl) ->
let dl = List.map (pdecl info) dl in Dmodule (id, args, dl)
| Dtype _ | Dexn _ as d -> d
| Dmodule (id, dl) ->
let dl = List.map (pdecl info) dl in Dmodule (id, dl)
| Dlet def ->
(* for top-level symbols we can forget the set of inlined variables *)
let e, _ = let_def info Mpv.empty def in Dlet e
......
......@@ -89,11 +89,7 @@ type decl =
| Dtype of its_defn list
| Dlet of let_def
| Dexn of xsymbol * ty option
| Dclone of ident * decl list
| Dmodule of string * (string * decl list) list * decl list
(*
| Dfunctor of ident * (ident * decl list) list * decl list
*)
| Dmodule of string * decl list
type namespace = (ident * decl list) list
......
......@@ -380,7 +380,7 @@ module Print = struct
(print_list arrow (print_ty_arg info)) args
(print_ty info) res;
forget_vars args
| Lany _ -> () (* FIXME: test driver here *)
| Lany _ -> () (* FIXME: test driver here and fail if no driver *)
and print_enode ?(paren=false) info fmt = function
| Econst c ->
......@@ -544,6 +544,25 @@ module Print = struct
(if fst then "type" else "and") print_tv_args its.its_args
(print_lident info) its.its_name print_def its.its_def
let rec is_signature_decl info = function
| Dtype _ -> true
| Dlet (Lany _) -> true
| Dlet _ -> false
| Dexn _ -> true
| Dmodule (_, dl) -> is_signature info dl
and is_signature info dl =
List.for_all (is_signature_decl info) dl
let extract_functor_args info dl =
let rec extract args = function
(* FIXME remove empty args? *)
(* | Dmodule (_, []) :: dl -> extract args dl *)
| Dmodule (x, dlx) :: dl when is_signature info dlx ->
extract ((x, dlx) :: args) dl
| dl -> List.rev args, dl in
extract [] dl
let rec print_decl ?(functor_arg=false) info fmt = function
| Dlet ldef ->
print_let_def info ~functor_arg fmt ldef
......@@ -554,12 +573,12 @@ module Print = struct
| Dexn (xs, Some t)->
fprintf fmt "@[<hov 2>exception %a of %a@]"
(print_uident info) xs.xs_name (print_ty ~paren:true info) t
| Dmodule (s, args, dl) ->
| Dmodule (s, dl) ->
let args, dl = extract_functor_args info dl in
let info = { info with info_current_ph = s :: info.info_current_ph } in
fprintf fmt "@[@[<hov 2>module %s%a@ =@ struct@ %a@]@ end@]" s
(print_functor_args info) args
(print_list newline (print_decl info)) dl
| Dclone _ -> assert false (*TODO*)
and print_functor_args info fmt args =
let print_sig info fmt dl =
......
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