--- a/src/HOL/Library/conditional_parametricity.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Library/conditional_parametricity.ML Sun Jan 28 19:28:52 2018 +0100
@@ -73,7 +73,7 @@
(case t of
Var (xi, _) =>
let
- val (bounds, tail) = take_prefix is_Bound ts;
+ val (bounds, tail) = chop_prefix is_Bound ts;
in
list_comb (Var (xi, fastype_of (betapplys (t, bounds))), map apply_Var_to_bounds tail)
end
--- a/src/HOL/Library/refute.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Library/refute.ML Sun Jan 28 19:28:52 2018 +0100
@@ -1943,7 +1943,7 @@
else ()
(* split the constructors into those occurring before/after *)
(* 'Const (s, T)' *)
- val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
+ val (constrs1, constrs2) = chop_prefix (fn (cname, ctypes) =>
not (cname = s andalso Sign.typ_instance thy (T,
map (typ_of_dtyp descr typ_assoc) ctypes
---> Type (s', Ts')))) constrs
@@ -2656,8 +2656,7 @@
(* go back up the stack until we find a level where we can go *)
(* to the next sibling node *)
let
- val offsets' = snd (take_prefix
- (fn off' => off' mod size_elem = size_elem - 1) offsets)
+ val offsets' = drop_prefix (fn off' => off' mod size_elem = size_elem - 1) offsets
in
case offsets' of
[] =>
--- a/src/HOL/Nominal/nominal_inductive2.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Jan 28 19:28:52 2018 +0100
@@ -330,7 +330,7 @@
rotate_tac 1 1,
REPEAT (eresolve_tac ctxt' [conjE] 1)])
[] ctxt;
- val (Ts1, _ :: Ts2) = take_prefix (not o equal T) (map snd sets);
+ val (Ts1, _ :: Ts2) = chop_prefix (not o equal T) (map snd sets);
val pTs = map NominalAtoms.mk_permT (Ts1 @ Ts2);
val (pis1, pis2) = chop (length Ts1)
(map Bound (length pTs - 1 downto 0));
--- a/src/HOL/Nominal/nominal_primrec.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun Jan 28 19:28:52 2018 +0100
@@ -50,8 +50,8 @@
else raise RecError "illegal head of function equation"
| _ => raise RecError "illegal head of function equation";
- val (ls', rest) = take_prefix is_Free args;
- val (middle, rs') = take_suffix is_Free rest;
+ val (ls', rest) = chop_prefix is_Free args;
+ val (middle, rs') = chop_suffix is_Free rest;
val rpos = length ls';
val (constr, cargs') = if null middle then raise RecError "constructor missing"
@@ -296,7 +296,7 @@
val rec_rewritess =
unflat (map (fn (_, (_, _, constrs)) => constrs) descr) rec_rewrites;
val fvars = rec_rewrites |> hd |> Thm.concl_of |> HOLogic.dest_Trueprop |>
- HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst;
+ HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var;
val (pvars, ctxtvars) = List.partition
(equal HOLogic.boolT o body_type o snd)
(subtract (op =)
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Sun Jan 28 19:28:52 2018 +0100
@@ -180,7 +180,7 @@
fun beginning n cs =
let
- val drop_blanks = #1 o take_suffix is_whitespace;
+ val drop_blanks = drop_suffix is_whitespace;
val all_cs = drop_blanks cs;
val dots = if length all_cs > n then " ..." else "";
in
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sun Jan 28 19:28:52 2018 +0100
@@ -33,7 +33,7 @@
fun err_unfinished () = error "An unfinished SPARK environment is still open."
-val strip_number = apply2 implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
+val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
val name_ord = prod_ord string_ord (option_ord int_ord) o
apply2 (strip_number ##> Int.fromString);
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Jan 28 19:28:52 2018 +0100
@@ -696,7 +696,7 @@
(case strip_comb t of
(Free (s, _), args as _ :: _) =>
if String.isPrefix spass_skolem_prefix s then
- insert (op =) (s, fst (take_prefix is_Var args))
+ insert (op =) (s, take_prefix is_Var args)
else
fold add_skolem_args args
| (u, args as _ :: _) => fold add_skolem_args (u :: args)
--- a/src/HOL/Tools/ATP/atp_util.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Sun Jan 28 19:28:52 2018 +0100
@@ -84,7 +84,7 @@
| strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum
and strip_spaces_in_list _ [] accum = accum
| strip_spaces_in_list true (#"%" :: cs) accum =
- strip_spaces_in_list true (cs |> take_prefix (not_equal #"\n") |> snd) accum
+ strip_spaces_in_list true (cs |> drop_prefix (not_equal #"\n")) accum
| strip_spaces_in_list true (#"/" :: #"*" :: cs) accum = strip_c_style_comment cs accum
| strip_spaces_in_list _ [c1] accum = accum |> not (is_spaceish c1) ? cons c1
| strip_spaces_in_list skip_comments (cs as [_, _]) accum =
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sun Jan 28 19:28:52 2018 +0100
@@ -296,8 +296,8 @@
handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn];
val (fun_name, args) = strip_comb lhs
|>> (fn x => if is_Free x then fst (dest_Free x) else ill_formed_equation_head ctxt [eqn]);
- val (left_args, rest) = take_prefix is_Free args;
- val (nonfrees, right_args) = take_suffix is_Free rest;
+ val (left_args, rest) = chop_prefix is_Free args;
+ val (nonfrees, right_args) = chop_suffix is_Free rest;
val num_nonfrees = length nonfrees;
val _ = num_nonfrees = 1 orelse
(if num_nonfrees = 0 then missing_pattern ctxt [eqn]
--- a/src/HOL/Tools/Function/induction_schema.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Sun Jan 28 19:28:52 2018 +0100
@@ -75,7 +75,7 @@
val _ $ Pxs = Logic.strip_assums_concl conc
val (P, _) = strip_comb Pxs
val (cases', conds) =
- take_prefix (Term.exists_subterm (curry op aconv P)) cases
+ chop_prefix (Term.exists_subterm (curry op aconv P)) cases
val concl' = fold_rev (curry Logic.mk_implies) conds conc
in
([mk_branch concl'], cases')
@@ -101,7 +101,7 @@
fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
val (gs, rcprs) =
- take_prefix (not o Term.exists_subterm is_pred) prems
+ chop_prefix (not o Term.exists_subterm is_pred) prems
in
SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*),
gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
--- a/src/HOL/Tools/Meson/meson.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Sun Jan 28 19:28:52 2018 +0100
@@ -730,7 +730,7 @@
(*This version does only one inference per call;
having only one eq_assume_tac speeds it up!*)
fun prolog_step_tac' ctxt horns =
- let val (horn0s, _) = (*0 subgoals vs 1 or more*)
+ let val horn0s = (*0 subgoals vs 1 or more*)
take_prefix Thm.no_prems horns
val nrtac = resolve_from_net_tac ctxt (Tactic.build_net horns)
in fn i => eq_assume_tac i ORELSE
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Sun Jan 28 19:28:52 2018 +0100
@@ -49,8 +49,8 @@
else primrec_error "illegal head of function equation"
| _ => primrec_error "illegal head of function equation");
- val (ls', rest) = take_prefix is_Free args;
- val (middle, rs') = take_suffix is_Free rest;
+ val (ls', rest) = chop_prefix is_Free args;
+ val (middle, rs') = chop_suffix is_Free rest;
val rpos = length ls';
val (constr, cargs') =
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sun Jan 28 19:28:52 2018 +0100
@@ -202,7 +202,7 @@
(Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
Quickcheck.message ctxt
"Quickcheck continues to find a genuine counterexample...";
- test true (snd (take_prefix (fn x => not (x = (card, size))) enum))
+ test true (drop_prefix (fn x => not (x = (card, size))) enum)
end
| NONE => ())
in (test genuine_only enumeration_card_size; !current_result) end)
--- a/src/HOL/Tools/SMT/smt_solver.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Sun Jan 28 19:28:52 2018 +0100
@@ -94,7 +94,7 @@
SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input
val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
- val output = fst (take_suffix (equal "") res)
+ val output = drop_suffix (equal "") res
val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
val _ = member (op =) normal_return_codes return_code orelse
--- a/src/HOL/Tools/SMT/smt_systems.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Sun Jan 28 19:28:52 2018 +0100
@@ -33,7 +33,7 @@
fun on_first_line test_outcome solver_name lines =
let
val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
- val (l, ls) = split_first (snd (take_prefix is_blank_or_error_line lines))
+ val (l, ls) = split_first (drop_prefix is_blank_or_error_line lines)
in (test_outcome solver_name l, ls) end
fun on_first_non_unsupported_line test_outcome solver_name lines =
--- a/src/HOL/Tools/SMT/smtlib.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/SMT/smtlib.ML Sun Jan 28 19:28:52 2018 +0100
@@ -40,7 +40,7 @@
(* utilities *)
fun read_raw pred l cs =
- (case take_prefix pred cs of
+ (case chop_prefix pred cs of
([], []) => raise PARSE (l, "empty token")
| ([], c :: _) => raise PARSE (l, "unexpected character " ^ quote c)
| x => x)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Sun Jan 28 19:28:52 2018 +0100
@@ -362,7 +362,7 @@
Math.pow (Real.fromInt remaining_max / Real.fromInt max_facts, max_imperfect_exp)))
val (perfect, imperfect) = candidates
|> sort (Real.compare o swap o apply2 snd)
- |> take_prefix (fn (_, w) => w > 0.99999)
+ |> chop_prefix (fn (_, w) => w > 0.99999)
val ((accepts, more_rejects), rejects) =
chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
in
--- a/src/HOL/Tools/sat_solver.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/sat_solver.ML Sun Jan 28 19:28:52 2018 +0100
@@ -307,7 +307,7 @@
| NONE => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number")
fun clauses xs =
let
- val (xs1, xs2) = take_prefix (fn i => i <> 0) xs
+ val (xs1, xs2) = chop_prefix (fn i => i <> 0) xs
in
case xs2 of
[] => [xs1]
--- a/src/Pure/General/antiquote.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/General/antiquote.ML Sun Jan 28 19:28:52 2018 +0100
@@ -49,7 +49,7 @@
fun add a (line, lines) = (a :: line, lines);
fun flush (line, lines) = ([], rev line :: lines);
fun split (a as Text ss) =
- (case take_prefix (fn ("\n", _) => false | _ => true) ss of
+ (case chop_prefix (fn ("\n", _) => false | _ => true) ss of
([], []) => I
| (_, []) => add a
| ([], _ :: rest) => flush #> split (Text rest)
--- a/src/Pure/General/path.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/General/path.ML Sun Jan 28 19:28:52 2018 +0100
@@ -150,7 +150,7 @@
handle ERROR msg => cat_error msg ("The error(s) above occurred in " ^ quote str);
val (roots, raw_elems) =
- (case take_prefix (equal "") (space_explode "/" str) |>> length of
+ (case chop_prefix (equal "") (space_explode "/" str) |>> length of
(0, es) => ([], es)
| (1, es) => ([Root ""], es)
| (_, []) => ([Root ""], [])
@@ -190,7 +190,7 @@
| ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
- (case take_suffix (fn c => c <> ".") (raw_explode s) of
+ (case chop_suffix (fn c => c <> ".") (raw_explode s) of
([], _) => (Path [Basic s], "")
| (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
--- a/src/Pure/General/pretty.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/General/pretty.ML Sun Jan 28 19:28:52 2018 +0100
@@ -128,7 +128,7 @@
val indent' = force_nat indent;
fun body_length prts len =
let
- val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
+ val (line, rest) = chop_prefix (fn Break (true, _, _) => false | _ => true) prts;
val len' = Int.max (fold (Integer.add o length) line 0, len);
in
(case rest of
--- a/src/Pure/General/symbol.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/General/symbol.ML Sun Jan 28 19:28:52 2018 +0100
@@ -199,7 +199,7 @@
fun beginning n cs =
let
- val drop_blanks = #1 o take_suffix is_ascii_blank;
+ val drop_blanks = drop_suffix is_ascii_blank;
val all_cs = drop_blanks cs;
val dots = if length all_cs > n then " ..." else "";
in
@@ -465,7 +465,7 @@
then chr (ord s + 1) :: ss
else "a" :: s :: ss;
- val (ss, qs) = apfst rev (take_suffix is_quasi (Symbol.explode str));
+ val (ss, qs) = apfst rev (chop_suffix is_quasi (Symbol.explode str));
val ss' = if symbolic_end ss then "'" :: ss else bump ss;
in implode (rev ss' @ qs) end;
--- a/src/Pure/Isar/code.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Isar/code.ML Sun Jan 28 19:28:52 2018 +0100
@@ -1380,7 +1380,7 @@
fun subsumptive_add thy verbose (thm, proper) eqns =
let
- val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
+ val args_of = drop_prefix is_Var o rev o snd o strip_comb
o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
val args = args_of thm;
val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
--- a/src/Pure/Isar/element.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Isar/element.ML Sun Jan 28 19:28:52 2018 +0100
@@ -233,7 +233,7 @@
val concl_term = Object_Logic.drop_judgment ctxt concl;
val (assumes, cases) =
- take_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
+ chop_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
val is_thesis = if null cases then K false else fn v => v aconv concl_term;
val fixes =
rev (fold_aterms (fn v as Free (x, T) =>
--- a/src/Pure/Isar/proof.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Isar/proof.ML Sun Jan 28 19:28:52 2018 +0100
@@ -975,7 +975,7 @@
fun implicit_vars props =
let
- val (var_props, _) = take_prefix is_var props;
+ val var_props = take_prefix is_var props;
val explicit_vars = fold Term.add_vars var_props [];
val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
in map (Logic.mk_term o Var) vars end;
--- a/src/Pure/Isar/proof_context.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Jan 28 19:28:52 2018 +0100
@@ -1536,7 +1536,7 @@
val print_name = Token.print_name (Thy_Header.get_keywords' ctxt);
fun trim_name x = if Name.is_internal x then Name.clean x else "_";
- val trim_names = map trim_name #> take_suffix (equal "_") #> #1;
+ val trim_names = map trim_name #> drop_suffix (equal "_");
fun print_case name xs =
(case trim_names xs of
--- a/src/Pure/PIDE/command.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/PIDE/command.ML Sun Jan 28 19:28:52 2018 +0100
@@ -131,7 +131,7 @@
let
val command_reports = Outer_Syntax.command_reports thy;
- val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
+ val proper_range = Token.range_of (drop_suffix Token.is_improper span);
val pos =
(case find_first Token.is_command span of
SOME tok => Token.pos_of tok
--- a/src/Pure/Proof/extraction.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Proof/extraction.ML Sun Jan 28 19:28:52 2018 +0100
@@ -70,7 +70,7 @@
| rlz_proc _ = NONE;
val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
- take_prefix (fn s => s <> ":") o raw_explode;
+ chop_prefix (fn s => s <> ":") o raw_explode;
type rules =
{next: int, rs: ((term * term) list * (term * term)) list,
--- a/src/Pure/Syntax/lexicon.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML Sun Jan 28 19:28:52 2018 +0100
@@ -406,7 +406,7 @@
let
val cs = Symbol.explode str;
val (intpart, fracpart) =
- (case take_prefix Symbol.is_digit cs of
+ (case chop_prefix Symbol.is_digit cs of
(intpart, "." :: fracpart) => (intpart, fracpart)
| _ => raise Fail "read_float");
in
--- a/src/Pure/Thy/markdown.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Thy/markdown.ML Sun Jan 28 19:28:52 2018 +0100
@@ -90,7 +90,7 @@
val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
fun strip_spaces (Antiquote.Text ss :: rest) =
- let val (sp, ss') = take_prefix is_space ss
+ let val (sp, ss') = chop_prefix is_space ss
in (length sp, if null ss' then rest else Antiquote.Text ss' :: rest) end
| strip_spaces source = (0, source);
@@ -149,7 +149,7 @@
fun list_items [] = []
| list_items (item :: rest) =
- let val (item_rest, rest') = take_prefix (not o is_item) rest;
+ let val (item_rest, rest') = chop_prefix (not o is_item) rest;
in (item :: item_rest) :: list_items rest' end;
--- a/src/Pure/Thy/thy_output.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Jan 28 19:28:52 2018 +0100
@@ -209,16 +209,16 @@
fun make_span cmd src =
let
- fun take_newline (tok :: toks) =
+ fun chop_newline (tok :: toks) =
if newline_token (fst tok) then ([tok], toks, true)
else ([], tok :: toks, false)
- | take_newline [] = ([], [], false);
+ | chop_newline [] = ([], [], false);
val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
src
- |> take_prefix (white_token o fst)
- ||>> take_suffix (white_token o fst)
- ||>> take_prefix (white_comment_token o fst)
- ||> take_newline;
+ |> chop_prefix (white_token o fst)
+ ||>> chop_suffix (white_token o fst)
+ ||>> chop_prefix (white_comment_token o fst)
+ ||> chop_newline;
in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
@@ -405,7 +405,7 @@
make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
val spans = toks
- |> take_suffix Token.is_space |> #1
+ |> drop_suffix Token.is_space
|> Source.of_list
|> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
|> Source.source stopper (Scan.error (Scan.bulk span))
--- a/src/Pure/library.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/library.ML Sun Jan 28 19:28:52 2018 +0100
@@ -99,9 +99,13 @@
val ~~ : 'a list * 'b list -> ('a * 'b) list
val split_list: ('a * 'b) list -> 'a list * 'b list
val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
+ val take_prefix: ('a -> bool) -> 'a list -> 'a list
+ val drop_prefix: ('a -> bool) -> 'a list -> 'a list
+ val chop_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
+ val take_suffix: ('a -> bool) -> 'a list -> 'a list
+ val drop_suffix: ('a -> bool) -> 'a list -> 'a list
+ val chop_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
- val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
- val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
val chop_common_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
val prefixes1: 'a list -> 'a list list
val prefixes: 'a list -> 'a list list
@@ -526,28 +530,53 @@
fun burrow_fst f xs = split_list xs |>> f |> op ~~;
+(* take, drop, chop, trim according to predicate *)
+
+fun take_prefix pred list =
+ let
+ fun take res (x :: xs) = if pred x then take (x :: res) xs else rev res
+ | take res [] = rev res;
+ in take [] list end;
+
+fun drop_prefix pred list =
+ let
+ fun drop (x :: xs) = if pred x then drop xs else x :: xs
+ | drop [] = [];
+ in drop list end;
+
+fun chop_prefix pred list =
+ let
+ val prfx = take_prefix pred list;
+ val sffx = drop (length prfx) list;
+ in (prfx, sffx) end;
+
+fun take_suffix pred list =
+ let
+ fun take res (x :: xs) = if pred x then take (x :: res) xs else res
+ | take res [] = res;
+ in take [] (rev list) end;
+
+fun drop_suffix pred list =
+ let
+ fun drop (x :: xs) = if pred x then drop xs else rev (x :: xs)
+ | drop [] = [];
+ in drop (rev list) end;
+
+fun chop_suffix pred list =
+ let
+ val prfx = drop_suffix pred list;
+ val sffx = drop (length prfx) list;
+ in (prfx, sffx) end;
+
+fun trim pred = drop_prefix pred #> drop_suffix pred;
+
+
(* prefixes, suffixes *)
fun is_prefix _ [] _ = true
| is_prefix eq (x :: xs) (y :: ys) = eq (x, y) andalso is_prefix eq xs ys
| is_prefix eq _ _ = false;
-(* [x1, ..., xi, ..., xn] ---> ([x1, ..., x(i-1)], [xi, ..., xn])
- where xi is the first element that does not satisfy the predicate*)
-fun take_prefix (pred : 'a -> bool) (xs: 'a list) : 'a list * 'a list =
- let fun take (rxs, []) = (rev rxs, [])
- | take (rxs, x :: xs) =
- if pred x then take(x :: rxs, xs) else (rev rxs, x :: xs)
- in take([], xs) end;
-
-(* [x1, ..., xi, ..., xn] ---> ([x1, ..., xi], [x(i+1), ..., xn])
- where xi is the last element that does not satisfy the predicate*)
-fun take_suffix _ [] = ([], [])
- | take_suffix pred (x :: xs) =
- (case take_suffix pred xs of
- ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
- | (prfx, sffx) => (x :: prfx, sffx));
-
fun chop_common_prefix eq ([], ys) = ([], ([], ys))
| chop_common_prefix eq (xs, []) = ([], (xs, []))
| chop_common_prefix eq (xs as x :: xs', ys as y :: ys') =
@@ -564,8 +593,6 @@
fun suffixes1 xs = map rev (prefixes1 (rev xs));
fun suffixes xs = [] :: suffixes1 xs;
-fun trim pred = take_prefix pred #> #2 #> take_suffix pred #> #1;
-
(** integers **)
--- a/src/Tools/case_product.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Tools/case_product.ML Sun Jan 28 19:28:52 2018 +0100
@@ -48,8 +48,8 @@
val concl = Thm.concl_of thm1
fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
- val (p_cons1, p_cases1) = take_prefix is_consumes (Thm.prems_of thm1)
- val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2)
+ val (p_cons1, p_cases1) = chop_prefix is_consumes (Thm.prems_of thm1)
+ val (p_cons2, p_cases2) = chop_prefix is_consumes (Thm.prems_of thm2)
val p_cases_prod = map (fn p1 => map (fn p2 =>
let
--- a/src/Tools/coherent.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Tools/coherent.ML Sun Jan 28 19:28:52 2018 +0100
@@ -54,8 +54,7 @@
let
val prems = Logic.strip_imp_prems prop;
val concl = Logic.strip_imp_concl prop;
- val (prems1, prems2) =
- take_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
+ val (prems1, prems2) = chop_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
in
(prems1,
if null prems2 then [([], [concl])]
--- a/src/ZF/Tools/primrec_package.ML Sun Jan 28 16:09:00 2018 +0100
+++ b/src/ZF/Tools/primrec_package.ML Sun Jan 28 19:28:52 2018 +0100
@@ -40,8 +40,8 @@
val (fname, ftype) = dest_Const recfun handle TERM _ =>
raise RecError "function is not declared as constant in theory";
- val (ls_frees, rest) = take_prefix is_Free args;
- val (middle, rs_frees) = take_suffix is_Free rest;
+ val (ls_frees, rest) = chop_prefix is_Free args;
+ val (middle, rs_frees) = chop_suffix is_Free rest;
val (constr, cargs_frees) =
if null middle then raise RecError "constructor missing"