Commit 8017de9c authored by Mário Pereira's avatar Mário Pereira

Extraction: Eany removed from Mltree expressions; introduced Dval to represent

top-level constants of the form [val c: tau]
parent 4ffe9a4a
......@@ -240,7 +240,6 @@ module Print = struct
forget_let_defn let_def
| Eabsurd ->
fprintf fmt (protect_on paren "assert false (* absurd *)")
| Eany _ -> assert false
| Eapp (rs, []) when rs_equal rs rs_true ->
fprintf fmt "true"
| Eapp (rs, []) when rs_equal rs rs_false ->
......@@ -424,6 +423,10 @@ module Print = struct
let rec print_decl info fmt = function
| Dlet ldef ->
print_let_def info fmt ldef
| Dval ({pv_vs}, _) ->
let loc = pv_vs.vs_name.id_loc in
Loc.errorm ?loc "cannot extract top-level undefined constant %a@."
(print_lident info) pv_vs.vs_name
| Dtype dl ->
print_list newline (print_type_decl info) fmt dl
| Dexn (xs, None) ->
......
......@@ -515,7 +515,7 @@ module Translate = struct
Debug.dprintf debug_compile "compiling undifined constant %a@"
print_pv pv;
let ty = mlty_of_ity cty.cty_mask cty.cty_result in
[ML.Dlet (ML.Lvar (pv, ML.e_any ty cty))]
[ML.Dval (pv, ty)]
| PDlet (LDvar (pv, e)) ->
Debug.dprintf debug_compile "compiling top-level symbol %a@."
print_pv pv;
......@@ -712,7 +712,7 @@ module Transform = struct
((pv, rs, e)::accl, Spv.union spv s))
([], Spv.empty) al in
mk (Eassign (List.rev al)), s
| Econst _ | Eabsurd | Eany _ -> e, Spv.empty
| Econst _ | Eabsurd -> e, Spv.empty
| Eignore e ->
let e, spv = expr info subst e in
mk (Eignore e), spv
......@@ -740,7 +740,7 @@ module Transform = struct
{ r with rec_exp = rec_exp }, spv
let rec pdecl info = function
| Dtype _ | Dexn _ as d -> d
| Dtype _ | Dexn _ | Dval _ as d -> d
| Dmodule (id, dl) ->
let dl = List.map (pdecl info) dl in Dmodule (id, dl)
| Dlet def ->
......
......@@ -1052,7 +1052,6 @@ module MLToC = struct
let v = expr info env e2 in
[], C.(Sexpr(Ebinop(Bassign, t, simplify_expr v)))
| Eassign _ -> raise (Unsupported "assign")
| Eany _ -> assert false
| Eexn (_,_,e) -> expr info env e
| Eignore e ->
[], C.Sseq(C.Sblock(expr info {env with computes_return_value = false} e),
......
......@@ -778,8 +778,6 @@ let rec interp_expr info (e:Mltree.expr) : value =
raise CannotReduce
| Eabsurd -> Debug.dprintf debug_interp "Eabsurd@.";
raise CannotReduce
| Eany _ -> Debug.dprintf debug_interp "Eany@.";
raise CannotReduce
| Ematch (e, l, bl) ->
Debug.dprintf debug_interp "Ematch@.";
begin match interp_expr info e with
......
......@@ -63,7 +63,6 @@ and expr_node =
| Eraise of xsymbol * expr option
| Eexn of xsymbol * ty option * expr
| Eignore of expr
| Eany of ty
| Eabsurd
and reg_branch = pat * expr
......@@ -104,6 +103,7 @@ type its_defn = {
type decl =
| Dtype of its_defn list
| Dlet of let_def
| Dval of pvsymbol * ty (* top-level constants, of the form [val c: tau] *)
| Dexn of xsymbol * ty option
| Dmodule of string * decl list
......@@ -134,6 +134,7 @@ let rec get_decl_name = function
| Dlet (Lvar ({pv_vs={vs_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)
......@@ -183,7 +184,7 @@ and iter_deps_pat f = function
| Pas (p, _) -> iter_deps_pat f p
and iter_deps_expr f e = match e.e_node with
| Econst _ | Evar _ | Eabsurd | Eany _ -> ()
| Econst _ | Evar _ | Eabsurd -> ()
| Eapp (rs, exprl) ->
f rs.rs_name; List.iter (iter_deps_expr f) exprl
| Efun (args, e) ->
......@@ -253,7 +254,7 @@ let rec iter_deps f = function
iter_deps_expr f e; iter_deps_ty f res) rdef
| Dlet (Lvar (_, e)) -> iter_deps_expr f e
| Dexn (_, None) -> ()
| Dexn (_, Some ty) -> iter_deps_ty f ty
| Dexn (_, Some ty) | Dval (_, ty) -> iter_deps_ty f ty
| Dmodule (_, dl) -> List.iter (iter_deps f) dl
let ity_unit = I Ity.ity_unit
......@@ -280,9 +281,6 @@ let is_unit = function
let enope = Eblock []
let e_any ty c =
mk_expr (Eany ty) (C c) MaskVisible Ity.eff_empty Sattr.empty
let mk_var id ty ghost = (id, ty, ghost)
let mk_var_unit =
......
......@@ -275,11 +275,11 @@ module Print = struct
| Eapp (s, []) -> rs_equal s rs_false
| _ -> false
let check_val_in_drv info ({rs_name = {id_loc = loc}} as rs) =
let check_val_in_drv info loc id =
(* here [rs] refers to a [val] declaration *)
match query_syntax info.info_syn rs.rs_name with
match query_syntax info.info_syn id with
| None (* when info.info_flat *) ->
Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
Loc.errorm ?loc "Symbol %a cannot be extracted" (print_lident info) id
| _ -> ()
let is_mapped_to_int info ity =
......@@ -384,9 +384,6 @@ module Print = struct
(print_expr info) e
and print_let_def ?(functor_arg=false) info fmt = function
| Lvar (pv, {e_node = Eany ty}) when functor_arg ->
fprintf fmt "@[<hov 2>val %a : %a@]"
(print_lident info) (pv_name pv) (print_ty info) ty;
| Lvar (pv, e) ->
fprintf fmt "@[<hov 2>let %a =@ %a@]"
(print_lident info) (pv_name pv) (print_expr info) e
......@@ -404,8 +401,7 @@ module Print = struct
(if fst then "let rec" else "and")
(print_lident info) rs1.rs_name
(print_fun_type_args info) (args, s, res, e);
forget_vars args
in
forget_vars args in
print_list_next newline print_one fmt rdef;
| Lany (rs, res, []) when functor_arg ->
fprintf fmt "@[<hov 2>val %a : %a@]"
......@@ -419,7 +415,7 @@ module Print = struct
(print_list arrow (print_ty_arg info)) args
(print_ty info) res;
forget_vars args
| Lany (rs, _, _) -> check_val_in_drv info rs
| 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
......@@ -442,7 +438,6 @@ module Print = struct
forget_let_defn let_def
| Eabsurd ->
fprintf fmt (protect_on paren "assert false (* absurd *)")
| Eany _ -> assert false
| Eapp (rs, []) when rs_equal rs rs_true ->
fprintf fmt "true"
| Eapp (rs, []) when rs_equal rs rs_false ->
......@@ -607,7 +602,7 @@ module Print = struct
let rec is_signature_decl info = function
| Dtype _ -> true
| Dlet (Lany _) -> true
| Dlet (Lvar (_, {e_node = Eany _})) -> true
| Dval _ -> true
| Dlet _ -> false
| Dexn _ -> true
| Dmodule (_, dl) -> is_signature info dl
......@@ -624,9 +619,18 @@ module Print = struct
| dl -> List.rev args, dl in
extract [] dl
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
else
check_val_in_drv info pv_vs.vs_name.id_loc pv_vs.vs_name
let rec print_decl ?(functor_arg=false) info fmt = function
| Dlet ldef ->
print_let_def info ~functor_arg fmt ldef
| Dval (pv, ty) ->
print_top_val info ~functor_arg fmt (pv, ty)
| Dtype dl ->
print_list_next newline (print_type_decl info) fmt dl
| Dexn (xs, None) ->
......
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