--- 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;
--- 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);
--- 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;
--- 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 =
--- 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
--- 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<m andalso m<n
- then list_all
- (params,
- Logic.list_implies(List.drop(asms, m) @
- List.take(asms, m),
- concl))
+ then let val (ps,qs) = splitAt(m,asms)
+ in list_all(params, Logic.list_implies(qs @ ps, concl))
+ end
else raise THM("rotate_rule", k, [state])
in (*no fix_shyps*)
Thm{sign_ref = sign_ref,
@@ -1152,10 +1150,8 @@
val m = if k<0 then n_j + k else k
val prop' = if 0 = m orelse m = n_j then prop
else if 0<m andalso m<n_j
- then Logic.list_implies(fixed_prems @
- List.drop(moved_prems, m) @
- List.take(moved_prems, m),
- concl)
+ then let val (ps,qs) = splitAt(m,moved_prems)
+ in Logic.list_implies(fixed_prems @ qs @ ps, concl) end
else raise THM("permute_prems:k", k, [rl])
in (*no fix_shyps*)
Thm{sign_ref = sign_ref,
--- a/src/Pure/type_infer.ML Fri Oct 04 15:57:32 2002 +0200
+++ b/src/Pure/type_infer.ML Mon Oct 07 19:01:51 2002 +0200
@@ -331,9 +331,8 @@
fun prep_output bs ts Ts =
let
val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
- val len = length Ts;
- val Ts' = take (len, Ts_bTs');
- val xs = map Free (map fst bs ~~ drop (len, Ts_bTs'));
+ val (Ts',Ts'') = Library.splitAt(length Ts, Ts_bTs');
+ val xs = map Free (map fst bs ~~ Ts'');
val ts'' = map (fn t => subst_bounds (xs, t)) ts';
in (ts'', Ts') end;