{-# LANGUAGE NoImplicitPrelude #-}
-- declarations of builtin functions and data types used by the compiler
module Internals where

-- used for type annotations
typeAnn x = x

undefined :: forall (a :: Type) . a

primFix :: forall (a :: Type) . (a -> a) -> a

data Unit = TT
data String
data Empty (a :: String)

unsafeCoerce :: forall a b . a -> b

-- equality constraints
type family EqCT (t :: Type) (a :: t) (b :: t)
{-
coe :: forall (a :: Type) (b :: Type) -> EqCT Type a b -> a -> b
coe a b TT x = unsafeCoerce @a @b x
-}
-- TODO: generate?
data Tuple0 = Tuple0
data Tuple1 a = Tuple1 a
data Tuple2 a b = Tuple2 a b
data Tuple3 a b c = Tuple3 a b c
data Tuple4 a b c d = Tuple4 a b c d
data Tuple5 a b c d e = Tuple5 a b c d e

-- ... TODO

-- builtin used for overlapping instances
parEval :: forall a -> a -> a -> a

type family JoinTupleType t1 t2 where
    -- TODO
    JoinTupleType a () = a
    JoinTupleType a (b, c) = (a, b, c)
    JoinTupleType a (b, c, d) = (a, b, c, d)
    JoinTupleType a (b, c, d, e) = (a, b, c, d, e)
    JoinTupleType a b = (a, b)

-- conjuction of constraints
type family T2 a b

match'Type :: forall (m :: Type -> Type) -> m Type -> forall (t :: Type) -> m t -> m t

testmt :: forall (t :: Type) -> t -> t
testmt 'Type = \'Tuple0 -> 'Tuple0
--testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> & 'Type) 'Tuple0 x undefined) t undefined) x
--testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> 'Type) 'Tuple0 x undefined) t undefined) x

--type instance EqCT Type = \'Type 'Type -> 'Unit
--type instance EqCT Type = \'(a, b) '(JoinTupleType a' b') -> '(T2 (EqCT Type a a') (EqCT Type b b'))

type EqCTt = EqCT _

-- builtin conjuction of constraint witnesses
t2C :: Unit -> Unit -> Unit

-- builtin type constructors
data Int
data Word
data Float
data Char

data Bool = False | True

data Ordering = LT | EQ | GT

data Nat = Zero | Succ Nat

-- builtin primitives
primIntToWord       :: Int   -> Word
primIntToFloat      :: Int   -> Float
primIntToNat        :: Int   -> Nat
primCompareInt      :: Int   -> Int   -> Ordering
primCompareWord     :: Word  -> Word  -> Ordering
primCompareFloat    :: Float -> Float -> Ordering
primCompareChar     :: Char  -> Char  -> Ordering
primCompareString   :: String -> String -> Ordering
primNegateInt       :: Int   -> Int
primNegateWord      :: Word  -> Word
primNegateFloat     :: Float -> Float
primAddInt          :: Int   -> Int   -> Int
primSubInt          :: Int   -> Int   -> Int
primModInt          :: Int   -> Int   -> Int
primSqrtFloat       :: Float -> Float
primRound           :: Float -> Int


primIfThenElse :: Bool -> a -> a -> a
primIfThenElse True  a b = a
primIfThenElse False a b = b

isEQ EQ = True
isEQ _ = False

-- fromInt is needed for integer literal
class Num a where
  fromInt :: Int -> a
  compare :: a -> a -> Ordering
  negate :: a -> a

instance Num Int where
  fromInt = \x -> x
  compare = primCompareInt
  negate  = primNegateInt
instance Num Word where
  fromInt = primIntToWord
  compare = primCompareWord
  negate  = primNegateWord
instance Num Float where
  fromInt = primIntToFloat
  compare = primCompareFloat
  negate  = primNegateFloat
instance Num Nat where
  fromInt = primIntToNat --if isEQ (primCompareInt n zero') then Zero else Succ (fromInt (primSubInt n one'))
  compare = undefined
  negate  = undefined

class Eq a where
    (==) :: a -> a -> Bool     -- todo: use (==) sign

infix 4 ==

instance Eq String where a == b = isEQ (primCompareString a b)
instance Eq Char where a == b = isEQ (primCompareChar a b)
instance Eq Int where a == b = isEQ (primCompareInt a b)
instance Eq Float where a == b = isEQ (primCompareFloat a b)
instance Eq Bool where
    True == True = True
    False == False = True
    _ == _ = False
instance Eq Nat where
    Zero   == Zero   = True
    Succ a == Succ b = a == b
    _      == _      = False

data List a = Nil | Cons a (List a)

infixr 5 :