--- a/src/Tools/Code/code_printer.ML Fri May 24 23:57:24 2013 +0200
+++ b/src/Tools/Code/code_printer.ML Fri May 24 23:57:24 2013 +0200
@@ -65,37 +65,6 @@
val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
- datatype ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr =
- Constant of 'a | Type_Constructor of 'b | Type_Class of 'c |
- Class_Relation of 'd | Class_Instance of 'e | Module of 'f
- val map_symbol_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l)
- -> ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr -> ('g, 'h, 'i, 'j, 'k, 'l) symbol_attr
- val maps_symbol_attr: ('a -> 'g list) -> ('b -> 'h list)
- -> ('c -> 'i list) -> ('d -> 'j list) -> ('e -> 'k list) -> ('f -> 'l list)
- -> ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr -> ('g, 'h, 'i, 'j, 'k, 'l) symbol_attr list
- val maps_symbol_attr': ('a -> ('m * 'g) list) -> ('b -> ('m * 'h) list)
- -> ('c -> ('m * 'i) list) -> ('d -> ('m * 'j) list) -> ('e -> ('m * 'k) list) -> ('f -> ('m * 'l) list)
- -> ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr -> ('m * ('g, 'h, 'i, 'j, 'k, 'l) symbol_attr) list
- type ('a, 'b, 'c, 'd, 'e, 'f) symbol_data
- val empty_symbol_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data
- val merge_symbol_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data * ('a, 'b, 'c, 'd, 'e, 'f) symbol_data
- -> ('a, 'b, 'c, 'd, 'e, 'f) symbol_data
- val lookup_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> string -> 'a option
- val lookup_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> string -> 'b option
- val lookup_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> string -> 'c option
- val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> string * string -> 'd option
- val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> string * string -> 'e option
- val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> string -> 'f option
- val dest_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> (string * 'a) list
- val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> (string * 'b) list
- val dest_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> (string * 'c) list
- val dest_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> ((string * string) * 'd) list
- val dest_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> ((string * string) * 'e) list
- val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> (string * 'f) list
- val set_symbol_data: (string * 'a option, string * 'b option, string * 'c option,
- (string * string) * 'd option, (string * string) * 'e option, string * 'f option) symbol_attr
- -> ('a, 'b, 'c, 'd, 'e, 'f) symbol_data -> ('a, 'b, 'c, 'd, 'e, 'f) symbol_data
-
type simple_const_syntax
type complex_const_syntax
type const_syntax
@@ -303,87 +272,6 @@
| tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
-(* data for symbols *)
-
-datatype ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr =
- Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f;
-
-fun map_symbol_attr const tyco class classrel inst module (Constant x) = Constant (const x)
- | map_symbol_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x)
- | map_symbol_attr const tyco class classrel inst module (Type_Class x) = Type_Class (class x)
- | map_symbol_attr const tyco class classrel inst module (Class_Relation x) = Class_Relation (classrel x)
- | map_symbol_attr const tyco class classrel inst module (Class_Instance x) = Class_Instance (inst x)
- | map_symbol_attr const tyco class classrel inst module (Module x) = Module (module x);
-
-fun maps_symbol_attr const tyco class classrel inst module (Constant x) = map Constant (const x)
- | maps_symbol_attr const tyco class classrel inst module (Type_Constructor x) = map Type_Constructor (tyco x)
- | maps_symbol_attr const tyco class classrel inst module (Type_Class x) = map Type_Class (class x)
- | maps_symbol_attr const tyco class classrel inst module (Class_Relation x) = map Class_Relation (classrel x)
- | maps_symbol_attr const tyco class classrel inst module (Class_Instance x) = map Class_Instance (inst x)
- | maps_symbol_attr const tyco class classrel inst module (Module x) = map Module (module x);
-
-fun maps_symbol_attr' const tyco class classrel inst module (Constant x) = (map o apsnd) Constant (const x)
- | maps_symbol_attr' const tyco class classrel inst module (Type_Constructor x) = (map o apsnd) Type_Constructor (tyco x)
- | maps_symbol_attr' const tyco class classrel inst module (Type_Class x) = (map o apsnd) Type_Class (class x)
- | maps_symbol_attr' const tyco class classrel inst module (Class_Relation x) = (map o apsnd) Class_Relation (classrel x)
- | maps_symbol_attr' const tyco class classrel inst module (Class_Instance x) = (map o apsnd) Class_Instance (inst x)
- | maps_symbol_attr' const tyco class classrel inst module (Module x) = (map o apsnd) Module (module x);
-
-datatype ('a, 'b, 'c, 'd, 'e, 'f) symbol_data =
- Symbol_Data of { constant: 'a Symtab.table, type_constructor: 'b Symtab.table,
- type_class: 'c Symtab.table, class_relation: 'd Symreltab.table, class_instance: 'e Symreltab.table,
- module: 'f Symtab.table };
-
-fun make_symbol_data constant type_constructor type_class class_relation class_instance module =
- Symbol_Data { constant = constant, type_constructor = type_constructor,
- type_class = type_class, class_relation = class_relation, class_instance = class_instance, module = module };
-fun dest_symbol_data (Symbol_Data x) = x;
-fun map_symbol_data map_constant map_type_constructor map_type_class map_class_relation map_class_instance map_module
- (Symbol_Data { constant, type_constructor, type_class, class_relation, class_instance, module }) =
- Symbol_Data { constant = map_constant constant, type_constructor = map_type_constructor type_constructor,
- type_class = map_type_class type_class, class_relation = map_class_relation class_relation,
- class_instance = map_class_instance class_instance, module = map_module module };
-
-val empty_symbol_data = Symbol_Data { constant = Symtab.empty, type_constructor = Symtab.empty,
- type_class = Symtab.empty, class_relation = Symreltab.empty, class_instance = Symreltab.empty, module = Symtab.empty };
-fun merge_symbol_data (Symbol_Data { constant = constant1, type_constructor = type_constructor1,
- type_class = type_class1, class_instance = class_instance1, class_relation = class_relation1, module = module1 },
- Symbol_Data { constant = constant2, type_constructor = type_constructor2,
- type_class = type_class2, class_instance = class_instance2, class_relation = class_relation2, module = module2 }) =
- make_symbol_data (Symtab.join (K snd) (constant1, constant2))
- (Symtab.join (K snd) (type_constructor1, type_constructor2))
- (Symtab.join (K snd) (type_class1, type_class2))
- (Symreltab.join (K snd) (class_relation1, class_relation2))
- (Symreltab.join (K snd) (class_instance1, class_instance2))
- (Symtab.join (K snd) (module1, module2)); (*prefer later entries: K snd*)
-
-fun lookup_constant_data x = (Symtab.lookup o #constant o dest_symbol_data) x;
-fun lookup_type_constructor_data x = (Symtab.lookup o #type_constructor o dest_symbol_data) x;
-fun lookup_type_class_data x = (Symtab.lookup o #type_class o dest_symbol_data) x;
-fun lookup_class_relation_data x = (Symreltab.lookup o #class_relation o dest_symbol_data) x;
-fun lookup_class_instance_data x = (Symreltab.lookup o #class_instance o dest_symbol_data) x;
-fun lookup_module_data x = (Symtab.lookup o #module o dest_symbol_data) x;
-
-fun dest_constant_data x = (Symtab.dest o #constant o dest_symbol_data) x;
-fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_symbol_data) x;
-fun dest_type_class_data x = (Symtab.dest o #type_class o dest_symbol_data) x;
-fun dest_class_relation_data x = (Symreltab.dest o #class_relation o dest_symbol_data) x;
-fun dest_class_instance_data x = (Symreltab.dest o #class_instance o dest_symbol_data) x;
-fun dest_module_data x = (Symtab.dest o #module o dest_symbol_data) x;
-
-fun set_sym (sym, NONE) = Symtab.delete_safe sym
- | set_sym (sym, SOME y) = Symtab.update (sym, y);
-fun set_symrel (symrel, NONE) = Symreltab.delete_safe symrel
- | set_symrel (symrel, SOME y) = Symreltab.update (symrel, y);
-
-fun set_symbol_data (Constant x) = map_symbol_data (set_sym x) I I I I I
- | set_symbol_data (Type_Constructor x) = map_symbol_data I (set_sym x) I I I I
- | set_symbol_data (Type_Class x) = map_symbol_data I I (set_sym x) I I I
- | set_symbol_data (Class_Relation x) = map_symbol_data I I I (set_symrel x) I I
- | set_symbol_data (Class_Instance x) = map_symbol_data I I I I (set_symrel x) I
- | set_symbol_data (Module x) = map_symbol_data I I I I I (set_sym x);
-
-
(* generic syntax *)
type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/code_symbol.ML Fri May 24 23:57:24 2013 +0200
@@ -0,0 +1,134 @@
+(* Title: Tools/Code/ML
+ Author: Florian Haftmann, TU Muenchen
+
+Data related to symbols in programs: constants, type constructors, classes,
+class relations, class instances, modules.
+*)
+
+signature CODE_SYMBOL =
+sig
+ 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
+ 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)
+ -> ('c -> 'i list) -> ('d -> 'j list) -> ('e -> 'k list) -> ('f -> 'l list)
+ -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr list
+ val maps_attr': ('a -> ('m * 'g) list) -> ('b -> ('m * 'h) list)
+ -> ('c -> ('m * 'i) list) -> ('d -> ('m * 'j) list) -> ('e -> ('m * 'k) list) -> ('f -> ('m * 'l) list)
+ -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('m * ('g, 'h, 'i, 'j, 'k, 'l) attr) list
+ type ('a, 'b, 'c, 'd, 'e, 'f) data
+ val empty_data: ('a, 'b, 'c, 'd, 'e, 'f) data
+ val merge_data: ('a, 'b, 'c, 'd, 'e, 'f) data * ('a, 'b, 'c, 'd, 'e, 'f) data
+ -> ('a, 'b, 'c, 'd, 'e, 'f) data
+ val lookup_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'a option
+ val lookup_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'b option
+ val lookup_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class -> 'c option
+ val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option
+ val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option
+ val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option
+ val dest_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'a) list
+ val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'b) list
+ val dest_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (class * 'c) list
+ 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 set_data: (string * 'a option, string * 'b option, string * 'c option,
+ (class * class) * 'd option, (string * class) * 'e option, string * 'f option) attr
+ -> ('a, 'b, 'c, 'd, 'e, 'f) data -> ('a, 'b, 'c, 'd, 'e, 'f) data
+ val quote_symbol: Proof.context -> (string, string, class, string * class, class * class, string) attr -> string
+end;
+
+structure Code_Symbol : CODE_SYMBOL =
+struct
+
+(* data for symbols *)
+
+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;
+
+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)
+ | map_attr const tyco class classrel inst module (Class_Relation x) = Class_Relation (classrel x)
+ | map_attr const tyco class classrel inst module (Class_Instance x) = Class_Instance (inst x)
+ | map_attr const tyco class classrel inst module (Module x) = Module (module x);
+
+fun maps_attr const tyco class classrel inst module (Constant x) = map Constant (const x)
+ | maps_attr const tyco class classrel inst module (Type_Constructor x) = map Type_Constructor (tyco x)
+ | maps_attr const tyco class classrel inst module (Type_Class x) = map Type_Class (class x)
+ | maps_attr const tyco class classrel inst module (Class_Relation x) = map Class_Relation (classrel x)
+ | maps_attr const tyco class classrel inst module (Class_Instance x) = map Class_Instance (inst x)
+ | maps_attr const tyco class classrel inst module (Module x) = map Module (module x);
+
+fun maps_attr' const tyco class classrel inst module (Constant x) = (map o apsnd) Constant (const x)
+ | maps_attr' const tyco class classrel inst module (Type_Constructor x) = (map o apsnd) Type_Constructor (tyco x)
+ | maps_attr' const tyco class classrel inst module (Type_Class x) = (map o apsnd) Type_Class (class x)
+ | maps_attr' const tyco class classrel inst module (Class_Relation x) = (map o apsnd) Class_Relation (classrel x)
+ | maps_attr' const tyco class classrel inst module (Class_Instance x) = (map o apsnd) Class_Instance (inst x)
+ | maps_attr' const tyco class classrel inst module (Module x) = (map o apsnd) Module (module x);
+
+datatype ('a, 'b, 'c, 'd, 'e, 'f) data =
+ Data of { constant: 'a Symtab.table, type_constructor: 'b Symtab.table,
+ type_class: 'c Symtab.table, class_relation: 'd Symreltab.table, class_instance: 'e Symreltab.table,
+ module: 'f Symtab.table };
+
+fun make_data constant type_constructor type_class class_relation class_instance module =
+ Data { constant = constant, type_constructor = type_constructor,
+ type_class = type_class, class_relation = class_relation, class_instance = class_instance, module = module };
+fun dest_data (Data x) = x;
+fun map_data map_constant map_type_constructor map_type_class map_class_relation map_class_instance map_module
+ (Data { constant, type_constructor, type_class, class_relation, class_instance, module }) =
+ Data { constant = map_constant constant, type_constructor = map_type_constructor type_constructor,
+ type_class = map_type_class type_class, class_relation = map_class_relation class_relation,
+ class_instance = map_class_instance class_instance, module = map_module module };
+
+val empty_data = Data { constant = Symtab.empty, type_constructor = Symtab.empty,
+ type_class = Symtab.empty, class_relation = Symreltab.empty, class_instance = Symreltab.empty, module = Symtab.empty };
+fun merge_data (Data { constant = constant1, type_constructor = type_constructor1,
+ type_class = type_class1, class_instance = class_instance1, class_relation = class_relation1, module = module1 },
+ Data { constant = constant2, type_constructor = type_constructor2,
+ type_class = type_class2, class_instance = class_instance2, class_relation = class_relation2, module = module2 }) =
+ make_data (Symtab.join (K snd) (constant1, constant2))
+ (Symtab.join (K snd) (type_constructor1, type_constructor2))
+ (Symtab.join (K snd) (type_class1, type_class2))
+ (Symreltab.join (K snd) (class_relation1, class_relation2))
+ (Symreltab.join (K snd) (class_instance1, class_instance2))
+ (Symtab.join (K snd) (module1, module2)); (*prefer later entries: K snd*)
+
+fun lookup_constant_data x = (Symtab.lookup o #constant o dest_data) x;
+fun lookup_type_constructor_data x = (Symtab.lookup o #type_constructor o dest_data) x;
+fun lookup_type_class_data x = (Symtab.lookup o #type_class o dest_data) x;
+fun lookup_class_relation_data x = (Symreltab.lookup o #class_relation o dest_data) x;
+fun lookup_class_instance_data x = (Symreltab.lookup o #class_instance o dest_data) x;
+fun lookup_module_data x = (Symtab.lookup o #module o dest_data) x;
+
+fun dest_constant_data x = (Symtab.dest o #constant o dest_data) x;
+fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_data) x;
+fun dest_type_class_data x = (Symtab.dest o #type_class o dest_data) x;
+fun dest_class_relation_data x = (Symreltab.dest o #class_relation o dest_data) x;
+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 set_sym (sym, NONE) = Symtab.delete_safe sym
+ | set_sym (sym, SOME y) = Symtab.update (sym, y);
+fun set_symrel (symrel, NONE) = Symreltab.delete_safe symrel
+ | set_symrel (symrel, SOME y) = Symreltab.update (symrel, y);
+
+fun set_data (Constant x) = map_data (set_sym x) I I I I I
+ | set_data (Type_Constructor x) = map_data I (set_sym x) I I I I
+ | set_data (Type_Class x) = map_data I I (set_sym x) I I I
+ | set_data (Class_Relation x) = map_data I I I (set_symrel x) I I
+ | set_data (Class_Instance x) = map_data I I I I (set_symrel x) I
+ | set_data (Module x) = map_data I I I I I (set_sym 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;
--- a/src/Tools/Code_Generator.thy Fri May 24 23:57:24 2013 +0200
+++ b/src/Tools/Code_Generator.thy Fri May 24 23:57:24 2013 +0200
@@ -17,6 +17,7 @@
ML_file "~~/src/Tools/value.ML"
ML_file "~~/src/Tools/cache_io.ML"
ML_file "~~/src/Tools/Code/code_preproc.ML"
+ML_file "~~/src/Tools/Code/code_symbol.ML"
ML_file "~~/src/Tools/Code/code_thingol.ML"
ML_file "~~/src/Tools/Code/code_simp.ML"
ML_file "~~/src/Tools/Code/code_printer.ML"