--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jan 10 12:07:08 2019 +0000
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jan 10 18:38:21 2019 +0100
@@ -236,12 +236,12 @@
fun mk_code_file module =
let
val (paths, base) = split_last module
- in Path.appends (in_path :: map Path.basic (paths @ [base ^ ".hs"])) end;
- val generatedN = Code_Target.generatedN
- val includes = AList.delete (op =) [generatedN] code_modules
+ in Path.appends (in_path :: map Path.basic (paths @ [suffix ".hs" base])) end;
+ val generatedN_suffix = suffix ".hs" Code_Target.generatedN;
+ val includes = AList.delete (op =) [generatedN_suffix] code_modules
|> (map o apfst) mk_code_file
- val code = the (AList.lookup (op =) code_modules [generatedN])
- val code_file = mk_code_file [generatedN]
+ val code = the (AList.lookup (op =) code_modules [generatedN_suffix])
+ val code_file = mk_code_file [Code_Target.generatedN]
val narrowing_engine_file = mk_code_file ["Narrowing_Engine"]
val main_file = mk_code_file ["Main"]
val main =
@@ -249,9 +249,9 @@
"import System.IO;\n" ^
"import System.Environment;\n" ^
"import Narrowing_Engine;\n" ^
- "import " ^ generatedN ^ " ;\n\n" ^
+ "import " ^ Code_Target.generatedN ^ " ;\n\n" ^
"main = getArgs >>= \\[potential, size] -> " ^
- "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^
+ "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ Code_Target.generatedN ^
".value ())\n\n}\n"
val _ =
map (uncurry File.write)