--- 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.
--- 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
--- 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
--- 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 }
--- 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
--- 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
--- 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