accomplish potentially case-insenstive file systems for Scala
authorhaftmann
Thu Oct 02 17:51:04 2014 +0200 (2014-10-02)
changeset 58520a4d1f8041af0
parent 58519 7d85162e8520
child 58521 b70e93c05efe
accomplish potentially case-insenstive file systems for Scala
src/HOL/Codegenerator_Test/Code_Test_Scala.thy
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_scala.ML
     1.1 --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Thu Oct 02 22:33:45 2014 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Thu Oct 02 17:51:04 2014 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  
     1.5  theory Code_Test_Scala imports Code_Test begin 
     1.6  
     1.7 +declare [[scala_case_insensitive]]
     1.8 +
     1.9  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
    1.10  
    1.11  value [Scala] "14 + 7 * -12 :: integer"
     2.1 --- a/src/Tools/Code/code_namespace.ML	Thu Oct 02 22:33:45 2014 +0200
     2.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Oct 02 17:51:04 2014 +0200
     2.3 @@ -6,6 +6,8 @@
     2.4  
     2.5  signature CODE_NAMESPACE =
     2.6  sig
     2.7 +  val variant_case_insensitive: string -> Name.context -> string * Name.context
     2.8 +
     2.9    datatype export = Private | Opaque | Public
    2.10    val is_public: export -> bool
    2.11    val not_private: export -> bool
    2.12 @@ -47,6 +49,25 @@
    2.13  structure Code_Namespace : CODE_NAMESPACE =
    2.14  struct
    2.15  
    2.16 +(** name handling on case-insensitive file systems **)
    2.17 +
    2.18 +fun restore_for cs =
    2.19 +  if forall Symbol.is_ascii_upper cs then map Symbol.to_ascii_upper
    2.20 +  else if Symbol.is_ascii_upper (nth cs 0) then nth_map 0 Symbol.to_ascii_upper
    2.21 +  else I;
    2.22 +
    2.23 +fun variant_case_insensitive s ctxt =
    2.24 +  let
    2.25 +    val cs = Symbol.explode s;
    2.26 +    val s_lower = implode (map Symbol.to_ascii_lower cs);
    2.27 +    val restore = implode o restore_for cs o Symbol.explode;
    2.28 +  in
    2.29 +    ctxt
    2.30 +    |> Name.variant s_lower
    2.31 +    |>> restore
    2.32 +  end;
    2.33 +
    2.34 +
    2.35  (** export **)
    2.36  
    2.37  datatype export = Private | Opaque | Public;
     3.1 --- a/src/Tools/Code/code_scala.ML	Thu Oct 02 22:33:45 2014 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Thu Oct 02 17:51:04 2014 +0200
     3.3 @@ -7,6 +7,7 @@
     3.4  signature CODE_SCALA =
     3.5  sig
     3.6    val target: string
     3.7 +  val case_insensitive: bool Config.T;
     3.8    val setup: theory -> theory
     3.9  end;
    3.10  
    3.11 @@ -22,6 +23,10 @@
    3.12  infixr 5 @@;
    3.13  infixr 5 @|;
    3.14  
    3.15 +(** preliminary: option to circumvent clashes on case-insensitive file systems **)
    3.16 +
    3.17 +val case_insensitive = Attrib.setup_config_bool @{binding "scala_case_insensitive"} (K false);
    3.18 +
    3.19  
    3.20  (** Scala serializer **)
    3.21  
    3.22 @@ -293,21 +298,24 @@
    3.23  
    3.24  fun scala_program_of_program ctxt module_name reserved identifiers exports program =
    3.25    let
    3.26 +    val variant = if Config.get ctxt case_insensitive
    3.27 +      then Code_Namespace.variant_case_insensitive
    3.28 +      else Name.variant;
    3.29      fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
    3.30        let
    3.31          val declare = Name.declare name_fragment;
    3.32        in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
    3.33      fun namify_class base ((nsp_class, nsp_object), nsp_common) =
    3.34        let
    3.35 -        val (base', nsp_class') = Name.variant base nsp_class
    3.36 +        val (base', nsp_class') = variant base nsp_class
    3.37        in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
    3.38      fun namify_object base ((nsp_class, nsp_object), nsp_common) =
    3.39        let
    3.40 -        val (base', nsp_object') = Name.variant base nsp_object
    3.41 +        val (base', nsp_object') = variant base nsp_object
    3.42        in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
    3.43      fun namify_common base ((nsp_class, nsp_object), nsp_common) =
    3.44        let
    3.45 -        val (base', nsp_common') = Name.variant base nsp_common
    3.46 +        val (base', nsp_common') = variant base nsp_common
    3.47        in
    3.48          (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
    3.49        end;