lambdacube-compiler-0.5.0.0: lc/Internals.lc

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

-- used for type annotations
typeAnn x = x

-- used for recognising double parenthesis
parens 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

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

-- conjuction of constraints
type family T2 a b

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

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 :

data HList :: [Type] -> Type where
    HNil :: HList '[]
    HCons :: x -> HList xs -> HList '(x: xs)

hlistNilCase :: forall c -> c -> HList Nil -> c
hlistConsCase
    :: forall (e :: Type) (f :: List Type)
    .  forall c
    -> (e -> HList f -> c)
    -> HList (Cons e f)
    -> c

{-
-- TODO: unsafeCoerce is not really needed here
hlistConsCase @e @f c fv x = 'HListCase 
    (\_ _ -> c)
    undefined
    (\ @t @lt y ys -> fv (unsafeCoerce @t @e y) (unsafeCoerce @(HList lt) @(HList f) ys))
    x

hlistNilCase c x v = 'HListCase
    (\_ _ -> c)
    x
    (\_ _ -> undefined :: c)
    v
-}