Commit ce738f74 authored by Mário Pereira's avatar Mário Pereira

Extraction: functors (wip)

parent 6632b3b8
......@@ -50,13 +50,14 @@ module ML = struct
| Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
| Dlet (Lvar ({pv_vs={vs_name=id}}, _))
| 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)
| Dmodule (_, _, dl) -> List.concat (List.map get_decl_name dl)
| Dclone _ -> [] (* FIXME? *)
let rec add_known_decl decl k_map id =
match decl with (* FIXME? keep this block *)
| Dmodule (_, dl) ->
match decl with
| 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
......@@ -113,6 +114,10 @@ module ML = struct
List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
iter_deps_expr f e1;
iter_deps_expr f e2
| Elet (Lany (_, ty_result, args), e2) ->
iter_deps_ty f ty_result;
List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
iter_deps_expr f e2
| Elet ((Lrec rdef), e) ->
List.iter
(fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
......@@ -157,6 +162,9 @@ module ML = struct
iter_deps_ty f ty_result;
iter_deps_args f args;
iter_deps_expr f e
| Dlet (Lany (_rs, ty_result, args)) ->
iter_deps_ty f ty_result;
iter_deps_args f args
| Dlet (Lrec rdef) ->
List.iter
(fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
......@@ -165,7 +173,8 @@ 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) -> List.iter (iter_deps f) dl
| Dclone (_, dl) | Dmodule (_, _, dl) -> (* FIXME: functor argument *)
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; }
......@@ -254,9 +263,15 @@ module Translate = struct
let rec filter_out_ghost_rdef = function
| [] -> []
| { rec_sym = rs; rec_rsym = rrs } :: l
when rs_ghost rs || rs_ghost rrs -> filter_out_ghost_rdef l
| rdef :: l -> rdef :: filter_out_ghost_rdef l
| { rec_sym = rs; rec_rsym = rrs } :: _ when rs_ghost rs || rs_ghost rrs ->
(* filter_out_ghost_rdef l *)
[] (* FIXME: In a mutually recursive block of lemma functions only the
first one is ghost. For now we delete the whole block as soon
as we find a ghost definition. This only works in practice if
the first function is declared as ghost, which is the case of
lemma functions *)
| rdef :: l ->
rdef :: filter_out_ghost_rdef l
let rec pat m p = match p.pat_node with
| Pwild ->
......@@ -700,8 +715,10 @@ module Translate = struct
match pd.pd_node with
| PDlet (LDsym (rs, _)) when rs_ghost rs ->
[]
| PDlet (LDsym (_rs, {c_node = Cany})) ->
[]
| PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cany})) ->
let args = params cty.cty_args in
let res = mlty_of_ity cty.cty_mask cty.cty_result in
[Mltree.Dlet (Mltree.Lany (rs, res, args))]
(* raise (ExtractionVal _rs) *)
| PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
[]
......@@ -739,14 +756,6 @@ module Translate = struct
let info = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
pdecl Sid.empty info pd
(* unit module declarations *)
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
[Mltree.Dmodule (s, dl)]
| Uuse _ | Uclone _ | Umeta _ -> []
let abstract_or_alias_type itd =
itd.itd_fields = [] && itd.itd_constructors = []
......@@ -778,6 +787,18 @@ module Translate = struct
| _ -> params in
List.fold_left add [] dl
(* unit module declarations *)
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)]
| 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;
......@@ -926,6 +947,7 @@ module Transform = struct
| Lsym (rs, res, args, e) ->
let e, spv = expr info subst e in
Lsym (rs, res, args, e), spv
| Lany _ as lany -> lany, Mpv.empty
| Lrec rl ->
let rdef, spv = mk_list_eb rl (rdef info subst) in
Lrec rdef, spv
......@@ -936,7 +958,8 @@ module Transform = struct
let rec pdecl info = function
| Dtype _ | Dexn _ | Dclone _ as d -> d
| Dmodule (id, dl) -> let dl = List.map (pdecl info) dl in Dmodule (id, dl)
| Dmodule (id, args, dl) ->
let dl = List.map (pdecl info) dl in Dmodule (id, args, 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
......
......@@ -59,6 +59,7 @@ and expr_node =
and let_def =
| Lvar of pvsymbol * expr
| Lsym of rsymbol * ty * var list * expr
| Lany of rsymbol * ty * var list
| Lrec of rdef list
and rdef = {
......@@ -89,7 +90,7 @@ type decl =
| Dlet of let_def
| Dexn of xsymbol * ty option
| Dclone of ident * decl list
| Dmodule of string * decl list
| Dmodule of string * (string * decl list) list * decl list
(*
| Dfunctor of ident * (ident * decl list) list * decl list
*)
......
......@@ -72,7 +72,7 @@ module Print = struct
let forget_let_defn = function
| Lvar (v,_) -> forget_id v.pv_vs.vs_name
| Lsym (s,_,_,_) -> forget_rs s
| Lsym (s,_,_,_) | Lany (s,_,_) -> forget_rs s
| Lrec rdl -> List.iter (fun fd -> forget_rs fd.rec_sym) rdl
let rec forget_pat = function
......@@ -346,7 +346,7 @@ module Print = struct
(print_list space (print_lident info)) id_args
(print_expr info) e
and print_let_def ?(top=false) info fmt = function
and print_let_def ?(top=false) ?(functor_arg=false) info fmt = function
| Lvar (pv, e) ->
fprintf fmt "@[<hov 2>let %a =@ %a@]"
(if top then print_global_ident else print_ident) (pv_name pv)
......@@ -370,6 +370,15 @@ module Print = struct
List.iter (fun fd -> Hrs.replace ht_rs fd.rec_rsym fd.rec_sym) rdef;
print_list_next newline print_one fmt rdef;
List.iter (fun fd -> Hrs.remove ht_rs fd.rec_rsym) rdef
| Lany (rs, res, args) when functor_arg ->
let print_ty_arg info fmt (_, ty, _) =
fprintf fmt "@[%a@]" (print_ty info) ty in
fprintf fmt "@[<hov 2>val %a : @[%a@] ->@ %a@]"
(if top then print_global_ident else print_ident) rs.rs_name
(print_list arrow (print_ty_arg info)) args
(print_ty info) res;
forget_vars args
| Lany _ -> () (* FIXME: test driver here *)
and print_enode ?(paren=false) info fmt = function
| Econst c ->
......@@ -531,11 +540,11 @@ module Print = struct
in
fprintf fmt "@[<hov 2>%s %a%a%a@]"
(if fst then "type" else "and") print_tv_args its.its_args
(print_lident info) its.its_name print_def its.its_def
print_ident its.its_name print_def its.its_def
let rec print_decl info fmt = function
let rec print_decl ?(functor_arg=false) info fmt = function
| Dlet ldef ->
print_let_def info ~top:true fmt ldef
print_let_def info ~top:true ~functor_arg fmt ldef
| Dtype dl ->
print_list_next newline (print_type_decl info) fmt dl
| Dexn (xs, None) ->
......@@ -543,12 +552,21 @@ 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, dl) ->
| Dmodule (s, args, dl) ->
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 =
fprintf fmt "sig@ %a@ end"
(print_list space (print_decl info ~functor_arg:true)) dl in
let print_pair fmt (s, dl) =
let info = { info with info_current_ph = s :: info.info_current_ph } in
fprintf fmt "module %s =@\n@[<hov 2>struct@\n%a@]@\nend"
s (print_list newline (print_decl info)) dl
| Dclone _ ->
assert false (*TODO*)
fprintf fmt "(%s:@ %a)" s (print_sig info) dl in
fprintf fmt "@[%a@]" (print_list space print_pair) args
let print_decl info fmt decl =
(* avoids printing the same decl for mutually recursive decls *)
......
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