# HG changeset patch # User haftmann # Date 1513273359 -3600 # Node ID ad538f6c5d2fcff2db8284dd9998de1e033c47d4 # Parent b8f30228a55b272cacb541f0472b1cfbbb70e12e dedicated case option for code generation to Scala diff -r b8f30228a55b -r ad538f6c5d2f NEWS --- 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 *** diff -r b8f30228a55b -r ad538f6c5d2f src/Doc/Codegen/Further.thy --- 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 + ``\(case_insensitive)\'' option for @{command export_code}. \ diff -r b8f30228a55b -r ad538f6c5d2f src/Doc/Isar_Ref/HOL_Specific.thy --- 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>\Haskell\ a module name prefix may be given using the ``\root:\'' argument; - ``\string_classes\'' adds a ``\<^verbatim>\deriving (Read, Show)\'' clause to each - appropriate datatype declaration. + Serializers take an optional list of arguments in parentheses. + + For \<^emph>\Haskell\ a module name prefix may be given using the ``\root:\'' + argument; ``\string_classes\'' adds a ``\<^verbatim>\deriving (Read, Show)\'' clause + to each appropriate datatype declaration. + + For \<^emph>\Scala\, ``\case_insensitive\'' avoids name clashes on + case-insensitive file systems. \<^descr> @{attribute (HOL) code} declare code equations for code generation. Variant \code equation\ declares a conventional equation as code equation. diff -r b8f30228a55b -r ad538f6c5d2f src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- 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" diff -r b8f30228a55b -r ad538f6c5d2f src/Tools/Code/code_haskell.ML --- 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 ( diff -r b8f30228a55b -r ad538f6c5d2f src/Tools/Code/code_ml.ML --- 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 diff -r b8f30228a55b -r ad538f6c5d2f src/Tools/Code/code_scala.ML --- 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 ( diff -r b8f30228a55b -r ad538f6c5d2f src/Tools/Code/code_target.ML --- 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