{-# OPTIONS_GHC -fglasgow-exts #-}

module Main where

import GHC.Base

main = do print (natToInt runtest2)
          print (natToInt runtest)

coerce :: a -> b
coerce = unsafeCoerce#

data Type = forall a. Type a
data Val = Val

class Project x where
    project :: forall val. Int -> x -> val

data Nat = O | S Nat
  deriving Show

elim_Nat :: TT_Nat -> a -> (TT_Nat -> a -> a) -> a
elim_Nat n mz ms = (coerce (fn_NatElim ((coerce n)::val) Type 
                                     ((coerce mz)::val) 
                                     ((coerce ms)::val)))::a

runtest :: Nat
runtest = getNat ((coerce fn_testval)::TT_Nat)

runtest2 :: Nat
runtest2 = getNat ((coerce fn_testval2)::TT_Nat)

getNat :: TT_Nat -> Nat
getNat n = elim_Nat n O (\k ih -> S ih)

natToInt :: Nat -> Integer
natToInt O = 0
natToInt (S k) = 1+(natToInt k)

{------ Generated stuff ---------}
data TT_Nat = TT_O | forall arg. TT_S arg 

instance Project TT_Nat where

        project 0 (TT_S  a0) = ((coerce a0)::val)

fn_NatElim :: val -> val -> val -> val -> val
fn_NatElim = (\v0 -> (\v1 -> (\v2 -> (\v3 -> (case ((coerce v0)::TT_Nat) of { TT_O  -> v2 ; TT_S _  -> (((coerce v3)::val->val->val) ((coerce (project 0((coerce v0)::TT_Nat)))::val) ((coerce (((coerce fn_NatElim)::val->val->val->val->val) ((coerce (project 0((coerce v0)::TT_Nat)))::val) ((coerce v1)::val) ((coerce v2)::val) ((coerce v3)::val) ))::val) ) ; })))))

fn_testval :: val
fn_testval = (((coerce fn_fact)::val->val) ((coerce (TT_S ((coerce (TT_S ((coerce (TT_S ((coerce (TT_S ((coerce (TT_S ((coerce (TT_S ((coerce (TT_S ((coerce (TT_S ((coerce (TT_S ((coerce (TT_O ))::val) ))::val) ))::val) ))::val) ))::val) ))::val) ))::val) ))::val) ))::val) ))::val) )

fn_fact :: val -> val
fn_fact = (\v0 -> (((coerce fn_NatElim)::val->val->val->val->val) ((coerce v0)::val) ((coerce (\v1 -> Type))::val) ((coerce (TT_S ((coerce (TT_O ))::val) ))::val) ((coerce (\v1 -> (\v2 -> (((coerce fn_mult)::val->val->val) ((coerce (TT_S ((coerce v1)::val) ))::val) ((coerce v2)::val) ))))::val) ))

fn_mult :: val -> val -> val
fn_mult = (\v0 -> (\v1 -> (((coerce fn_NatElim)::val->val->val->val->val) ((coerce v0)::val) ((coerce (\v2 -> Type))::val) ((coerce (TT_O ))::val) ((coerce (\v2 -> (\v3 -> (((coerce fn_plus)::val->val->val) ((coerce v1)::val) ((coerce v3)::val) ))))::val) )))

fn_adder :: val -> val -> val
fn_adder = (\v0 -> (((coerce fn_NatElim)::val->val->val->val->val) ((coerce v0)::val) ((coerce (\v1 -> Type))::val) ((coerce (\v1 -> v1))::val) ((coerce (\v1 -> (\v2 -> (\v3 -> (\v4 -> (((coerce v2)::val->val) ((coerce (((coerce fn_plus)::val->val->val) ((coerce v3)::val) ((coerce v4)::val) ))::val) ))))))::val) ))

fn_adderType :: val -> val -> val
fn_adderType = (\v0 -> (\v1 -> (((coerce fn_NatElim)::val->val->val->val->val) ((coerce v0)::val) ((coerce (\v2 -> Type))::val) ((coerce Type)::val) ((coerce (\v2 -> (\v3 -> Type)))::val) )))

fn_plus :: val -> val -> val
fn_plus = (\v0 -> (((coerce fn_NatElim)::val->val->val->val->val) ((coerce v0)::val) ((coerce (\v1 -> Type))::val) ((coerce (\v1 -> v1))::val) ((coerce (\v1 -> (\v2 -> (\v3 -> (TT_S ((coerce (((coerce v2)::val->val) ((coerce v3)::val) ))::val) )))))::val) ))


data TT_Vect = forall arg. TT_vnil arg | forall arg. TT_vcons arg arg arg arg 

instance Project TT_Vect where
    project 0 (TT_vnil  a0) = ((coerce a0)::val)
    project 3 (TT_vcons  a0 a1 a2 a3) = ((coerce a3)::val)  
    project 2 (TT_vcons  a0 a1 a2 a3) = ((coerce a2)::val)  
    project 1 (TT_vcons  a0 a1 a2 a3) = ((coerce a1)::val)  
    project 0 (TT_vcons  a0 a1 a2 a3) = ((coerce a0)::val)


fn_VectElim :: val -> val -> val -> val -> val -> val -> val
fn_VectElim = (\v0 -> (\v1 -> (\v2 -> (\v3 -> (\v4 -> (\v5 -> (case ((coerce v2)::TT_Vect) of { TT_vnil _  -> v4 ; TT_vcons _ _ _ _  -> (((coerce v5)::val->val->val->val->val) ((coerce (project 1((coerce v2)::TT_Vect)))::val) ((coerce (project 2((coerce v2)::TT_Vect)))::val) ((coerce (project 3((coerce v2)::TT_Vect)))::val) ((coerce (((coerce fn_VectElim)::val->val->val->val->val->val->val) ((coerce (project 0((coerce v2)::TT_Vect)))::val) ((coerce (project 1((coerce v2)::TT_Vect)))::val) ((coerce (project 3((coerce v2)::TT_Vect)))::val) ((coerce v3)::val) ((coerce v4)::val) ((coerce v5)::val) ))::val) ) ; })))))))



fn_testvect2 :: val
fn_testvect2 = (coerce (TT_vcons ((coerce Type)::val) ((coerce (TT_S ((coerce (TT_O ))::val) ))::val) ((coerce (TT_S ((coerce (TT_O ))::val) ))::val) ((coerce (TT_vcons ((coerce Type)::val) ((coerce (TT_O ))::val) ((coerce (TT_S ((coerce (TT_S ((coerce (TT_S ((coerce (TT_O ))::val) ))::val) ))::val) ))::val) ((coerce (TT_vnil ((coerce Type)::val) ))::val) ))::val) )::val)

fn_vectsum :: val -> val -> val
fn_vectsum = (\v0 -> (\v1 -> (((coerce fn_VectElim)::val->val->val->val->val->val->val) ((coerce Type)::val) ((coerce v0)::val) ((coerce v1)::val) ((coerce (\v2 -> (\v3 -> Type)))::val) ((coerce (TT_O ))::val) ((coerce (\v2 -> (\v3 -> (\v4 -> (\v5 -> (((coerce fn_plus)::val->val->val) ((coerce v3)::val) ((coerce v5)::val) ))))))::val) )))


fn_testval2 :: val
fn_testval2 = (((coerce fn_vectsum)::val->val->val) ((coerce (TT_S ((coerce (TT_S ((coerce (TT_O ))::val) ))::val) ))::val) ((coerce fn_testvect2)::val) )