src/HOL/Tools/TFL/utils.ML
author wenzelm
Thu, 31 May 2007 13:18:52 +0200
changeset 23150 073a65f0bc40
child 41589 bbd861837ebc
permissions -rw-r--r--
moved TFL files to canonical place;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23150
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/TFL/utils.ML
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     5
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     6
Basic utilities.
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     7
*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     8
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
     9
signature UTILS =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    10
sig
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    11
  exception ERR of {module: string, func: string, mesg: string}
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    12
  val C: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    13
  val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    14
  val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    15
  val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    16
  val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    17
  val take: ('a -> 'b) -> int * 'a list -> 'b list
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    18
end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    19
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    20
structure Utils: UTILS =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    21
struct
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    22
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    23
(*standard exception for TFL*)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    24
exception ERR of {module: string, func: string, mesg: string};
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    25
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    26
fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    27
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    28
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    29
fun C f x y = f y x
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    30
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    31
fun end_itlist f [] = raise (UTILS_ERR "end_itlist" "list too short")
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    32
  | end_itlist f [x] = x 
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    33
  | end_itlist f (x :: xs) = f x (end_itlist f xs);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    34
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    35
fun itlist2 f L1 L2 base_value =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    36
 let fun it ([],[]) = base_value
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    37
       | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    38
       | it _ = raise UTILS_ERR "itlist2" "different length lists"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    39
 in  it (L1,L2)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    40
 end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    41
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    42
fun pluck p  =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    43
  let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found"
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    44
        | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    45
  in fn L => remv(L,[])
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    46
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    47
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    48
fun take f =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    49
  let fun grab(0,L) = []
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    50
        | grab(n, x::rst) = f x::grab(n-1,rst)
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    51
  in grab
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    52
  end;
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    53
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    54
fun zip3 [][][] = []
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    55
  | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    56
  | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths";
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    57
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    58
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    59
end;