--- a/src/Tools/Code/code_ml.ML Wed Jul 14 14:53:44 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Wed Jul 14 14:53:44 2010 +0200
@@ -948,8 +948,8 @@
(** for instrumentalization **)
fun evaluation_code_of thy target struct_name =
- Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
- serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
+ Code_Target.serialize_custom thy (target, fn _ => fn [] =>
+ serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
(** formal checking of compiled code **)
@@ -965,19 +965,21 @@
(** Isar setup **)
-fun isar_seri_sml module_name =
+fun isar_serializer_sml module_name =
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
>> (fn with_signatures => serialize_ml target_SML
print_sml_module print_sml_stmt module_name with_signatures));
-fun isar_seri_ocaml module_name =
+fun isar_serializer_ocaml module_name =
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
>> (fn with_signatures => serialize_ml target_OCaml
print_ocaml_module print_ocaml_stmt module_name with_signatures));
val setup =
- Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
- #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
+ Code_Target.add_target
+ (target_SML, { serializer = isar_serializer_sml, literals = literals_sml, check = () })
+ #> Code_Target.add_target
+ (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml, check = () })
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
--- a/src/Tools/Code/code_target.ML Wed Jul 14 14:53:44 2010 +0200
+++ b/src/Tools/Code/code_target.ML Wed Jul 14 14:53:44 2010 +0200
@@ -11,7 +11,8 @@
type serializer
type literals = Code_Printer.literals
- val add_target: string * (serializer * literals) -> theory -> theory
+ val add_target: string * { serializer: serializer, literals: literals, check: unit }
+ -> theory -> theory
val extend_target: string *
(string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
-> theory -> theory
@@ -26,7 +27,7 @@
-> 'a -> serialization
val serialize: theory -> string -> int option -> string option -> Token.T list
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
- val serialize_custom: theory -> string * (serializer * literals)
+ val serialize_custom: theory -> string * serializer
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
val the_literals: theory -> string -> literals
val export: serialization -> unit
@@ -114,39 +115,39 @@
-> string list (*selected statements*)
-> serialization;
-datatype serializer_entry = Serializer of serializer * Code_Printer.literals
- | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
+datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, check: unit }
+ | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
datatype target = Target of {
serial: serial,
- serializer: serializer_entry,
+ description: description,
reserved: string list,
includes: (Pretty.T * string list) Symtab.table,
name_syntax_table: name_syntax_table,
module_alias: string Symtab.table
};
-fun make_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
- Target { serial = serial, serializer = serializer, reserved = reserved,
+fun make_target ((serial, description), ((reserved, includes), (name_syntax_table, 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, serializer, reserved, includes, name_syntax_table, module_alias } ) =
- make_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
-fun merge_target strict target (Target { serial = serial1, serializer = serializer,
+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))));
+fun merge_target strict target (Target { serial = serial1, description = description,
reserved = reserved1, includes = includes1,
name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
- Target { serial = serial2, serializer = _,
+ Target { serial = serial2, description = _,
reserved = reserved2, includes = includes2,
name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
if serial1 = serial2 orelse not strict then
- make_target ((serial1, serializer),
+ make_target ((serial1, description),
((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
(merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
Symtab.join (K fst) (module_alias1, module_alias2))
))
else
- error ("Incompatible serializers: " ^ quote target);
+ error ("Incompatible targets: " ^ quote target);
-fun the_serializer (Target { serializer, ... }) = serializer;
+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;
@@ -172,14 +173,14 @@
let
val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
val _ = case seri
- of Extends (super, _) => if is_some (lookup_target super) then ()
+ of Extension (super, _) => if is_some (lookup_target super) then ()
else error ("Unknown code target language: " ^ quote super)
| _ => ();
- val overwriting = case (Option.map the_serializer o lookup_target) target
+ val overwriting = case (Option.map the_description o lookup_target) target
of NONE => false
- | SOME (Extends _) => true
- | SOME (Serializer _) => (case seri
- of Extends _ => error ("Will not overwrite existing target " ^ quote target)
+ | SOME (Extension _) => true
+ | SOME (Fundamental _) => (case seri
+ of Extension _ => error ("Will not overwrite existing target " ^ quote target)
| _ => true);
val _ = if overwriting
then warning ("Overwriting existing target " ^ quote target)
@@ -192,9 +193,9 @@
Symtab.empty))))
end;
-fun add_target (target, seri) = put_target (target, Serializer seri);
+fun add_target (target, seri) = put_target (target, Fundamental seri);
fun extend_target (target, (super, modify)) =
- put_target (target, Extends (super, modify));
+ put_target (target, Extension (super, modify));
fun map_target_data target f thy =
let
@@ -224,9 +225,9 @@
let
val ((targets, _), _) = Targets.get thy;
fun literals target = case Symtab.lookup targets target
- of SOME data => (case the_serializer data
- of Serializer (_, literals) => literals
- | Extends (super, _) => literals super)
+ of SOME data => (case the_description data
+ of Fundamental { literals, ... } => literals
+ | Extension (super, _) => literals super)
| NONE => error ("Unknown code target language: " ^ quote target);
in literals end;
@@ -286,15 +287,15 @@
val data = case Symtab.lookup targets target
of SOME data => data
| NONE => error ("Unknown code target language: " ^ quote target);
- in case the_serializer data
- of Serializer _ => (I, data)
- | Extends (super, modify) => let
+ in case the_description data
+ of Fundamental _ => (I, data)
+ | Extension (super, modify) => let
val (modify', data') = collapse_hierarchy super
in (modify' #> modify naming, merge_target false target (data', data)) end
end;
val (modify, data) = collapse_hierarchy target;
- val (serializer, _) = the_default (case the_serializer data
- of Serializer seri => seri) alt_serializer;
+ val serializer = the_default (case the_description data
+ of Fundamental seri => #serializer seri) alt_serializer;
val reserved = the_reserved data;
fun select_include names_all (name, (content, cs)) =
if null cs then SOME (name, content)
@@ -376,9 +377,8 @@
fun export_code thy cs seris =
let
val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
- fun mk_seri_dest dest = case dest
- of "-" => export
- | f => file (Path.explode f)
+ fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
+ else file (Path.explode dest);
val _ = map (fn (((target, module), dest), args) =>
(mk_seri_dest dest (serialize thy target NONE module args naming program cs'))) seris;
in () end;
@@ -524,7 +524,7 @@
(Scan.repeat1 Parse.term_group
-- Scan.repeat (Parse.$$$ inK |-- Parse.name
-- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
- --| Parse.$$$ fileK -- Parse.name
+ -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
-- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));