fact: Fixpoint runATest (st : State) (f : nat -> RandomSeed -> QProp) (maxSteps : nat) := if maxSteps is maxSteps'.+1 then let size := (computeSize st) (numSuccessTests st) (numDiscardedTests st) in let (rnd1, rnd2) := randomSplit (randomSeed st) in let test (st : State) := if (gte (numSuccessTests st) (maxSuccessTests st)) then doneTesting st else if (gte (numDiscardedTests st) (maxDiscardedTests st)) then giveUp st else runATest st f maxSteps' in match st with | MkState mst mdt ms cs nst ndt ls e r nss nts ana => match f size rnd1 with | MkProp (MkRose res ts) => let res_cb := callbackPostTest st res in match res with | MkResult (Some x) e reas _ s _ t => if x then let ls' := match s with | nil => ls | _ => let s_to_add := ShowFunctions.string_concat (ShowFunctions.intersperse " , "%string s) in match Map.find s_to_add ls with | None => Map.add s_to_add (res_cb + 1) ls | Some k => Map.add s_to_add (k+1) ls end end in test (MkState mst mdt ms cs (nst + 1) ndt ls' e rnd2 nss nts ana) else let tag_text := match t with | Some s => "Tag: " ++ s ++ nl | _ => "" end in let pre : string := ( if ana then ( if expect res then """result"": ""failed"", " else """result"": ""expected_failure"" " ) else ( if expect res then "*** Failed " else "+++ Failed (as expected) " ) )%string in let (numShrinks, res') := localMin st (MkRose res ts) in let suf := ( if ana then ( """tests"": " ++ (show (S nst)) ++ ", ""shrinks"": " ++ (show numShrinks) ++ ", ""discards"": " ++ (show ndt) ) else ( "after " ++ (show (S nst)) ++ " tests and " ++ (show numShrinks) ++ " shrinks. (" ++ (show ndt) ++ " discards)" ) )%string in if (negb (expect res)) then Success (nst + 1) ndt (summary st) (tag_text ++ pre ++ suf) else Failure (nst + 1) numShrinks ndt r size (tag_text ++ pre ++ suf) (summary st) reas | MkResult None e reas _ s _ t => let ls' := match s with | nil => ls | _ => let s_to_add := "(Discarded) " ++ ShowFunctions.string_concat (ShowFunctions.intersperse " , "%string s) in match Map.find s_to_add ls with | None => Map.add s_to_add (res_cb + 1) ls | Some k => Map.add s_to_add (k+1) ls end end in test (MkState mst mdt ms cs nst ndt.+1 ls' e rnd2 nss nts ana) end end end else giveUp st.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrnat ssrbool eqtype div) ExtLib(Structures.Monad) SimpleIO(SimpleIO) QuickChick(RoseTrees RandomQC Generators Producer SemChecker) QuickChick(Show Checker State Classes) Coq.Strings.Ascii Coq.Strings.String List Recdef Arith.EqNat