Prelude.tel

and = \a b -> if a then b else 0

or = \a b -> if a then 1 else b

not = \x -> if x then 0 else 1

succ = \x -> (x,0)

d2cG = \r -> let layer = \recur i f b -> if i
                                            then f (recur (left i) f b)
                                            else b
             in r layer (\i f b -> b)
d2c = d2cG ?

c2d = \c -> c succ 0

plus = \m n f x -> m f (n f x)

times = \m n f -> m (n f)

pow = \m n -> n m

dMinus = \a b -> d2c b (\x -> left x) a

minus = \a b -> d2c (b (\x -> left x) (c2d a))

range = \a b -> let layer = \recur i -> if dMinus b i
                                           then (i, recur (i,0))
                                           else 0
                in ? layer (\i -> 0) a

mapG = \r f -> let layer = \recur l -> if l then (f (left l), recur (right l)) else 0
                   base = \l -> 0
               in r layer base
map = mapG ?

foldrG = \r f -> let layer = \recur accum l -> if l then f (left l) (recur accum (right l))
                                                    else accum
                     base = \accum l -> accum
                 in r layer base 
foldr = foldrG ?

foldlG = \r f -> let layer = \recur accum l -> if l then recur (f accum (left l)) (right l)
                                                    else accum
                     base = \accum l -> accum
                 in r layer base 
foldl = foldlG ?

zipWithG = \r f -> let layer = \recur a b -> if (and a b)
                                                then (f (left a) (left b)
                                                      , recur (right a) (right b)
                                                      )
                                                else 0
                       base = \a b -> 0
                   in r layer base 
zipWith = zipWithG ?

filter = \f -> foldr (\a b -> if f a then (a, b) else b) 0 

dEqual = \a b -> let equalsOne = \x -> if x then (not (left x)) else 0
                 in if a then equalsOne (d2c (left a) (\x -> left x) b)
                         else not b

listLength = foldr (\a b -> succ b) 0

listEqual = \a b -> let pairsEqual = zipWith dEqual a b
                        lengthEqual = dEqual (listLength a) (listLength b)
                    in foldr and 1 (lengthEqual,pairsEqual)

listPlus = \a b -> foldr (\x l -> (x,l)) b a

concat = foldr listPlus 0

drop = \n l -> n (\x -> right x) l

take = \n l -> let lengthed = n (\x -> (0,x)) 0
               in zipWith (\a b -> a) l lengthed

takeG = \r n l -> let lengthed = n (\x -> (0,x)) 0
                  in zipWithG r (\a b -> a) l lengthed

factorial = \n -> foldr (\a b -> times (d2c a) b) $1 (range 1 (n,0))

quicksort = let layer = \recur l -> if right l
                                       then let t = left l
                                                test = \x -> dMinus x t
                                                p1 = filter test (right l)
                                                p2 = filter (\x -> not (test x)) (right l)
                                            in listPlus (recur p2) (t,(recur p1))
                                       else l
            in ? layer (\l -> 0)