src/Tools/Code/code_symbol.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 56826 ba18bd41e510
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      Tools/Code/code_symbol.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 BASIC_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
    13 end
    14 
    15 signature CODE_SYMBOL =
    16 sig
    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
    51 end;
    52 
    53 structure Code_Symbol : CODE_SYMBOL =
    54 struct
    55 
    56 (* data for symbols *)
    57 
    58 datatype ('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 
    61 type T = (string, string, class, string * class, class * class, string) attr;
    62 
    63 fun 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 
    82 structure Table = Table(type key = T val ord = symbol_ord);
    83 structure Graph = Graph(type key = T val ord = symbol_ord);
    84 
    85 local
    86   val base = Name.desymbolize NONE 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 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 
    97 end;
    98 
    99 local
   100   fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
   101   fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
   102   fun thyname_of_instance thy inst = case Axclass.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 => #theory_name (Name_Space.the_entry (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;
   116 in
   117 
   118 fun default_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
   119 
   120 end;
   121 
   122 val value = Constant "";
   123 fun is_value (Constant "") = true
   124   | is_value _ = false;
   125 
   126 fun 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 
   139 fun 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 
   145 fun 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 
   152 fun 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 
   159 fun 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 
   166 datatype ('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 
   171 fun 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 };
   174 fun dest_data (Data x) = x;
   175 fun 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 
   181 val 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 };
   183 fun 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 
   194 fun set_sym (sym, NONE) = Symtab.delete_safe sym
   195   | set_sym (sym, SOME y) = Symtab.update (sym, y);
   196 fun set_symrel (symrel, NONE) = Symreltab.delete_safe symrel
   197   | set_symrel (symrel, SOME y) = Symreltab.update (symrel, y);
   198 
   199 fun 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 
   206 fun lookup_constant_data x = (Symtab.lookup o #constant o dest_data) x;
   207 fun lookup_type_constructor_data x = (Symtab.lookup o #type_constructor o dest_data) x;
   208 fun lookup_type_class_data x = (Symtab.lookup o #type_class o dest_data) x;
   209 fun lookup_class_relation_data x = (Symreltab.lookup o #class_relation o dest_data) x;
   210 fun lookup_class_instance_data x = (Symreltab.lookup o #class_instance o dest_data) x;
   211 fun lookup_module_data x = (Symtab.lookup o #module o dest_data) x;
   212 
   213 fun 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 
   220 fun 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 
   227 fun dest_module_data x = (Symtab.dest o #module o dest_data) x;
   228 
   229 end;
   230 
   231 
   232 structure Basic_Code_Symbol: BASIC_CODE_SYMBOL = Code_Symbol;