# HG changeset patch
# User haftmann
# Date 1279112024 -7200
# Node ID 3cbb22cec751f3e993ab904164409dbb4dcb74ee
# Parent  ffaca9167c1605a68c5a793c50acf4b2fddb8284
formal slot for code checker

diff -r ffaca9167c16 -r 3cbb22cec751 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Wed Jul 14 14:53:44 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Jul 14 14:53:44 2010 +0200
@@ -474,7 +474,7 @@
 
 (** Isar setup **)
 
-fun isar_seri_haskell module_name =
+fun isar_serializer module_name =
   Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
     -- Scan.optional (Args.$$$ "string_classes" >> K true) false
     >> (fn (module_prefix, string_classes) =>
@@ -487,7 +487,8 @@
   );
 
 val setup =
-  Code_Target.add_target (target, (isar_seri_haskell, literals))
+  Code_Target.add_target
+    (target, { serializer = isar_serializer, literals = literals, check = () })
   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
diff -r ffaca9167c16 -r 3cbb22cec751 src/Tools/Code/code_ml.ML
--- 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,
diff -r ffaca9167c16 -r 3cbb22cec751 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Jul 14 14:53:44 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Jul 14 14:53:44 2010 +0200
@@ -424,12 +424,13 @@
 
 (** Isar setup **)
 
-fun isar_seri_scala module_name =
+fun isar_serializer module_name =
   Code_Target.parse_args (Scan.succeed ())
   #> (fn () => serialize_scala module_name);
 
 val setup =
-  Code_Target.add_target (target, (isar_seri_scala, literals))
+  Code_Target.add_target
+    (target, { serializer = isar_serializer, literals = literals, check = () })
   #> Code_Target.add_syntax_tyco target "fun"
      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
         brackify_infix (1, R) fxy (
diff -r ffaca9167c16 -r 3cbb22cec751 src/Tools/Code/code_target.ML
--- 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));