Commit 8a11378a authored by MARCHE Claude's avatar MARCHE Claude

extraction: delete ghost parameters

parent 4df96e8e
......@@ -253,7 +253,7 @@ module Translate = struct
if has_syntax info ts.ts_name || is_record d then []
else projections info d
let filter_ghost ls def al =
let filter_ghost_fields ls def al =
let flt fd arg = if fd.Mlw_expr.fd_ghost then def else arg in
try List.map2 flt (Mlw_expr.restore_pl ls).Mlw_expr.pl_args al
with Not_found -> al
......@@ -274,7 +274,7 @@ module Translate = struct
| Some s -> ML.Psyntax (s, List.map (pat info) pl)
| None ->
let pat_void = Term.pat_app Mlw_expr.fs_void [] Mlw_ty.ty_unit in
let pl = filter_ghost cs pat_void pl in
let pl = filter_ghost_fields cs pat_void pl in
let pjl = get_record info cs in
if pjl = [] then
ML.Papp (cs.ls_name, List.map (pat info) pl)
......@@ -320,7 +320,7 @@ module Translate = struct
let id = ls.ls_name in
match tl with
| tl when isconstr ->
let tl = filter_ghost ls Mlw_expr.t_void tl in
let tl = filter_ghost_fields ls Mlw_expr.t_void tl in
let pjl = get_record info ls in
if pjl = [] then
ML.Econstr (id, List.map (term info) tl)
......@@ -474,6 +474,13 @@ module Translate = struct
| [fd] -> fd.fun_lambda.l_spec.c_letrec <> 0
| _ -> true
let filter_ghost_params =
let dummy = create_pvsymbol (Ident.id_fresh "") ity_unit in
fun args ->
match List.filter (fun v -> not v.Mlw_ty.pv_ghost) args with
| [] -> [dummy]
| l -> l
let rec expr info e =
assert (not e.e_ghost);
match e.e_node with
......@@ -494,6 +501,13 @@ module Translate = struct
let n = Number.compute_int (get_int_constant e1) in
let e1 = ML.Esyntax (BigInt.to_string n, []) in
ML.Esyntax (s, [e1])
| Eapp (e, v, _) when v.pv_ghost ->
(* ghost parameters are ignored *)
begin
match e.e_node with
| Eapp _ -> expr info e
| _ -> ML.Eapp (expr info e, [ML.enop])
end
| Eapp (e, v, _) ->
ML.Eapp (expr info e, [ML.Eident (pv_name v)])
| Elet ({ let_expr = e1 }, e2) when e1.e_ghost ->
......@@ -550,7 +564,8 @@ module Translate = struct
and recdef info { fun_ps = ps; fun_lambda = lam } =
assert (not ps.ps_ghost);
ps.ps_name, List.map (pvty info) lam.l_args, expr info lam.l_expr
let args = filter_ghost_params lam.l_args in
ps.ps_name, List.map (pvty info) args, expr info lam.l_expr
and ebranch info ({ppat_pattern=p}, e) =
pat info p, expr info e
......@@ -780,7 +795,7 @@ module Print = struct
| tvl -> fprintf fmt "(%a)@ " (print_list comma print_tv_arg) tvl
let print_ty_arg info fmt ty = fprintf fmt "%a" (print_ty ~paren:true info) ty
let print_vs_arg info fmt vs = fprintf fmt "(%a)" (print_vsty info) vs
let print_vs_arg info fmt vs = fprintf fmt "@[(%a)@]" (print_vsty info) vs
let print_type_decl info fst fmt (ts, args, def) =
let print_constr fmt (cs, args) = match args with
......@@ -1019,7 +1034,7 @@ module Print = struct
fprintf fmt "@\n@\n"
| Dlet (isrec, dl) ->
let print_one fst fmt (ls, vl, e) =
fprintf fmt "@[<hv 2>%s %a @[%a@] =@ %a@]"
fprintf fmt "@[<hov 2>%s %a@ %a@ =@ %a@]"
(if fst then if isrec then "let rec" else "let" else "and")
(print_lident info) ls
(print_list space (print_vs_arg info)) vl
......
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