src/Pure/basis.ML
author nipkow
Fri Mar 14 10:35:30 1997 +0100 (1997-03-14)
changeset 2792 6c17c5ec3d8b
parent 2470 273580d5c040
child 2862 3f38cbd57d47
permissions -rw-r--r--
Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.
     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 Int =
    22   struct
    23   fun toString (i: int) = makestring i;
    24   fun max (x, y) = if x < y then y else x : int;
    25   fun min (x, y) = if x < y then x else y : int;
    26   end;
    27 
    28 
    29 structure List =
    30   struct
    31   exception Empty
    32 
    33   fun last []      = raise Empty
    34     | last [x]     = x
    35     | last (x::xs) = last xs;
    36 
    37   fun nth (xs, n) =
    38       let fun h []      _ = raise Subscript
    39 	    | h (x::xs) n = if n=0 then x else h xs (n-1)
    40       in if n<0 then raise Subscript else h xs n end;
    41 
    42   fun drop (xs, n) =
    43       let fun h xs      0 = xs
    44 	    | h []      n = raise Subscript
    45 	    | h (x::xs) n = h xs (n-1)
    46       in if n<0 then raise Subscript else h xs n end;
    47 
    48   fun take (xs, n) =
    49       let fun h xs      0 = []
    50 	    | h []      n = raise Subscript
    51 	    | h (x::xs) n = x :: h xs (n-1)
    52       in if n<0 then raise Subscript else h xs n end;
    53 
    54   fun concat []      = []
    55     | concat (l::ls) = l @ concat ls;
    56   end;
    57 
    58 
    59 structure ListPair =
    60   struct
    61   fun zip ([], [])      = []
    62     | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
    63 
    64   fun unzip [] = ([],[])
    65     | unzip((x,y)::pairs) =
    66 	  let val (xs,ys) = unzip pairs
    67 	  in  (x::xs, y::ys)  end;
    68 
    69   fun map f ([], [])      = []
    70     | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
    71 
    72   fun exists pred =
    73     let fun boolf ([], [])      = false
    74 	  | boolf (x::xs,y::ys) = pred(x,y) orelse boolf (xs,ys)
    75     in boolf end;
    76 
    77   fun all pred =
    78     let fun boolf ([], [])      = true
    79 	  | boolf (x::xs,y::ys) = pred(x,y) andalso boolf (xs,ys)
    80     in boolf end;
    81   end;
    82 
    83 
    84 structure TextIO =
    85   struct
    86   type instream = instream
    87   and  outstream = outstream
    88   exception Io of {name: string, function: string, cause: exn}
    89   val stdIn 	= std_in
    90   val stdOut 	= std_out
    91   val openIn 	= open_in
    92   val openAppend = open_append
    93   val openOut 	= open_out
    94   val closeIn 	= close_in
    95   val closeOut 	= close_out
    96   val inputN 	= input
    97   val inputAll  = fn is => inputN (is, 999999)
    98   val inputLine = input_line
    99   val endOfStream = end_of_stream
   100   val output 	= output
   101   val flushOut 	= flush_out
   102   end;
   103 
   104 
   105 fun print s = (output (std_out, s); flush_out std_out);