Ident printing fixes

src/ecEnv.ml

@@ -346,7 +346,7 @@ let pp_lookup_failure fmt e =
     | `MPath   p -> EcPath.m_tostring p
     | `Path    p -> EcPath.tostring p
     | `QSymbol p -> string_of_qsymbol p
-    | `AbsStmt p -> EcIdent.tostring p
+    | `AbsStmt p -> EcIdent.name p
   in
     Format.fprintf fmt "unknown symbol: %s" p
 
@@ -3328,11 +3328,11 @@ module LDecl = struct
 
     | LookupError (`Ident id) ->
         Format.fprintf fmt "unknown identifier `%s`, please report"
-        (EcIdent.tostring id)
+        (EcIdent.tostring_internal id)
 
     | NameClash (`Ident id) ->
         Format.fprintf fmt "name clash for `%s`, please report"
-        (EcIdent.tostring id)
+        (EcIdent.tostring_internal id)
 
   let _ = EcPException.register (fun fmt exn ->
     match exn with

src/ecFol.ml

@@ -1113,14 +1113,14 @@ let rec dump_f f =
   in
 
   match f.f_node with
-  | Fquant (q, bs, f) -> dump_quant q ^ " ( " ^ String.concat ", " (List.map EcIdent.tostring (List.fst bs)) ^ " )" ^ "." ^ dump_f f (* of quantif * bindings * form *)
+  | Fquant (q, bs, f) -> dump_quant q ^ " ( " ^ String.concat ", " (List.map EcIdent.tostring_internal (List.fst bs)) ^ " )" ^ "." ^ dump_f f (* of quantif * bindings * form *)
   | Fif    (c, t, f) -> "IF " ^ dump_f c ^ " THEN " ^ dump_f t ^ " ELSE " ^ dump_f f
   | Fmatch _ -> "MATCH"
   | Flet   (_, f, g) -> "LET _ = " ^ dump_f f ^ " IN " ^ dump_f g
   | Fint    x -> BI.to_string x
-  | Flocal  x -> EcIdent.tostring x
-  | Fpvar   (pv, x) -> EcTypes.string_of_pvar pv ^ "{" ^ EcIdent.tostring x ^ "}"
-  | Fglob   (mp, x) -> EcIdent.tostring mp ^ "{" ^ EcIdent.tostring x ^ "}"
+  | Flocal  x -> EcIdent.tostring_internal x
+  | Fpvar   (pv, x) -> EcTypes.string_of_pvar pv ^ "{" ^ EcIdent.tostring_internal x ^ "}"
+  | Fglob   (mp, x) -> EcIdent.tostring_internal mp ^ "{" ^ EcIdent.tostring_internal x ^ "}"
   | Fop     (p, _) -> EcPath.tostring p
   | Fapp    (f, a) -> "APP " ^ dump_f f ^ " ( " ^ String.concat ", " (List.map dump_f a) ^ " )"
   | Ftuple  f -> " ( " ^ String.concat ", " (List.map dump_f f) ^ " )"
@@ -1130,16 +1130,16 @@ let rec dump_f f =
   | FhoareS _ -> "HoareS"
   | FbdHoareF _ -> "bdHoareF"
   | FbdHoareS ({bhs_m = (m, _)} as hs) ->
-     "bdHoareS [ ME = " ^ EcIdent.tostring m
+     "bdHoareS [ ME = " ^ EcIdent.tostring_internal m
      ^ "; PR = " ^ dump_f (bhs_pr hs).inv
      ^ "; PO = " ^ dump_f (bhs_po hs).inv
      ^ "; BD = " ^ dump_f (bhs_bd hs).inv ^ "]"
   | FeHoareS _ -> "eHoareS"
   | FeHoareF _ -> "eHoareF"
   | FequivF _ -> "equivF"
   | FequivS ({es_ml = (ml, _); es_mr = (mr, _)} as es) ->
-     "equivS [ ML = " ^ EcIdent.tostring ml
-     ^ "; MR = " ^ EcIdent.tostring mr
+     "equivS [ ML = " ^ EcIdent.tostring_internal ml
+     ^ "; MR = " ^ EcIdent.tostring_internal mr
      ^ "; PR = " ^ dump_f (es_pr es).inv
      ^ "; PO = " ^ dump_f (es_po es).inv
      ^ "]"

src/ecIdent.ml

@@ -52,7 +52,7 @@ let create (x : symbol) =
 
 let fresh (id : t) = create (name id)
 
-let tostring (id : t) =
+let tostring_internal (id : t) =
   Printf.sprintf "%s/%d" id.id_symb id.id_tag
 
 (* -------------------------------------------------------------------- *)

src/ecIdent.mli

@@ -16,7 +16,7 @@ val create   : symbol -> t
 val fresh    : t -> t
 val name     : t -> symbol
 val tag      : t -> int
-val tostring : t -> string
+val tostring_internal : t -> string
 
 (* -------------------------------------------------------------------- *)
 val id_equal : t -> t -> bool

src/ecPath.ml

@@ -306,7 +306,7 @@ let rec pp_m fmt mp =
       Format.fprintf fmt "@[(%a)@]" (pp_list "," pp_m) args in
   match mp.m_top with
   | `Local id ->
-    Format.fprintf fmt "%s%a" (EcIdent.tostring id) pp_args mp.m_args
+    Format.fprintf fmt "%s%a" (EcIdent.name id) pp_args mp.m_args
   | `Concrete(p,None) ->
     Format.fprintf fmt "%s%a" (tostring p) pp_args mp.m_args
   | `Concrete(p,Some sub) ->
@@ -375,7 +375,7 @@ end
 let rec m_tostring (m : mpath) =
   let top, sub =
     match m.m_top with
-    | `Local id -> (EcIdent.tostring id, "")
+    | `Local id -> (EcIdent.name id, "")
 
     | `Concrete (p, sub) ->
       let strsub =

src/ecPrinting.ml

@@ -276,7 +276,7 @@ module PPEnv = struct
                 let name = EcIdent.name x in
                   match EcEnv.Mod.sp_lookup_opt ([], name) ppe.ppe_env with
                   | Some (p, _, _) when EcPath.mt_equal mp.P.m_top p.P.m_top -> name
-                  | _ -> EcIdent.tostring x
+                  | _ -> EcIdent.name x
           in
             ([], name, None)
 
@@ -354,7 +354,7 @@ module PPEnv = struct
 
   let tyvar (ppe : t) x =
     match Mid.find_opt x ppe.ppe_locals with
-    | None   -> EcIdent.tostring x
+    | None   -> EcIdent.name x
     | Some x -> x
 
   exception FoundUnivarSym of symbol
@@ -620,7 +620,7 @@ let pp_modtype1 (ppe : PPEnv.t) fmt mty =
 
 (* -------------------------------------------------------------------- *)
 let pp_local (ppe : PPEnv.t) fmt x =
-  Format.fprintf fmt "%s" (EcIdent.tostring x)
+  Format.fprintf fmt "%s" (EcIdent.name x)
 
 (* -------------------------------------------------------------------- *)
 let pp_local ?fv (ppe : PPEnv.t) fmt x =
@@ -836,7 +836,7 @@ let pp_mem (ppe : PPEnv.t) (fmt : Format.formatter) (x as id : memory) =
     else x
   in
     if debug_mode then
-      Format.fprintf fmt "%s<%s>" x (EcIdent.tostring id)
+      Format.fprintf fmt "%s<%s>" x (EcIdent.tostring_internal id)
     else
       Format.fprintf fmt "%s" x
 

src/ecTypes.ml

@@ -39,13 +39,13 @@ module Hty = MSHty.H
 let rec dump_ty ty =
   match ty.ty_node with
   | Tglob p ->
-      EcIdent.tostring p
+      EcIdent.tostring_internal p
 
   | Tunivar i ->
       Printf.sprintf "#%d" i
 
   | Tvar id ->
-      EcIdent.tostring id
+      EcIdent.tostring_internal id
 
   | Ttuple tys ->
       Printf.sprintf "(%s)" (String.concat ", " (List.map dump_ty tys))