TFL/utils.ML
changeset 16854 fdd362b7e980
parent 10769 70b9b0cfe05f
equal deleted inserted replaced
16853:33b886cbdc8f 16854:fdd362b7e980
     8 
     8 
     9 signature UTILS =
     9 signature UTILS =
    10 sig
    10 sig
    11   exception ERR of {module: string, func: string, mesg: string}
    11   exception ERR of {module: string, func: string, mesg: string}
    12   val C: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
    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
    13   val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
    16   val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    14   val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    17   val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
    15   val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
    18   val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
    16   val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
    19   val take: ('a -> 'b) -> int * 'a list -> 'b list
    17   val take: ('a -> 'b) -> int * 'a list -> 'b list
    28 fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
    26 fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
    29 
    27 
    30 
    28 
    31 fun C f x y = f y x
    29 fun C f x y = f y x
    32 
    30 
    33 fun itlist f L base_value =
    31 fun end_itlist f [] = raise (UTILS_ERR "end_itlist" "list too short")
    34    let fun it [] = base_value
    32   | end_itlist f [x] = x 
    35          | it (a::rst) = f a (it rst)
    33   | end_itlist f (x :: xs) = f x (end_itlist f xs);
    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 
    34 
    54 fun itlist2 f L1 L2 base_value =
    35 fun itlist2 f L1 L2 base_value =
    55  let fun it ([],[]) = base_value
    36  let fun it ([],[]) = base_value
    56        | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
    37        | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
    57        | it _ = raise UTILS_ERR "itlist2" "different length lists"
    38        | it _ = raise UTILS_ERR "itlist2" "different length lists"