1(* Title: Tools/Code/code_symbol.ML 2 Author: Florian Haftmann, TU Muenchen 3 4Data related to symbols in programs: constants, type constructors, classes, 5class relations, class instances, modules. 6*) 7 8signature BASIC_CODE_SYMBOL = 9sig 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 13end 14 15signature CODE_SYMBOL = 16sig 17 include BASIC_CODE_SYMBOL 18 type T = (string, string, class, class * class, string * class, string) attr 19 structure Table: TABLE 20 structure Graph: GRAPH 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 27 val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l) 28 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr 29 val maps_attr: ('a -> 'g list) -> ('b -> 'h list) 30 -> ('c -> 'i list) -> ('d -> 'j list) -> ('e -> 'k list) -> ('f -> 'l list) 31 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr list 32 val maps_attr': ('a -> ('m * 'g) list) -> ('b -> ('m * 'h) list) 33 -> ('c -> ('m * 'i) list) -> ('d -> ('m * 'j) list) -> ('e -> ('m * 'k) list) -> ('f -> ('m * 'l) list) 34 -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('m * ('g, 'h, 'i, 'j, 'k, 'l) attr) list 35 type ('a, 'b, 'c, 'd, 'e, 'f) data 36 val empty_data: ('a, 'b, 'c, 'd, 'e, 'f) data 37 val merge_data: ('a, 'b, 'c, 'd, 'e, 'f) data * ('a, 'b, 'c, 'd, 'e, 'f) data 38 -> ('a, 'b, 'c, 'd, 'e, 'f) data 39 val set_data: (string * 'a option, string * 'b option, string * 'c option, 40 (class * class) * 'd option, (string * class) * 'e option, string * 'f option) attr 41 -> ('a, 'b, 'c, 'd, 'e, 'f) data -> ('a, 'b, 'c, 'd, 'e, 'f) data 42 val lookup_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'a option 43 val lookup_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'b option 44 val lookup_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class -> 'c option 45 val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option 46 val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option 47 val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option 48 val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> T -> 'a option 49 val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> T list 50 val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list 51end; 52 53structure Code_Symbol : CODE_SYMBOL = 54struct 55 56(* data for symbols *) 57 58datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = 59 Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f; 60 61type T = (string, string, class, string * class, class * class, string) attr; 62 63fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2) 64 | symbol_ord (Constant _, _) = GREATER 65 | symbol_ord (_, Constant _) = LESS 66 | symbol_ord (Type_Constructor tyco1, Type_Constructor tyco2) = fast_string_ord (tyco1, tyco2) 67 | symbol_ord (Type_Constructor _, _) = GREATER 68 | symbol_ord (_, Type_Constructor _) = LESS 69 | symbol_ord (Type_Class class1, Type_Class class2) = fast_string_ord (class1, class2) 70 | symbol_ord (Type_Class _, _) = GREATER 71 | symbol_ord (_, Type_Class _) = LESS 72 | symbol_ord (Class_Relation classrel1, Class_Relation classrel2) = 73 prod_ord fast_string_ord fast_string_ord (classrel1, classrel2) 74 | symbol_ord (Class_Relation _, _) = GREATER 75 | symbol_ord (_, Class_Relation _) = LESS 76 | symbol_ord (Class_Instance inst1, Class_Instance inst2) = 77 prod_ord fast_string_ord fast_string_ord (inst1, inst2) 78 | symbol_ord (Class_Instance _, _) = GREATER 79 | symbol_ord (_, Class_Instance _) = LESS 80 | symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2); 81 82structure Table = Table(type key = T val ord = symbol_ord); 83structure Graph = Graph(type key = T val ord = symbol_ord); 84 85local 86 val base = Name.desymbolize NONE o Long_Name.base_name; 87 fun base_rel (x, y) = base y ^ "_" ^ base x; 88in 89 90fun default_base (Constant "") = "value" 91 | default_base (Constant c) = base c 92 | default_base (Type_Constructor tyco) = base tyco 93 | default_base (Type_Class class) = base class 94 | default_base (Class_Relation classrel) = base_rel classrel 95 | default_base (Class_Instance inst) = base_rel inst; 96 97end; 98 99local 100 val thyname_of_type = Name_Space.the_entry_theory_name o Sign.type_space; 101 val thyname_of_class = Name_Space.the_entry_theory_name o Sign.class_space; 102 fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst 103 of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst)) 104 | thyname :: _ => thyname; 105 fun thyname_of_const thy c = case Axclass.class_of_param thy c 106 of SOME class => thyname_of_class thy class 107 | NONE => (case Code.get_type_of_constr_or_abstr thy c 108 of SOME (tyco, _) => thyname_of_type thy tyco 109 | NONE => Name_Space.the_entry_theory_name (Sign.const_space thy) c); 110 fun prefix thy (Constant "") = "Code" 111 | prefix thy (Constant c) = thyname_of_const thy c 112 | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco 113 | prefix thy (Type_Class class) = thyname_of_class thy class 114 | prefix thy (Class_Relation (class, _)) = thyname_of_class thy class 115 | prefix thy (Class_Instance inst) = thyname_of_instance thy inst; 116in 117 118fun default_prefix ctxt = prefix (Proof_Context.theory_of ctxt); 119 120end; 121 122val value = Constant ""; 123fun is_value (Constant "") = true 124 | is_value _ = false; 125 126fun quote ctxt (Constant c) = 127 Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) 128 | quote ctxt (Type_Constructor tyco) = 129 "type " ^ Library.quote (Proof_Context.markup_type ctxt tyco) 130 | quote ctxt (Type_Class class) = 131 "class " ^ Library.quote (Proof_Context.markup_class ctxt class) 132 | quote ctxt (Class_Relation (sub, super)) = 133 Library.quote (Proof_Context.markup_class ctxt sub) ^ " < " ^ 134 Library.quote (Proof_Context.markup_class ctxt super) 135 | quote ctxt (Class_Instance (tyco, class)) = 136 Library.quote (Proof_Context.markup_type ctxt tyco) ^ " :: " ^ 137 Library.quote (Proof_Context.markup_class ctxt class); 138 139fun marker (Constant c) = "CONST " ^ c 140 | marker (Type_Constructor tyco) = "TYPE " ^ tyco 141 | marker (Type_Class class) = "CLASS " ^ class 142 | marker (Class_Relation (sub, super)) = "CLASSREL " ^ sub ^ " < " ^ super 143 | marker (Class_Instance (tyco, class)) = "INSTANCE " ^ tyco ^ " :: " ^ class; 144 145fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x) 146 | map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x) 147 | map_attr const tyco class classrel inst module (Type_Class x) = Type_Class (class x) 148 | map_attr const tyco class classrel inst module (Class_Relation x) = Class_Relation (classrel x) 149 | map_attr const tyco class classrel inst module (Class_Instance x) = Class_Instance (inst x) 150 | map_attr const tyco class classrel inst module (Module x) = Module (module x); 151 152fun maps_attr const tyco class classrel inst module (Constant x) = map Constant (const x) 153 | maps_attr const tyco class classrel inst module (Type_Constructor x) = map Type_Constructor (tyco x) 154 | maps_attr const tyco class classrel inst module (Type_Class x) = map Type_Class (class x) 155 | maps_attr const tyco class classrel inst module (Class_Relation x) = map Class_Relation (classrel x) 156 | maps_attr const tyco class classrel inst module (Class_Instance x) = map Class_Instance (inst x) 157 | maps_attr const tyco class classrel inst module (Module x) = map Module (module x); 158 159fun maps_attr' const tyco class classrel inst module (Constant x) = (map o apsnd) Constant (const x) 160 | maps_attr' const tyco class classrel inst module (Type_Constructor x) = (map o apsnd) Type_Constructor (tyco x) 161 | maps_attr' const tyco class classrel inst module (Type_Class x) = (map o apsnd) Type_Class (class x) 162 | maps_attr' const tyco class classrel inst module (Class_Relation x) = (map o apsnd) Class_Relation (classrel x) 163 | maps_attr' const tyco class classrel inst module (Class_Instance x) = (map o apsnd) Class_Instance (inst x) 164 | maps_attr' const tyco class classrel inst module (Module x) = (map o apsnd) Module (module x); 165 166datatype ('a, 'b, 'c, 'd, 'e, 'f) data = 167 Data of { constant: 'a Symtab.table, type_constructor: 'b Symtab.table, 168 type_class: 'c Symtab.table, class_relation: 'd Symreltab.table, class_instance: 'e Symreltab.table, 169 module: 'f Symtab.table }; 170 171fun make_data constant type_constructor type_class class_relation class_instance module = 172 Data { constant = constant, type_constructor = type_constructor, 173 type_class = type_class, class_relation = class_relation, class_instance = class_instance, module = module }; 174fun dest_data (Data x) = x; 175fun map_data map_constant map_type_constructor map_type_class map_class_relation map_class_instance map_module 176 (Data { constant, type_constructor, type_class, class_relation, class_instance, module }) = 177 Data { constant = map_constant constant, type_constructor = map_type_constructor type_constructor, 178 type_class = map_type_class type_class, class_relation = map_class_relation class_relation, 179 class_instance = map_class_instance class_instance, module = map_module module }; 180 181val empty_data = Data { constant = Symtab.empty, type_constructor = Symtab.empty, 182 type_class = Symtab.empty, class_relation = Symreltab.empty, class_instance = Symreltab.empty, module = Symtab.empty }; 183fun merge_data (Data { constant = constant1, type_constructor = type_constructor1, 184 type_class = type_class1, class_instance = class_instance1, class_relation = class_relation1, module = module1 }, 185 Data { constant = constant2, type_constructor = type_constructor2, 186 type_class = type_class2, class_instance = class_instance2, class_relation = class_relation2, module = module2 }) = 187 make_data (Symtab.join (K snd) (constant1, constant2)) 188 (Symtab.join (K snd) (type_constructor1, type_constructor2)) 189 (Symtab.join (K snd) (type_class1, type_class2)) 190 (Symreltab.join (K snd) (class_relation1, class_relation2)) 191 (Symreltab.join (K snd) (class_instance1, class_instance2)) 192 (Symtab.join (K snd) (module1, module2)); (*prefer later entries: K snd*) 193 194fun set_sym (sym, NONE) = Symtab.delete_safe sym 195 | set_sym (sym, SOME y) = Symtab.update (sym, y); 196fun set_symrel (symrel, NONE) = Symreltab.delete_safe symrel 197 | set_symrel (symrel, SOME y) = Symreltab.update (symrel, y); 198 199fun set_data (Constant x) = map_data (set_sym x) I I I I I 200 | set_data (Type_Constructor x) = map_data I (set_sym x) I I I I 201 | set_data (Type_Class x) = map_data I I (set_sym x) I I I 202 | set_data (Class_Relation x) = map_data I I I (set_symrel x) I I 203 | set_data (Class_Instance x) = map_data I I I I (set_symrel x) I 204 | set_data (Module x) = map_data I I I I I (set_sym x); 205 206fun lookup_constant_data x = (Symtab.lookup o #constant o dest_data) x; 207fun lookup_type_constructor_data x = (Symtab.lookup o #type_constructor o dest_data) x; 208fun lookup_type_class_data x = (Symtab.lookup o #type_class o dest_data) x; 209fun lookup_class_relation_data x = (Symreltab.lookup o #class_relation o dest_data) x; 210fun lookup_class_instance_data x = (Symreltab.lookup o #class_instance o dest_data) x; 211fun lookup_module_data x = (Symtab.lookup o #module o dest_data) x; 212 213fun lookup data (Constant x) = lookup_constant_data data x 214 | lookup data (Type_Constructor x) = lookup_type_constructor_data data x 215 | lookup data (Type_Class x) = lookup_type_class_data data x 216 | lookup data (Class_Relation x) = lookup_class_relation_data data x 217 | lookup data (Class_Instance x) = lookup_class_instance_data data x 218 | lookup data (Module x) = lookup_module_data data x; 219 220fun symbols_of x = (map Constant o Symtab.keys o #constant o dest_data) x 221 @ (map Type_Constructor o Symtab.keys o #type_constructor o dest_data) x 222 @ (map Type_Class o Symtab.keys o #type_class o dest_data) x 223 @ (map Class_Relation o Symreltab.keys o #class_relation o dest_data) x 224 @ (map Class_Instance o Symreltab.keys o #class_instance o dest_data) x 225 @ (map Module o Symtab.keys o #module o dest_data) x; 226 227fun dest_module_data x = (Symtab.dest o #module o dest_data) x; 228 229end; 230 231 232structure Basic_Code_Symbol: BASIC_CODE_SYMBOL = Code_Symbol; 233