--- a/src/HOL/Import/lazy_seq.ML Thu Nov 16 01:07:23 2006 +0100
+++ b/src/HOL/Import/lazy_seq.ML Thu Nov 16 01:07:25 2006 +0100
@@ -453,7 +453,7 @@
(*partial function as procedure*)
fun try f x =
make (fn () =>
- case Library.try f x of
+ case Basics.try f x of
SOME y => SOME(y,Seq (value NONE))
| NONE => NONE)
@@ -528,7 +528,7 @@
else
case getItem xq of
NONE => ([], xq)
- | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))
+ | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1, xq'))
fun foldl f e s =
let
--- a/src/HOL/Tools/inductive_realizer.ML Thu Nov 16 01:07:23 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Nov 16 01:07:25 2006 +0100
@@ -295,7 +295,7 @@
val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
val (_, params) = strip_comb S;
val params' = map dest_Var params;
- val rss = [] |> Library.fold add_rule intrs;
+ val rss = [] |> fold add_rule intrs;
val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
--- a/src/HOL/Tools/old_inductive_package.ML Thu Nov 16 01:07:23 2006 +0100
+++ b/src/HOL/Tools/old_inductive_package.ML Thu Nov 16 01:07:25 2006 +0100
@@ -403,7 +403,7 @@
val ind_prems = map mk_ind_prem intr_ts;
- val factors = Library.fold (mg_prod_factors preds) ind_prems [];
+ val factors = fold (mg_prod_factors preds) ind_prems [];
(* make conclusions for induction rules *)
@@ -814,7 +814,7 @@
(* external interfaces *)
fun try_term f msg thy t =
- (case Library.try f t of
+ (case try f t of
SOME x => x
| NONE => error (msg ^ Sign.string_of_term thy t));
--- a/src/HOL/ex/svc_funcs.ML Thu Nov 16 01:07:23 2006 +0100
+++ b/src/HOL/ex/svc_funcs.ML Thu Nov 16 01:07:25 2006 +0100
@@ -73,7 +73,7 @@
" " ^ File.shell_path svc_input_file ^
">/dev/null 2>&1"))
val svc_output =
- (case Library.try File.read svc_output_file of
+ (case try File.read svc_output_file of
SOME out => out
| NONE => error "SVC returned no output");
in
--- a/src/Provers/IsaPlanner/zipper.ML Thu Nov 16 01:07:23 2006 +0100
+++ b/src/Provers/IsaPlanner/zipper.ML Thu Nov 16 01:07:25 2006 +0100
@@ -215,7 +215,7 @@
fun add_outerctxt ctop cbottom = cbottom @ ctop;
(* mkterm : zipper -> trm -> trm *)
- val apply = Library.fold D.apply;
+ val apply = Basics.fold D.apply;
(* named type context *)
val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys
@@ -228,7 +228,7 @@
val map = List.map : (D.dtrm -> D.dtrm) -> T -> T
- val fold = Library.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
+ val fold = Basics.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
end;
--- a/src/Pure/General/seq.ML Thu Nov 16 01:07:23 2006 +0100
+++ b/src/Pure/General/seq.ML Thu Nov 16 01:07:25 2006 +0100
@@ -80,7 +80,7 @@
(*partial function as procedure*)
fun try f x =
- (case Library.try f x of
+ (case Basics.try f x of
SOME y => single y
| NONE => empty);
@@ -92,7 +92,7 @@
else
(case pull xq of
NONE => ([], xq)
- | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1) xq'));
+ | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1) xq'));
(*conversion from sequence to list*)
fun list_of xq =
--- a/src/Pure/IsaMakefile Thu Nov 16 01:07:23 2006 +0100
+++ b/src/Pure/IsaMakefile Thu Nov 16 01:07:25 2006 +0100
@@ -23,16 +23,15 @@
Pure: $(OUT)/Pure$(ML_SUFFIX)
-$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML \
- General/buffer.ML General/file.ML General/graph.ML General/heap.ML \
- General/history.ML General/name_space.ML \
- General/ord_list.ML General/output.ML General/path.ML \
- General/position.ML General/pretty.ML General/rat.ML General/scan.ML \
- General/secure.ML General/seq.ML General/source.ML General/stack.ML \
- General/susp.ML General/symbol.ML General/table.ML General/url.ML \
- General/xml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \
- Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML \
- Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML \
+$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML \
+ General/basics.ML General/buffer.ML General/file.ML General/graph.ML \
+ General/heap.ML General/history.ML General/name_space.ML General/ord_list.ML \
+ General/output.ML General/path.ML General/position.ML General/pretty.ML \
+ General/rat.ML General/scan.ML General/secure.ML General/seq.ML \
+ General/source.ML General/stack.ML General/susp.ML General/symbol.ML \
+ General/table.ML General/url.ML General/xml.ML Isar/ROOT.ML Isar/antiquote.ML \
+ Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \
+ Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML \
Isar/induct_attrib.ML Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML \
Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \
--- a/src/Pure/Isar/rule_cases.ML Thu Nov 16 01:07:23 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML Thu Nov 16 01:07:25 2006 +0100
@@ -234,8 +234,9 @@
val save_consumes = put_consumes o lookup_consumes;
fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
+
fun consumes_default n x =
- if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
+ if is_some (lookup_consumes (#2 x)) then x else consumes n x;
--- a/src/Pure/library.ML Thu Nov 16 01:07:23 2006 +0100
+++ b/src/Pure/library.ML Thu Nov 16 01:07:25 2006 +0100
@@ -5,15 +5,16 @@
Basic library: functions, options, pairs, booleans, lists, integers,
strings, lists as sets, balanced trees, orders, current directory, misc.
+
+See also General/basics.ML for the most fundamental concepts.
*)
-infix 1 |> |-> ||> ||>> |>> #> #-> ##> ##>> #>> |>>> ;
-infix 2 ?;
-infix 3 o oo ooo oooo;
-
-infix 4 ~~ upto downto;
+infix 1 |>>>
+infix 2 ?
+infix 3 o oo ooo oooo
+infix 4 ~~ upto downto
infix orf andf \ \\ mem mem_int mem_string union union_int
- union_string inter inter_int inter_string subset subset_int subset_string;
+ union_string inter inter_int inter_string subset subset_int subset_string
signature BASIC_LIBRARY =
sig
@@ -22,37 +23,14 @@
val K: 'a -> 'b -> 'a
val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
- val |> : 'a * ('a -> 'b) -> 'b
- val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
- val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
- val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
- val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
- val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
- val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
- val ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd
- val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd
- val #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b
val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
val ? : ('a -> bool) * ('a -> 'a) -> 'a -> 'a
- val ` : ('b -> 'a) -> 'b -> 'a * 'b
- val tap: ('b -> 'a) -> 'b -> 'b
val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
val funpow: int -> ('a -> 'a) -> 'a -> 'a
- (*options*)
- val the: 'a option -> 'a
- val these: 'a list option -> 'a list
- val the_default: 'a -> 'a option -> 'a
- val the_list: 'a option -> 'a list
- val is_some: 'a option -> bool
- val is_none: 'a option -> bool
- val perhaps: ('a -> 'a option) -> 'a -> 'a
-
(*exceptions*)
- val try: ('a -> 'b) -> 'a -> 'b option
- val can: ('a -> 'b) -> 'a -> bool
exception EXCEPTION of exn * string
val do_transform_failure: bool ref
val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
@@ -102,22 +80,17 @@
(*lists*)
exception UnequalLengths
- val cons: 'a -> 'a list -> 'a list
val single: 'a -> 'a list
val the_single: 'a list -> 'a
val singleton: ('a list -> 'b list) -> 'a -> 'b
- val append: 'a list -> 'a list -> 'a list
val apply: ('a -> 'a) list -> 'a -> 'a
- val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
- val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
- val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
val flat: 'a list list -> 'a list
- val maps: ('a -> 'b list) -> 'a list -> 'b list
val unflat: 'a list list -> 'b list -> 'b list list
val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
+ val maps: ('a -> 'b list) -> 'a list -> 'b list
val chop: int -> 'a list -> 'a list * 'a list
val dropwhile: ('a -> bool) -> 'a list -> 'a list
val nth: 'a list -> int -> 'a
@@ -290,36 +263,19 @@
structure Library: LIBRARY =
struct
-
-(** functions **)
+(* functions *)
fun I x = x;
fun K x = fn _ => x;
fun curry f x y = f (x, y);
fun uncurry f (x, y) = f x y;
-(*reverse application and structured results*)
-fun x |> f = f x;
-fun (x, y) |-> f = f x y;
-fun (x, y) |>> f = (f x, y);
-fun (x, y) ||> f = (x, f y);
+(*application and structured results -- old version*)
fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
-fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
-
-(*reverse composition and structured results*)
-fun f #> g = g o f;
-fun f #-> g = uncurry g o f;
-fun (f ##> g) x = let val (y, z) = f x in (y, g z) end;
-fun (f ##>> g) x = let val (y, z) = f x; val (w, u) = g z in ((y, w), u) end;
-fun (f #>> g) x = let val (y, z) = f x in (g y, z) end;
(*conditional application*)
fun b ? f = fn x => if b x then f x else x;
-(*view results*)
-fun `f = fn x => (f x, x);
-fun tap f = fn x => (f x; x);
-
(*composition with multiple args*)
fun (f oo g) x y = f (g x y);
fun (f ooo g) x y z = f (g x y z);
@@ -332,28 +288,6 @@
in rep (n, x) end;
-(** options **)
-
-val the = Option.valOf;
-
-fun these (SOME x) = x
- | these _ = [];
-
-fun the_default x (SOME y) = y
- | the_default x _ = x;
-
-fun the_list (SOME x) = [x]
- | the_list _ = []
-
-fun is_some (SOME _) = true
- | is_some NONE = false;
-
-fun is_none (SOME _) = false
- | is_none NONE = true;
-
-fun perhaps f x = the_default x (f x);
-
-
(* exceptions *)
val do_transform_failure = ref true;
@@ -365,13 +299,6 @@
exception EXCEPTION of exn * string;
-
-fun try f x = SOME (f x)
- handle Interrupt => raise Interrupt | _ => NONE;
-
-fun can f x = is_some (try f x);
-
-
datatype 'a result =
Result of 'a |
Exn of exn;
@@ -409,7 +336,7 @@
in ass list end;
-(** pairs **)
+(* pairs *)
fun pair x y = (x, y);
fun rpair x y = (y, x);
@@ -431,20 +358,16 @@
fun string_of_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
-(** booleans **)
+(* booleans *)
-(* equality *)
-
+(*polymorphic equality*)
fun equal x y = x = y;
fun not_equal x y = x <> y;
-(* operators for combining predicates *)
-
+(*combining predicates*)
fun p orf q = fn x => p x orelse q x;
fun p andf q = fn x => p x andalso q x;
-(* predicates on lists *)
-
(*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
fun exists (pred: 'a -> bool) : 'a list -> bool =
let fun boolf [] = false
@@ -481,12 +404,11 @@
fun conditional b f = if b then f () else ();
+
(** lists **)
exception UnequalLengths;
-fun cons x xs = x :: xs;
-
fun single x = [x];
fun the_single [x] = x
@@ -494,35 +416,11 @@
fun singleton f x = the_single (f [x]);
-fun append xs ys = xs @ ys;
-
fun apply [] x = x
| apply (f :: fs) x = apply fs (f x);
-(* fold *)
-
-fun fold f =
- let
- fun fold_aux [] y = y
- | fold_aux (x :: xs) y = fold_aux xs (f x y);
- in fold_aux end;
-
-fun fold_rev f =
- let
- fun fold_aux [] y = y
- | fold_aux (x :: xs) y = f x (fold_aux xs y);
- in fold_aux end;
-
-fun fold_map f =
- let
- fun fold_aux [] y = ([], y)
- | fold_aux (x :: xs) y =
- let
- val (x', y') = f x y;
- val (xs', y'') = fold_aux xs y';
- in (x' :: xs', y'') end;
- in fold_aux end;
+(* fold -- old versions *)
(*the following versions of fold are designed to fit nicely with infixes*)
@@ -570,9 +468,7 @@
fun maps f [] = []
| maps f (x :: xs) = f x @ maps f xs;
-fun chop 0 xs = ([], xs)
- | chop _ [] = ([], [])
- | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
+fun chop n xs = unfold_rev n dest xs;
(*take the first n elements from a list*)
fun take (n, []) = []