src/Tools/Metis/src/Stream.sml
author blanchet
Mon, 13 Sep 2010 21:09:43 +0200
changeset 39348 6f9c9899f99f
child 39349 2d0a4361c3ef
permissions -rw-r--r--
new version of the Metis files
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
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     3
(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
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 Stream :> Stream =
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
val K = Useful.K;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
val pair = Useful.pair;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
val funpow = Useful.funpow;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
(* The stream type.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
datatype 'a stream =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
    Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
  | Cons of 'a * (unit -> 'a stream);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
(* Stream constructors.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
fun repeat x = let fun rep () = Cons (x,rep) in rep () end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
fun count n = Cons (n, fn () => count (n + 1));
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 funpows f x = Cons (x, fn () => funpows f (f x));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
(* Stream versions of standard list operations: these should all terminate.  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
fun cons h t = Cons (h,t);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
fun null Nil = true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
  | null (Cons _) = false;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
fun hd Nil = raise Empty
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
  | hd (Cons (h,_)) = h;
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 tl Nil = raise Empty
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
  | tl (Cons (_,t)) = t ();
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
fun hdTl s = (hd s, tl s);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
fun singleton s = Cons (s, K Nil);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
fun append Nil s = s ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
  | append (Cons (h,t)) s = Cons (h, fn () => append (t ()) s);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
fun map f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
      fun m Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
        | m (Cons (h,t)) = Cons (f h, m o t)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
      m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
fun maps f g =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
      fun mm s Nil = g s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
        | mm s (Cons (x,xs)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
            val (y,s') = f x s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
            Cons (y, mm s' o xs)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
      mm
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
    end;
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 zipwith f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
      fun z Nil _ = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
        | z _ Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
        | z (Cons (x,xs)) (Cons (y,ys)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
          Cons (f x y, fn () => z (xs ()) (ys ()))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
      z
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
fun zip s t = zipwith pair s t;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
fun take 0 _ = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
  | take n Nil = raise Subscript
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
  | take 1 (Cons (x,_)) = Cons (x, K Nil)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
  | take n (Cons (x,xs)) = Cons (x, fn () => take (n - 1) (xs ()));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
fun drop n s = funpow n tl s handle Empty => raise Subscript;
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
(* Stream versions of standard list operations: these might not terminate.   *)
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
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
  fun len n Nil = n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
    | len n (Cons (_,t)) = len (n + 1) (t ());
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
  fun length s = len 0 s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
fun exists pred =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
      fun f Nil = false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
        | f (Cons (h,t)) = pred h orelse f (t ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
      f
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
fun all pred = not o exists (not o pred);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
fun filter p Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
  | filter p (Cons (x,xs)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
    if p x then Cons (x, fn () => filter p (xs ())) else filter p (xs ());
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
fun foldl f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
      fun fold b Nil = b
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
        | fold b (Cons (h,t)) = fold (f (h,b)) (t ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
      fold
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
fun concat Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
  | concat (Cons (Nil, ss)) = concat (ss ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
  | concat (Cons (Cons (x, xs), ss)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
    Cons (x, fn () => concat (Cons (xs (), ss)));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
fun mapPartial f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   135
      fun mp Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   136
        | mp (Cons (h,t)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   137
          case f h of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   138
            NONE => mp (t ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   139
          | SOME h' => Cons (h', fn () => mp (t ()))
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
      mp
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
fun mapsPartial f g =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   145
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   146
      fun mp s Nil = g s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   147
        | mp s (Cons (h,t)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
            val (h,s) = f h s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
            case h of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
              NONE => mp s (t ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
            | SOME h => Cons (h, fn () => mp s (t ()))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
      mp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
    end;
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 mapConcat f =
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 mc Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
        | mc (Cons (h,t)) = append (f h) (fn () => mc (t ()))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
      mc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
fun mapsConcat f g =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
      fun mc s Nil = g s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
        | mc s (Cons (h,t)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
            val (l,s) = f h s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
            append l (fn () => mc s (t ()))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
      mc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
(* Stream operations.                                                        *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   184
fun memoize Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   185
  | memoize (Cons (h,t)) = Cons (h, Lazy.memoize (fn () => memoize (t ())));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   186
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   187
fun concatList [] = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   188
  | concatList (h :: t) = append h (fn () => concatList t);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   189
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   190
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   191
  fun toLst res Nil = rev res
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   192
    | toLst res (Cons (x, xs)) = toLst (x :: res) (xs ());
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   193
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   194
  fun toList s = toLst [] s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   195
end;
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 fromList [] = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   198
  | fromList (x :: xs) = Cons (x, fn () => fromList xs);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   199
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   200
fun listConcat s = concat (map fromList s);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   201
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   202
fun toString s = implode (toList s);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   203
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   204
fun fromString s = fromList (explode s);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   205
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   206
fun toTextFile {filename = f} s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   207
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   208
      val (h,close) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   209
          if f = "-" then (TextIO.stdOut, K ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   210
          else (TextIO.openOut f, TextIO.closeOut)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   211
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   212
      fun toFile Nil = ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   213
        | toFile (Cons (x,y)) = (TextIO.output (h,x); toFile (y ()))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   214
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   215
      val () = toFile s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   216
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   217
      close h
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   218
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   219
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   220
fun fromTextFile {filename = f} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   221
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   222
      val (h,close) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   223
          if f = "-" then (TextIO.stdIn, K ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   224
          else (TextIO.openIn f, TextIO.closeIn)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   225
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   226
      fun strm () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   227
          case TextIO.inputLine h of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   228
            NONE => (close h; Nil)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   229
          | SOME s => Cons (s,strm)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   230
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   231
      memoize (strm ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   232
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   233
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   234
end