Commit ef1bfced authored by MARCHE Claude's avatar MARCHE Claude

fix issue #240

parent 07638376
let rec f x =
let rec aux y = () in
aux x
let rec g x diverges =
let rec aux y diverges = g () in
aux x
......@@ -198,11 +198,11 @@ module Print = struct
| Lvar (pv, e) ->
fprintf fmt "@[<hov 2>val %a =@ %a@]" (print_lident info) (pv_name pv)
(print_expr info) e
| Lsym (rs, _, [], ef) ->
| Lsym (rs, _, _, [], ef) ->
(* TODO? zero-arguments functions as Lvar in compile.Translate *)
fprintf fmt "@[<hov 2>val %a =@ @[%a@]@]"
(print_lident info) rs.rs_name (print_expr info) ef;
| Lsym (rs, _, args, ef) ->
| Lsym (rs, _, _, args, ef) ->
fprintf fmt "@[<hov 2>fun %a @[%a@] =@ @[%a@]@]"
(print_lident info) rs.rs_name
(print_list space (print_vs_arg info)) args
......@@ -218,7 +218,7 @@ module Print = struct
(print_fun_type_args info) (args, s, res, e);
forget_vars args in
print_list_next newline print_one fmt rdef;
| Lany (rs, _, _) ->
| Lany (rs, _, _, _) ->
check_val_in_drv info rs
and print_expr ?(paren=false) info fmt e =
......
......@@ -234,6 +234,13 @@ module Translate = struct
| ML.Tapp (_, tyl) | ML.Ttuple tyl ->
List.fold_left add_tvar acc tyl
let new_svar args res svar =
let new_svar =
let args' = List.map (fun (_, ty, _) -> ty) args in
let svar = List.fold_left add_tvar Stv.empty args' in
add_tvar svar res in
Stv.diff new_svar svar
(* expressions *)
let rec expr info svar mask ({e_effect = eff; e_attrs = attrs} as e) =
assert (not (e_ghost e));
......@@ -287,15 +294,18 @@ module Translate = struct
rs.rs_name.id_string;
let args = params cty.cty_args in
let res = mlty_of_ity cty.cty_mask cty.cty_result in
let ld = ML.sym_defn rs res args (expr info svar cty.cty_mask ef) in
let new_svar = new_svar args res svar in
let ld = ML.sym_defn rs new_svar res args (expr info svar cty.cty_mask ef) in
ML.e_let ld (expr info svar mask ein) (ML.I e.e_ity) mask eff attrs
| Elet (LDsym (rs, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein)
when isconstructor info rs_app -> (* partial application of constructor *)
let eta_app = mk_eta_expansion rs_app pvl cty in
let mk_func pv f = ity_func pv.pv_ity f in
let func = List.fold_right mk_func cty.cty_args cty.cty_result in
let args = params cty.cty_args in
let res = mlty_of_ity cty.cty_mask func in
let ld = ML.sym_defn rs res [] eta_app in
let new_svar = new_svar args res svar in
let ld = ML.sym_defn rs new_svar res [] eta_app in
let ein = expr info svar mask ein in
ML.e_let ld ein (ML.I e.e_ity) mask eff attrs
| Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
......@@ -307,8 +317,10 @@ module Translate = struct
let pvl = app pvl rs_app.rs_cty.cty_args (fun x -> x) in
let rs_app = Hrs.find_def ht_rs rs_app rs_app in
let eapp = ML.e_app rs_app pvl (ML.C cty) cmk ceff Sattr.empty in
let args = params cty.cty_args in
let res = mlty_of_ity cty.cty_mask cty.cty_result in
let ld = ML.sym_defn rsf res (params cty.cty_args) eapp in
let new_svar = new_svar args res svar in
let ld = ML.sym_defn rsf new_svar res args eapp in
let ein = expr info svar mask ein in
ML.e_let ld ein (ML.I e.e_ity) mask eff attrs
| Elet (LDsym (_, {c_node = Cany; _}), _) -> let loc = e.e_loc in
......@@ -322,11 +334,7 @@ module Translate = struct
| { rec_sym = rs1; rec_fun = {c_node = Cfun ef; c_cty = cty} } ->
let res = mlty_of_ity rs1.rs_cty.cty_mask rs1.rs_cty.cty_result in
let args = params cty.cty_args in
let new_svar =
let args' = List.map (fun (_, ty, _) -> ty) args in
let svar = List.fold_left add_tvar Stv.empty args' in
add_tvar svar res in
let new_svar = Stv.diff new_svar svar in
let new_svar = new_svar args res svar in
let ef = expr info (Stv.union svar new_svar) ef.e_mask ef in
{ ML.rec_sym = rs1; ML.rec_args = args; ML.rec_exp = ef;
ML.rec_res = res; ML.rec_svar = new_svar; }
......@@ -525,11 +533,14 @@ module Translate = struct
| 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
[ML.Dlet (ML.Lany (rs, res, args))]
let new_svar = new_svar args res Stv.empty in
[ML.Dlet (ML.Lany (rs, new_svar, res, args))]
| PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e}))
when is_val e.e_node -> (* zero argument functions *)
let res = mlty_of_ity cty.cty_mask cty.cty_result in
[ML.Dlet (ML.Lany (rs, res, []))]
let args = params cty.cty_args in
let new_svar = new_svar args res Stv.empty in
[ML.Dlet (ML.Lany (rs, new_svar, res, []))]
| PDlet (LDsym ({rs_cty = cty; rs_logic} as rs, {c_node = Cfun e; c_cty}))
when c_cty.cty_args = [] ->
Debug.dprintf debug_compile "compiling zero-arguments function %a@."
......@@ -541,22 +552,16 @@ module Translate = struct
Debug.dprintf debug_compile "rlnone ici@."; [ML.mk_var_unit]
| _ -> [] in
let res = mlty_of_ity cty.cty_mask cty.cty_result in
let svar =
let args' = List.map (fun (_, ty, _) -> ty) args in
let svar = List.fold_left add_tvar Stv.empty args' in
add_tvar svar res in
let svar = new_svar args res Stv.empty in
let e = expr info svar cty.cty_mask e in
[ML.Dlet (ML.Lsym (rs, res, args, e))]
[ML.Dlet (ML.Lsym (rs, svar, res, args, e))]
| PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
Debug.dprintf debug_compile "compiling function %a@." Expr.print_rs rs;
let args = params cty.cty_args in
let res = mlty_of_ity cty.cty_mask cty.cty_result in
let svar =
let args' = List.map (fun (_, ty, _) -> ty) args in
let svar = List.fold_left add_tvar Stv.empty args' in
add_tvar svar res in
let svar = new_svar args res Stv.empty in
let e = expr info svar cty.cty_mask e in
[ML.Dlet (ML.Lsym (rs, res, args, e))]
[ML.Dlet (ML.Lsym (rs, svar, res, args, e))]
| PDlet (LDrec rl) ->
let rl = filter_out_ghost_rdef rl in
List.iter (fun {rec_sym = rs1; rec_rsym = rs2} ->
......@@ -727,9 +732,9 @@ module Transform = struct
assert (not (Mpv.mem pv subst)); (* no capture *)
let e, spv = expr info subst e in
Lvar (pv, e), spv
| Lsym (rs, res, args, e) ->
| Lsym (rs, svar, res, args, e) ->
let e, spv = expr info subst e in
Lsym (rs, res, args, e), spv
Lsym (rs, svar, res, args, e), spv
| Lany _ as lany -> lany, Mpv.empty
| Lrec rl ->
let rdef, spv = mk_list_eb rl (rdef info subst) in
......
......@@ -1175,7 +1175,7 @@ module MLToC = struct
sdecls@[C.Dfun (rs.rs_name, (rtype,params), (d,s))] in
try
begin match d with
| Dlet (Lsym(rs, _, vl, e)) -> translate_fun rs vl e
| Dlet (Lsym(rs, _, _, vl, e)) -> translate_fun rs vl e
| Dtype [{its_name=id; its_def=idef}] ->
Debug.dprintf debug_c_extraction "PDtype %s@." id.id_string;
begin
......
......@@ -118,7 +118,7 @@ module MLPrinter (K: sig val keywords: string list end) = struct
let forget_let_defn = function
| Lvar (v,_) -> forget_id v.pv_vs.vs_name
| Lsym (s,_,_,_) | Lany (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
......
......@@ -643,7 +643,7 @@ let rec interp_expr info (e:Mltree.expr) : value =
with Not_found -> info.get_decl rs in
Debug.dprintf debug_interp "decl found@.";
match decl with
| Dlet (Lsym (rs, _ty, vl, e)) ->
| Dlet (Lsym (rs, _, _ty, vl, e)) ->
eval_call info vl e rs
| Dlet(Lrec([{rec_args = vl; rec_exp = e;
rec_sym = rs; rec_res=_ty}])) ->
......@@ -761,7 +761,7 @@ let rec interp_expr info (e:Mltree.expr) : value =
end
| Elet (Lany _,_) -> Debug.dprintf debug_interp "unhandled Lany@.";
raise CannotReduce
| Elet ((Lsym(rs,_,_,_) as ld), e) ->
| Elet ((Lsym(rs,_,_,_,_) as ld), e) ->
interp_expr (add_fundecl rs (Dlet ld) info) e
| Elet ((Lrec rdl as ld), e) ->
let info = List.fold_left
......@@ -870,6 +870,6 @@ let interp env mm rs vars =
if Debug.test_flag debug_flamegraph then ts := Unix.gettimeofday ();
let decl = info.get_decl rs in
match decl with
| Dlet (Lsym (_rs, _, _vl, expr)) ->
| Dlet (Lsym (_rs, _, _, _vl, expr)) ->
interp_expr info expr
| _ -> raise CannotReduce
......@@ -71,8 +71,8 @@ and exn_branch = xsymbol * pvsymbol list * expr
and let_def =
| Lvar of pvsymbol * expr
| Lsym of rsymbol * ty * var list * expr
| Lany of rsymbol * ty * var list
| Lsym of rsymbol * Stv.t * ty * var list * expr
| Lany of rsymbol * Stv.t * ty * var list
| Lrec of rdef list
and rdef = {
......@@ -132,8 +132,8 @@ let rec get_decl_name = function
List.flatten (List.map add_td_ids itdefl)
| 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}, _, _))
| Dlet (Lsym ({rs_name=id}, _, _, _, _))
| Dlet (Lany ({rs_name=id}, _, _, _))
| Dval ({pv_vs={vs_name=id}}, _)
| Dexn ({xs_name=id}, _) -> [id]
| Dmodule (_, dl) -> List.concat (List.map get_decl_name dl)
......@@ -194,12 +194,12 @@ and iter_deps_expr f e = match e.e_node with
| Elet (Lvar (_, e1), e2) ->
iter_deps_expr f e1;
iter_deps_expr f e2
| Elet (Lsym (_, ty_result, args, e1), e2) ->
| Elet (Lsym (_, _, ty_result, args, e1), e2) ->
iter_deps_ty f ty_result;
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) ->
| 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
......@@ -241,11 +241,11 @@ and iter_deps_expr f e = match e.e_node with
let rec iter_deps f = function
| Dtype its_dl ->
List.iter (iter_deps_its_defn f) its_dl
| Dlet (Lsym (_rs, ty_result, args, e)) ->
| Dlet (Lsym (_rs, _, ty_result, args, e)) ->
iter_deps_ty f ty_result;
iter_deps_args f args;
iter_deps_expr f e
| Dlet (Lany (_rs, ty_result, args)) ->
| Dlet (Lany (_rs, _, ty_result, args)) ->
iter_deps_ty f ty_result;
iter_deps_args f args
| Dlet (Lrec rdef) ->
......@@ -303,8 +303,8 @@ let e_var pv =
let var_defn pv e =
Lvar (pv, e)
let sym_defn f ty_res args e =
Lsym (f, ty_res, args, e)
let sym_defn f svars ty_res args e =
Lsym (f, svars, ty_res, args, e)
let e_let ld e = mk_expr (Elet (ld, e))
......
......@@ -88,7 +88,7 @@ module Print = struct
let forget_let_defn = function
| Lvar (v,_) -> forget_id v.pv_vs.vs_name
| Lsym (s,_,_,_) | Lany (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
......@@ -146,8 +146,8 @@ module Print = struct
let print_lident = print_qident ~sanitizer:Strings.uncapitalize
let print_uident = print_qident ~sanitizer:Strings.capitalize
let print_tv fmt tv =
fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
let print_tv ~use_quote fmt tv =
fprintf fmt (if use_quote then "'%s" else "%s") (id_unique aprinter tv.tv_name)
let protect_on b s =
if b then "(" ^^ s ^^ ")" else s
......@@ -168,53 +168,53 @@ module Print = struct
(** Types *)
let rec print_ty ?(paren=false) info fmt = function
let rec print_ty ~use_quote ?(paren=false) info fmt = function
| Tvar tv ->
print_tv fmt tv
print_tv ~use_quote fmt tv
| Ttuple [] ->
fprintf fmt "unit"
| Ttuple [t] ->
print_ty ~paren info fmt t
print_ty ~use_quote ~paren info fmt t
| Ttuple tl ->
fprintf fmt (protect_on paren "@[%a@]")
(print_list star (print_ty ~paren:true info)) tl
(print_list star (print_ty ~use_quote ~paren:true info)) tl
| Tapp (ts, tl) ->
match query_syntax info.info_syn ts with
| Some s ->
fprintf fmt (protect_on paren "%a")
(syntax_arguments s (print_ty ~paren:true info)) tl
(syntax_arguments s (print_ty ~use_quote ~paren:true info)) tl
| None ->
match tl with
| [] ->
(print_lident info) fmt ts
| [ty] ->
fprintf fmt (protect_on paren "%a@ %a")
(print_ty ~paren:true info) ty (print_lident info) ts
(print_ty ~use_quote ~paren:true info) ty (print_lident info) ts
| tl ->
fprintf fmt (protect_on paren "(%a)@ %a")
(print_list comma (print_ty ~paren:false info)) tl
(print_list comma (print_ty ~use_quote ~paren:false info)) tl
(print_lident info) ts
let print_vsty_opt info fmt id ty =
fprintf fmt "?%s:(%a:@ %a)" id.id_string (print_lident info) id
(print_ty ~paren:false info) ty
(print_ty ~use_quote:false ~paren:false info) ty
let print_vsty_named info fmt id ty =
fprintf fmt "~%s:(%a:@ %a)" id.id_string (print_lident info) id
(print_ty ~paren:false info) ty
(print_ty ~use_quote:false ~paren:false info) ty
let print_vsty info fmt (id, ty, _) =
let attrs = id.id_attrs in
if is_optional ~attrs then print_vsty_opt info fmt id ty
else if is_named ~attrs then print_vsty_named info fmt id ty
else fprintf fmt "(%a:@ %a)" (print_lident info) id
(print_ty ~paren:false info) ty
(print_ty ~use_quote:false ~paren:false info) ty
let print_tv_arg = print_tv
let print_tv_args fmt = function
let print_tv_args ~use_quote fmt = function
| [] -> ()
| [tv] -> fprintf fmt "%a@ " print_tv_arg tv
| tvl -> fprintf fmt "(%a)@ " (print_list comma print_tv_arg) tvl
| [tv] -> fprintf fmt "%a@ " (print_tv_arg ~use_quote) tv
| tvl -> fprintf fmt "(%a)@ " (print_list comma (print_tv_arg ~use_quote)) tvl
let print_vs_arg info fmt vs =
fprintf fmt "@[%a@]" (print_vsty info) vs
......@@ -363,36 +363,36 @@ module Print = struct
(* (print_list space (print_expr ~paren:true info)) tl *)
and print_svar fmt s =
Stv.iter (fun tv -> fprintf fmt "%a " print_tv tv) s
Stv.iter (fun tv -> fprintf fmt "%a " (print_tv ~use_quote:false) tv) s
and print_fun_type_args info fmt (args, s, res, e) =
if Stv.is_empty s then
fprintf fmt "@[%a@] :@ %a@ =@ %a"
(print_list space (print_vs_arg info)) args
(print_ty info) res
(print_ty ~use_quote:false info) res
(print_expr info) e
else
let ty_args = List.map (fun (_, ty, _) -> ty) args in
let id_args = List.map (fun (id, _, _) -> id) args in
let arrow fmt () = fprintf fmt " ->@ " in
fprintf fmt ":@ @[<h>@[%a@]. @[%a ->@ %a@]@] =@ \
@[<hov 2>fun @[%a@]@ ->@ %a@]"
let start fmt () = fprintf fmt "fun@ " in
fprintf fmt ":@ @[<h>type @[%a@]. @[%a@ %a@]@] =@ \
@[<hov 2>@[%a@]@ %a@]"
print_svar s
(print_list arrow (print_ty ~paren:true info)) ty_args
(print_ty ~paren:true info) res
(print_list space (print_lident info)) id_args
(print_list_suf arrow (print_ty ~use_quote:false ~paren:true info)) ty_args
(print_ty ~use_quote:false ~paren:true info) res
(print_list_delim ~start ~stop:arrow ~sep:space (print_lident info)) id_args
(print_expr info) e
and print_let_def ?(functor_arg=false) info fmt = function
| Lvar (pv, e) ->
fprintf fmt "@[<hov 2>let %a =@ %a@]"
(print_lident info) (pv_name pv) (print_expr info) e
| Lsym (rs, res, args, ef) ->
fprintf fmt "@[<hov 2>let %a @[%a@] : %a@ =@ @[%a@]@]"
| Lsym (rs, svar, res, args, ef) ->
fprintf fmt "@[<hov 2>let %a %a@]"
(print_lident info) rs.rs_name
(print_list space (print_vs_arg info)) args
(print_ty info) res (print_expr info) ef;
forget_vars args
(print_fun_type_args info) (args,svar,res,ef);
forget_vars args
| Lrec rdef ->
let print_one fst fmt = function
| { rec_sym = rs1; rec_args = args; rec_exp = e;
......@@ -403,19 +403,19 @@ module Print = struct
(print_fun_type_args info) (args, s, res, e);
forget_vars args in
print_list_next newline print_one fmt rdef;
| Lany (rs, res, []) when functor_arg ->
| Lany (rs, _svar, res, []) when functor_arg ->
fprintf fmt "@[<hov 2>val %a : %a@]"
(print_lident info) rs.rs_name
(print_ty info) res;
| Lany (rs, res, args) when functor_arg ->
(print_ty ~use_quote:true info) res;
| Lany (rs, _svar, res, args) when functor_arg ->
let print_ty_arg info fmt (_, ty, _) =
fprintf fmt "@[%a@]" (print_ty info) ty in
fprintf fmt "@[%a@]" (print_ty ~use_quote:true info) ty in
fprintf fmt "@[<hov 2>val %a : @[%a@] ->@ %a@]"
(print_lident info) rs.rs_name
(print_list arrow (print_ty_arg info)) args
(print_ty info) res;
(print_ty ~use_quote:true info) res;
forget_vars args
| Lany ({rs_name}, _, _) -> check_val_in_drv info rs_name.id_loc rs_name
| Lany ({rs_name}, _, _, _) -> check_val_in_drv info rs_name.id_loc rs_name
and print_expr ?(paren=false) info fmt e =
match e.e_node with
......@@ -528,7 +528,7 @@ module Print = struct
(print_uident info) xs.xs_name (print_expr info) e
| Eexn (xs, Some t, e) ->
fprintf fmt "@[<hv>let exception %a of %a in@\n%a@]"
(print_uident info) xs.xs_name (print_ty ~paren:true info) t
(print_uident info) xs.xs_name (print_ty ~use_quote:false ~paren:true info) t
(print_expr info) e
| Eignore e -> fprintf fmt "ignore (%a)" (print_expr info) e
......@@ -573,10 +573,10 @@ module Print = struct
match cs_args with
| [] -> fprintf fmt "@[<hov 4>| %a@]" (print_uident info) id
| l -> fprintf fmt "@[<hov 4>| %a of %a@]" (print_uident info) id
(print_list star (print_ty ~paren:false info)) l in
(print_list star (print_ty ~use_quote:true ~paren:false info)) l in
let print_field fmt (is_mutable, id, ty) =
fprintf fmt "%s%a: @[%a@];" (if is_mutable then "mutable " else "")
(print_lident info) id (print_ty ~paren:false info) ty in
(print_lident info) id (print_ty ~use_quote:true ~paren:false info) ty in
let print_def fmt = function
| None ->
()
......@@ -587,7 +587,7 @@ module Print = struct
(if its.its_private then "private " else "")
(print_list newline print_field) fl
| Some (Dalias ty) ->
fprintf fmt " =@ %a" (print_ty ~paren:false info) ty
fprintf fmt " =@ %a" (print_ty ~use_quote:true ~paren:false info) ty
| Some (Drange _) ->
fprintf fmt " =@ Z.t"
| Some (Dfloat _) ->
......@@ -596,7 +596,7 @@ module Print = struct
let attrs = its.its_name.id_attrs in
if not (is_ocaml_remove ~attrs) then
fprintf fmt "@[<hov 2>@[%s %a%a@]%a@]"
(if fst then "type" else "and") print_tv_args its.its_args
(if fst then "type" else "and") (print_tv_args ~use_quote:true) its.its_args
(print_lident info) its.its_name print_def its.its_def
let rec is_signature_decl info = function
......@@ -622,7 +622,7 @@ module Print = struct
let print_top_val ?(functor_arg=false) info fmt ({pv_vs}, ty) =
if functor_arg then
fprintf fmt "@[<hov 2>val %a : %a@]"
(print_lident info) pv_vs.vs_name (print_ty info) ty
(print_lident info) pv_vs.vs_name (print_ty ~use_quote:true info) ty
else
check_val_in_drv info pv_vs.vs_name.id_loc pv_vs.vs_name
......@@ -637,7 +637,7 @@ module Print = struct
fprintf fmt "exception %a" (print_uident info) xs.xs_name
| Dexn (xs, Some t)->
fprintf fmt "@[<hov 2>exception %a of %a@]"
(print_uident info) xs.xs_name (print_ty ~paren:true info) t
(print_uident info) xs.xs_name (print_ty ~use_quote:true ~paren:true info) t
| 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
......
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