src/Tools/Metis/src/Useful.sml
author wenzelm
Mon, 21 Jul 2025 16:21:37 +0200
changeset 82892 45107da819fc
parent 72004 913162a47d9f
permissions -rw-r--r--
eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* ML UTILITY FUNCTIONS                                                      *)
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
     3
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License     *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
structure Useful :> Useful =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
(* Exceptions.                                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
exception Error of string;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
exception Bug of string;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
fun errorToStringOption err =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
    case err of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
      Error message => SOME ("Error: " ^ message)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
    | _ => NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
(*mlton
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
val () = MLton.Exn.addExnMessager errorToStringOption;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
fun errorToString err =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
    case errorToStringOption err of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
      SOME s => "\n" ^ s ^ "\n"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
    | NONE => raise Bug "errorToString: not an Error exception";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
fun bugToStringOption err =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
    case err of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
      Bug message => SOME ("Bug: " ^ message)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
    | _ => NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
(*mlton
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
val () = MLton.Exn.addExnMessager bugToStringOption;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
fun bugToString err =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
    case bugToStringOption err of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
      SOME s => "\n" ^ s ^ "\n"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
    | NONE => raise Bug "bugToString: not a Bug exception";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
fun total f x = SOME (f x) handle Error _ => NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
fun can f = Option.isSome o total f;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
(* Tracing.                                                                  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    53
local
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    54
  val traceOut = TextIO.stdOut;
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    55
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    56
  fun tracePrintFn mesg =
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    57
      let
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    58
        val () = TextIO.output (traceOut,mesg)
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    59
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    60
        val () = TextIO.flushOut traceOut
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    61
      in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    62
        ()
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    63
      end;
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    64
in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    65
  val tracePrint = ref tracePrintFn;
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    66
end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
fun trace mesg = !tracePrint mesg;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
(* Combinators.                                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
fun C f x y = f y x;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
fun I x = x;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
fun K x y = x;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
fun S f g x = f x (g x);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
fun W f x = f x x;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
fun funpow 0 _ x = x
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
  | funpow n f x = funpow (n - 1) f (f x);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
fun exp m =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
      fun f _ 0 z = z
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
        | f x y z = f (m (x,x)) (y div 2) (if y mod 2 = 0 then z else m (z,x))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
      f
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
(* Pairs.                                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
fun fst (x,_) = x;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
fun snd (_,y) = y;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
fun pair x y = (x,y);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
fun swap (x,y) = (y,x);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
fun curry f x y = f (x,y);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
fun uncurry f (x,y) = f x y;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
val op## = fn (f,g) => fn (x,y) => (f x, g y);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
(* State transformers.                                                       *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
val unit : 'a -> 's -> 'a * 's = pair;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
fun mmap f (m : 's -> 'a * 's) = bind m (unit o f);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
fun mjoin (f : 's -> ('s -> 'a * 's) * 's) = bind f I;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
fun mwhile c b = let fun f a = if c a then bind (b a) f else unit a in f end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
(* Equality.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
val equal = fn x => fn y => x = y;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
val notEqual = fn x => fn y => x <> y;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   135
fun listEqual xEq =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   136
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   137
      fun xsEq [] [] = true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   138
        | xsEq (x1 :: xs1) (x2 :: xs2) = xEq x1 x2 andalso xsEq xs1 xs2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   139
        | xsEq _ _ = false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   140
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   141
      xsEq
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   142
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   143
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   144
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   145
(* Comparisons.                                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   146
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   147
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
fun mapCompare f cmp (a,b) = cmp (f a, f b);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
fun revCompare cmp x_y =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
    case cmp x_y of LESS => GREATER | EQUAL => EQUAL | GREATER => LESS;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
fun prodCompare xCmp yCmp ((x1,y1),(x2,y2)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
    case xCmp (x1,x2) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
      LESS => LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
    | EQUAL => yCmp (y1,y2)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
    | GREATER => GREATER;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   158
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
fun lexCompare cmp =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
      fun lex ([],[]) = EQUAL
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
        | lex ([], _ :: _) = LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
        | lex (_ :: _, []) = GREATER
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
        | lex (x :: xs, y :: ys) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
          case cmp (x,y) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
            LESS => LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
          | EQUAL => lex (xs,ys)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
          | GREATER => GREATER
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
      lex
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
fun optionCompare _ (NONE,NONE) = EQUAL
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
  | optionCompare _ (NONE,_) = LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
  | optionCompare _ (_,NONE) = GREATER
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
  | optionCompare cmp (SOME x, SOME y) = cmp (x,y);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
fun boolCompare (false,true) = LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
  | boolCompare (true,false) = GREATER
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
  | boolCompare _ = EQUAL;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
(* Lists.                                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   184
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   185
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   186
fun cons x y = x :: y;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   187
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   188
fun hdTl l = (hd l, tl l);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   189
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   190
fun append xs ys = xs @ ys;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   191
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   192
fun singleton a = [a];
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   193
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   194
fun first f [] = NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   195
  | first f (x :: xs) = (case f x of NONE => first f xs | s => s);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   196
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   197
fun maps (_ : 'a -> 's -> 'b * 's) [] = unit []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   198
  | maps f (x :: xs) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   199
    bind (f x) (fn y => bind (maps f xs) (fn ys => unit (y :: ys)));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   200
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   201
fun mapsPartial (_ : 'a -> 's -> 'b option * 's) [] = unit []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   202
  | mapsPartial f (x :: xs) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   203
    bind
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   204
      (f x)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   205
      (fn yo =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   206
          bind
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   207
            (mapsPartial f xs)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   208
            (fn ys => unit (case yo of NONE => ys | SOME y => y :: ys)));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   209
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   210
fun zipWith f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   211
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   212
      fun z l [] [] = l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   213
        | z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   214
        | z _ _ _ = raise Error "zipWith: lists different lengths";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   215
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   216
      fn xs => fn ys => List.rev (z [] xs ys)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   217
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   218
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   219
fun zip xs ys = zipWith pair xs ys;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   220
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   221
local
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   222
  fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys);
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   223
in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   224
  fun unzip ab = List.foldl inc ([],[]) (List.rev ab);
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   225
end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   226
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   227
fun cartwith f =
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   228
    let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   229
      fun aux _ res _ [] = res
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   230
        | aux xsCopy res [] (y :: yt) = aux xsCopy res xsCopy yt
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   231
        | aux xsCopy res (x :: xt) (ys as y :: _) =
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   232
          aux xsCopy (f x y :: res) xt ys
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   233
    in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   234
      fn xs => fn ys =>
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   235
         let val xs' = List.rev xs in aux xs' [] xs' (List.rev ys) end
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   236
    end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   237
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   238
fun cart xs ys = cartwith pair xs ys;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   239
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   240
fun takeWhile p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   241
    let
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   242
      fun f acc [] = List.rev acc
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   243
        | f acc (x :: xs) = if p x then f (x :: acc) xs else List.rev acc
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   244
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   245
      f []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   246
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   247
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   248
fun dropWhile p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   249
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   250
      fun f [] = []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   251
        | f (l as x :: xs) = if p x then f xs else l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   252
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   253
      f
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   254
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   255
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   256
fun divideWhile p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   257
    let
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   258
      fun f acc [] = (List.rev acc, [])
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   259
        | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (List.rev acc, l)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   260
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   261
      f []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   262
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   263
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   264
fun groups f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   265
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   266
      fun group acc row x l =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   267
          case l of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   268
            [] =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   269
            let
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   270
              val acc = if List.null row then acc else List.rev row :: acc
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   271
            in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   272
              List.rev acc
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   273
            end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   274
          | h :: t =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   275
            let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   276
              val (eor,x) = f (h,x)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   277
            in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   278
              if eor then group (List.rev row :: acc) [h] x t
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   279
              else group acc (h :: row) x t
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   280
            end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   281
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   282
      group [] []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   283
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   284
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   285
fun groupsBy eq =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   286
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   287
      fun f (x_y as (x,_)) = (not (eq x_y), x)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   288
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   289
      fn [] => []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   290
       | h :: t =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   291
         case groups f h t of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   292
           [] => [[h]]
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   293
         | hs :: ts => (h :: hs) :: ts
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   294
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   295
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   296
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   297
  fun fstEq ((x,_),(y,_)) = x = y;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   298
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   299
  fun collapse l = (fst (hd l), List.map snd l);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   300
in
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   301
  fun groupsByFst l = List.map collapse (groupsBy fstEq l);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   302
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   303
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   304
fun groupsOf n =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   305
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   306
      fun f (_,i) = if i = 1 then (true,n) else (false, i - 1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   307
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   308
      groups f (n + 1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   309
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   310
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   311
fun index p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   312
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   313
    fun idx _ [] = NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   314
      | idx n (x :: xs) = if p x then SOME n else idx (n + 1) xs
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   315
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   316
    idx 0
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   317
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   318
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   319
fun enumerate l = fst (maps (fn x => fn m => ((m, x), m + 1)) l 0);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   320
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   321
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   322
  fun revDiv acc l 0 = (acc,l)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   323
    | revDiv _ [] _ = raise Subscript
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   324
    | revDiv acc (h :: t) n = revDiv (h :: acc) t (n - 1);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   325
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   326
  fun revDivide l = revDiv [] l;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   327
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   328
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   329
fun divide l n = let val (a,b) = revDivide l n in (List.rev a, b) end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   330
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   331
fun updateNth (n,x) l =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   332
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   333
      val (a,b) = revDivide l n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   334
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   335
      case b of [] => raise Subscript | _ :: t => List.revAppend (a, x :: t)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   336
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   337
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   338
fun deleteNth n l =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   339
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   340
      val (a,b) = revDivide l n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   341
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   342
      case b of [] => raise Subscript | _ :: t => List.revAppend (a,t)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   343
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   344
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   345
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   346
(* Sets implemented with lists.                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   347
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   349
fun mem x = List.exists (equal x);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   350
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   351
fun insert x s = if mem x s then s else x :: s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   352
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   353
fun delete x s = List.filter (not o equal x) s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   354
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   355
local
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   356
  fun inc (v,x) = if mem v x then x else v :: x;
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   357
in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   358
  fun setify s = List.rev (List.foldl inc [] s);
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   359
end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   360
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   361
fun union s t =
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   362
    let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   363
      fun inc (v,x) = if mem v t then x else v :: x
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   364
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   365
      List.foldl inc t (List.rev s)
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   366
    end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   367
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   368
fun intersect s t =
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   369
    let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   370
      fun inc (v,x) = if mem v t then v :: x else x
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   371
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   372
      List.foldl inc [] (List.rev s)
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   373
    end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   374
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   375
fun difference s t =
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   376
    let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   377
      fun inc (v,x) = if mem v t then x else v :: x
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   378
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   379
      List.foldl inc [] (List.rev s)
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   380
    end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   381
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   382
fun subset s t = List.all (fn x => mem x t) s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   383
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   384
fun distinct [] = true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   385
  | distinct (x :: rest) = not (mem x rest) andalso distinct rest;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   386
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   387
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   388
(* Sorting and searching.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   389
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   390
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   391
(* Finding the minimum and maximum element of a list, wrt some order. *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   392
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   393
fun minimum cmp =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   394
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   395
      fun min (l,m,r) _ [] = (m, List.revAppend (l,r))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   396
        | min (best as (_,m,_)) l (x :: r) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   397
          min (case cmp (x,m) of LESS => (l,x,r) | _ => best) (x :: l) r
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   398
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   399
      fn [] => raise Empty
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   400
       | h :: t => min ([],h,t) [h] t
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   401
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   402
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   403
fun maximum cmp = minimum (revCompare cmp);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   404
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   405
(* Merge (for the following merge-sort, but generally useful too). *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   406
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   407
fun merge cmp =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   408
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   409
      fun mrg acc [] ys = List.revAppend (acc,ys)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   410
        | mrg acc xs [] = List.revAppend (acc,xs)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   411
        | mrg acc (xs as x :: xt) (ys as y :: yt) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   412
          (case cmp (x,y) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   413
             GREATER => mrg (y :: acc) xs yt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   414
           | _ => mrg (x :: acc) xt ys)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   415
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   416
      mrg []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   417
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   418
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   419
(* Merge sort (stable). *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   420
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   421
fun sort cmp =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   422
    let
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   423
      fun findRuns acc r rs [] = List.rev (List.rev (r :: rs) :: acc)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   424
        | findRuns acc r rs (x :: xs) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   425
          case cmp (r,x) of
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   426
            GREATER => findRuns (List.rev (r :: rs) :: acc) x [] xs
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   427
          | _ => findRuns acc x (r :: rs) xs
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   428
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   429
      fun mergeAdj acc [] = List.rev acc
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   430
        | mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   431
        | mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   432
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   433
      fun mergePairs [xs] = xs
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   434
        | mergePairs l = mergePairs (mergeAdj [] l)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   435
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   436
      fn [] => []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   437
       | l as [_] => l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   438
       | h :: t => mergePairs (findRuns [] h [] t)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   439
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   440
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   441
fun sortMap _ _ [] = []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   442
  | sortMap _ _ (l as [_]) = l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   443
  | sortMap f cmp xs =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   444
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   445
      fun ncmp ((m,_),(n,_)) = cmp (m,n)
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   446
      val nxs = List.map (fn x => (f x, x)) xs
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   447
      val nys = sort ncmp nxs
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   448
    in
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   449
      List.map snd nys
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   450
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   451
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   452
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   453
(* Integers.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   454
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   455
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   456
fun interval m 0 = []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   457
  | interval m len = m :: interval (m + 1) (len - 1);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   458
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   459
fun divides _ 0 = true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   460
  | divides 0 _ = false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   461
  | divides a b = b mod (Int.abs a) = 0;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   462
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   463
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   464
  fun hcf 0 n = n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   465
    | hcf 1 _ = 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   466
    | hcf m n = hcf (n mod m) m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   467
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   468
  fun gcd m n =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   469
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   470
        val m = Int.abs m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   471
        and n = Int.abs n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   472
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   473
        if m < n then hcf m n else hcf n m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   474
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   475
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   476
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   477
(* Primes *)
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   478
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   479
datatype sieve =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   480
    Sieve of
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   481
      {max : int,
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   482
       primes : (int * (int * int)) list};
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   483
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   484
val initSieve =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   485
    let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   486
      val n = 1
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   487
      and ps = []
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   488
    in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   489
      Sieve
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   490
        {max = n,
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   491
         primes = ps}
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   492
    end;
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   493
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   494
fun maxSieve (Sieve {max = n, ...}) = n;
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   495
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   496
fun primesSieve (Sieve {primes = ps, ...}) = List.map fst ps;
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   497
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   498
fun incSieve sieve =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   499
    let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   500
      val n = maxSieve sieve + 1
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   501
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   502
      fun add i ps =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   503
          case ps of
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   504
            [] => (true,[(n,(0,0))])
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   505
          | (p,(k,j)) :: ps =>
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   506
              let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   507
                val k = (k + i) mod p
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   508
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   509
                val j = j + i
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   510
              in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   511
                if k = 0 then (false, (p,(k,j)) :: ps)
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   512
                else
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   513
                  let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   514
                    val (b,ps) = add j ps
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   515
                  in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   516
                    (b, (p,(k,0)) :: ps)
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   517
                  end
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   518
              end
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   519
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   520
      val Sieve {primes = ps, ...} = sieve
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   521
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   522
      val (b,ps) = add 1 ps
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   523
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   524
      val sieve =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   525
          Sieve
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   526
            {max = n,
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   527
             primes = ps}
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   528
    in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   529
      (b,sieve)
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   530
    end;
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   531
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   532
fun nextSieve sieve =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   533
    let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   534
      val (b,sieve) = incSieve sieve
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   535
    in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   536
      if b then (maxSieve sieve, sieve)
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   537
      else nextSieve sieve
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   538
    end;
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   539
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   540
local
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   541
  fun inc s =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   542
      let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   543
        val (_,s) = incSieve s
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   544
      in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   545
        s
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   546
      end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   547
in
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   548
  fun primesUpTo m =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   549
      if m <= 1 then []
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   550
      else primesSieve (funpow (m - 1) inc initSieve);
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   551
end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   552
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   553
val primes =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   554
    let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   555
      fun next s n =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   556
          if n <= 0 then []
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   557
          else
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   558
            let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   559
              val (p,s) = nextSieve s
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   560
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   561
              val n = n - 1
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   562
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   563
              val ps = next s n
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   564
            in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   565
              p :: ps
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   566
            end
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   567
    in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   568
      next initSieve
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   569
    end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   570
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   571
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   572
(* Strings.                                                                  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   573
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   574
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   575
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   576
  fun len l = (length l, l)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   577
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   578
  val upper = len (String.explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   579
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   580
  val lower = len (String.explode "abcdefghijklmnopqrstuvwxyz");
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   581
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   582
  fun rotate (n,l) c k =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   583
      List.nth (l, (k + Option.valOf (index (equal c) l)) mod n);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   584
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   585
  fun rot k c =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   586
      if Char.isLower c then rotate lower c k
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   587
      else if Char.isUpper c then rotate upper c k
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   588
      else c;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   589
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   590
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   591
fun charToInt #"0" = SOME 0
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   592
  | charToInt #"1" = SOME 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   593
  | charToInt #"2" = SOME 2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   594
  | charToInt #"3" = SOME 3
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   595
  | charToInt #"4" = SOME 4
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   596
  | charToInt #"5" = SOME 5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   597
  | charToInt #"6" = SOME 6
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   598
  | charToInt #"7" = SOME 7
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   599
  | charToInt #"8" = SOME 8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   600
  | charToInt #"9" = SOME 9
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   601
  | charToInt _ = NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   602
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   603
fun charFromInt 0 = SOME #"0"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   604
  | charFromInt 1 = SOME #"1"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   605
  | charFromInt 2 = SOME #"2"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   606
  | charFromInt 3 = SOME #"3"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   607
  | charFromInt 4 = SOME #"4"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   608
  | charFromInt 5 = SOME #"5"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   609
  | charFromInt 6 = SOME #"6"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   610
  | charFromInt 7 = SOME #"7"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   611
  | charFromInt 8 = SOME #"8"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   612
  | charFromInt 9 = SOME #"9"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   613
  | charFromInt _ = NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   614
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   615
fun nChars x =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   616
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   617
      fun dup 0 l = l | dup n l = dup (n - 1) (x :: l)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   618
    in
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   619
      fn n => String.implode (dup n [])
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   620
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   621
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   622
fun chomp s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   623
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   624
      val n = size s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   625
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   626
      if n = 0 orelse String.sub (s, n - 1) <> #"\n" then s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   627
      else String.substring (s, 0, n - 1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   628
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   629
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   630
local
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   631
  fun chop l =
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   632
      case l of
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   633
        [] => []
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   634
      | h :: t => if Char.isSpace h then chop t else l;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   635
in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   636
  val trim = String.implode o chop o List.rev o chop o List.rev o String.explode;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   637
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   638
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   639
val join = String.concatWith;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   640
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   641
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   642
  fun match [] l = SOME l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   643
    | match _ [] = NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   644
    | match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   645
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   646
  fun stringify acc [] = acc
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   647
    | stringify acc (h :: t) = stringify (String.implode h :: acc) t;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   648
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   649
  fun split sep =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   650
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   651
        val pat = String.explode sep
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   652
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   653
        fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   654
          | div1 prev recent (l as h :: t) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   655
            case match pat l of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   656
              NONE => div1 prev (h :: recent) t
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   657
            | SOME rest => div1 (List.rev recent :: prev) [] rest
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   658
      in
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   659
        fn s => div1 [] [] (String.explode s)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   660
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   661
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   662
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   663
fun capitalize s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   664
    if s = "" then s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   665
    else str (Char.toUpper (String.sub (s,0))) ^ String.extract (s,1,NONE);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   666
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   667
fun mkPrefix p s = p ^ s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   668
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   669
fun destPrefix p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   670
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   671
      fun check s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   672
          if String.isPrefix p s then ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   673
          else raise Error "destPrefix"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   674
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   675
      val sizeP = size p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   676
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   677
      fn s =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   678
         let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   679
           val () = check s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   680
         in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   681
           String.extract (s,sizeP,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   682
         end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   683
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   684
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   685
fun isPrefix p = can (destPrefix p);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   686
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   687
fun stripPrefix pred s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   688
    Substring.string (Substring.dropl pred (Substring.full s));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   689
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   690
fun mkSuffix p s = s ^ p;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   691
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   692
fun destSuffix p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   693
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   694
      fun check s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   695
          if String.isSuffix p s then ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   696
          else raise Error "destSuffix"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   697
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   698
      val sizeP = size p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   699
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   700
      fn s =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   701
         let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   702
           val () = check s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   703
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   704
           val sizeS = size s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   705
         in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   706
           String.substring (s, 0, sizeS - sizeP)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   707
         end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   708
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   709
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   710
fun isSuffix p = can (destSuffix p);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   711
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   712
fun stripSuffix pred s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   713
    Substring.string (Substring.dropr pred (Substring.full s));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   714
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   715
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   716
(* Tables.                                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   717
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   718
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   719
type columnAlignment = {leftAlign : bool, padChar : char}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   720
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   721
fun alignColumn {leftAlign,padChar} column =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   722
    let
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   723
      val (n,_) = maximum Int.compare (List.map size column)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   724
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   725
      fun pad entry row =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   726
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   727
            val padding = nChars padChar (n - size entry)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   728
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   729
            if leftAlign then entry ^ padding ^ row
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   730
            else padding ^ entry ^ row
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   731
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   732
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   733
      zipWith pad column
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   734
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   735
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   736
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   737
  fun alignTab aligns rows =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   738
      case aligns of
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   739
        [] => List.map (K "") rows
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   740
      | [{leftAlign = true, padChar = #" "}] => List.map hd rows
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   741
      | align :: aligns =>
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   742
        let
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   743
          val col = List.map hd rows
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   744
          and cols = alignTab aligns (List.map tl rows)
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   745
        in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   746
          alignColumn align col cols
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   747
        end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   748
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   749
  fun alignTable aligns rows =
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   750
      if List.null rows then [] else alignTab aligns rows;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   751
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   752
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   753
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   754
(* Reals.                                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   755
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   756
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   757
val realToString = Real.toString;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   758
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   759
fun percentToString x = Int.toString (Real.round (100.0 * x)) ^ "%";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   760
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   761
fun pos r = Real.max (r,0.0);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   762
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   763
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   764
  val invLn2 = 1.0 / Math.ln 2.0;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   765
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   766
  fun log2 x = invLn2 * Math.ln x;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   767
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   768
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   769
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   770
(* Sums.                                                                     *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   771
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   772
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   773
datatype ('a,'b) sum = Left of 'a | Right of 'b
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   774
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   775
fun destLeft (Left l) = l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   776
  | destLeft _ = raise Error "destLeft";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   777
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   778
fun isLeft (Left _) = true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   779
  | isLeft (Right _) = false;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   780
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   781
fun destRight (Right r) = r
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   782
  | destRight _ = raise Error "destRight";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   783
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   784
fun isRight (Left _) = false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   785
  | isRight (Right _) = true;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   786
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   787
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   788
(* Useful impure features.                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   789
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   790
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   791
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   792
  val generator = ref 0
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   793
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   794
  fun newIntThunk () =
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   795
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   796
        val n = !generator
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   797
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   798
        val () = generator := n + 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   799
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   800
        n
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   801
      end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   802
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   803
  fun newIntsThunk k () =
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   804
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   805
        val n = !generator
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   806
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   807
        val () = generator := n + k
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   808
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   809
        interval n k
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   810
      end;
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   811
in
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   812
  fun newInt () = Portable.critical newIntThunk ();
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   813
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   814
  fun newInts k =
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   815
      if k <= 0 then []
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   816
      else Portable.critical (newIntsThunk k) ();
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   817
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   818
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   819
fun withRef (r,new) f x =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   820
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   821
    val old = !r
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   822
    val () = r := new
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   823
    val y = f x handle e => (r := old; raise e)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   824
    val () = r := old
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   825
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   826
    y
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   827
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   828
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   829
fun cloneArray a =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   830
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   831
      fun index i = Array.sub (a,i)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   832
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   833
      Array.tabulate (Array.length a, index)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   834
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   835
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   836
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   837
(* Environment.                                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   838
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   839
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   840
fun host () = Option.getOpt (OS.Process.getEnv "HOSTNAME", "unknown");
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   841
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   842
fun time () = Date.fmt "%H:%M:%S" (Date.fromTimeLocal (Time.now ()));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   843
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   844
fun date () = Date.fmt "%d/%m/%Y" (Date.fromTimeLocal (Time.now ()));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   845
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   846
fun readDirectory {directory = dir} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   847
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   848
      val dirStrm = OS.FileSys.openDir dir
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   849
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   850
      fun readAll acc =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   851
          case OS.FileSys.readDir dirStrm of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   852
            NONE => acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   853
          | SOME file =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   854
            let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   855
              val filename = OS.Path.joinDirFile {dir = dir, file = file}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   856
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   857
              val acc = {filename = filename} :: acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   858
            in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   859
              readAll acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   860
            end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   861
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   862
      val filenames = readAll []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   863
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   864
      val () = OS.FileSys.closeDir dirStrm
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   865
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   866
      List.rev filenames
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   867
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   868
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   869
fun readTextFile {filename} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   870
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   871
    open TextIO
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   872
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   873
    val h = openIn filename
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   874
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   875
    val contents = inputAll h
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   876
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   877
    val () = closeIn h
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   878
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   879
    contents
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   880
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   881
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   882
fun writeTextFile {contents,filename} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   883
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   884
    open TextIO
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   885
    val h = openOut filename
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   886
    val () = output (h,contents)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   887
    val () = closeOut h
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   888
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   889
    ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   890
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   891
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   892
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   893
(* Profiling and error reporting.                                            *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   894
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   895
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   896
fun chat s = TextIO.output (TextIO.stdOut, s ^ "\n");
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   897
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   898
fun chide s = TextIO.output (TextIO.stdErr, s ^ "\n");
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   899
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   900
local
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   901
  fun err x s = chide (x ^ ": " ^ s);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   902
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   903
  fun try f x = f x
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   904
      handle e as Error _ => (err "try" (errorToString e); raise e)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   905
           | e as Bug _ => (err "try" (bugToString e); raise e)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   906
           | e => (err "try" "strange exception raised"; raise e);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   907
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   908
  val warn = err "WARNING";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   909
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   910
  fun die s = (err "\nFATAL ERROR" s; OS.Process.exit OS.Process.failure);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   911
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   912
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   913
fun timed f a =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   914
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   915
    val tmr = Timer.startCPUTimer ()
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   916
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   917
    val res = f a
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   918
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   919
    val {usr,sys,...} = Timer.checkCPUTimer tmr
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   920
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   921
    (Time.toReal usr + Time.toReal sys, res)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   922
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   923
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   924
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   925
  val MIN = 1.0;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   926
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   927
  fun several n t f a =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   928
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   929
      val (t',res) = timed f a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   930
      val t = t + t'
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   931
      val n = n + 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   932
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   933
      if t > MIN then (t / Real.fromInt n, res) else several n t f a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   934
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   935
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   936
  fun timedMany f a = several 0 0.0 f a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   937
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   938
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   939
val executionTime =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   940
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   941
      val startTime = Time.toReal (Time.now ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   942
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   943
      fn () => Time.toReal (Time.now ()) - startTime
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   944
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   945
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   946
end