# HG changeset patch
# User haftmann
# Date 1343420798 -7200
# Node ID 084cd758a8ab92a9dcd2312c24509336da50c3da
# Parent  6e57023954917569545aa69e21ccbd5eff4f7132
evaluation: allow multiple code modules

diff -r 6e5702395491 -r 084cd758a8ab src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Jul 27 21:57:56 2012 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jul 27 22:26:38 2012 +0200
@@ -281,9 +281,10 @@
   (SML "HOLogic.mk'_number/ HOLogic.natT")
 
 text {*
-  FIXME -- Evaluation with @{text "Quickcheck_Narrowing"} does not work, as
-  @{text "code_module"} is very aggressive leading to bad Haskell code.
-  Therefore, we simply deactivate the narrowing-based quickcheck from here on.
+  Evaluation with @{text "Quickcheck_Narrowing"} does not work yet,
+  since a couple of questions how to perform evaluations in Haskell are not that
+  clear yet.  Therefore, we simply deactivate the narrowing-based quickcheck
+  from here on.
 *}
 
 declare [[quickcheck_narrowing_active = false]] 
diff -r 6e5702395491 -r 084cd758a8ab src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 21:57:56 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 22:26:38 2012 +0200
@@ -223,7 +223,7 @@
   let val ({elapsed, ...}, result) = Timing.timing e ()
   in (result, (description, Time.toMilliseconds elapsed)) end
   
-fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code, value_name) =
+fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, value_name) =
   let
     val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
     fun message s = if quiet then () else Output.urgent_message s
@@ -238,31 +238,34 @@
       if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
     fun run in_path = 
       let
-        val code_file = Path.append in_path (Path.basic "Generated_Code.hs")
-        val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
-        val main_file = Path.append in_path (Path.basic "Main.hs")
+        fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
+        val generatedN = Code_Target.generatedN
+        val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file;
+        val code = the (AList.lookup (op =) code_modules generatedN)
+        val code_file = mk_code_file generatedN
+        val narrowing_engine_file = mk_code_file "Narrowing_Engine"
+        val main_file = mk_code_file "Main"
         val main = "module Main where {\n\n" ^
           "import System.IO;\n" ^
           "import System.Environment;\n" ^
           "import Narrowing_Engine;\n" ^
-          "import Generated_Code;\n\n" ^
+          "import " ^ generatedN ^ " ;\n\n" ^
           "main = getArgs >>= \\[potential, size] -> " ^
-          "Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
+          "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^
           "}\n"
         val code' = code
           |> unsuffix "}\n"
           |> suffix "data Typerep = Typerep String [Typerep];\n\n}\n" (* FIXME *)
-        val _ = File.write code_file code'
-        val _ = File.write narrowing_engine_file
-          (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
-        val _ = File.write main_file main
+        val _ = map (uncurry File.write) (includes @
+          [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
+           (code_file, code'), (main_file, main)])
         val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
         val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
           ghc_options ^ " " ^
-          (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
+          (space_implode " " (map File.shell_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
           " -o " ^ executable ^ ";"
         val (result, compilation_time) =
-          elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
+          elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
         val _ = Quickcheck.add_timing compilation_time current_result
         fun haskell_string_of_bool v = if v then "True" else "False"
         val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
@@ -314,7 +317,7 @@
     val ctxt = Proof_Context.init_global thy
     fun evaluator naming program ((_, vs_ty), t) deps =
       Exn.interruptible_capture (value opts ctxt cookie)
-        (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
+        (Code_Target.evaluator thy target naming program deps (vs_ty, t));
   in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
 
 (** counterexample generator **)
diff -r 6e5702395491 -r 084cd758a8ab src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_haskell.ML	Fri Jul 27 22:26:38 2012 +0200
@@ -395,7 +395,7 @@
     Code_Target.serialization
       (fn width => fn destination => K () o map (write_module width destination))
       (fn present => fn width => rpair (try (deresolver ""))
-        o format present width o Pretty.chunks o map snd)
+        o (map o apsnd) (format present width))
       (map (uncurry print_module_frame o apsnd single) includes
         @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
           ((flat o rev o Graph.strong_conn) haskell_program))
diff -r 6e5702395491 -r 084cd758a8ab src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_ml.ML	Fri Jul 27 22:26:38 2012 +0200
@@ -811,8 +811,9 @@
         lift_markup = apsnd } ml_program));
     fun write width NONE = writeln o format [] width
       | write width (SOME p) = File.write p o format [] width;
+    fun prepare names width p = ([("", format names width p)], try (deresolver []));
   in
-    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
+    Code_Target.serialization write prepare p
   end;
 
 val serializer_sml : Code_Target.serializer =
diff -r 6e5702395491 -r 084cd758a8ab src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Jul 27 22:26:38 2012 +0200
@@ -87,7 +87,9 @@
     val ctxt = Proof_Context.init_global thy;
   in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
 
-fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target);
+fun obtain_evaluator thy some_target naming program consts expr =
+  Code_Target.evaluator thy (the_default target some_target) naming program consts expr
+  |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
 
 fun evaluation cookie thy evaluator vs_t args =
   let
@@ -192,9 +194,10 @@
     val ctxt = Proof_Context.init_global thy;
     val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
     val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
-    val (ml_code, target_names) =
+    val (ml_modules, target_names) =
       Code_Target.produce_code_for thy
         target NONE module_name [] naming program (consts' @ tycos');
+    val ml_code = space_implode "\n\n" (map snd ml_modules);
     val (consts'', tycos'') = chop (length consts') target_names;
     val consts_map = map2 (fn const =>
       fn NONE =>
diff -r 6e5702395491 -r 084cd758a8ab src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_scala.ML	Fri Jul 27 22:26:38 2012 +0200
@@ -385,8 +385,9 @@
         lift_markup = I } scala_program);
     fun write width NONE = writeln o format [] width
       | write width (SOME p) = File.write p o format [] width;
+    fun prepare names width p = ([("", format names width p)], try (deresolver []));
   in
-    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
+    Code_Target.serialization write prepare p
   end;
 
 val serializer : Code_Target.serializer =
diff -r 6e5702395491 -r 084cd758a8ab src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Jul 27 22:26:38 2012 +0200
@@ -13,7 +13,7 @@
   val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
   val produce_code_for: theory -> string -> int option -> string -> Token.T list
-    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
+    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> (string * string) list * string option list
   val present_code_for: theory -> string -> int option -> string -> Token.T list
     -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
   val check_code_for: theory -> string -> bool -> Token.T list
@@ -22,15 +22,16 @@
   val export_code: theory -> string list
     -> (((string * string) * Path.T option) * Token.T list) list -> unit
   val produce_code: theory -> string list
-    -> string -> int option -> string -> Token.T list -> string * string option list
+    -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
   val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
     -> string -> int option -> string -> Token.T list -> string
   val check_code: theory -> string list
     -> ((string * bool) * Token.T list) list -> unit
 
+  val generatedN: string
   val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program
     -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-    -> string * string
+    -> (string * string) list * string
 
   type serializer
   type literals = Code_Printer.literals
@@ -45,7 +46,7 @@
   type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
   val serialization: (int -> Path.T option -> 'a -> unit)
-    -> (string list -> int -> 'a -> string * (string -> string option))
+    -> (string list -> int -> 'a -> (string * string) list * (string -> string option))
     -> 'a -> serialization
   val set_default_code_width: int -> theory -> theory
 
@@ -77,7 +78,7 @@
 (** abstract nonsense **)
 
 datatype destination = Export of Path.T option | Produce | Present of string list;
-type serialization = int -> destination -> (string * (string -> string option)) option;
+type serialization = int -> destination -> ((string * string) list * (string -> string option)) option;
 
 fun serialization output _ content width (Export some_path) =
       (output width some_path content; NONE)
@@ -85,12 +86,12 @@
       string [] width content |> SOME
   | serialization _ string content width (Present stmt_names) =
      string stmt_names width content
-     |> apfst (Pretty.output (SOME width) o Pretty.str)
+     |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str)
      |> SOME;
 
 fun export some_path f = (f (Export some_path); ());
 fun produce f = the (f Produce);
-fun present stmt_names f = fst (the (f (Present stmt_names)));
+fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names)))));
 
 
 (** theory data **)
@@ -378,6 +379,8 @@
 
 in
 
+val generatedN = "Generated_Code";
+
 fun export_code_for thy some_path target some_width module_name args =
   export (using_master_directory thy some_path)
   ooo invoke_serializer thy target some_width module_name args;
@@ -398,15 +401,14 @@
 
 fun check_code_for thy target strict args naming program names_cs =
   let
-    val module_name = "Generated_Code";
     val { env_var, make_destination, make_command } =
       (#check o the_fundamental thy) target;
     fun ext_check p =
       let
         val destination = make_destination p;
         val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
-          module_name args naming program names_cs);
-        val cmd = make_command module_name;
+          generatedN args naming program names_cs);
+        val cmd = make_command generatedN;
       in
         if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
         then error ("Code check failed for " ^ target ^ ": " ^ cmd)
@@ -439,7 +441,7 @@
 fun evaluator thy target naming program consts =
   let
     val (mounted_serializer, prepared_program) = mount_serializer thy
-      target NONE "Generated_Code" [] naming program consts;
+      target NONE generatedN [] naming program consts;
   in evaluation mounted_serializer prepared_program consts end;
 
 end; (* local *)