# HG changeset patch # User haftmann # Date 1285921536 -7200 # Node ID 0659e84bdc5f26a208c59d09f0852dcc99ead0fe # Parent 5c9fe600525e1d9cda7e08a4b94dc5954fb0bd12 chop_while replace drop_while and take_while diff -r 5c9fe600525e -r 0659e84bdc5f src/HOL/Tools/SMT/cvc3_solver.ML --- a/src/HOL/Tools/SMT/cvc3_solver.ML Fri Oct 01 08:25:23 2010 +0200 +++ b/src/HOL/Tools/SMT/cvc3_solver.ML Fri Oct 01 10:25:36 2010 +0200 @@ -27,7 +27,7 @@ let val empty_line = (fn "" => true | _ => false) val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) - val (l, _) = split_first (drop_while empty_line output) + val (l, _) = split_first (snd (chop_while empty_line output)) in if is_unsat l then @{cprop False} else if is_sat l then raise_cex true diff -r 5c9fe600525e -r 0659e84bdc5f src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Fri Oct 01 08:25:23 2010 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Oct 01 10:25:36 2010 +0200 @@ -160,7 +160,7 @@ val (res, err) = with_timeout ctxt (run ctxt cmd args) input val _ = trace_msg ctxt (pretty "SMT solver:") err - val ls = rev (drop_while (equal "") (rev res)) + val ls = rev (snd (chop_while (equal "") (rev res))) val _ = trace_msg ctxt (pretty "SMT result:") ls in ls end diff -r 5c9fe600525e -r 0659e84bdc5f src/HOL/Tools/SMT/yices_solver.ML --- a/src/HOL/Tools/SMT/yices_solver.ML Fri Oct 01 08:25:23 2010 +0200 +++ b/src/HOL/Tools/SMT/yices_solver.ML Fri Oct 01 10:25:36 2010 +0200 @@ -23,7 +23,7 @@ let val empty_line = (fn "" => true | _ => false) val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) - val (l, _) = split_first (drop_while empty_line output) + val (l, _) = split_first (snd (chop_while empty_line output)) in if String.isPrefix "unsat" l then @{cprop False} else if String.isPrefix "sat" l then raise_cex true diff -r 5c9fe600525e -r 0659e84bdc5f src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Fri Oct 01 08:25:23 2010 +0200 +++ b/src/HOL/Tools/refute.ML Fri Oct 01 10:25:36 2010 +0200 @@ -2772,8 +2772,8 @@ (* go back up the stack until we find a level where we can go *) (* to the next sibling node *) let - val offsets' = drop_while - (fn off' => off' mod size_elem = size_elem - 1) offsets + val offsets' = snd (chop_while + (fn off' => off' mod size_elem = size_elem - 1) offsets) in case offsets' of [] => diff -r 5c9fe600525e -r 0659e84bdc5f src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Oct 01 08:25:23 2010 +0200 +++ b/src/Pure/Isar/code.ML Fri Oct 01 10:25:36 2010 +0200 @@ -1049,7 +1049,7 @@ val c = const_eqn thy thm; fun update_subsume thy (thm, proper) eqns = let - val args_of = drop_while is_Var o rev o snd o strip_comb + val args_of = snd o chop_while is_Var o rev o snd o strip_comb o 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); diff -r 5c9fe600525e -r 0659e84bdc5f src/Pure/library.ML --- a/src/Pure/library.ML Fri Oct 01 08:25:23 2010 +0200 +++ b/src/Pure/library.ML Fri Oct 01 10:25:36 2010 +0200 @@ -83,8 +83,7 @@ val take: int -> 'a list -> 'a list val drop: int -> 'a list -> 'a list val chop: int -> 'a list -> 'a list * 'a list - val take_while: ('a -> bool) -> 'a list -> 'a list - val drop_while: ('a -> bool) -> 'a list -> 'a list + val chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list val nth: 'a list -> int -> 'a val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list val nth_drop: int -> 'a list -> 'a list @@ -422,11 +421,9 @@ | chop _ [] = ([], []) | chop n (x :: xs) = chop (n - 1) xs |>> cons x; -fun drop_while P [] = [] - | drop_while P (ys as x :: xs) = if P x then drop_while P xs else ys; - -fun take_while P [] = [] - | take_while P (x :: xs) = if P x then x :: take_while P xs else []; +fun chop_while P [] = ([], []) + | chop_while P (ys as x :: xs) = + if P x then chop_while P xs |>> cons x else ([], ys); (*return nth element of a list, where 0 designates the first element; raise Subscript if list too short*)