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