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.
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@2217
    21
structure Int =
paulson@2217
    22
  struct
paulson@2230
    23
  fun toString (i: int) = makestring i;
paulson@2217
    24
  fun max (x, y) = if x < y then y else x : int;
paulson@2217
    25
  fun min (x, y) = if x < y then x else y : int;
paulson@2217
    26
  end;
paulson@2217
    27
paulson@2265
    28
paulson@2265
    29
structure List =
paulson@2265
    30
  struct
paulson@2265
    31
  exception Empty
paulson@2265
    32
paulson@2265
    33
  fun last []      = raise Empty
paulson@2265
    34
    | last [x]     = x
paulson@2265
    35
    | last (x::xs) = last xs;
paulson@2265
    36
paulson@2265
    37
  fun nth (xs, n) =
paulson@2265
    38
      let fun h []      _ = raise Subscript
paulson@2265
    39
	    | h (x::xs) n = if n=0 then x else h xs (n-1)
paulson@2265
    40
      in if n<0 then raise Subscript else h xs n end;
paulson@2265
    41
paulson@2265
    42
  fun drop (xs, n) =
paulson@2265
    43
      let fun h xs      0 = xs
paulson@2265
    44
	    | h []      n = raise Subscript
paulson@2265
    45
	    | h (x::xs) n = h xs (n-1)
paulson@2265
    46
      in if n<0 then raise Subscript else h xs n end;
paulson@2265
    47
paulson@2265
    48
  fun take (xs, n) =
paulson@2265
    49
      let fun h xs      0 = []
paulson@2265
    50
	    | h []      n = raise Subscript
paulson@2265
    51
	    | h (x::xs) n = x :: h xs (n-1)
paulson@2265
    52
      in if n<0 then raise Subscript else h xs n end;
paulson@2265
    53
paulson@2265
    54
  fun concat []      = []
paulson@2265
    55
    | concat (l::ls) = l @ concat ls;
paulson@2265
    56
  end;
paulson@2265
    57
paulson@2265
    58
paulson@2265
    59
structure ListPair =
paulson@2265
    60
  struct
paulson@2265
    61
  fun zip ([], [])      = []
paulson@2265
    62
    | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
paulson@2265
    63
paulson@2265
    64
  fun unzip [] = ([],[])
paulson@2265
    65
    | unzip((x,y)::pairs) =
paulson@2265
    66
	  let val (xs,ys) = unzip pairs
paulson@2265
    67
	  in  (x::xs, y::ys)  end;
paulson@2265
    68
paulson@2265
    69
  fun map f ([], [])      = []
paulson@2265
    70
    | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
paulson@2265
    71
paulson@2265
    72
  fun exists pred =
paulson@2265
    73
    let fun boolf ([], [])      = false
paulson@2265
    74
	  | boolf (x::xs,y::ys) = pred(x,y) orelse boolf (xs,ys)
paulson@2265
    75
    in boolf end;
paulson@2265
    76
paulson@2265
    77
  fun all pred =
paulson@2265
    78
    let fun boolf ([], [])      = true
paulson@2265
    79
	  | boolf (x::xs,y::ys) = pred(x,y) andalso boolf (xs,ys)
paulson@2265
    80
    in boolf end;
paulson@2265
    81
  end;
paulson@2265
    82
paulson@2265
    83
paulson@2217
    84
structure TextIO =
paulson@2217
    85
  struct
paulson@2217
    86
  type instream = instream
paulson@2217
    87
  and  outstream = outstream
paulson@2217
    88
  exception Io of {name: string, function: string, cause: exn}
paulson@2217
    89
  val stdIn 	= std_in
paulson@2217
    90
  val stdOut 	= std_out
paulson@2217
    91
  val openIn 	= open_in
paulson@2217
    92
  val openAppend = open_append
paulson@2217
    93
  val openOut 	= open_out
paulson@2217
    94
  val closeIn 	= close_in
paulson@2217
    95
  val closeOut 	= close_out
paulson@2217
    96
  val inputN 	= input
paulson@2217
    97
  val inputAll  = fn is => inputN (is, 999999)
paulson@2217
    98
  val inputLine = input_line
paulson@2217
    99
  val endOfStream = end_of_stream
paulson@2217
   100
  val output 	= output
paulson@2217
   101
  val flushOut 	= flush_out
paulson@2217
   102
  end;
paulson@2470
   103
paulson@2470
   104
paulson@2470
   105
fun print s = (output (std_out, s); flush_out std_out);