From 2a666d0113c072d4ecce9a5db908d53761ae9e1c Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Thu, 30 Oct 2025 12:27:51 +0000 Subject: [PATCH] PR: Fix printing of idents and rename EcIdent.tostring to tostring_internal for clarity of use --- src/ecEnv.ml | 6 +++--- src/ecFol.ml | 14 +++++++------- src/ecIdent.ml | 2 +- src/ecIdent.mli | 2 +- src/ecPath.ml | 4 ++-- src/ecPrinting.ml | 8 ++++---- src/ecTypes.ml | 4 ++-- 7 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 56e638796e..a4a5c8a7ca 100644 --- a/src/ecEnv.ml +++ b/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 diff --git a/src/ecFol.ml b/src/ecFol.ml index 96e516fbd0..57322210d9 100644 --- a/src/ecFol.ml +++ b/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,7 +1130,7 @@ 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 ^ "]" @@ -1138,8 +1138,8 @@ let rec dump_f f = | 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 ^ "]" diff --git a/src/ecIdent.ml b/src/ecIdent.ml index 60ab346526..9487c0e42c 100644 --- a/src/ecIdent.ml +++ b/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 (* -------------------------------------------------------------------- *) diff --git a/src/ecIdent.mli b/src/ecIdent.mli index 988430a72e..82942edb77 100644 --- a/src/ecIdent.mli +++ b/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 diff --git a/src/ecPath.ml b/src/ecPath.ml index 091840b6bd..0cb0edf4da 100644 --- a/src/ecPath.ml +++ b/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 = diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index c428b8553d..fd8171647b 100644 --- a/src/ecPrinting.ml +++ b/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 diff --git a/src/ecTypes.ml b/src/ecTypes.ml index 3da35d7287..87efc57bee 100644 --- a/src/ecTypes.ml +++ b/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))