checking generated code for various target languages
authorhaftmann
Thu Jul 08 16:19:24 2010 +0200 (2010-07-08)
changeset 377456315b6426200
parent 37744 3daaf23b9ab4
child 37746 39253da888c1
checking generated code for various target languages
src/HOL/Codegenerator_Test/Generate.thy
src/HOL/Codegenerator_Test/Generate_Pretty.thy
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/HOL/Codegenerator_Test/Generate.thy	Thu Jul 08 16:19:24 2010 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate.thy	Thu Jul 08 16:19:24 2010 +0200
     1.3 @@ -7,9 +7,23 @@
     1.4  imports Candidates
     1.5  begin
     1.6  
     1.7 -export_code * in SML module_name Code_Test
     1.8 -  in OCaml module_name Code_Test file -
     1.9 -  in Haskell file -
    1.10 -  in Scala file -
    1.11 +subsection {* Check whether generated code compiles *}
    1.12 +
    1.13 +text {*
    1.14 +  If any of the @{text ML} ... check fails, inspect the code generated
    1.15 +  by the previous @{text export_code} command.
    1.16 +*}
    1.17 +
    1.18 +export_code "*" in SML module_name Code_Test file -
    1.19 +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
    1.20 +
    1.21 +export_code "*" in OCaml module_name Code_Test file -
    1.22 +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
    1.23 +
    1.24 +export_code "*" in Haskell module_name Code_Test file -
    1.25 +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
    1.26 +
    1.27 +export_code "*" in Scala module_name Code_Test file -
    1.28 +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
    1.29  
    1.30  end
     2.1 --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Thu Jul 08 16:19:24 2010 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Thu Jul 08 16:19:24 2010 +0200
     2.3 @@ -12,9 +12,23 @@
     2.4  lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
     2.5  lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
     2.6  
     2.7 -export_code * in SML module_name Code_Test
     2.8 -  in OCaml module_name Code_Test file -
     2.9 -  in Haskell file -
    2.10 -  in Scala file -
    2.11 +subsection {* Check whether generated code compiles *}
    2.12 +
    2.13 +text {*
    2.14 +  If any of the @{text ML} ... check fails, inspect the code generated
    2.15 +  by the previous @{text export_code} command.
    2.16 +*}
    2.17 +
    2.18 +export_code "*" in SML module_name Code_Test file -
    2.19 +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
    2.20 +
    2.21 +export_code "*" in OCaml module_name Code_Test file -
    2.22 +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
    2.23 +
    2.24 +export_code "*" in Haskell module_name Code_Test file -
    2.25 +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
    2.26 +
    2.27 +export_code "*" in Scala module_name Code_Test file -
    2.28 +ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
    2.29  
    2.30  end
     3.1 --- a/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:19:24 2010 +0200
     3.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:19:24 2010 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      Tools/code/code_haskell.ML
     3.5 +(*  Title:      Tools/Code/code_haskell.ML
     3.6      Author:     Florian Haftmann, TU Muenchen
     3.7  
     3.8  Serializer for Haskell.
     3.9 @@ -6,6 +6,8 @@
    3.10  
    3.11  signature CODE_HASKELL =
    3.12  sig
    3.13 +  val target: string
    3.14 +  val check: theory -> Path.T -> unit
    3.15    val setup: theory -> theory
    3.16  end;
    3.17  
    3.18 @@ -462,6 +464,14 @@
    3.19    else error "Only Haskell target allows for monad syntax" end;
    3.20  
    3.21  
    3.22 +(** formal checking of compiled code **)
    3.23 +
    3.24 +fun check thy = Code_Target.external_check thy target
    3.25 +  "EXEC_GHC" I (fn ghc => fn p => fn module_name =>
    3.26 +    ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs");
    3.27 +
    3.28 +
    3.29 +
    3.30  (** Isar setup **)
    3.31  
    3.32  fun isar_seri_haskell module_name =
     4.1 --- a/src/Tools/Code/code_ml.ML	Thu Jul 08 16:19:24 2010 +0200
     4.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jul 08 16:19:24 2010 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      Tools/code/code_ml.ML
     4.5 +(*  Title:      Tools/Code/code_ml.ML
     4.6      Author:     Florian Haftmann, TU Muenchen
     4.7  
     4.8  Serializer for SML and OCaml.
     4.9 @@ -7,10 +7,13 @@
    4.10  signature CODE_ML =
    4.11  sig
    4.12    val target_SML: string
    4.13 +  val target_OCaml: string
    4.14    val evaluation_code_of: theory -> string -> string
    4.15      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    4.16    val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
    4.17      -> Code_Printer.fixity -> 'a list -> Pretty.T option
    4.18 +  val check_SML: theory -> Path.T -> unit
    4.19 +  val check_OCaml: theory -> Path.T -> unit
    4.20    val setup: theory -> theory
    4.21  end;
    4.22  
    4.23 @@ -950,6 +953,17 @@
    4.24      serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
    4.25  
    4.26  
    4.27 +(** formal checking of compiled code **)
    4.28 +
    4.29 +fun check_SML thy = Code_Target.external_check thy target_SML
    4.30 +  "ISABELLE_PROCESS" (fn p => Path.append p (Path.explode "ROOT.ML"))
    4.31 +  (fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure");
    4.32 +
    4.33 +fun check_OCaml thy = Code_Target.external_check thy target_OCaml
    4.34 +  "EXEC_OCAML" (fn p => Path.append p (Path.explode "ROOT.ocaml"))
    4.35 +  (fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p);
    4.36 +
    4.37 +
    4.38  (** Isar setup **)
    4.39  
    4.40  fun isar_seri_sml module_name =
     5.1 --- a/src/Tools/Code/code_scala.ML	Thu Jul 08 16:19:24 2010 +0200
     5.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jul 08 16:19:24 2010 +0200
     5.3 @@ -1,10 +1,13 @@
     5.4 -(*  Author:     Florian Haftmann, TU Muenchen
     5.5 +(*  Title:      Tools/Code/code_scala.ML
     5.6 +    Author:     Florian Haftmann, TU Muenchen
     5.7  
     5.8  Serializer for Scala.
     5.9  *)
    5.10  
    5.11  signature CODE_SCALA =
    5.12  sig
    5.13 +  val target: string
    5.14 +  val check: theory -> Path.T -> unit
    5.15    val setup: theory -> theory
    5.16  end;
    5.17  
    5.18 @@ -411,6 +414,14 @@
    5.19  } end;
    5.20  
    5.21  
    5.22 +(** formal checking of compiled code **)
    5.23 +
    5.24 +fun check thy = Code_Target.external_check thy target
    5.25 +  "SCALA_HOME" I (fn scala_home => fn p => fn _ =>
    5.26 +    Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala");
    5.27 +
    5.28 +
    5.29 +
    5.30  (** Isar setup **)
    5.31  
    5.32  fun isar_seri_scala module_name =
     6.1 --- a/src/Tools/Code/code_target.ML	Thu Jul 08 16:19:24 2010 +0200
     6.2 +++ b/src/Tools/Code/code_target.ML	Thu Jul 08 16:19:24 2010 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      Tools/code/code_target.ML
     6.5 +(*  Title:      Tools/Code/code_target.ML
     6.6      Author:     Florian Haftmann, TU Muenchen
     6.7  
     6.8  Serializer from intermediate language ("Thin-gol") to target languages.
     6.9 @@ -36,6 +36,8 @@
    6.10    val string: string list -> serialization -> string
    6.11    val code_of: theory -> string -> int option -> string
    6.12      -> string list -> (Code_Thingol.naming -> string list) -> string
    6.13 +  val external_check: theory -> string -> string
    6.14 +    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> Path.T -> unit
    6.15    val set_default_code_width: int -> theory -> theory
    6.16    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    6.17  
    6.18 @@ -355,6 +357,27 @@
    6.19        if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
    6.20    in union (op =) cs3 cs1 end;
    6.21  
    6.22 +fun external_check thy target env_var make_destination make_command p =
    6.23 +  let
    6.24 +    val env_param = getenv env_var;
    6.25 +    fun ext_check env_param =
    6.26 +      let 
    6.27 +        val module_name = "Code_Test";
    6.28 +        val (cs, (naming, program)) =
    6.29 +          Code_Thingol.consts_program thy false (read_const_exprs thy ["*"]);
    6.30 +        val destination = make_destination p;
    6.31 +        val _ = file destination (serialize thy target (SOME 80)
    6.32 +          (SOME module_name) [] naming program cs);
    6.33 +        val cmd = make_command env_param destination module_name;
    6.34 +      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd) <> 0
    6.35 +        then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    6.36 +        else ()
    6.37 +      end;
    6.38 +  in if env_param = ""
    6.39 +    then warning (env_var ^ " not set; skipped code check for " ^ target)
    6.40 +    else ext_check env_param
    6.41 +  end;
    6.42 +
    6.43  fun export_code thy cs seris =
    6.44    let
    6.45      val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;