author | wenzelm |
Sun, 08 Mar 2009 17:26:14 +0100 | |
changeset 30364 | 577edc39b501 |
parent 30161 | c26e515f1c29 |
child 30648 | 17365ef082f3 |
permissions | -rw-r--r-- |
24219 | 1 |
(* Title: Tools/code/code_name.ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
||
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
4 |
Some code generator infrastructure concerning names. |
24219 | 5 |
*) |
6 |
||
7 |
signature CODE_NAME = |
|
8 |
sig |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
9 |
structure StringPairTab: TABLE |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
10 |
val first_upper: string -> string |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
11 |
val first_lower: string -> string |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
12 |
val dest_name: string -> string * string |
27103 | 13 |
|
24219 | 14 |
val purify_var: string -> string |
15 |
val purify_tvar: string -> string |
|
25337 | 16 |
val purify_sym: string -> string |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
17 |
val purify_base: bool -> string -> string |
24219 | 18 |
val check_modulename: string -> string |
27103 | 19 |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
20 |
type var_ctxt |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
21 |
val make_vars: string list -> var_ctxt |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
22 |
val intro_vars: string list -> var_ctxt -> var_ctxt |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
23 |
val lookup_var: var_ctxt -> string -> string |
24219 | 24 |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
25 |
val read_const_exprs: theory -> string list -> string list * string list |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
26 |
val mk_name_module: Name.context -> string option -> (string -> string option) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
27 |
-> 'a Graph.T -> string -> string |
24219 | 28 |
end; |
29 |
||
28054 | 30 |
structure Code_Name: CODE_NAME = |
24219 | 31 |
struct |
32 |
||
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
33 |
(** auxiliary **) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
34 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
35 |
structure StringPairTab = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
36 |
TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord); |
27103 | 37 |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
38 |
val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
39 |
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
40 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
41 |
val dest_name = |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30161
diff
changeset
|
42 |
apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode; |
27103 | 43 |
|
44 |
||
24219 | 45 |
(** purification **) |
46 |
||
25337 | 47 |
fun purify_name upper lower = |
24219 | 48 |
let |
49 |
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'"; |
|
50 |
val is_junk = not o is_valid andf Symbol.is_regular; |
|
51 |
val junk = Scan.many is_junk; |
|
52 |
val scan_valids = Symbol.scanner "Malformed input" |
|
53 |
((junk |-- |
|
54 |
(Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) |
|
55 |
--| junk)) |
|
25999 | 56 |
::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); |
25337 | 57 |
fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs |
58 |
else if lower then (if forall Symbol.is_ascii_upper cs |
|
59 |
then map else nth_map 0) Symbol.to_ascii_lower cs |
|
60 |
else cs; |
|
24219 | 61 |
in |
62 |
explode |
|
63 |
#> scan_valids |
|
64 |
#> space_implode "_" |
|
65 |
#> explode |
|
66 |
#> upper_lower |
|
67 |
#> implode |
|
68 |
end; |
|
69 |
||
70 |
fun purify_var "" = "x" |
|
25337 | 71 |
| purify_var v = purify_name false true v; |
24219 | 72 |
|
73 |
fun purify_tvar "" = "'a" |
|
74 |
| purify_tvar v = |
|
75 |
(unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v; |
|
76 |
||
77 |
val purify_prefix = |
|
78 |
explode |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
79 |
(*FIMXE should disappear as soon as hierarchical theory name spaces are available*) |
24219 | 80 |
#> Symbol.scanner "Malformed name" |
81 |
(Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular)) |
|
82 |
#> implode |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30161
diff
changeset
|
83 |
#> Long_Name.explode |
25337 | 84 |
#> map (purify_name true false); |
24219 | 85 |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
86 |
(*FIMXE non-canonical function treating non-canonical names*) |
25337 | 87 |
fun purify_base _ "op &" = "and" |
88 |
| purify_base _ "op |" = "or" |
|
89 |
| purify_base _ "op -->" = "implies" |
|
90 |
| purify_base _ "{}" = "empty" |
|
91 |
| purify_base _ "op :" = "member" |
|
92 |
| purify_base _ "op Int" = "intersect" |
|
93 |
| purify_base _ "op Un" = "union" |
|
94 |
| purify_base _ "*" = "product" |
|
95 |
| purify_base _ "+" = "sum" |
|
96 |
| purify_base lower s = if String.isPrefix "op =" s |
|
97 |
then "eq" ^ purify_name false lower s |
|
98 |
else purify_name false lower s; |
|
99 |
||
100 |
val purify_sym = purify_base false; |
|
24219 | 101 |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
102 |
fun check_modulename mn = |
24219 | 103 |
let |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30161
diff
changeset
|
104 |
val mns = Long_Name.explode mn; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
105 |
val mns' = map (purify_name true false) mns; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
106 |
in |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
107 |
if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n" |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30161
diff
changeset
|
108 |
^ "perhaps try " ^ quote (Long_Name.implode mns')) |
24219 | 109 |
end; |
110 |
||
111 |
||
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
112 |
(** variable name contexts **) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
113 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
114 |
type var_ctxt = string Symtab.table * Name.context; |
24219 | 115 |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
116 |
fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
117 |
Name.make_context names); |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
118 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
119 |
fun intro_vars names (namemap, namectxt) = |
24219 | 120 |
let |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
121 |
val (names', namectxt') = Name.variants names namectxt; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
122 |
val namemap' = fold2 (curry Symtab.update) names names' namemap; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
123 |
in (namemap', namectxt') end; |
24219 | 124 |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
125 |
fun lookup_var (namemap, _) name = case Symtab.lookup namemap name |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
126 |
of SOME name' => name' |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
127 |
| NONE => error ("Invalid name in context: " ^ quote name); |
24219 | 128 |
|
129 |
||
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
130 |
(** misc **) |
24219 | 131 |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
132 |
fun read_const_exprs thy = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
133 |
let |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
134 |
fun consts_of some_thyname = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
135 |
let |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
136 |
val thy' = case some_thyname |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
137 |
of SOME thyname => ThyInfo.the_theory thyname thy |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
138 |
| NONE => thy; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
139 |
val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
140 |
((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') []; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
141 |
fun belongs_here c = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
142 |
not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy')) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
143 |
in case some_thyname |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
144 |
of NONE => cs |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
145 |
| SOME thyname => filter belongs_here cs |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
146 |
end; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
147 |
fun read_const_expr "*" = ([], consts_of NONE) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
148 |
| read_const_expr s = if String.isSuffix ".*" s |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
149 |
then ([], consts_of (SOME (unsuffix ".*" s))) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
150 |
else ([Code_Unit.read_const thy s], []); |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
151 |
in pairself flat o split_list o map read_const_expr end; |
24219 | 152 |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
153 |
fun mk_name_module reserved_names module_prefix module_alias program = |
24219 | 154 |
let |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
155 |
fun mk_alias name = case module_alias name |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
156 |
of SOME name' => name' |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
157 |
| NONE => name |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30161
diff
changeset
|
158 |
|> Long_Name.explode |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
159 |
|> map (fn name => (the_single o fst) (Name.variants [name] reserved_names)) |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30161
diff
changeset
|
160 |
|> Long_Name.implode; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
161 |
fun mk_prefix name = case module_prefix |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30161
diff
changeset
|
162 |
of SOME module_prefix => Long_Name.append module_prefix name |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
163 |
| NONE => name; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
164 |
val tab = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
165 |
Symtab.empty |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
166 |
|> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
167 |
o fst o dest_name o fst) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
168 |
program |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28346
diff
changeset
|
169 |
in the o Symtab.lookup tab end; |
24219 | 170 |
|
171 |
end; |