1 (* Title: Tools/code/code_name.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 Some code generator infrastructure concerning names. |
|
5 *) |
|
6 |
|
7 signature CODE_NAME = |
|
8 sig |
|
9 val purify_var: string -> string |
|
10 val purify_tvar: string -> string |
|
11 val purify_base: string -> string |
|
12 val check_modulename: string -> string |
|
13 |
|
14 val read_const_exprs: theory -> string list -> string list * string list |
|
15 end; |
|
16 |
|
17 structure Code_Name: CODE_NAME = |
|
18 struct |
|
19 |
|
20 (** purification **) |
|
21 |
|
22 fun purify_name upper = |
|
23 let |
|
24 fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'"; |
|
25 val is_junk = not o is_valid andf Symbol.is_regular; |
|
26 val junk = Scan.many is_junk; |
|
27 val scan_valids = Symbol.scanner "Malformed input" |
|
28 ((junk |-- |
|
29 (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) |
|
30 --| junk)) |
|
31 ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); |
|
32 fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs |
|
33 else (if forall Symbol.is_ascii_upper cs |
|
34 then map else nth_map 0) Symbol.to_ascii_lower cs; |
|
35 in |
|
36 explode |
|
37 #> scan_valids |
|
38 #> space_implode "_" |
|
39 #> explode |
|
40 #> upper_lower |
|
41 #> implode |
|
42 end; |
|
43 |
|
44 fun purify_var "" = "x" |
|
45 | purify_var v = purify_name false v; |
|
46 |
|
47 fun purify_tvar "" = "'a" |
|
48 | purify_tvar v = |
|
49 (unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v; |
|
50 |
|
51 val purify_prefix = |
|
52 explode |
|
53 (*FIMXE should disappear as soon as hierarchical theory name spaces are available*) |
|
54 #> Symbol.scanner "Malformed name" |
|
55 (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular)) |
|
56 #> implode |
|
57 #> Long_Name.explode |
|
58 #> map (purify_name true); |
|
59 |
|
60 (*FIMXE non-canonical function treating non-canonical names*) |
|
61 fun purify_base "op &" = "and" |
|
62 | purify_base "op |" = "or" |
|
63 | purify_base "op -->" = "implies" |
|
64 | purify_base "op :" = "member" |
|
65 | purify_base "*" = "product" |
|
66 | purify_base "+" = "sum" |
|
67 | purify_base s = if String.isPrefix "op =" s |
|
68 then "eq" ^ purify_name false s |
|
69 else purify_name false s; |
|
70 |
|
71 fun check_modulename mn = |
|
72 let |
|
73 val mns = Long_Name.explode mn; |
|
74 val mns' = map (purify_name true) mns; |
|
75 in |
|
76 if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n" |
|
77 ^ "perhaps try " ^ quote (Long_Name.implode mns')) |
|
78 end; |
|
79 |
|
80 |
|
81 (** misc **) |
|
82 |
|
83 fun read_const_exprs thy = |
|
84 let |
|
85 fun consts_of some_thyname = |
|
86 let |
|
87 val thy' = case some_thyname |
|
88 of SOME thyname => ThyInfo.the_theory thyname thy |
|
89 | NONE => thy; |
|
90 val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) |
|
91 ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') []; |
|
92 fun belongs_here c = |
|
93 not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy')) |
|
94 in case some_thyname |
|
95 of NONE => cs |
|
96 | SOME thyname => filter belongs_here cs |
|
97 end; |
|
98 fun read_const_expr "*" = ([], consts_of NONE) |
|
99 | read_const_expr s = if String.isSuffix ".*" s |
|
100 then ([], consts_of (SOME (unsuffix ".*" s))) |
|
101 else ([Code_Unit.read_const thy s], []); |
|
102 in pairself flat o split_list o map read_const_expr end; |
|
103 |
|
104 end; |
|