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