# HG changeset patch # User haftmann # Date 1388997081 -3600 # Node ID 45624a38109f436930235652f3558cb4b39dbab3 # Parent 409de8cf33b2b8cb9de3ff8c16f6561f920de20b order and graph for code symbols diff -r 409de8cf33b2 -r 45624a38109f src/Tools/Code/code_symbol.ML --- a/src/Tools/Code/code_symbol.ML Mon Jan 06 09:31:19 2014 +0100 +++ b/src/Tools/Code/code_symbol.ML Mon Jan 06 09:31:21 2014 +0100 @@ -10,7 +10,11 @@ datatype ('a, 'b, 'c, 'd, 'e, 'f) attr = Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f - type symbol = (string, string, class, string * class, class * class, string) attr + type symbol = (string, string, class, class * class, string * class, string) attr + structure Graph: GRAPH; + val plain_name: Proof.context -> symbol -> string + val tyco_fun: string + val quote_symbol: Proof.context -> symbol -> string val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l) -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr val maps_attr: ('a -> 'g list) -> ('b -> 'h list) @@ -39,7 +43,6 @@ val dest_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((class * class) * 'd) list val dest_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> ((string * class) * 'e) list val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list - val quote_symbol: Proof.context -> symbol -> string end; structure Code_Symbol : CODE_SYMBOL = @@ -52,6 +55,73 @@ type symbol = (string, string, class, string * class, class * class, string) attr; +fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2) + | symbol_ord (Constant _, _) = GREATER + | symbol_ord (_, Constant _) = LESS + | symbol_ord (Type_Constructor tyco1, Type_Constructor tyco2) = fast_string_ord (tyco1, tyco2) + | symbol_ord (Type_Constructor _, _) = GREATER + | symbol_ord (_, Type_Constructor _) = LESS + | symbol_ord (Type_Class class1, Type_Class class2) = fast_string_ord (class1, class2) + | symbol_ord (Type_Class _, _) = GREATER + | symbol_ord (_, Type_Class _) = LESS + | symbol_ord (Class_Relation classrel1, Class_Relation classrel2) = + prod_ord fast_string_ord fast_string_ord (classrel1, classrel2) + | symbol_ord (Class_Relation _, _) = GREATER + | symbol_ord (_, Class_Relation _) = LESS + | symbol_ord (Class_Instance inst1, Class_Instance inst2) = + prod_ord fast_string_ord fast_string_ord (inst1, inst2) + | symbol_ord (Class_Instance _, _) = GREATER + | symbol_ord (_, Class_Instance _) = LESS + | symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2); + +structure Graph = Graph(type key = symbol val ord = symbol_ord); + +local + fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); + fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); + fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst + of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst)) + | thyname :: _ => thyname; + fun thyname_of_const thy c = case Axclass.class_of_param thy c + of SOME class => thyname_of_class thy class + | NONE => (case Code.get_type_of_constr_or_abstr thy c + of SOME (tyco, _) => thyname_of_type thy tyco + | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c)); + fun base_rel (x, y) = Long_Name.base_name y ^ "_" ^ Long_Name.base_name x; + fun plainify ctxt get_prefix get_basename thing = + Long_Name.append (get_prefix (Proof_Context.theory_of ctxt) thing) + (Name.desymbolize false (get_basename thing)); +in + +fun plain_name ctxt (Constant "==>") = + plainify ctxt thyname_of_const (K "follows") "==>" + | plain_name ctxt (Constant "==") = + plainify ctxt thyname_of_const (K "meta_eq") "==" + | plain_name ctxt (Constant c) = + plainify ctxt thyname_of_const Long_Name.base_name c + | plain_name ctxt (Type_Constructor "fun") = + plainify ctxt thyname_of_type (K "fun") "fun" + | plain_name ctxt (Type_Constructor tyco) = + plainify ctxt thyname_of_type Long_Name.base_name tyco + | plain_name ctxt (Type_Class class) = + plainify ctxt thyname_of_class Long_Name.base_name class + | plain_name ctxt (Class_Relation classrel) = + plainify ctxt (fn thy => fn (class, _) => thyname_of_class thy class) base_rel classrel + | plain_name ctxt (Class_Instance inst) = + plainify ctxt thyname_of_instance base_rel inst; + +val tyco_fun = plain_name @{context} (Type_Constructor "fun"); + +end; + +fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) + | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco) + | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class) + | quote_symbol ctxt (Class_Relation (sub, super)) = + quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super) + | quote_symbol ctxt (Class_Instance (tyco, class)) = + quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ quote (Proof_Context.extern_class ctxt class); + fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x) | map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x) | map_attr const tyco class classrel inst module (Type_Class x) = Type_Class (class x) @@ -134,12 +204,4 @@ fun dest_class_instance_data x = (Symreltab.dest o #class_instance o dest_data) x; fun dest_module_data x = (Symtab.dest o #module o dest_data) x; -fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) - | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco) - | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class) - | quote_symbol ctxt (Class_Relation (sub, super)) = - quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super) - | quote_symbol ctxt (Class_Instance (tyco, class)) = - quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ quote (Proof_Context.extern_class ctxt class); - end;