src/Tools/Metis/src/Useful.sig
author paulson
Tue, 13 Nov 2007 18:29:28 +0100
changeset 25430 372d6749f00e
parent 23510 4521fead5609
child 39353 7f11d833d65b
permissions -rw-r--r--
patching in the latest changes from Hurd
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     1
(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     2
(* ML UTILITY FUNCTIONS                                                      *)
23510
4521fead5609 GPL -> BSD
paulson
parents: 23442
diff changeset
     3
(* Copyright (c) 2001-2005 Joe Hurd, distributed under the BSD License *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     4
(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     5
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     6
signature Useful =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     7
sig
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     8
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    10
(* Exceptions.                                                               *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    12
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    13
exception Error of string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    14
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    15
exception Bug of string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    16
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    17
val partial : exn -> ('a -> 'b option) -> 'a -> 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    18
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    19
val total : ('a -> 'b) -> 'a -> 'b option
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    20
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    21
val can : ('a -> 'b) -> 'a -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    22
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    23
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    24
(* Tracing.                                                                  *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    25
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    26
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    27
val tracePrint : (string -> unit) ref
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    28
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    29
val trace : string -> unit
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    30
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    31
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    32
(* Combinators.                                                              *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    33
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    34
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    35
val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    36
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    37
val I : 'a -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    38
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    39
val K : 'a -> 'b -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    40
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    41
val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    42
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    43
val W : ('a -> 'a -> 'b) -> 'a -> 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    44
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    45
val funpow : int -> ('a -> 'a) -> 'a -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    46
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    47
val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    48
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    49
val equal : ''a -> ''a -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    50
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    51
val notEqual : ''a -> ''a -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    52
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    53
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    54
(* Pairs.                                                                    *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    55
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    56
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    57
val fst : 'a * 'b -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    58
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    59
val snd : 'a * 'b -> 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    60
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    61
val pair : 'a -> 'b -> 'a * 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    62
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    63
val swap : 'a * 'b -> 'b * 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    64
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    65
val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    66
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    67
val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    68
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    69
val ## : ('a -> 'c) * ('b -> 'd) -> 'a * 'b -> 'c * 'd
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    70
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    71
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    72
(* State transformers.                                                       *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    73
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    74
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    75
val unit : 'a -> 's -> 'a * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    76
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    77
val bind : ('s -> 'a * 's) -> ('a -> 's -> 'b * 's) -> 's -> 'b * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    78
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    79
val mmap : ('a -> 'b) -> ('s -> 'a * 's) -> 's -> 'b * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    80
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    81
val mjoin : ('s -> ('s -> 'a * 's) * 's) -> 's -> 'a * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    82
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    83
val mwhile : ('a -> bool) -> ('a -> 's -> 'a * 's) -> 'a -> 's -> 'a * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    84
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    85
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    86
(* Lists: note we count elements from 0.                                     *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    87
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    88
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    89
val cons : 'a -> 'a list -> 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    90
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    91
val hdTl : 'a list -> 'a * 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    92
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    93
val append : 'a list -> 'a list -> 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    94
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    95
val singleton : 'a -> 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    96
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    97
val first : ('a -> 'b option) -> 'a list -> 'b option
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    98
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    99
val index : ('a -> bool) -> 'a list -> int option
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   100
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   101
val maps : ('a -> 's -> 'b * 's) -> 'a list -> 's -> 'b list * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   102
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   103
val mapsPartial : ('a -> 's -> 'b option * 's) -> 'a list -> 's -> 'b list * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   104
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   105
val enumerate : 'a list -> (int * 'a) list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   106
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   107
val zipwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   108
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   109
val zip : 'a list -> 'b list -> ('a * 'b) list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   110
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   111
val unzip : ('a * 'b) list -> 'a list * 'b list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   112
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   113
val cartwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   114
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   115
val cart : 'a list -> 'b list -> ('a * 'b) list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   116
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   117
val divide : 'a list -> int -> 'a list * 'a list  (* Subscript *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   118
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   119
val revDivide : 'a list -> int -> 'a list * 'a list  (* Subscript *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   120
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   121
val updateNth : int * 'a -> 'a list -> 'a list  (* Subscript *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   122
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   123
val deleteNth : int -> 'a list -> 'a list  (* Subscript *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   124
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   125
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   126
(* Sets implemented with lists.                                              *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   127
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   128
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   129
val mem : ''a -> ''a list -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   130
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   131
val insert : ''a -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   132
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   133
val delete : ''a -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   134
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   135
val setify : ''a list -> ''a list  (* removes duplicates *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   136
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   137
val union : ''a list -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   138
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   139
val intersect : ''a list -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   140
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   141
val difference : ''a list -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   142
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   143
val subset : ''a list -> ''a list -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   144
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   145
val distinct : ''a list -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   146
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   147
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   148
(* Comparisons.                                                              *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   149
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   150
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   151
val mapCompare : ('a -> 'b) -> ('b * 'b -> order) -> 'a * 'a -> order
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   152
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   153
val revCompare : ('a * 'a -> order) -> 'a * 'a -> order
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   154
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   155
val prodCompare :
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   156
    ('a * 'a -> order) -> ('b * 'b -> order) -> ('a * 'b) * ('a * 'b) -> order
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   157
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   158
val lexCompare : ('a * 'a -> order) -> 'a list * 'a list -> order
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   159
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 23510
diff changeset
   160
val optionCompare : ('a * 'a -> order) -> 'a option * 'a option -> order
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 23510
diff changeset
   161
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   162
val boolCompare : bool * bool -> order  (* true < false *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   163
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   164
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   165
(* Sorting and searching.                                                    *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   166
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   167
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   168
val minimum : ('a * 'a -> order) -> 'a list -> 'a * 'a list  (* Empty *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   169
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   170
val maximum : ('a * 'a -> order) -> 'a list -> 'a * 'a list  (* Empty *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   171
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   172
val merge : ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   173
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   174
val sort : ('a * 'a -> order) -> 'a list -> 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   175
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   176
val sortMap : ('a -> 'b) -> ('b * 'b -> order) -> 'a list -> 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   177
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   178
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   179
(* Integers.                                                                 *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   180
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   181
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   182
val interval : int -> int -> int list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   183
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   184
val divides : int -> int -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   185
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   186
val gcd : int -> int -> int
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   187
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   188
val primes : int -> int list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   189
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   190
val primesUpTo : int -> int list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   191
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   192
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   193
(* Strings.                                                                  *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   194
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   195
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   196
val rot : int -> char -> char
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   197
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   198
val charToInt : char -> int option
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   199
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   200
val charFromInt : int -> char option
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   201
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   202
val nChars : char -> int -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   203
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   204
val chomp : string -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   205
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   206
val trim : string -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   207
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   208
val join : string -> string list -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   209
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   210
val split : string -> string -> string list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   211
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   212
val mkPrefix : string -> string -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   213
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   214
val destPrefix : string -> string -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   215
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   216
val isPrefix : string -> string -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   217
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   218
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   219
(* Tables.                                                                   *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   220
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   221
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   222
type columnAlignment = {leftAlign : bool, padChar : char}
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   223
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   224
val alignColumn : columnAlignment -> string list -> string list -> string list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   225
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   226
val alignTable : columnAlignment list -> string list list -> string list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   227
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   228
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   229
(* Reals.                                                                    *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   230
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   231
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   232
val percentToString : real -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   233
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   234
val pos : real -> real
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   235
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   236
val log2 : real -> real  (* Domain *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   237
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   238
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   239
(* Sum datatype.                                                             *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   240
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   241
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   242
datatype ('a,'b) sum = Left of 'a | Right of 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   243
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   244
val destLeft : ('a,'b) sum -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   245
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   246
val isLeft : ('a,'b) sum -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   247
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   248
val destRight : ('a,'b) sum -> 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   249
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   250
val isRight : ('a,'b) sum -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   251
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   252
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   253
(* Useful impure features.                                                   *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   254
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   255
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   256
val newInt : unit -> int
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   257
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   258
val newInts : int -> int list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   259
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 23510
diff changeset
   260
val withRef : 'r ref * 'r -> ('a -> 'b) -> 'a -> 'b
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   261
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 23510
diff changeset
   262
val cloneArray : 'a Array.array -> 'a Array.array
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   263
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   264
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   265
(* The environment.                                                          *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   266
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   267
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   268
val host : unit -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   269
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   270
val time : unit -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   271
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   272
val date : unit -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   273
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   274
val readTextFile : {filename : string} -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   275
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   276
val writeTextFile : {filename : string, contents : string} -> unit
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   277
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   278
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   279
(* Profiling and error reporting.                                            *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   280
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   281
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   282
val try : ('a -> 'b) -> 'a -> 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   283
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   284
val warn : string -> unit
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   285
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   286
val die : string -> 'exit
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   287
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   288
val timed : ('a -> 'b) -> 'a -> real * 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   289
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   290
val timedMany : ('a -> 'b) -> 'a -> real * 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   291
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   292
val executionTime : unit -> real  (* Wall clock execution time *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   293
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   294
end