src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 44321 975c9ba50a41
parent 44272 360fcbb1aa01
child 44751 f523923d8182
equal deleted inserted replaced
44320:33439faadd67 44321:975c9ba50a41
   249         val _ = File.write code_file code'
   249         val _ = File.write code_file code'
   250         val _ = File.write narrowing_engine_file
   250         val _ = File.write narrowing_engine_file
   251           (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
   251           (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
   252         val _ = File.write main_file main
   252         val _ = File.write main_file main
   253         val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
   253         val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
   254         val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
   254         val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables " ^
   255           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
   255           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
   256           " -o " ^ executable ^ ";"
   256           " -o " ^ executable ^ ";"
   257         val (result, compilation_time) =
   257         val (result, compilation_time) =
   258           elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
   258           elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
   259         val _ = Quickcheck.add_timing compilation_time current_result
   259         val _ = Quickcheck.add_timing compilation_time current_result