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