Commit 26eecfce authored by Guillaume Melquiond's avatar Guillaume Melquiond

Mark "any" expressions as ghost. (Fix #225.)

This commit also raises an assertion failure on Ehole and Eany in the
OCaml printer. (This was already the case for the C printer.)
parent fb6a5a7f
......@@ -243,7 +243,6 @@ module Print = struct
forget_let_defn let_def
| Eabsurd ->
fprintf fmt (protect_on paren "assert false (* absurd *)")
| Ehole -> ()
| Eany _ -> assert false
| Eapp (rs, []) when rs_equal rs rs_true ->
fprintf fmt "true"
......
......@@ -280,6 +280,8 @@ module Translate = struct
ML.e_let ld (expr info svar mask e2) (ML.I e.e_ity) mask eff attrs
| Elet (LDsym (rs, _), ein) when rs_ghost rs ->
expr info svar mask ein
| Elet (LDsym (_, {c_node = Cpur (_, _); _}), _) ->
assert false (* necessarily handled above *)
| Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
Debug.dprintf debug_compile "compiling local function definition %s@."
rs.rs_name.id_string;
......@@ -309,6 +311,8 @@ module Translate = struct
let ld = ML.sym_defn rsf res (params cty.cty_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
Loc.errorm ?loc "This expression cannot be extracted"
| Elet (LDrec rdefl, ein) ->
let rdefl = filter_out_ghost_rdef rdefl in
List.iter
......@@ -369,8 +373,10 @@ module Translate = struct
Debug.dprintf debug_compile "compiling a lambda expression@.";
let ef = expr info svar e.e_mask ef in
ML.e_fun (params cty.cty_args) ef (ML.I e.e_ity) mask eff attrs
| Eexec ({c_node = Cany}, _) ->
ML.mk_hole
| Eexec ({c_node = Cpur (_, _); _ }, _) ->
assert false (* necessarily ghost *)
| Eexec ({c_node = Cany}, _) -> let loc = e.e_loc in
Loc.errorm ?loc "This expression cannot be extracted"
| Eabsurd ->
ML.e_absurd (ML.I e.e_ity) mask eff attrs
| Eassert _ ->
......@@ -438,8 +444,6 @@ module Translate = struct
let ty = if ity_equal xs.xs_ity ity_unit then None
else Some (mlty_of_ity xs.xs_mask xs.xs_ity) in
ML.mk_expr (ML.Eexn (xs, ty, e1)) (ML.I e.e_ity) mask eff attrs
| Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
| Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
and ebranch info svar mask ({pp_pat = p; pp_mask = m}, e) =
(* if the [case] expression is not ghost but there is (at least) one ghost
......@@ -505,7 +509,7 @@ 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)})) ->
| 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
......@@ -692,7 +696,7 @@ module Transform = struct
mk (Eraise (exn, Some e)), spv
| Eassign _al ->
e, Spv.empty
| Econst _ | Eabsurd | Ehole | Eany _ -> e, Spv.empty
| Econst _ | Eabsurd | Eany _ -> e, Spv.empty
| Eignore e ->
let e, spv = expr info subst e in
mk (Eignore e), spv
......
......@@ -1066,7 +1066,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 | Eany _ -> assert false
| Eany _ -> assert false
| Eexn (_,_,e) -> expr info env e
| Eignore e ->
[], C.Sseq(C.Sblock(expr info {env with computes_return_value = false} e),
......
......@@ -776,8 +776,6 @@ let rec interp_expr info (e:Mltree.expr) : value =
raise CannotReduce
| Eabsurd -> Debug.dprintf debug_interp "Eabsurd@.";
raise CannotReduce
| Ehole -> Debug.dprintf debug_interp "Ehole@.";
raise CannotReduce
| Eany _ -> Debug.dprintf debug_interp "Eany@.";
raise CannotReduce
| Ematch (e, l, bl) ->
......
......@@ -65,7 +65,6 @@ and expr_node =
| Eignore of expr
| Eany of ty
| Eabsurd
| Ehole
and reg_branch = pat * expr
......@@ -184,7 +183,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 | Eany _ -> ()
| Econst _ | Evar _ | Eabsurd | Eany _ -> ()
| Eapp (rs, exprl) ->
f rs.rs_name; List.iter (iter_deps_expr f) exprl
| Efun (args, e) ->
......@@ -284,9 +283,6 @@ 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
let mk_var id ty ghost = (id, ty, ghost)
let mk_var_unit =
......@@ -350,7 +346,7 @@ let e_absurd =
let e_seq e1 e2 =
let e = match e1.e_node, e2.e_node with
| (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
| Eblock [], e | e, Eblock [] -> e
| Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
| _, Eblock e2 -> Eblock (e1 :: e2)
| Eblock e1, _ -> Eblock (e1 @ [e2])
......
......@@ -279,7 +279,7 @@ module Print = struct
let check_val_in_drv info ({rs_name = {id_loc = loc}} as rs) =
(* here [rs] refers to a [val] declaration *)
match query_syntax info.info_convert rs.rs_name,
query_syntax info.info_syn rs.rs_name with
query_syntax info.info_syn rs.rs_name with
| None, None (* when info.info_flat *) ->
Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
| _ -> ()
......@@ -447,7 +447,6 @@ module Print = struct
forget_let_defn let_def
| Eabsurd ->
fprintf fmt (protect_on paren "assert false (* absurd *)")
| Ehole -> ()
| Eany _ -> assert false
| Eapp (rs, []) when rs_equal rs rs_true ->
fprintf fmt "true"
......
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