type label = string * Loc.position option

src/core/pretty.ml

@@ -177,7 +177,7 @@ let prio_binop = function
   | Fimplies -> 1
   | Fiff -> 1
 
-let print_label fmt l = fprintf fmt "\"%s\"" l
+let print_label fmt (l,_) = fprintf fmt "\"%s\"" l
 
 let rec print_term fmt t = print_lterm 0 fmt t
 and     print_fmla fmt f = print_lfmla 0 fmt f

src/core/pretty.mli

@@ -48,6 +48,7 @@ val print_term : formatter -> term -> unit        (* term *)
 val print_fmla : formatter -> fmla -> unit        (* formula *)
 val print_expr : formatter -> expr -> unit        (* term or formula *)
 
+val print_label : formatter -> label -> unit
 val print_pkind : formatter -> prop_kind -> unit
 val print_meta_arg : formatter -> meta_arg -> unit
 val print_meta_arg_type : formatter -> meta_arg_type -> unit

src/core/term.ml

@@ -252,9 +252,13 @@ let rec pat_gen_fold fnT fnV fnL acc pat =
     | Por (p, q) -> fn (fn acc p) q
     | Pas (p, v) -> fn (fnV acc v) p
 
-(** Terms and formulas *)
+(** Labels *)
+
+type label = string * Loc.position option
 
-type label = string
+let label ?loc s = (s,loc)
+
+(** Terms and formulas *)
 
 type quant =
   | Fforall

src/core/term.mli

@@ -103,9 +103,13 @@ val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
 val pat_all : (pattern -> bool) -> pattern -> bool
 val pat_any : (pattern -> bool) -> pattern -> bool
 
-(** {2 Terms and formulas} *)
+(** {2 Labels} *)
+
+type label = string * Loc.position option
 
-type label = string
+val label : ?loc:Loc.position -> string -> label
+
+(** {2 Terms and formulas} *)
 
 type quant =
   | Fforall

src/parser/denv.ml

@@ -154,7 +154,7 @@ and dterm_node =
   | Tif of dfmla * dterm * dterm
   | Tlet of dterm * ident * dterm
   | Tmatch of dterm * (dpattern * dterm) list
-  | Tnamed of string * dterm
+  | Tnamed of label * dterm
   | Teps of ident * dty * dfmla
 
 and dfmla =
@@ -167,7 +167,7 @@ and dfmla =
   | Fif of dfmla * dfmla * dfmla
   | Flet of dterm * ident * dfmla
   | Fmatch of dterm * (dpattern * dfmla) list
-  | Fnamed of string * dfmla
+  | Fnamed of label * dfmla
   | Fvar of fmla
 
 and dtrigger =

src/parser/denv.mli

@@ -60,7 +60,7 @@ and dterm_node =
   | Tif of dfmla * dterm * dterm
   | Tlet of dterm * ident * dterm
   | Tmatch of dterm * (dpattern * dterm) list
-  | Tnamed of string * dterm
+  | Tnamed of label * dterm
   | Teps of ident * dty * dfmla
 
 and dfmla =
@@ -73,7 +73,7 @@ and dfmla =
   | Fif of dfmla * dfmla * dfmla
   | Flet of dterm * ident * dfmla
   | Fmatch of dterm * (dpattern * dfmla) list
-  | Fnamed of string * dfmla
+  | Fnamed of label * dfmla
   | Fvar of fmla
 
 and dtrigger =

src/parser/parser.mly

@@ -405,11 +405,13 @@ lexpr:
 | lexpr OR lexpr
    { infix_pp $1 PPor $3 }
 | lexpr ASYM_OR lexpr
-   { mk_pp (PPnamed ("asym_split", infix_pp $1 PPor $3)) }
+   { let label = Term.label "asym_split" in
+     mk_pp (PPnamed (label, infix_pp $1 PPor $3)) }
 | lexpr AND lexpr
    { infix_pp $1 PPand $3 }
 | lexpr ASYM_AND lexpr
-   { mk_pp (PPnamed ("asym_split", infix_pp $1 PPand $3)) }
+   { let label = Term.label "asym_split" in
+     mk_pp (PPnamed (label, infix_pp $1 PPand $3)) }
 | NOT lexpr
    { prefix_pp PPnot $2 }
 | lexpr EQUAL lexpr
@@ -442,7 +444,7 @@ lexpr:
 | EXISTS list1_param_var_sep_comma triggers DOT lexpr
    { mk_pp (PPquant (PPexists, $2, $3, $5)) }
 | STRING lexpr %prec prec_named
-   { mk_pp (PPnamed ($1, $2)) }
+   { mk_pp (PPnamed (Term.label ~loc:(loc ()) $1, $2)) }
 | LET pattern EQUAL lexpr IN lexpr
    { match $2.pat_desc with
        | PPpvar id -> mk_pp (PPlet (id, $4, $6))

src/parser/ptree.ml

@@ -25,6 +25,7 @@ type loc = Loc.position
 
 type real_constant = Term.real_constant
 type constant = Term.constant
+type label = Term.label
 
 type pp_quant =
   | PPforall | PPexists
@@ -73,7 +74,7 @@ and pp_desc =
   | PPunop of pp_unop * lexpr
   | PPif of lexpr * lexpr * lexpr
   | PPquant of pp_quant * param list * lexpr list list * lexpr
-  | PPnamed of string * lexpr
+  | PPnamed of label * lexpr
   | PPlet of ident * lexpr * lexpr
   | PPeps of ident * pty * lexpr
   | PPmatch of lexpr * (pattern * lexpr) list

src/printer/coq.ml

@@ -143,7 +143,7 @@ let print_binop fmt = function
   | Fimplies -> fprintf fmt "->"
   | Fiff -> fprintf fmt "<->"
 
-let print_label fmt l = fprintf fmt "\"%s\"" l
+let print_label = Pretty.print_label
 
 let protect_on x s = if x then "(" ^^ s ^^ ")" else s
 

src/printer/why3.ml

@@ -168,7 +168,7 @@ let prio_binop = function
   | Fimplies -> 1
   | Fiff -> 1
 
-let print_label fmt l = fprintf fmt "\"%s\"" l
+let print_label = Pretty.print_label
 
 let rec print_term fmt t = print_lterm 0 fmt t
 and     print_fmla fmt f = print_lfmla 0 fmt f

src/transform/split_goal.ml

@@ -35,13 +35,15 @@ let split_case spl c acc tl bl =
   in
   apply_append (f_case tl) acc bll
 
-let asym_split = "asym_split"
+let asym_split = Term.label "asym_split"
+
+let to_split f = List.exists (fun (l,_) -> l = "asym_split") f.f_label
 
 let rec split_pos acc f = match f.f_node with
   | Ftrue -> acc
   | Ffalse -> f::acc
   | Fapp _ -> f::acc
-  | Fbinop (Fand,f1,f2) when List.mem asym_split f.f_label ->
+  | Fbinop (Fand,f1,f2) when to_split f ->
       split_pos (split_pos acc (f_implies f1 f2)) f1
   | Fbinop (Fand,f1,f2) ->
       split_pos (split_pos acc f2) f1
@@ -70,13 +72,13 @@ and split_neg acc f = match f.f_node with
   | Fapp _ -> f::acc
   | Fbinop (Fand,f1,f2) ->
       apply_append2 f_and acc (split_neg [] f1) (split_neg [] f2)
-  | Fbinop (Fimplies,f1,f2) when List.mem asym_split f.f_label ->
+  | Fbinop (Fimplies,f1,f2) when to_split f ->
       split_neg (split_neg acc (f_and f1 f2)) (f_not f1)
   | Fbinop (Fimplies,f1,f2) ->
       split_neg (split_neg acc f2) (f_not f1)
   | Fbinop (Fiff,f1,f2) ->
       split_neg (split_neg acc (f_and (f_not f1) (f_not f2))) (f_and f2 f1)
-  | Fbinop (For,f1,f2) when List.mem asym_split f.f_label ->
+  | Fbinop (For,f1,f2) when to_split f ->
       split_neg (split_neg acc (f_and (f_not f1) f2)) f1
   | Fbinop (For,f1,f2) ->
       split_neg (split_neg acc f2) f1
@@ -128,7 +130,7 @@ let rec rsplit pr dl acc f =
   let rsp = rsplit pr dl in
   match f.f_node with
   | Ftrue -> acc
-  | Fbinop (Fand,f1,f2) when List.mem asym_split f.f_label ->
+  | Fbinop (Fand,f1,f2) when to_split f ->
       rsp (rsp acc (f_implies f1 f2)) f1
   | Fbinop (Fand,f1,f2) ->
       rsp (rsp acc f2) f1