src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42090 ef566ce50170
parent 42039 cef738d55348
child 42159 234ec7011e5d
equal deleted inserted replaced
42089:904897d0c5bd 42090:ef566ce50170
   134         val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
   134         val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
   135         val main_file = Path.append in_path (Path.basic "Main.hs")
   135         val main_file = Path.append in_path (Path.basic "Main.hs")
   136         val main = "module Main where {\n\n" ^
   136         val main = "module Main where {\n\n" ^
   137           "import Narrowing_Engine;\n" ^
   137           "import Narrowing_Engine;\n" ^
   138           "import Code;\n\n" ^
   138           "import Code;\n\n" ^
   139           "main = Narrowing_Engine.smallCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
   139           "main = Narrowing_Engine.depthCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
   140           "}\n"
   140           "}\n"
   141         val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
   141         val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
   142           (unprefix "module Code where {" code)
   142           (unprefix "module Code where {" code)
   143         val _ = File.write code_file code'
   143         val _ = File.write code_file code'
   144         val _ = File.write narrowing_engine_file narrowing_engine
   144         val _ = File.write narrowing_engine_file narrowing_engine