src/Tools/Code/code_symbol.ML
changeset 55150 0940309ed8f1
parent 55149 626d8f08d479
child 55304 55ac31bc08a4
     1.1 --- a/src/Tools/Code/code_symbol.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_symbol.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -5,20 +5,25 @@
     1.4  class relations, class instances, modules.
     1.5  *)
     1.6  
     1.7 -signature CODE_SYMBOL =
     1.8 +signature BASIC_CODE_SYMBOL =
     1.9  sig
    1.10    datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
    1.11      Constant of 'a | Type_Constructor of 'b | Type_Class of 'c |
    1.12      Class_Relation of 'd  | Class_Instance of 'e | Module of 'f
    1.13 -  type symbol = (string, string, class, class * class, string * class, string) attr
    1.14 -  structure Table: TABLE;
    1.15 -  structure Graph: GRAPH;
    1.16 -  val namespace_prefix: Proof.context -> symbol -> string
    1.17 -  val base_name: symbol -> string
    1.18 -  val quote: Proof.context -> symbol -> string
    1.19 -  val marker: symbol -> string
    1.20 -  val value: symbol
    1.21 -  val is_value: symbol -> bool
    1.22 +end
    1.23 +
    1.24 +signature CODE_SYMBOL =
    1.25 +sig
    1.26 +  include BASIC_CODE_SYMBOL
    1.27 +  type T = (string, string, class, class * class, string * class, string) attr
    1.28 +  structure Table: TABLE
    1.29 +  structure Graph: GRAPH
    1.30 +  val default_base: T -> string
    1.31 +  val default_prefix: Proof.context -> T -> string
    1.32 +  val quote: Proof.context -> T -> string
    1.33 +  val marker: T -> string
    1.34 +  val value: T
    1.35 +  val is_value: T -> bool
    1.36    val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l)
    1.37      -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr
    1.38    val maps_attr: ('a -> 'g list) -> ('b -> 'h list)
    1.39 @@ -40,8 +45,8 @@
    1.40    val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option
    1.41    val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option
    1.42    val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option
    1.43 -  val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option
    1.44 -  val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> symbol list
    1.45 +  val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> T -> 'a option
    1.46 +  val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> T list
    1.47    val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list
    1.48  end;
    1.49  
    1.50 @@ -53,7 +58,7 @@
    1.51  datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
    1.52    Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd  | Class_Instance of 'e | Module of 'f;
    1.53  
    1.54 -type symbol = (string, string, class, string * class, class * class, string) attr;
    1.55 +type T = (string, string, class, string * class, class * class, string) attr;
    1.56  
    1.57  fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2)
    1.58    | symbol_ord (Constant _, _) = GREATER
    1.59 @@ -74,8 +79,24 @@
    1.60    | symbol_ord (_, Class_Instance _) = LESS
    1.61    | symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2);
    1.62  
    1.63 -structure Table = Table(type key = symbol val ord = symbol_ord);
    1.64 -structure Graph = Graph(type key = symbol val ord = symbol_ord);
    1.65 +structure Table = Table(type key = T val ord = symbol_ord);
    1.66 +structure Graph = Graph(type key = T val ord = symbol_ord);
    1.67 +
    1.68 +local
    1.69 +  val base = Name.desymbolize false o Long_Name.base_name;
    1.70 +  fun base_rel (x, y) = base y ^ "_" ^ base x;
    1.71 +in
    1.72 +
    1.73 +fun default_base (Constant "") = "value"
    1.74 +  | default_base (Constant "==>") = "follows"
    1.75 +  | default_base (Constant "==") = "meta_eq"
    1.76 +  | default_base (Constant c) = base c
    1.77 +  | default_base (Type_Constructor tyco) = base tyco
    1.78 +  | default_base (Type_Class class) = base class
    1.79 +  | default_base (Class_Relation classrel) = base_rel classrel
    1.80 +  | default_base (Class_Instance inst) = base_rel inst;
    1.81 +
    1.82 +end;
    1.83  
    1.84  local
    1.85    fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
    1.86 @@ -94,29 +115,16 @@
    1.87      | prefix thy (Type_Class class) = thyname_of_class thy class
    1.88      | prefix thy (Class_Relation (class, _)) = thyname_of_class thy class
    1.89      | prefix thy (Class_Instance inst) = thyname_of_instance thy inst;
    1.90 -  val base = Name.desymbolize false o Long_Name.base_name;
    1.91 -  fun base_rel (x, y) = base y ^ "_" ^ base x;
    1.92  in
    1.93  
    1.94 -fun base_name (Constant "") = "value"
    1.95 -  | base_name (Constant "==>") = "follows"
    1.96 -  | base_name (Constant "==") = "meta_eq"
    1.97 -  | base_name (Constant c) = base c
    1.98 -  | base_name (Type_Constructor tyco) = base tyco
    1.99 -  | base_name (Type_Class class) = base class
   1.100 -  | base_name (Class_Relation classrel) = base_rel classrel
   1.101 -  | base_name (Class_Instance inst) = base_rel inst;
   1.102 +fun default_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
   1.103  
   1.104 -fun namespace_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
   1.105 -
   1.106 -fun default_name ctxt sym = (namespace_prefix ctxt sym, base_name sym);
   1.107 +end;
   1.108  
   1.109  val value = Constant "";
   1.110  fun is_value (Constant "") = true
   1.111    | is_value _ = false;
   1.112  
   1.113 -end;
   1.114 -
   1.115  fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
   1.116    | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco)
   1.117    | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class)
   1.118 @@ -216,3 +224,6 @@
   1.119  fun dest_module_data x = (Symtab.dest o #module o dest_data) x;
   1.120  
   1.121  end;
   1.122 +
   1.123 +
   1.124 +structure Basic_Code_Symbol: BASIC_CODE_SYMBOL = Code_Symbol;