module LambdaChurch where

import Data.Char (isLetter)
import Data.List ( nub )

class ShowNice a where
    showNice :: a -> String

class ReadNice a where
    readNice :: String -> (a, String)

data Variable
  = Variable
  { name :: String
  , count :: Int
  }
  deriving (Show, Eq, Ord)

var :: String -> Variable
var x = Variable x 0

instance ShowNice Variable where
    showNice (Variable x 0) = x
    showNice (Variable x cnt) = x <> "_" <> show cnt

instance ReadNice Variable where
    readNice s
      | null x = error $ "expected variable but found " <> s
      | otherwise = (var x, s')
      where
        (x, s') = span isLetter s

freshVariable :: Variable -> [Variable] -> Variable
freshVariable var vars = Variable x (cnt + 1)
  where
    x = name var
    varsWithName = filter ((== x) . name) vars
    Variable _ cnt = maximum (var : varsWithName)


data Term
  = V Variable
  | App Term Term
  | Lam Variable Term
  deriving (Show)

-- alpha-equivalence
aEq :: Term -> Term -> Bool
aEq (V x) (V x') = x == x'
aEq (App t1 t2) (App t1' t2') = aEq t1 t1' && aEq t2 t2'
aEq (Lam x t) (Lam x' t')
  | x == x'   = aEq t t'
  | otherwise = aEq (subst (V y) x t) (subst (V y) x' t')
  where
    fvT = freeVars t
    fvT' = freeVars t'
    allFV = nub ([x, x'] ++ fvT ++ fvT')
    y = freshVariable x allFV
aEq _ _ = False

v :: String -> Term
v x = V (var x)

lam :: String -> Term -> Term
lam x = Lam (var x)

lams :: [String] -> Term -> Term
lams xs t = foldr lam t xs

($$) :: Term -> Term -> Term
($$) = App
infixl 9 $$

instance ShowNice Term where
    showNice (V var) = showNice var
    showNice (App t1 t2) = "(" <> showNice t1 <> " " <> showNice t2 <> ")"
    showNice (Lam var t) = "(" <> "\\" <> showNice var <> "." <> showNice t <> ")"

instance ReadNice Term where
    readNice [] = error "Nothing to read"
    readNice ('(' : '\\' : s) = (Lam var t, s'')
      where
        (var, '.' : s') = readNice s
        (t, ')' : s'') = readNice s'
    readNice ('(' : s) = (App t1 t2, s'')
      where
        (t1, ' ' : s') = readNice s
        (t2, ')' : s'') = readNice s'
    readNice s = (V var, s')
      where
        (var, s') = readNice s

freeVars :: Term -> [Variable]
freeVars (V var) = [var]
freeVars (App t1 t2) = nub $ freeVars t1 ++ freeVars t2
freeVars (Lam var t) = filter (/= var) (freeVars t)


-- subst u x t defines [u/x]t, i.e.,  substituting u for x in t
  for example [ 3 / x](x + x ) = = 3 + 3
-- This substitution avoids variable captures so it is safe to be used when 
-- reducing terms with free variables (e.g., if evaluating inside lambda abstractions)
subst
    :: Term     -- ^ substitution term
    -> Variable -- ^ variable to be substitutes
    -> Term     -- ^ term in which the substitution occurs
    -> Term
subst u x (V y)
  | x == y    = u
  | otherwise = V y
subst u x (App t1 t2) = App (subst u x t1) (subst u x t2)
subst u x (Lam y t)
  | x == y          = Lam y t
  | y `notElem` fvU = Lam y (subst u x t)
  | x `notElem` fvT = Lam y t
  | otherwise       = Lam y' (subst u x (subst (V y') y t))
  where
    fvT = freeVars t
    fvU = freeVars u
    allFV = nub ([x] ++ fvU ++ fvT)
    y' = freshVariable y allFV

-- Normal order reduction
-- - like call by name
-- - but also reduce under lambda abstractions if no application is possible
-- - guarantees reaching a normal form if it exists
normalReduceStep :: Term -> Maybe Term
normalReduceStep (App (Lam v t) t2) = Just $ subst t2 v t
normalReduceStep (App t1 t2)
  | Just t1' <- normalReduceStep t1 = Just $ App t1' t2
  | Just t2' <- normalReduceStep t2 = Just $ App t1 t2'
normalReduceStep (Lam x t)
  | Just t' <- normalReduceStep t = Just $ Lam x t'
normalReduceStep _ = Nothing

normalReduce :: Term -> Term
normalReduce t
  | Just t' <- normalReduceStep t = normalReduce t'
  | otherwise = t

reduce :: Term -> Term
reduce = normalReduce

-- alpha-beta equivalence (for strongly normalizing terms) is obtained by
-- fully evaluating the terms using beta-reduction, then checking their
-- alpha-equivalence.
abEq :: Term -> Term -> Bool
abEq t1 t2 = aEq (reduce t1) (reduce t2)

evaluate :: String -> String
evaluate s = showNice (reduce t)
  where
    (t, "") = readNice s


-- Church Encodings in Lambda

-- BOOLEANS

  A boolean is any way to choose between two alternatives ( t - > t - > t )

The boolean constant true always chooses the first alternative
cTrue :: Term
cTrue = lams ["t", "f"] (v "t")

The boolean constant false always chooses the second alternative
cFalse :: Term
cFalse = lams ["t", "f"] (v "f")

--If is not really needed because we can use the booleans themselves, but...
cIf :: Term
cIf = lams ["c", "then", "else"] (v "c" $$ v "then" $$ v "else")

--The boolean negation switches the alternatives
cNot :: Term
cNot = lam "b" (v "b" $$ cFalse $$ cTrue)

--The boolean conjunction can be built as a conditional
cAnd :: Term
cAnd = lams ["b1", "b2"] (v "b1" $$ v "b2" $$ cFalse)

--The boolean disjunction can be built as a conditional
cOr :: Term
cOr = lams ["b1", "b2"] (v "b1" $$ cTrue $$ v "b2")

----------
-- PAIRS--
--------

-- a pair with components of type a and b is a way to compute something based
-- on the values contained within the pair (a -> b -> c) -> c


cPair :: Term
cPair = lams ["f", "s", "action"] (v "action" $$ v "f" $$ v "s")

cFst :: Term
cFst = lam "pair" (v "pair" $$ cTrue)

cSnd :: Term
cSnd = lam "pair" (v "pair" $$ cFalse)

c0 :: Term
c0 = lams ["s", "z"] (v "z") -- note that it's the same as cFalse

c1 :: Term
c1 = lams ["s", "z"] (v "s" $$ v "z")

c2 :: Term
c2 = lams ["s", "z"] (v "s" $$ (v "s" $$ v "z"))

cS :: Term
cS = lams ["t","s","z"] (v "s" $$ (v "t" $$ v "s" $$ v "z"))

cNat :: Integer -> Term
cNat = undefined

cPlus :: Term
cPlus = lams ["n", "m", "s", "z"] (v "n" $$ v "s" $$ (v "m" $$ v "s" $$ v "z"))

cPlus' :: Term
cPlus' = lams ["n", "m"] (v "n" $$ cS $$ v "m")

cMul :: Term
cMul = lams ["n", "m", "s"] (v "n" $$ (v "m" $$ v "s"))

cMul' :: Term
cMul' = lams ["n", "m"] (v "n" $$ (cPlus' $$ v "m") $$ c0)

cPow :: Term
cPow = lams ["m", "n"] (v "n" $$ v "m")

cPow' :: Term
cPow' = lams ["m", "n"] (v "n" $$ (cMul' $$ v "m") $$ c1)

cIs0 :: Term
cIs0 = lam "n" (v "n" $$ (cAnd $$ cFalse) $$ cTrue)

cS' :: Term
cS' = lam "n" (v "n" $$ cS $$ c1)

cS'Rev0 :: Term
cS'Rev0 = lams ["s","z"] c0

cPred :: Term
cPred =
    lam "n"
        (cIf
        $$ (cIs0 $$ v "n")
        $$ c0
        $$ (v "n" $$ cS' $$ cS'Rev0))

cSub :: Term
cSub = lams ["m", "n"] (v "n" $$ cPred $$ v "m")

cLte :: Term
cLte = lams ["m", "n"] (cIs0 $$ (cSub $$ v "m" $$ v "n"))

cGte :: Term
cGte = lams ["m", "n"] (cLte $$ v "n" $$ v "m")

cLt :: Term
cLt = lams ["m", "n"] (cNot $$ (cGte $$ v "m" $$ v "n"))

cGt :: Term
cGt = lams ["m", "n"] (cLt $$ v "n" $$ v "m")

cEq :: Term
cEq = lams ["m", "n"] (cAnd $$ (cLte $$ v "m" $$ v "n") $$ (cLte $$ v "n" $$ v "m"))

cPred' :: Term
cPred' = lam "n" (cFst $$
    (v "n"
    $$ lam "p" (lam "x" (cPair $$ v "x" $$ (cS $$ v "x"))
          $$ (cSnd $$ v "p"))
    $$ (cPair $$ c0 $$ c0)
    ))

cFactorial :: Term
cFactorial = lam "n" (cSnd $$
    (v "n"
    $$ lam "p"
        (cPair
        $$ (cS $$ (cFst $$ v "p"))
        $$ (cMul $$ (cFst $$ v "p") $$ (cSnd $$ v "p"))
        )
    $$ (cPair $$ c1 $$ c1)
    ))

cFibonacci :: Term
cFibonacci = lam "n" (cFst $$
    (v "n"
    $$ lam "p"
        (cPair
        $$ (cSnd $$ v "p")
        $$ (cPlus $$ (cFst $$ v "p") $$ (cSnd $$ v "p"))
        )
    $$ (cPair $$ c0 $$ c1)
    ))

cDivMod :: Term
cDivMod =
    lams ["m", "n"]
        (v "m"
        $$ lam "pair"
          (cIf
          $$ (cLte $$ v "n" $$ (cSnd $$ v "pair"))
          $$ (cPair
             $$ (cS $$ (cFst $$ v "pair"))
             $$ (cSub
                $$ (cSnd $$ v "pair")
                $$ v "n"
                )
             )
          $$ v "pair"
          )
        $$ (cPair $$ c0 $$ v "m")
        )

cNil :: Term
cNil = lams ["agg", "init"] (v "init")

cCons :: Term
cCons = lams ["x","l","agg", "init"]
    (v "agg"
    $$ v "x"
    $$ (v "l" $$ v "agg" $$ v "init")
    )

cList :: [Term] -> Term
cList = foldr (\x l -> cCons $$ x $$ l) cNil

cNatList :: [Integer] -> Term
cNatList = cList . map cNat

cSum :: Term
cSum = lam "l" (v "l" $$ cPlus $$ c0)

cIsNil :: Term
cIsNil = lam "l" (v "l" $$ lams ["x", "a"] cFalse $$ cTrue)

cHead :: Term
cHead = lams ["l", "default"] (v "l" $$ lams ["x", "a"] (v "x") $$ v "default")

cTail :: Term
cTail = lam "l" (cFst $$
    (v "l"
    $$ lams ["x","p"] (lam "t" (cPair $$ v "t" $$ (cCons $$ v "x" $$ v "t"))
          $$ (cSnd $$ v "p"))
    $$ (cPair $$ cNil $$ cNil)
    ))

fix :: Term
fix = lam "f" (lam "x" (v "f" $$ (v "x" $$ v "x")) $$ lam "x" (v "f" $$ (v "x" $$ v "x")))

cDivMod' :: Term
cDivMod' = lams ["m", "n"]
  (cIs0 $$ v "n"
  $$ (cPair $$ c0 $$ v "m")
  $$ (fix
      $$ lams ["f", "p"]
          (lam "x"
              (cIs0 $$ v "x"
              $$ (cLte $$ v "n" $$ (cSnd $$ v "p")
                  $$ (cPair $$ (cS $$ (cFst $$ v "p")) $$ c0)
                  $$ v "p"
                 )
              $$ (v "f" $$ (cPair $$ (cS $$ (cFst $$ v "p")) $$ v "x"))
              )
          $$ (cSub $$ (cSnd $$ v "p") $$ v "n")
          )
      $$ (cPair $$ c0 $$ v "m")
      )
  )

cSudan :: Term
cSudan = fix $$ lam "f" (lams ["n", "x", "y"]
    (cIs0 $$ v "n"
        $$ (cPlus $$ v "x" $$ v "y")
        $$ (cIs0 $$ v "y"
            $$ v "x"
            $$ (lam "fnpy"
                (v "f" $$ (cPred $$ v "n")
                $$ v "fnpy"
                $$ (cPlus $$ v "fnpy" $$ v "y")
                )
                $$ (v "f" $$ v "n" $$ v "x" $$ (cPred $$ v "y"))
                )
            )
    ))

cAckermann :: Term
cAckermann = fix $$ lam "A" (lams ["m", "n"]
    (cIs0 $$ v "m"
    $$ (cS $$ v "n")
    $$ (cIs0 $$ v "n"
        $$ (v "A" $$ (cPred $$ v "m") $$ c1)
        $$ (v "A" $$ (cPred $$ v "m")
            $$ (v "A" $$ v "m" $$ (cPred $$ v "n")))
        )
    ))

 alpha-equivalence
 subst u x t defines [u/x]t, i.e.,  substituting u for x in t
 This substitution avoids variable captures so it is safe to be used when 
 reducing terms with free variables (e.g., if evaluating inside lambda abstractions)
 ^ substitution term
 ^ variable to be substitutes
 ^ term in which the substitution occurs
 Normal order reduction
 - like call by name
 - but also reduce under lambda abstractions if no application is possible
 - guarantees reaching a normal form if it exists
 alpha-beta equivalence (for strongly normalizing terms) is obtained by
 fully evaluating the terms using beta-reduction, then checking their
 alpha-equivalence.
 Church Encodings in Lambda
 BOOLEANS
If is not really needed because we can use the booleans themselves, but...
The boolean negation switches the alternatives
The boolean conjunction can be built as a conditional
The boolean disjunction can be built as a conditional
--------
 PAIRS--
------
 a pair with components of type a and b is a way to compute something based
 on the values contained within the pair (a -> b -> c) -> c
 note that it's the same as cFalse
module LambdaChurch where

import Data.Char (isLetter)
import Data.List ( nub )

class ShowNice a where
    showNice :: a -> String

class ReadNice a where
    readNice :: String -> (a, String)

data Variable
  = Variable
  { name :: String
  , count :: Int
  }
  deriving (Show, Eq, Ord)

var :: String -> Variable
var x = Variable x 0

instance ShowNice Variable where
    showNice (Variable x 0) = x
    showNice (Variable x cnt) = x <> "_" <> show cnt

instance ReadNice Variable where
    readNice s
      | null x = error $ "expected variable but found " <> s
      | otherwise = (var x, s')
      where
        (x, s') = span isLetter s

freshVariable :: Variable -> [Variable] -> Variable
freshVariable var vars = Variable x (cnt + 1)
  where
    x = name var
    varsWithName = filter ((== x) . name) vars
    Variable _ cnt = maximum (var : varsWithName)


data Term
  = V Variable
  | App Term Term
  | Lam Variable Term
  deriving (Show)

aEq :: Term -> Term -> Bool
aEq (V x) (V x') = x == x'
aEq (App t1 t2) (App t1' t2') = aEq t1 t1' && aEq t2 t2'
aEq (Lam x t) (Lam x' t')
  | x == x'   = aEq t t'
  | otherwise = aEq (subst (V y) x t) (subst (V y) x' t')
  where
    fvT = freeVars t
    fvT' = freeVars t'
    allFV = nub ([x, x'] ++ fvT ++ fvT')
    y = freshVariable x allFV
aEq _ _ = False

v :: String -> Term
v x = V (var x)

lam :: String -> Term -> Term
lam x = Lam (var x)

lams :: [String] -> Term -> Term
lams xs t = foldr lam t xs

($$) :: Term -> Term -> Term
($$) = App
infixl 9 $$

instance ShowNice Term where
    showNice (V var) = showNice var
    showNice (App t1 t2) = "(" <> showNice t1 <> " " <> showNice t2 <> ")"
    showNice (Lam var t) = "(" <> "\\" <> showNice var <> "." <> showNice t <> ")"

instance ReadNice Term where
    readNice [] = error "Nothing to read"
    readNice ('(' : '\\' : s) = (Lam var t, s'')
      where
        (var, '.' : s') = readNice s
        (t, ')' : s'') = readNice s'
    readNice ('(' : s) = (App t1 t2, s'')
      where
        (t1, ' ' : s') = readNice s
        (t2, ')' : s'') = readNice s'
    readNice s = (V var, s')
      where
        (var, s') = readNice s

freeVars :: Term -> [Variable]
freeVars (V var) = [var]
freeVars (App t1 t2) = nub $ freeVars t1 ++ freeVars t2
freeVars (Lam var t) = filter (/= var) (freeVars t)


  for example [ 3 / x](x + x ) = = 3 + 3
subst
    -> Term
subst u x (V y)
  | x == y    = u
  | otherwise = V y
subst u x (App t1 t2) = App (subst u x t1) (subst u x t2)
subst u x (Lam y t)
  | x == y          = Lam y t
  | y `notElem` fvU = Lam y (subst u x t)
  | x `notElem` fvT = Lam y t
  | otherwise       = Lam y' (subst u x (subst (V y') y t))
  where
    fvT = freeVars t
    fvU = freeVars u
    allFV = nub ([x] ++ fvU ++ fvT)
    y' = freshVariable y allFV

normalReduceStep :: Term -> Maybe Term
normalReduceStep (App (Lam v t) t2) = Just $ subst t2 v t
normalReduceStep (App t1 t2)
  | Just t1' <- normalReduceStep t1 = Just $ App t1' t2
  | Just t2' <- normalReduceStep t2 = Just $ App t1 t2'
normalReduceStep (Lam x t)
  | Just t' <- normalReduceStep t = Just $ Lam x t'
normalReduceStep _ = Nothing

normalReduce :: Term -> Term
normalReduce t
  | Just t' <- normalReduceStep t = normalReduce t'
  | otherwise = t

reduce :: Term -> Term
reduce = normalReduce

abEq :: Term -> Term -> Bool
abEq t1 t2 = aEq (reduce t1) (reduce t2)

evaluate :: String -> String
evaluate s = showNice (reduce t)
  where
    (t, "") = readNice s




  A boolean is any way to choose between two alternatives ( t - > t - > t )

The boolean constant true always chooses the first alternative
cTrue :: Term
cTrue = lams ["t", "f"] (v "t")

The boolean constant false always chooses the second alternative
cFalse :: Term
cFalse = lams ["t", "f"] (v "f")

cIf :: Term
cIf = lams ["c", "then", "else"] (v "c" $$ v "then" $$ v "else")

cNot :: Term
cNot = lam "b" (v "b" $$ cFalse $$ cTrue)

cAnd :: Term
cAnd = lams ["b1", "b2"] (v "b1" $$ v "b2" $$ cFalse)

cOr :: Term
cOr = lams ["b1", "b2"] (v "b1" $$ cTrue $$ v "b2")




cPair :: Term
cPair = lams ["f", "s", "action"] (v "action" $$ v "f" $$ v "s")

cFst :: Term
cFst = lam "pair" (v "pair" $$ cTrue)

cSnd :: Term
cSnd = lam "pair" (v "pair" $$ cFalse)

c0 :: Term

c1 :: Term
c1 = lams ["s", "z"] (v "s" $$ v "z")

c2 :: Term
c2 = lams ["s", "z"] (v "s" $$ (v "s" $$ v "z"))

cS :: Term
cS = lams ["t","s","z"] (v "s" $$ (v "t" $$ v "s" $$ v "z"))

cNat :: Integer -> Term
cNat = undefined

cPlus :: Term
cPlus = lams ["n", "m", "s", "z"] (v "n" $$ v "s" $$ (v "m" $$ v "s" $$ v "z"))

cPlus' :: Term
cPlus' = lams ["n", "m"] (v "n" $$ cS $$ v "m")

cMul :: Term
cMul = lams ["n", "m", "s"] (v "n" $$ (v "m" $$ v "s"))

cMul' :: Term
cMul' = lams ["n", "m"] (v "n" $$ (cPlus' $$ v "m") $$ c0)

cPow :: Term
cPow = lams ["m", "n"] (v "n" $$ v "m")

cPow' :: Term
cPow' = lams ["m", "n"] (v "n" $$ (cMul' $$ v "m") $$ c1)

cIs0 :: Term
cIs0 = lam "n" (v "n" $$ (cAnd $$ cFalse) $$ cTrue)

cS' :: Term
cS' = lam "n" (v "n" $$ cS $$ c1)

cS'Rev0 :: Term
cS'Rev0 = lams ["s","z"] c0

cPred :: Term
cPred =
    lam "n"
        (cIf
        $$ (cIs0 $$ v "n")
        $$ c0
        $$ (v "n" $$ cS' $$ cS'Rev0))

cSub :: Term
cSub = lams ["m", "n"] (v "n" $$ cPred $$ v "m")

cLte :: Term
cLte = lams ["m", "n"] (cIs0 $$ (cSub $$ v "m" $$ v "n"))

cGte :: Term
cGte = lams ["m", "n"] (cLte $$ v "n" $$ v "m")

cLt :: Term
cLt = lams ["m", "n"] (cNot $$ (cGte $$ v "m" $$ v "n"))

cGt :: Term
cGt = lams ["m", "n"] (cLt $$ v "n" $$ v "m")

cEq :: Term
cEq = lams ["m", "n"] (cAnd $$ (cLte $$ v "m" $$ v "n") $$ (cLte $$ v "n" $$ v "m"))

cPred' :: Term
cPred' = lam "n" (cFst $$
    (v "n"
    $$ lam "p" (lam "x" (cPair $$ v "x" $$ (cS $$ v "x"))
          $$ (cSnd $$ v "p"))
    $$ (cPair $$ c0 $$ c0)
    ))

cFactorial :: Term
cFactorial = lam "n" (cSnd $$
    (v "n"
    $$ lam "p"
        (cPair
        $$ (cS $$ (cFst $$ v "p"))
        $$ (cMul $$ (cFst $$ v "p") $$ (cSnd $$ v "p"))
        )
    $$ (cPair $$ c1 $$ c1)
    ))

cFibonacci :: Term
cFibonacci = lam "n" (cFst $$
    (v "n"
    $$ lam "p"
        (cPair
        $$ (cSnd $$ v "p")
        $$ (cPlus $$ (cFst $$ v "p") $$ (cSnd $$ v "p"))
        )
    $$ (cPair $$ c0 $$ c1)
    ))

cDivMod :: Term
cDivMod =
    lams ["m", "n"]
        (v "m"
        $$ lam "pair"
          (cIf
          $$ (cLte $$ v "n" $$ (cSnd $$ v "pair"))
          $$ (cPair
             $$ (cS $$ (cFst $$ v "pair"))
             $$ (cSub
                $$ (cSnd $$ v "pair")
                $$ v "n"
                )
             )
          $$ v "pair"
          )
        $$ (cPair $$ c0 $$ v "m")
        )

cNil :: Term
cNil = lams ["agg", "init"] (v "init")

cCons :: Term
cCons = lams ["x","l","agg", "init"]
    (v "agg"
    $$ v "x"
    $$ (v "l" $$ v "agg" $$ v "init")
    )

cList :: [Term] -> Term
cList = foldr (\x l -> cCons $$ x $$ l) cNil

cNatList :: [Integer] -> Term
cNatList = cList . map cNat

cSum :: Term
cSum = lam "l" (v "l" $$ cPlus $$ c0)

cIsNil :: Term
cIsNil = lam "l" (v "l" $$ lams ["x", "a"] cFalse $$ cTrue)

cHead :: Term
cHead = lams ["l", "default"] (v "l" $$ lams ["x", "a"] (v "x") $$ v "default")

cTail :: Term
cTail = lam "l" (cFst $$
    (v "l"
    $$ lams ["x","p"] (lam "t" (cPair $$ v "t" $$ (cCons $$ v "x" $$ v "t"))
          $$ (cSnd $$ v "p"))
    $$ (cPair $$ cNil $$ cNil)
    ))

fix :: Term
fix = lam "f" (lam "x" (v "f" $$ (v "x" $$ v "x")) $$ lam "x" (v "f" $$ (v "x" $$ v "x")))

cDivMod' :: Term
cDivMod' = lams ["m", "n"]
  (cIs0 $$ v "n"
  $$ (cPair $$ c0 $$ v "m")
  $$ (fix
      $$ lams ["f", "p"]
          (lam "x"
              (cIs0 $$ v "x"
              $$ (cLte $$ v "n" $$ (cSnd $$ v "p")
                  $$ (cPair $$ (cS $$ (cFst $$ v "p")) $$ c0)
                  $$ v "p"
                 )
              $$ (v "f" $$ (cPair $$ (cS $$ (cFst $$ v "p")) $$ v "x"))
              )
          $$ (cSub $$ (cSnd $$ v "p") $$ v "n")
          )
      $$ (cPair $$ c0 $$ v "m")
      )
  )

cSudan :: Term
cSudan = fix $$ lam "f" (lams ["n", "x", "y"]
    (cIs0 $$ v "n"
        $$ (cPlus $$ v "x" $$ v "y")
        $$ (cIs0 $$ v "y"
            $$ v "x"
            $$ (lam "fnpy"
                (v "f" $$ (cPred $$ v "n")
                $$ v "fnpy"
                $$ (cPlus $$ v "fnpy" $$ v "y")
                )
                $$ (v "f" $$ v "n" $$ v "x" $$ (cPred $$ v "y"))
                )
            )
    ))

cAckermann :: Term
cAckermann = fix $$ lam "A" (lams ["m", "n"]
    (cIs0 $$ v "m"
    $$ (cS $$ v "n")
    $$ (cIs0 $$ v "n"
        $$ (v "A" $$ (cPred $$ v "m") $$ c1)
        $$ (v "A" $$ (cPred $$ v "m")
            $$ (v "A" $$ v "m" $$ (cPred $$ v "n")))
        )
    ))
