diff --git a/src/mlw/cakeml_printer.ml b/src/mlw/cakeml_printer.ml index 41e3f6061939caad3802aa27b89895132a0bc0f6..5e6e11c07829ffa1f81b23d1b6ada5c90287ef74 100644 --- a/src/mlw/cakeml_printer.ml +++ b/src/mlw/cakeml_printer.ml @@ -227,7 +227,8 @@ module Print = struct | Lany (rs, _, _) -> check_val_in_drv info rs - and print_expr ?(paren=false) info fmt e = match e.e_node with + and print_expr ?(paren=false) info fmt e = + match e.e_node with | Econst c -> let n = Number.compute_int_constant c in let n = BigInt.to_string n in @@ -246,6 +247,7 @@ module Print = struct | Eabsurd -> fprintf fmt (protect_on paren "assert false (* absurd *)") | Ehole -> () + | Eany _ -> assert false | Eapp (rs, []) when rs_equal rs rs_true -> fprintf fmt "true" | Eapp (rs, []) when rs_equal rs rs_false -> diff --git a/src/mlw/compile.ml b/src/mlw/compile.ml index 8deb6ef92d7d2f46397a7271c40b8ea90f90456d..f64966d61a13e53c9a8b99daa128efc5e570daab 100644 --- a/src/mlw/compile.ml +++ b/src/mlw/compile.ml @@ -494,6 +494,11 @@ module Translate = struct if eff_pure e.e_effect then [] else let unit_ = pv (* create_pvsymbol (id_fresh "_") ity_unit *) in [ML.Dlet (ML.Lvar (unit_, expr info Stv.empty MaskGhost e))] + | PDlet (LDvar (pv, {e_node = Eexec ({c_node = Cany}, cty)})) -> + 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))] | PDlet (LDvar (pv, e)) -> Debug.dprintf debug_compile "compiling top-level symbol %a@." print_pv pv; @@ -674,7 +679,7 @@ module Transform = struct mk (Eraise (exn, Some e)), spv | Eassign _al -> e, Spv.empty - | Econst _ | Eabsurd | Ehole -> e, Spv.empty + | Econst _ | Eabsurd | Ehole | Eany _ -> e, Spv.empty | Eignore e -> let e, spv = expr info subst e in mk (Eignore e), spv diff --git a/src/mlw/cprinter.ml b/src/mlw/cprinter.ml index c414075b74d24ff0526ec579dc712fe1f9125767..da6fc1db1878fecf61e804be6956dae5962783a9 100644 --- a/src/mlw/cprinter.ml +++ b/src/mlw/cprinter.ml @@ -1011,7 +1011,7 @@ module MLToC = struct | None, None -> raise (Unsupported ("assign not in driver")) in [], C.(Sexpr(Ebinop(Bassign, t, C.Evar v.pv_vs.vs_name))) | Eassign _ -> raise (Unsupported "assign") - | Ehole -> assert false + | Ehole | Eany _ -> assert false | Eexn _ -> raise (Unsupported "exception") | Eignore e -> [], C.Sseq(C.Sblock(expr info {env with computes_return_value = false} e), diff --git a/src/mlw/mlinterp.ml b/src/mlw/mlinterp.ml index 94de8fa08abbc543142bd74c8c5f2db717cffa60..7322593ea3b6a6b7e172cb4493d59641d96c9d2c 100644 --- a/src/mlw/mlinterp.ml +++ b/src/mlw/mlinterp.ml @@ -769,6 +769,8 @@ let rec interp_expr info (e:Mltree.expr) : value = raise CannotReduce | Ehole -> Debug.dprintf debug_interp "Ehole@."; 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 diff --git a/src/mlw/mltree.ml b/src/mlw/mltree.ml index 24074167300ddd2d726fdd3c3065cca632de05e6..7e7c8b63d50d9c84dee1e923911b3a0c3796735a 100644 --- a/src/mlw/mltree.ml +++ b/src/mlw/mltree.ml @@ -63,6 +63,7 @@ and expr_node = | Eraise of xsymbol * expr option | Eexn of xsymbol * ty option * expr | Eignore of expr + | Eany of ty | Eabsurd | Ehole @@ -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 | Ehole -> () + | Econst _ | Evar _ | Eabsurd | Ehole | Eany _ -> () | Eapp (rs, exprl) -> f rs.rs_name; List.iter (iter_deps_expr f) exprl | Efun (args, e) -> @@ -280,6 +281,9 @@ 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_hole = mk_expr Ehole (I Ity.ity_unit) MaskVisible Ity.eff_empty Sattr.empty diff --git a/src/mlw/ocaml_printer.ml b/src/mlw/ocaml_printer.ml index 9bd122afdb80d224a614e09117a66f6d07d026e4..6ae1114f4075c0695b01f367a4259efd99251d01 100644 --- a/src/mlw/ocaml_printer.ml +++ b/src/mlw/ocaml_printer.ml @@ -387,6 +387,10 @@ 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) @@ -424,7 +428,8 @@ module Print = struct forget_vars args | Lany (rs, _, _) -> check_val_in_drv info rs - and print_expr ?(paren=false) info fmt e = match e.e_node with + and print_expr ?(paren=false) info fmt e = + match e.e_node with | Econst c -> let n = Number.compute_int_constant c in let n = BigInt.to_string n in @@ -445,6 +450,7 @@ module Print = struct | Eabsurd -> fprintf fmt (protect_on paren "assert false (* absurd *)") | Ehole -> () + | Eany _ -> assert false | Eapp (rs, []) when rs_equal rs rs_true -> fprintf fmt "true" | Eapp (rs, []) when rs_equal rs rs_false -> @@ -612,6 +618,7 @@ module Print = struct let rec is_signature_decl info = function | Dtype _ -> true | Dlet (Lany _) -> true + | Dlet (Lvar (_, {e_node = Eany _})) -> true | Dlet _ -> false | Dexn _ -> true | Dmodule (_, dl) -> is_signature info dl