1.1 --- a/src/Tools/Code/code_target.ML Wed Jul 14 14:53:44 2010 +0200
1.2 +++ b/src/Tools/Code/code_target.ML Wed Jul 14 14:53:44 2010 +0200
1.3 @@ -11,7 +11,8 @@
1.4
1.5 type serializer
1.6 type literals = Code_Printer.literals
1.7 - val add_target: string * (serializer * literals) -> theory -> theory
1.8 + val add_target: string * { serializer: serializer, literals: literals, check: unit }
1.9 + -> theory -> theory
1.10 val extend_target: string *
1.11 (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
1.12 -> theory -> theory
1.13 @@ -26,7 +27,7 @@
1.14 -> 'a -> serialization
1.15 val serialize: theory -> string -> int option -> string option -> Token.T list
1.16 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
1.17 - val serialize_custom: theory -> string * (serializer * literals)
1.18 + val serialize_custom: theory -> string * serializer
1.19 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
1.20 val the_literals: theory -> string -> literals
1.21 val export: serialization -> unit
1.22 @@ -114,39 +115,39 @@
1.23 -> string list (*selected statements*)
1.24 -> serialization;
1.25
1.26 -datatype serializer_entry = Serializer of serializer * Code_Printer.literals
1.27 - | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
1.28 +datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, check: unit }
1.29 + | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
1.30
1.31 datatype target = Target of {
1.32 serial: serial,
1.33 - serializer: serializer_entry,
1.34 + description: description,
1.35 reserved: string list,
1.36 includes: (Pretty.T * string list) Symtab.table,
1.37 name_syntax_table: name_syntax_table,
1.38 module_alias: string Symtab.table
1.39 };
1.40
1.41 -fun make_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
1.42 - Target { serial = serial, serializer = serializer, reserved = reserved,
1.43 +fun make_target ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))) =
1.44 + Target { serial = serial, description = description, reserved = reserved,
1.45 includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
1.46 -fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
1.47 - make_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
1.48 -fun merge_target strict target (Target { serial = serial1, serializer = serializer,
1.49 +fun map_target f ( Target { serial, description, reserved, includes, name_syntax_table, module_alias } ) =
1.50 + make_target (f ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))));
1.51 +fun merge_target strict target (Target { serial = serial1, description = description,
1.52 reserved = reserved1, includes = includes1,
1.53 name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
1.54 - Target { serial = serial2, serializer = _,
1.55 + Target { serial = serial2, description = _,
1.56 reserved = reserved2, includes = includes2,
1.57 name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
1.58 if serial1 = serial2 orelse not strict then
1.59 - make_target ((serial1, serializer),
1.60 + make_target ((serial1, description),
1.61 ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
1.62 (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
1.63 Symtab.join (K fst) (module_alias1, module_alias2))
1.64 ))
1.65 else
1.66 - error ("Incompatible serializers: " ^ quote target);
1.67 + error ("Incompatible targets: " ^ quote target);
1.68
1.69 -fun the_serializer (Target { serializer, ... }) = serializer;
1.70 +fun the_description (Target { description, ... }) = description;
1.71 fun the_reserved (Target { reserved, ... }) = reserved;
1.72 fun the_includes (Target { includes, ... }) = includes;
1.73 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
1.74 @@ -172,14 +173,14 @@
1.75 let
1.76 val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
1.77 val _ = case seri
1.78 - of Extends (super, _) => if is_some (lookup_target super) then ()
1.79 + of Extension (super, _) => if is_some (lookup_target super) then ()
1.80 else error ("Unknown code target language: " ^ quote super)
1.81 | _ => ();
1.82 - val overwriting = case (Option.map the_serializer o lookup_target) target
1.83 + val overwriting = case (Option.map the_description o lookup_target) target
1.84 of NONE => false
1.85 - | SOME (Extends _) => true
1.86 - | SOME (Serializer _) => (case seri
1.87 - of Extends _ => error ("Will not overwrite existing target " ^ quote target)
1.88 + | SOME (Extension _) => true
1.89 + | SOME (Fundamental _) => (case seri
1.90 + of Extension _ => error ("Will not overwrite existing target " ^ quote target)
1.91 | _ => true);
1.92 val _ = if overwriting
1.93 then warning ("Overwriting existing target " ^ quote target)
1.94 @@ -192,9 +193,9 @@
1.95 Symtab.empty))))
1.96 end;
1.97
1.98 -fun add_target (target, seri) = put_target (target, Serializer seri);
1.99 +fun add_target (target, seri) = put_target (target, Fundamental seri);
1.100 fun extend_target (target, (super, modify)) =
1.101 - put_target (target, Extends (super, modify));
1.102 + put_target (target, Extension (super, modify));
1.103
1.104 fun map_target_data target f thy =
1.105 let
1.106 @@ -224,9 +225,9 @@
1.107 let
1.108 val ((targets, _), _) = Targets.get thy;
1.109 fun literals target = case Symtab.lookup targets target
1.110 - of SOME data => (case the_serializer data
1.111 - of Serializer (_, literals) => literals
1.112 - | Extends (super, _) => literals super)
1.113 + of SOME data => (case the_description data
1.114 + of Fundamental { literals, ... } => literals
1.115 + | Extension (super, _) => literals super)
1.116 | NONE => error ("Unknown code target language: " ^ quote target);
1.117 in literals end;
1.118
1.119 @@ -286,15 +287,15 @@
1.120 val data = case Symtab.lookup targets target
1.121 of SOME data => data
1.122 | NONE => error ("Unknown code target language: " ^ quote target);
1.123 - in case the_serializer data
1.124 - of Serializer _ => (I, data)
1.125 - | Extends (super, modify) => let
1.126 + in case the_description data
1.127 + of Fundamental _ => (I, data)
1.128 + | Extension (super, modify) => let
1.129 val (modify', data') = collapse_hierarchy super
1.130 in (modify' #> modify naming, merge_target false target (data', data)) end
1.131 end;
1.132 val (modify, data) = collapse_hierarchy target;
1.133 - val (serializer, _) = the_default (case the_serializer data
1.134 - of Serializer seri => seri) alt_serializer;
1.135 + val serializer = the_default (case the_description data
1.136 + of Fundamental seri => #serializer seri) alt_serializer;
1.137 val reserved = the_reserved data;
1.138 fun select_include names_all (name, (content, cs)) =
1.139 if null cs then SOME (name, content)
1.140 @@ -376,9 +377,8 @@
1.141 fun export_code thy cs seris =
1.142 let
1.143 val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
1.144 - fun mk_seri_dest dest = case dest
1.145 - of "-" => export
1.146 - | f => file (Path.explode f)
1.147 + fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
1.148 + else file (Path.explode dest);
1.149 val _ = map (fn (((target, module), dest), args) =>
1.150 (mk_seri_dest dest (serialize thy target NONE module args naming program cs'))) seris;
1.151 in () end;
1.152 @@ -524,7 +524,7 @@
1.153 (Scan.repeat1 Parse.term_group
1.154 -- Scan.repeat (Parse.$$$ inK |-- Parse.name
1.155 -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
1.156 - --| Parse.$$$ fileK -- Parse.name
1.157 + -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
1.158 -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
1.159 ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
1.160