module Delay where

import qualified Prelude

__ = Prelude.error "Logical or arity value used"

data Bool = True
            | False

data Nat = O
           | S Nat

data Prod a b = Pair b a

plus n m =
  case n of
    O -> m
    S p -> S (plus p m)

mult n m =
  case n of
    O -> O
    S p -> plus m (mult p m)

data Delay a = Now a
               | Later (Delay a)

never _ =
  Later (never __)

returnD a =
  Now a

lfpAux k f a =
  case f k a of
    Now a0 -> Now a0
    Later d' -> Later (lfpAux (f k) f a)

lfp f a =
  lfpAux (\x -> never __) f a

fact x =
  lfp (\factfn arg ->
    case arg of
      O -> returnD (S O)
      S k ->
        (case factfn k of
           Now a -> returnD (mult a (S k))
           Later d -> d)) x

pred x =
  lfp (\predfn arg -> case arg of
                        O -> never __
                        S n -> returnD n) x

pminus m n =
  lfp (\pminusfn arg ->
    case arg of
      Pair min nin ->
        (case nin of
           O -> returnD min
           S nk ->
             (case min of
                O -> never __
                S mk -> pminusfn (Pair mk nk)))) (Pair m n)

data SK = S_comb
          | K_comb
          | App SK SK

sK_rect f f0 f1 s =
  case s of
    S_comb -> f
    K_comb -> f0
    App s0 s1 -> f1 s0 (sK_rect f f0 f1 s0) s1 (sK_rect f f0 f1 s1)

sK_rec f f0 f1 s =
  sK_rect f f0 f1 s

eqSK a x =
  sK_rec (\b ->
    case b of
      S_comb -> True
      K_comb -> False
      App s s0 -> False) (\b ->
    case b of
      S_comb -> False
      K_comb -> True
      App s s0 -> False) (\a1 iHa1 a2 iHa2 b ->
    case b of
      S_comb -> False
      K_comb -> False
      App fn arg -> (case iHa1 fn of
                       True -> iHa2 arg
                       False -> False)) a x

eqSK2 a b a' b' =
  case eqSK a a' of
    True -> eqSK b b'
    False -> False

evalSK h =
  lfp (\eval arg ->
    case arg of
      S_comb -> returnD S_comb
      K_comb -> returnD K_comb
      App x y ->
        (case x of
           S_comb ->
             (case eval x of
                Now x' ->
                  (case eval y of
                     Now y' ->
                       (case eqSK2 x y x' y' of
                          True -> returnD (App x' y')
                          False -> eval (App x' y'))
                     Later d -> never __)
                Later d -> never __)
           K_comb ->
             (case eval x of
                Now x' ->
                  (case eval y of
                     Now y' ->
                       (case eqSK2 x y x' y' of
                          True -> returnD (App x' y')
                          False -> eval (App x' y'))
                     Later d -> never __)
                Later d -> never __)
           App s g ->
             (case s of
                S_comb ->
                  (case eval x of
                     Now x' ->
                       (case eval y of
                          Now y' ->
                            (case eqSK2 x y x' y' of
                               True -> returnD (App x' y')
                               False -> eval (App x' y'))
                          Later d -> never __)
                     Later d -> never __)
                K_comb -> eval g
                App s0 f ->
                  (case s0 of
                     S_comb -> eval (App (App f y) (App g y))
                     K_comb ->
                       (case eval x of
                          Now x' ->
                            (case eval y of
                               Now y' ->
                                 (case eqSK2 x y x' y' of
                                    True -> returnD (App x' y')
                                    False -> eval (App x' y'))
                               Later d -> never __)
                          Later d -> never __)
                     App s1 s2 ->
                       (case eval x of
                          Now x' ->
                            (case eval y of
                               Now y' ->
                                 (case eqSK2 x y x' y' of
                                    True -> returnD (App x' y')
                                    False -> eval (App x' y'))
                               Later d -> never __)
                          Later d -> never __))))) h