added serial numbers;
authorwenzelm
Fri Jun 17 18:33:24 2005 +0200 (2005-06-17)
changeset 164390509ef1b1ec3
parent 16438 1093f2400411
child 16440 9b6e6d5fba05
added serial numbers;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Jun 17 18:33:23 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Jun 17 18:33:24 2005 +0200
     1.3 @@ -31,10 +31,6 @@
     1.4    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
     1.5    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
     1.6  
     1.7 -  (*stamps*)
     1.8 -  type stamp
     1.9 -  val stamp: unit -> stamp
    1.10 -
    1.11    (*old options -- invalidated*)
    1.12    datatype invalid = None of invalid
    1.13    exception OPTION of invalid
    1.14 @@ -261,6 +257,10 @@
    1.15    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
    1.16    val gensym: string -> string
    1.17    val scanwords: (string -> bool) -> string list -> string list
    1.18 +  type stamp
    1.19 +  val stamp: unit -> stamp
    1.20 +  type serial
    1.21 +  val serial: unit -> serial
    1.22  end;
    1.23  
    1.24  signature LIBRARY =
    1.25 @@ -312,13 +312,6 @@
    1.26  
    1.27  
    1.28  
    1.29 -(** stamps **)
    1.30 -
    1.31 -type stamp = unit ref;
    1.32 -val stamp: unit -> stamp = ref;
    1.33 -
    1.34 -
    1.35 -
    1.36  (** options **)
    1.37  
    1.38  (*invalidate former constructors to prevent accidental use as match-all patterns!*)
    1.39 @@ -665,12 +658,12 @@
    1.40  
    1.41  (** integers **)
    1.42  
    1.43 -fun gcd(x,y) =
    1.44 +fun gcd (x, y) =
    1.45    let fun gxd x y : IntInf.int =
    1.46      if y = 0 then x else gxd y (x mod y)
    1.47    in if x < y then gxd y x else gxd x y end;
    1.48  
    1.49 -fun lcm(x,y) = (x * y) div gcd(x,y);
    1.50 +fun lcm (x, y) = (x * y) div gcd (x, y);
    1.51  
    1.52  fun inc i = (i := ! i + 1; ! i);
    1.53  fun dec i = (i := ! i - 1; ! i);
    1.54 @@ -906,11 +899,11 @@
    1.55    | (x :: xs) subset ys = x mem ys andalso xs subset ys;
    1.56  
    1.57  (*subset, optimized version for ints*)
    1.58 -fun ([]:int list) subset_int ys = true
    1.59 +fun ([]: int list) subset_int ys = true
    1.60    | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
    1.61  
    1.62  (*subset, optimized version for strings*)
    1.63 -fun ([]:string list) subset_string ys = true
    1.64 +fun ([]: string list) subset_string ys = true
    1.65    | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
    1.66  
    1.67  (*set equality*)
    1.68 @@ -918,7 +911,7 @@
    1.69    xs = ys orelse (xs subset ys andalso ys subset xs);
    1.70  
    1.71  (*set equality for strings*)
    1.72 -fun eq_set_string ((xs:string list), ys) =
    1.73 +fun eq_set_string ((xs: string list), ys) =
    1.74    xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
    1.75  
    1.76  fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
    1.77 @@ -1289,6 +1282,15 @@
    1.78    in scan1 (#2 (take_prefix (not o is_let) cs)) end;
    1.79  
    1.80  
    1.81 +(* stamps and serial numbers *)
    1.82 +
    1.83 +type stamp = unit ref;
    1.84 +val stamp: unit -> stamp = ref;
    1.85 +
    1.86 +type serial = int;
    1.87 +local val count = ref 0
    1.88 +in fun serial () = inc count end;
    1.89 +
    1.90  end;
    1.91  
    1.92  structure BasicLibrary: BASIC_LIBRARY = Library;