# HG changeset patch
# User haftmann
# Date 1278598764 -7200
# Node ID 6315b6426200429377b1f8628e3db004cece1c15
# Parent  3daaf23b9ab4ec43ad79a99559ee3efbdbb9d103
checking generated code for various target languages

diff -r 3daaf23b9ab4 -r 6315b6426200 src/HOL/Codegenerator_Test/Generate.thy
--- a/src/HOL/Codegenerator_Test/Generate.thy	Thu Jul 08 16:19:24 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Thu Jul 08 16:19:24 2010 +0200
@@ -7,9 +7,23 @@
 imports Candidates
 begin
 
-export_code * in SML module_name Code_Test
-  in OCaml module_name Code_Test file -
-  in Haskell file -
-  in Scala file -
+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.
+*}
+
+export_code "*" in SML module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
+
+export_code "*" in OCaml module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
+
+export_code "*" in Haskell module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
+
+export_code "*" in Scala module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
 
 end
diff -r 3daaf23b9ab4 -r 6315b6426200 src/HOL/Codegenerator_Test/Generate_Pretty.thy
--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Thu Jul 08 16:19:24 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Thu Jul 08 16:19:24 2010 +0200
@@ -12,9 +12,23 @@
 lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
 lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
 
-export_code * in SML module_name Code_Test
-  in OCaml module_name Code_Test file -
-  in Haskell file -
-  in Scala file -
+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.
+*}
+
+export_code "*" in SML module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
+
+export_code "*" in OCaml module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
+
+export_code "*" in Haskell module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
+
+export_code "*" in Scala module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
 
 end
diff -r 3daaf23b9ab4 -r 6315b6426200 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:19:24 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_haskell.ML
+(*  Title:      Tools/Code/code_haskell.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Serializer for Haskell.
@@ -6,6 +6,8 @@
 
 signature CODE_HASKELL =
 sig
+  val target: string
+  val check: theory -> Path.T -> unit
   val setup: theory -> theory
 end;
 
@@ -462,6 +464,14 @@
   else error "Only Haskell target allows for monad syntax" end;
 
 
+(** formal checking of compiled code **)
+
+fun check thy = Code_Target.external_check thy target
+  "EXEC_GHC" I (fn ghc => fn p => fn module_name =>
+    ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs");
+
+
+
 (** Isar setup **)
 
 fun isar_seri_haskell module_name =
diff -r 3daaf23b9ab4 -r 6315b6426200 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Jul 08 16:19:24 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_ml.ML
+(*  Title:      Tools/Code/code_ml.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Serializer for SML and OCaml.
@@ -7,10 +7,13 @@
 signature CODE_ML =
 sig
   val target_SML: string
+  val target_OCaml: string
   val evaluation_code_of: theory -> string -> string
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
   val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
     -> Code_Printer.fixity -> 'a list -> Pretty.T option
+  val check_SML: theory -> Path.T -> unit
+  val check_OCaml: theory -> Path.T -> unit
   val setup: theory -> theory
 end;
 
@@ -950,6 +953,17 @@
     serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
 
 
+(** formal checking of compiled code **)
+
+fun check_SML thy = Code_Target.external_check thy target_SML
+  "ISABELLE_PROCESS" (fn p => Path.append p (Path.explode "ROOT.ML"))
+  (fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure");
+
+fun check_OCaml thy = Code_Target.external_check thy target_OCaml
+  "EXEC_OCAML" (fn p => Path.append p (Path.explode "ROOT.ocaml"))
+  (fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p);
+
+
 (** Isar setup **)
 
 fun isar_seri_sml module_name =
diff -r 3daaf23b9ab4 -r 6315b6426200 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jul 08 16:19:24 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Florian Haftmann, TU Muenchen
+(*  Title:      Tools/Code/code_scala.ML
+    Author:     Florian Haftmann, TU Muenchen
 
 Serializer for Scala.
 *)
 
 signature CODE_SCALA =
 sig
+  val target: string
+  val check: theory -> Path.T -> unit
   val setup: theory -> theory
 end;
 
@@ -411,6 +414,14 @@
 } end;
 
 
+(** formal checking of compiled code **)
+
+fun check thy = Code_Target.external_check thy target
+  "SCALA_HOME" I (fn scala_home => fn p => fn _ =>
+    Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala");
+
+
+
 (** Isar setup **)
 
 fun isar_seri_scala module_name =
diff -r 3daaf23b9ab4 -r 6315b6426200 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Jul 08 16:19:24 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Tools/code/code_target.ML
+(*  Title:      Tools/Code/code_target.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Serializer from intermediate language ("Thin-gol") to target languages.
@@ -36,6 +36,8 @@
   val string: string list -> serialization -> string
   val code_of: theory -> string -> int option -> string
     -> string list -> (Code_Thingol.naming -> string list) -> string
+  val external_check: theory -> string -> string
+    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> Path.T -> unit
   val set_default_code_width: int -> theory -> theory
   val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
 
@@ -355,6 +357,27 @@
       if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
   in union (op =) cs3 cs1 end;
 
+fun external_check thy target env_var make_destination make_command p =
+  let
+    val env_param = getenv env_var;
+    fun ext_check env_param =
+      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) <> 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 ext_check env_param
+  end;
+
 fun export_code thy cs seris =
   let
     val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;