compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
authorbulwahn
Thu Jun 09 08:32:13 2011 +0200 (2011-06-09)
changeset 43308fd6cc1378fec
parent 43307 1a32a953cef1
child 43309 3bc28ce6986c
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
src/HOL/Library/Quickcheck_Narrowing.thy
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Library/Quickcheck_Narrowing.thy	Thu Jun 09 08:31:41 2011 +0200
     1.2 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:13 2011 +0200
     1.3 @@ -12,17 +12,21 @@
     1.4  
     1.5  subsection {* Counterexample generator *}
     1.6  
     1.7 +text {* We create a new target for the necessary code generation setup. *}
     1.8 +
     1.9 +setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
    1.10 +
    1.11  subsubsection {* Code generation setup *}
    1.12  
    1.13  code_type typerep
    1.14 -  ("Haskell" "Typerep")
    1.15 +  (Haskell_Quickcheck "Typerep")
    1.16  
    1.17  code_const Typerep.Typerep
    1.18 -  ("Haskell" "Typerep")
    1.19 +  (Haskell_Quickcheck "Typerep")
    1.20  
    1.21 -code_reserved Haskell Typerep
    1.22 +code_reserved Haskell_Quickcheck Typerep
    1.23  
    1.24 -subsubsection {* Type @{text "code_int"} for Haskell's Int type *}
    1.25 +subsubsection {* Type @{text "code_int"} for Haskell_Quickcheck's Int type *}
    1.26  
    1.27  typedef (open) code_int = "UNIV \<Colon> int set"
    1.28    morphisms int_of of_int by rule
    1.29 @@ -169,34 +173,34 @@
    1.30  
    1.31  
    1.32  code_instance code_numeral :: equal
    1.33 -  (Haskell -)
    1.34 +  (Haskell_Quickcheck -)
    1.35  
    1.36  setup {* fold (Numeral.add_code @{const_name number_code_int_inst.number_of_code_int}
    1.37 -  false Code_Printer.literal_numeral) ["Haskell"]  *}
    1.38 +  false Code_Printer.literal_numeral) ["Haskell_Quickcheck"]  *}
    1.39  
    1.40  code_const "0 \<Colon> code_int"
    1.41 -  (Haskell "0")
    1.42 +  (Haskell_Quickcheck "0")
    1.43  
    1.44  code_const "1 \<Colon> code_int"
    1.45 -  (Haskell "1")
    1.46 +  (Haskell_Quickcheck "1")
    1.47  
    1.48  code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
    1.49 -  (Haskell "(_/ -/ _)")
    1.50 +  (Haskell_Quickcheck "(_/ -/ _)")
    1.51  
    1.52  code_const div_mod_code_int
    1.53 -  (Haskell "divMod")
    1.54 +  (Haskell_Quickcheck "divMod")
    1.55  
    1.56  code_const "HOL.equal \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
    1.57 -  (Haskell infix 4 "==")
    1.58 +  (Haskell_Quickcheck infix 4 "==")
    1.59  
    1.60  code_const "op \<le> \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
    1.61 -  (Haskell infix 4 "<=")
    1.62 +  (Haskell_Quickcheck infix 4 "<=")
    1.63  
    1.64  code_const "op < \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
    1.65 -  (Haskell infix 4 "<")
    1.66 +  (Haskell_Quickcheck infix 4 "<")
    1.67  
    1.68  code_type code_int
    1.69 -  (Haskell "Int")
    1.70 +  (Haskell_Quickcheck "Int")
    1.71  
    1.72  code_abort of_int
    1.73  
    1.74 @@ -220,15 +224,15 @@
    1.75  
    1.76  consts nth :: "'a list => code_int => 'a"
    1.77  
    1.78 -code_const nth ("Haskell" infixl 9  "!!")
    1.79 +code_const nth (Haskell_Quickcheck infixl 9  "!!")
    1.80  
    1.81  consts error :: "char list => 'a"
    1.82  
    1.83 -code_const error ("Haskell" "error")
    1.84 +code_const error (Haskell_Quickcheck "error")
    1.85  
    1.86  consts toEnum :: "code_int => char"
    1.87  
    1.88 -code_const toEnum ("Haskell" "toEnum")
    1.89 +code_const toEnum (Haskell_Quickcheck "toEnum")
    1.90  
    1.91  consts map_index :: "(code_int * 'a => 'b) => 'a list => 'b list"  
    1.92  
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 08:31:41 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 08:32:13 2011 +0200
     2.3 @@ -194,7 +194,7 @@
     2.4  
     2.5  (* testing framework *)
     2.6  
     2.7 -val target = "Haskell"
     2.8 +val target = "Haskell_Quickcheck"
     2.9  
    2.10  (** invocation of Haskell interpreter **)
    2.11  
    2.12 @@ -210,9 +210,9 @@
    2.13      val _ = Isabelle_System.mkdirs path;
    2.14    in Exn.release (Exn.capture f path) end;
    2.15    
    2.16 -fun value contains_existentials ctxt (get, put, put_ml) (code, value_name) =
    2.17 +fun value (contains_existentials, (quiet, size)) ctxt (get, put, put_ml) (code, value_name) =
    2.18    let
    2.19 -    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
    2.20 +    fun message s = if quiet then () else Output.urgent_message s
    2.21      val tmp_prefix = "Quickcheck_Narrowing"
    2.22      val with_tmp_dir =
    2.23        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
    2.24 @@ -239,7 +239,7 @@
    2.25            " -o " ^ executable ^ ";"
    2.26          val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
    2.27          fun with_size k =
    2.28 -          if k > Config.get ctxt Quickcheck.size then
    2.29 +          if k > size then
    2.30              NONE
    2.31            else
    2.32              let
    2.33 @@ -264,10 +264,10 @@
    2.34        end
    2.35    in with_tmp_dir tmp_prefix run end;
    2.36  
    2.37 -fun dynamic_value_strict contains_existentials cookie thy postproc t =
    2.38 +fun dynamic_value_strict opts cookie thy postproc t =
    2.39    let
    2.40      val ctxt = Proof_Context.init_global thy
    2.41 -    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value contains_existentials ctxt cookie)
    2.42 +    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value opts ctxt cookie)
    2.43        (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
    2.44    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    2.45  
    2.46 @@ -373,6 +373,7 @@
    2.47    
    2.48  fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
    2.49    let
    2.50 +    val opts = (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
    2.51      val thy = Proof_Context.theory_of ctxt
    2.52      val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
    2.53      val pnf_t = make_pnf_term thy t'
    2.54 @@ -388,7 +389,7 @@
    2.55          val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
    2.56            ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
    2.57          val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
    2.58 -        val result = dynamic_value_strict true
    2.59 +        val result = dynamic_value_strict (true, opts)
    2.60            (Existential_Counterexample.get, Existential_Counterexample.put,
    2.61              "Narrowing_Generators.put_existential_counterexample")
    2.62            thy' (Option.map o map_counterexample) (mk_property qs prop_def')
    2.63 @@ -404,7 +405,7 @@
    2.64          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
    2.65          fun ensure_testable t =
    2.66            Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    2.67 -        val result = dynamic_value_strict false
    2.68 +        val result = dynamic_value_strict (false, opts)
    2.69            (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    2.70            thy (Option.map o map) (ensure_testable (finitize t'))
    2.71        in