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