data Bool :: * = False :: Bool ; True :: Bool
data List (a :: *) :: * = Nil :: List a ; Cons :: a -> List a -> List a

primitive primAdd :: Int -> Int -> Int
primitive primSub :: Int -> Int -> Int
primitive primMod :: Int -> Int -> Int
primitive primSqrt :: Int -> Int
primitive primIntEq :: Int -> Int -> Bool
primitive primIntLess :: Int -> Int -> Bool

primitive primFix :: forall {i :: Int} . forall {{a :: *}} . (a -> a) -> a 

{-
let int' =
        (fix (Int -> List Int -> Int)
            (\f n xs ->   --   ((f, n, xs); xs, n)
                boolCase (\ _ -> Int)
                    (f  (primSub n #1)
                        (listCase Int (\ _ -> List Int)
                            (fix (List Int) (\u -> u))
                            (\ x xs -> xs)
                            xs))
                    (listCase Int (\ _ -> Int)
                        (fix Int (\u -> u))
                        (\ x xs -> x)
                        xs)
                    (primIntEq #0 n)))
        #10000
        (fix (List Int)
            (\primes ->   -- primes
                (Cons Int #2 (Cons Int #3
                    (fix (List Int -> List Int)
                        (\fil ->   --  (fil + primes)
                            listCase Int (\ _ -> List Int)
                                (Nil Int)
                                (\ x' xs' ->  --  ((fil, xs'); (x', (fil, xs')), (x', primes))
                                    boolCase (\ _ -> List Int)
                                        (fil xs')
                                        (Cons Int x' (fil xs'))
                                        (fix (List Int -> Bool)
                                            (\al ->   --  (al, x')
                                                listCase Int (\ _ -> Bool)
                                                    True
                                                    (\ x'' xs ->  -- (;(al, xs), (x', x''))
                                                        boolCase (\ _ -> Bool)
                                                            False
                                                            (al xs)
                                                            (boolCase (\ _ -> Bool)
                                                                True
                                                                False
                                                                (primIntEq #0 (primMod x' x'')))))
                                            (fix (List Int -> List Int)
                                                (\tw ->   -- (tw + x')
                                                    listCase Int (\ _ -> List Int)
                                                        (Nil Int)
                                                        (\ x xs ->   -- (;(x, (tw, xs)), (x + x'))
                                                            boolCase (\ _ -> List Int)
                                                                (Nil Int)
                                                                (Cons Int x (tw xs))
                                                                (((\m ->  -- (((x, m);, (x, m)), x')
                                                                        boolCase (\ _ -> Bool)
                                                                            (primIntEq !x !m)
                                                                            True
                                                                            (primIntLess !x !m)) :: Int -> Bool)
                                                                    (primSqrt x'))))
                                                primes))))
                        (fix (Int -> List Int)
                            !(\ f n ->  -- (n, (f, n))
                                Cons Int n (f !(primAdd #1 !n))) !#5))))))
-}

let filter =
  \{a :: *} (p :: a -> Bool) -> fix (List a -> List a) (\fil -> listCase a (\ _ -> List a) (Nil a)
        (\x xs -> boolCase (\ _ -> List a)
                     (fil xs)
                     (Cons a x (fil xs))
                     (p x)))

let fromThen = \(d :: Int) -> fix (Int -> List Int) (\f n -> Cons Int n (f (primAdd d n)))

let undefined = \{a :: *} -> fix a (\u -> u)

let head =
  \{a :: *} (xs :: List a) -> listCase a (\ _ -> a) (undefined a) (\ x xs -> x) xs

let tail =
  \{a :: *} (xs :: List a) -> listCase a (\ _ -> List a) (undefined (List a)) (\ x xs -> xs) xs

let nth =
  \{a :: *} -> fix (Int -> List a -> a) (\f n xs -> boolCase (\ _ -> a)
                     (listCase a (\ _ -> a) (undefined a) (\x xs -> f (primSub n #1) xs) xs)
                     (head a xs)
                     (primIntEq #0 n))

let takeWhile =
  \{a :: *} (p :: a -> Bool) -> fix (List a -> List a) (\tw -> listCase a (\ _ -> List a) (Nil a)
        (\x xs -> boolCase (\ _ -> List a)
                     (Nil a)
                     (Cons a x (tw xs))
                     (p x)))

let and = \(a :: Bool) (b :: Bool) -> boolCase (\ _ -> Bool) False b a
let or  = \(a :: Bool) (b :: Bool) -> boolCase (\ _ -> Bool) b True a
let not = boolCase (\ _ -> Bool) True False

let all =
  \{a :: *} (p :: a -> Bool) -> fix (List a -> Bool) (\al -> listCase a (\ _ -> Bool) True
        (\x xs -> and (p x) (al xs)))

let intLEq = \(n :: Int) (m :: Int) -> or (primIntLess n m) (primIntEq n m)

let primes = fix (List Int) (\primes ->
   (Cons Int #2 (Cons Int #3 (filter Int (\ x -> all Int (\ i -> not (primIntEq #0 (primMod x i))) (
        takeWhile Int (\p -> (\(m :: Int) -> or (primIntLess p m) (primIntEq p m)) (primSqrt x)) primes
        )) (fromThen #2 #5)))
    ))

let nthPrimes = \(n :: Int) -> nth Int n primes

let main = nthPrimes