# HG changeset patch # User berghofe # Date 1189433341 -7200 # Node ID 08578e380a41e238d8aba83722bfa158821b7854 # Parent 260a65fa2900735a10913767a96d021b42646e4f Auto quickcheck now displays counterexample using Proof.goal_message rather than producing an error message. diff -r 260a65fa2900 -r 08578e380a41 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sat Sep 08 20:37:22 2007 +0200 +++ b/src/Pure/codegen.ML Mon Sep 10 16:09:01 2007 +0200 @@ -957,39 +957,43 @@ NONE => test (k+1) | SOME x => SOME x); in test 0 end; -fun test_goal out quiet ({size, iterations, default_type}, tvinsts) i assms state = +fun test_goal quiet ({size, iterations, default_type}, tvinsts) i assms state = let val thy = Proof.theory_of state; fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t | strip t = t; - val (gi, frees) = Logic.goal_params - (prop_of (snd (snd (Proof.get_goal state)))) i; + val (_, (_, st)) = Proof.get_goal state; + val (gi, frees) = Logic.goal_params (prop_of st) i; val gi' = ObjectLogic.atomize_term thy (map_types (map_type_tfree (fn p as (s, _) => the_default (the_default (TFree p) default_type) (AList.lookup (op =) tvinsts s))) (Logic.list_implies (assms, subst_bounds (frees, strip gi)))); - in case test_term thy quiet size iterations gi' of - NONE => writeln "No counterexamples found." - | SOME cex => out ("Counterexample found:\n" ^ - Pretty.string_of (Pretty.chunks (map (fn (s, t) => + in test_term thy quiet size iterations gi' end; + +fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found." + | pretty_counterex ctxt (SOME cex) = + Pretty.chunks (Pretty.str "Counterexample found:\n" :: + map (fn (s, t) => Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, - Sign.pretty_term thy t]) cex))) - end; - -exception Counterex of string; + ProofContext.pretty_term ctxt t]) cex); val auto_quickcheck = ref true; fun test_goal' int state = - let val assms = map term_of (Assumption.assms_of (Proof.context_of state)) + let + val ctxt = Proof.context_of state; + val assms = map term_of (Assumption.assms_of ctxt) in - (if int andalso !auto_quickcheck andalso not (!Toplevel.quiet) - then - (test_goal (fn s => raise Counterex s) true - (get_test_params (Proof.theory_of state), []) 1 assms state - handle ERROR _ => () | Counterex s => error s) - else (); state) + if int andalso !auto_quickcheck andalso not (!Toplevel.quiet) + then + (case try (test_goal true + (get_test_params (Proof.theory_of state), []) 1 assms) state of + SOME (cex as SOME _) => + Proof.goal_message (fn () => Pretty.chunks [Pretty.str "", + Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state + | _ => state) + else state end; val _ = Context.add_setup @@ -1170,9 +1174,11 @@ (Scan.option (P.$$$ "[" |-- P.list1 ( parse_test_params >> (fn f => fn thy => apfst (f thy)) || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >> - (fn (ps, g) => Toplevel.keep (fn st => test_goal writeln false - (Library.apply (the_default [] (Option.map (map (fn f => f (Toplevel.theory_of st))) ps)) - (get_test_params (Toplevel.theory_of st), [])) g [] (Toplevel.proof_of st)))); + (fn (ps, g) => Toplevel.keep (fn st => Toplevel.proof_of st |> + test_goal false (Library.apply (the_default [] + (Option.map (map (fn f => f (Toplevel.theory_of st))) ps)) + (get_test_params (Toplevel.theory_of st), [])) g [] |> + pretty_counterex (Toplevel.context_of st) |> Pretty.writeln))); val valueP = OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag