TFL/utils.ML
author berghofe
Mon, 12 Nov 2001 10:37:36 +0100
changeset 12152 46f128d8133c
parent 10769 70b9b0cfe05f
child 16854 fdd362b7e980
permissions -rw-r--r--
Renamed some bound variables due to changes in simplifier.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      TFL/utils.ML
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     5
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     6
Basic utilities.
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     7
*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     8
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     9
signature UTILS =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    10
sig
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    11
  exception ERR of {module: string, func: string, mesg: string}
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    12
  val C: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    13
  val itlist: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    14
  val rev_itlist: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    15
  val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    16
  val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    17
  val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    18
  val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    19
  val take: ('a -> 'b) -> int * 'a list -> 'b list
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    20
end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    21
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    22
structure Utils: UTILS =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    23
struct
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    24
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    25
(*standard exception for TFL*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    26
exception ERR of {module: string, func: string, mesg: string};
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    27
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    28
fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    29
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    30
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    31
fun C f x y = f y x
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    32
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    33
fun itlist f L base_value =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    34
   let fun it [] = base_value
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    35
         | it (a::rst) = f a (it rst)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    36
   in it L
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    37
   end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    38
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    39
fun rev_itlist f =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    40
   let fun rev_it [] base = base
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    41
         | rev_it (a::rst) base = rev_it rst (f a base)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    42
   in rev_it
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    43
   end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    44
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    45
fun end_itlist f =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    46
   let fun endit [] = raise UTILS_ERR "end_itlist" "list too short"
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    47
         | endit alist =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    48
            let val (base::ralist) = rev alist
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    49
            in itlist f (rev ralist) base
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    50
            end
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    51
   in endit
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    52
   end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    53
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    54
fun itlist2 f L1 L2 base_value =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    55
 let fun it ([],[]) = base_value
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    56
       | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    57
       | it _ = raise UTILS_ERR "itlist2" "different length lists"
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    58
 in  it (L1,L2)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    59
 end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    60
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    61
fun pluck p  =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    62
  let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found"
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    63
        | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    64
  in fn L => remv(L,[])
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    65
  end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    66
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    67
fun take f =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    68
  let fun grab(0,L) = []
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    69
        | grab(n, x::rst) = f x::grab(n-1,rst)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    70
  in grab
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    71
  end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    72
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    73
fun zip3 [][][] = []
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    74
  | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    75
  | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths";
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    76
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    77
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    78
end;