(* Line added for Coq 8.9.0, see refman Section 7.7 *)
From Coq Require Extraction.

Require Import Coq.Strings.String.
Require Import QuickChick.Show.

Record It {A : Type} : Type := mkIt {
 st_t : Type;
 start : st_t;
 next : st_t -> option A * st_t;
 hasnext : st_t -> bool
}.

Inductive answerSC {A : Type} :=
  ErrorSC : answerSC
| SuccessSC : answerSC
| FailSC : A -> answerSC.

Local Open Scope string.

Instance showAnswerSC {A : Type} `{_ : Show A} : Show answerSC  :=
{|
  show t := match t with
    | ErrorSC => "Error" 
    | SuccessSC => "Success"
    | FailSC x => "Failure: " ++ show x
  end
|}.

Fixpoint iter {A : Type} It (pf : A -> bool) st n :=
match n with
  0 => ErrorSC
| S k => if (hasnext It) st 
         then 
         match (next It) st with
         (r, st') =>
	 (match r with 
         Some v =>  if pf v 
             then iter It pf st' k
             else FailSC v
	 | None => ErrorSC
          end) 
	 end
         else SuccessSC
end. 

Parameter fuel_iter : nat.

Definition smallCheck  {A : Type} It (pf : A -> bool) := iter It pf (start It) fuel_iter.

Extract Inlined Constant fuel_iter => "40000000".

Definition answerSC2bool {A : Type} (a : @answerSC A) := match a with
  SuccessSC  => true
 | _ => false
end.

Definition smallCheckb {A : Type} It (pf : A -> bool) := answerSC2bool (smallCheck It pf).


