3 |
3 |
4 Data related to symbols in programs: constants, type constructors, classes, |
4 Data related to symbols in programs: constants, type constructors, classes, |
5 class relations, class instances, modules. |
5 class relations, class instances, modules. |
6 *) |
6 *) |
7 |
7 |
8 signature CODE_SYMBOL = |
8 signature BASIC_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, class * class, string * class, string) attr |
13 end |
14 structure Table: TABLE; |
14 |
15 structure Graph: GRAPH; |
15 signature CODE_SYMBOL = |
16 val namespace_prefix: Proof.context -> symbol -> string |
16 sig |
17 val base_name: symbol -> string |
17 include BASIC_CODE_SYMBOL |
18 val quote: Proof.context -> symbol -> string |
18 type T = (string, string, class, class * class, string * class, string) attr |
19 val marker: symbol -> string |
19 structure Table: TABLE |
20 val value: symbol |
20 structure Graph: GRAPH |
21 val is_value: symbol -> bool |
21 val default_base: T -> string |
|
22 val default_prefix: Proof.context -> T -> string |
|
23 val quote: Proof.context -> T -> string |
|
24 val marker: T -> string |
|
25 val value: T |
|
26 val is_value: T -> bool |
22 val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l) |
27 val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l) |
23 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr |
28 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr |
24 val maps_attr: ('a -> 'g list) -> ('b -> 'h list) |
29 val maps_attr: ('a -> 'g list) -> ('b -> 'h list) |
25 -> ('c -> 'i list) -> ('d -> 'j list) -> ('e -> 'k list) -> ('f -> 'l list) |
30 -> ('c -> 'i list) -> ('d -> 'j list) -> ('e -> 'k list) -> ('f -> 'l list) |
26 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr list |
31 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr list |
38 val lookup_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'b option |
43 val lookup_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'b option |
39 val lookup_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class -> 'c option |
44 val lookup_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class -> 'c option |
40 val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option |
45 val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option |
41 val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option |
46 val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option |
42 val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option |
47 val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option |
43 val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option |
48 val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> T -> 'a option |
44 val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> symbol list |
49 val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> T list |
45 val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list |
50 val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list |
46 end; |
51 end; |
47 |
52 |
48 structure Code_Symbol : CODE_SYMBOL = |
53 structure Code_Symbol : CODE_SYMBOL = |
49 struct |
54 struct |
51 (* data for symbols *) |
56 (* data for symbols *) |
52 |
57 |
53 datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = |
58 datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = |
54 Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f; |
59 Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f; |
55 |
60 |
56 type symbol = (string, string, class, string * class, class * class, string) attr; |
61 type T = (string, string, class, string * class, class * class, string) attr; |
57 |
62 |
58 fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2) |
63 fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2) |
59 | symbol_ord (Constant _, _) = GREATER |
64 | symbol_ord (Constant _, _) = GREATER |
60 | symbol_ord (_, Constant _) = LESS |
65 | symbol_ord (_, Constant _) = LESS |
61 | symbol_ord (Type_Constructor tyco1, Type_Constructor tyco2) = fast_string_ord (tyco1, tyco2) |
66 | symbol_ord (Type_Constructor tyco1, Type_Constructor tyco2) = fast_string_ord (tyco1, tyco2) |
72 prod_ord fast_string_ord fast_string_ord (inst1, inst2) |
77 prod_ord fast_string_ord fast_string_ord (inst1, inst2) |
73 | symbol_ord (Class_Instance _, _) = GREATER |
78 | symbol_ord (Class_Instance _, _) = GREATER |
74 | symbol_ord (_, Class_Instance _) = LESS |
79 | symbol_ord (_, Class_Instance _) = LESS |
75 | symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2); |
80 | symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2); |
76 |
81 |
77 structure Table = Table(type key = symbol val ord = symbol_ord); |
82 structure Table = Table(type key = T val ord = symbol_ord); |
78 structure Graph = Graph(type key = symbol val ord = symbol_ord); |
83 structure Graph = Graph(type key = T val ord = symbol_ord); |
|
84 |
|
85 local |
|
86 val base = Name.desymbolize false o Long_Name.base_name; |
|
87 fun base_rel (x, y) = base y ^ "_" ^ base x; |
|
88 in |
|
89 |
|
90 fun default_base (Constant "") = "value" |
|
91 | default_base (Constant "==>") = "follows" |
|
92 | default_base (Constant "==") = "meta_eq" |
|
93 | default_base (Constant c) = base c |
|
94 | default_base (Type_Constructor tyco) = base tyco |
|
95 | default_base (Type_Class class) = base class |
|
96 | default_base (Class_Relation classrel) = base_rel classrel |
|
97 | default_base (Class_Instance inst) = base_rel inst; |
|
98 |
|
99 end; |
79 |
100 |
80 local |
101 local |
81 fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); |
102 fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); |
82 fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); |
103 fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); |
83 fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst |
104 fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst |
92 | prefix thy (Constant c) = thyname_of_const thy c |
113 | prefix thy (Constant c) = thyname_of_const thy c |
93 | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco |
114 | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco |
94 | prefix thy (Type_Class class) = thyname_of_class thy class |
115 | prefix thy (Type_Class class) = thyname_of_class thy class |
95 | prefix thy (Class_Relation (class, _)) = thyname_of_class thy class |
116 | prefix thy (Class_Relation (class, _)) = thyname_of_class thy class |
96 | prefix thy (Class_Instance inst) = thyname_of_instance thy inst; |
117 | prefix thy (Class_Instance inst) = thyname_of_instance thy inst; |
97 val base = Name.desymbolize false o Long_Name.base_name; |
|
98 fun base_rel (x, y) = base y ^ "_" ^ base x; |
|
99 in |
118 in |
100 |
119 |
101 fun base_name (Constant "") = "value" |
120 fun default_prefix ctxt = prefix (Proof_Context.theory_of ctxt); |
102 | base_name (Constant "==>") = "follows" |
121 |
103 | base_name (Constant "==") = "meta_eq" |
122 end; |
104 | base_name (Constant c) = base c |
|
105 | base_name (Type_Constructor tyco) = base tyco |
|
106 | base_name (Type_Class class) = base class |
|
107 | base_name (Class_Relation classrel) = base_rel classrel |
|
108 | base_name (Class_Instance inst) = base_rel inst; |
|
109 |
|
110 fun namespace_prefix ctxt = prefix (Proof_Context.theory_of ctxt); |
|
111 |
|
112 fun default_name ctxt sym = (namespace_prefix ctxt sym, base_name sym); |
|
113 |
123 |
114 val value = Constant ""; |
124 val value = Constant ""; |
115 fun is_value (Constant "") = true |
125 fun is_value (Constant "") = true |
116 | is_value _ = false; |
126 | is_value _ = false; |
117 |
|
118 end; |
|
119 |
127 |
120 fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) |
128 fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) |
121 | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco) |
129 | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco) |
122 | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class) |
130 | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class) |
123 | quote ctxt (Class_Relation (sub, super)) = |
131 | quote ctxt (Class_Relation (sub, super)) = |