CoInductive Delay (A:Set) : Set :=
   Now : forall a:A, Delay A
 | Later : forall (d:Delay A), Delay A.

CoFixpoint never (A:Set) : Delay A :=
  Later _ (never A).

Definition returnD (A:Set)(a:A) := Now A a.

CoFixpoint bindD (A:Set)(B:Set)(d:Delay A)(k:forall a:A, Delay B)  : Delay B :=
  match d with 
  | Now a => k a
  | Later d => Later _ (bindD A B d k)
  end.

CoFixpoint race (A:Set)(x:Delay A) (y:Delay A) : Delay A :=
  match x, y with
  | Now a, _ => Now _ a
  | Later _, Now a => Now _ a
  | Later d, Later d' => Later _ (race _ d d')
  end.

CoFixpoint lfpAux (A:Set)(B:Set)(k:A -> Delay B)
  (f:(A -> Delay B) -> A -> Delay B) (a:A) : Delay B :=
  match f k a with
   | Now a => Now _ a
   | Later d' => (Later _ (lfpAux _ _ (f k) f a))
  end.

Definition lfp :=
 fun (A:Set)(B:Set)(f:((A -> Delay B) -> (A -> Delay B)))(a:A) =>
   (lfpAux _ _ (fun x:A => never B) f a).

Require Arith.

Definition fact : forall (x:nat), Delay nat.
intros.
refine (lfp nat nat 
  (fun factfn:nat -> Delay nat =>
    (fun arg:nat => _)) x).
case arg.
apply returnD.
apply 1.
intro k.
case (factfn k).
intros.
apply returnD.
apply (mult a (S k)).
auto.
Defined.

Definition pred : forall (x:nat), Delay nat.
intros.
refine (lfp nat nat
  (fun predfn:nat -> Delay nat =>
    (fun arg:nat => _)) x).
case arg.
apply never.
intros.
apply returnD.
apply n.
Defined.

Definition pminus : forall (m:nat)(n:nat), Delay nat.
intros m n. 
refine (lfp _ _ 
   (fun pminusfn : (nat * nat) -> Delay nat =>
     (fun arg : (nat * nat) => _)) (m,n)).
case arg.
intros min nin.
case nin.
apply returnD.
apply min.
intros nk.
case min.
apply never.
intros mk.
apply (pminusfn (mk,nk)).
Defined.

Inductive SK : Set :=
    S_comb : SK
  | K_comb : SK
  | app : SK -> SK -> SK.

Definition eqSK : SK -> SK -> bool.
intros a.
induction a.
intros b.
case b.
apply true.
apply false.
intros.
apply false.
intros b.
case b.
apply false.
apply true.
intros.
apply false.
intros b.
case b.
apply false.
apply false.
intros fn arg.
case (IHa1 fn).
apply (IHa2 arg).
apply false.
Defined.

Definition eqSK2 : SK -> SK -> SK -> SK -> bool.
intros a b a' b'.
case (eqSK a a').
apply (eqSK b b').
apply false.
Defined.

Definition evalSK : SK -> Delay SK.
intros.
refine (lfp _ _
   (fun eval : SK -> Delay SK =>
      (fun arg : SK => _)) H).
refine (match arg with
         | S_comb => returnD _ S_comb
         | K_comb => returnD _ K_comb
         | (app (app K_comb x) y) => eval x
	 | (app (app (app S_comb f) g) x) => 
	      eval (app (app f x) (app g x))
	 | (app x y) => match (eval x, eval y) with
              | (Now x', Now y') => if (eqSK2 x y x' y') 
		                      then returnD _ (app x' y')
	                              else eval (app x' y')
	      | (xfail, yfail) => never _
            end
	end).
Defined.

Extraction Language Haskell.
Recursive Extraction fact pred pminus evalSK.