8 signature CODE_SYMBOL = |
8 signature CODE_SYMBOL = |
9 sig |
9 sig |
10 datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = |
10 datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = |
11 Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | |
11 Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | |
12 Class_Relation of 'd | Class_Instance of 'e | Module of 'f |
12 Class_Relation of 'd | Class_Instance of 'e | Module of 'f |
|
13 type symbol = (string, string, class, string * class, class * class, string) attr |
13 val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l) |
14 val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l) |
14 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr |
15 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr |
15 val maps_attr: ('a -> 'g list) -> ('b -> 'h list) |
16 val maps_attr: ('a -> 'g list) -> ('b -> 'h list) |
16 -> ('c -> 'i list) -> ('d -> 'j list) -> ('e -> 'k list) -> ('f -> 'l list) |
17 -> ('c -> 'i list) -> ('d -> 'j list) -> ('e -> 'k list) -> ('f -> 'l list) |
17 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr list |
18 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr list |
20 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('m * ('g, 'h, 'i, 'j, 'k, 'l) attr) list |
21 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('m * ('g, 'h, 'i, 'j, 'k, 'l) attr) list |
21 type ('a, 'b, 'c, 'd, 'e, 'f) data |
22 type ('a, 'b, 'c, 'd, 'e, 'f) data |
22 val empty_data: ('a, 'b, 'c, 'd, 'e, 'f) data |
23 val empty_data: ('a, 'b, 'c, 'd, 'e, 'f) data |
23 val merge_data: ('a, 'b, 'c, 'd, 'e, 'f) 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 |
24 -> ('a, 'b, 'c, 'd, 'e, 'f) data |
25 -> ('a, 'b, 'c, 'd, 'e, 'f) data |
|
26 val set_data: (string * 'a option, string * 'b option, string * 'c option, |
|
27 (class * class) * 'd option, (string * class) * 'e option, string * 'f option) attr |
|
28 -> ('a, 'b, 'c, 'd, 'e, 'f) data -> ('a, 'b, 'c, 'd, 'e, 'f) data |
25 val lookup_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'a option |
29 val lookup_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'a option |
26 val lookup_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'b option |
30 val lookup_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'b option |
27 val lookup_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class -> 'c option |
31 val lookup_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class -> 'c option |
28 val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option |
32 val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option |
29 val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option |
33 val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option |
30 val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option |
34 val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option |
|
35 val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option |
31 val dest_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'a) list |
36 val dest_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'a) list |
32 val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'b) list |
37 val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'b) list |
33 val dest_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (class * 'c) list |
38 val dest_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (class * 'c) list |
34 val dest_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((class * class) * 'd) list |
39 val dest_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((class * class) * 'd) list |
35 val dest_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((string * class) * 'e) list |
40 val dest_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((string * class) * 'e) list |
36 val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list |
41 val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list |
37 val set_data: (string * 'a option, string * 'b option, string * 'c option, |
42 val quote_symbol: Proof.context -> symbol -> string |
38 (class * class) * 'd option, (string * class) * 'e option, string * 'f option) attr |
|
39 -> ('a, 'b, 'c, 'd, 'e, 'f) data -> ('a, 'b, 'c, 'd, 'e, 'f) data |
|
40 val quote_symbol: Proof.context -> (string, string, class, string * class, class * class, string) attr -> string |
|
41 end; |
43 end; |
42 |
44 |
43 structure Code_Symbol : CODE_SYMBOL = |
45 structure Code_Symbol : CODE_SYMBOL = |
44 struct |
46 struct |
45 |
47 |
46 (* data for symbols *) |
48 (* data for symbols *) |
47 |
49 |
48 datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = |
50 datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = |
49 Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f; |
51 Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f; |
|
52 |
|
53 type symbol = (string, string, class, string * class, class * class, string) attr; |
50 |
54 |
51 fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x) |
55 fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x) |
52 | map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x) |
56 | map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x) |
53 | map_attr const tyco class classrel inst module (Type_Class x) = Type_Class (class x) |
57 | map_attr const tyco class classrel inst module (Type_Class x) = Type_Class (class x) |
54 | map_attr const tyco class classrel inst module (Class_Relation x) = Class_Relation (classrel x) |
58 | map_attr const tyco class classrel inst module (Class_Relation x) = Class_Relation (classrel x) |
95 (Symtab.join (K snd) (type_class1, type_class2)) |
99 (Symtab.join (K snd) (type_class1, type_class2)) |
96 (Symreltab.join (K snd) (class_relation1, class_relation2)) |
100 (Symreltab.join (K snd) (class_relation1, class_relation2)) |
97 (Symreltab.join (K snd) (class_instance1, class_instance2)) |
101 (Symreltab.join (K snd) (class_instance1, class_instance2)) |
98 (Symtab.join (K snd) (module1, module2)); (*prefer later entries: K snd*) |
102 (Symtab.join (K snd) (module1, module2)); (*prefer later entries: K snd*) |
99 |
103 |
100 fun lookup_constant_data x = (Symtab.lookup o #constant o dest_data) x; |
|
101 fun lookup_type_constructor_data x = (Symtab.lookup o #type_constructor o dest_data) x; |
|
102 fun lookup_type_class_data x = (Symtab.lookup o #type_class o dest_data) x; |
|
103 fun lookup_class_relation_data x = (Symreltab.lookup o #class_relation o dest_data) x; |
|
104 fun lookup_class_instance_data x = (Symreltab.lookup o #class_instance o dest_data) x; |
|
105 fun lookup_module_data x = (Symtab.lookup o #module o dest_data) x; |
|
106 |
|
107 fun dest_constant_data x = (Symtab.dest o #constant o dest_data) x; |
|
108 fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_data) x; |
|
109 fun dest_type_class_data x = (Symtab.dest o #type_class o dest_data) x; |
|
110 fun dest_class_relation_data x = (Symreltab.dest o #class_relation o dest_data) x; |
|
111 fun dest_class_instance_data x = (Symreltab.dest o #class_instance o dest_data) x; |
|
112 fun dest_module_data x = (Symtab.dest o #module o dest_data) x; |
|
113 |
|
114 fun set_sym (sym, NONE) = Symtab.delete_safe sym |
104 fun set_sym (sym, NONE) = Symtab.delete_safe sym |
115 | set_sym (sym, SOME y) = Symtab.update (sym, y); |
105 | set_sym (sym, SOME y) = Symtab.update (sym, y); |
116 fun set_symrel (symrel, NONE) = Symreltab.delete_safe symrel |
106 fun set_symrel (symrel, NONE) = Symreltab.delete_safe symrel |
117 | set_symrel (symrel, SOME y) = Symreltab.update (symrel, y); |
107 | set_symrel (symrel, SOME y) = Symreltab.update (symrel, y); |
118 |
108 |
121 | set_data (Type_Class x) = map_data I I (set_sym x) I I I |
111 | set_data (Type_Class x) = map_data I I (set_sym x) I I I |
122 | set_data (Class_Relation x) = map_data I I I (set_symrel x) I I |
112 | set_data (Class_Relation x) = map_data I I I (set_symrel x) I I |
123 | set_data (Class_Instance x) = map_data I I I I (set_symrel x) I |
113 | set_data (Class_Instance x) = map_data I I I I (set_symrel x) I |
124 | set_data (Module x) = map_data I I I I I (set_sym x); |
114 | set_data (Module x) = map_data I I I I I (set_sym x); |
125 |
115 |
|
116 fun lookup_constant_data x = (Symtab.lookup o #constant o dest_data) x; |
|
117 fun lookup_type_constructor_data x = (Symtab.lookup o #type_constructor o dest_data) x; |
|
118 fun lookup_type_class_data x = (Symtab.lookup o #type_class o dest_data) x; |
|
119 fun lookup_class_relation_data x = (Symreltab.lookup o #class_relation o dest_data) x; |
|
120 fun lookup_class_instance_data x = (Symreltab.lookup o #class_instance o dest_data) x; |
|
121 fun lookup_module_data x = (Symtab.lookup o #module o dest_data) x; |
|
122 |
|
123 fun lookup data (Constant x) = lookup_constant_data data x |
|
124 | lookup data (Type_Constructor x) = lookup_type_constructor_data data x |
|
125 | lookup data (Type_Class x) = lookup_type_class_data data x |
|
126 | lookup data (Class_Relation x) = lookup_class_relation_data data x |
|
127 | lookup data (Class_Instance x) = lookup_class_instance_data data x |
|
128 | lookup data (Module x) = lookup_module_data data x; |
|
129 |
|
130 fun dest_constant_data x = (Symtab.dest o #constant o dest_data) x; |
|
131 fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_data) x; |
|
132 fun dest_type_class_data x = (Symtab.dest o #type_class o dest_data) x; |
|
133 fun dest_class_relation_data x = (Symreltab.dest o #class_relation o dest_data) x; |
|
134 fun dest_class_instance_data x = (Symreltab.dest o #class_instance o dest_data) x; |
|
135 fun dest_module_data x = (Symtab.dest o #module o dest_data) x; |
|
136 |
126 fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) |
137 fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) |
127 | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco) |
138 | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco) |
128 | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class) |
139 | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class) |
129 | quote_symbol ctxt (Class_Relation (sub, super)) = |
140 | quote_symbol ctxt (Class_Relation (sub, super)) = |
130 quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super) |
141 quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super) |