Quickcheck Narrowing only requires one compilation with GHC now
authorbulwahn
Tue May 31 15:45:27 2011 +0200 (2011-05-31)
changeset 43114b9fca691addd
parent 43113 7226051e8b89
child 43115 6773d8a9e351
Quickcheck Narrowing only requires one compilation with GHC now
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue May 31 15:45:26 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue May 31 15:45:27 2011 +0200
     1.3 @@ -6,8 +6,7 @@
     1.4  
     1.5  signature NARROWING_GENERATORS =
     1.6  sig
     1.7 -  val compile_generator_expr:
     1.8 -    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     1.9 +  val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
    1.10    val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    1.11    val finite_functions : bool Config.T
    1.12    val overlord : bool Config.T
    1.13 @@ -197,8 +196,9 @@
    1.14      val _ = Isabelle_System.mkdirs path;
    1.15    in Exn.release (Exn.capture f path) end;
    1.16    
    1.17 -fun value ctxt (get, put, put_ml) (code, value) size =
    1.18 +fun value ctxt (get, put, put_ml) (code, value_name) =
    1.19    let
    1.20 +    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
    1.21      val tmp_prefix = "Quickcheck_Narrowing"
    1.22      val with_tmp_dir =
    1.23        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
    1.24 @@ -208,45 +208,55 @@
    1.25          val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
    1.26          val main_file = Path.append in_path (Path.basic "Main.hs")
    1.27          val main = "module Main where {\n\n" ^
    1.28 +          "import System;\n" ^
    1.29            "import Narrowing_Engine;\n" ^
    1.30            "import Code;\n\n" ^
    1.31 -          "main = Narrowing_Engine.depthCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
    1.32 +          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Code.value ())\n\n" ^
    1.33            "}\n"
    1.34          val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    1.35            (unprefix "module Code where {" code)
    1.36          val _ = File.write code_file code'
    1.37          val _ = File.write narrowing_engine_file narrowing_engine
    1.38          val _ = File.write main_file main
    1.39 -        val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
    1.40 -        val cmd = "( exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
    1.41 +        val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
    1.42 +        val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
    1.43            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.44 -          " -o " ^ executable ^ "; ) && " ^ executable
    1.45 -      in
    1.46 -        bash_output cmd
    1.47 +          " -o " ^ executable ^ ";"
    1.48 +        val _ = if bash cmd <> 0 then
    1.49 +          error "Compilation failed!"
    1.50 +        else
    1.51 +          ()
    1.52 +        fun with_size k =
    1.53 +          if k > Config.get ctxt Quickcheck.size then
    1.54 +            NONE
    1.55 +          else
    1.56 +            let
    1.57 +              val _ = message ("Test data size: " ^ string_of_int k)
    1.58 +              val (response, _) = bash_output (executable ^ " " ^ string_of_int k)
    1.59 +            in
    1.60 +              if response = "NONE\n" then with_size (k + 1) else SOME response
    1.61 +            end
    1.62 +      in case with_size 0 of
    1.63 +           NONE => NONE
    1.64 +         | SOME response =>
    1.65 +           let
    1.66 +             val output_value = the_default "NONE"
    1.67 +               (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
    1.68 +               |> translate_string (fn s => if s = "\\" then "\\\\" else s)
    1.69 +             val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    1.70 +               ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
    1.71 +             val ctxt' = ctxt
    1.72 +               |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.73 +               |> Context.proof_map (exec false ml_code);
    1.74 +           in get ctxt' () end     
    1.75        end
    1.76 -    val result = with_tmp_dir tmp_prefix run
    1.77 -    val output_value = the_default "NONE"
    1.78 -      (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
    1.79 -      |> translate_string (fn s => if s = "\\" then "\\\\" else s)
    1.80 -    val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    1.81 -      ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
    1.82 -    val ctxt' = ctxt
    1.83 -      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.84 -      |> Context.proof_map (exec false ml_code);
    1.85 -  in get ctxt' () end;
    1.86 +  in with_tmp_dir tmp_prefix run end;
    1.87  
    1.88 -fun evaluation cookie thy evaluator vs_t args size =
    1.89 +fun dynamic_value_strict cookie thy postproc t =
    1.90    let
    1.91 -    val ctxt = Proof_Context.init_global thy;
    1.92 -    val (program_code, value_name) = evaluator vs_t;
    1.93 -    val value_code = space_implode " "
    1.94 -      (value_name :: "()" :: map (enclose "(" ")") args);
    1.95 -  in Exn.interruptible_capture (value ctxt cookie (program_code, value_code)) size end;
    1.96 -
    1.97 -fun dynamic_value_strict cookie thy postproc t args size =
    1.98 -  let
    1.99 -    fun evaluator naming program ((_, vs_ty), t) deps =
   1.100 -      evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size;
   1.101 +    val ctxt = Proof_Context.init_global thy
   1.102 +    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value ctxt cookie)
   1.103 +      (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
   1.104    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
   1.105  
   1.106  (** counterexample generator **)
   1.107 @@ -286,7 +296,9 @@
   1.108      list_abs (names ~~ Ts', t'')
   1.109    end
   1.110  
   1.111 -fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
   1.112 +(** tester **)
   1.113 +  
   1.114 +fun test_term  ctxt (limit_time, is_interactive) (t, eval_terms) =
   1.115    let
   1.116      val thy = Proof_Context.theory_of ctxt
   1.117      val t' = list_abs_free (Term.add_frees t [], t)
   1.118 @@ -295,11 +307,22 @@
   1.119        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   1.120      val result = dynamic_value_strict
   1.121        (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   1.122 -      thy (Option.map o map) (ensure_testable t'') [] size
   1.123 +      thy (Option.map o map) (ensure_testable t'')
   1.124    in
   1.125 -    (result, NONE)
   1.126 +    Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
   1.127 +      evaluation_terms = Option.map (K []) result, timings = [], reports = []}
   1.128    end;
   1.129  
   1.130 +fun test_goals ctxt (limit_time, is_interactive) insts goals =
   1.131 +  let
   1.132 +    val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
   1.133 +  in
   1.134 +    if Config.get ctxt Quickcheck.finite_types then
   1.135 +      error "Quickcheck-Narrowing does not support finite_types"
   1.136 +    else
   1.137 +      Quickcheck.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
   1.138 +  end
   1.139 +
   1.140  (* setup *)
   1.141  
   1.142  val setup =
   1.143 @@ -307,7 +330,6 @@
   1.144    #> Code.datatype_interpretation ensure_partial_term_of_code
   1.145    #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   1.146      (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
   1.147 -  #> Context.theory_map
   1.148 -    (Quickcheck.add_generator ("narrowing", compile_generator_expr))
   1.149 +  #> Context.theory_map (Quickcheck.add_tester ("narrowing", test_goals))
   1.150      
   1.151  end;
   1.152 \ No newline at end of file
     2.1 --- a/src/Tools/quickcheck.ML	Tue May 31 15:45:26 2011 +0200
     2.2 +++ b/src/Tools/quickcheck.ML	Tue May 31 15:45:27 2011 +0200
     2.3 @@ -567,7 +567,9 @@
     2.4    | read_expectation "counterexample" = Counterexample
     2.5    | read_expectation s = error ("Not an expectation value: " ^ s)
     2.6  
     2.7 -fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (fst (Data.get genctxt))))
     2.8 +fun valid_tester_name genctxt name =
     2.9 +  AList.defined (op =) (fst (fst (fst (Data.get genctxt)))) name orelse
    2.10 +    AList.defined (op =) (snd (fst (fst (Data.get genctxt)))) name
    2.11  
    2.12  fun parse_tester name genctxt =
    2.13    if valid_tester_name genctxt name then