restored narrowing quickcheck after 6efff142bb54
authorhaftmann
Fri Jul 27 20:05:56 2012 +0200 (2012-07-27)
changeset 485657c497a239007
parent 48561 12aa0cb2b447
child 48566 6e5702395491
restored narrowing quickcheck after 6efff142bb54
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 27 19:27:21 2012 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 27 20:05:56 2012 +0200
     1.3 @@ -165,7 +165,7 @@
     1.4    false Code_Printer.literal_numeral) ["Haskell_Quickcheck"]  *}
     1.5  
     1.6  code_type code_int
     1.7 -  (Haskell_Quickcheck "Int")
     1.8 +  (Haskell_Quickcheck "Prelude.Int")
     1.9  
    1.10  code_const "0 \<Colon> code_int"
    1.11    (Haskell_Quickcheck "0")
    1.12 @@ -222,7 +222,7 @@
    1.13  
    1.14  consts toEnum :: "code_int => char"
    1.15  
    1.16 -code_const toEnum (Haskell_Quickcheck "toEnum")
    1.17 +code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
    1.18  
    1.19  consts marker :: "char"
    1.20  
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 19:27:21 2012 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 20:05:56 2012 +0200
     2.3 @@ -249,8 +249,9 @@
     2.4            "main = getArgs >>= \\[potential, size] -> " ^
     2.5            "Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
     2.6            "}\n"
     2.7 -        val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
     2.8 -          (unprefix "module Generated_Code where {" code)
     2.9 +        val code' = code
    2.10 +          |> unsuffix "}\n"
    2.11 +          |> suffix "data Typerep = Typerep String [Typerep];\n\n}\n" (* FIXME *)
    2.12          val _ = File.write code_file code'
    2.13          val _ = File.write narrowing_engine_file
    2.14            (if contains_existentials then pnf_narrowing_engine else narrowing_engine)