order and graph for code symbols
authorhaftmann
Mon Jan 06 09:31:21 2014 +0100 (2014-01-06 ago)
changeset 5493345624a38109f
parent 54932 409de8cf33b2
child 54934 4587de627cd8
child 54935 a7704d87f30a
order and graph for code symbols
src/Tools/Code/code_symbol.ML
     1.1 --- a/src/Tools/Code/code_symbol.ML	Mon Jan 06 09:31:19 2014 +0100
     1.2 +++ b/src/Tools/Code/code_symbol.ML	Mon Jan 06 09:31:21 2014 +0100
     1.3 @@ -10,7 +10,11 @@
     1.4    datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
     1.5      Constant of 'a | Type_Constructor of 'b | Type_Class of 'c |
     1.6      Class_Relation of 'd  | Class_Instance of 'e | Module of 'f
     1.7 -  type symbol = (string, string, class, string * class, class * class, string) attr
     1.8 +  type symbol = (string, string, class, class * class, string * class, string) attr
     1.9 +  structure Graph: GRAPH;
    1.10 +  val plain_name: Proof.context -> symbol -> string
    1.11 +  val tyco_fun: string
    1.12 +  val quote_symbol: Proof.context -> symbol -> string
    1.13    val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l)
    1.14      -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr
    1.15    val maps_attr: ('a -> 'g list) -> ('b -> 'h list)
    1.16 @@ -39,7 +43,6 @@
    1.17    val dest_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((class * class) * 'd) list
    1.18    val dest_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((string * class) * 'e) list
    1.19    val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list
    1.20 -  val quote_symbol: Proof.context -> symbol -> string
    1.21  end;
    1.22  
    1.23  structure Code_Symbol : CODE_SYMBOL =
    1.24 @@ -52,6 +55,73 @@
    1.25  
    1.26  type symbol = (string, string, class, string * class, class * class, string) attr;
    1.27  
    1.28 +fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2)
    1.29 +  | symbol_ord (Constant _, _) = GREATER
    1.30 +  | symbol_ord (_, Constant _) = LESS
    1.31 +  | symbol_ord (Type_Constructor tyco1, Type_Constructor tyco2) = fast_string_ord (tyco1, tyco2)
    1.32 +  | symbol_ord (Type_Constructor _, _) = GREATER
    1.33 +  | symbol_ord (_, Type_Constructor _) = LESS
    1.34 +  | symbol_ord (Type_Class class1, Type_Class class2) = fast_string_ord (class1, class2)
    1.35 +  | symbol_ord (Type_Class _, _) = GREATER
    1.36 +  | symbol_ord (_, Type_Class _) = LESS
    1.37 +  | symbol_ord (Class_Relation classrel1, Class_Relation classrel2) =
    1.38 +      prod_ord fast_string_ord fast_string_ord (classrel1, classrel2)
    1.39 +  | symbol_ord (Class_Relation _, _) = GREATER
    1.40 +  | symbol_ord (_, Class_Relation _) = LESS
    1.41 +  | symbol_ord (Class_Instance inst1, Class_Instance inst2) =
    1.42 +      prod_ord fast_string_ord fast_string_ord (inst1, inst2)
    1.43 +  | symbol_ord (Class_Instance _, _) = GREATER
    1.44 +  | symbol_ord (_, Class_Instance _) = LESS
    1.45 +  | symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2);
    1.46 +
    1.47 +structure Graph = Graph(type key = symbol val ord = symbol_ord);
    1.48 +
    1.49 +local
    1.50 +  fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
    1.51 +  fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
    1.52 +  fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst
    1.53 +   of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^  snd inst))
    1.54 +    | thyname :: _ => thyname;
    1.55 +  fun thyname_of_const thy c = case Axclass.class_of_param thy c
    1.56 +   of SOME class => thyname_of_class thy class
    1.57 +    | NONE => (case Code.get_type_of_constr_or_abstr thy c
    1.58 +       of SOME (tyco, _) => thyname_of_type thy tyco
    1.59 +        | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
    1.60 +  fun base_rel (x, y) = Long_Name.base_name y ^ "_" ^ Long_Name.base_name x;
    1.61 +  fun plainify ctxt get_prefix get_basename thing =
    1.62 +    Long_Name.append (get_prefix (Proof_Context.theory_of ctxt) thing)
    1.63 +      (Name.desymbolize false (get_basename thing));
    1.64 +in
    1.65 +
    1.66 +fun plain_name ctxt (Constant "==>") =
    1.67 +      plainify ctxt thyname_of_const (K "follows") "==>"
    1.68 +  | plain_name ctxt (Constant "==") =
    1.69 +      plainify ctxt thyname_of_const (K "meta_eq") "=="
    1.70 +  | plain_name ctxt (Constant c) =
    1.71 +      plainify ctxt thyname_of_const Long_Name.base_name c
    1.72 +  | plain_name ctxt (Type_Constructor "fun") =
    1.73 +      plainify ctxt thyname_of_type (K "fun") "fun"
    1.74 +  | plain_name ctxt (Type_Constructor tyco) =
    1.75 +      plainify ctxt thyname_of_type Long_Name.base_name tyco
    1.76 +  | plain_name ctxt (Type_Class class) =
    1.77 +      plainify ctxt thyname_of_class Long_Name.base_name class
    1.78 +  | plain_name ctxt (Class_Relation classrel) =
    1.79 +      plainify ctxt (fn thy => fn (class, _) => thyname_of_class thy class) base_rel classrel
    1.80 +  | plain_name ctxt (Class_Instance inst) =
    1.81 +      plainify ctxt thyname_of_instance base_rel inst;
    1.82 +
    1.83 +val tyco_fun = plain_name @{context} (Type_Constructor "fun");
    1.84 +
    1.85 +end;
    1.86 +
    1.87 +fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
    1.88 +  | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco)
    1.89 +  | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class)
    1.90 +  | quote_symbol ctxt (Class_Relation (sub, super)) =
    1.91 +      quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super)
    1.92 +  | quote_symbol ctxt (Class_Instance (tyco, class)) =
    1.93 +      quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ quote (Proof_Context.extern_class ctxt class);
    1.94 +
    1.95  fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x)
    1.96    | map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x)
    1.97    | map_attr const tyco class classrel inst module (Type_Class x) = Type_Class (class x)
    1.98 @@ -134,12 +204,4 @@
    1.99  fun dest_class_instance_data x = (Symreltab.dest o #class_instance o dest_data) x;
   1.100  fun dest_module_data x = (Symtab.dest o #module o dest_data) x;
   1.101  
   1.102 -fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
   1.103 -  | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco)
   1.104 -  | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class)
   1.105 -  | quote_symbol ctxt (Class_Relation (sub, super)) =
   1.106 -      quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super)
   1.107 -  | quote_symbol ctxt (Class_Instance (tyco, class)) =
   1.108 -      quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ quote (Proof_Context.extern_class ctxt class);
   1.109 -
   1.110  end;