--- a/src/HOL/Quickcheck_Narrowing.thy Sat Feb 22 22:06:10 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Sun Feb 23 10:33:43 2014 +0100
@@ -14,8 +14,11 @@
setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *}
code_printing
- type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
-| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
+ code_module Typerep \<rightharpoonup> (Haskell_Quickcheck) {*
+data Typerep = Typerep String [Typerep]
+*}
+| type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
+| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
| type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
code_reserved Haskell_Quickcheck Typerep
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Sat Feb 22 22:06:10 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Sun Feb 23 10:33:43 2014 +0100
@@ -4,6 +4,7 @@
import Control.Exception;
import System.IO;
import System.Exit;
+import qualified Typerep;
import qualified Generated_Code;
type Pos = [Int];
@@ -67,8 +68,8 @@
-- Testable
-instance Show Generated_Code.Typerep where {
- show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
+instance Show Typerep.Typerep where {
+ show (Typerep.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
};
instance Show Generated_Code.Term where {
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Sat Feb 22 22:06:10 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Sun Feb 23 10:33:43 2014 +0100
@@ -10,6 +10,7 @@
import Data.Maybe
import Data.List (partition, findIndex)
import qualified Generated_Code
+import qualified Typerep
type Pos = [Int]
@@ -156,8 +157,8 @@
-- presentation of counterexample
-instance Show Generated_Code.Typerep where {
- show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
+instance Show Typerep.Typerep where {
+ show (Typerep.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
};
instance Show Generated_Code.Term where {
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Feb 22 22:06:10 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Feb 23 10:33:43 2014 +0100
@@ -247,12 +247,9 @@
"main = getArgs >>= \\[potential, size] -> " ^
"Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^
"}\n"
- val code' = code
- |> unsuffix "}\n"
- |> suffix "data Typerep = Typerep String [Typerep];\n\n}\n" (* FIXME *)
val _ = map (uncurry File.write) (includes @
[(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
- (code_file, code'), (main_file, main)])
+ (code_file, code), (main_file, main)])
val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
ghc_options ^ " " ^