Mlw: use a special label to mark user annotations

We will want to use stop_split higher in the VC formulas.

src/mlw/eval_match.ml

@@ -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 ->

src/mlw/ity.ml

@@ -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;

src/mlw/ity.mli

@@ -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;

src/mlw/typeinv.ml

@@ -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

src/mlw/vc.ml

@@ -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