# HG changeset patch # User haftmann # Date 1153839086 -7200 # Node ID 956cd30ef3bebbe59df6b74672f7599e7fd518ff # Parent b43fd26e1aaa8edd756b023494a3536ffa233ba3 renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum diff -r b43fd26e1aaa -r 956cd30ef3be src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Tue Jul 25 16:43:47 2006 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Tue Jul 25 16:51:26 2006 +0200 @@ -364,7 +364,7 @@ in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end; fun mk_cons tyco (c, tys) = let - val ts = Name.give_names Name.context "a" tys; + val ts = Name.names Name.context "a" tys; val ty = tys ---> Type (tyco, map TFree vs); in list_comb (Const (c, ty), map Free ts) end; in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css @@ -379,7 +379,7 @@ | SOME insts => let fun proven ((tyco, asorts), sort) = Sorts.of_sort (Sign.classes_of thy) - (Type (tyco, map TFree (Name.give_names Name.context "'a" asorts)), sort); + (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort); val (arities, css) = (split_list o map_filter (fn (tyco, (arity, cs)) => if proven arity then NONE else SOME (arity, (tyco, cs)))) insts; @@ -395,7 +395,7 @@ fun dest_case_app cs ts tys = let - val abs = Name.give_names Name.context "a" (Library.drop (length ts, tys)); + val abs = Name.names Name.context "a" (Library.drop (length ts, tys)); val (ts', t) = split_last (ts @ map Free abs); val (tys', sty) = split_last tys; fun freenames_of t = fold_aterms diff -r b43fd26e1aaa -r 956cd30ef3be src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Tue Jul 25 16:43:47 2006 +0200 +++ b/src/Pure/General/symbol.ML Tue Jul 25 16:51:26 2006 +0200 @@ -60,6 +60,7 @@ val default_raw: string -> string val xsymbolsN: string val symbol_output: string -> string * real + val alphanum: string -> string end; structure Symbol: SYMBOL = @@ -516,6 +517,26 @@ in (implode (map out syms), real (sym_length syms)) end; +(*turning arbitrary names into alphanumerics*) + +fun alphanum s = + let + fun replace_invalid c (last_inv, cs) = + if ((Char.isAlphaNum o the o Char.fromString) c orelse c = "'") + andalso not ("." = c) + then (false, if last_inv then c :: "_" :: cs else c :: cs) + else (true, cs); + fun prefix_num_empty [] = ["x"] + | prefix_num_empty (cs as c::_) = + if (Char.isDigit o the o Char.fromString) c + then "x" :: cs + else cs; + val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs); + val (_, cs2) = fold_rev replace_invalid cs1 (false, []); + val cs3 = prefix_num_empty cs2; + in implode (prefix :: cs3) end; + + (*final declarations of this structure!*) val length = sym_length; val explode = sym_explode; diff -r b43fd26e1aaa -r 956cd30ef3be src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Tue Jul 25 16:43:47 2006 +0200 +++ b/src/Pure/Tools/class_package.ML Tue Jul 25 16:51:26 2006 +0200 @@ -461,7 +461,7 @@ end; fun get_consts_sort (tyco, asorts, sort) = let - val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.give_names Name.context "'a" asorts)) + val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts)) in maps (get_consts_class tyco ty) (the_ancestry theory sort) end; val cs = maps get_consts_sort arities; fun read_defs defs cs thy_read = diff -r b43fd26e1aaa -r 956cd30ef3be src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Jul 25 16:43:47 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Tue Jul 25 16:51:26 2006 +0200 @@ -756,7 +756,7 @@ |-> (fn ty => pair (IVar v)) | exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns = let - val (v, t) = Term.variant_abs (Name.alphanum raw_v, ty, raw_t); + val (v, t) = Term.variant_abs (Symbol.alphanum raw_v, ty, raw_t); in trns |> exprgen_type thy tabs ty @@ -792,7 +792,7 @@ if length ts < i then let val tys = Library.take (i - length ts, ((fst o strip_type) ty)); - val vs = Name.give_names (Name.declare f Name.context) "a" tys; + val vs = Name.names (Name.declare f Name.context) "a" tys; in trns |> fold_map (exprgen_type thy tabs) tys diff -r b43fd26e1aaa -r 956cd30ef3be src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Jul 25 16:43:47 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Jul 25 16:51:26 2006 +0200 @@ -343,9 +343,9 @@ type src = string; val ord = string_ord; fun mk reserved_ml (name, 0) = - (Name.alphanum o NameSpace.base) name + (Symbol.alphanum o NameSpace.base) name | mk reserved_ml (name, i) = - (Name.alphanum o NameSpace.base) name ^ replicate_string i "'"; + (Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'"; fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml; fun maybe_unique _ _ = NONE; fun re_mangle _ dst = error ("no such definition name: " ^ quote dst); diff -r b43fd26e1aaa -r 956cd30ef3be src/Pure/Tools/codegen_theorems.ML --- a/src/Pure/Tools/codegen_theorems.ML Tue Jul 25 16:43:47 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Tue Jul 25 16:51:26 2006 +0200 @@ -225,7 +225,7 @@ (ctyp_of thy ty, ctyp_of thy (TVar ((v', maxidx), sort))) :: acc) end; val lower_name = implode o map (Char.toString o Char.toLower o the o Char.fromString) - o explode o Name.alphanum; + o explode o Symbol.alphanum; fun tvars_of thm = (fold_types o fold_atyps) (fn TVar (v_i as (v, i), sort) => cons (v_i, (lower_name v, sort)) | _ => I) (prop_of thm) []; @@ -244,7 +244,7 @@ (cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc) end; val lower_name = implode o map (Char.toString o Char.toLower o the o Char.fromString) - o explode o Name.alphanum; + o explode o Symbol.alphanum; fun vars_of thm = fold_aterms (fn Var (v_i as (v, i), ty) => cons (v_i, (lower_name v, ty)) | _ => I) (prop_of thm) []; diff -r b43fd26e1aaa -r 956cd30ef3be src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Jul 25 16:43:47 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Jul 25 16:51:26 2006 +0200 @@ -370,7 +370,7 @@ val j = length es; val l = k - j; val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty; - val vs_tys = Name.give_names (fold Name.declare (fold add_varnames es []) Name.context) "a" tys; + val vs_tys = Name.names (fold Name.declare (fold add_varnames es []) Name.context) "a" tys; in vs_tys `|--> IConst c `$$ es @ map (fn (v, _) => IVar v) vs_tys end; diff -r b43fd26e1aaa -r 956cd30ef3be src/Pure/name.ML --- a/src/Pure/name.ML Tue Jul 25 16:43:47 2006 +0200 +++ b/src/Pure/name.ML Tue Jul 25 16:51:26 2006 +0200 @@ -21,12 +21,11 @@ val declare: string -> context -> context val is_declared: context -> string -> bool val invents: context -> string -> int -> string list - val give_names: context -> string -> 'a list -> (string * 'a) list + val names: context -> string -> 'a list -> (string * 'a) list val invent_list: string list -> string -> int -> string list val variants: string list -> context -> string list * context val variant_list: string list -> string list -> string list val variant: string list -> string -> string - val alphanum: string -> string end; structure Name: NAME = @@ -101,7 +100,7 @@ in invs o clean end; val invent_list = invents o make_context; -fun give_names ctxt x xs = invents ctxt x (length xs) ~~ xs; +fun names ctxt x xs = invents ctxt x (length xs) ~~ xs; (* variants *) @@ -131,24 +130,4 @@ fun variant_list used names = #1 (make_context used |> variants names); fun variant used = singleton (variant_list used); - -(*turning arbitrary names into alphanumerics*) - -fun alphanum s = - let - fun replace_invalid c (last_inv, cs) = - if ((Char.isAlphaNum o the o Char.fromString) c orelse c = "'") - andalso not (NameSpace.separator = c) - then (false, if last_inv then c :: "_" :: cs else c :: cs) - else (true, cs); - fun prefix_num_empty [] = ["x"] - | prefix_num_empty (cs as c::_) = - if (Char.isDigit o the o Char.fromString) c - then "x" :: cs - else cs; - val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs); - val (_, cs2) = fold_rev replace_invalid cs1 (false, []); - val cs3 = prefix_num_empty cs2; - in implode (prefix :: cs3) end; - end;