author | wenzelm |
Sat, 25 May 2013 17:40:44 +0200 | |
changeset 52147 | 9943f8067f11 |
parent 52138 | e21426f244aa |
child 52265 | bb907eba5902 |
permissions | -rw-r--r-- |
52136 | 1 |
(* Title: Tools/Code/ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
||
4 |
Data related to symbols in programs: constants, type constructors, classes, |
|
5 |
class relations, class instances, modules. |
|
6 |
*) |
|
7 |
||
8 |
signature CODE_SYMBOL = |
|
9 |
sig |
|
10 |
datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = |
|
11 |
Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | |
|
12 |
Class_Relation of 'd | Class_Instance of 'e | Module of 'f |
|
52138
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
13 |
type symbol = (string, string, class, string * class, class * class, string) attr |
52136 | 14 |
val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l) |
15 |
-> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr |
|
16 |
val maps_attr: ('a -> 'g list) -> ('b -> 'h list) |
|
17 |
-> ('c -> 'i list) -> ('d -> 'j list) -> ('e -> 'k list) -> ('f -> 'l list) |
|
18 |
-> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr list |
|
19 |
val maps_attr': ('a -> ('m * 'g) list) -> ('b -> ('m * 'h) list) |
|
20 |
-> ('c -> ('m * 'i) list) -> ('d -> ('m * 'j) list) -> ('e -> ('m * 'k) list) -> ('f -> ('m * 'l) list) |
|
21 |
-> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('m * ('g, 'h, 'i, 'j, 'k, 'l) attr) list |
|
22 |
type ('a, 'b, 'c, 'd, 'e, 'f) data |
|
23 |
val empty_data: ('a, 'b, 'c, 'd, 'e, 'f) data |
|
24 |
val merge_data: ('a, 'b, 'c, 'd, 'e, 'f) data * ('a, 'b, 'c, 'd, 'e, 'f) data |
|
25 |
-> ('a, 'b, 'c, 'd, 'e, 'f) data |
|
52138
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
26 |
val set_data: (string * 'a option, string * 'b option, string * 'c option, |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
27 |
(class * class) * 'd option, (string * class) * 'e option, string * 'f option) attr |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
28 |
-> ('a, 'b, 'c, 'd, 'e, 'f) data -> ('a, 'b, 'c, 'd, 'e, 'f) data |
52136 | 29 |
val lookup_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'a option |
30 |
val lookup_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'b option |
|
31 |
val lookup_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class -> 'c option |
|
32 |
val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option |
|
33 |
val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option |
|
34 |
val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option |
|
52138
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
35 |
val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option |
52136 | 36 |
val dest_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'a) list |
37 |
val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'b) list |
|
38 |
val dest_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (class * 'c) list |
|
39 |
val dest_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((class * class) * 'd) list |
|
40 |
val dest_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((string * class) * 'e) list |
|
41 |
val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list |
|
52138
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
42 |
val quote_symbol: Proof.context -> symbol -> string |
52136 | 43 |
end; |
44 |
||
45 |
structure Code_Symbol : CODE_SYMBOL = |
|
46 |
struct |
|
47 |
||
48 |
(* data for symbols *) |
|
49 |
||
50 |
datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = |
|
51 |
Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f; |
|
52 |
||
52138
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
53 |
type symbol = (string, string, class, string * class, class * class, string) attr; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
54 |
|
52136 | 55 |
fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x) |
56 |
| map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x) |
|
57 |
| map_attr const tyco class classrel inst module (Type_Class x) = Type_Class (class x) |
|
58 |
| map_attr const tyco class classrel inst module (Class_Relation x) = Class_Relation (classrel x) |
|
59 |
| map_attr const tyco class classrel inst module (Class_Instance x) = Class_Instance (inst x) |
|
60 |
| map_attr const tyco class classrel inst module (Module x) = Module (module x); |
|
61 |
||
62 |
fun maps_attr const tyco class classrel inst module (Constant x) = map Constant (const x) |
|
63 |
| maps_attr const tyco class classrel inst module (Type_Constructor x) = map Type_Constructor (tyco x) |
|
64 |
| maps_attr const tyco class classrel inst module (Type_Class x) = map Type_Class (class x) |
|
65 |
| maps_attr const tyco class classrel inst module (Class_Relation x) = map Class_Relation (classrel x) |
|
66 |
| maps_attr const tyco class classrel inst module (Class_Instance x) = map Class_Instance (inst x) |
|
67 |
| maps_attr const tyco class classrel inst module (Module x) = map Module (module x); |
|
68 |
||
69 |
fun maps_attr' const tyco class classrel inst module (Constant x) = (map o apsnd) Constant (const x) |
|
70 |
| maps_attr' const tyco class classrel inst module (Type_Constructor x) = (map o apsnd) Type_Constructor (tyco x) |
|
71 |
| maps_attr' const tyco class classrel inst module (Type_Class x) = (map o apsnd) Type_Class (class x) |
|
72 |
| maps_attr' const tyco class classrel inst module (Class_Relation x) = (map o apsnd) Class_Relation (classrel x) |
|
73 |
| maps_attr' const tyco class classrel inst module (Class_Instance x) = (map o apsnd) Class_Instance (inst x) |
|
74 |
| maps_attr' const tyco class classrel inst module (Module x) = (map o apsnd) Module (module x); |
|
75 |
||
76 |
datatype ('a, 'b, 'c, 'd, 'e, 'f) data = |
|
77 |
Data of { constant: 'a Symtab.table, type_constructor: 'b Symtab.table, |
|
78 |
type_class: 'c Symtab.table, class_relation: 'd Symreltab.table, class_instance: 'e Symreltab.table, |
|
79 |
module: 'f Symtab.table }; |
|
80 |
||
81 |
fun make_data constant type_constructor type_class class_relation class_instance module = |
|
82 |
Data { constant = constant, type_constructor = type_constructor, |
|
83 |
type_class = type_class, class_relation = class_relation, class_instance = class_instance, module = module }; |
|
84 |
fun dest_data (Data x) = x; |
|
85 |
fun map_data map_constant map_type_constructor map_type_class map_class_relation map_class_instance map_module |
|
86 |
(Data { constant, type_constructor, type_class, class_relation, class_instance, module }) = |
|
87 |
Data { constant = map_constant constant, type_constructor = map_type_constructor type_constructor, |
|
88 |
type_class = map_type_class type_class, class_relation = map_class_relation class_relation, |
|
89 |
class_instance = map_class_instance class_instance, module = map_module module }; |
|
90 |
||
91 |
val empty_data = Data { constant = Symtab.empty, type_constructor = Symtab.empty, |
|
92 |
type_class = Symtab.empty, class_relation = Symreltab.empty, class_instance = Symreltab.empty, module = Symtab.empty }; |
|
93 |
fun merge_data (Data { constant = constant1, type_constructor = type_constructor1, |
|
94 |
type_class = type_class1, class_instance = class_instance1, class_relation = class_relation1, module = module1 }, |
|
95 |
Data { constant = constant2, type_constructor = type_constructor2, |
|
96 |
type_class = type_class2, class_instance = class_instance2, class_relation = class_relation2, module = module2 }) = |
|
97 |
make_data (Symtab.join (K snd) (constant1, constant2)) |
|
98 |
(Symtab.join (K snd) (type_constructor1, type_constructor2)) |
|
99 |
(Symtab.join (K snd) (type_class1, type_class2)) |
|
100 |
(Symreltab.join (K snd) (class_relation1, class_relation2)) |
|
101 |
(Symreltab.join (K snd) (class_instance1, class_instance2)) |
|
102 |
(Symtab.join (K snd) (module1, module2)); (*prefer later entries: K snd*) |
|
103 |
||
104 |
fun set_sym (sym, NONE) = Symtab.delete_safe sym |
|
105 |
| set_sym (sym, SOME y) = Symtab.update (sym, y); |
|
106 |
fun set_symrel (symrel, NONE) = Symreltab.delete_safe symrel |
|
107 |
| set_symrel (symrel, SOME y) = Symreltab.update (symrel, y); |
|
108 |
||
109 |
fun set_data (Constant x) = map_data (set_sym x) I I I I I |
|
110 |
| set_data (Type_Constructor x) = map_data I (set_sym x) I I I I |
|
111 |
| set_data (Type_Class x) = map_data I I (set_sym x) I I I |
|
112 |
| set_data (Class_Relation x) = map_data I I I (set_symrel x) I I |
|
113 |
| set_data (Class_Instance x) = map_data I I I I (set_symrel x) I |
|
114 |
| set_data (Module x) = map_data I I I I I (set_sym x); |
|
115 |
||
52138
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
116 |
fun lookup_constant_data x = (Symtab.lookup o #constant o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
117 |
fun lookup_type_constructor_data x = (Symtab.lookup o #type_constructor o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
118 |
fun lookup_type_class_data x = (Symtab.lookup o #type_class o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
119 |
fun lookup_class_relation_data x = (Symreltab.lookup o #class_relation o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
120 |
fun lookup_class_instance_data x = (Symreltab.lookup o #class_instance o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
121 |
fun lookup_module_data x = (Symtab.lookup o #module o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
122 |
|
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
123 |
fun lookup data (Constant x) = lookup_constant_data data x |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
124 |
| lookup data (Type_Constructor x) = lookup_type_constructor_data data x |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
125 |
| lookup data (Type_Class x) = lookup_type_class_data data x |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
126 |
| lookup data (Class_Relation x) = lookup_class_relation_data data x |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
127 |
| lookup data (Class_Instance x) = lookup_class_instance_data data x |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
128 |
| lookup data (Module x) = lookup_module_data data x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
129 |
|
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
130 |
fun dest_constant_data x = (Symtab.dest o #constant o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
131 |
fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
132 |
fun dest_type_class_data x = (Symtab.dest o #type_class o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
133 |
fun dest_class_relation_data x = (Symreltab.dest o #class_relation o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
134 |
fun dest_class_instance_data x = (Symreltab.dest o #class_instance o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
135 |
fun dest_module_data x = (Symtab.dest o #module o dest_data) x; |
e21426f244aa
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents:
52136
diff
changeset
|
136 |
|
52136 | 137 |
fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) |
138 |
| quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco) |
|
139 |
| quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class) |
|
140 |
| quote_symbol ctxt (Class_Relation (sub, super)) = |
|
141 |
quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super) |
|
142 |
| quote_symbol ctxt (Class_Instance (tyco, class)) = |
|
143 |
quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ quote (Proof_Context.extern_class ctxt class); |
|
144 |
||
145 |
end; |