First attempt at having a printer using a label name:.

src/core/ident.ml

@@ -98,6 +98,25 @@ let get_model_trace_string ~labels =
   | [_; t_str] -> t_str
   | _ -> ""
 
+(* Functions for working with ITP labels *)
+
+let is_name_label label =
+  Strings.has_prefix "name:" label.lab_string
+
+let get_name_label ~labels = Slab.choose (Slab.filter is_name_label labels)
+
+let get_element_name ~labels =
+  let name_label = get_name_label ~labels in
+  let splitted1 = Strings.bounded_split ':' name_label.lab_string 2 in
+  match splitted1 with
+  | ["name"; content] ->
+    begin
+      content
+    end;
+  | [_] -> ""
+  | _ -> assert false
+
+
 
 (** Identifiers *)
 
@@ -209,6 +228,22 @@ let id_unique printer ?(sanitizer = same) id =
     Hid.replace printer.values id name;
     name
 
+let id_unique_label printer ?(sanitizer = same) id =
+  try
+    Hid.find printer.values id
+  with Not_found ->
+    let labels =  id.id_label in
+    if Slab.exists is_name_label labels then
+      let name = sanitizer (get_element_name ~labels) in
+      let name = find_unique printer.indices name in
+      Hid.replace printer.values id name;
+      name
+    else
+      let name = sanitizer (printer.sanitizer id.id_string) in
+      let name = find_unique printer.indices name in
+      Hid.replace printer.values id name;
+      name
+
 let string_unique printer s = find_unique printer.indices s
 
 let forget_id printer id =

src/core/ident.mli

@@ -119,6 +119,11 @@ val id_unique :
 (** use ident_printer to generate a unique name for ident
     an optional sanitizer is applied over the printer's sanitizer *)
 
+val id_unique_label :
+  ident_printer -> ?sanitizer : (string -> string) -> ident -> string
+(** Do the same as id_unique except that it tries first to
+   use the "name:" label to generate the name instead of id.id_string *)
+
 val string_unique : ident_printer -> string -> string
 (** Uniquify string *)
 

src/transform/args_wrapper.ml

@@ -20,6 +20,11 @@ let fresh_printer =
 
 open Stdlib
 
+let sanitizer x = x (*sanitizer char_to_lalpha char_to_lalpha x*)
+
+let id_unique printer id =
+  id_unique_label printer ~sanitizer:sanitizer id
+
 type name_tables = {
     namespace : namespace;
     known_map : known_map;

tests/test_argument.why

@@ -2,7 +2,7 @@
 theory Test
    use import int.Int
 
-   goal G: forall x. exists y. x = 2 * y
+   goal G: forall x "name:TOTO". forall y. x = y -> x = 2 * y
 
    (*
 ng

tests/test_argument.whyitp

 ?
 t introduce_premises
 (* print goal with premisses introduced *)
+k
+t cut "y = y"
+t cut "TOTO = TOTO"
 t cut "exists x: int. x = x"
 (* print goal with h in context *)
 t exists "5"