made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
authorblanchet
Fri Dec 18 14:02:58 2009 +0100 (2009-12-18)
changeset 341288650a073dd9b
parent 34127 85257fa296f6
child 34132 7492eca87ab4
made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
up to now, only Auto Quickcheck did -- the old behavior is available by passing "no_assms" as option
src/Tools/quickcheck.ML
     1.1 --- a/src/Tools/quickcheck.ML	Fri Dec 18 12:00:44 2009 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Dec 18 14:02:58 2009 +0100
     1.3 @@ -32,24 +32,27 @@
     1.4  (* quickcheck configuration -- default parameters, test generators *)
     1.5  
     1.6  datatype test_params = Test_Params of
     1.7 -  { size: int, iterations: int, default_type: typ option };
     1.8 +  { size: int, iterations: int, default_type: typ option, no_assms: bool };
     1.9  
    1.10 -fun dest_test_params (Test_Params { size, iterations, default_type }) =
    1.11 -  ((size, iterations), default_type);
    1.12 -fun make_test_params ((size, iterations), default_type) =
    1.13 -  Test_Params { size = size, iterations = iterations, default_type = default_type };
    1.14 -fun map_test_params f (Test_Params { size, iterations, default_type}) =
    1.15 -  make_test_params (f ((size, iterations), default_type));
    1.16 -fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 },
    1.17 -  Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) =
    1.18 +fun dest_test_params (Test_Params { size, iterations, default_type, no_assms }) =
    1.19 +  ((size, iterations), (default_type, no_assms));
    1.20 +fun make_test_params ((size, iterations), (default_type, no_assms)) =
    1.21 +  Test_Params { size = size, iterations = iterations, default_type = default_type,
    1.22 +                no_assms = no_assms };
    1.23 +fun map_test_params f (Test_Params { size, iterations, default_type, no_assms }) =
    1.24 +  make_test_params (f ((size, iterations), (default_type, no_assms)));
    1.25 +fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
    1.26 +                                     no_assms = no_assms1 },
    1.27 +  Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
    1.28 +                no_assms = no_assms2 }) =
    1.29    make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    1.30 -    case default_type1 of NONE => default_type2 | _ => default_type1);
    1.31 +    (case default_type1 of NONE => default_type2 | _ => default_type1, no_assms1 orelse no_assms2));
    1.32  
    1.33  structure Data = Theory_Data
    1.34  (
    1.35    type T = (string * (Proof.context -> term -> int -> term list option)) list
    1.36      * test_params;
    1.37 -  val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE });
    1.38 +  val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE, no_assms = false });
    1.39    val extend = I;
    1.40    fun merge ((generators1, params1), (generators2, params2)) : T =
    1.41      (AList.merge (op =) (K true) (generators1, generators2),
    1.42 @@ -130,7 +133,7 @@
    1.43        | subst T = T;
    1.44    in (map_types o map_atyps) subst end;
    1.45  
    1.46 -fun test_goal quiet generator_name size iterations default_T insts i assms state =
    1.47 +fun test_goal quiet generator_name size iterations default_T no_assms insts i assms state =
    1.48    let
    1.49      val ctxt = Proof.context_of state;
    1.50      val thy = Proof.theory_of state;
    1.51 @@ -138,7 +141,8 @@
    1.52        | strip t = t;
    1.53      val {goal = st, ...} = Proof.raw_goal state;
    1.54      val (gi, frees) = Logic.goal_params (prop_of st) i;
    1.55 -    val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
    1.56 +    val gi' = Logic.list_implies (if no_assms then [] else assms,
    1.57 +                                  subst_bounds (frees, strip gi))
    1.58        |> monomorphic_term thy insts default_T
    1.59        |> ObjectLogic.atomize_term thy;
    1.60    in test_term ctxt quiet generator_name size iterations gi' end;
    1.61 @@ -159,10 +163,10 @@
    1.62      let
    1.63        val ctxt = Proof.context_of state;
    1.64        val assms = map term_of (Assumption.all_assms_of ctxt);
    1.65 -      val Test_Params { size, iterations, default_type } =
    1.66 +      val Test_Params { size, iterations, default_type, no_assms } =
    1.67          (snd o Data.get o Proof.theory_of) state;
    1.68        val res =
    1.69 -        try (test_goal true NONE size iterations default_type [] 1 assms) state;
    1.70 +        try (test_goal true NONE size iterations default_type no_assms [] 1 assms) state;
    1.71      in
    1.72        case res of
    1.73          NONE => (false, state)
    1.74 @@ -180,15 +184,20 @@
    1.75   of (k, []) => if k >= 0 then k
    1.76        else error ("Not a natural number: " ^ s)
    1.77    | (_, _ :: _) => error ("Not a natural number: " ^ s);
    1.78 +fun read_bool "false" = false
    1.79 +  | read_bool "true" = true
    1.80 +  | read_bool s = error ("Not a Boolean value: " ^ s)
    1.81  
    1.82  fun parse_test_param ctxt ("size", arg) =
    1.83        (apfst o apfst o K) (read_nat arg)
    1.84    | parse_test_param ctxt ("iterations", arg) =
    1.85        (apfst o apsnd o K) (read_nat arg)
    1.86    | parse_test_param ctxt ("default_type", arg) =
    1.87 -      (apsnd o K o SOME) (ProofContext.read_typ ctxt arg)
    1.88 +      (apsnd o apfst o K o SOME) (ProofContext.read_typ ctxt arg)
    1.89 +  | parse_test_param ctxt ("no_assms", arg) =
    1.90 +      (apsnd o apsnd o K) (read_bool arg)
    1.91    | parse_test_param ctxt (name, _) =
    1.92 -      error ("Bad test parameter: " ^ name);
    1.93 +      error ("Unknown test parameter: " ^ name);
    1.94  
    1.95  fun parse_test_param_inst ctxt ("generator", arg) =
    1.96        (apsnd o apfst o K o SOME) arg
    1.97 @@ -211,12 +220,13 @@
    1.98    let
    1.99      val thy = Proof.theory_of state;
   1.100      val ctxt = Proof.context_of state;
   1.101 +    val assms = map term_of (Assumption.all_assms_of ctxt);
   1.102      val default_params = (dest_test_params o snd o Data.get) thy;
   1.103      val f = fold (parse_test_param_inst ctxt) args;
   1.104 -    val (((size, iterations), default_type), (generator_name, insts)) =
   1.105 +    val (((size, iterations), (default_type, no_assms)), (generator_name, insts)) =
   1.106        f (default_params, (NONE, []));
   1.107    in
   1.108 -    test_goal false generator_name size iterations default_type insts i [] state
   1.109 +    test_goal false generator_name size iterations default_type no_assms insts i assms state
   1.110    end;
   1.111  
   1.112  fun quickcheck_cmd args i state =
   1.113 @@ -225,7 +235,8 @@
   1.114  
   1.115  local structure P = OuterParse and K = OuterKeyword in
   1.116  
   1.117 -val parse_arg = P.name --| P.$$$ "=" -- P.name;
   1.118 +val parse_arg = P.name -- (Scan.optional (P.$$$ "=" |-- P.name) "true")
   1.119 +
   1.120  val parse_args = P.$$$ "[" |-- P.list1 parse_arg --| P.$$$ "]"
   1.121    || Scan.succeed [];
   1.122