enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
authorhaftmann
Fri May 02 21:18:50 2014 +0200 (2014-05-02)
changeset 56826ba18bd41e510
parent 56825 8872e0776e97
child 56839 94477e9ff063
enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
NEWS
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_symbol.ML
src/Tools/Code/code_target.ML
     1.1 --- a/NEWS	Fri May 02 14:15:23 2014 +0200
     1.2 +++ b/NEWS	Fri May 02 21:18:50 2014 +0200
     1.3 @@ -226,6 +226,9 @@
     1.4    "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
     1.5    "uint_word_arith_bintrs".
     1.6  
     1.7 +* Code generator: enforce case of identifiers only for strict
     1.8 +target language requirements.  INCOMPATIBILITY.
     1.9 +
    1.10  * Code generator: explicit proof contexts in many ML interfaces.
    1.11  INCOMPATIBILITY.
    1.12  
     2.1 --- a/src/Tools/Code/code_haskell.ML	Fri May 02 14:15:23 2014 +0200
     2.2 +++ b/src/Tools/Code/code_haskell.ML	Fri May 02 21:18:50 2014 +0200
     2.3 @@ -277,8 +277,7 @@
     2.4    let
     2.5      fun namify_fun upper base (nsp_fun, nsp_typ) =
     2.6        let
     2.7 -        val (base', nsp_fun') =
     2.8 -          Name.variant (if upper then Name.enforce_case true base else base) nsp_fun;
     2.9 +        val (base', nsp_fun') = Name.variant (Name.enforce_case upper base) nsp_fun;
    2.10        in (base', (nsp_fun', nsp_typ)) end;
    2.11      fun namify_typ base (nsp_fun, nsp_typ) =
    2.12        let
     3.1 --- a/src/Tools/Code/code_ml.ML	Fri May 02 14:15:23 2014 +0200
     3.2 +++ b/src/Tools/Code/code_ml.ML	Fri May 02 21:18:50 2014 +0200
     3.3 @@ -723,12 +723,11 @@
     3.4    let
     3.5      fun namify_const upper base (nsp_const, nsp_type) =
     3.6        let
     3.7 -        val (base', nsp_const') =
     3.8 -          Name.variant (if upper then Name.enforce_case true base else base) nsp_const
     3.9 +        val (base', nsp_const') = Name.variant (Name.enforce_case upper base) nsp_const
    3.10        in (base', (nsp_const', nsp_type)) end;
    3.11      fun namify_type base (nsp_const, nsp_type) =
    3.12        let
    3.13 -        val (base', nsp_type') = Name.variant base nsp_type
    3.14 +        val (base', nsp_type') = Name.variant (Name.enforce_case false base) nsp_type
    3.15        in (base', (nsp_const, nsp_type')) end;
    3.16      fun namify_stmt (Code_Thingol.Fun _) = namify_const false
    3.17        | namify_stmt (Code_Thingol.Datatype _) = namify_type
     4.1 --- a/src/Tools/Code/code_namespace.ML	Fri May 02 14:15:23 2014 +0200
     4.2 +++ b/src/Tools/Code/code_namespace.ML	Fri May 02 21:18:50 2014 +0200
     4.3 @@ -158,13 +158,14 @@
     4.4    then module_fragments' { identifiers = identifiers, reserved = reserved }
     4.5    else K (Long_Name.explode module_name);
     4.6  
     4.7 -fun build_module_namespace ctxt { module_prefix, module_name, identifiers, reserved } program =
     4.8 +fun build_module_namespace ctxt enforce_upper { module_prefix, module_name, identifiers, reserved } program =
     4.9    let
    4.10      val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
    4.11      val module_fragments' = module_fragments
    4.12        { module_name = module_name, identifiers = identifiers, reserved = reserved };
    4.13 +    val adjust_case = if enforce_upper then map (Name.enforce_case true) else I;
    4.14    in
    4.15 -    fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ module_fragments' name))
    4.16 +    fold (fn name => Symtab.update (name, adjust_case (Long_Name.explode module_prefix @ module_fragments' name)))
    4.17        module_names Symtab.empty
    4.18    end;
    4.19  
    4.20 @@ -195,7 +196,7 @@
    4.21    let
    4.22  
    4.23      (* building module name hierarchy *)
    4.24 -    val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix,
    4.25 +    val module_namespace = build_module_namespace ctxt true { module_prefix = module_prefix,
    4.26        module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    4.27      val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    4.28        force_module = Long_Name.explode module_name, identifiers = identifiers }
    4.29 @@ -317,7 +318,7 @@
    4.30    let
    4.31  
    4.32      (* building module name hierarchy *)
    4.33 -    val module_namespace = build_module_namespace ctxt { module_prefix = "",
    4.34 +    val module_namespace = build_module_namespace ctxt false { module_prefix = "",
    4.35        module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    4.36      val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    4.37        force_module = Long_Name.explode module_name, identifiers = identifiers }
     5.1 --- a/src/Tools/Code/code_scala.ML	Fri May 02 14:15:23 2014 +0200
     5.2 +++ b/src/Tools/Code/code_scala.ML	Fri May 02 21:18:50 2014 +0200
     5.3 @@ -305,21 +305,19 @@
     5.4        let
     5.5          val (base', nsp_object') = Name.variant base nsp_object
     5.6        in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
     5.7 -    fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
     5.8 +    fun namify_common base ((nsp_class, nsp_object), nsp_common) =
     5.9        let
    5.10 -        val (base', nsp_common') =
    5.11 -          Name.variant (if upper then Name.enforce_case true base else base) nsp_common
    5.12 +        val (base', nsp_common') = Name.variant base nsp_common
    5.13        in
    5.14 -        (base',
    5.15 -          ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
    5.16 +        (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
    5.17        end;
    5.18      fun namify_stmt (Code_Thingol.Fun _) = namify_object
    5.19        | namify_stmt (Code_Thingol.Datatype _) = namify_class
    5.20 -      | namify_stmt (Code_Thingol.Datatypecons _) = namify_common true
    5.21 +      | namify_stmt (Code_Thingol.Datatypecons _) = namify_common
    5.22        | namify_stmt (Code_Thingol.Class _) = namify_class
    5.23        | namify_stmt (Code_Thingol.Classrel _) = namify_object
    5.24        | namify_stmt (Code_Thingol.Classparam _) = namify_object
    5.25 -      | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
    5.26 +      | namify_stmt (Code_Thingol.Classinst _) = namify_common;
    5.27      fun memorize_implicits sym =
    5.28        let
    5.29          fun is_classinst stmt = case stmt
     6.1 --- a/src/Tools/Code/code_symbol.ML	Fri May 02 14:15:23 2014 +0200
     6.2 +++ b/src/Tools/Code/code_symbol.ML	Fri May 02 21:18:50 2014 +0200
     6.3 @@ -83,7 +83,7 @@
     6.4  structure Graph = Graph(type key = T val ord = symbol_ord);
     6.5  
     6.6  local
     6.7 -  val base = Name.desymbolize (SOME false) o Long_Name.base_name;
     6.8 +  val base = Name.desymbolize NONE o Long_Name.base_name;
     6.9    fun base_rel (x, y) = base y ^ "_" ^ base x;
    6.10  in
    6.11  
     7.1 --- a/src/Tools/Code/code_target.ML	Fri May 02 14:15:23 2014 +0200
     7.2 +++ b/src/Tools/Code/code_target.ML	Fri May 02 21:18:50 2014 +0200
     7.3 @@ -128,14 +128,14 @@
     7.4      val _ = if s = "" then error "Bad empty code name" else ();
     7.5      val xs = Long_Name.explode s;
     7.6      val xs' = if is_module
     7.7 -        then map (Name.desymbolize (SOME true)) xs
     7.8 +        then map (Name.desymbolize NONE) xs
     7.9        else if length xs < 2
    7.10          then error ("Bad code name without module component: " ^ quote s)
    7.11        else
    7.12          let
    7.13            val (ys, y) = split_last xs;
    7.14 -          val ys' = map (Name.desymbolize (SOME true)) ys;
    7.15 -          val y' = Name.desymbolize (SOME false) y;
    7.16 +          val ys' = map (Name.desymbolize NONE) ys;
    7.17 +          val y' = Name.desymbolize NONE y;
    7.18          in ys' @ [y'] end;
    7.19    in if xs' = xs
    7.20      then if is_module then (xs, "") else split_last xs