Commit 1b2c54b0 authored by Andrei Paskevich's avatar Andrei Paskevich

preserve labels and positions in eval_match (closes #13130)

parent 86566a6f
......@@ -660,7 +660,6 @@ and dexpr_desc ~ghost env loc = function
let e3 = dexpr ~ghost env e3 in
expected_type e3 (dty_unit env.uc);
DEfor (x, e1, d, e2, inv, e3), dty_unit env.uc
| Ptree.Eassert (k, le) ->
DEassert (k, le), dty_unit env.uc
| Ptree.Emark ({id=s}, e1) ->
......@@ -1613,7 +1612,6 @@ and expr_desc ~userloc gl env loc ty = function
let add_effect ef (_,_,_,ef') = E.union ef ef' in
let ef = List.fold_left add_effect e1.expr_effect dl in
Eletrec (dl, e1), e1.expr_type_v, ef
| IEif (e1, e2, e3) ->
let e1 = expr ~userloc gl env e1 in
let e2 = expr ~userloc gl env e2 in
......@@ -1704,7 +1702,6 @@ and expr_desc ~userloc gl env loc ty = function
let ef = e3.expr_effect in
let ef, inv = option_map_fold term_effect ef inv in
Efor (x, v1, d, v2, inv, e3), type_v_unit gl, ef
| IEassert (k, f) ->
let ef, f = term_effect E.empty f in
Eassert (k, f), tpure ty, ef
......
......@@ -55,6 +55,11 @@ let get_mutable_field ts i =
(* smart constructors for building WPs
TODO: tag with label "WP" *)
let wp_label e f =
let loc = if f.t_loc = None then Some e.expr_loc else f.t_loc in
let lab = e.expr_lab @ f.t_label in
t_label ?loc lab f
let wp_and ?(sym=false) f1 f2 =
if sym then t_and_simp f1 f2 else t_and_asym_simp f1 f2
......@@ -406,14 +411,6 @@ let well_founded_rel = function
(* Recursive computation of the weakest precondition *)
let wp_label ?loc ?(lab=[]) f =
let loc = option_apply loc (fun x -> Some x) f.t_loc in
let lab = lab @ f.t_label in
(*
let lab = if List.mem "WP" lab then lab else "WP" :: lab in
*)
t_label ?loc lab f
let t_True env =
fs_app (find_ls ~pure:true env "True") []
(ty_app (find_ts ~pure:true env "bool") [])
......@@ -433,7 +430,7 @@ let rec wp_expr env rm e q =
let q = post_map (old_mark lab) q in
let f = wp_desc env rm e q in
let f = erase_mark lab f in
let f = wp_label ~loc:e.expr_loc ~lab:e.expr_lab f in
let f = wp_label e f in
if Debug.test_flag debug then begin
eprintf "@[--------@\n@[<hov 2>e = %a@]@\n" Pgm_pretty.print_expr e;
eprintf "@[<hov 2>q = %a@]@\n" Pretty.print_term (snd (fst q));
......
......@@ -67,6 +67,10 @@ let rec add_quant kn (vl,tl,f) v =
| _ ->
(v::vl, tl, f)
let t_label_merge { t_label = l; t_loc = p } t =
let p = if t.t_loc = None then p else t.t_loc in
t_label ?loc:p (l @ t.t_label) t
let eval_match ~inline kn t =
let rec eval env t = match t.t_node with
| Tapp (ls, tl) when inline kn ls (List.map t_type tl) t.t_ty ->
......@@ -74,13 +78,13 @@ let eval_match ~inline kn t =
| None ->
t_map (eval env) t
| Some def ->
t_label_copy t (eval env (unfold def tl t.t_ty))
t_label_merge t (eval env (unfold def tl t.t_ty))
end
| Tlet (t1, tb2) ->
let t1 = eval env t1 in
let x, t2, close = t_open_bound_cb tb2 in
let t2 = eval (Mvs.add x t1 env) t2 in
t_label_copy t (t_let_simp t1 (close x t2))
t_label_merge t (t_let_simp t1 (close x t2))
| Tcase (t1, bl1) ->
let t1 = eval env t1 in
let t1flat = dive env t1 in
......@@ -105,11 +109,11 @@ let eval_match ~inline kn t =
in
t_case t1 (List.map mk_b bl1)
in
t_label_copy t r
t_label_merge t r
| Tquant (q, qf) ->
let vl,tl,f,close = t_open_quant_cb qf in
let vl,tl,f = List.fold_left (add_quant kn) ([],tl,f) vl in
t_label_copy t (t_quant_simp q (close (List.rev vl) tl (eval env f)))
t_label_merge t (t_quant_simp q (close (List.rev vl) tl (eval env f)))
| _ ->
t_map (eval env) t
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