src/Pure/library.ML
changeset 31250 4b99b1214034
parent 30572 8fbc355100f2
child 31986 a68f88d264f7
     1.1 --- a/src/Pure/library.ML	Sun May 24 15:02:22 2009 +0200
     1.2 +++ b/src/Pure/library.ML	Sun May 24 15:02:23 2009 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
     1.5    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
     1.6    val funpow: int -> ('a -> 'a) -> 'a -> 'a
     1.7 +  val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
     1.8  
     1.9    (*errors*)
    1.10    exception SYS_ERROR of string
    1.11 @@ -109,6 +110,7 @@
    1.12    val split_list: ('a * 'b) list -> 'a list * 'b list
    1.13    val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    1.14    val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    1.15 +  val multiply: 'a list -> 'a list list -> 'a list list
    1.16    val separate: 'a -> 'a list -> 'a list
    1.17    val surround: 'a -> 'a list -> 'a list
    1.18    val replicate: int -> 'a -> 'a list
    1.19 @@ -157,7 +159,6 @@
    1.20    val unsuffix: string -> string -> string
    1.21    val replicate_string: int -> string -> string
    1.22    val translate_string: (string -> string) -> string -> string
    1.23 -  val multiply: 'a list -> 'a list list -> 'a list list
    1.24    val match_string: string -> string -> bool
    1.25  
    1.26    (*lists as sets -- see also Pure/General/ord_list.ML*)
    1.27 @@ -266,10 +267,12 @@
    1.28  fun (f ooo g) x y z = f (g x y z);
    1.29  fun (f oooo g) x y z w = f (g x y z w);
    1.30  
    1.31 -(*function exponentiation: f(...(f x)...) with n applications of f*)
    1.32 -fun funpow (0: int) _ x = x
    1.33 -  | funpow n f x = funpow (n - 1) f (f x);
    1.34 +(*function exponentiation: f (... (f x) ...) with n applications of f*)
    1.35 +fun funpow (0 : int) _ = I
    1.36 +  | funpow n f = f #> funpow (n - 1) f;
    1.37  
    1.38 +fun funpow_yield (0 : int) _ x = ([], x)
    1.39 +  | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
    1.40  
    1.41  (* errors *)
    1.42  
    1.43 @@ -552,8 +555,6 @@
    1.44      else rep (n, [])
    1.45    end;
    1.46  
    1.47 -fun translate_string f = String.translate (f o String.str);
    1.48 -
    1.49  (*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
    1.50  fun multiply [] _ = []
    1.51    | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
    1.52 @@ -790,6 +791,8 @@
    1.53        if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
    1.54        else replicate_string (k div 2) (a ^ a) ^ a;
    1.55  
    1.56 +fun translate_string f = String.translate (f o String.str);
    1.57 +
    1.58  (*crude matching of str against simple glob pat*)
    1.59  fun match_string pat str =
    1.60    let