1(* Title: Pure/name.ML 2 Author: Makarius 3 4Names of basic logical entities (variables etc.). 5*) 6 7signature NAME = 8sig 9 val uu: string 10 val uu_: string 11 val aT: string 12 val bound: int -> string 13 val is_bound: string -> bool 14 val internal: string -> string 15 val dest_internal: string -> string 16 val is_internal: string -> bool 17 val reject_internal: string * Position.T list -> unit 18 val skolem: string -> string 19 val dest_skolem: string -> string 20 val is_skolem: string -> bool 21 val reject_skolem: string * Position.T list -> unit 22 val clean_index: string * int -> string * int 23 val clean: string -> string 24 type context 25 val context: context 26 val make_context: string list -> context 27 val declare: string -> context -> context 28 val is_declared: context -> string -> bool 29 val invent: context -> string -> int -> string list 30 val invent_names: context -> string -> 'a list -> (string * 'a) list 31 val invent_list: string list -> string -> int -> string list 32 val variant: string -> context -> string * context 33 val variant_list: string list -> string list -> string list 34 val enforce_case: bool -> string -> string 35 val desymbolize: bool option -> string -> string 36end; 37 38structure Name: NAME = 39struct 40 41(** common defaults **) 42 43val uu = "uu"; 44val uu_ = "uu_"; 45val aT = "'a"; 46 47 48 49(** special variable names **) 50 51(* encoded bounds *) 52 53(*names for numbered variables -- 54 preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*) 55 56val small_int = Vector.tabulate (1000, fn i => 57 let val leading = if i < 10 then "00" else if i < 100 then "0" else "" 58 in ":" ^ leading ^ string_of_int i end); 59 60fun bound n = 61 if n < 1000 then Vector.sub (small_int, n) 62 else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000); 63 64val is_bound = String.isPrefix ":"; 65 66 67(* internal names -- NB: internal subsumes skolem *) 68 69val internal = suffix "_"; 70val dest_internal = unsuffix "_"; 71val is_internal = String.isSuffix "_"; 72fun reject_internal (x, ps) = 73 if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else (); 74 75val skolem = suffix "__"; 76val dest_skolem = unsuffix "__"; 77val is_skolem = String.isSuffix "__"; 78fun reject_skolem (x, ps) = 79 if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else (); 80 81fun clean_index (x, i) = 82 (case try dest_internal x of 83 NONE => (x, i) 84 | SOME x' => clean_index (x', i + 1)); 85 86fun clean x = #1 (clean_index (x, 0)); 87 88 89 90(** generating fresh names **) 91 92(* context *) 93 94datatype context = 95 Context of string option Symtab.table; (*declared names with latest renaming*) 96 97fun declare x (Context tab) = 98 Context (Symtab.default (clean x, NONE) tab); 99 100fun declare_renaming (x, x') (Context tab) = 101 Context (Symtab.update (clean x, SOME (clean x')) tab); 102 103fun is_declared (Context tab) = Symtab.defined tab; 104fun declared (Context tab) = Symtab.lookup tab; 105 106val context = Context Symtab.empty |> fold declare ["", "'"]; 107fun make_context used = fold declare used context; 108 109 110(* invent names *) 111 112fun invent ctxt = 113 let 114 fun invs _ 0 = [] 115 | invs x n = 116 let val x' = Symbol.bump_string x 117 in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end; 118 in invs o clean end; 119 120fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs; 121 122val invent_list = invent o make_context; 123 124 125(* variants *) 126 127(*makes a variant of a name distinct from already used names in a 128 context; preserves a suffix of underscores "_"*) 129fun variant name ctxt = 130 let 131 fun vary x = 132 (case declared ctxt x of 133 NONE => x 134 | SOME x' => vary (Symbol.bump_string (the_default x x'))); 135 136 val (x, n) = clean_index (name, 0); 137 val (x', ctxt') = 138 if not (is_declared ctxt x) then (x, declare x ctxt) 139 else 140 let 141 val x0 = Symbol.bump_init x; 142 val x' = vary x0; 143 val ctxt' = ctxt 144 |> x0 <> x' ? declare_renaming (x0, x') 145 |> declare x'; 146 in (x', ctxt') end; 147 in (x' ^ replicate_string n "_", ctxt') end; 148 149fun variant_list used names = #1 (make_context used |> fold_map variant names); 150 151 152(* names conforming to typical requirements of identifiers in the world outside *) 153 154fun enforce_case' false cs = 155 (if forall Symbol.is_ascii_upper cs then map else nth_map 0) Symbol.to_ascii_lower cs 156 | enforce_case' true cs = 157 nth_map 0 Symbol.to_ascii_upper cs; 158 159fun enforce_case upper = implode o enforce_case' upper o raw_explode; 160 161fun desymbolize perhaps_upper "" = 162 if the_default false perhaps_upper then "X" else "x" 163 | desymbolize perhaps_upper s = 164 let 165 val xs as (x :: _) = Symbol.explode s; 166 val ys = 167 if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs 168 else "x" :: xs; 169 fun is_valid x = 170 Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x; 171 fun sep [] = [] 172 | sep (xs as "_" :: _) = xs 173 | sep xs = "_" :: xs; 174 fun desep ("_" :: xs) = xs 175 | desep xs = xs; 176 fun desymb x xs = 177 if is_valid x then x :: xs 178 else 179 (case Symbol.decode x of 180 Symbol.Sym name => "_" :: raw_explode name @ sep xs 181 | _ => sep xs); 182 val upper_lower = Option.map enforce_case' perhaps_upper |> the_default I; 183 in fold_rev desymb ys [] |> desep |> upper_lower |> implode end; 184 185end; 186