author | wenzelm |
Fri, 21 Apr 2017 15:26:24 +0200 | |
changeset 65534 | b6250ee6ce79 |
parent 56812 | baef1c110f12 |
child 69137 | 90fce429e1bc |
permissions | -rw-r--r-- |
20089 | 1 |
(* Title: Pure/name.ML |
2 |
Author: Makarius |
|
3 |
||
28965 | 4 |
Names of basic logical entities (variables etc.). |
20089 | 5 |
*) |
6 |
||
7 |
signature NAME = |
|
8 |
sig |
|
24849 | 9 |
val uu: string |
43683 | 10 |
val uu_: string |
24849 | 11 |
val aT: string |
20089 | 12 |
val bound: int -> string |
13 |
val is_bound: string -> bool |
|
14 |
val internal: string -> string |
|
15 |
val dest_internal: string -> string |
|
55948 | 16 |
val is_internal: string -> bool |
55949 | 17 |
val reject_internal: string * Position.T list -> unit |
20089 | 18 |
val skolem: string -> string |
19 |
val dest_skolem: string -> string |
|
55948 | 20 |
val is_skolem: string -> bool |
55949 | 21 |
val reject_skolem: string * Position.T list -> unit |
20089 | 22 |
val clean_index: string * int -> string * int |
23 |
val clean: string -> string |
|
24 |
type context |
|
25 |
val context: context |
|
20158 | 26 |
val make_context: string list -> context |
20089 | 27 |
val declare: string -> context -> context |
20158 | 28 |
val is_declared: context -> string -> bool |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
29 |
val invent: context -> string -> int -> string list |
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
30 |
val invent_names: context -> string -> 'a list -> (string * 'a) list |
20089 | 31 |
val invent_list: string list -> string -> int -> string list |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset
|
32 |
val variant: string -> context -> string * context |
20089 | 33 |
val variant_list: string list -> string list -> string list |
56812 | 34 |
val enforce_case: bool -> string -> string |
56811 | 35 |
val desymbolize: bool option -> string -> string |
20089 | 36 |
end; |
37 |
||
38 |
structure Name: NAME = |
|
39 |
struct |
|
40 |
||
24849 | 41 |
(** common defaults **) |
42 |
||
43 |
val uu = "uu"; |
|
43683 | 44 |
val uu_ = "uu_"; |
24849 | 45 |
val aT = "'a"; |
46 |
||
47 |
||
20089 | 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 |
||
56 |
val 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 |
||
60 |
fun 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 |
||
64 |
val is_bound = String.isPrefix ":"; |
|
65 |
||
66 |
||
55949 | 67 |
(* internal names -- NB: internal subsumes skolem *) |
20089 | 68 |
|
69 |
val internal = suffix "_"; |
|
70 |
val dest_internal = unsuffix "_"; |
|
55948 | 71 |
val is_internal = String.isSuffix "_"; |
55949 | 72 |
fun reject_internal (x, ps) = |
73 |
if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else (); |
|
20089 | 74 |
|
75 |
val skolem = suffix "__"; |
|
76 |
val dest_skolem = unsuffix "__"; |
|
55948 | 77 |
val is_skolem = String.isSuffix "__"; |
55949 | 78 |
fun reject_skolem (x, ps) = |
79 |
if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else (); |
|
20089 | 80 |
|
20099 | 81 |
fun clean_index (x, i) = |
82 |
(case try dest_internal x of |
|
83 |
NONE => (x, i) |
|
84 |
| SOME x' => clean_index (x', i + 1)); |
|
20089 | 85 |
|
86 |
fun clean x = #1 (clean_index (x, 0)); |
|
87 |
||
88 |
||
89 |
||
90 |
(** generating fresh names **) |
|
91 |
||
92 |
(* context *) |
|
93 |
||
94 |
datatype context = |
|
95 |
Context of string option Symtab.table; (*declared names with latest renaming*) |
|
96 |
||
20099 | 97 |
fun declare x (Context tab) = |
98 |
Context (Symtab.default (clean x, NONE) tab); |
|
99 |
||
100 |
fun declare_renaming (x, x') (Context tab) = |
|
101 |
Context (Symtab.update (clean x, SOME (clean x')) tab); |
|
20089 | 102 |
|
20158 | 103 |
fun is_declared (Context tab) = Symtab.defined tab; |
20089 | 104 |
fun declared (Context tab) = Symtab.lookup tab; |
105 |
||
20121 | 106 |
val context = Context Symtab.empty |> fold declare ["", "'"]; |
20089 | 107 |
fun make_context used = fold declare used context; |
108 |
||
109 |
||
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
110 |
(* invent names *) |
20089 | 111 |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
112 |
fun invent ctxt = |
20089 | 113 |
let |
114 |
fun invs _ 0 = [] |
|
115 |
| invs x n = |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
116 |
let val x' = Symbol.bump_string x |
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
117 |
in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end; |
20099 | 118 |
in invs o clean end; |
20089 | 119 |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
120 |
fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs; |
20198 | 121 |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
122 |
val invent_list = invent o make_context; |
20089 | 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 "_"*) |
|
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset
|
129 |
fun variant name ctxt = |
20089 | 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 |
||
20121 | 136 |
val (x, n) = clean_index (name, 0); |
20089 | 137 |
val (x', ctxt') = |
20158 | 138 |
if not (is_declared ctxt x) then (x, declare x ctxt) |
20089 | 139 |
else |
140 |
let |
|
141 |
val x0 = Symbol.bump_init x; |
|
142 |
val x' = vary x0; |
|
143 |
val ctxt' = ctxt |
|
21565 | 144 |
|> x0 <> x' ? declare_renaming (x0, x') |
20089 | 145 |
|> declare x'; |
146 |
in (x', ctxt') end; |
|
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset
|
147 |
in (x' ^ replicate_string n "_", ctxt') end; |
20089 | 148 |
|
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset
|
149 |
fun variant_list used names = #1 (make_context used |> fold_map variant names); |
20089 | 150 |
|
31013 | 151 |
|
31035 | 152 |
(* names conforming to typical requirements of identifiers in the world outside *) |
31013 | 153 |
|
56812 | 154 |
fun 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 |
||
159 |
fun enforce_case upper = implode o enforce_case' upper o raw_explode; |
|
160 |
||
56811 | 161 |
fun desymbolize perhaps_upper "" = |
162 |
if the_default false perhaps_upper then "X" else "x" |
|
163 |
| desymbolize perhaps_upper s = |
|
31013 | 164 |
let |
31035 | 165 |
val xs as (x :: _) = Symbol.explode s; |
33547 | 166 |
val ys = |
167 |
if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs |
|
31013 | 168 |
else "x" :: xs; |
169 |
fun is_valid x = |
|
34307 | 170 |
Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x; |
31013 | 171 |
fun sep [] = [] |
172 |
| sep (xs as "_" :: _) = xs |
|
173 |
| sep xs = "_" :: xs; |
|
31035 | 174 |
fun desep ("_" :: xs) = xs |
175 |
| desep xs = xs; |
|
33547 | 176 |
fun desymb x xs = |
177 |
if is_valid x then x :: xs |
|
31013 | 178 |
else |
33547 | 179 |
(case Symbol.decode x of |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
34307
diff
changeset
|
180 |
Symbol.Sym name => "_" :: raw_explode name @ sep xs |
33547 | 181 |
| _ => sep xs); |
56812 | 182 |
val upper_lower = Option.map enforce_case' perhaps_upper |> the_default I; |
31035 | 183 |
in fold_rev desymb ys [] |> desep |> upper_lower |> implode end; |
31013 | 184 |
|
20089 | 185 |
end; |