18387
|
1 |
(* Title: Pure/General/name_mangler.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
|
|
5 |
Generic name mangler -- provides bijective mappings from any expressions
|
|
6 |
to strings and vice versa.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature NAME_MANGLER =
|
|
10 |
sig
|
|
11 |
type ctxt
|
|
12 |
type src
|
|
13 |
type T
|
18453
|
14 |
val mk_unique: ('b * 'b -> bool) -> ('a * int -> 'b)
|
|
15 |
-> 'a -> 'b list -> 'b * 'b list
|
|
16 |
val mk_unique_multi: ('b * 'b -> bool) -> ('a * int -> 'b)
|
|
17 |
-> 'a list -> 'b list -> 'b list * 'b list
|
|
18 |
val empty: T
|
18387
|
19 |
val get: ctxt -> T -> src -> string
|
|
20 |
val rev: ctxt -> T -> string -> src
|
|
21 |
val declare: ctxt -> src -> T -> string * T
|
18453
|
22 |
val declare_multi: ctxt -> src list -> T -> string list * T
|
|
23 |
val merge: T * T -> T
|
|
24 |
val dest: T -> (src * string) list
|
18387
|
25 |
end;
|
|
26 |
|
|
27 |
functor NameManglerFun (
|
|
28 |
type ctxt
|
|
29 |
type src
|
|
30 |
val ord: src * src -> order
|
|
31 |
val mk: ctxt -> src * int -> string
|
|
32 |
val is_valid: ctxt -> string -> bool
|
|
33 |
val maybe_unique: ctxt -> src -> string option
|
|
34 |
val re_mangle: ctxt -> string -> src
|
|
35 |
) : NAME_MANGLER =
|
|
36 |
struct
|
|
37 |
|
|
38 |
structure Srctab = TableFun (
|
|
39 |
type key = src
|
|
40 |
val ord = ord
|
|
41 |
);
|
|
42 |
|
|
43 |
type ctxt = ctxt;
|
|
44 |
type src = src;
|
|
45 |
type T = string Srctab.table * src Symtab.table;
|
|
46 |
|
|
47 |
fun mk_unique eq mk seed used =
|
|
48 |
let
|
|
49 |
fun mk_name i =
|
|
50 |
let
|
|
51 |
val name = mk (seed, i)
|
|
52 |
in
|
|
53 |
if member eq used name
|
|
54 |
then mk_name (i+1)
|
|
55 |
else name
|
|
56 |
end;
|
|
57 |
val name = mk_name 0;
|
|
58 |
in (name, name :: used) end;
|
|
59 |
|
18453
|
60 |
fun mk_unique_multi eq mk seeds used =
|
|
61 |
let
|
|
62 |
fun mk_names i =
|
18494
|
63 |
if i < 2 then
|
|
64 |
let
|
|
65 |
val names = map (fn seed => mk (seed, i)) seeds
|
|
66 |
in
|
|
67 |
if null (gen_inter eq (used, names))
|
|
68 |
andalso (not oo has_duplicates) eq names
|
|
69 |
then names
|
|
70 |
else mk_names (i+1)
|
|
71 |
end
|
|
72 |
else
|
|
73 |
used
|
|
74 |
|> fold_map (mk_unique eq mk) seeds
|
|
75 |
|> fst;
|
|
76 |
val names = mk_names 0;
|
18453
|
77 |
in (names, fold cons names used) end;
|
|
78 |
|
|
79 |
val empty = (Srctab.empty, Symtab.empty);
|
|
80 |
|
18387
|
81 |
fun get ctxt (tab_f, _) x =
|
|
82 |
case Srctab.lookup tab_f x
|
|
83 |
of SOME s => s
|
|
84 |
| NONE => (the o maybe_unique ctxt) x;
|
|
85 |
|
|
86 |
fun rev ctxt (_, tab_r) s =
|
|
87 |
case Symtab.lookup tab_r s
|
|
88 |
of SOME x => x
|
|
89 |
| NONE => re_mangle ctxt s;
|
|
90 |
|
|
91 |
fun declare ctxt x (tabs as (tab_f, tab_r)) =
|
|
92 |
case maybe_unique ctxt x
|
|
93 |
of NONE =>
|
|
94 |
let
|
|
95 |
fun mk_it (seed, i) =
|
|
96 |
let
|
|
97 |
val name = mk ctxt (seed, i)
|
18455
|
98 |
in
|
|
99 |
if is_valid ctxt name
|
|
100 |
andalso (not oo Symtab.defined) tab_r name
|
|
101 |
then name
|
|
102 |
else mk_it (seed, i+1)
|
|
103 |
end;
|
18387
|
104 |
val name = (fst oooo mk_unique) (op =) mk_it x [];
|
|
105 |
in
|
|
106 |
(name,
|
|
107 |
(tab_f |> Srctab.update (x, name),
|
|
108 |
tab_r |> Symtab.update (name, x)))
|
|
109 |
end
|
|
110 |
| SOME s => (s, tabs)
|
|
111 |
|
18453
|
112 |
fun declare_multi ctxt xs (tabs as (tab_f, tab_r)) =
|
|
113 |
let
|
|
114 |
val xs' = map (maybe_unique ctxt) xs
|
|
115 |
in
|
|
116 |
if forall is_some xs'
|
|
117 |
then (map the xs', tabs)
|
|
118 |
else
|
|
119 |
let
|
|
120 |
fun mk_it (seed, i) =
|
|
121 |
let
|
|
122 |
val name = mk ctxt (seed, i)
|
18455
|
123 |
in
|
|
124 |
if is_valid ctxt name
|
|
125 |
andalso (not oo Symtab.defined) tab_r name
|
|
126 |
then name
|
|
127 |
else mk_it (seed, i+1)
|
|
128 |
end;
|
18453
|
129 |
val names = (fst oooo mk_unique_multi) (op =) mk_it xs [];
|
|
130 |
in
|
|
131 |
(names,
|
|
132 |
(tab_f |> fold2 (curry Srctab.update) xs names,
|
|
133 |
tab_r |> fold2 (curry Symtab.update) names xs))
|
|
134 |
end
|
|
135 |
end;
|
|
136 |
|
|
137 |
fun merge ((tab_f_1, tab_r_1), (tab_f_2, tab_r_2)) =
|
|
138 |
(Srctab.merge (op = : string * string -> bool) (tab_f_1, tab_f_2),
|
19596
|
139 |
Symtab.merge (is_equal o ord) (tab_r_1, tab_r_2));
|
18453
|
140 |
|
|
141 |
fun dest (tab_f, _) = Srctab.dest tab_f;
|
|
142 |
|
18387
|
143 |
end; |