src/Pure/library.ML
changeset 32737 76fa673eee8b
parent 32352 4839a704939a
child 32966 5b21661fe618
equal deleted inserted replaced
32736:f126e68d003d 32737:76fa673eee8b
    55   val not_equal: ''a -> ''a -> bool
    55   val not_equal: ''a -> ''a -> bool
    56   val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool
    56   val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool
    57   val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
    57   val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
    58   val exists: ('a -> bool) -> 'a list -> bool
    58   val exists: ('a -> bool) -> 'a list -> bool
    59   val forall: ('a -> bool) -> 'a list -> bool
    59   val forall: ('a -> bool) -> 'a list -> bool
    60   val set: bool ref -> bool
    60   val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    61   val reset: bool ref -> bool
    61   val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    62   val toggle: bool ref -> bool
       
    63   val change: 'a ref -> ('a -> 'a) -> unit
       
    64   val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
       
    65   val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
       
    66   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
       
    67   val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
    62   val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
    68 
    63 
    69   (*lists*)
    64   (*lists*)
    70   exception UnequalLengths
    65   exception UnequalLengths
    71   val single: 'a -> 'a list
    66   val single: 'a -> 'a list
   121   val prefixes: 'a list -> 'a list list
   116   val prefixes: 'a list -> 'a list list
   122   val suffixes1: 'a list -> 'a list list
   117   val suffixes1: 'a list -> 'a list list
   123   val suffixes: 'a list -> 'a list list
   118   val suffixes: 'a list -> 'a list list
   124 
   119 
   125   (*integers*)
   120   (*integers*)
   126   val inc: int ref -> int
       
   127   val dec: int ref -> int
       
   128   val upto: int * int -> int list
   121   val upto: int * int -> int list
   129   val downto: int * int -> int list
   122   val downto: int * int -> int list
   130   val radixpand: int * int -> int list
   123   val radixpand: int * int -> int list
   131   val radixstring: int * string * int -> string
   124   val radixstring: int * string * int -> string
   132   val string_of_int: int -> string
   125   val string_of_int: int -> string
   324 val forall = List.all;
   317 val forall = List.all;
   325 
   318 
   326 
   319 
   327 (* flags *)
   320 (* flags *)
   328 
   321 
   329 fun set flag = (flag := true; true);
       
   330 fun reset flag = (flag := false; false);
       
   331 fun toggle flag = (flag := not (! flag); ! flag);
       
   332 
       
   333 fun change r f = r := f (! r);
       
   334 fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
       
   335 
       
   336 (*temporarily set flag during execution*)
   322 (*temporarily set flag during execution*)
   337 fun setmp_noncritical flag value f x =
   323 fun setmp_noncritical flag value f x =
   338   uninterruptible (fn restore_attributes => fn () =>
   324   uninterruptible (fn restore_attributes => fn () =>
   339     let
   325     let
   340       val orig_value = ! flag;
   326       val orig_value = ! flag;
   640 fun suffixes xs = [] :: suffixes1 xs;
   626 fun suffixes xs = [] :: suffixes1 xs;
   641 
   627 
   642 
   628 
   643 
   629 
   644 (** integers **)
   630 (** integers **)
   645 
       
   646 fun inc i = (i := ! i + (1: int); ! i);
       
   647 fun dec i = (i := ! i - (1: int); ! i);
       
   648 
       
   649 
   631 
   650 (* lists of integers *)
   632 (* lists of integers *)
   651 
   633 
   652 (*make the list [from, from + 1, ..., to]*)
   634 (*make the list [from, from + 1, ..., to]*)
   653 fun ((i: int) upto j) =
   635 fun ((i: int) upto j) =
  1053 fun rmod x y = x - y * Real.realFloor (x / y);
  1035 fun rmod x y = x - y * Real.realFloor (x / y);
  1054 
  1036 
  1055 local
  1037 local
  1056   val a = 16807.0;
  1038   val a = 16807.0;
  1057   val m = 2147483647.0;
  1039   val m = 2147483647.0;
  1058   val random_seed = ref 1.0;
  1040   val random_seed = Unsynchronized.ref 1.0;
  1059 in
  1041 in
  1060 
  1042 
  1061 fun random () = CRITICAL (fn () =>
  1043 fun random () = CRITICAL (fn () =>
  1062   let val r = rmod (a * ! random_seed) m
  1044   let val r = rmod (a * ! random_seed) m
  1063   in (random_seed := r; r) end);
  1045   in (random_seed := r; r) end);
  1119   else chr (ord "0" + i - 52);
  1101   else chr (ord "0" + i - 52);
  1120 
  1102 
  1121 val char_vec = Vector.tabulate (62, gensym_char);
  1103 val char_vec = Vector.tabulate (62, gensym_char);
  1122 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
  1104 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
  1123 
  1105 
  1124 val gensym_seed = ref (0: int);
  1106 val gensym_seed = Unsynchronized.ref (0: int);
  1125 
  1107 
  1126 in
  1108 in
  1127   fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
  1109   fun gensym pre =
       
  1110     pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
  1128 end;
  1111 end;
  1129 
  1112 
  1130 
  1113 
  1131 (* stamps and serial numbers *)
  1114 (* stamps and serial numbers *)
  1132 
  1115 
  1133 type stamp = unit ref;
  1116 type stamp = unit Unsynchronized.ref;
  1134 val stamp: unit -> stamp = ref;
  1117 val stamp: unit -> stamp = Unsynchronized.ref;
  1135 
  1118 
  1136 type serial = int;
  1119 type serial = int;
  1137 val serial = Multithreading.serial;
  1120 val serial = Multithreading.serial;
  1138 val serial_string = string_of_int o serial;
  1121 val serial_string = string_of_int o serial;
  1139 
  1122