# HG changeset patch # User haftmann # Date 1285864649 -7200 # Node ID dac3c3106746b85451f27f1fac110c7b563fe0b9 # Parent b5f978f97347cfd2ad867d56725ecca8b6db162f take_while, drop_while diff -r b5f978f97347 -r dac3c3106746 src/HOL/Tools/SMT/cvc3_solver.ML --- a/src/HOL/Tools/SMT/cvc3_solver.ML Thu Sep 30 09:45:18 2010 +0200 +++ b/src/HOL/Tools/SMT/cvc3_solver.ML Thu Sep 30 18:37:29 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 (dropwhile empty_line output) + val (l, _) = split_first (drop_while empty_line output) in if is_unsat l then @{cprop False} else if is_sat l then raise_cex true diff -r b5f978f97347 -r dac3c3106746 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Thu Sep 30 09:45:18 2010 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Thu Sep 30 18:37:29 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 (dropwhile (equal "") (rev res)) + val ls = rev (drop_while (equal "") (rev res)) val _ = trace_msg ctxt (pretty "SMT result:") ls in ls end diff -r b5f978f97347 -r dac3c3106746 src/HOL/Tools/SMT/yices_solver.ML --- a/src/HOL/Tools/SMT/yices_solver.ML Thu Sep 30 09:45:18 2010 +0200 +++ b/src/HOL/Tools/SMT/yices_solver.ML Thu Sep 30 18:37:29 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 (dropwhile empty_line output) + val (l, _) = split_first (drop_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 b5f978f97347 -r dac3c3106746 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Sep 30 09:45:18 2010 +0200 +++ b/src/HOL/Tools/refute.ML Thu Sep 30 18:37:29 2010 +0200 @@ -2772,7 +2772,7 @@ (* go back up the stack until we find a level where we can go *) (* to the next sibling node *) let - val offsets' = dropwhile + val offsets' = drop_while (fn off' => off' mod size_elem = size_elem - 1) offsets in case offsets' of diff -r b5f978f97347 -r dac3c3106746 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Sep 30 09:45:18 2010 +0200 +++ b/src/Pure/Isar/code.ML Thu Sep 30 18:37:29 2010 +0200 @@ -1049,7 +1049,7 @@ val c = const_eqn thy thm; fun update_subsume thy (thm, proper) eqns = let - val args_of = dropwhile is_Var o rev o snd o strip_comb + val args_of = drop_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 b5f978f97347 -r dac3c3106746 src/Pure/library.ML --- a/src/Pure/library.ML Thu Sep 30 09:45:18 2010 +0200 +++ b/src/Pure/library.ML Thu Sep 30 18:37:29 2010 +0200 @@ -83,7 +83,8 @@ val take: int -> 'a list -> 'a list val drop: int -> 'a list -> 'a list val chop: int -> 'a list -> 'a list * 'a list - val dropwhile: ('a -> bool) -> 'a list -> 'a list + val take_while: ('a -> bool) -> 'a list -> 'a list + val drop_while: ('a -> bool) -> '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 @@ -421,8 +422,11 @@ | chop _ [] = ([], []) | chop n (x :: xs) = chop (n - 1) xs |>> cons x; -fun dropwhile P [] = [] - | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys; +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 []; (*return nth element of a list, where 0 designates the first element; raise Subscript if list too short*)