centralized upper/lowercase name mangling
authorhaftmann
Thu May 01 09:30:36 2014 +0200 (2014-05-01)
changeset 56812baef1c110f12
parent 56811 b66639331db5
child 56813 80a5905c1610
centralized upper/lowercase name mangling
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/Pure/name.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu May 01 09:30:35 2014 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu May 01 09:30:36 2014 +0200
     1.3 @@ -132,12 +132,6 @@
     1.4  )
     1.5  
     1.6  
     1.7 -(* general string functions *)
     1.8 -
     1.9 -val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
    1.10 -val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
    1.11 -
    1.12 -
    1.13  (* internal program representation *)
    1.14  
    1.15  datatype arith_op = Plus | Minus
    1.16 @@ -225,7 +219,7 @@
    1.17      fun update' c table =
    1.18        if AList.defined (op =) table c then table else
    1.19          let
    1.20 -          val c' = mk_conform first_lower "pred" (map snd table) (Long_Name.base_name c)
    1.21 +          val c' = mk_conform (Name.enforce_case false) "pred" (map snd table) (Long_Name.base_name c)
    1.22          in
    1.23            AList.update (op =) (c, c') table
    1.24          end
    1.25 @@ -433,7 +427,7 @@
    1.26          let
    1.27            val name = Long_Name.base_name pred ^ (if pol then "p" else "n")
    1.28              ^ Predicate_Compile_Aux.ascii_string_of_mode mode
    1.29 -          val p' = mk_conform first_lower "pred" (map snd table) name
    1.30 +          val p' = mk_conform (Name.enforce_case false) "pred" (map snd table) name
    1.31          in
    1.32            AList.update (op =) (p, p') table
    1.33          end
    1.34 @@ -526,7 +520,7 @@
    1.35    | add_ground_typ _ = I
    1.36  
    1.37  fun mk_relname (Type (Tcon, Targs)) =
    1.38 -      first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
    1.39 +      Name.enforce_case false (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
    1.40    | mk_relname _ = raise Fail "unexpected type"
    1.41  
    1.42  fun mk_lim_relname T = "lim_" ^  mk_relname T
    1.43 @@ -677,7 +671,7 @@
    1.44  fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming)
    1.45  
    1.46  fun mk_renaming v renaming =
    1.47 -  (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming
    1.48 +  (v, mk_conform (Name.enforce_case true) "Var" (map snd renaming) v) :: renaming
    1.49  
    1.50  fun rename_vars_clause ((rel, args), prem) =
    1.51    let
     2.1 --- a/src/Pure/name.ML	Thu May 01 09:30:35 2014 +0200
     2.2 +++ b/src/Pure/name.ML	Thu May 01 09:30:36 2014 +0200
     2.3 @@ -31,6 +31,7 @@
     2.4    val invent_list: string list -> string -> int -> string list
     2.5    val variant: string -> context -> string * context
     2.6    val variant_list: string list -> string list -> string list
     2.7 +  val enforce_case: bool -> string -> string
     2.8    val desymbolize: bool option -> string -> string
     2.9  end;
    2.10  
    2.11 @@ -150,6 +151,13 @@
    2.12  
    2.13  (* names conforming to typical requirements of identifiers in the world outside *)
    2.14  
    2.15 +fun enforce_case' false cs = 
    2.16 +      (if forall Symbol.is_ascii_upper cs then map else nth_map 0) Symbol.to_ascii_lower cs
    2.17 +  | enforce_case' true cs = 
    2.18 +      nth_map 0 Symbol.to_ascii_upper cs;
    2.19 +
    2.20 +fun enforce_case upper = implode o enforce_case' upper o raw_explode;
    2.21 +
    2.22  fun desymbolize perhaps_upper "" =
    2.23        if the_default false perhaps_upper then "X" else "x"
    2.24    | desymbolize perhaps_upper s =
    2.25 @@ -171,13 +179,7 @@
    2.26              (case Symbol.decode x of
    2.27                Symbol.Sym name => "_" :: raw_explode name @ sep xs
    2.28              | _ => sep xs);
    2.29 -        fun upper_lower cs =
    2.30 -          case perhaps_upper of
    2.31 -            NONE => cs
    2.32 -          | SOME true => nth_map 0 Symbol.to_ascii_upper cs
    2.33 -          | SOME false =>
    2.34 -              (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
    2.35 -                Symbol.to_ascii_lower cs;
    2.36 +        val upper_lower = Option.map enforce_case' perhaps_upper |> the_default I;
    2.37        in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
    2.38  
    2.39  end;
     3.1 --- a/src/Tools/Code/code_haskell.ML	Thu May 01 09:30:35 2014 +0200
     3.2 +++ b/src/Tools/Code/code_haskell.ML	Thu May 01 09:30:36 2014 +0200
     3.3 @@ -278,11 +278,11 @@
     3.4      fun namify_fun upper base (nsp_fun, nsp_typ) =
     3.5        let
     3.6          val (base', nsp_fun') =
     3.7 -          Name.variant (if upper then first_upper base else base) nsp_fun;
     3.8 +          Name.variant (if upper then Name.enforce_case true base else base) nsp_fun;
     3.9        in (base', (nsp_fun', nsp_typ)) end;
    3.10      fun namify_typ base (nsp_fun, nsp_typ) =
    3.11        let
    3.12 -        val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
    3.13 +        val (base', nsp_typ') = Name.variant (Name.enforce_case true base) nsp_typ;
    3.14        in (base', (nsp_fun, nsp_typ')) end;
    3.15      fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair
    3.16        | namify_stmt (Code_Thingol.Fun _) = namify_fun false
     4.1 --- a/src/Tools/Code/code_ml.ML	Thu May 01 09:30:35 2014 +0200
     4.2 +++ b/src/Tools/Code/code_ml.ML	Thu May 01 09:30:36 2014 +0200
     4.3 @@ -84,8 +84,8 @@
     4.4              (if is_pseudo_fun (Class_Instance inst) then [str "()"]
     4.5              else map_filter (print_dicts is_pseudo_fun BR) dss))
     4.6        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
     4.7 -          [str (if k = 1 then first_upper v ^ "_"
     4.8 -            else first_upper v ^ string_of_int (i+1) ^ "_")]
     4.9 +          [str (if k = 1 then Name.enforce_case true v ^ "_"
    4.10 +            else Name.enforce_case true v ^ string_of_int (i+1) ^ "_")]
    4.11      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    4.12      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    4.13        (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
    4.14 @@ -395,8 +395,8 @@
    4.15              (if is_pseudo_fun (Class_Instance inst) then [str "()"]
    4.16              else map_filter (print_dicts is_pseudo_fun BR) dss))
    4.17        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
    4.18 -          str (if k = 1 then "_" ^ first_upper v
    4.19 -            else "_" ^ first_upper v ^ string_of_int (i+1))
    4.20 +          str (if k = 1 then "_" ^ Name.enforce_case true v
    4.21 +            else "_" ^ Name.enforce_case true v ^ string_of_int (i+1))
    4.22      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    4.23      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    4.24        (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
    4.25 @@ -655,7 +655,7 @@
    4.26                  (Constant classparam, ([(v, [class])], ty));
    4.27              fun print_classparam_field (classparam, ty) =
    4.28                print_field (deresolve_const classparam) (print_typ NOBR ty);
    4.29 -            val w = "_" ^ first_upper v;
    4.30 +            val w = "_" ^ Name.enforce_case true v;
    4.31              fun print_classparam_proj (classparam, _) =
    4.32                (concat o map str) ["let", deresolve_const classparam, w, "=",
    4.33                  w ^ "." ^ deresolve_const classparam ^ ";;"];
    4.34 @@ -724,7 +724,7 @@
    4.35      fun namify_const upper base (nsp_const, nsp_type) =
    4.36        let
    4.37          val (base', nsp_const') =
    4.38 -          Name.variant (if upper then first_upper base else base) nsp_const
    4.39 +          Name.variant (if upper then Name.enforce_case true base else base) nsp_const
    4.40        in (base', (nsp_const', nsp_type)) end;
    4.41      fun namify_type base (nsp_const, nsp_type) =
    4.42        let
     5.1 --- a/src/Tools/Code/code_printer.ML	Thu May 01 09:30:35 2014 +0200
     5.2 +++ b/src/Tools/Code/code_printer.ML	Thu May 01 09:30:36 2014 +0200
     5.3 @@ -28,8 +28,6 @@
     5.4    val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
     5.5    val format: Code_Symbol.T list -> int -> Pretty.T -> string
     5.6  
     5.7 -  val first_upper: string -> string
     5.8 -  val first_lower: string -> string
     5.9    type var_ctxt
    5.10    val make_vars: string list -> var_ctxt
    5.11    val intro_vars: string list -> var_ctxt -> var_ctxt
    5.12 @@ -175,9 +173,6 @@
    5.13      SOME name' => name'
    5.14    | NONE => error ("Invalid name in context: " ^ quote name);
    5.15  
    5.16 -val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
    5.17 -val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
    5.18 -
    5.19  fun aux_params vars lhss =
    5.20    let
    5.21      fun fish_param _ (w as SOME _) = w
     6.1 --- a/src/Tools/Code/code_scala.ML	Thu May 01 09:30:35 2014 +0200
     6.2 +++ b/src/Tools/Code/code_scala.ML	Thu May 01 09:30:36 2014 +0200
     6.3 @@ -31,8 +31,8 @@
     6.4      val deresolve_const = deresolve o Constant;
     6.5      val deresolve_tyco = deresolve o Type_Constructor;
     6.6      val deresolve_class = deresolve o Type_Class;
     6.7 -    fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
     6.8 -    fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
     6.9 +    fun lookup_tyvar tyvars = lookup_var tyvars o Name.enforce_case true;
    6.10 +    fun intro_tyvars vs = intro_vars (map (Name.enforce_case true o fst) vs);
    6.11      fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
    6.12            (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
    6.13      and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    6.14 @@ -308,7 +308,7 @@
    6.15      fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
    6.16        let
    6.17          val (base', nsp_common') =
    6.18 -          Name.variant (if upper then first_upper base else base) nsp_common
    6.19 +          Name.variant (if upper then Name.enforce_case true base else base) nsp_common
    6.20        in
    6.21          (base',
    6.22            ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))