dedicated case option for code generation to Scala
authorhaftmann
Thu Dec 14 18:42:39 2017 +0100 (17 months ago)
changeset 67207ad538f6c5d2f
parent 67206 b8f30228a55b
child 67208 16519cd83ed4
dedicated case option for code generation to Scala
NEWS
src/Doc/Codegen/Further.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/HOL/Codegenerator_Test/Code_Test_Scala.thy
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/NEWS	Thu Dec 14 21:40:43 2017 +0100
     1.2 +++ b/NEWS	Thu Dec 14 18:42:39 2017 +0100
     1.3 @@ -127,6 +127,9 @@
     1.4  * Predicate coprime is now a real definition, not a mere
     1.5  abbreviation. INCOMPATIBILITY.
     1.6  
     1.7 +* Code generation: Code generation takes an explicit option
     1.8 +"case_insensitive" to accomodate case-insensitive file systems.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/Doc/Codegen/Further.thy	Thu Dec 14 21:40:43 2017 +0100
     2.2 +++ b/src/Doc/Codegen/Further.thy	Thu Dec 14 18:42:39 2017 +0100
     2.3 @@ -90,6 +90,10 @@
     2.4    the type arguments are just appended.  Otherwise they are ignored;
     2.5    hence user-defined adaptations for polymorphic constants have to be
     2.6    designed very carefully to avoid ambiguity.
     2.7 +
     2.8 +  Note also that name clashes can occur when generating Scala code
     2.9 +  to case-insensitive file systems; these can be avoid using the
    2.10 +  ``\<open>(case_insensitive)\<close>'' option for @{command export_code}.
    2.11  \<close>
    2.12  
    2.13  
     3.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Dec 14 21:40:43 2017 +0100
     3.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Dec 14 18:42:39 2017 +0100
     3.3 @@ -2405,10 +2405,14 @@
     3.4    generated in multiple files reflecting the module hierarchy. Omitting the
     3.5    file specification denotes standard output.
     3.6  
     3.7 -  Serializers take an optional list of arguments in parentheses. For
     3.8 -  \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' argument;
     3.9 -  ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause to each
    3.10 -  appropriate datatype declaration.
    3.11 +  Serializers take an optional list of arguments in parentheses.
    3.12 +
    3.13 +  For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>''
    3.14 +  argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause 
    3.15 +  to each appropriate datatype declaration.
    3.16 +
    3.17 +  For \<^emph>\<open>Scala\<close>, ``\<open>case_insensitive\<close>'' avoids name clashes on
    3.18 +  case-insensitive file systems.
    3.19  
    3.20    \<^descr> @{attribute (HOL) code} declare code equations for code generation.
    3.21    Variant \<open>code equation\<close> declares a conventional equation as code equation.
     4.1 --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Thu Dec 14 21:40:43 2017 +0100
     4.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Thu Dec 14 18:42:39 2017 +0100
     4.3 @@ -6,8 +6,6 @@
     4.4  
     4.5  theory Code_Test_Scala imports  "HOL-Library.Code_Test" begin
     4.6  
     4.7 -declare [[scala_case_insensitive]]
     4.8 -
     4.9  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
    4.10  
    4.11  value [Scala] "14 + 7 * -12 :: integer"
     5.1 --- a/src/Tools/Code/code_haskell.ML	Thu Dec 14 21:40:43 2017 +0100
     5.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Dec 14 18:42:39 2017 +0100
     5.3 @@ -494,11 +494,12 @@
     5.4  
     5.5  val _ = Theory.setup
     5.6    (Code_Target.add_language
     5.7 -    (target, { serializer = serializer, literals = literals,
     5.8 +    (target, {serializer = serializer, literals = literals,
     5.9        check = { env_var = "ISABELLE_GHC", make_destination = I,
    5.10          make_command = fn module_name =>
    5.11            "\"$ISABELLE_GHC\" " ^ language_params  ^ " -odir build -hidir build -stubdir build -e \"\" " ^
    5.12 -            module_name ^ ".hs" } })
    5.13 +            module_name ^ ".hs"},
    5.14 +      evaluation_args = []})
    5.15    #> Code_Target.set_printings (Type_Constructor ("fun",
    5.16      [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    5.17        brackify_infix (1, R) fxy (
     6.1 --- a/src/Tools/Code/code_ml.ML	Thu Dec 14 21:40:43 2017 +0100
     6.2 +++ b/src/Tools/Code/code_ml.ML	Thu Dec 14 18:42:39 2017 +0100
     6.3 @@ -872,16 +872,18 @@
     6.4  
     6.5  val _ = Theory.setup
     6.6    (Code_Target.add_language
     6.7 -    (target_SML, { serializer = serializer_sml, literals = literals_sml,
     6.8 -      check = { env_var = "",
     6.9 +    (target_SML, {serializer = serializer_sml, literals = literals_sml,
    6.10 +      check = {env_var = "",
    6.11          make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
    6.12          make_command = fn _ =>
    6.13 -          "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure" } })
    6.14 +          "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure"},
    6.15 +      evaluation_args = []})
    6.16    #> Code_Target.add_language
    6.17 -    (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
    6.18 -      check = { env_var = "ISABELLE_OCAML",
    6.19 +    (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
    6.20 +      check = {env_var = "ISABELLE_OCAML",
    6.21          make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
    6.22 -        make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
    6.23 +        make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml"},
    6.24 +      evaluation_args = []})
    6.25    #> Code_Target.set_printings (Type_Constructor ("fun",
    6.26      [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
    6.27    #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
     7.1 --- a/src/Tools/Code/code_scala.ML	Thu Dec 14 21:40:43 2017 +0100
     7.2 +++ b/src/Tools/Code/code_scala.ML	Thu Dec 14 18:42:39 2017 +0100
     7.3 @@ -7,7 +7,6 @@
     7.4  signature CODE_SCALA =
     7.5  sig
     7.6    val target: string
     7.7 -  val case_insensitive: bool Config.T;
     7.8  end;
     7.9  
    7.10  structure Code_Scala : CODE_SCALA =
    7.11 @@ -20,11 +19,6 @@
    7.12  infixr 5 @@;
    7.13  infixr 5 @|;
    7.14  
    7.15 -(** preliminary: option to circumvent clashes on case-insensitive file systems **)
    7.16 -
    7.17 -val case_insensitive = Attrib.setup_config_bool @{binding "scala_case_insensitive"} (K false);
    7.18 -
    7.19 -
    7.20  (** Scala serializer **)
    7.21  
    7.22  val target = "Scala";
    7.23 @@ -339,9 +333,9 @@
    7.24             | _ => I) program;
    7.25    in Symtab.lookup_list tab end;
    7.26  
    7.27 -fun scala_program_of_program ctxt module_name reserved identifiers exports program =
    7.28 +fun scala_program_of_program ctxt case_insensitive module_name reserved identifiers exports program =
    7.29    let
    7.30 -    val variant = if Config.get ctxt case_insensitive
    7.31 +    val variant = if case_insensitive
    7.32        then Code_Namespace.variant_case_insensitive
    7.33        else Name.variant;
    7.34      fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
    7.35 @@ -389,13 +383,13 @@
    7.36        exports program
    7.37    end;
    7.38  
    7.39 -fun serialize_scala ctxt { module_name, reserved_syms, identifiers,
    7.40 +fun serialize_scala case_insensitive ctxt { module_name, reserved_syms, identifiers,
    7.41      includes, class_syntax, tyco_syntax, const_syntax } exports program =
    7.42    let
    7.43  
    7.44      (* build program *)
    7.45      val { deresolver, hierarchical_program = scala_program } =
    7.46 -      scala_program_of_program ctxt module_name (Name.make_context reserved_syms)
    7.47 +      scala_program_of_program ctxt case_insensitive module_name (Name.make_context reserved_syms)
    7.48          identifiers exports program;
    7.49  
    7.50      (* print statements *)
    7.51 @@ -434,7 +428,8 @@
    7.52    end;
    7.53  
    7.54  val serializer : Code_Target.serializer =
    7.55 -  Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
    7.56 +  Code_Target.parse_args (Scan.optional (Args.$$$ "case_insensitive" >> K true) false
    7.57 +    >> (fn case_insensitive => serialize_scala case_insensitive));
    7.58  
    7.59  val literals = let
    7.60    fun char_scala c = if c = "'" then "\\'"
    7.61 @@ -464,7 +459,8 @@
    7.62        check = { env_var = "SCALA_HOME",
    7.63          make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
    7.64          make_command = fn _ =>
    7.65 -          "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala" } })
    7.66 +          "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"},
    7.67 +      evaluation_args = Token.explode Keyword.empty_keywords @{here} "case_insensitive"})
    7.68    #> Code_Target.set_printings (Type_Constructor ("fun",
    7.69      [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    7.70        brackify_infix (1, R) fxy (
     8.1 --- a/src/Tools/Code/code_target.ML	Thu Dec 14 21:40:43 2017 +0100
     8.2 +++ b/src/Tools/Code/code_target.ML	Thu Dec 14 18:42:39 2017 +0100
     8.3 @@ -178,14 +178,15 @@
     8.4    
     8.5  (** theory data **)
     8.6  
     8.7 -type language = { serializer: serializer, literals: literals,
     8.8 -  check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }; 
     8.9 +type language = {serializer: serializer, literals: literals,
    8.10 +  check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string},
    8.11 +  evaluation_args: Token.T list}; 
    8.12  
    8.13  type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list;
    8.14  
    8.15  val merge_ancestry : ancestry * ancestry -> ancestry = AList.join (op =) (K snd);
    8.16  
    8.17 -type target = { serial: serial, language: language, ancestry: ancestry };
    8.18 +type target = {serial: serial, language: language, ancestry: ancestry};
    8.19  
    8.20  structure Targets = Theory_Data
    8.21  (
    8.22 @@ -195,7 +196,7 @@
    8.23    fun merge (targets1, targets2) : T =
    8.24      Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
    8.25        if #serial target1 = #serial target2 then
    8.26 -      ({ serial = #serial target1, language = #language target1,
    8.27 +      ({serial = #serial target1, language = #language target1,
    8.28          ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
    8.29          Code_Printer.merge_data (data1, data2))
    8.30        else error ("Incompatible targets: " ^ quote target_name) 
    8.31 @@ -234,7 +235,8 @@
    8.32    end;
    8.33  
    8.34  fun add_language (target_name, language) =
    8.35 -  allocate_target target_name { serial = serial (), language = language, ancestry = [] };
    8.36 +  allocate_target target_name {serial = serial (), language = language,
    8.37 +    ancestry = []};
    8.38  
    8.39  fun add_derived_target (target_name, initial_ancestry) thy =
    8.40    let
    8.41 @@ -251,8 +253,8 @@
    8.42      val ancestry = fold1 (fn ancestry' => fn ancestry =>
    8.43        merge_ancestry (ancestry, ancestry')) ancestries;
    8.44    in
    8.45 -    allocate_target target_name { serial = #serial supremum, language = #language supremum,
    8.46 -      ancestry = ancestry } thy 
    8.47 +    allocate_target target_name {serial = #serial supremum, language = #language supremum,
    8.48 +      ancestry = ancestry} thy 
    8.49    end;
    8.50    
    8.51  fun map_data target_name f thy =
    8.52 @@ -285,6 +287,8 @@
    8.53  
    8.54  fun the_literals ctxt = #literals o the_language ctxt;
    8.55  
    8.56 +fun the_evaluation_args ctxt = #evaluation_args o the_language ctxt;
    8.57 +
    8.58  local
    8.59  
    8.60  fun activate_target ctxt target_name =
    8.61 @@ -421,8 +425,9 @@
    8.62  
    8.63  fun compilation_text' ctxt target_name some_module_name program syms =
    8.64    let
    8.65 +    val evaluation_args = the_evaluation_args ctxt target_name;
    8.66      val (mounted_serializer, (_, prepared_program)) =
    8.67 -      mount_serializer ctxt target_name NONE (the_default generatedN some_module_name) [] program syms;
    8.68 +      mount_serializer ctxt target_name NONE (the_default generatedN some_module_name) evaluation_args program syms;
    8.69    in
    8.70      Code_Preproc.timed_exec "serializing"
    8.71      (fn () => dynamic_compilation_text mounted_serializer prepared_program syms) ctxt