Commit d5b9da7f authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr/git/why3/why3 into new_system

parents 750ea0bd 840c13b9
......@@ -135,7 +135,7 @@ let flat_case t bl =
Pattern.compile_bare ~mk_case ~mk_let [t] (List.map mk_b bl)
let rec eval_match kn stop env t =
let stop = stop || Slab.mem Term.stop_split t.t_label in
let stop = stop || Slab.mem Ity.annot_label t.t_label in
let eval env t = eval_match kn stop env t in
t_label_copy t (match t.t_node with
| Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
......
......@@ -1241,6 +1241,8 @@ let clone_post_result q = match q.t_node with
| Teps bf -> t_clone_bound_id bf
| _ -> invalid_arg "Ity.clone_post_result"
let annot_label = Ident.create_label "vc:annotation"
type cty = {
cty_args : pvsymbol list;
cty_pre : pre list;
......
......@@ -404,6 +404,8 @@ val clone_post_result : post -> preid
val create_post : vsymbol -> term -> post
val annot_label : label
type cty = private {
cty_args : pvsymbol list;
cty_pre : pre list;
......
......@@ -676,7 +676,7 @@ let rec inject kn uf pins caps pos f = match f.t_node with
let t2, c2 = cap_of_term kn uf pins caps t2 in
let f = t_label_copy f (t_equ t1 t2) in
cap_equality kn uf pins f t1 c1 t2 c2
| _ when Slab.mem stop_split f.t_label ->
| _ when Slab.mem annot_label f.t_label ->
fst (cap_of_term kn uf pins caps f), uf
| Tapp _ ->
fst (cap_of_term kn uf pins caps f), uf
......
......@@ -111,8 +111,10 @@ let expl_type_inv = Ident.create_label "expl:type invariant"
let lab_has_expl lab =
Slab.exists (fun l -> Strings.has_prefix "expl:" l.lab_string) lab
let annot_labels = Slab.add stop_split (Slab.singleton annot_label)
let vc_expl loc lab expl f =
let lab = Slab.add stop_split (Slab.union lab f.t_label) in
let lab = Slab.union annot_labels (Slab.union lab f.t_label) in
let lab = if lab_has_expl lab then lab else Slab.add expl lab in
t_label ?loc:(if loc = None then f.t_loc else loc) lab f
......@@ -148,7 +150,7 @@ let sp_case t bl =
if List.for_all isfalse bl then t_false else add_case (t_case t bl)
let can_simp wp = match wp.t_node with
| Ttrue -> not (Slab.mem stop_split wp.t_label)
| Ttrue -> not (Slab.mem annot_label wp.t_label)
| _ -> false
let wp_and wp1 wp2 = match wp1.t_node, wp2.t_node with
......@@ -270,7 +272,8 @@ let wp_of_post expl ity ql =
let push_stop loc lab expl f =
let rec push f = match f.t_node with
| Tbinop (Tand,g,h) when not (Slab.mem stop_split f.t_label) ->
| Tbinop (Tand,g,h)
when not (Slab.mem annot_label f.t_label) ->
t_label_copy f (t_and (push g) (push h))
| _ -> vc_expl loc lab expl f in
push f
......
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