# HG changeset patch
# User haftmann
# Date 1279115369 -7200
# Node ID 365e37fe93f37ba76cb1c4e8605afbeaf2027d9a
# Parent  194a7d543a700a520ea3dc3fae97b3976d6e1199
added Isar syntax for code checking

diff -r 194a7d543a70 -r 365e37fe93f3 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Jul 14 15:49:29 2010 +0200
+++ b/etc/isar-keywords.el	Wed Jul 14 15:49:29 2010 +0200
@@ -285,6 +285,7 @@
     "avoids"
     "begin"
     "binder"
+    "checking"
     "congs"
     "constrains"
     "contains"
diff -r 194a7d543a70 -r 365e37fe93f3 src/HOL/Codegenerator_Test/Generate.thy
--- a/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 15:49:29 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 15:49:29 2010 +0200
@@ -10,20 +10,10 @@
 subsection {* Check whether generated code compiles *}
 
 text {*
-  If any of the @{text ML} ... check fails, inspect the code generated
-  by the previous @{text export_code} command.
+  If any of the checks fails, inspect the code generated
+  by a corresponding @{text export_code} command.
 *}
 
-export_code "*" in SML module_name Code_Test file -
-ML {* Code_ML.check_SML @{theory} *}
-
-export_code "*" in OCaml module_name Code_Test file -
-ML {* Code_ML.check_OCaml @{theory} *}
-
-export_code "*" in Haskell module_name Code_Test file -
-ML {* Code_Haskell.check @{theory} *}
-
-export_code "*" in Scala module_name Code_Test file -
-ML {* Code_Scala.check @{theory} *}
+export_code "*" checking SML OCaml Haskell Scala
 
 end
diff -r 194a7d543a70 -r 365e37fe93f3 src/HOL/Codegenerator_Test/Generate_Pretty.thy
--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 15:49:29 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 15:49:29 2010 +0200
@@ -15,20 +15,10 @@
 subsection {* Check whether generated code compiles *}
 
 text {*
-  If any of the @{text ML} ... check fails, inspect the code generated
-  by the previous @{text export_code} command.
+  If any of the checks fails, inspect the code generated
+  by a corresponding @{text export_code} command.
 *}
 
-export_code "*" in SML module_name Code_Test file -
-ML {* Code_ML.check_SML @{theory} *}
-
-export_code "*" in OCaml module_name Code_Test file -
-ML {* Code_ML.check_OCaml @{theory} *}
-
-export_code "*" in Haskell module_name Code_Test file -
-ML {* Code_Haskell.check @{theory} *}
-
-export_code "*" in Scala module_name Code_Test file -
-ML {* Code_Scala.check @{theory} *}
+export_code "*" checking SML OCaml Haskell Scala
 
 end
diff -r 194a7d543a70 -r 365e37fe93f3 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Jul 14 15:49:29 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Wed Jul 14 15:49:29 2010 +0200
@@ -36,7 +36,6 @@
   val string: string list -> serialization -> string
   val code_of: theory -> string -> int option -> string
     -> string list -> (Code_Thingol.naming -> string list) -> string
-  val check: theory -> string -> unit
   val set_default_code_width: int -> theory -> theory
   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
 
@@ -322,6 +321,27 @@
 
 fun serialize thy = mount_serializer thy NONE;
 
+fun check thy names_cs naming program target args =
+  let
+    val module_name = "Code_Test";
+    val { env_var, make_destination, make_command } =
+      (#check o the_fundamental thy) target;
+    val env_param = getenv env_var;
+    fun ext_check env_param p =
+      let 
+        val destination = make_destination p;
+        val _ = file destination (serialize thy target (SOME 80)
+          (SOME module_name) args naming program names_cs);
+        val cmd = make_command env_param destination module_name;
+      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
+        then error ("Code check failed for " ^ target ^ ": " ^ cmd)
+        else ()
+      end;
+  in if env_param = ""
+    then warning (env_var ^ " not set; skipped code check for " ^ target)
+    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
+  end;
+
 fun serialize_custom thy (target_name, seri) naming program names =
   mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
   |> the;
@@ -357,41 +377,25 @@
       if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
   in union (op =) cs3 cs1 end;
 
-fun check thy target =
-  let
-    val { env_var, make_destination, make_command } =
-      (#check o the_fundamental thy) target;
-    val env_param = getenv env_var;
-    fun ext_check env_param p =
-      let 
-        val module_name = "Code_Test";
-        val (cs, (naming, program)) =
-          Code_Thingol.consts_program thy false (read_const_exprs thy ["*"]);
-        val destination = make_destination p;
-        val _ = file destination (serialize thy target (SOME 80)
-          (SOME module_name) [] naming program cs);
-        val cmd = make_command env_param destination module_name;
-      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
-        then error ("Code check failed for " ^ target ^ ": " ^ cmd)
-        else ()
-      end;
-  in if env_param = ""
-    then warning (env_var ^ " not set; skipped code check for " ^ target)
-    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
-  end;
-
-
 fun export_code thy cs seris =
   let
-    val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
+    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
     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;
+      (mk_seri_dest dest (serialize thy target NONE module args naming program names_cs))) seris;
   in () end;
 
 fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
 
+fun check_code thy cs seris =
+  let
+    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
+    val _ = map (fn (target, args) => check thy names_cs naming program target args) seris;
+  in () end;
+
+fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
+
 
 (** serializer configuration **)
 
@@ -525,17 +529,20 @@
 
 (** Isar setup **)
 
-val (inK, module_nameK, fileK) = ("in", "module_name", "file");
+val (inK, module_nameK, fileK, checkingK) = ("in", "module_name", "file", "checking");
+
+val code_expr_argsP = Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") [];
 
 val code_exprP =
-  (Scan.repeat1 Parse.term_group
-  -- Scan.repeat (Parse.$$$ inK |-- Parse.name
-     -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
-     -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
-     -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
-  ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
+  Scan.repeat1 Parse.term_group :|-- (fn raw_cs =>
+    ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name -- code_expr_argsP))
+      >> (fn seris => check_code_cmd raw_cs seris)
+    || Scan.repeat (Parse.$$$ inK |-- Parse.name
+       -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
+       -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
+       -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
 
-val _ = List.app Keyword.keyword [inK, module_nameK, fileK];
+val _ = List.app Keyword.keyword [inK, module_nameK, fileK, checkingK];
 
 val _ =
   Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (