src/Pure/basis.ML
author wenzelm
Tue Jul 28 17:02:41 1998 +0200 (1998-07-28)
changeset 5208 cea0adbc7276
parent 5021 235f8508d440
child 5643 983ce1421211
permissions -rw-r--r--
added Real structure (taken from SML/NJ basis lib);
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@5021
     6
Basis Library emulation.  Needed for Poly/ML and Standard ML of New
wenzelm@5021
     7
Jersey version 0.93 to 1.08.  Full compatibility cannot be obtained
wenzelm@5021
     8
using a file: what about char constants?
paulson@2217
     9
*)
paulson@2217
    10
paulson@2265
    11
exception Subscript;
paulson@2265
    12
paulson@2230
    13
structure Bool =
paulson@2230
    14
  struct
paulson@2230
    15
  fun toString true  = "true"
paulson@2230
    16
    | toString false = "false"
paulson@2230
    17
  end;
paulson@2230
    18
paulson@3244
    19
paulson@3244
    20
structure Option =
paulson@2862
    21
  struct
paulson@2862
    22
  exception Option
paulson@2862
    23
paulson@2862
    24
  datatype 'a option = NONE | SOME of 'a
paulson@2862
    25
paulson@2862
    26
  fun getOpt (SOME v, _) = v
paulson@2862
    27
    | getOpt (NONE,   a) = a
paulson@2862
    28
paulson@2862
    29
  fun isSome (SOME _) = true 
paulson@2862
    30
    | isSome NONE     = false
paulson@2862
    31
paulson@2862
    32
  fun valOf (SOME v) = v
paulson@2862
    33
    | valOf NONE     = raise Option
paulson@2862
    34
  end;
paulson@2862
    35
paulson@2862
    36
paulson@2217
    37
structure Int =
paulson@2217
    38
  struct
paulson@2230
    39
  fun toString (i: int) = makestring i;
paulson@2217
    40
  fun max (x, y) = if x < y then y else x : int;
paulson@2217
    41
  fun min (x, y) = if x < y then x else y : int;
paulson@2217
    42
  end;
paulson@2217
    43
paulson@2265
    44
wenzelm@5208
    45
structure Real =
wenzelm@5208
    46
  struct
wenzelm@5208
    47
  fun toString (x: real) = makestring x;
wenzelm@5208
    48
  fun max (x, y) = if x < y then y else x : real;
wenzelm@5208
    49
  fun min (x, y) = if x < y then x else y : real;
wenzelm@5208
    50
  val real = real;
wenzelm@5208
    51
  val floor = floor;
wenzelm@5208
    52
  fun ceil x = ~1 - floor (~ (x + 1.0));
wenzelm@5208
    53
  fun round x = floor (x + 0.5);  (*does not do round-to-nearest*)
wenzelm@5208
    54
  fun trunc x = if x < 0.0 then ceil x else floor x;
wenzelm@5208
    55
  end;
wenzelm@5208
    56
wenzelm@5208
    57
paulson@2265
    58
structure List =
paulson@2265
    59
  struct
paulson@2265
    60
  exception Empty
paulson@2265
    61
paulson@2265
    62
  fun last []      = raise Empty
paulson@2265
    63
    | last [x]     = x
paulson@2265
    64
    | last (x::xs) = last xs;
paulson@2265
    65
paulson@2265
    66
  fun nth (xs, n) =
paulson@2265
    67
      let fun h []      _ = raise Subscript
paulson@2265
    68
	    | h (x::xs) n = if n=0 then x else h xs (n-1)
paulson@2265
    69
      in if n<0 then raise Subscript else h xs n end;
paulson@2265
    70
paulson@2265
    71
  fun drop (xs, n) =
paulson@2265
    72
      let fun h xs      0 = xs
paulson@2265
    73
	    | h []      n = raise Subscript
paulson@2265
    74
	    | h (x::xs) n = h xs (n-1)
paulson@2265
    75
      in if n<0 then raise Subscript else h xs n end;
paulson@2265
    76
paulson@2265
    77
  fun take (xs, n) =
paulson@2265
    78
      let fun h xs      0 = []
paulson@2265
    79
	    | h []      n = raise Subscript
paulson@2265
    80
	    | h (x::xs) n = x :: h xs (n-1)
paulson@2265
    81
      in if n<0 then raise Subscript else h xs n end;
paulson@2265
    82
paulson@2265
    83
  fun concat []      = []
paulson@2265
    84
    | concat (l::ls) = l @ concat ls;
paulson@2862
    85
paulson@2862
    86
  fun mapPartial f []      = []
paulson@2862
    87
    | mapPartial f (x::xs) = 
paulson@3244
    88
         (case f x of Option.NONE   => mapPartial f xs
paulson@3244
    89
                    | Option.SOME y => y :: mapPartial f xs);
paulson@2884
    90
paulson@3244
    91
  fun find _ []        = Option.NONE
paulson@3244
    92
    | find p (x :: xs) = if p x then Option.SOME x else find p xs;
paulson@2884
    93
paulson@2884
    94
paulson@2884
    95
  (*copy the list preserving elements that satisfy the predicate*)
paulson@2884
    96
  fun filter p [] = []
paulson@2884
    97
    | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
paulson@2884
    98
paulson@2884
    99
  (*Partition list into elements that satisfy predicate and those that don't.
paulson@2884
   100
    Preserves order of elements in both lists.*)
paulson@2884
   101
  fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
paulson@2884
   102
      let fun part ([], answer) = answer
paulson@2884
   103
	    | part (x::xs, (ys, ns)) = if p(x)
paulson@2884
   104
	      then  part (xs, (x::ys, ns))
paulson@2884
   105
	      else  part (xs, (ys, x::ns))
paulson@2884
   106
      in  part (rev ys, ([], []))  end;
paulson@2884
   107
paulson@2265
   108
  end;
paulson@2265
   109
paulson@2265
   110
paulson@2265
   111
structure ListPair =
paulson@2265
   112
  struct
paulson@2265
   113
  fun zip ([], [])      = []
paulson@2265
   114
    | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
paulson@2265
   115
paulson@2265
   116
  fun unzip [] = ([],[])
paulson@2265
   117
    | unzip((x,y)::pairs) =
paulson@2265
   118
	  let val (xs,ys) = unzip pairs
paulson@2265
   119
	  in  (x::xs, y::ys)  end;
paulson@2265
   120
paulson@2265
   121
  fun map f ([], [])      = []
paulson@2265
   122
    | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
paulson@2265
   123
paulson@2884
   124
  fun exists p =
paulson@2265
   125
    let fun boolf ([], [])      = false
paulson@2884
   126
	  | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
paulson@2265
   127
    in boolf end;
paulson@2265
   128
paulson@2884
   129
  fun all p =
paulson@2265
   130
    let fun boolf ([], [])      = true
paulson@2884
   131
	  | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
paulson@2265
   132
    in boolf end;
paulson@2265
   133
  end;
paulson@2265
   134
paulson@2265
   135
paulson@2217
   136
structure TextIO =
paulson@2217
   137
  struct
paulson@2217
   138
  type instream = instream
paulson@2217
   139
  and  outstream = outstream
paulson@2217
   140
  exception Io of {name: string, function: string, cause: exn}
paulson@2217
   141
  val stdIn 	= std_in
paulson@2217
   142
  val stdOut 	= std_out
paulson@2217
   143
  val openIn 	= open_in
paulson@2217
   144
  val openAppend = open_append
paulson@2217
   145
  val openOut 	= open_out
paulson@2217
   146
  val closeIn 	= close_in
paulson@2217
   147
  val closeOut 	= close_out
paulson@2217
   148
  val inputN 	= input
paulson@2217
   149
  val inputAll  = fn is => inputN (is, 999999)
paulson@2217
   150
  val inputLine = input_line
paulson@2217
   151
  val endOfStream = end_of_stream
paulson@2217
   152
  val output 	= output
paulson@2217
   153
  val flushOut 	= flush_out
paulson@2217
   154
  end;
paulson@2470
   155
paulson@2470
   156
paulson@2470
   157
fun print s = (output (std_out, s); flush_out std_out);
wenzelm@5021
   158
wenzelm@5021
   159
wenzelm@5021
   160
structure General =
wenzelm@5021
   161
struct
wenzelm@5021
   162
wenzelm@5021
   163
local
wenzelm@5021
   164
  fun raised name = "exception " ^ name ^ " raised";
wenzelm@5021
   165
  fun raised_msg name msg = raised name ^ ": " ^ msg;
wenzelm@5021
   166
in
wenzelm@5021
   167
  fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure"
wenzelm@5021
   168
    | exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure"
wenzelm@5021
   169
    | exnMessage Interrupt = "Interrupt"
wenzelm@5021
   170
    | exnMessage (Io msg) = "I/O error: " ^ msg
wenzelm@5021
   171
    | exnMessage Neg = raised "Neg"
wenzelm@5021
   172
    | exnMessage Sum = raised "Sum"
wenzelm@5021
   173
    | exnMessage Diff = raised "Diff"
wenzelm@5021
   174
    | exnMessage Prod = raised "Prod"
wenzelm@5021
   175
    | exnMessage Quot = raised "Quot"
wenzelm@5021
   176
    | exnMessage Abs = raised "Abs"
wenzelm@5021
   177
    | exnMessage Div = raised "Div"
wenzelm@5021
   178
    | exnMessage Mod = raised "Mod"
wenzelm@5021
   179
    | exnMessage Floor = raised "Floor"
wenzelm@5021
   180
    | exnMessage Sqrt = raised "Sqrt"
wenzelm@5021
   181
    | exnMessage Exp = raised "Exp"
wenzelm@5021
   182
    | exnMessage Ln = raised "Ln"
wenzelm@5021
   183
    | exnMessage Ord = raised "Ord"
wenzelm@5021
   184
    | exnMessage Subscript = raised_msg "Subscript " "subscript out of bounds"
wenzelm@5021
   185
    | exnMessage Option.Option = raised "Option.Option"
wenzelm@5021
   186
    | exnMessage List.Empty = raised "List.Empty"
wenzelm@5021
   187
    | exnMessage (TextIO.Io {name, ...}) = raised_msg "TextIO.Io" name
wenzelm@5021
   188
    | exnMessage exn = raised "???";
wenzelm@5021
   189
end;
wenzelm@5021
   190
wenzelm@5021
   191
end;