Commit d60c21eb authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Expr: e_let

parent 3d34cbef
......@@ -292,7 +292,7 @@ let e_fold fn acc e = match e.e_node with
exception FoundExpr of expr
(* find a minimal sub-expression satisfying [pr] *)
let find_minimal pr e =
let e_find_minimal pr e =
let rec find () e = e_fold find () e;
if pr e then raise (FoundExpr e) in
try find () e; raise Not_found with FoundExpr e -> e
......@@ -370,6 +370,37 @@ let create_let_defn_ps id ?(ghost=false) ?(kind=PKnone) e =
let ps = create_psymbol id ~ghost ~kind cty in
{ let_sym = ValS ps; let_expr = e }, ps
let e_let ({let_sym = lv; let_expr = d} as ld) e = match lv with
| ValV _ ->
let eff = eff_union d.e_effect e.e_effect in
mk_expr (Elet (ld,e)) e.e_vty e.e_ghost eff
| ValS {ps_logic = PLls _} ->
invalid_arg "Expr.e_let"
| ValS s ->
let rec rewind d = match d.e_node with
| Efun _ | Eany | Eapp _ ->
let ld = {let_sym = lv; let_expr = d} in
let eff = eff_union d.e_effect e.e_effect in
mk_expr (Elet (ld,e)) e.e_vty e.e_ghost eff
| Eghost d -> assert s.ps_ghost; rewind d
| Elet ({let_sym = ValS {ps_ghost = gh}}, _)
| Elet ({let_sym = ValV {pv_ghost = gh}}, _)
when s.ps_ghost && not gh -> Loc.errorm ?loc:d.e_loc
"This let-definition must be explicitly marked ghost"
| Elet ({let_expr = d} as ld, e) ->
let e = rewind e in
let eff = eff_union d.e_effect e.e_effect in
mk_expr (Elet (ld,e)) e.e_vty e.e_ghost eff
| Erec ({rec_defn = dl} as rd, e) ->
let ngh fd = not fd.fun_sym.ps_ghost in
if s.ps_ghost && List.exists ngh dl then Loc.errorm ?loc:d.e_loc
"%s must be explicitly marked ghost" (if List.length dl > 1 then
"These recursive definitions" else "This recursive definition");
let e = rewind e in
mk_expr (Erec (rd,e)) e.e_vty e.e_ghost e.e_effect
in
rewind d
(* lambda construction *)
let rec e_vars e = match e.e_node with
......
......@@ -157,6 +157,12 @@ exception CtyExpected of expr
val ity_of_expr : expr -> ity
val cty_of_expr : expr -> cty
val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
val e_find_minimal : (expr -> bool) -> expr -> expr
(* [e_find_minimal pr e] looks for a minimal sub-expression
of [e] satisfying [pr], raises [Not_found] if none found. *)
(** {2 Smart constructors} *)
val e_var : pvsymbol -> expr
......@@ -172,5 +178,7 @@ val create_let_defn_pv : preid -> ?ghost:bool -> expr -> let_defn * pvsymbol
val create_let_defn_ps :
preid -> ?ghost:bool -> ?kind:ps_kind -> expr -> let_defn * psymbol
val e_let : let_defn -> expr -> expr
val e_fun :
pvsymbol list -> pre list -> post list -> post list Mexn.t -> expr -> expr
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