Prelude.tel

id = \x -> x

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)

d2c = \n f b -> { id
                , \recur i  -> f (recur (left i))
                , \i -> b
                } n

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 -> { \i -> dMinus b i
                , \recur i -> (i, recur (i,0))
                , \i -> 0
                } a

map = \f -> { id
            , \recur l -> (f (left l), recur (right l))
            , \l -> 0
            }

foldr = \f b ta -> let fixed = { id
                               , \recur l accum -> f (left l) (recur (right l) accum)
                               , \l accum -> accum
                               }
                   in fixed ta b

foldl = \f b ta -> let fixed = { id
                               , \recur l accum -> recur (right l) (f accum (left l))
                               , \l accum -> accum
                               }
                   in fixed ta b

zipWith = \f a b -> let fixed = { \ab -> and (left ab) (right ab)
                                , \recur ab -> (f (left (left ab)) (left (right ab))
                                               , recur (right (left ab), right (right ab))
                                               )
                                , \ab -> 0
                                }
                    in fixed (a,b)

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

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

quicksort = { \l -> right l
            , \recur l -> 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))
            , id
            }

abort = \str -> let x : (\y -> listPlus "abort: " str) = 1
                in x

assert = \t s -> if not t then (1, s) else 0

-- useful for making sure main input isn't unbounded
truncate = \n ->
  let layer = \recur current -> if current
                                then (recur (left current), recur (right current))
                                else 0
  in n layer (\x -> 0)

max = \a b -> { \p -> or (left p) (right p)
              , \recur p -> recur (left (left p), left (right p))
              , \p -> if (left p) then b else a
              } (a,b)