--- a/NEWS Thu Dec 14 21:40:43 2017 +0100
+++ b/NEWS Thu Dec 14 18:42:39 2017 +0100
@@ -127,6 +127,9 @@
* Predicate coprime is now a real definition, not a mere
abbreviation. INCOMPATIBILITY.
+* Code generation: Code generation takes an explicit option
+"case_insensitive" to accomodate case-insensitive file systems.
+
*** System ***
--- a/src/Doc/Codegen/Further.thy Thu Dec 14 21:40:43 2017 +0100
+++ b/src/Doc/Codegen/Further.thy Thu Dec 14 18:42:39 2017 +0100
@@ -90,6 +90,10 @@
the type arguments are just appended. Otherwise they are ignored;
hence user-defined adaptations for polymorphic constants have to be
designed very carefully to avoid ambiguity.
+
+ Note also that name clashes can occur when generating Scala code
+ to case-insensitive file systems; these can be avoid using the
+ ``\<open>(case_insensitive)\<close>'' option for @{command export_code}.
\<close>
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Dec 14 21:40:43 2017 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Dec 14 18:42:39 2017 +0100
@@ -2405,10 +2405,14 @@
generated in multiple files reflecting the module hierarchy. Omitting the
file specification denotes standard output.
- Serializers take an optional list of arguments in parentheses. For
- \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' argument;
- ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause to each
- appropriate datatype declaration.
+ Serializers take an optional list of arguments in parentheses.
+
+ For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>''
+ argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause
+ to each appropriate datatype declaration.
+
+ For \<^emph>\<open>Scala\<close>, ``\<open>case_insensitive\<close>'' avoids name clashes on
+ case-insensitive file systems.
\<^descr> @{attribute (HOL) code} declare code equations for code generation.
Variant \<open>code equation\<close> declares a conventional equation as code equation.
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Thu Dec 14 21:40:43 2017 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Thu Dec 14 18:42:39 2017 +0100
@@ -6,8 +6,6 @@
theory Code_Test_Scala imports "HOL-Library.Code_Test" begin
-declare [[scala_case_insensitive]]
-
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
value [Scala] "14 + 7 * -12 :: integer"
--- a/src/Tools/Code/code_haskell.ML Thu Dec 14 21:40:43 2017 +0100
+++ b/src/Tools/Code/code_haskell.ML Thu Dec 14 18:42:39 2017 +0100
@@ -494,11 +494,12 @@
val _ = Theory.setup
(Code_Target.add_language
- (target, { serializer = serializer, literals = literals,
+ (target, {serializer = serializer, literals = literals,
check = { env_var = "ISABELLE_GHC", make_destination = I,
make_command = fn module_name =>
"\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^
- module_name ^ ".hs" } })
+ module_name ^ ".hs"},
+ evaluation_args = []})
#> Code_Target.set_printings (Type_Constructor ("fun",
[(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_ml.ML Thu Dec 14 21:40:43 2017 +0100
+++ b/src/Tools/Code/code_ml.ML Thu Dec 14 18:42:39 2017 +0100
@@ -872,16 +872,18 @@
val _ = Theory.setup
(Code_Target.add_language
- (target_SML, { serializer = serializer_sml, literals = literals_sml,
- check = { env_var = "",
+ (target_SML, {serializer = serializer_sml, literals = literals_sml,
+ check = {env_var = "",
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn _ =>
- "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure" } })
+ "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure"},
+ evaluation_args = []})
#> Code_Target.add_language
- (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
- check = { env_var = "ISABELLE_OCAML",
+ (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
+ check = {env_var = "ISABELLE_OCAML",
make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
- make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
+ make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml"},
+ evaluation_args = []})
#> Code_Target.set_printings (Type_Constructor ("fun",
[(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
--- a/src/Tools/Code/code_scala.ML Thu Dec 14 21:40:43 2017 +0100
+++ b/src/Tools/Code/code_scala.ML Thu Dec 14 18:42:39 2017 +0100
@@ -7,7 +7,6 @@
signature CODE_SCALA =
sig
val target: string
- val case_insensitive: bool Config.T;
end;
structure Code_Scala : CODE_SCALA =
@@ -20,11 +19,6 @@
infixr 5 @@;
infixr 5 @|;
-(** preliminary: option to circumvent clashes on case-insensitive file systems **)
-
-val case_insensitive = Attrib.setup_config_bool @{binding "scala_case_insensitive"} (K false);
-
-
(** Scala serializer **)
val target = "Scala";
@@ -339,9 +333,9 @@
| _ => I) program;
in Symtab.lookup_list tab end;
-fun scala_program_of_program ctxt module_name reserved identifiers exports program =
+fun scala_program_of_program ctxt case_insensitive module_name reserved identifiers exports program =
let
- val variant = if Config.get ctxt case_insensitive
+ val variant = if case_insensitive
then Code_Namespace.variant_case_insensitive
else Name.variant;
fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
@@ -389,13 +383,13 @@
exports program
end;
-fun serialize_scala ctxt { module_name, reserved_syms, identifiers,
+fun serialize_scala case_insensitive ctxt { module_name, reserved_syms, identifiers,
includes, class_syntax, tyco_syntax, const_syntax } exports program =
let
(* build program *)
val { deresolver, hierarchical_program = scala_program } =
- scala_program_of_program ctxt module_name (Name.make_context reserved_syms)
+ scala_program_of_program ctxt case_insensitive module_name (Name.make_context reserved_syms)
identifiers exports program;
(* print statements *)
@@ -434,7 +428,8 @@
end;
val serializer : Code_Target.serializer =
- Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
+ Code_Target.parse_args (Scan.optional (Args.$$$ "case_insensitive" >> K true) false
+ >> (fn case_insensitive => serialize_scala case_insensitive));
val literals = let
fun char_scala c = if c = "'" then "\\'"
@@ -464,7 +459,8 @@
check = { env_var = "SCALA_HOME",
make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
make_command = fn _ =>
- "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala" } })
+ "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"},
+ evaluation_args = Token.explode Keyword.empty_keywords @{here} "case_insensitive"})
#> Code_Target.set_printings (Type_Constructor ("fun",
[(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_target.ML Thu Dec 14 21:40:43 2017 +0100
+++ b/src/Tools/Code/code_target.ML Thu Dec 14 18:42:39 2017 +0100
@@ -178,14 +178,15 @@
(** theory data **)
-type language = { serializer: serializer, literals: literals,
- check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } };
+type language = {serializer: serializer, literals: literals,
+ check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string},
+ evaluation_args: Token.T list};
type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list;
val merge_ancestry : ancestry * ancestry -> ancestry = AList.join (op =) (K snd);
-type target = { serial: serial, language: language, ancestry: ancestry };
+type target = {serial: serial, language: language, ancestry: ancestry};
structure Targets = Theory_Data
(
@@ -195,7 +196,7 @@
fun merge (targets1, targets2) : T =
Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
if #serial target1 = #serial target2 then
- ({ serial = #serial target1, language = #language target1,
+ ({serial = #serial target1, language = #language target1,
ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
Code_Printer.merge_data (data1, data2))
else error ("Incompatible targets: " ^ quote target_name)
@@ -234,7 +235,8 @@
end;
fun add_language (target_name, language) =
- allocate_target target_name { serial = serial (), language = language, ancestry = [] };
+ allocate_target target_name {serial = serial (), language = language,
+ ancestry = []};
fun add_derived_target (target_name, initial_ancestry) thy =
let
@@ -251,8 +253,8 @@
val ancestry = fold1 (fn ancestry' => fn ancestry =>
merge_ancestry (ancestry, ancestry')) ancestries;
in
- allocate_target target_name { serial = #serial supremum, language = #language supremum,
- ancestry = ancestry } thy
+ allocate_target target_name {serial = #serial supremum, language = #language supremum,
+ ancestry = ancestry} thy
end;
fun map_data target_name f thy =
@@ -285,6 +287,8 @@
fun the_literals ctxt = #literals o the_language ctxt;
+fun the_evaluation_args ctxt = #evaluation_args o the_language ctxt;
+
local
fun activate_target ctxt target_name =
@@ -421,8 +425,9 @@
fun compilation_text' ctxt target_name some_module_name program syms =
let
+ val evaluation_args = the_evaluation_args ctxt target_name;
val (mounted_serializer, (_, prepared_program)) =
- mount_serializer ctxt target_name NONE (the_default generatedN some_module_name) [] program syms;
+ mount_serializer ctxt target_name NONE (the_default generatedN some_module_name) evaluation_args program syms;
in
Code_Preproc.timed_exec "serializing"
(fn () => dynamic_compilation_text mounted_serializer prepared_program syms) ctxt