compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
--- a/src/HOL/Library/Quickcheck_Narrowing.thy Thu Jun 09 08:31:41 2011 +0200
+++ b/src/HOL/Library/Quickcheck_Narrowing.thy Thu Jun 09 08:32:13 2011 +0200
@@ -12,17 +12,21 @@
subsection {* Counterexample generator *}
+text {* We create a new target for the necessary code generation setup. *}
+
+setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
+
subsubsection {* Code generation setup *}
code_type typerep
- ("Haskell" "Typerep")
+ (Haskell_Quickcheck "Typerep")
code_const Typerep.Typerep
- ("Haskell" "Typerep")
+ (Haskell_Quickcheck "Typerep")
-code_reserved Haskell Typerep
+code_reserved Haskell_Quickcheck Typerep
-subsubsection {* Type @{text "code_int"} for Haskell's Int type *}
+subsubsection {* Type @{text "code_int"} for Haskell_Quickcheck's Int type *}
typedef (open) code_int = "UNIV \<Colon> int set"
morphisms int_of of_int by rule
@@ -169,34 +173,34 @@
code_instance code_numeral :: equal
- (Haskell -)
+ (Haskell_Quickcheck -)
setup {* fold (Numeral.add_code @{const_name number_code_int_inst.number_of_code_int}
- false Code_Printer.literal_numeral) ["Haskell"] *}
+ false Code_Printer.literal_numeral) ["Haskell_Quickcheck"] *}
code_const "0 \<Colon> code_int"
- (Haskell "0")
+ (Haskell_Quickcheck "0")
code_const "1 \<Colon> code_int"
- (Haskell "1")
+ (Haskell_Quickcheck "1")
code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
- (Haskell "(_/ -/ _)")
+ (Haskell_Quickcheck "(_/ -/ _)")
code_const div_mod_code_int
- (Haskell "divMod")
+ (Haskell_Quickcheck "divMod")
code_const "HOL.equal \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
- (Haskell infix 4 "==")
+ (Haskell_Quickcheck infix 4 "==")
code_const "op \<le> \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
- (Haskell infix 4 "<=")
+ (Haskell_Quickcheck infix 4 "<=")
code_const "op < \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
- (Haskell infix 4 "<")
+ (Haskell_Quickcheck infix 4 "<")
code_type code_int
- (Haskell "Int")
+ (Haskell_Quickcheck "Int")
code_abort of_int
@@ -220,15 +224,15 @@
consts nth :: "'a list => code_int => 'a"
-code_const nth ("Haskell" infixl 9 "!!")
+code_const nth (Haskell_Quickcheck infixl 9 "!!")
consts error :: "char list => 'a"
-code_const error ("Haskell" "error")
+code_const error (Haskell_Quickcheck "error")
consts toEnum :: "code_int => char"
-code_const toEnum ("Haskell" "toEnum")
+code_const toEnum (Haskell_Quickcheck "toEnum")
consts map_index :: "(code_int * 'a => 'b) => 'a list => 'b list"
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 09 08:31:41 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 09 08:32:13 2011 +0200
@@ -194,7 +194,7 @@
(* testing framework *)
-val target = "Haskell"
+val target = "Haskell_Quickcheck"
(** invocation of Haskell interpreter **)
@@ -210,9 +210,9 @@
val _ = Isabelle_System.mkdirs path;
in Exn.release (Exn.capture f path) end;
-fun value contains_existentials ctxt (get, put, put_ml) (code, value_name) =
+fun value (contains_existentials, (quiet, size)) ctxt (get, put, put_ml) (code, value_name) =
let
- fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
+ fun message s = if quiet then () else Output.urgent_message s
val tmp_prefix = "Quickcheck_Narrowing"
val with_tmp_dir =
if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir
@@ -239,7 +239,7 @@
" -o " ^ executable ^ ";"
val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
fun with_size k =
- if k > Config.get ctxt Quickcheck.size then
+ if k > size then
NONE
else
let
@@ -264,10 +264,10 @@
end
in with_tmp_dir tmp_prefix run end;
-fun dynamic_value_strict contains_existentials cookie thy postproc t =
+fun dynamic_value_strict opts cookie thy postproc t =
let
val ctxt = Proof_Context.init_global thy
- fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value contains_existentials ctxt cookie)
+ 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));
in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
@@ -373,6 +373,7 @@
fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
let
+ val opts = (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
val thy = Proof_Context.theory_of ctxt
val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
val pnf_t = make_pnf_term thy t'
@@ -388,7 +389,7 @@
val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt')
- val result = dynamic_value_strict true
+ val result = dynamic_value_strict (true, opts)
(Existential_Counterexample.get, Existential_Counterexample.put,
"Narrowing_Generators.put_existential_counterexample")
thy' (Option.map o map_counterexample) (mk_property qs prop_def')
@@ -404,7 +405,7 @@
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
fun ensure_testable t =
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
- val result = dynamic_value_strict false
+ val result = dynamic_value_strict (false, opts)
(Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
thy (Option.map o map) (ensure_testable (finitize t'))
in