src/Pure/basis.ML
author wenzelm
Thu Apr 24 19:46:05 1997 +0200 (1997-04-24)
changeset 3047 599cb28f8502
parent 2884 4f2a4c27f9b5
child 3244 71b760618f30
permissions -rw-r--r--
open General (type option is in Option in the newer versions, but always
the top-level);
     1 (*  Title:      Pure/basis.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Basis Library emulation.
     7 
     8 Needed for Poly/ML and Standard ML of New Jersey version 0.93 to 1.08.
     9 
    10 Full compatibility cannot be obtained using a file: what about char constants?
    11 *)
    12 
    13 exception Subscript;
    14 
    15 structure Bool =
    16   struct
    17   fun toString true  = "true"
    18     | toString false = "false"
    19   end;
    20 
    21 structure General =
    22   struct
    23   exception Option
    24 
    25   datatype 'a option = NONE | SOME of 'a
    26 
    27   fun getOpt (SOME v, _) = v
    28     | getOpt (NONE,   a) = a
    29 
    30   fun isSome (SOME _) = true 
    31     | isSome NONE     = false
    32 
    33   fun valOf (SOME v) = v
    34     | valOf NONE     = raise Option
    35   end;
    36 
    37 open General;
    38 
    39 
    40 structure Int =
    41   struct
    42   fun toString (i: int) = makestring i;
    43   fun max (x, y) = if x < y then y else x : int;
    44   fun min (x, y) = if x < y then x else y : int;
    45   end;
    46 
    47 
    48 structure List =
    49   struct
    50   exception Empty
    51 
    52   fun last []      = raise Empty
    53     | last [x]     = x
    54     | last (x::xs) = last xs;
    55 
    56   fun nth (xs, n) =
    57       let fun h []      _ = raise Subscript
    58 	    | h (x::xs) n = if n=0 then x else h xs (n-1)
    59       in if n<0 then raise Subscript else h xs n end;
    60 
    61   fun drop (xs, n) =
    62       let fun h xs      0 = xs
    63 	    | h []      n = raise Subscript
    64 	    | h (x::xs) n = h xs (n-1)
    65       in if n<0 then raise Subscript else h xs n end;
    66 
    67   fun take (xs, n) =
    68       let fun h xs      0 = []
    69 	    | h []      n = raise Subscript
    70 	    | h (x::xs) n = x :: h xs (n-1)
    71       in if n<0 then raise Subscript else h xs n end;
    72 
    73   fun concat []      = []
    74     | concat (l::ls) = l @ concat ls;
    75 
    76   fun mapPartial f []      = []
    77     | mapPartial f (x::xs) = 
    78          (case f x of General.NONE   => mapPartial f xs
    79                     | General.SOME y => y :: mapPartial f xs);
    80 
    81   fun find _ []        = General.NONE
    82     | find p (x :: xs) = if p x then General.SOME x else find p xs;
    83 
    84 
    85   (*copy the list preserving elements that satisfy the predicate*)
    86   fun filter p [] = []
    87     | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
    88 
    89   (*Partition list into elements that satisfy predicate and those that don't.
    90     Preserves order of elements in both lists.*)
    91   fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
    92       let fun part ([], answer) = answer
    93 	    | part (x::xs, (ys, ns)) = if p(x)
    94 	      then  part (xs, (x::ys, ns))
    95 	      else  part (xs, (ys, x::ns))
    96       in  part (rev ys, ([], []))  end;
    97 
    98   end;
    99 
   100 
   101 structure ListPair =
   102   struct
   103   fun zip ([], [])      = []
   104     | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
   105 
   106   fun unzip [] = ([],[])
   107     | unzip((x,y)::pairs) =
   108 	  let val (xs,ys) = unzip pairs
   109 	  in  (x::xs, y::ys)  end;
   110 
   111   fun map f ([], [])      = []
   112     | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
   113 
   114   fun exists p =
   115     let fun boolf ([], [])      = false
   116 	  | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
   117     in boolf end;
   118 
   119   fun all p =
   120     let fun boolf ([], [])      = true
   121 	  | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
   122     in boolf end;
   123   end;
   124 
   125 
   126 structure TextIO =
   127   struct
   128   type instream = instream
   129   and  outstream = outstream
   130   exception Io of {name: string, function: string, cause: exn}
   131   val stdIn 	= std_in
   132   val stdOut 	= std_out
   133   val openIn 	= open_in
   134   val openAppend = open_append
   135   val openOut 	= open_out
   136   val closeIn 	= close_in
   137   val closeOut 	= close_out
   138   val inputN 	= input
   139   val inputAll  = fn is => inputN (is, 999999)
   140   val inputLine = input_line
   141   val endOfStream = end_of_stream
   142   val output 	= output
   143   val flushOut 	= flush_out
   144   end;
   145 
   146 
   147 fun print s = (output (std_out, s); flush_out std_out);