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