added give_names and alphanum
authorhaftmann
Fri Jul 21 14:45:25 2006 +0200 (2006-07-21)
changeset 20174c057b3618963
parent 20173 c8f791af9a60
child 20175 0a8ca32f6e64
added give_names and alphanum
src/Pure/name.ML
     1.1 --- a/src/Pure/name.ML	Fri Jul 21 14:11:14 2006 +0200
     1.2 +++ b/src/Pure/name.ML	Fri Jul 21 14:45:25 2006 +0200
     1.3 @@ -21,10 +21,12 @@
     1.4    val declare: string -> context -> context
     1.5    val is_declared: context -> string -> bool
     1.6    val invents: context -> string -> int -> string list
     1.7 +  val give_names: context -> string -> 'a list -> (string * 'a) list
     1.8    val invent_list: string list -> string -> int -> string list
     1.9    val variants: string list -> context -> string list * context
    1.10    val variant_list: string list -> string list -> string list
    1.11    val variant: string list -> string -> string
    1.12 +  val alphanum: string -> string
    1.13  end;
    1.14  
    1.15  structure Name: NAME =
    1.16 @@ -99,6 +101,7 @@
    1.17    in invs o clean end;
    1.18  
    1.19  val invent_list = invents o make_context;
    1.20 +fun give_names ctxt x xs = invents ctxt x (length xs) ~~ xs;
    1.21  
    1.22  
    1.23  (* variants *)
    1.24 @@ -128,4 +131,24 @@
    1.25  fun variant_list used names = #1 (make_context used |> variants names);
    1.26  fun variant used = singleton (variant_list used);
    1.27  
    1.28 +
    1.29 +(*turning arbitrary names into alphanumerics*)
    1.30 +
    1.31 +fun alphanum s =
    1.32 +  let
    1.33 +    fun replace_invalid c (last_inv, cs) =
    1.34 +      if ((Char.isAlphaNum o the o Char.fromString) c orelse c = "'")
    1.35 +        andalso not (NameSpace.separator = c)
    1.36 +      then (false, if last_inv then c :: "_" :: cs else c :: cs)
    1.37 +      else (true, cs);
    1.38 +    fun prefix_num_empty [] = ["x"]
    1.39 +      | prefix_num_empty (cs as c::_) =
    1.40 +          if (Char.isDigit o the o Char.fromString) c
    1.41 +          then "x" :: cs
    1.42 +          else cs;
    1.43 +    val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs);
    1.44 +    val (_, cs2) = fold_rev replace_invalid cs1 (false, []);
    1.45 +    val cs3 = prefix_num_empty cs2;
    1.46 +  in implode (prefix :: cs3) end;
    1.47 +
    1.48  end;