src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 48568 084cd758a8ab
parent 48565 7c497a239007
child 48901 5e0455e29339
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 21:57:56 2012 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 22:26:38 2012 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4    let val ({elapsed, ...}, result) = Timing.timing e ()
     1.5    in (result, (description, Time.toMilliseconds elapsed)) end
     1.6    
     1.7 -fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code, value_name) =
     1.8 +fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, value_name) =
     1.9    let
    1.10      val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
    1.11      fun message s = if quiet then () else Output.urgent_message s
    1.12 @@ -238,31 +238,34 @@
    1.13        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
    1.14      fun run in_path = 
    1.15        let
    1.16 -        val code_file = Path.append in_path (Path.basic "Generated_Code.hs")
    1.17 -        val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
    1.18 -        val main_file = Path.append in_path (Path.basic "Main.hs")
    1.19 +        fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
    1.20 +        val generatedN = Code_Target.generatedN
    1.21 +        val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file;
    1.22 +        val code = the (AList.lookup (op =) code_modules generatedN)
    1.23 +        val code_file = mk_code_file generatedN
    1.24 +        val narrowing_engine_file = mk_code_file "Narrowing_Engine"
    1.25 +        val main_file = mk_code_file "Main"
    1.26          val main = "module Main where {\n\n" ^
    1.27            "import System.IO;\n" ^
    1.28            "import System.Environment;\n" ^
    1.29            "import Narrowing_Engine;\n" ^
    1.30 -          "import Generated_Code;\n\n" ^
    1.31 +          "import " ^ generatedN ^ " ;\n\n" ^
    1.32            "main = getArgs >>= \\[potential, size] -> " ^
    1.33 -          "Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
    1.34 +          "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^
    1.35            "}\n"
    1.36          val code' = code
    1.37            |> unsuffix "}\n"
    1.38            |> suffix "data Typerep = Typerep String [Typerep];\n\n}\n" (* FIXME *)
    1.39 -        val _ = File.write code_file code'
    1.40 -        val _ = File.write narrowing_engine_file
    1.41 -          (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
    1.42 -        val _ = File.write main_file main
    1.43 +        val _ = map (uncurry File.write) (includes @
    1.44 +          [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
    1.45 +           (code_file, code'), (main_file, main)])
    1.46          val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
    1.47          val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
    1.48            ghc_options ^ " " ^
    1.49 -          (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.50 +          (space_implode " " (map File.shell_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
    1.51            " -o " ^ executable ^ ";"
    1.52          val (result, compilation_time) =
    1.53 -          elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
    1.54 +          elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
    1.55          val _ = Quickcheck.add_timing compilation_time current_result
    1.56          fun haskell_string_of_bool v = if v then "True" else "False"
    1.57          val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
    1.58 @@ -314,7 +317,7 @@
    1.59      val ctxt = Proof_Context.init_global thy
    1.60      fun evaluator naming program ((_, vs_ty), t) deps =
    1.61        Exn.interruptible_capture (value opts ctxt cookie)
    1.62 -        (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
    1.63 +        (Code_Target.evaluator thy target naming program deps (vs_ty, t));
    1.64    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    1.65  
    1.66  (** counterexample generator **)