src/Pure/library.ML
changeset 4063 0b19014b9155
parent 4046 f89dbf002604
child 4102 f746af27164b
     1.1 --- a/src/Pure/library.ML	Sat Nov 01 13:01:07 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Nov 01 13:01:57 1997 +0100
     1.3 @@ -78,8 +78,6 @@
     1.4    | merge_opts _ (None, some as Some _) = some
     1.5    | merge_opts merge (Some x, Some y) = Some (merge (x, y));
     1.6  
     1.7 -
     1.8 -
     1.9  (** pairs **)
    1.10  
    1.11  fun pair x y = (x, y);
    1.12 @@ -126,8 +124,12 @@
    1.13  
    1.14  (*Several object-logics declare theories named List or Option, hiding the
    1.15    eponymous basis library structures.*)
    1.16 -structure List_ = List
    1.17 -and       Option_ = Option;
    1.18 +structure Basis_Library =
    1.19 +    struct
    1.20 +    structure List = List
    1.21 +    and       Option = Option
    1.22 +    end;
    1.23 +
    1.24  
    1.25  (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
    1.26  fun exists (pred: 'a -> bool) : 'a list -> bool =
    1.27 @@ -1009,27 +1011,42 @@
    1.28  
    1.29  (* generating identifiers *)
    1.30  
    1.31 +(** Freshly generated identifiers; supplied prefix MUST start with a letter **)
    1.32  local
    1.33 -  val a = ord "a" and z = ord "z" and A = ord "A" and Z = ord "Z"
    1.34 -  and k0 = ord "0" and k9 = ord "9"
    1.35 +(*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
    1.36 +fun char i =      if i<26 then chr (ord "A" + i)
    1.37 +	     else if i<52 then chr (ord "a" + i - 26)
    1.38 +	     else if i<62 then chr (ord"0" + i - 52)
    1.39 +	     else if i=62 then "_"
    1.40 +	     else  (*i=63*)    "'";
    1.41 +
    1.42 +val charVec = Vector.tabulate (64, char);
    1.43 +
    1.44 +fun newid n = 
    1.45 +  let 
    1.46 +  in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end
    1.47  
    1.48    val seedr = ref 0;
    1.49 -in
    1.50  
    1.51 -(*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
    1.52 -fun newid n = 
    1.53 -  let fun char i =
    1.54 -               if i<26 then chr (A+i)
    1.55 -          else if i<52 then chr (a+i-26)
    1.56 -          else if i<62 then chr (k0+i-52)
    1.57 -          else if i=62 then "_"
    1.58 -          else  (*i=63*)    "'"
    1.59 -  in  implode (map char (radixpand (64,n)))  end;
    1.60 +in
    1.61 +fun init_gensym() = (seedr := 0);
    1.62  
    1.63 -(*Freshly generated identifiers with given prefix; MUST start with a letter*)
    1.64  fun gensym pre = pre ^ 
    1.65                   (#1(newid (!seedr), 
    1.66                       seedr := 1+ !seedr))
    1.67 +end;
    1.68 +
    1.69 +
    1.70 +local
    1.71 +(*Identifies those character codes legal in identifiers.
    1.72 +  chould use Basis Library character functions if Poly/ML provided characters*)
    1.73 +fun idCode k = (ord "a" <= k andalso k < ord "z") orelse 
    1.74 +               (ord "A" <= k andalso k < ord "Z") orelse
    1.75 +               (ord "0" <= k andalso k < ord "9");
    1.76 +
    1.77 +val idCodeVec = Vector.tabulate (256, idCode);
    1.78 +
    1.79 +in
    1.80  
    1.81  (*Increment a list of letters like a reversed base 26 number.
    1.82    If head is "z", bumps chars in tail.
    1.83 @@ -1037,8 +1054,10 @@
    1.84    "_" and "'" are not changed.
    1.85    For making variants of identifiers.*)
    1.86  
    1.87 -fun bump_int_list(c::cs) = if c="9" then "0" :: bump_int_list cs else
    1.88 -        if k0 <= ord(c) andalso ord(c) < k9 then chr(ord(c)+1) :: cs
    1.89 +fun bump_int_list(c::cs) = 
    1.90 +	if c="9" then "0" :: bump_int_list cs 
    1.91 +	else
    1.92 +        if "0" <= c andalso c < "9" then chr(ord(c)+1) :: cs
    1.93          else "1" :: c :: cs
    1.94    | bump_int_list([]) = error("bump_int_list: not an identifier");
    1.95  
    1.96 @@ -1047,12 +1066,13 @@
    1.97    | bump_list("z"::cs, _) = "a" :: bump_list(cs, "a")
    1.98    | bump_list("Z"::cs, _) = "A" :: bump_list(cs, "A")
    1.99    | bump_list("9"::cs, _) = "0" :: bump_int_list cs
   1.100 -  | bump_list(c::cs, _) = let val k = ord(c)
   1.101 -        in if (a <= k andalso k < z) orelse (A <= k andalso k < Z) orelse
   1.102 -              (k0 <= k andalso k < k9) then chr(k+1) :: cs else
   1.103 -           if c="'" orelse c="_" then c :: bump_list(cs, "") else
   1.104 -                error("bump_list: not legal in identifier: " ^
   1.105 -                        implode(rev(c::cs)))
   1.106 +  | bump_list(c::cs, _) = 
   1.107 +        let val k = ord(c)
   1.108 +        in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs 
   1.109 +	   else
   1.110 +           if c="'" orelse c="_" then c :: bump_list(cs, "") 
   1.111 +	   else error("bump_list: not legal in identifier: " ^
   1.112 +		      implode(rev(c::cs)))
   1.113          end;
   1.114  
   1.115  end;