Commit a5234052 authored by Andrei Paskevich's avatar Andrei Paskevich

handle the VC for tuple-typed "any"

parent decf59f2
......@@ -106,6 +106,7 @@ let rec add_quant kn (vl,tl,f) ({vs_ty = ty} as v) =
| Tcase (t, [bt]) ->
lookup_names t; lookup_names (snd (t_open_branch bt))
| Tcase (t, _) | Tbinop (Timplies, _, t) -> lookup_names t
| Tbinop (Tand, t1, t2) -> lookup_names t1; lookup_names t2
| Tquant (_, qf) -> let _,_,f = t_open_quant qf in lookup_names f
| _ -> () in
let idl = try lookup_names f; clone v.vs_name with FoundIdl idl -> idl in
......@@ -185,8 +186,10 @@ let rec eval_match kn stop env t =
with Exit -> branch_map eval env t1 bl1 end
| Tquant (q, qf) ->
let vl,tl,f,close = t_open_quant_cb qf in
let vl,tl,f = if stop then List.rev vl,tl,f else
List.fold_left (add_quant kn) ([],tl,f) vl in
let add_quant (vl,tl,f as acc) ({vs_name = id} as v) =
if stop && not (Sattr.mem Ity.break_attr id.id_attrs)
then v::vl, tl, f else add_quant kn acc v in
let vl,tl,f = List.fold_left add_quant ([],tl,f) vl in
t_quant_simp q (close (List.rev vl) tl (eval env f))
| _ ->
t_map (eval env) t)
......
......@@ -1230,6 +1230,7 @@ let clone_post_result q = match q.t_node with
| _ -> invalid_arg "Ity.clone_post_result"
let annot_attr = Ident.create_attribute "vc:annotation"
let break_attr = Ident.create_attribute "vc:break_me"
type cty = {
cty_args : pvsymbol list;
......
......@@ -400,6 +400,7 @@ val clone_post_result : post -> preid
val create_post : vsymbol -> term -> post
val annot_attr : attribute
val break_attr : attribute
type cty = private {
cty_args : pvsymbol list;
......
......@@ -124,7 +124,8 @@
| [] -> assert false (* never *)
| [q] -> case q
| q::ql -> mk_t (Tbinop (case q, Dterm.DTand_asym, join ql)) in
let bl = [any_loc, Some (ri any_loc), false, Some ty] in
let id = add_attr (ri any_loc) [ATstr Ity.break_attr] in
let bl = [any_loc, Some id, false, Some ty] in
let p = mk_t (Tquant (Dterm.DTexists, bl, [], join ql)) in
[mk_t (Tattr (ATstr we_attr, p))]
......
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