# HG changeset patch # User wenzelm # Date 1147777287 -7200 # Node ID 0b01436e184305d65caed5c76973349b89f0832c # Parent 213e12ad2c0328e88ba814354b7fded82c3e7ccd added divide_and_conquer combinator (by Amine Chaieb); removed remains of old option type; removed obsolete eq_opt; removed obsolete string_of_bool (use Bool.toString instead); tuned; diff -r 213e12ad2c03 -r 0b01436e1843 src/Pure/library.ML --- a/src/Pure/library.ML Tue May 16 13:01:26 2006 +0200 +++ b/src/Pure/library.ML Tue May 16 13:01:27 2006 +0200 @@ -38,10 +38,6 @@ val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b val funpow: int -> ('a -> 'a) -> 'a -> 'a - (*old options -- invalidated*) - datatype invalid = None of invalid - exception OPTION of invalid - (*options*) val the: 'a option -> 'a val these: 'a list option -> 'a list @@ -50,9 +46,7 @@ val is_some: 'a option -> bool val is_none: 'a option -> bool val perhaps: ('a -> 'a option) -> 'a -> 'a - val eq_opt: ('a * 'b -> bool) -> 'a option * 'b option -> bool val merge_opt: ('a * 'a -> bool) -> 'a option * 'a option -> 'a option - val string_of_option: ('a -> string) -> 'a option -> string (*exceptions*) val try: ('a -> 'b) -> 'a -> 'b option @@ -103,7 +97,6 @@ val change: 'a ref -> ('a -> 'a) -> unit val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c val conditional: bool -> (unit -> unit) -> unit - val string_of_bool: bool -> string (*lists*) exception UnequalLengths @@ -156,7 +149,6 @@ val prefixes: 'a list -> 'a list list val suffixes1: 'a list -> 'a list list val suffixes: 'a list -> 'a list list - val string_of_list: ('a -> string) -> 'a list -> string (*integers*) val gcd: IntInf.int * IntInf.int -> IntInf.int @@ -196,6 +188,8 @@ val unsuffix: string -> string -> string val replicate_string: int -> string -> string val translate_string: (string -> string) -> string -> string + val string_of_list: ('a -> string) -> 'a list -> string + val string_of_option: ('a -> string) -> 'a option -> string (*lists as sets -- see also Pure/General/ord_list.ML*) val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool @@ -272,6 +266,7 @@ val pwd: unit -> string (*misc*) + val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list val gensym: string -> string @@ -340,10 +335,6 @@ (** options **) -(*invalidate former constructors to prevent accidental use as match-all patterns!*) -datatype invalid = None of invalid; -exception OPTION of invalid; - val the = Option.valOf; fun these (SOME x) = x @@ -363,17 +354,10 @@ fun perhaps f x = the_default x (f x); -fun eq_opt eq (NONE, NONE) = true - | eq_opt eq (SOME x, SOME y) = eq (x, y) - | eq_opt _ _ = false; - fun merge_opt _ (NONE, y) = y | merge_opt _ (x, NONE) = x | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option; -fun string_of_option f NONE = "NONE" - | string_of_option f (SOME x) = "SOME (" ^ f x ^ ")"; - (* exceptions *) @@ -478,6 +462,7 @@ | boolf (x :: xs) = pred x andalso boolf xs in boolf end; + (* flags *) fun set flag = (flag := true; true); @@ -495,14 +480,11 @@ val _ = flag := orig_value; in release result end; + (* conditional execution *) fun conditional b f = if b then f () else (); -(* convert a bool to a string *) - -fun string_of_bool b = if b then "true" else "false"; - (** lists **) @@ -851,11 +833,6 @@ fun oct_char s = chr (#1 (read_radixint (8, explode s))); -(* convert a list to a string *) - -fun string_of_list f xs = - let val fxs = separate ", " (map f xs) - in String.concat ("[" :: fxs @ ["]"]) end; (** strings **) @@ -943,6 +920,11 @@ if k mod 2 = 0 then replicate_string (k div 2) (a ^ a) else replicate_string (k div 2) (a ^ a) ^ a; +fun string_of_list f = enclose "[" "]" o commas o map f; + +fun string_of_option f NONE = "NONE" + | string_of_option f (SOME x) = "SOME (" ^ f x ^ ")"; + (** lists as sets -- see also Pure/General/ord_list.ML **) @@ -1143,11 +1125,6 @@ else if rel (y, x) then GREATER else EQUAL; -fun eq_ord ord xy = - case ord xy - of EQUAL => true - | _ => false; - val int_ord = Int.compare; val string_ord = String.compare; @@ -1244,8 +1221,13 @@ val pwd = OS.FileSys.getDir; + (** misc **) +fun divide_and_conquer decomp x = + let val (ys, recomb) = decomp x + in recomb (map (divide_and_conquer decomp) ys) end; + (*Partition list into elements that satisfy predicate and those that don't. Preserves order of elements in both lists.*) val partition = List.partition;