--- a/src/Tools/Code/code_target.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/Tools/Code/code_target.ML Tue Aug 31 13:29:38 2010 +0200
@@ -45,10 +45,10 @@
val allow_abort: string -> theory -> theory
type tyco_syntax = Code_Printer.tyco_syntax
type const_syntax = Code_Printer.const_syntax
- val add_syntax_class: string -> class -> string option -> theory -> theory
- val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
- val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
- val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
+ val add_class_syntax: string -> class -> string option -> theory -> theory
+ val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
+ val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
+ val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
val add_reserved: string -> string -> theory -> theory
val add_include: string -> string * (string * string list) option -> theory -> theory
end;
@@ -63,7 +63,7 @@
type const_syntax = Code_Printer.const_syntax;
-(** basics **)
+(** abstract nonsense **)
datatype destination = File of Path.T option | String of string list;
type serialization = destination -> (string * string option list) option;
@@ -80,21 +80,21 @@
(** theory data **)
-datatype name_syntax_table = NameSyntaxTable of {
+datatype symbol_syntax_data = Symbol_Syntax_Data of {
class: string Symtab.table,
instance: unit Symreltab.table,
tyco: Code_Printer.tyco_syntax Symtab.table,
const: Code_Printer.const_syntax Symtab.table
};
-fun mk_name_syntax_table ((class, instance), (tyco, const)) =
- NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
-fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
- mk_name_syntax_table (f ((class, instance), (tyco, const)));
-fun merge_name_syntax_table
- (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
- NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
- mk_name_syntax_table (
+fun make_symbol_syntax_data ((class, instance), (tyco, const)) =
+ Symbol_Syntax_Data { class = class, instance = instance, tyco = tyco, const = const };
+fun map_symbol_syntax_data f (Symbol_Syntax_Data { class, instance, tyco, const }) =
+ make_symbol_syntax_data (f ((class, instance), (tyco, const)));
+fun merge_symbol_syntax_data
+ (Symbol_Syntax_Data { class = class1, instance = instance1, tyco = tyco1, const = const1 },
+ Symbol_Syntax_Data { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
+ make_symbol_syntax_data (
(Symtab.join (K snd) (class1, class2),
Symreltab.join (K snd) (instance1, instance2)),
(Symtab.join (K snd) (tyco1, tyco2),
@@ -128,25 +128,25 @@
description: description,
reserved: string list,
includes: (Pretty.T * string list) Symtab.table,
- name_syntax_table: name_syntax_table,
+ symbol_syntax_data: symbol_syntax_data,
module_alias: string Symtab.table
};
-fun make_target ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))) =
+fun make_target ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))) =
Target { serial = serial, description = description, reserved = reserved,
- includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
-fun map_target f ( Target { serial, description, reserved, includes, name_syntax_table, module_alias } ) =
- make_target (f ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))));
+ includes = includes, symbol_syntax_data = symbol_syntax_data, module_alias = module_alias };
+fun map_target f ( Target { serial, description, reserved, includes, symbol_syntax_data, module_alias } ) =
+ make_target (f ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))));
fun merge_target strict target (Target { serial = serial1, description = description,
reserved = reserved1, includes = includes1,
- name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
+ symbol_syntax_data = symbol_syntax_data1, module_alias = module_alias1 },
Target { serial = serial2, description = _,
reserved = reserved2, includes = includes2,
- name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
+ symbol_syntax_data = symbol_syntax_data2, module_alias = module_alias2 }) =
if serial1 = serial2 orelse not strict then
make_target ((serial1, description),
((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
- (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
+ (merge_symbol_syntax_data (symbol_syntax_data1, symbol_syntax_data2),
Symtab.join (K snd) (module_alias1, module_alias2))
))
else
@@ -155,7 +155,7 @@
fun the_description (Target { description, ... }) = description;
fun the_reserved (Target { reserved, ... }) = reserved;
fun the_includes (Target { includes, ... }) = includes;
-fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
+fun the_symbol_syntax_data (Target { symbol_syntax_data = Symbol_Syntax_Data x, ... }) = x;
fun the_module_alias (Target { module_alias , ... }) = module_alias;
structure Targets = Theory_Data
@@ -194,7 +194,7 @@
thy
|> (Targets.map o apfst o apfst o Symtab.update)
(target, make_target ((serial (), seri), (([], Symtab.empty),
- (mk_name_syntax_table ((Symtab.empty, Symreltab.empty),
+ (make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
(Symtab.empty, Symtab.empty)), Symtab.empty))))
end;
@@ -215,7 +215,7 @@
fun map_includes target =
map_target_data target o apsnd o apfst o apsnd;
fun map_name_syntax target =
- map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
+ map_target_data target o apsnd o apsnd o apfst o map_symbol_syntax_data;
fun map_module_alias target =
map_target_data target o apsnd o apsnd o apsnd;
@@ -315,7 +315,7 @@
fun includes names_all = map_filter (select_include names_all)
((Symtab.dest o the_includes) data);
val module_alias = the_module_alias data
- val { class, instance, tyco, const } = the_name_syntax data;
+ val { class, instance, tyco, const } = the_symbol_syntax_data data;
val literals = the_literals thy target;
val width = the_default default_width some_width;
in
@@ -437,19 +437,19 @@
| NONE => del x;
in (map_name_syntax target o mapp) change thy end;
-fun gen_add_syntax_class prep_class =
+fun gen_add_class_syntax prep_class =
gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);
-fun gen_add_syntax_inst prep_inst =
+fun gen_add_instance_syntax prep_inst =
gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst ((K o K) I);
-fun gen_add_syntax_tyco prep_tyco =
+fun gen_add_tyco_syntax prep_tyco =
gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco
(fn thy => fn tyco => fn syn => if fst syn <> Sign.arity_number thy tyco
then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
else syn);
-fun gen_add_syntax_const prep_const =
+fun gen_add_const_syntax prep_const =
gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
(fn thy => fn c => fn syn =>
if Code_Printer.requires_args syn > Code.args_number thy c
@@ -513,18 +513,18 @@
in
-val add_syntax_class = gen_add_syntax_class cert_class;
-val add_syntax_inst = gen_add_syntax_inst cert_inst;
-val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
-val add_syntax_const = gen_add_syntax_const (K I);
+val add_class_syntax = gen_add_class_syntax cert_class;
+val add_instance_syntax = gen_add_instance_syntax cert_inst;
+val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
+val add_const_syntax = gen_add_const_syntax (K I);
val allow_abort = gen_allow_abort (K I);
val add_reserved = add_reserved;
val add_include = add_include;
-val add_syntax_class_cmd = gen_add_syntax_class read_class;
-val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
-val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
+val add_class_syntax_cmd = gen_add_class_syntax read_class;
+val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
+val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
+val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
val allow_abort_cmd = gen_allow_abort Code.read_const;
fun parse_args f args =
@@ -554,23 +554,23 @@
val _ =
Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
process_multi_syntax Parse.xname (Scan.option Parse.string)
- add_syntax_class_cmd);
+ add_class_syntax_cmd);
val _ =
Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
(Scan.option (Parse.minus >> K ()))
- add_syntax_inst_cmd);
+ add_instance_syntax_cmd);
val _ =
Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
- add_syntax_tyco_cmd);
+ add_tyco_syntax_cmd);
val _ =
Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
- add_syntax_const_cmd);
+ add_const_syntax_cmd);
val _ =
Outer_Syntax.command "code_reserved" "declare words as reserved for target language"