src/Pure/library.ML
changeset 4621 79e6a11ba8a9
parent 4616 d257e6c6614f
child 4629 401dd9b1b548
     1.1 --- a/src/Pure/library.ML	Thu Feb 12 14:52:17 1998 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Feb 12 14:53:00 1998 +0100
     1.3 @@ -5,15 +5,241 @@
     1.4  
     1.5  Basic library: functions, options, pairs, booleans, lists, integers,
     1.6  strings, lists as sets, association lists, generic tables, balanced
     1.7 -trees, orders, diagnostics, timing, misc functions.
     1.8 +trees, orders, I/O and diagnostics, timing, misc.
     1.9  *)
    1.10  
    1.11  infix |> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
    1.12    mem mem_int mem_string union union_int union_string inter inter_int
    1.13    inter_string subset subset_int subset_string;
    1.14  
    1.15 +signature LIBRARY =
    1.16 +sig
    1.17 +  (*functions*)
    1.18 +  val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
    1.19 +  val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
    1.20 +  val I: 'a -> 'a
    1.21 +  val K: 'a -> 'b -> 'a
    1.22 +  val |> : 'a * ('a -> 'b) -> 'b
    1.23 +  val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    1.24 +  val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
    1.25 +  val funpow: int -> ('a -> 'a) -> 'a -> 'a
    1.26  
    1.27 -structure Library =
    1.28 +  (*stamps*)
    1.29 +  type stamp
    1.30 +  val stamp: unit -> stamp
    1.31 +
    1.32 +  (*options*)
    1.33 +  datatype 'a option = None | Some of 'a
    1.34 +  exception OPTION
    1.35 +  val the: 'a option -> 'a
    1.36 +  val if_none: 'a option -> 'a -> 'a
    1.37 +  val is_some: 'a option -> bool
    1.38 +  val is_none: 'a option -> bool
    1.39 +  val apsome: ('a -> 'b) -> 'a option -> 'b option
    1.40 +  val can: ('a -> 'b) -> 'a -> bool
    1.41 +  val try: ('a -> 'b) -> 'a -> 'b option
    1.42 +
    1.43 +  (*pairs*)
    1.44 +  val pair: 'a -> 'b -> 'a * 'b
    1.45 +  val rpair: 'a -> 'b -> 'b * 'a
    1.46 +  val fst: 'a * 'b -> 'a
    1.47 +  val snd: 'a * 'b -> 'b
    1.48 +  val eq_fst: (''a * 'b) * (''a * 'c) -> bool
    1.49 +  val eq_snd: ('a * ''b) * ('c * ''b) -> bool
    1.50 +  val swap: 'a * 'b -> 'b * 'a
    1.51 +  val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c
    1.52 +  val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b
    1.53 +  val pairself: ('a -> 'b) -> 'a * 'a -> 'b * 'b
    1.54 +
    1.55 +  (*booleans*)
    1.56 +  val equal: ''a -> ''a -> bool
    1.57 +  val not_equal: ''a -> ''a -> bool
    1.58 +  val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool
    1.59 +  val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
    1.60 +  val exists: ('a -> bool) -> 'a list -> bool
    1.61 +  val forall: ('a -> bool) -> 'a list -> bool
    1.62 +  val set: bool ref -> bool
    1.63 +  val reset: bool ref -> bool
    1.64 +  val toggle: bool ref -> bool
    1.65 +  val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    1.66 +
    1.67 +  (*lists*)
    1.68 +  exception LIST of string
    1.69 +  val null: 'a list -> bool
    1.70 +  val hd: 'a list -> 'a
    1.71 +  val tl: 'a list -> 'a list
    1.72 +  val cons: 'a -> 'a list -> 'a list
    1.73 +  val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
    1.74 +  val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    1.75 +  val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.76 +  val length: 'a list -> int
    1.77 +  val take: int * 'a list -> 'a list
    1.78 +  val drop: int * 'a list -> 'a list
    1.79 +  val nth_elem: int * 'a list -> 'a
    1.80 +  val last_elem: 'a list -> 'a
    1.81 +  val split_last: 'a list -> 'a list * 'a
    1.82 +  val find_index: ('a -> bool) -> 'a list -> int
    1.83 +  val find_index_eq: ''a -> ''a list -> int
    1.84 +  val find_first: ('a -> bool) -> 'a list -> 'a option
    1.85 +  val flat: 'a list list -> 'a list
    1.86 +  val seq: ('a -> unit) -> 'a list -> unit
    1.87 +  val separate: 'a -> 'a list -> 'a list
    1.88 +  val replicate: int -> 'a -> 'a list
    1.89 +  val multiply: 'a list * 'a list list -> 'a list list
    1.90 +  val filter: ('a -> bool) -> 'a list -> 'a list
    1.91 +  val filter_out: ('a -> bool) -> 'a list -> 'a list
    1.92 +  val mapfilter: ('a -> 'b option) -> 'a list -> 'b list
    1.93 +  val map2: ('a * 'b -> 'c) -> 'a list * 'b list -> 'c list
    1.94 +  val exists2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.95 +  val forall2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.96 +  val ~~ : 'a list * 'b list -> ('a * 'b) list
    1.97 +  val split_list: ('a * 'b) list -> 'a list * 'b list
    1.98 +  val prefix: ''a list * ''a list -> bool
    1.99 +  val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   1.100 +  val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   1.101 +
   1.102 +  (*integers*)
   1.103 +  val inc: int ref -> int
   1.104 +  val dec: int ref -> int
   1.105 +  val upto: int * int -> int list
   1.106 +  val downto: int * int -> int list
   1.107 +  val downto0: int list * int -> bool
   1.108 +  val radixpand: int * int -> int list
   1.109 +  val radixstring: int * string * int -> string
   1.110 +  val string_of_int: int -> string
   1.111 +  val string_of_indexname: string * int -> string
   1.112 +
   1.113 +  (*strings*)
   1.114 +  val is_letter: string -> bool
   1.115 +  val is_digit: string -> bool
   1.116 +  val is_quasi_letter: string -> bool
   1.117 +  val is_blank: string -> bool
   1.118 +  val is_letdig: string -> bool
   1.119 +  val is_printable: string -> bool
   1.120 +  val to_lower: string -> string
   1.121 +  val enclose: string -> string -> string -> string
   1.122 +  val quote: string -> string
   1.123 +  val space_implode: string -> string list -> string
   1.124 +  val commas: string list -> string
   1.125 +  val commas_quote: string list -> string
   1.126 +  val cat_lines: string list -> string
   1.127 +  val space_explode: string -> string -> string list
   1.128 +  val split_lines: string -> string list
   1.129 +
   1.130 +  (*lists as sets*)
   1.131 +  val mem: ''a * ''a list -> bool
   1.132 +  val mem_int: int * int list -> bool
   1.133 +  val mem_string: string * string list -> bool
   1.134 +  val gen_mem: ('a * 'b -> bool) -> 'a * 'b list -> bool
   1.135 +  val ins: ''a * ''a list -> ''a list
   1.136 +  val ins_int: int * int list -> int list
   1.137 +  val ins_string: string * string list -> string list
   1.138 +  val gen_ins: ('a * 'a -> bool) -> 'a * 'a list -> 'a list
   1.139 +  val union: ''a list * ''a list -> ''a list
   1.140 +  val union_int: int list * int list -> int list
   1.141 +  val union_string: string list * string list -> string list
   1.142 +  val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   1.143 +  val inter: ''a list * ''a list -> ''a list
   1.144 +  val inter_int: int list * int list -> int list
   1.145 +  val inter_string: string list * string list -> string list
   1.146 +  val subset: ''a list * ''a list -> bool
   1.147 +  val subset_int: int list * int list -> bool
   1.148 +  val subset_string: string list * string list -> bool
   1.149 +  val eq_set: ''a list * ''a list -> bool
   1.150 +  val eq_set_string: string list * string list -> bool
   1.151 +  val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   1.152 +  val \ : ''a list * ''a -> ''a list
   1.153 +  val \\ : ''a list * ''a list -> ''a list
   1.154 +  val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
   1.155 +  val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
   1.156 +  val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   1.157 +  val distinct: ''a list -> ''a list
   1.158 +  val findrep: ''a list -> ''a list
   1.159 +  val gen_duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   1.160 +  val duplicates: ''a list -> ''a list
   1.161 +
   1.162 +  (*association lists*)
   1.163 +  val assoc: (''a * 'b) list * ''a -> 'b option
   1.164 +  val assoc_int: (int * 'a) list * int -> 'a option
   1.165 +  val assoc_string: (string * 'a) list * string -> 'a option
   1.166 +  val assoc_string_int: ((string * int) * 'a) list * (string * int) -> 'a option
   1.167 +  val assocs: (''a * 'b list) list -> ''a -> 'b list
   1.168 +  val assoc2: (''a * (''b * 'c) list) list * (''a * ''b) -> 'c option
   1.169 +  val gen_assoc: ('a * 'b -> bool) -> ('b * 'c) list * 'a -> 'c option
   1.170 +  val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
   1.171 +  val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
   1.172 +
   1.173 +  (*generic tables*)
   1.174 +  val generic_extend: ('a * 'a -> bool)
   1.175 +    -> ('b -> 'a list) -> ('a list -> 'b) -> 'b -> 'a list -> 'b
   1.176 +  val generic_merge: ('a * 'a -> bool) -> ('b -> 'a list) -> ('a list -> 'b) -> 'b -> 'b -> 'b
   1.177 +  val extend_list: ''a list -> ''a list -> ''a list
   1.178 +  val merge_lists: ''a list -> ''a list -> ''a list
   1.179 +  val merge_rev_lists: ''a list -> ''a list -> ''a list
   1.180 +
   1.181 +  (*balanced trees*)
   1.182 +  exception Balance
   1.183 +  val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a
   1.184 +  val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a
   1.185 +  val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
   1.186 +
   1.187 +  (*orders*)
   1.188 +  datatype order = EQUAL | GREATER | LESS
   1.189 +  val rev_order: order -> order
   1.190 +  val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
   1.191 +  val int_ord: int * int -> order
   1.192 +  val string_ord: string * string -> order
   1.193 +  val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
   1.194 +  val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
   1.195 +  val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
   1.196 +  val sort: ('a * 'a -> order) -> 'a list -> 'a list
   1.197 +  val sort_strings: string list -> string list
   1.198 +  val sort_wrt: ('a -> string) -> 'a list -> 'a list
   1.199 +
   1.200 +  (*I/O and diagnostics*)
   1.201 +  val cd: string -> unit
   1.202 +  val pwd: unit -> string
   1.203 +  val prs_fn: (string -> unit) ref
   1.204 +  val warning_fn: (string -> unit) ref
   1.205 +  val error_fn: (string -> unit) ref
   1.206 +  val prs: string -> unit
   1.207 +  val writeln: string -> unit
   1.208 +  val warning: string -> unit
   1.209 +  exception ERROR
   1.210 +  val error_msg: string -> unit
   1.211 +  val error: string -> 'a
   1.212 +  val sys_error: string -> 'a
   1.213 +  val assert: bool -> string -> unit
   1.214 +  val deny: bool -> string -> unit
   1.215 +  val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
   1.216 +  datatype 'a error = Error of string | OK of 'a
   1.217 +  val get_error: 'a error -> string option
   1.218 +  val get_ok: 'a error -> 'a option
   1.219 +  val handle_error: ('a -> 'b) -> 'a -> 'b error
   1.220 +
   1.221 +  (*timing*)
   1.222 +  val cond_timeit: bool -> (unit -> 'a) -> 'a
   1.223 +  val timeit: (unit -> 'a) -> 'a
   1.224 +  val timeap: ('a -> 'b) -> 'a -> 'b
   1.225 +
   1.226 +  (*misc*)
   1.227 +  val make_keylist: ('a -> 'b) -> 'a list -> ('a * 'b) list
   1.228 +  val keyfilter: ('a * ''b) list -> ''b -> 'a list
   1.229 +  val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
   1.230 +  val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   1.231 +  val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   1.232 +  val transitive_closure: (string * string list) list -> (string * string list) list
   1.233 +  val init_gensym: unit -> unit
   1.234 +  val gensym: string -> string
   1.235 +  val bump_int_list: string list -> string list
   1.236 +  val bump_list: string list * string -> string list
   1.237 +  val bump_string: string -> string
   1.238 +  val scanwords: (string -> bool) -> string list -> string list
   1.239 +  datatype 'a mtree = Join of 'a * 'a mtree list
   1.240 +  type object
   1.241 +end;
   1.242 +
   1.243 +structure Library: LIBRARY =
   1.244  struct
   1.245  
   1.246  (** functions **)
   1.247 @@ -748,6 +974,31 @@
   1.248    prod_ord int_ord (dict_ord elem_ord) ((length xs, xs), (length ys, ys));
   1.249  
   1.250  
   1.251 +(* sorting *)
   1.252 +
   1.253 +(*quicksort (stable, i.e. does not reorder equal elements)*)
   1.254 +fun sort ord =
   1.255 +  let
   1.256 +    fun qsort xs =
   1.257 +      let val len = length xs in
   1.258 +        if len <= 1 then xs
   1.259 +        else
   1.260 +          let val (lts, eqs, gts) = part (nth_elem (len div 2, xs)) xs in
   1.261 +            qsort lts @ eqs @ qsort gts
   1.262 +          end
   1.263 +      end
   1.264 +    and part _ [] = ([], [], [])
   1.265 +      | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
   1.266 +    and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts)
   1.267 +      | add EQUAL x (lts, eqs, gts) = (lts, x :: eqs, gts)
   1.268 +      | add GREATER x (lts, eqs, gts) = (lts, eqs, x :: gts);
   1.269 +  in qsort end;
   1.270 +
   1.271 +(*sort strings*)
   1.272 +val sort_strings = sort string_ord;
   1.273 +fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
   1.274 +
   1.275 +
   1.276  
   1.277  (** input / output and diagnostics **)
   1.278  
   1.279 @@ -837,7 +1088,7 @@
   1.280  
   1.281  
   1.282  
   1.283 -(** misc functions **)
   1.284 +(** misc **)
   1.285  
   1.286  (*use the keyfun to make a list of (x, key) pairs*)
   1.287  fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =
   1.288 @@ -882,31 +1133,6 @@
   1.289    in  part i end;
   1.290  
   1.291  
   1.292 -(* sorting *)
   1.293 -
   1.294 -(*quicksort (stable, i.e. does not reorder equal elements)*)
   1.295 -fun sort ord =
   1.296 -  let
   1.297 -    fun qsort xs =
   1.298 -      let val len = length xs in
   1.299 -        if len <= 1 then xs
   1.300 -        else
   1.301 -          let val (lts, eqs, gts) = part (nth_elem (len div 2, xs)) xs in
   1.302 -            qsort lts @ eqs @ qsort gts
   1.303 -          end
   1.304 -      end
   1.305 -    and part _ [] = ([], [], [])
   1.306 -      | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
   1.307 -    and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts)
   1.308 -      | add EQUAL x (lts, eqs, gts) = (lts, x :: eqs, gts)
   1.309 -      | add GREATER x (lts, eqs, gts) = (lts, eqs, x :: gts);
   1.310 -  in qsort end;
   1.311 -
   1.312 -(*sort strings*)
   1.313 -val sort_strings = sort string_ord;
   1.314 -fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
   1.315 -
   1.316 -
   1.317  (* transitive closure (not Warshall's algorithm) *)
   1.318  
   1.319  fun transitive_closure [] = []