# HG changeset patch # User wenzelm # Date 1163635645 -3600 # Node ID f34ac19659aea0d51e03fc376fb40adcd7943050 # Parent 9f20604d2b5e40b640fe16e3a76149843375a964 moved some fundamental concepts to General/basics.ML; diff -r 9f20604d2b5e -r f34ac19659ae src/HOL/Import/lazy_seq.ML --- 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 diff -r 9f20604d2b5e -r f34ac19659ae src/HOL/Tools/inductive_realizer.ML --- 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; diff -r 9f20604d2b5e -r f34ac19659ae src/HOL/Tools/old_inductive_package.ML --- 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)); diff -r 9f20604d2b5e -r f34ac19659ae src/HOL/ex/svc_funcs.ML --- 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 diff -r 9f20604d2b5e -r f34ac19659ae src/Provers/IsaPlanner/zipper.ML --- 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; diff -r 9f20604d2b5e -r f34ac19659ae src/Pure/General/seq.ML --- 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 = diff -r 9f20604d2b5e -r f34ac19659ae src/Pure/IsaMakefile --- 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 \ diff -r 9f20604d2b5e -r f34ac19659ae src/Pure/Isar/rule_cases.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; diff -r 9f20604d2b5e -r f34ac19659ae src/Pure/library.ML --- 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, []) = []