Commit fdb529ac authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: push the expression labels past the implicit "let"

parent 0fa37276
......@@ -623,7 +623,8 @@ let e_let ({ let_sym = lv ; let_expr = d } as ld) e =
let on_value fn e = match e.e_node with
| Evalue pv -> fn pv
| _ ->
let ld = create_let_defn (id_fresh "o") e in
let id = id_fresh ?loc:e.e_loc "o" in
let ld = create_let_defn id e in
let pv = match ld.let_sym with
| LetA _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
| LetV pv -> pv in
......@@ -827,7 +828,8 @@ let on_fmla fn e = match e.e_node with
| Elogic t -> fn e (t_equ_simp t t_bool_true)
| Evalue pv -> fn e (t_equ_simp (t_var pv.pv_vs) t_bool_true)
| _ ->
let ld = create_let_defn (id_fresh "o") e in
let id = id_fresh ?loc:e.e_loc "o" in
let ld = create_let_defn id e in
let pv = match ld.let_sym with
| LetA _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
| LetV pv -> pv in
......
......@@ -267,7 +267,7 @@ let mk_let ~loc ~uloc e (desc,dvty) =
if test_var e then desc, dvty else
let loc = def_option loc uloc in
let e1 = mk_dexpr desc dvty loc Slab.empty in
DElet (mk_id "q" loc, false, e, e1), dvty
DElet (mk_id "q" e.de_loc, false, e, e1), dvty
(* patterns *)
......
......@@ -631,16 +631,25 @@ and wp_desc env e q xq = match e.e_node with
| Earrow _ ->
let q = open_unit_post q in
(* wp_label e *) q (* FIXME? *)
| Elet ({ let_sym = lv; let_expr = e1 }, e2) ->
| Elet ({ let_sym = LetV v; let_expr = e1 }, e2)
when Util.option_eq Loc.equal v.pv_vs.vs_name.id_loc e1.e_loc ->
(* we push the label down, past the implicitly inserted "let" *)
let w = wp_expr env (e_label_copy e e2) q xq in
let q = create_post v.pv_vs w in
wp_expr env e1 q xq
| Elet ({ let_sym = LetV v; let_expr = e1 }, e2) ->
let w = wp_expr env e2 q xq in
let q = match lv with
| LetV v -> create_post v.pv_vs w
| LetA _ -> create_unit_post w in
let q = create_post v.pv_vs w in
wp_label e (wp_expr env e1 q xq)
| Erec (rdl, e) ->
| Elet ({ let_sym = LetA _; let_expr = e1 }, e2) ->
let w = wp_expr env e2 q xq in
let q = create_unit_post w in
wp_label e (wp_expr env e1 q xq)
| Erec (rdl, e1) ->
let fr = wp_rec_defn env rdl in
let fe = wp_expr env e q xq in
wp_and ~sym:true (wp_ands ~sym:true fr) fe
let fe = wp_expr env e1 q xq in
let fr = wp_ands ~sym:true fr in
wp_label e (wp_and ~sym:true fr fe)
| Eif (e1, e2, e3) ->
let res = vs_result e1 in
let test = t_equ (t_var res) t_bool_true 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