# HG changeset patch # User noschinl # Date 1315988662 -7200 # Node ID de3ed037c9a5be80c98e3604205db231b44789d6 # Parent 1a5811bfe837ea4eb2184499ee24695b3897b4be create central list for language extensions used by the haskell code generator diff -r 1a5811bfe837 -r de3ed037c9a5 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Sep 14 06:49:24 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Sep 14 10:24:22 2011 +0200 @@ -251,7 +251,7 @@ (if contains_existentials then pnf_narrowing_engine else narrowing_engine) val _ = File.write main_file main val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing")) - val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls " ^ + val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^ " -o " ^ executable ^ ";" val (result, compilation_time) = diff -r 1a5811bfe837 -r de3ed037c9a5 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Wed Sep 14 06:49:24 2011 +0200 +++ b/src/Tools/Code/code_haskell.ML Wed Sep 14 10:24:22 2011 +0200 @@ -6,6 +6,7 @@ signature CODE_HASKELL = sig + val language_params: string val target: string val setup: theory -> theory end; @@ -15,6 +16,15 @@ val target = "Haskell"; +val language_extensions = + ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"]; + +val language_pragma = + "{-# LANGUAGE " ^ commas language_extensions ^ " #-}"; + +val language_params = + space_implode " " (map (prefix "-X") language_extensions); + open Basic_Code_Thingol; open Code_Printer; @@ -348,7 +358,7 @@ val _ = Isabelle_System.mkdirs (Path.dir filepath); in (File.write filepath o format [] width o Pretty.chunks2) - [str "{-# LANGUAGE ScopedTypeVariables #-}", content] + [str language_pragma, content] end | write_module width NONE (_, content) = writeln (format [] width content); in @@ -446,7 +456,7 @@ (target, { serializer = serializer, literals = literals, check = { env_var = "ISABELLE_GHC", make_destination = I, make_command = fn module_name => - "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls -odir build -hidir build -stubdir build -e \"\" " ^ + "\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } }) #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => brackify_infix (1, R) fxy (