src/Tools/Metis/src/Stream.sml
author desharna
Thu, 09 Jul 2020 11:39:16 +0200
changeset 72004 913162a47d9f
parent 45778 df6e210fb44c
permissions -rw-r--r--
Update Metis to 2.4
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                                *)
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
     3
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License     *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
structure 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
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
    95
fun unfold f =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
    96
    let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
    97
      fun next b () =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
    98
          case f b of
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
    99
            NONE => Nil
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   100
          | SOME (a,b) => Cons (a, next b)
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   101
    in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   102
      fn b => next b ()
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   103
    end;
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   104
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
(* Stream versions of standard list operations: these might not terminate.   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
  fun len n Nil = n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
    | len n (Cons (_,t)) = len (n + 1) (t ());
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
  fun length s = len 0 s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
end;
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 exists pred =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
      fun f Nil = false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
        | f (Cons (h,t)) = pred h orelse f (t ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
      f
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
fun all pred = not o exists (not o pred);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
fun filter p Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
  | filter p (Cons (x,xs)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
    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
   129
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
fun foldl f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
      fun fold b Nil = b
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
        | fold b (Cons (h,t)) = fold (f (h,b)) (t ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   135
      fold
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   136
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   137
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   138
fun concat Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   139
  | concat (Cons (Nil, ss)) = concat (ss ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   140
  | concat (Cons (Cons (x, xs), ss)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   141
    Cons (x, fn () => concat (Cons (xs (), ss)));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   142
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   143
fun mapPartial f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   144
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   145
      fun mp Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   146
        | mp (Cons (h,t)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   147
          case f h of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
            NONE => mp (t ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
          | SOME h' => Cons (h', fn () => mp (t ()))
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
      mp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
fun mapsPartial f g =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
      fun mp s Nil = g s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
        | mp s (Cons (h,t)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   158
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
            val (h,s) = f h s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
            case h of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
              NONE => mp s (t ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
            | SOME h => Cons (h, fn () => mp s (t ()))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
      mp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
fun mapConcat f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
      fun mc Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
        | mc (Cons (h,t)) = append (f h) (fn () => mc (t ()))
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
      mc
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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
fun mapsConcat f g =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
      fun mc s Nil = g s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
        | mc s (Cons (h,t)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
            val (l,s) = f h s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   184
            append l (fn () => mc s (t ()))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   185
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   186
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   187
      mc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   188
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   189
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   190
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   191
(* Stream operations.                                                        *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   192
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   193
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   194
val primes =
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   195
    let
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   196
      fun next s = SOME (Useful.nextSieve s)
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   197
    in
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   198
      unfold next Useful.initSieve
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   199
    end;
913162a47d9f Update Metis to 2.4
desharna
parents: 45778
diff changeset
   200
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   201
fun memoize Nil = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   202
  | memoize (Cons (h,t)) = Cons (h, Lazy.memoize (fn () => memoize (t ())));
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 concatList [] = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   205
  | concatList (h :: t) = append h (fn () => concatList t);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   206
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   207
local
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 39502
diff changeset
   208
  fun toLst res Nil = List.rev res
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   209
    | toLst res (Cons (x, xs)) = toLst (x :: res) (xs ());
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   210
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   211
  fun toList s = toLst [] s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   212
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   213
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   214
fun fromList [] = Nil
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   215
  | fromList (x :: xs) = Cons (x, fn () => fromList xs);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   216
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   217
fun listConcat s = concat (map fromList s);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   218
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39414
diff changeset
   219
fun toString s = String.implode (toList s);
39348
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
fun fromString s = fromList (String.explode s);
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   222
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   223
fun toTextFile {filename = f} s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   224
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   225
      val (h,close) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   226
          if f = "-" then (TextIO.stdOut, K ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   227
          else (TextIO.openOut f, TextIO.closeOut)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   228
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   229
      fun toFile Nil = ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   230
        | toFile (Cons (x,y)) = (TextIO.output (h,x); toFile (y ()))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   231
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   232
      val () = toFile s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   233
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   234
      close h
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   235
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   236
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   237
fun fromTextFile {filename = f} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   238
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   239
      val (h,close) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   240
          if f = "-" then (TextIO.stdIn, K ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   241
          else (TextIO.openIn f, TextIO.closeIn)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   242
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   243
      fun strm () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   244
          case TextIO.inputLine h of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   245
            NONE => (close h; Nil)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   246
          | SOME s => Cons (s,strm)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   247
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   248
      memoize (strm ())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   249
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   250
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   251
end