src/Pure/codegen.ML
changeset 24565 08578e380a41
parent 24508 c8b82fec6447
child 24585 c359896d0f48
     1.1 --- a/src/Pure/codegen.ML	Sat Sep 08 20:37:22 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Mon Sep 10 16:09:01 2007 +0200
     1.3 @@ -957,39 +957,43 @@
     1.4            NONE => test (k+1) | SOME x => SOME x);
     1.5    in test 0 end;
     1.6  
     1.7 -fun test_goal out quiet ({size, iterations, default_type}, tvinsts) i assms state =
     1.8 +fun test_goal quiet ({size, iterations, default_type}, tvinsts) i assms state =
     1.9    let
    1.10      val thy = Proof.theory_of state;
    1.11      fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
    1.12        | strip t = t;
    1.13 -    val (gi, frees) = Logic.goal_params
    1.14 -      (prop_of (snd (snd (Proof.get_goal state)))) i;
    1.15 +    val (_, (_, st)) = Proof.get_goal state;
    1.16 +    val (gi, frees) = Logic.goal_params (prop_of st) i;
    1.17      val gi' = ObjectLogic.atomize_term thy (map_types
    1.18        (map_type_tfree (fn p as (s, _) =>
    1.19          the_default (the_default (TFree p) default_type)
    1.20            (AList.lookup (op =) tvinsts s)))
    1.21        (Logic.list_implies (assms, subst_bounds (frees, strip gi))));
    1.22 -  in case test_term thy quiet size iterations gi' of
    1.23 -      NONE => writeln "No counterexamples found."
    1.24 -    | SOME cex => out ("Counterexample found:\n" ^
    1.25 -        Pretty.string_of (Pretty.chunks (map (fn (s, t) =>
    1.26 +  in test_term thy quiet size iterations gi' end;
    1.27 +
    1.28 +fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
    1.29 +  | pretty_counterex ctxt (SOME cex) =
    1.30 +      Pretty.chunks (Pretty.str "Counterexample found:\n" ::
    1.31 +        map (fn (s, t) =>
    1.32            Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
    1.33 -            Sign.pretty_term thy t]) cex)))
    1.34 -  end;
    1.35 -
    1.36 -exception Counterex of string;
    1.37 +            ProofContext.pretty_term ctxt t]) cex);
    1.38  
    1.39  val auto_quickcheck = ref true;
    1.40  
    1.41  fun test_goal' int state =
    1.42 -  let val assms = map term_of (Assumption.assms_of (Proof.context_of state))
    1.43 +  let
    1.44 +    val ctxt = Proof.context_of state;
    1.45 +    val assms = map term_of (Assumption.assms_of ctxt)
    1.46    in
    1.47 -    (if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
    1.48 -     then
    1.49 -       (test_goal (fn s => raise Counterex s) true
    1.50 -          (get_test_params (Proof.theory_of state), []) 1 assms state
    1.51 -        handle ERROR _ => () | Counterex s => error s)
    1.52 -     else (); state)
    1.53 +    if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
    1.54 +    then
    1.55 +      (case try (test_goal true
    1.56 +           (get_test_params (Proof.theory_of state), []) 1 assms) state of
    1.57 +         SOME (cex as SOME _) =>
    1.58 +           Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
    1.59 +             Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
    1.60 +       | _ => state)
    1.61 +    else state
    1.62    end;
    1.63  
    1.64  val _ = Context.add_setup
    1.65 @@ -1170,9 +1174,11 @@
    1.66    (Scan.option (P.$$$ "[" |-- P.list1
    1.67      (   parse_test_params >> (fn f => fn thy => apfst (f thy))
    1.68       || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
    1.69 -    (fn (ps, g) => Toplevel.keep (fn st => test_goal writeln false
    1.70 -      (Library.apply (the_default [] (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
    1.71 -        (get_test_params (Toplevel.theory_of st), [])) g [] (Toplevel.proof_of st))));
    1.72 +    (fn (ps, g) => Toplevel.keep (fn st => Toplevel.proof_of st |>
    1.73 +      test_goal false (Library.apply (the_default []
    1.74 +          (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
    1.75 +        (get_test_params (Toplevel.theory_of st), [])) g [] |>
    1.76 +      pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
    1.77  
    1.78  val valueP =
    1.79    OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag