ident: blacklisting, sanitizers, forgetting (see pretty and alt-ergo)

src/core/ident.ml

@@ -70,29 +70,84 @@ let id_dup id = { id with id_tag = -1 }
 
 (** Unique names for pretty printing *)
 
-type printer = (string, int) Hashtbl.t * (int, string) Hashtbl.t
-
-let create_printer () = Hashtbl.create 1997, Hashtbl.create 1997
+type printer =
+  (string, int) Hashtbl.t * (int, string) Hashtbl.t * (string -> string)
 
 let rec find_index indices name ind =
   if Hashtbl.mem indices (name ^ string_of_int ind)
   then find_index indices name (succ ind) else ind
 
 let find_unique indices name =
-  try
+  let name = try
     let ind = Hashtbl.find indices name + 1 in
     let ind = find_index indices name ind in
-    Hashtbl.add indices name ind;
+    Hashtbl.replace indices name ind;
     name ^ string_of_int ind
-  with Not_found ->
-    name
+  with Not_found -> name in
+  Hashtbl.replace indices name 0;
+  name
 
-let id_unique (indices,values) id =
+let same x = x
+
+let create_printer ?(sanitizer = same) sl =
+  let indices = Hashtbl.create 1997 in
+  let block n = ignore (find_unique indices n) in
+  List.iter block sl;
+  indices, Hashtbl.create 1997, sanitizer
+
+let id_unique (indices,values,san0) ?(sanitizer = same) id =
   try
     Hashtbl.find values id.id_tag
   with Not_found ->
-    let name = find_unique indices id.id_long in
-    Hashtbl.add values id.id_tag name;
-    Hashtbl.add indices name 0;
+    let name = sanitizer (san0 id.id_long) in
+    let name = find_unique indices name in
+    Hashtbl.replace values id.id_tag name;
     name
 
+let forget_id (indices,values,_) id =
+  try
+    let name = Hashtbl.find values id.id_tag in
+    Hashtbl.remove indices name;
+    Hashtbl.remove values id.id_tag
+  with Not_found -> ()
+
+(** Sanitizers *)
+
+exception Unsanitizable
+
+let char_to_alpha c = match c with
+  | 'a'..'z' | 'A'..'Z' -> String.make 1 c
+  | ' ' -> "sp" | '_'  -> "us" | '#' -> "sh"
+  | '`' -> "bq" | '~'  -> "tl" | '!' -> "ex"
+  | '@' -> "at" | '$'  -> "dl" | '%' -> "pc"
+  | '^' -> "cf" | '&'  -> "et" | '*' -> "as"
+  | '(' -> "lp" | ')'  -> "rp" | '-' -> "mn"
+  | '+' -> "pl" | '='  -> "eq" | '[' -> "lb"
+  | ']' -> "rb" | '{'  -> "lc" | '}' -> "rc"
+  | ':' -> "cl" | '\'' -> "qt" | '"' -> "dq"
+  | '<' -> "ls" | '>'  -> "gt" | '/' -> "sl"
+  | '?' -> "qu" | '\\' -> "bs" | '|' -> "br"
+  | ';' -> "sc" | ','  -> "cm" | '.' -> "dt"
+  | '0' -> "zr" | '1'  -> "un" | '2' -> "du"
+  | '3' -> "tr" | '4'  -> "qr" | '5' -> "qn"
+  | '6' -> "sx" | '7'  -> "st" | '8' -> "oc"
+  | '9' -> "nn" | _ -> raise Unsanitizable
+
+let char_to_lalpha c = String.uncapitalize (char_to_alpha c)
+let char_to_ualpha c = String.capitalize (char_to_alpha c)
+
+let char_to_alnum c =
+  match c with '0'..'9' -> String.make 1 c | _ -> char_to_alpha c
+
+let char_to_alnumus c =
+  match c with '_' | ' ' -> "_" | _ -> char_to_alnum c
+
+let sanitizer head rest n =
+  let lst = ref [] in
+  let code c = lst := rest c :: !lst in
+  let n = if n = "" then "zilch" else n in
+  String.iter code n;
+  let rst = List.tl (List.rev !lst) in
+  let cs = head (String.get n 0) :: rst in
+  String.concat "" cs
+

src/core/ident.mli

@@ -63,9 +63,23 @@ val id_dup : ident -> preid
 
 type printer
 
-(* create new printing session *)
-val create_printer : unit -> printer
+(* create new printing session with a sanitizing function and a blacklist *)
+val create_printer : ?sanitizer : (string -> string) -> string list -> printer
 
 (* generate a unique name for ident in the printing session *)
-val id_unique : printer -> ident -> string
+(* an optional sanitizer is applied over the printer's sanitizer *)
+val id_unique : printer -> ?sanitizer : (string -> string) -> ident -> string
+
+(* forget an ident *)
+val forget_id : printer -> ident -> unit
+
+(* generic sanitizer taking a separate encoder for the first letter *)
+val sanitizer : (char -> string) -> (char -> string) -> string -> string
+
+(* various character encoders *)
+val char_to_alpha : char -> string
+val char_to_lalpha : char -> string
+val char_to_ualpha : char -> string
+val char_to_alnum : char -> string
+val char_to_alnumus : char -> string
 

src/core/theory.ml

@@ -750,7 +750,7 @@ end
 (** Debugging *)
 
 let print_ident =
-  let printer = create_printer () in
+  let printer = create_printer [] in
   let print fmt id = Format.fprintf fmt "%s" (id_unique printer id) in
   print
 

src/output/alt_ergo.ml

@@ -6,11 +6,16 @@ open Ty
 open Term
 open Theory
 
-let ident_printer = create_printer ()
+let ident_printer = 
+  let bls = ["let"; "forall"; "exists"; "and"; "or"] in
+  let san = sanitizer char_to_alpha char_to_alnumus in
+  create_printer bls ~sanitizer:san
 
 let print_ident fmt id =
   fprintf fmt "%s" (id_unique ident_printer id)
 
+let forget_var v = forget_id ident_printer v.vs_name
+
 let rec print_type fmt ty = match ty.ty_node with
   | Tyvar id -> 
       fprintf fmt "'%a" print_ident id
@@ -37,7 +42,8 @@ let rec print_term fmt t = match t.t_node with
   | Tlet (t1, tb) ->
       let v, t2 = t_open_bound tb in
       fprintf fmt "@[(let %a = %a@ in %a)@]" print_ident v.vs_name
-	print_term t1 print_term t2
+        print_term t1 print_term t2;
+      forget_var v
   | Tcase _ ->
       assert false
   | Teps _ ->
@@ -57,7 +63,8 @@ let rec print_fmla fmt f = match f.f_node with
 	fprintf fmt "forall %a:%a" print_ident v.vs_name print_type v.vs_ty
       in
       fprintf fmt "@[<hov2>(%a%a.@ %a)@]" (print_list dot forall) vl
-	(print_list alt print_triggers) tl print_fmla f
+        (print_list alt print_triggers) tl print_fmla f;
+      List.iter forget_var vl
   | Fquant (Fexists, fq) ->
       assert false (*TODO*)
   | Fbinop (Fand, f1, f2) ->
@@ -109,7 +116,8 @@ let print_logic_decl fmt = function
       let _, vl, t = open_fs_defn defn in
       let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
       fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" print_ident id
-	(print_list comma print_logic_binder) vl print_type ty print_term t
+        (print_list comma print_logic_binder) vl print_type ty print_term t;
+      List.iter forget_var vl
   | Lpredicate _ ->
       assert false (*TODO*)
   | Linductive _ ->

src/pretty.ml

@@ -26,10 +26,13 @@ open Theory
 
 let print_list_paren x = print_list_delim lparen rparen x
 
-let print_ident =
-  let printer = create_printer () in
-  let print fmt id = Format.fprintf fmt "%s" (id_unique printer id) in
-  print
+let printer =
+  let sanitize = sanitizer char_to_alpha char_to_alnumus in
+  create_printer [] ~sanitizer:sanitize
+
+let print_ident fmt id = Format.fprintf fmt "%s" (id_unique printer id)
+
+let forget_var v = forget_id printer v.vs_name
 
 let print_typevar fmt x =
   fprintf fmt "'%a" print_ident x
@@ -54,13 +57,14 @@ let rec print_term fmt t = match t.t_node with
   | Tconst (ConstReal _) ->
       fprintf fmt "<real constant>"
   | Tapp (s, tl) ->
-      fprintf fmt "@[<hov>(%a(%a)@ : %a)@](" 
+      fprintf fmt "@[<hov>%a(%a):%a@]" 
 	print_ident s.ls_name (print_list comma print_term) tl
 	print_ty t.t_ty
   | Tlet (t1,tbound) -> 
       let vs,t2 = t_open_bound tbound in
       fprintf fmt "(let %a = %a in@ %a)"
-      print_ident vs.vs_name print_term t1 print_term t2
+      print_ident vs.vs_name print_term t1 print_term t2;
+      forget_var vs
   | Tcase _ ->
       assert false (*TODO*)
   | Teps _ -> 
@@ -71,13 +75,14 @@ let print_vsymbol fmt vs =
 
 let rec print_fmla fmt f = match f.f_node with
   | Fapp (s,tl) -> 
-      fprintf fmt "@[<hov>(%a(%a))@]" 
+      fprintf fmt "@[<hov>%a(%a)@]" 
 	print_ident s.ls_name (print_list comma print_term) tl
   | Fquant (q,fquant) ->
       let vl,tl,f = f_open_quant fquant in
       fprintf fmt "(%s %a %a.@ %a)"
         (match q with Fforall -> "forall" | Fexists -> "exists")
-        (print_list comma print_vsymbol) vl print_tl tl print_fmla f
+        (print_list comma print_vsymbol) vl print_tl tl print_fmla f;
+      List.iter forget_var vl
   | Ftrue -> 
       fprintf fmt "true"
   | Ffalse -> 
@@ -94,7 +99,8 @@ let rec print_fmla fmt f = match f.f_node with
   | Flet (t, f) -> 
       let v,f = f_open_bound f in
       fprintf fmt "@[<hov 2>let %a = %a in@ %a@]" print_ident v.vs_name
-	print_term t print_fmla f
+        print_term t print_fmla f;
+      forget_var v
   | Fcase _ ->
       assert false (*TODO*)
   | Fif _ ->