--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu May 01 09:30:35 2014 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu May 01 09:30:36 2014 +0200
@@ -132,12 +132,6 @@
)
-(* general string functions *)
-
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
-
-
(* internal program representation *)
datatype arith_op = Plus | Minus
@@ -225,7 +219,7 @@
fun update' c table =
if AList.defined (op =) table c then table else
let
- val c' = mk_conform first_lower "pred" (map snd table) (Long_Name.base_name c)
+ val c' = mk_conform (Name.enforce_case false) "pred" (map snd table) (Long_Name.base_name c)
in
AList.update (op =) (c, c') table
end
@@ -433,7 +427,7 @@
let
val name = Long_Name.base_name pred ^ (if pol then "p" else "n")
^ Predicate_Compile_Aux.ascii_string_of_mode mode
- val p' = mk_conform first_lower "pred" (map snd table) name
+ val p' = mk_conform (Name.enforce_case false) "pred" (map snd table) name
in
AList.update (op =) (p, p') table
end
@@ -526,7 +520,7 @@
| add_ground_typ _ = I
fun mk_relname (Type (Tcon, Targs)) =
- first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
+ Name.enforce_case false (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
| mk_relname _ = raise Fail "unexpected type"
fun mk_lim_relname T = "lim_" ^ mk_relname T
@@ -677,7 +671,7 @@
fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming)
fun mk_renaming v renaming =
- (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming
+ (v, mk_conform (Name.enforce_case true) "Var" (map snd renaming) v) :: renaming
fun rename_vars_clause ((rel, args), prem) =
let
--- a/src/Pure/name.ML Thu May 01 09:30:35 2014 +0200
+++ b/src/Pure/name.ML Thu May 01 09:30:36 2014 +0200
@@ -31,6 +31,7 @@
val invent_list: string list -> string -> int -> string list
val variant: string -> context -> string * context
val variant_list: string list -> string list -> string list
+ val enforce_case: bool -> string -> string
val desymbolize: bool option -> string -> string
end;
@@ -150,6 +151,13 @@
(* names conforming to typical requirements of identifiers in the world outside *)
+fun enforce_case' false cs =
+ (if forall Symbol.is_ascii_upper cs then map else nth_map 0) Symbol.to_ascii_lower cs
+ | enforce_case' true cs =
+ nth_map 0 Symbol.to_ascii_upper cs;
+
+fun enforce_case upper = implode o enforce_case' upper o raw_explode;
+
fun desymbolize perhaps_upper "" =
if the_default false perhaps_upper then "X" else "x"
| desymbolize perhaps_upper s =
@@ -171,13 +179,7 @@
(case Symbol.decode x of
Symbol.Sym name => "_" :: raw_explode name @ sep xs
| _ => sep xs);
- fun upper_lower cs =
- case perhaps_upper of
- NONE => cs
- | SOME true => nth_map 0 Symbol.to_ascii_upper cs
- | SOME false =>
- (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
- Symbol.to_ascii_lower cs;
+ val upper_lower = Option.map enforce_case' perhaps_upper |> the_default I;
in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
end;
--- a/src/Tools/Code/code_haskell.ML Thu May 01 09:30:35 2014 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu May 01 09:30:36 2014 +0200
@@ -278,11 +278,11 @@
fun namify_fun upper base (nsp_fun, nsp_typ) =
let
val (base', nsp_fun') =
- Name.variant (if upper then first_upper base else base) nsp_fun;
+ Name.variant (if upper then Name.enforce_case true base else base) nsp_fun;
in (base', (nsp_fun', nsp_typ)) end;
fun namify_typ base (nsp_fun, nsp_typ) =
let
- val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
+ val (base', nsp_typ') = Name.variant (Name.enforce_case true base) nsp_typ;
in (base', (nsp_fun, nsp_typ')) end;
fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair
| namify_stmt (Code_Thingol.Fun _) = namify_fun false
--- a/src/Tools/Code/code_ml.ML Thu May 01 09:30:35 2014 +0200
+++ b/src/Tools/Code/code_ml.ML Thu May 01 09:30:36 2014 +0200
@@ -84,8 +84,8 @@
(if is_pseudo_fun (Class_Instance inst) then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
- [str (if k = 1 then first_upper v ^ "_"
- else first_upper v ^ string_of_int (i+1) ^ "_")]
+ [str (if k = 1 then Name.enforce_case true v ^ "_"
+ else Name.enforce_case true v ^ string_of_int (i+1) ^ "_")]
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
@@ -395,8 +395,8 @@
(if is_pseudo_fun (Class_Instance inst) then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
- str (if k = 1 then "_" ^ first_upper v
- else "_" ^ first_upper v ^ string_of_int (i+1))
+ str (if k = 1 then "_" ^ Name.enforce_case true v
+ else "_" ^ Name.enforce_case true v ^ string_of_int (i+1))
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
@@ -655,7 +655,7 @@
(Constant classparam, ([(v, [class])], ty));
fun print_classparam_field (classparam, ty) =
print_field (deresolve_const classparam) (print_typ NOBR ty);
- val w = "_" ^ first_upper v;
+ val w = "_" ^ Name.enforce_case true v;
fun print_classparam_proj (classparam, _) =
(concat o map str) ["let", deresolve_const classparam, w, "=",
w ^ "." ^ deresolve_const classparam ^ ";;"];
@@ -724,7 +724,7 @@
fun namify_const upper base (nsp_const, nsp_type) =
let
val (base', nsp_const') =
- Name.variant (if upper then first_upper base else base) nsp_const
+ Name.variant (if upper then Name.enforce_case true base else base) nsp_const
in (base', (nsp_const', nsp_type)) end;
fun namify_type base (nsp_const, nsp_type) =
let
--- a/src/Tools/Code/code_printer.ML Thu May 01 09:30:35 2014 +0200
+++ b/src/Tools/Code/code_printer.ML Thu May 01 09:30:36 2014 +0200
@@ -28,8 +28,6 @@
val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
val format: Code_Symbol.T list -> int -> Pretty.T -> string
- val first_upper: string -> string
- val first_lower: string -> string
type var_ctxt
val make_vars: string list -> var_ctxt
val intro_vars: string list -> var_ctxt -> var_ctxt
@@ -175,9 +173,6 @@
SOME name' => name'
| NONE => error ("Invalid name in context: " ^ quote name);
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
-
fun aux_params vars lhss =
let
fun fish_param _ (w as SOME _) = w
--- a/src/Tools/Code/code_scala.ML Thu May 01 09:30:35 2014 +0200
+++ b/src/Tools/Code/code_scala.ML Thu May 01 09:30:36 2014 +0200
@@ -31,8 +31,8 @@
val deresolve_const = deresolve o Constant;
val deresolve_tyco = deresolve o Type_Constructor;
val deresolve_class = deresolve o Type_Class;
- fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
- fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
+ fun lookup_tyvar tyvars = lookup_var tyvars o Name.enforce_case true;
+ fun intro_tyvars vs = intro_vars (map (Name.enforce_case true o fst) vs);
fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
(print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
@@ -308,7 +308,7 @@
fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
let
val (base', nsp_common') =
- Name.variant (if upper then first_upper base else base) nsp_common
+ Name.variant (if upper then Name.enforce_case true base else base) nsp_common
in
(base',
((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))