src/Tools/Metis/src/Useful.sml
author blanchet
Mon, 07 Jan 2013 19:15:01 +0100
changeset 50758 26936f4ae087
parent 45778 df6e210fb44c
child 72004 913162a47d9f
permissions -rw-r--r--
tuned output
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                                                      *)
39502
cffceed8e7fa fix license
blanchet
parents: 39501
diff changeset
     3
(* Copyright (c) 2001 Joe 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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   477
local
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   478
  fun calcPrimes mode ps i n =
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   479
      if n = 0 then ps
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   480
      else if List.exists (fn p => divides p i) ps then
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   481
        let
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   482
          val i = i + 1
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   483
          and n = if mode then n else n - 1
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   484
        in
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   485
          calcPrimes mode ps i n
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   486
        end
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   487
      else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   488
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   489
          val ps = ps @ [i]
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   490
          and i = i + 1
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   491
          and n = n - 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   492
        in
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   493
          calcPrimes mode ps i n
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   494
        end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   495
in
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   496
  fun primes n =
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   497
      if n <= 0 then []
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   498
      else calcPrimes true [2] 3 (n - 1);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   499
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   500
  fun primesUpTo n =
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   501
      if n < 2 then []
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   502
      else calcPrimes false [2] 3 (n - 2);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   503
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   504
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   505
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   506
(* Strings.                                                                  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   507
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   508
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   509
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   510
  fun len l = (length l, l)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   511
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   512
  val upper = len (String.explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   513
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   514
  val lower = len (String.explode "abcdefghijklmnopqrstuvwxyz");
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   515
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   516
  fun rotate (n,l) c k =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   517
      List.nth (l, (k + Option.valOf (index (equal c) l)) mod n);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   518
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   519
  fun rot k c =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   520
      if Char.isLower c then rotate lower c k
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   521
      else if Char.isUpper c then rotate upper c k
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   522
      else c;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   523
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   524
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   525
fun charToInt #"0" = SOME 0
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   526
  | charToInt #"1" = SOME 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   527
  | charToInt #"2" = SOME 2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   528
  | charToInt #"3" = SOME 3
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   529
  | charToInt #"4" = SOME 4
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   530
  | charToInt #"5" = SOME 5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   531
  | charToInt #"6" = SOME 6
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   532
  | charToInt #"7" = SOME 7
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   533
  | charToInt #"8" = SOME 8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   534
  | charToInt #"9" = SOME 9
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   535
  | charToInt _ = NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   536
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   537
fun charFromInt 0 = SOME #"0"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   538
  | charFromInt 1 = SOME #"1"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   539
  | charFromInt 2 = SOME #"2"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   540
  | charFromInt 3 = SOME #"3"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   541
  | charFromInt 4 = SOME #"4"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   542
  | charFromInt 5 = SOME #"5"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   543
  | charFromInt 6 = SOME #"6"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   544
  | charFromInt 7 = SOME #"7"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   545
  | charFromInt 8 = SOME #"8"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   546
  | charFromInt 9 = SOME #"9"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   547
  | charFromInt _ = NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   548
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   549
fun nChars x =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   550
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   551
      fun dup 0 l = l | dup n l = dup (n - 1) (x :: l)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   552
    in
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   553
      fn n => String.implode (dup n [])
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   554
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   555
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   556
fun chomp s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   557
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   558
      val n = size s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   559
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   560
      if n = 0 orelse String.sub (s, n - 1) <> #"\n" then s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   561
      else String.substring (s, 0, n - 1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   562
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   563
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   564
local
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   565
  fun chop l =
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   566
      case l of
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   567
        [] => []
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   568
      | h :: t => if Char.isSpace h then chop t else l;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   569
in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   570
  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
   571
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   572
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   573
val join = String.concatWith;
39348
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 match [] l = SOME l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   577
    | match _ [] = NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   578
    | 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
   579
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   580
  fun stringify acc [] = acc
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   581
    | stringify acc (h :: t) = stringify (String.implode h :: acc) t;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   582
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   583
  fun split sep =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   584
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   585
        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
   586
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   587
        fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   588
          | div1 prev recent (l as h :: t) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   589
            case match pat l of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   590
              NONE => div1 prev (h :: recent) t
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   591
            | SOME rest => div1 (List.rev recent :: prev) [] rest
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   592
      in
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   593
        fn s => div1 [] [] (String.explode s)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   594
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   595
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   596
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   597
fun capitalize s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   598
    if s = "" then s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   599
    else str (Char.toUpper (String.sub (s,0))) ^ String.extract (s,1,NONE);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   600
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   601
fun mkPrefix p s = p ^ s;
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 destPrefix p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   604
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   605
      fun check s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   606
          if String.isPrefix p s then ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   607
          else raise Error "destPrefix"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   608
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   609
      val sizeP = size p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   610
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   611
      fn s =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   612
         let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   613
           val () = check s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   614
         in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   615
           String.extract (s,sizeP,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   616
         end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   617
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   618
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   619
fun isPrefix p = can (destPrefix p);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   620
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   621
fun stripPrefix pred s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   622
    Substring.string (Substring.dropl pred (Substring.full s));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   623
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   624
fun mkSuffix p s = s ^ p;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   625
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   626
fun destSuffix p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   627
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   628
      fun check s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   629
          if String.isSuffix p s then ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   630
          else raise Error "destSuffix"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   631
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   632
      val sizeP = size p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   633
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   634
      fn s =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   635
         let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   636
           val () = check s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   637
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   638
           val sizeS = size s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   639
         in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   640
           String.substring (s, 0, sizeS - sizeP)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   641
         end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   642
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   643
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   644
fun isSuffix p = can (destSuffix p);
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 stripSuffix pred s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   647
    Substring.string (Substring.dropr pred (Substring.full s));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   648
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   649
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   650
(* Tables.                                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   651
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   652
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   653
type columnAlignment = {leftAlign : bool, padChar : char}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   654
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   655
fun alignColumn {leftAlign,padChar} column =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   656
    let
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   657
      val (n,_) = maximum Int.compare (List.map size column)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   658
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   659
      fun pad entry row =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   660
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   661
            val padding = nChars padChar (n - size entry)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   662
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   663
            if leftAlign then entry ^ padding ^ row
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   664
            else padding ^ entry ^ row
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   665
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   666
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   667
      zipWith pad column
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   668
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   669
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   670
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   671
  fun alignTab aligns rows =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   672
      case aligns of
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   673
        [] => List.map (K "") rows
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   674
      | [{leftAlign = true, padChar = #" "}] => List.map hd rows
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   675
      | align :: aligns =>
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   676
        let
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   677
          val col = List.map hd rows
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   678
          and cols = alignTab aligns (List.map tl rows)
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   679
        in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   680
          alignColumn align col cols
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   681
        end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   682
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   683
  fun alignTable aligns rows =
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   684
      if List.null rows then [] else alignTab aligns rows;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   685
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   686
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   687
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   688
(* Reals.                                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   689
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   690
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   691
val realToString = Real.toString;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   692
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   693
fun percentToString x = Int.toString (Real.round (100.0 * x)) ^ "%";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   694
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   695
fun pos r = Real.max (r,0.0);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   696
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   697
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   698
  val invLn2 = 1.0 / Math.ln 2.0;
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
  fun log2 x = invLn2 * Math.ln x;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   701
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   702
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   703
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   704
(* Sums.                                                                     *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   705
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   706
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   707
datatype ('a,'b) sum = Left of 'a | Right of 'b
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   708
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   709
fun destLeft (Left l) = l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   710
  | destLeft _ = raise Error "destLeft";
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 isLeft (Left _) = true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   713
  | isLeft (Right _) = false;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   714
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   715
fun destRight (Right r) = r
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   716
  | destRight _ = raise Error "destRight";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   717
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   718
fun isRight (Left _) = false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   719
  | isRight (Right _) = true;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   720
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   721
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   722
(* Useful impure features.                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   723
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   724
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   725
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   726
  val generator = ref 0
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   727
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   728
  fun newIntThunk () =
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   729
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   730
        val n = !generator
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   731
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   732
        val () = generator := n + 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   733
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   734
        n
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   735
      end;
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   736
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   737
  fun newIntsThunk k () =
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   738
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   739
        val n = !generator
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   740
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   741
        val () = generator := n + k
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   742
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   743
        interval n k
39501
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   744
      end;
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   745
in
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   746
  fun newInt () = Portable.critical newIntThunk ();
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   747
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   748
  fun newInts k =
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   749
      if k <= 0 then []
aaa7078fff55 updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents: 39445
diff changeset
   750
      else Portable.critical (newIntsThunk k) ();
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
fun withRef (r,new) f x =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   754
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   755
    val old = !r
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   756
    val () = r := new
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   757
    val y = f x handle e => (r := old; raise e)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   758
    val () = r := old
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   759
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   760
    y
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   761
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   762
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   763
fun cloneArray a =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   764
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   765
      fun index i = Array.sub (a,i)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   766
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   767
      Array.tabulate (Array.length a, index)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   768
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   769
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   770
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   771
(* Environment.                                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   772
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   773
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   774
fun host () = Option.getOpt (OS.Process.getEnv "HOSTNAME", "unknown");
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   775
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   776
fun time () = Date.fmt "%H:%M:%S" (Date.fromTimeLocal (Time.now ()));
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 date () = Date.fmt "%d/%m/%Y" (Date.fromTimeLocal (Time.now ()));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   779
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   780
fun readDirectory {directory = dir} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   781
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   782
      val dirStrm = OS.FileSys.openDir dir
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 readAll acc =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   785
          case OS.FileSys.readDir dirStrm of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   786
            NONE => acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   787
          | SOME file =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   788
            let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   789
              val filename = OS.Path.joinDirFile {dir = dir, file = file}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   790
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   791
              val acc = {filename = filename} :: acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   792
            in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   793
              readAll acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   794
            end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   795
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   796
      val filenames = readAll []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   797
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   798
      val () = OS.FileSys.closeDir dirStrm
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   799
    in
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   800
      List.rev filenames
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   801
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   802
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   803
fun readTextFile {filename} =
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
    open TextIO
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   806
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   807
    val h = openIn filename
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   808
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   809
    val contents = inputAll h
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   810
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   811
    val () = closeIn h
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   812
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   813
    contents
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   814
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   815
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   816
fun writeTextFile {contents,filename} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   817
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   818
    open TextIO
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   819
    val h = openOut filename
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   820
    val () = output (h,contents)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   821
    val () = closeOut h
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   822
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   823
    ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   824
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   825
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   826
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   827
(* Profiling and error reporting.                                            *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   828
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   829
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   830
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
   831
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   832
fun chide s = TextIO.output (TextIO.stdErr, s ^ "\n");
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   833
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   834
local
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   835
  fun err x s = chide (x ^ ": " ^ s);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   836
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   837
  fun try f x = f x
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   838
      handle e as Error _ => (err "try" (errorToString e); raise e)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   839
           | e as Bug _ => (err "try" (bugToString e); raise e)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   840
           | e => (err "try" "strange exception raised"; raise e);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   841
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   842
  val warn = err "WARNING";
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 die s = (err "\nFATAL ERROR" s; OS.Process.exit OS.Process.failure);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   845
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   846
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   847
fun timed f a =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   848
  let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   849
    val tmr = Timer.startCPUTimer ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   850
    val res = f a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   851
    val {usr,sys,...} = Timer.checkCPUTimer tmr
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   852
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   853
    (Time.toReal usr + Time.toReal sys, res)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   854
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   855
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   856
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   857
  val MIN = 1.0;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   858
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   859
  fun several n t f a =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   860
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   861
      val (t',res) = timed f a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   862
      val t = t + t'
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   863
      val n = n + 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   864
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   865
      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
   866
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   867
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   868
  fun timedMany f a = several 0 0.0 f a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   869
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   870
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   871
val executionTime =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   872
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   873
      val startTime = Time.toReal (Time.now ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   874
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   875
      fn () => Time.toReal (Time.now ()) - startTime
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   876
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   877
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   878
end