src/Tools/Metis/metis.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45778 df6e210fb44c
child 56281 03c3d1a7c3b8
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
     1
(*
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
     2
   This file was generated by the "make_metis" script. The BSD License is used
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
     3
   with Joe Hurd's kind permission. Extract from a September 13, 2010 email
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
     4
   written by Joe Hurd:
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
     5
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
     6
       I hereby give permission to the Isabelle team to release Metis as part
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
     7
       of Isabelle, with the Metis code covered under the Isabelle BSD
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
     8
       license.
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
     9
*)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    10
23442
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
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    13
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    14
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    15
(******************************************************************)
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
print_depth 0;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    18
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
    19
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
    20
(**** Original file: src/Random.sig ****)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    21
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    22
(*  Title:      Tools/random_word.ML
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    23
    Author:     Makarius
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    24
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    25
Simple generator for pseudo-random numbers, using unboxed word
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    26
arithmetic only.  Unprotected concurrency introduces some true
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    27
randomness.
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    28
*)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    29
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
    30
signature Metis_Random =
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    31
sig
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
    32
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    33
  val nextWord : unit -> word
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    34
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    35
  val nextBool : unit -> bool
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    36
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    37
  val nextInt : int -> int  (* k -> [0,k) *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    38
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    39
  val nextReal : unit -> real  (* () -> [0,1) *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    40
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    41
end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    42
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
    43
(**** Original file: src/Random.sml ****)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    44
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    45
(*  Title:      Tools/random_word.ML
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    46
    Author:     Makarius
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    47
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    48
Simple generator for pseudo-random numbers, using unboxed word
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    49
arithmetic only.  Unprotected concurrency introduces some true
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    50
randomness.
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    51
*)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    52
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
    53
structure Metis_Random :> Metis_Random =
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    54
struct
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    55
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    56
(* random words: 0w0 <= result <= max_word *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    57
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    58
(*minimum length of unboxed words on all supported ML platforms*)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    59
val _ = Word.wordSize >= 30
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    60
  orelse raise Fail ("Bad platform word size");
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    61
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    62
val max_word = 0wx3FFFFFFF;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    63
val top_bit = 0wx20000000;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    64
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    65
(*multiplier according to Borosh and Niederreiter (for modulus = 2^30),
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    66
  see http://random.mat.sbg.ac.at/~charly/server/server.html*)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    67
val a = 0w777138309;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    68
fun step x = Word.andb (a * x + 0w1, max_word);
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    69
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    70
fun change r f = r := f (!r);
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    71
local val rand = (*Unsynchronized.*)Unsynchronized.ref 0w1
39428
b42d9885c129 regenerated "metis.ML"
blanchet
parents: 39417
diff changeset
    72
in fun nextWord () = ((*Unsynchronized.*)change rand step; ! rand) end;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    73
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    74
(*NB: higher bits are more random than lower ones*)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    75
fun nextBool () = Word.andb (nextWord (), top_bit) = 0w0;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    76
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    77
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    78
(* random integers: 0 <= result < k *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    79
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    80
val max_int = Word.toInt max_word;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    81
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    82
fun nextInt k =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    83
  if k <= 0 orelse k > max_int then raise Fail ("next_int: out of range")
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    84
  else if k = max_int then Word.toInt (nextWord ())
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    85
  else Word.toInt (Word.mod (nextWord (), Word.fromInt k));
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    86
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    87
(* random reals: 0.0 <= result < 1.0 *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    88
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    89
val scaling = real max_int + 1.0;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    90
fun nextReal () = real (Word.toInt (nextWord ())) / scaling;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    91
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    92
end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
    93
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
    94
(**** Original file: src/Portable.sig ****)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
    95
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
    96
(* ========================================================================= *)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
    97
(* ML COMPILER SPECIFIC FUNCTIONS                                            *)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
    98
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    99
(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   100
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
   101
signature Metis_Portable =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   102
sig
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   103
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   104
(* ------------------------------------------------------------------------- *)
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   105
(* The ML implementation.                                                    *)
23442
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
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   108
val ml : string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   109
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   110
(* ------------------------------------------------------------------------- *)
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   111
(* Pointer equality using the run-time system.                               *)
23442
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
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   114
val pointerEqual : 'a * 'a -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   115
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   116
(* ------------------------------------------------------------------------- *)
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   117
(* Marking critical sections of code.                                        *)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   118
(* ------------------------------------------------------------------------- *)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   119
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   120
val critical : (unit -> 'a) -> unit -> 'a
39429
126b879df319 move "CRITICAL" to "PortableXxx", where it belongs and used to be;
blanchet
parents: 39428
diff changeset
   121
126b879df319 move "CRITICAL" to "PortableXxx", where it belongs and used to be;
blanchet
parents: 39428
diff changeset
   122
(* ------------------------------------------------------------------------- *)
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   123
(* Generating random values.                                                 *)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   124
(* ------------------------------------------------------------------------- *)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   125
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   126
val randomBool : unit -> bool
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   127
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   128
val randomInt : int -> int  (* n |-> [0,n) *)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   129
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   130
val randomReal : unit -> real  (* () |-> [0,1] *)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   131
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
   132
val randomWord : unit -> Word.word
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   133
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   134
(* ------------------------------------------------------------------------- *)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   135
(* Timing function applications.                                             *)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   136
(* ------------------------------------------------------------------------- *)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   137
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   138
val time : ('a -> 'b) -> 'a -> 'b
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   139
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   140
end
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   141
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   142
(**** Original file: PortableIsabelle.sml ****)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   143
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   144
(*  Title:      Tools/Metis/PortableIsabelle.sml
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   145
    Author:     Jasmin Blanchette, TU Muenchen
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   146
    Copyright   2010
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   147
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   148
Isabelle-specific setup for Metis. Based on "src/PortablePolyml.sml".
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   149
*)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   150
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
   151
structure Metis_Portable :> Metis_Portable =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   152
struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   153
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   154
val ml = "isabelle"
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   155
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   156
fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   157
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   158
fun critical e () = NAMED_CRITICAL "metis" e
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   159
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   160
val randomWord = Metis_Random.nextWord
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   161
val randomBool = Metis_Random.nextBool
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   162
val randomInt = Metis_Random.nextInt
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   163
val randomReal = Metis_Random.nextReal
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   164
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   165
fun time f x = f x (* dummy *)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   166
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   167
end
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   168
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   169
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   170
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   171
(**** Original file: src/Useful.sig ****)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   172
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
(* ML UTILITY FUNCTIONS                                                      *)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   175
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   176
(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   177
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
   178
signature Metis_Useful =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   179
sig
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
(* Exceptions.                                                               *)
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
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   185
exception Error of string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   186
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   187
exception Bug of string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   188
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   189
val total : ('a -> 'b) -> 'a -> 'b option
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   190
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   191
val can : ('a -> 'b) -> 'a -> bool
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
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   194
(* Tracing.                                                                  *)
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
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
   197
val tracePrint : (string -> unit) Unsynchronized.ref
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   198
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   199
val trace : string -> unit
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   200
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
(* Combinators.                                                              *)
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
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   205
val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   206
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   207
val I : 'a -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   208
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   209
val K : 'a -> 'b -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   210
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   211
val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   212
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   213
val W : ('a -> 'a -> 'b) -> 'a -> 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   214
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   215
val funpow : int -> ('a -> 'a) -> 'a -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   216
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   217
val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a
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
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   220
(* Pairs.                                                                    *)
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
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   223
val fst : 'a * 'b -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   224
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   225
val snd : 'a * 'b -> 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   226
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   227
val pair : 'a -> 'b -> 'a * 'b
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
val swap : 'a * 'b -> 'b * 'a
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
val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   232
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   233
val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   234
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   235
val ## : ('a -> 'c) * ('b -> 'd) -> 'a * 'b -> 'c * 'd
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   236
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
(* State transformers.                                                       *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   239
(* ------------------------------------------------------------------------- *)
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
val unit : 'a -> 's -> 'a * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   242
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   243
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
   244
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   245
val mmap : ('a -> 'b) -> ('s -> 'a * 's) -> 's -> 'b * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   246
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   247
val mjoin : ('s -> ('s -> 'a * 's) * 's) -> 's -> 'a * 's
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   248
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   249
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
   250
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   251
(* ------------------------------------------------------------------------- *)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   252
(* Equality.                                                                 *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   253
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   254
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   255
val equal : ''a -> ''a -> bool
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   256
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   257
val notEqual : ''a -> ''a -> bool
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   258
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   259
val listEqual : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   260
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   261
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   262
(* Comparisons.                                                              *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   263
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   264
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   265
val mapCompare : ('a -> 'b) -> ('b * 'b -> order) -> 'a * 'a -> order
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   266
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   267
val revCompare : ('a * 'a -> order) -> 'a * 'a -> order
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   268
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   269
val prodCompare :
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   270
    ('a * 'a -> order) -> ('b * 'b -> order) -> ('a * 'b) * ('a * 'b) -> order
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   271
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   272
val lexCompare : ('a * 'a -> order) -> 'a list * 'a list -> order
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   273
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   274
val optionCompare : ('a * 'a -> order) -> 'a option * 'a option -> order
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   275
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   276
val boolCompare : bool * bool -> order  (* false < true *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   277
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   278
(* ------------------------------------------------------------------------- *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   279
(* Lists: note we count elements from 0.                                     *)
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 cons : 'a -> 'a list -> 'a list
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 hdTl : 'a list -> 'a * 'a list
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 append : 'a list -> 'a list -> 'a list
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 singleton : 'a -> 'a list
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 first : ('a -> 'b option) -> 'a list -> 'b option
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 maps : ('a -> 's -> 'b * 's) -> 'a list -> 's -> 'b list * 's
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
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
   295
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   296
val zipWith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   297
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   298
val zip : 'a list -> 'b list -> ('a * 'b) list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   299
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   300
val unzip : ('a * 'b) list -> 'a list * 'b list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   301
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   302
val cartwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   303
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   304
val cart : 'a list -> 'b list -> ('a * 'b) list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   305
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   306
val takeWhile : ('a -> bool) -> 'a list -> 'a list
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   307
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   308
val dropWhile : ('a -> bool) -> 'a list -> 'a list
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   309
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   310
val divideWhile : ('a -> bool) -> 'a list -> 'a list * 'a list
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   311
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   312
val groups : ('a * 's -> bool * 's) -> 's -> 'a list -> 'a list list
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   313
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   314
val groupsBy : ('a * 'a -> bool) -> 'a list -> 'a list list
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   315
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   316
val groupsByFst : (''a * 'b) list -> (''a * 'b list) list
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   317
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   318
val groupsOf : int -> 'a list -> 'a list list
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   319
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   320
val index : ('a -> bool) -> 'a list -> int option
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   321
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   322
val enumerate : 'a list -> (int * 'a) list
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   323
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   324
val divide : 'a list -> int -> 'a list * 'a list  (* Subscript *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   325
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   326
val revDivide : 'a list -> int -> 'a list * 'a list  (* Subscript *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   327
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   328
val updateNth : int * 'a -> 'a list -> 'a list  (* Subscript *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   329
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   330
val deleteNth : int -> 'a list -> 'a list  (* Subscript *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   331
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   332
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   333
(* Sets implemented with lists.                                              *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   334
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   335
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   336
val mem : ''a -> ''a list -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   337
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   338
val insert : ''a -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   339
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   340
val delete : ''a -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   341
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   342
val setify : ''a list -> ''a list  (* removes duplicates *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   343
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   344
val union : ''a list -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   345
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   346
val intersect : ''a list -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   347
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   348
val difference : ''a list -> ''a list -> ''a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   349
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   350
val subset : ''a list -> ''a list -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   351
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   352
val distinct : ''a list -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   353
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   354
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   355
(* Sorting and searching.                                                    *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   356
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   357
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   358
val minimum : ('a * 'a -> order) -> 'a list -> 'a * 'a list  (* Empty *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   359
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   360
val maximum : ('a * 'a -> order) -> 'a list -> 'a * 'a list  (* Empty *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   361
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   362
val merge : ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   363
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   364
val sort : ('a * 'a -> order) -> 'a list -> 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   365
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   366
val sortMap : ('a -> 'b) -> ('b * 'b -> order) -> 'a list -> 'a list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   367
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   368
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   369
(* Integers.                                                                 *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   370
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   371
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   372
val interval : int -> int -> int list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   373
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   374
val divides : int -> int -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   375
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   376
val gcd : int -> int -> int
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   377
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   378
val primes : int -> int list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   379
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   380
val primesUpTo : int -> int list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   381
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   382
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   383
(* Strings.                                                                  *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   384
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   385
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   386
val rot : int -> char -> char
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   387
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   388
val charToInt : char -> int option
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   389
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   390
val charFromInt : int -> char option
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   391
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   392
val nChars : char -> int -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   393
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   394
val chomp : string -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   395
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   396
val trim : string -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   397
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   398
val join : string -> string list -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   399
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   400
val split : string -> string -> string list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   401
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   402
val capitalize : string -> string
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   403
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   404
val mkPrefix : string -> string -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   405
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   406
val destPrefix : string -> string -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   407
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   408
val isPrefix : string -> string -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   409
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   410
val stripPrefix : (char -> bool) -> string -> string
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   411
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   412
val mkSuffix : string -> string -> string
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   413
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   414
val destSuffix : string -> string -> string
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   415
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   416
val isSuffix : string -> string -> bool
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   417
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   418
val stripSuffix : (char -> bool) -> string -> string
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   419
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   420
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   421
(* Tables.                                                                   *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   422
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   423
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   424
type columnAlignment = {leftAlign : bool, padChar : char}
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   425
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   426
val alignColumn : columnAlignment -> string list -> string list -> string list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   427
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   428
val alignTable : columnAlignment list -> string list list -> string list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   429
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   430
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   431
(* Reals.                                                                    *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   432
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   433
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   434
val percentToString : real -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   435
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   436
val pos : real -> real
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   437
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   438
val log2 : real -> real  (* Domain *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   439
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   440
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   441
(* Sum datatype.                                                             *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   442
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   443
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   444
datatype ('a,'b) sum = Left of 'a | Right of 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   445
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   446
val destLeft : ('a,'b) sum -> 'a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   447
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   448
val isLeft : ('a,'b) sum -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   449
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   450
val destRight : ('a,'b) sum -> 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   451
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   452
val isRight : ('a,'b) sum -> bool
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   453
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   454
(* ------------------------------------------------------------------------- *)
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
   455
(* Metis_Useful impure features.                                                   *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   456
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   457
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   458
val newInt : unit -> int
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   459
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   460
val newInts : int -> int list
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   461
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
   462
val withRef : 'r Unsynchronized.ref * 'r -> ('a -> 'b) -> 'a -> 'b
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   463
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
   464
val cloneArray : 'a Array.array -> 'a Array.array
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   465
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   466
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   467
(* The environment.                                                          *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   468
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   469
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   470
val host : unit -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   471
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   472
val time : unit -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   473
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   474
val date : unit -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   475
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   476
val readDirectory : {directory : string} -> {filename : string} list
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   477
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   478
val readTextFile : {filename : string} -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   479
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   480
val writeTextFile : {contents : string, filename : string} -> unit
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   481
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   482
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   483
(* Profiling and error reporting.                                            *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   484
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   485
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   486
val try : ('a -> 'b) -> 'a -> 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   487
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   488
val chat : string -> unit  (* stdout *)
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   489
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   490
val chide : string -> unit  (* stderr *)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   491
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   492
val warn : string -> unit
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   493
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   494
val die : string -> 'exit
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   495
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   496
val timed : ('a -> 'b) -> 'a -> real * 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   497
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   498
val timedMany : ('a -> 'b) -> 'a -> real * 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   499
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   500
val executionTime : unit -> real  (* Wall clock execution time *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   501
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   502
end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   503
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   504
(**** Original file: src/Useful.sml ****)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   505
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   506
(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   507
(* ML UTILITY FUNCTIONS                                                      *)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   508
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   509
(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   510
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
   511
structure Metis_Useful :> Metis_Useful =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   512
struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   513
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   514
(* ------------------------------------------------------------------------- *)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   515
(* Exceptions.                                                               *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   516
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   517
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   518
exception Error of string;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   519
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   520
exception Bug of string;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   521
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   522
fun errorToStringOption err =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   523
    case err of
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   524
      Error message => SOME ("Error: " ^ message)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   525
    | _ => NONE;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   526
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   527
(*mlton
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   528
val () = MLton.Exn.addExnMessager errorToStringOption;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   529
*)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   530
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   531
fun errorToString err =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   532
    case errorToStringOption err of
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   533
      SOME s => "\n" ^ s ^ "\n"
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   534
    | NONE => raise Bug "errorToString: not an Error exception";
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   535
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   536
fun bugToStringOption err =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   537
    case err of
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   538
      Bug message => SOME ("Bug: " ^ message)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   539
    | _ => NONE;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   540
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   541
(*mlton
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   542
val () = MLton.Exn.addExnMessager bugToStringOption;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   543
*)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   544
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   545
fun bugToString err =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   546
    case bugToStringOption err of
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   547
      SOME s => "\n" ^ s ^ "\n"
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   548
    | NONE => raise Bug "bugToString: not a Bug exception";
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   549
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   550
fun total f x = SOME (f x) handle Error _ => NONE;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   551
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   552
fun can f = Option.isSome o total f;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   553
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   554
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   555
(* Tracing.                                                                  *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   556
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   557
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   558
local
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   559
  val traceOut = TextIO.stdOut;
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   560
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   561
  fun tracePrintFn mesg =
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   562
      let
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   563
        val () = TextIO.output (traceOut,mesg)
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   564
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   565
        val () = TextIO.flushOut traceOut
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   566
      in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   567
        ()
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   568
      end;
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   569
in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   570
  val tracePrint = Unsynchronized.ref tracePrintFn;
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   571
end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   572
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   573
fun trace mesg = !tracePrint mesg;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   574
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   575
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   576
(* Combinators.                                                              *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   577
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   578
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   579
fun C f x y = f y x;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   580
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   581
fun I x = x;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   582
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   583
fun K x y = x;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   584
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   585
fun S f g x = f x (g x);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   586
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   587
fun W f x = f x x;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   588
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   589
fun funpow 0 _ x = x
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   590
  | funpow n f x = funpow (n - 1) f (f x);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   591
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   592
fun exp m =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   593
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   594
      fun f _ 0 z = z
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   595
        | f x y z = f (m (x,x)) (y div 2) (if y mod 2 = 0 then z else m (z,x))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   596
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   597
      f
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   598
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   599
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   600
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   601
(* Pairs.                                                                    *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   602
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   603
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   604
fun fst (x,_) = x;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   605
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   606
fun snd (_,y) = y;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   607
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   608
fun pair x y = (x,y);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   609
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   610
fun swap (x,y) = (y,x);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   611
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   612
fun curry f x y = f (x,y);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   613
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   614
fun uncurry f (x,y) = f x y;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   615
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   616
val op## = fn (f,g) => fn (x,y) => (f x, g y);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   617
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   618
(* ------------------------------------------------------------------------- *)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   619
(* State transformers.                                                       *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   620
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   621
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   622
val unit : 'a -> 's -> 'a * 's = pair;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   623
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   624
fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   625
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   626
fun mmap f (m : 's -> 'a * 's) = bind m (unit o f);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   627
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   628
fun mjoin (f : 's -> ('s -> 'a * 's) * 's) = bind f I;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   629
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   630
fun mwhile c b = let fun f a = if c a then bind (b a) f else unit a in f end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   631
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   632
(* ------------------------------------------------------------------------- *)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   633
(* Equality.                                                                 *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   634
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   635
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   636
val equal = fn x => fn y => x = y;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   637
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   638
val notEqual = fn x => fn y => x <> y;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   639
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   640
fun listEqual xEq =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   641
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   642
      fun xsEq [] [] = true
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   643
        | xsEq (x1 :: xs1) (x2 :: xs2) = xEq x1 x2 andalso xsEq xs1 xs2
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   644
        | xsEq _ _ = false
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   645
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   646
      xsEq
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   647
    end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   648
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   649
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   650
(* Comparisons.                                                              *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   651
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   652
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   653
fun mapCompare f cmp (a,b) = cmp (f a, f b);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   654
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   655
fun revCompare cmp x_y =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   656
    case cmp x_y of LESS => GREATER | EQUAL => EQUAL | GREATER => LESS;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   657
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   658
fun prodCompare xCmp yCmp ((x1,y1),(x2,y2)) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   659
    case xCmp (x1,x2) of
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   660
      LESS => LESS
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   661
    | EQUAL => yCmp (y1,y2)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   662
    | GREATER => GREATER;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   663
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   664
fun lexCompare cmp =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   665
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   666
      fun lex ([],[]) = EQUAL
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   667
        | lex ([], _ :: _) = LESS
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   668
        | lex (_ :: _, []) = GREATER
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   669
        | lex (x :: xs, y :: ys) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   670
          case cmp (x,y) of
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   671
            LESS => LESS
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   672
          | EQUAL => lex (xs,ys)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   673
          | GREATER => GREATER
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   674
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   675
      lex
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   676
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   677
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   678
fun optionCompare _ (NONE,NONE) = EQUAL
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   679
  | optionCompare _ (NONE,_) = LESS
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   680
  | optionCompare _ (_,NONE) = GREATER
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   681
  | optionCompare cmp (SOME x, SOME y) = cmp (x,y);
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
   682
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   683
fun boolCompare (false,true) = LESS
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   684
  | boolCompare (true,false) = GREATER
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   685
  | boolCompare _ = EQUAL;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   686
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   687
(* ------------------------------------------------------------------------- *)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   688
(* Lists.                                                                    *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   689
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   690
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   691
fun cons x y = x :: y;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   692
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   693
fun hdTl l = (hd l, tl l);
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   694
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   695
fun append xs ys = xs @ ys;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   696
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   697
fun singleton a = [a];
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   698
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   699
fun first f [] = NONE
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   700
  | first f (x :: xs) = (case f x of NONE => first f xs | s => s);
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   701
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   702
fun maps (_ : 'a -> 's -> 'b * 's) [] = unit []
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   703
  | maps f (x :: xs) =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   704
    bind (f x) (fn y => bind (maps f xs) (fn ys => unit (y :: ys)));
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   705
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   706
fun mapsPartial (_ : 'a -> 's -> 'b option * 's) [] = unit []
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   707
  | mapsPartial f (x :: xs) =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   708
    bind
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   709
      (f x)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   710
      (fn yo =>
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   711
          bind
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   712
            (mapsPartial f xs)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   713
            (fn ys => unit (case yo of NONE => ys | SOME y => y :: ys)));
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   714
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   715
fun zipWith f =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   716
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   717
      fun z l [] [] = l
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   718
        | z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   719
        | z _ _ _ = raise Error "zipWith: lists different lengths";
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   720
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   721
      fn xs => fn ys => List.rev (z [] xs ys)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   722
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   723
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   724
fun zip xs ys = zipWith pair xs ys;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   725
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   726
local
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   727
  fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys);
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   728
in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   729
  fun unzip ab = List.foldl inc ([],[]) (List.rev ab);
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   730
end;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   731
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   732
fun cartwith f =
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   733
    let
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   734
      fun aux _ res _ [] = res
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   735
        | aux xsCopy res [] (y :: yt) = aux xsCopy res xsCopy yt
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   736
        | aux xsCopy res (x :: xt) (ys as y :: _) =
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   737
          aux xsCopy (f x y :: res) xt ys
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   738
    in
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   739
      fn xs => fn ys =>
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   740
         let val xs' = List.rev xs in aux xs' [] xs' (List.rev ys) end
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   741
    end;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   742
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   743
fun cart xs ys = cartwith pair xs ys;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   744
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   745
fun takeWhile p =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   746
    let
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   747
      fun f acc [] = List.rev acc
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   748
        | f acc (x :: xs) = if p x then f (x :: acc) xs else List.rev acc
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   749
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   750
      f []
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   751
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   752
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   753
fun dropWhile p =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   754
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   755
      fun f [] = []
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   756
        | f (l as x :: xs) = if p x then f xs else l
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   757
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   758
      f
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   759
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   760
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   761
fun divideWhile p =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   762
    let
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   763
      fun f acc [] = (List.rev acc, [])
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   764
        | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (List.rev acc, l)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   765
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   766
      f []
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   767
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   768
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   769
fun groups f =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   770
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   771
      fun group acc row x l =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   772
          case l of
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   773
            [] =>
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   774
            let
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   775
              val acc = if List.null row then acc else List.rev row :: acc
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   776
            in
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   777
              List.rev acc
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   778
            end
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   779
          | h :: t =>
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   780
            let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   781
              val (eor,x) = f (h,x)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   782
            in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   783
              if eor then group (List.rev row :: acc) [h] x t
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   784
              else group acc (h :: row) x t
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   785
            end
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   786
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   787
      group [] []
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   788
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   789
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   790
fun groupsBy eq =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   791
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   792
      fun f (x_y as (x,_)) = (not (eq x_y), x)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   793
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   794
      fn [] => []
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   795
       | h :: t =>
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   796
         case groups f h t of
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   797
           [] => [[h]]
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   798
         | hs :: ts => (h :: hs) :: ts
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   799
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   800
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   801
local
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   802
  fun fstEq ((x,_),(y,_)) = x = y;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   803
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   804
  fun collapse l = (fst (hd l), List.map snd l);
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   805
in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   806
  fun groupsByFst l = List.map collapse (groupsBy fstEq l);
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   807
end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   808
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   809
fun groupsOf n =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   810
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   811
      fun f (_,i) = if i = 1 then (true,n) else (false, i - 1)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   812
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   813
      groups f (n + 1)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   814
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   815
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   816
fun index p =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   817
  let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   818
    fun idx _ [] = NONE
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   819
      | idx n (x :: xs) = if p x then SOME n else idx (n + 1) xs
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   820
  in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   821
    idx 0
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   822
  end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   823
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   824
fun enumerate l = fst (maps (fn x => fn m => ((m, x), m + 1)) l 0);
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   825
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   826
local
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   827
  fun revDiv acc l 0 = (acc,l)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   828
    | revDiv _ [] _ = raise Subscript
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   829
    | revDiv acc (h :: t) n = revDiv (h :: acc) t (n - 1);
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   830
in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   831
  fun revDivide l = revDiv [] l;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   832
end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   833
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   834
fun divide l n = let val (a,b) = revDivide l n in (List.rev a, b) end;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   835
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   836
fun updateNth (n,x) l =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   837
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   838
      val (a,b) = revDivide l n
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   839
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   840
      case b of [] => raise Subscript | _ :: t => List.revAppend (a, x :: t)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   841
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   842
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   843
fun deleteNth n l =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   844
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   845
      val (a,b) = revDivide l n
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   846
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   847
      case b of [] => raise Subscript | _ :: t => List.revAppend (a,t)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   848
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   849
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   850
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   851
(* Sets implemented with lists.                                              *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   852
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   853
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   854
fun mem x = List.exists (equal x);
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   855
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   856
fun insert x s = if mem x s then s else x :: s;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   857
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   858
fun delete x s = List.filter (not o equal x) s;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   859
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   860
local
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   861
  fun inc (v,x) = if mem v x then x else v :: x;
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   862
in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   863
  fun setify s = List.rev (List.foldl inc [] s);
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   864
end;
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   865
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   866
fun union s t =
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   867
    let
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   868
      fun inc (v,x) = if mem v t then x else v :: x
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   869
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   870
      List.foldl inc t (List.rev s)
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   871
    end;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   872
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   873
fun intersect s t =
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   874
    let
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   875
      fun inc (v,x) = if mem v t then v :: x else x
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   876
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   877
      List.foldl inc [] (List.rev s)
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   878
    end;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   879
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   880
fun difference s t =
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   881
    let
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   882
      fun inc (v,x) = if mem v t then x else v :: x
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   883
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   884
      List.foldl inc [] (List.rev s)
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
   885
    end;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   886
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   887
fun subset s t = List.all (fn x => mem x t) s;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   888
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   889
fun distinct [] = true
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   890
  | distinct (x :: rest) = not (mem x rest) andalso distinct rest;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   891
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   892
(* ------------------------------------------------------------------------- *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   893
(* Sorting and searching.                                                    *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   894
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   895
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   896
(* Finding the minimum and maximum element of a list, wrt some order. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   897
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   898
fun minimum cmp =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   899
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   900
      fun min (l,m,r) _ [] = (m, List.revAppend (l,r))
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   901
        | min (best as (_,m,_)) l (x :: r) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   902
          min (case cmp (x,m) of LESS => (l,x,r) | _ => best) (x :: l) r
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   903
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   904
      fn [] => raise Empty
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   905
       | h :: t => min ([],h,t) [h] t
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   906
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   907
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   908
fun maximum cmp = minimum (revCompare cmp);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   909
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   910
(* Merge (for the following merge-sort, but generally useful too). *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   911
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   912
fun merge cmp =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   913
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   914
      fun mrg acc [] ys = List.revAppend (acc,ys)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   915
        | mrg acc xs [] = List.revAppend (acc,xs)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   916
        | mrg acc (xs as x :: xt) (ys as y :: yt) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   917
          (case cmp (x,y) of
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   918
             GREATER => mrg (y :: acc) xs yt
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   919
           | _ => mrg (x :: acc) xt ys)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   920
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   921
      mrg []
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   922
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   923
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   924
(* Merge sort (stable). *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   925
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   926
fun sort cmp =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   927
    let
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   928
      fun findRuns acc r rs [] = List.rev (List.rev (r :: rs) :: acc)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   929
        | findRuns acc r rs (x :: xs) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   930
          case cmp (r,x) of
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   931
            GREATER => findRuns (List.rev (r :: rs) :: acc) x [] xs
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   932
          | _ => findRuns acc x (r :: rs) xs
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   933
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
   934
      fun mergeAdj acc [] = List.rev acc
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   935
        | mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   936
        | mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   937
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   938
      fun mergePairs [xs] = xs
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   939
        | mergePairs l = mergePairs (mergeAdj [] l)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   940
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   941
      fn [] => []
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   942
       | l as [_] => l
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   943
       | h :: t => mergePairs (findRuns [] h [] t)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   944
    end;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   945
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   946
fun sortMap _ _ [] = []
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   947
  | sortMap _ _ (l as [_]) = l
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   948
  | sortMap f cmp xs =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   949
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   950
      fun ncmp ((m,_),(n,_)) = cmp (m,n)
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   951
      val nxs = List.map (fn x => (f x, x)) xs
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   952
      val nys = sort ncmp nxs
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   953
    in
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
   954
      List.map snd nys
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   955
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   956
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   957
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   958
(* Integers.                                                                 *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   959
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   960
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   961
fun interval m 0 = []
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   962
  | interval m len = m :: interval (m + 1) (len - 1);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   963
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   964
fun divides _ 0 = true
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   965
  | divides 0 _ = false
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   966
  | divides a b = b mod (Int.abs a) = 0;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   967
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   968
local
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   969
  fun hcf 0 n = n
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   970
    | hcf 1 _ = 1
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   971
    | hcf m n = hcf (n mod m) m;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   972
in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   973
  fun gcd m n =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   974
      let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   975
        val m = Int.abs m
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   976
        and n = Int.abs n
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   977
      in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   978
        if m < n then hcf m n else hcf n m
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   979
      end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   980
end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   981
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   982
local
39503
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   983
  fun calcPrimes mode ps i n =
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   984
      if n = 0 then ps
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   985
      else if List.exists (fn p => divides p i) ps then
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   986
        let
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   987
          val i = i + 1
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   988
          and n = if mode then n else n - 1
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   989
        in
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   990
          calcPrimes mode ps i n
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   991
        end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   992
      else
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   993
        let
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   994
          val ps = ps @ [i]
39503
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   995
          and i = i + 1
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   996
          and n = n - 1
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   997
        in
39503
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
   998
          calcPrimes mode ps i n
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
   999
        end;
39503
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1000
in
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1001
  fun primes n =
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1002
      if n <= 0 then []
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1003
      else calcPrimes true [2] 3 (n - 1);
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1004
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1005
  fun primesUpTo n =
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1006
      if n < 2 then []
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1007
      else calcPrimes false [2] 3 (n - 2);
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1008
end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1009
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1010
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1011
(* Strings.                                                                  *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1012
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1013
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1014
local
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1015
  fun len l = (length l, l)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1016
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1017
  val upper = len (String.explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1018
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1019
  val lower = len (String.explode "abcdefghijklmnopqrstuvwxyz");
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1020
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1021
  fun rotate (n,l) c k =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1022
      List.nth (l, (k + Option.valOf (index (equal c) l)) mod n);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1023
in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1024
  fun rot k c =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1025
      if Char.isLower c then rotate lower c k
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1026
      else if Char.isUpper c then rotate upper c k
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1027
      else c;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1028
end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1029
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1030
fun charToInt #"0" = SOME 0
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1031
  | charToInt #"1" = SOME 1
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1032
  | charToInt #"2" = SOME 2
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1033
  | charToInt #"3" = SOME 3
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1034
  | charToInt #"4" = SOME 4
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1035
  | charToInt #"5" = SOME 5
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1036
  | charToInt #"6" = SOME 6
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1037
  | charToInt #"7" = SOME 7
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1038
  | charToInt #"8" = SOME 8
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1039
  | charToInt #"9" = SOME 9
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1040
  | charToInt _ = NONE;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1041
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1042
fun charFromInt 0 = SOME #"0"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1043
  | charFromInt 1 = SOME #"1"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1044
  | charFromInt 2 = SOME #"2"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1045
  | charFromInt 3 = SOME #"3"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1046
  | charFromInt 4 = SOME #"4"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1047
  | charFromInt 5 = SOME #"5"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1048
  | charFromInt 6 = SOME #"6"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1049
  | charFromInt 7 = SOME #"7"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1050
  | charFromInt 8 = SOME #"8"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1051
  | charFromInt 9 = SOME #"9"
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1052
  | charFromInt _ = NONE;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1053
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1054
fun nChars x =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1055
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1056
      fun dup 0 l = l | dup n l = dup (n - 1) (x :: l)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1057
    in
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1058
      fn n => String.implode (dup n [])
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1059
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1060
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1061
fun chomp s =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1062
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1063
      val n = size s
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1064
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1065
      if n = 0 orelse String.sub (s, n - 1) <> #"\n" then s
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1066
      else String.substring (s, 0, n - 1)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1067
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1068
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1069
local
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1070
  fun chop l =
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1071
      case l of
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1072
        [] => []
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1073
      | h :: t => if Char.isSpace h then chop t else l;
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1074
in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
  1075
  val trim = String.implode o chop o List.rev o chop o List.rev o String.explode;
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1076
end;
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1077
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1078
val join = String.concatWith;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1079
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1080
local
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1081
  fun match [] l = SOME l
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1082
    | match _ [] = NONE
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1083
    | match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1084
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1085
  fun stringify acc [] = acc
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1086
    | stringify acc (h :: t) = stringify (String.implode h :: acc) t;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1087
in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1088
  fun split sep =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1089
      let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1090
        val pat = String.explode sep
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1091
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
  1092
        fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1093
          | div1 prev recent (l as h :: t) =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1094
            case match pat l of
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1095
              NONE => div1 prev (h :: recent) t
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
  1096
            | SOME rest => div1 (List.rev recent :: prev) [] rest
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1097
      in
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1098
        fn s => div1 [] [] (String.explode s)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1099
      end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1100
end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1101
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1102
fun capitalize s =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1103
    if s = "" then s
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1104
    else str (Char.toUpper (String.sub (s,0))) ^ String.extract (s,1,NONE);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1105
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1106
fun mkPrefix p s = p ^ s;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1107
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1108
fun destPrefix p =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1109
    let
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1110
      fun check s =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1111
          if String.isPrefix p s then ()
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1112
          else raise Error "destPrefix"
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1113
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1114
      val sizeP = size p
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1115
    in
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1116
      fn s =>
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1117
         let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1118
           val () = check s
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1119
         in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1120
           String.extract (s,sizeP,NONE)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1121
         end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1122
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1123
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1124
fun isPrefix p = can (destPrefix p);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1125
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1126
fun stripPrefix pred s =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1127
    Substring.string (Substring.dropl pred (Substring.full s));
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1128
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1129
fun mkSuffix p s = s ^ p;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1130
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1131
fun destSuffix p =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1132
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1133
      fun check s =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1134
          if String.isSuffix p s then ()
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1135
          else raise Error "destSuffix"
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1136
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1137
      val sizeP = size p
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1138
    in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1139
      fn s =>
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1140
         let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1141
           val () = check s
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1142
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1143
           val sizeS = size s
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1144
         in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1145
           String.substring (s, 0, sizeS - sizeP)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1146
         end
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1147
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1148
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1149
fun isSuffix p = can (destSuffix p);
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1150
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1151
fun stripSuffix pred s =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1152
    Substring.string (Substring.dropr pred (Substring.full s));
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1153
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1154
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1155
(* Tables.                                                                   *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1156
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1157
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1158
type columnAlignment = {leftAlign : bool, padChar : char}
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1159
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1160
fun alignColumn {leftAlign,padChar} column =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1161
    let
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1162
      val (n,_) = maximum Int.compare (List.map size column)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1163
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1164
      fun pad entry row =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1165
          let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1166
            val padding = nChars padChar (n - size entry)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1167
          in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1168
            if leftAlign then entry ^ padding ^ row
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1169
            else padding ^ entry ^ row
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1170
          end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1171
    in
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1172
      zipWith pad column
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1173
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1174
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1175
local
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1176
  fun alignTab aligns rows =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1177
      case aligns of
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1178
        [] => List.map (K "") rows
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1179
      | [{leftAlign = true, padChar = #" "}] => List.map hd rows
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1180
      | align :: aligns =>
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1181
        let
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1182
          val col = List.map hd rows
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1183
          and cols = alignTab aligns (List.map tl rows)
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1184
        in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1185
          alignColumn align col cols
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1186
        end;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1187
in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1188
  fun alignTable aligns rows =
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39672
diff changeset
  1189
      if List.null rows then [] else alignTab aligns rows;
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1190
end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1191
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1192
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1193
(* Reals.                                                                    *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1194
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1195
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1196
val realToString = Real.toString;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1197
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1198
fun percentToString x = Int.toString (Real.round (100.0 * x)) ^ "%";
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1199
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1200
fun pos r = Real.max (r,0.0);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1201
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1202
local
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1203
  val invLn2 = 1.0 / Math.ln 2.0;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1204
in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1205
  fun log2 x = invLn2 * Math.ln x;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1206
end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1207
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1208
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1209
(* Sums.                                                                     *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1210
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1211
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1212
datatype ('a,'b) sum = Left of 'a | Right of 'b
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1213
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1214
fun destLeft (Left l) = l
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1215
  | destLeft _ = raise Error "destLeft";
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1216
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1217
fun isLeft (Left _) = true
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1218
  | isLeft (Right _) = false;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1219
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1220
fun destRight (Right r) = r
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1221
  | destRight _ = raise Error "destRight";
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1222
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1223
fun isRight (Left _) = false
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1224
  | isRight (Right _) = true;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1225
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1226
(* ------------------------------------------------------------------------- *)
39417
0be01cad5df4 regenerate "metis.ML", this time without manual hacks
blanchet
parents: 39385
diff changeset
  1227
(* Metis_Useful impure features.                                                   *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1228
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1229
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1230
local
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
  1231
  val generator = Unsynchronized.ref 0
39503
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1232
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1233
  fun newIntThunk () =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1234
      let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1235
        val n = !generator
39503
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1236
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1237
        val () = generator := n + 1
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1238
      in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1239
        n
39503
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1240
      end;
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1241
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1242
  fun newIntsThunk k () =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1243
      let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1244
        val n = !generator
39503
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1245
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1246
        val () = generator := n + k
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1247
      in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1248
        interval n k
39503
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1249
      end;
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1250
in
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1251
  fun newInt () = Metis_Portable.critical newIntThunk ();
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1252
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1253
  fun newInts k =
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1254
      if k <= 0 then []
b7ff4b15be13 regenerate "metis.ML"
blanchet
parents: 39449
diff changeset
  1255
      else Metis_Portable.critical (newIntsThunk k) ();
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1256
end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1257
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1258
fun withRef (r,new) f x =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1259
  let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1260
    val old = !r
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1261
    val () = r := new
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1262
    val y = f x handle e => (r := old; raise e)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1263
    val () = r := old
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1264
  in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1265
    y
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1266
  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1267
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1268
fun cloneArray a =
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1269
    let
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1270
      fun index i = Array.sub (a,i)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1271
    in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1272
      Array.tabulate (Array.length a, index)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1273
    end;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24324
diff changeset
  1274
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1275
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1276
(* Environment.                                                              *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1277
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1278
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1279
fun host () = Option.getOpt (OS.Process.getEnv "HOSTNAME", "unknown");
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1280
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1281
fun time () = Date.fmt "%H:%M:%S" (Date.fromTimeLocal (Time.now ()));
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1282
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1283
fun date () = Date.fmt "%d/%m/%Y" (Date.fromTimeLocal (Time.now ()));
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1284
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1285
fun readDirectory {directory = dir} =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1286
    let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1287
      val dirStrm = OS.FileSys.openDir dir
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1288
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1289
      fun readAll acc =
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1290
          case OS.FileSys.readDir dirStrm of
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1291
            NONE => acc
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1292
          | SOME file =>
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1293
            let
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1294
              val filename = OS.Path.joinDirFile {dir = dir, file = file}
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1295
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1296
              val acc = {filename = filename} :: acc
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1297
            in
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1298
              readAll acc
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1299
            end
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1300
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1301
      val filenames = readAll []
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1302
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1303
      val () = OS.FileSys.closeDir dirStrm
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1304
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
  1305
      List.rev filenames
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1306
    end;
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1307
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1308
fun readTextFile {filename} =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1309
  let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1310
    open TextIO
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1311
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1312
    val h = openIn filename
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1313
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1314
    val contents = inputAll h
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1315
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1316
    val () = closeIn h
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1317
  in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1318
    contents
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1319
  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1320
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1321
fun writeTextFile {contents,filename} =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1322
  let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1323
    open TextIO
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1324
    val h = openOut filename
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1325
    val () = output (h,contents)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1326
    val () = closeOut h
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1327
  in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1328
    ()
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1329
  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1330
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1331
(* ------------------------------------------------------------------------- *)
39351
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1332
(* Profiling and error reporting.                                            *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1333
(* ------------------------------------------------------------------------- *)
1e118007e41a regenerated "metis.ML" and reintroduced Larry's old hacks manually;
blanchet
parents: 33514
diff changeset
  1334
39449
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1335
fun chat s = TextIO.output (TextIO.stdOut, s ^ "\n");
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1336
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1337
fun chide s = TextIO.output (TextIO.stdErr, s ^ "\n");
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1338
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1339
local
fbc1ab44b5f1 regenerated "metis.ML"
blanchet
parents: 39433
diff changeset
  1340
  fun err x s = chide (x ^ ": " ^ s);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1341
in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1342
  fun try f x = f x
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1343
      handle e as Error _ => (err "try" (errorToString e); raise e)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1344
           | e as Bug _ => (err "try" (bugToString e); raise e)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1345
           | e => (err "try" "strange exception raised"; raise e);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1346
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1347
  val warn = err "WARNING";
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1348
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1349
  fun die s = (err "\nFATAL ERROR" s; OS.Process.exit OS.Process.failure);
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1350
end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1351
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1352
fun timed f a =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1353
  let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1354
    val tmr = Timer.startCPUTimer ()
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1355
    val res = f a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1356
    val {usr,sys,...} = Timer.checkCPUTimer tmr
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1357
  in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1358
    (Time.toReal usr + Time.toReal sys, res)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1359
  end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1360
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1361
local
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1362
  val MIN = 1.0;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1363
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1364
  fun several n t f a =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1365
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1366
      val (t',res) = timed f a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1367
      val t = t + t'
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1368
      val n = n + 1
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1369
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1370
      if t > MIN then (t / Real.fromInt n, res) else several n t f a
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1371
    end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
  1372
in