1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Jul 27 21:57:56 2012 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jul 27 22:26:38 2012 +0200
     1.3 @@ -281,9 +281,10 @@
     1.4    (SML "HOLogic.mk'_number/ HOLogic.natT")
     1.5  
     1.6  text {*
     1.7 -  FIXME -- Evaluation with @{text "Quickcheck_Narrowing"} does not work, as
     1.8 -  @{text "code_module"} is very aggressive leading to bad Haskell code.
     1.9 -  Therefore, we simply deactivate the narrowing-based quickcheck from here on.
    1.10 +  Evaluation with @{text "Quickcheck_Narrowing"} does not work yet,
    1.11 +  since a couple of questions how to perform evaluations in Haskell are not that
    1.12 +  clear yet.  Therefore, we simply deactivate the narrowing-based quickcheck
    1.13 +  from here on.
    1.14  *}
    1.15  
    1.16  declare [[quickcheck_narrowing_active = false]] 

     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 21:57:56 2012 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 22:26:38 2012 +0200
     2.3 @@ -223,7 +223,7 @@
     2.4    let val ({elapsed, ...}, result) = Timing.timing e ()
     2.5    in (result, (description, Time.toMilliseconds elapsed)) end
     2.6    
     2.7 -fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code, value_name) =
     2.8 +fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, value_name) =
     2.9    let
    2.10      val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
    2.11      fun message s = if quiet then () else Output.urgent_message s
    2.12 @@ -238,31 +238,34 @@
    2.13        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
    2.14      fun run in_path = 
    2.15        let
    2.16 -        val code_file = Path.append in_path (Path.basic "Generated_Code.hs")
    2.17 -        val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
    2.18 -        val main_file = Path.append in_path (Path.basic "Main.hs")
    2.19 +        fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
    2.20 +        val generatedN = Code_Target.generatedN
    2.21 +        val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file;
    2.22 +        val code = the (AList.lookup (op =) code_modules generatedN)
    2.23 +        val code_file = mk_code_file generatedN
    2.24 +        val narrowing_engine_file = mk_code_file "Narrowing_Engine"
    2.25 +        val main_file = mk_code_file "Main"
    2.26          val main = "module Main where {\n\n" ^
    2.27            "import System.IO;\n" ^
    2.28            "import System.Environment;\n" ^
    2.29            "import Narrowing_Engine;\n" ^
    2.30 -          "import Generated_Code;\n\n" ^
    2.31 +          "import " ^ generatedN ^ " ;\n\n" ^
    2.32            "main = getArgs >>= \\[potential, size] -> " ^
    2.33 -          "Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
    2.34 +          "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^
    2.35            "}\n"
    2.36          val code' = code
    2.37            |> unsuffix "}\n"
    2.38            |> suffix "data Typerep = Typerep String [Typerep];\n\n}\n" (* FIXME *)
    2.39 -        val _ = File.write code_file code'
    2.40 -        val _ = File.write narrowing_engine_file
    2.41 -          (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
    2.42 -        val _ = File.write main_file main
    2.43 +        val _ = map (uncurry File.write) (includes @
    2.44 +          [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
    2.45 +           (code_file, code'), (main_file, main)])
    2.46          val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
    2.47          val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
    2.48            ghc_options ^ " " ^
    2.49 -          (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    2.50 +          (space_implode " " (map File.shell_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
    2.51            " -o " ^ executable ^ ";"
    2.52          val (result, compilation_time) =
    2.53 -          elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
    2.54 +          elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
    2.55          val _ = Quickcheck.add_timing compilation_time current_result
    2.56          fun haskell_string_of_bool v = if v then "True" else "False"
    2.57          val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
    2.58 @@ -314,7 +317,7 @@
    2.59      val ctxt = Proof_Context.init_global thy
    2.60      fun evaluator naming program ((_, vs_ty), t) deps =
    2.61        Exn.interruptible_capture (value opts ctxt cookie)
    2.62 -        (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
    2.63 +        (Code_Target.evaluator thy target naming program deps (vs_ty, t));
    2.64    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    2.65  
    2.66  (** counterexample generator **)

     3.1 --- a/src/Tools/Code/code_haskell.ML	Fri Jul 27 21:57:56 2012 +0200
     3.2 +++ b/src/Tools/Code/code_haskell.ML	Fri Jul 27 22:26:38 2012 +0200
     3.3 @@ -395,7 +395,7 @@
     3.4      Code_Target.serialization
     3.5        (fn width => fn destination => K () o map (write_module width destination))
     3.6        (fn present => fn width => rpair (try (deresolver ""))
     3.7 -        o format present width o Pretty.chunks o map snd)
     3.8 +        o (map o apsnd) (format present width))
     3.9        (map (uncurry print_module_frame o apsnd single) includes
    3.10          @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
    3.11            ((flat o rev o Graph.strong_conn) haskell_program))

     4.1 --- a/src/Tools/Code/code_ml.ML	Fri Jul 27 21:57:56 2012 +0200
     4.2 +++ b/src/Tools/Code/code_ml.ML	Fri Jul 27 22:26:38 2012 +0200
     4.3 @@ -811,8 +811,9 @@
     4.4          lift_markup = apsnd } ml_program));
     4.5      fun write width NONE = writeln o format [] width
     4.6        | write width (SOME p) = File.write p o format [] width;
     4.7 +    fun prepare names width p = ([("", format names width p)], try (deresolver []));
     4.8    in
     4.9 -    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
    4.10 +    Code_Target.serialization write prepare p
    4.11    end;
    4.12  
    4.13  val serializer_sml : Code_Target.serializer =

     5.1 --- a/src/Tools/Code/code_runtime.ML	Fri Jul 27 21:57:56 2012 +0200
     5.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Jul 27 22:26:38 2012 +0200
     5.3 @@ -87,7 +87,9 @@
     5.4      val ctxt = Proof_Context.init_global thy;
     5.5    in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
     5.6  
     5.7 -fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target);
     5.8 +fun obtain_evaluator thy some_target naming program consts expr =
     5.9 +  Code_Target.evaluator thy (the_default target some_target) naming program consts expr
    5.10 +  |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    5.11  
    5.12  fun evaluation cookie thy evaluator vs_t args =
    5.13    let
    5.14 @@ -192,9 +194,10 @@
    5.15      val ctxt = Proof_Context.init_global thy;
    5.16      val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
    5.17      val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
    5.18 -    val (ml_code, target_names) =
    5.19 +    val (ml_modules, target_names) =
    5.20        Code_Target.produce_code_for thy
    5.21          target NONE module_name [] naming program (consts' @ tycos');
    5.22 +    val ml_code = space_implode "\n\n" (map snd ml_modules);
    5.23      val (consts'', tycos'') = chop (length consts') target_names;
    5.24      val consts_map = map2 (fn const =>
    5.25        fn NONE =>

     6.1 --- a/src/Tools/Code/code_scala.ML	Fri Jul 27 21:57:56 2012 +0200
     6.2 +++ b/src/Tools/Code/code_scala.ML	Fri Jul 27 22:26:38 2012 +0200
     6.3 @@ -385,8 +385,9 @@
     6.4          lift_markup = I } scala_program);
     6.5      fun write width NONE = writeln o format [] width
     6.6        | write width (SOME p) = File.write p o format [] width;
     6.7 +    fun prepare names width p = ([("", format names width p)], try (deresolver []));
     6.8    in
     6.9 -    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
    6.10 +    Code_Target.serialization write prepare p
    6.11    end;
    6.12  
    6.13  val serializer : Code_Target.serializer =

     7.1 --- a/src/Tools/Code/code_target.ML	Fri Jul 27 21:57:56 2012 +0200
     7.2 +++ b/src/Tools/Code/code_target.ML	Fri Jul 27 22:26:38 2012 +0200
     7.3 @@ -13,7 +13,7 @@
     7.4    val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
     7.5      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
     7.6    val produce_code_for: theory -> string -> int option -> string -> Token.T list
     7.7 -    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
     7.8 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> (string * string) list * string option list
     7.9    val present_code_for: theory -> string -> int option -> string -> Token.T list
    7.10      -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
    7.11    val check_code_for: theory -> string -> bool -> Token.T list
    7.12 @@ -22,15 +22,16 @@
    7.13    val export_code: theory -> string list
    7.14      -> (((string * string) * Path.T option) * Token.T list) list -> unit
    7.15    val produce_code: theory -> string list
    7.16 -    -> string -> int option -> string -> Token.T list -> string * string option list
    7.17 +    -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
    7.18    val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
    7.19      -> string -> int option -> string -> Token.T list -> string
    7.20    val check_code: theory -> string list
    7.21      -> ((string * bool) * Token.T list) list -> unit
    7.22  
    7.23 +  val generatedN: string
    7.24    val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program
    7.25      -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    7.26 -    -> string * string
    7.27 +    -> (string * string) list * string
    7.28  
    7.29    type serializer
    7.30    type literals = Code_Printer.literals
    7.31 @@ -45,7 +46,7 @@
    7.32    type serialization
    7.33    val parse_args: 'a parser -> Token.T list -> 'a
    7.34    val serialization: (int -> Path.T option -> 'a -> unit)
    7.35 -    -> (string list -> int -> 'a -> string * (string -> string option))
    7.36 +    -> (string list -> int -> 'a -> (string * string) list * (string -> string option))
    7.37      -> 'a -> serialization
    7.38    val set_default_code_width: int -> theory -> theory
    7.39  
    7.40 @@ -77,7 +78,7 @@
    7.41  (** abstract nonsense **)
    7.42  
    7.43  datatype destination = Export of Path.T option | Produce | Present of string list;
    7.44 -type serialization = int -> destination -> (string * (string -> string option)) option;
    7.45 +type serialization = int -> destination -> ((string * string) list * (string -> string option)) option;
    7.46  
    7.47  fun serialization output _ content width (Export some_path) =
    7.48        (output width some_path content; NONE)
    7.49 @@ -85,12 +86,12 @@
    7.50        string [] width content |> SOME
    7.51    | serialization _ string content width (Present stmt_names) =
    7.52       string stmt_names width content
    7.53 -     |> apfst (Pretty.output (SOME width) o Pretty.str)
    7.54 +     |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str)
    7.55       |> SOME;
    7.56  
    7.57  fun export some_path f = (f (Export some_path); ());
    7.58  fun produce f = the (f Produce);
    7.59 -fun present stmt_names f = fst (the (f (Present stmt_names)));
    7.60 +fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names)))));
    7.61  
    7.62  
    7.63  (** theory data **)
    7.64 @@ -378,6 +379,8 @@
    7.65  
    7.66  in
    7.67  
    7.68 +val generatedN = "Generated_Code";
    7.69 +
    7.70  fun export_code_for thy some_path target some_width module_name args =
    7.71    export (using_master_directory thy some_path)
    7.72    ooo invoke_serializer thy target some_width module_name args;
    7.73 @@ -398,15 +401,14 @@
    7.74  
    7.75  fun check_code_for thy target strict args naming program names_cs =
    7.76    let
    7.77 -    val module_name = "Generated_Code";
    7.78      val { env_var, make_destination, make_command } =
    7.79        (#check o the_fundamental thy) target;
    7.80      fun ext_check p =
    7.81        let
    7.82          val destination = make_destination p;
    7.83          val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
    7.84 -          module_name args naming program names_cs);
    7.85 -        val cmd = make_command module_name;
    7.86 +          generatedN args naming program names_cs);
    7.87 +        val cmd = make_command generatedN;
    7.88        in
    7.89          if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    7.90          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    7.91 @@ -439,7 +441,7 @@
    7.92  fun evaluator thy target naming program consts =
    7.93    let
    7.94      val (mounted_serializer, prepared_program) = mount_serializer thy
    7.95 -      target NONE "Generated_Code" [] naming program consts;
    7.96 +      target NONE generatedN [] naming program consts;
    7.97    in evaluation mounted_serializer prepared_program consts end;
    7.98  
    7.99  end; (* local *)