# HG changeset patch # User nipkow # Date 1034010111 -7200 # Node ID a46362d2b19b6521c91099ebe9032c519bad8036 # Parent 87482b5e3f2e780515cbc460b130aa84a1cf8723 take/drop -> splitAt diff -r 87482b5e3f2e -r a46362d2b19b src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Oct 04 15:57:32 2002 +0200 +++ b/src/Pure/Isar/locale.ML Mon Oct 07 19:01:51 2002 +0200 @@ -405,11 +405,11 @@ | activate_elem _ ((ctxt, axs), Assumes asms) = let val ts = flat (map (map #1 o #2) asms); - val n = length ts; + val (ps,qs) = splitAt (length ts, axs) val (ctxt', _) = ctxt |> ProofContext.fix_frees ts - |> ProofContext.assume_i (export_axioms (Library.take (n, axs))) asms; - in ((ctxt', Library.drop (n, axs)), []) end + |> ProofContext.assume_i (export_axioms ps) asms; + in ((ctxt', qs), []) end | activate_elem _ ((ctxt, axs), Defines defs) = let val (ctxt', _) = ctxt |> ProofContext.assume_i ProofContext.export_def @@ -627,9 +627,7 @@ val all_propp' = map2 (op ~~) (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp); - val n = length raw_concl; - val concl = Library.take (n, all_propp'); - val propp = Library.drop (n, all_propp'); + val (concl, propp) = splitAt(length raw_concl, all_propp'); val propps = unflat raw_propps propp; val proppss = map (uncurry unflat) (raw_proppss ~~ propps); @@ -695,11 +693,11 @@ val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; - val n = length raw_import_elemss; + val (ps,qs) = splitAt(length raw_import_elemss, all_elemss) val ((import_ctxt, axioms'), (import_elemss, _)) = - activate_facts prep_facts ((context, axioms), Library.take (n, all_elemss)); + activate_facts prep_facts ((context, axioms), ps); val ((ctxt, _), (elemss, _)) = - activate_facts prep_facts ((import_ctxt, axioms'), Library.drop (n, all_elemss)); + activate_facts prep_facts ((import_ctxt, axioms'), qs); in ((((import_ctxt, import_elemss), (ctxt, elemss)), (parms, spec, defs)), concl) end; @@ -899,8 +897,8 @@ fun change_elem _ (axms, Assumes asms) = apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) => - let val n = length spec - in (Library.drop (n, axs), (a, [(Library.take (n, axs), [])])) end)) + let val (ps,qs) = splitAt(length spec, axs) + in (qs, (a, [(ps, [])])) end)) | change_elem f (axms, Notes facts) = (axms, Notes (map (apsnd (map (apfst (map f)))) facts)) | change_elem _ e = e; diff -r 87482b5e3f2e -r a46362d2b19b src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Oct 04 15:57:32 2002 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon Oct 07 19:01:51 2002 +0200 @@ -889,8 +889,7 @@ let val ctxt' = declare_term prop ctxt; val pats = prep_pats ctxt' (raw_pats1 @ raw_pats2); (*simultaneous type inference!*) - val len1 = length raw_pats1; - in ((ctxt', props), (prop, (take (len1, pats), drop (len1, pats)))) end + in ((ctxt', props), (prop, splitAt(length raw_pats1, pats))) end | prep _ = sys_error "prep_propp"; val ((context', _), propp) = foldl_map (foldl_map prep) ((context, prep_props schematic context (flat (map (map fst) args))), args); diff -r 87482b5e3f2e -r a46362d2b19b src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Fri Oct 04 15:57:32 2002 +0200 +++ b/src/Pure/Isar/rule_cases.ML Mon Oct 07 19:01:51 2002 +0200 @@ -113,7 +113,7 @@ val Bi = hhf_nth_subgoal sg (i,prop); val all_xs = Logic.strip_params Bi val n = length all_xs - (if_none open_params 0) - val ind_xs = take(n,all_xs) and goal_xs = drop(n,all_xs) + val (ind_xs, goal_xs) = splitAt(n,all_xs) val rename = if is_none open_params then I else apfst Syntax.internal val xs = map rename ind_xs @ goal_xs val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi); @@ -121,7 +121,8 @@ (case split of None => [("", asms)] | Some t => let val h = length (Logic.strip_assums_hyp(nth_subgoal(i,t))) - in [(hypsN, Library.take (h, asms)), (premsN, Library.drop (h, asms))] end); + val (ps,qs) = splitAt(h, asms) + in [(hypsN, ps), (premsN, qs)] end); val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi); val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl)); in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end; diff -r 87482b5e3f2e -r a46362d2b19b src/Pure/library.ML --- a/src/Pure/library.ML Fri Oct 04 15:57:32 2002 +0200 +++ b/src/Pure/library.ML Mon Oct 07 19:01:51 2002 +0200 @@ -90,6 +90,7 @@ val length: 'a list -> int val take: int * 'a list -> 'a list val drop: int * 'a list -> 'a list + val splitAt: int * 'a list -> 'a list * 'a list val dropwhile: ('a -> bool) -> 'a list -> 'a list val nth_elem: int * 'a list -> 'a val map_nth_elem: int -> ('a -> 'a) -> 'a list -> 'a list @@ -507,6 +508,11 @@ | drop (n, x :: xs) = if n > 0 then drop (n - 1, xs) else x :: xs; +fun splitAt(n,[]) = ([],[]) + | splitAt(n,xs as x::ys) = + if n>0 then let val (ps,qs) = splitAt(n-1,ys) in (x::ps,qs) end + else ([],xs) + fun dropwhile P [] = [] | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys; @@ -532,15 +538,10 @@ | split_last (x :: xs) = apfst (cons x) (split_last xs); (*update nth element*) -fun nth_update x (n, xs) = - let - val prfx = take (n, xs); - val sffx = drop (n, xs); - in - (case sffx of - [] => raise LIST "nth_update" - | _ :: sffx' => prfx @ (x :: sffx')) - end; +fun nth_update x n_xs = + (case splitAt n_xs of + (_,[]) => raise LIST "nth_update" + | (prfx, _ :: sffx') => prfx @ (x :: sffx')) (*find the position of an element in a list*) fun find_index pred = @@ -566,7 +567,8 @@ fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []); fun unflat (xs :: xss) ys = - let val n = length xs in take (n, ys) :: unflat xss (drop (n, ys)) end + let val (ps,qs) = splitAt(length xs,ys) + in ps :: unflat xss qs end | unflat [] [] = [] | unflat _ _ = raise LIST "unflat"; @@ -1032,10 +1034,8 @@ fun fold_bal f [x] = x | fold_bal f [] = raise Balance | fold_bal f xs = - let val k = length xs div 2 - in f (fold_bal f (take(k, xs)), - fold_bal f (drop(k, xs))) - end; + let val (ps,qs) = splitAt(length xs div 2, xs) + in f (fold_bal f ps, fold_bal f qs) end; (*construct something of the form f(...g(...(x)...)) for balanced access*) fun access_bal (f, g, x) n i = diff -r 87482b5e3f2e -r a46362d2b19b src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Oct 04 15:57:32 2002 +0200 +++ b/src/Pure/proofterm.ML Mon Oct 07 19:01:51 2002 +0200 @@ -864,8 +864,7 @@ val prop = (case prf of PThm (_, _, prop, _) => prop | PAxm (_, prop, _) => prop | Oracle (_, prop, _) => prop | _ => error "shrink: proof not in normal form"); val vs = vars_of prop; - val ts' = take (length vs, ts) - val ts'' = drop (length vs, ts) + val (ts', ts'') = splitAt (length vs, ts) val insts = take (length ts', map (fst o dest_Var) vs) ~~ ts'; val nvs = foldl (fn (ixns', (ixn, ixns)) => ixn ins (case assoc (insts, ixn) of diff -r 87482b5e3f2e -r a46362d2b19b src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Oct 04 15:57:32 2002 +0200 +++ b/src/Pure/thm.ML Mon Oct 07 19:01:51 2002 +0200 @@ -1122,11 +1122,9 @@ val m = if k<0 then n+k else k val Bi' = if 0=m orelse m=n then Bi else if 0 subst_bounds (xs, t)) ts'; in (ts'', Ts') end;