# HG changeset patch
# User haftmann
# Date 1393148023 -3600
# Node ID fb46f1c379b549f96484454f7267e196941d14d8
# Parent  ccbf1722ae32a8ef79a7e764818a0cfe35abb082
avoid ad-hoc patching of generated code

diff -r ccbf1722ae32 -r fb46f1c379b5 src/HOL/Quickcheck_Narrowing.thy
--- 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
diff -r ccbf1722ae32 -r fb46f1c379b5 src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- 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 {
diff -r ccbf1722ae32 -r fb46f1c379b5 src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
--- 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 {
diff -r ccbf1722ae32 -r fb46f1c379b5 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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 ^ " " ^