# HG changeset patch # User haftmann # Date 1398929436 -7200 # Node ID baef1c110f120aac21f0535cb29c188bf4920e74 # Parent b66639331db50cb7ce44158c4bd6ae110f2c6783 centralized upper/lowercase name mangling diff -r b66639331db5 -r baef1c110f12 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 diff -r b66639331db5 -r baef1c110f12 src/Pure/name.ML --- 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; diff -r b66639331db5 -r baef1c110f12 src/Tools/Code/code_haskell.ML --- 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 diff -r b66639331db5 -r baef1c110f12 src/Tools/Code/code_ml.ML --- 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 diff -r b66639331db5 -r baef1c110f12 src/Tools/Code/code_printer.ML --- 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 diff -r b66639331db5 -r baef1c110f12 src/Tools/Code/code_scala.ML --- 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'))