call ghc with -XEmptyDataDecls
authornoschinl
Thu Sep 08 12:23:11 2011 +0200 (2011-09-08)
changeset 448528ac91e7b6024
parent 44851 4bc70ab28787
child 44853 e3310cdb4e48
child 44854 0b3d3570ab31
call ghc with -XEmptyDataDecls
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Tools/Code/code_haskell.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Sep 09 06:47:14 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Sep 08 12:23:11 2011 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4            (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
     1.5          val _ = File.write main_file main
     1.6          val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
     1.7 -        val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables " ^
     1.8 +        val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls " ^
     1.9            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.10            " -o " ^ executable ^ ";"
    1.11          val (result, compilation_time) =
     2.1 --- a/src/Tools/Code/code_haskell.ML	Fri Sep 09 06:47:14 2011 +0200
     2.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Sep 08 12:23:11 2011 +0200
     2.3 @@ -446,7 +446,7 @@
     2.4      (target, { serializer = serializer, literals = literals,
     2.5        check = { env_var = "ISABELLE_GHC", make_destination = I,
     2.6          make_command = fn module_name =>
     2.7 -          "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e \"\" " ^
     2.8 +          "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls -odir build -hidir build -stubdir build -e \"\" " ^
     2.9              module_name ^ ".hs" } })
    2.10    #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    2.11        brackify_infix (1, R) fxy (