# HG changeset patch
# User wenzelm
# Date 1399066285 -7200
# Node ID 94477e9ff063c6aa33148d4b170ecda05f248fcf
# Parent  ba18bd41e51033669f2357866f64bc6ecda1437e# Parent  477cd67f963fffa0d623256560a7afb0a47ece03
merged

diff -r 477cd67f963f -r 94477e9ff063 NEWS
--- a/NEWS	Fri May 02 23:30:47 2014 +0200
+++ b/NEWS	Fri May 02 23:31:25 2014 +0200
@@ -229,6 +229,9 @@
   "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
   "uint_word_arith_bintrs".
 
+* Code generator: enforce case of identifiers only for strict
+target language requirements.  INCOMPATIBILITY.
+
 * Code generator: explicit proof contexts in many ML interfaces.
 INCOMPATIBILITY.
 
diff -r 477cd67f963f -r 94477e9ff063 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri May 02 23:30:47 2014 +0200
+++ b/src/Tools/Code/code_haskell.ML	Fri May 02 23:31:25 2014 +0200
@@ -277,8 +277,7 @@
   let
     fun namify_fun upper base (nsp_fun, nsp_typ) =
       let
-        val (base', nsp_fun') =
-          Name.variant (if upper then Name.enforce_case true base else base) nsp_fun;
+        val (base', nsp_fun') = Name.variant (Name.enforce_case upper base) nsp_fun;
       in (base', (nsp_fun', nsp_typ)) end;
     fun namify_typ base (nsp_fun, nsp_typ) =
       let
diff -r 477cd67f963f -r 94477e9ff063 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri May 02 23:30:47 2014 +0200
+++ b/src/Tools/Code/code_ml.ML	Fri May 02 23:31:25 2014 +0200
@@ -723,12 +723,11 @@
   let
     fun namify_const upper base (nsp_const, nsp_type) =
       let
-        val (base', nsp_const') =
-          Name.variant (if upper then Name.enforce_case true base else base) nsp_const
+        val (base', nsp_const') = Name.variant (Name.enforce_case upper base) nsp_const
       in (base', (nsp_const', nsp_type)) end;
     fun namify_type base (nsp_const, nsp_type) =
       let
-        val (base', nsp_type') = Name.variant base nsp_type
+        val (base', nsp_type') = Name.variant (Name.enforce_case false base) nsp_type
       in (base', (nsp_const, nsp_type')) end;
     fun namify_stmt (Code_Thingol.Fun _) = namify_const false
       | namify_stmt (Code_Thingol.Datatype _) = namify_type
diff -r 477cd67f963f -r 94477e9ff063 src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Fri May 02 23:30:47 2014 +0200
+++ b/src/Tools/Code/code_namespace.ML	Fri May 02 23:31:25 2014 +0200
@@ -158,13 +158,14 @@
   then module_fragments' { identifiers = identifiers, reserved = reserved }
   else K (Long_Name.explode module_name);
 
-fun build_module_namespace ctxt { module_prefix, module_name, identifiers, reserved } program =
+fun build_module_namespace ctxt enforce_upper { module_prefix, module_name, identifiers, reserved } program =
   let
     val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
     val module_fragments' = module_fragments
       { module_name = module_name, identifiers = identifiers, reserved = reserved };
+    val adjust_case = if enforce_upper then map (Name.enforce_case true) else I;
   in
-    fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ module_fragments' name))
+    fold (fn name => Symtab.update (name, adjust_case (Long_Name.explode module_prefix @ module_fragments' name)))
       module_names Symtab.empty
   end;
 
@@ -195,7 +196,7 @@
   let
 
     (* building module name hierarchy *)
-    val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix,
+    val module_namespace = build_module_namespace ctxt true { module_prefix = module_prefix,
       module_name = module_name, identifiers = identifiers, reserved = reserved } program;
     val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
       force_module = Long_Name.explode module_name, identifiers = identifiers }
@@ -317,7 +318,7 @@
   let
 
     (* building module name hierarchy *)
-    val module_namespace = build_module_namespace ctxt { module_prefix = "",
+    val module_namespace = build_module_namespace ctxt false { module_prefix = "",
       module_name = module_name, identifiers = identifiers, reserved = reserved } program;
     val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
       force_module = Long_Name.explode module_name, identifiers = identifiers }
diff -r 477cd67f963f -r 94477e9ff063 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri May 02 23:30:47 2014 +0200
+++ b/src/Tools/Code/code_scala.ML	Fri May 02 23:31:25 2014 +0200
@@ -305,21 +305,19 @@
       let
         val (base', nsp_object') = Name.variant base nsp_object
       in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
-    fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
+    fun namify_common base ((nsp_class, nsp_object), nsp_common) =
       let
-        val (base', nsp_common') =
-          Name.variant (if upper then Name.enforce_case true base else base) nsp_common
+        val (base', nsp_common') = Name.variant base nsp_common
       in
-        (base',
-          ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
+        (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
       end;
     fun namify_stmt (Code_Thingol.Fun _) = namify_object
       | namify_stmt (Code_Thingol.Datatype _) = namify_class
-      | namify_stmt (Code_Thingol.Datatypecons _) = namify_common true
+      | namify_stmt (Code_Thingol.Datatypecons _) = namify_common
       | namify_stmt (Code_Thingol.Class _) = namify_class
       | namify_stmt (Code_Thingol.Classrel _) = namify_object
       | namify_stmt (Code_Thingol.Classparam _) = namify_object
-      | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
+      | namify_stmt (Code_Thingol.Classinst _) = namify_common;
     fun memorize_implicits sym =
       let
         fun is_classinst stmt = case stmt
diff -r 477cd67f963f -r 94477e9ff063 src/Tools/Code/code_symbol.ML
--- a/src/Tools/Code/code_symbol.ML	Fri May 02 23:30:47 2014 +0200
+++ b/src/Tools/Code/code_symbol.ML	Fri May 02 23:31:25 2014 +0200
@@ -83,7 +83,7 @@
 structure Graph = Graph(type key = T val ord = symbol_ord);
 
 local
-  val base = Name.desymbolize (SOME false) o Long_Name.base_name;
+  val base = Name.desymbolize NONE o Long_Name.base_name;
   fun base_rel (x, y) = base y ^ "_" ^ base x;
 in
 
diff -r 477cd67f963f -r 94477e9ff063 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri May 02 23:30:47 2014 +0200
+++ b/src/Tools/Code/code_target.ML	Fri May 02 23:31:25 2014 +0200
@@ -128,14 +128,14 @@
     val _ = if s = "" then error "Bad empty code name" else ();
     val xs = Long_Name.explode s;
     val xs' = if is_module
-        then map (Name.desymbolize (SOME true)) xs
+        then map (Name.desymbolize NONE) xs
       else if length xs < 2
         then error ("Bad code name without module component: " ^ quote s)
       else
         let
           val (ys, y) = split_last xs;
-          val ys' = map (Name.desymbolize (SOME true)) ys;
-          val y' = Name.desymbolize (SOME false) y;
+          val ys' = map (Name.desymbolize NONE) ys;
+          val y' = Name.desymbolize NONE y;
         in ys' @ [y'] end;
   in if xs' = xs
     then if is_module then (xs, "") else split_last xs