{-# LANGUAGE PolyKinds #-}

module MAlonzo.RTE where

import Prelude
  ( Bool, Char, Double, Integer, String
  , Enum(..), Eq(..), Ord(..), Integral(..), Num(..)
  , ($), error, otherwise
  , (++), fromIntegral
  )

import Data.Char ( GeneralCategory(Surrogate), generalCategory )
import Data.Kind ( Type)
import qualified Data.Word
import qualified GHC.Exts as GHC ( Any )
import Unsafe.Coerce ( unsafeCoerce )

type AgdaAny = GHC.Any

-- Special version of coerce that plays well with rules.
{-# INLINE [1] coe #-}
coe :: a -> b
coe :: forall a b. a -> b
coe = a -> b
forall a b. a -> b
unsafeCoerce
{-# RULES "coerce-id" forall (x :: a) . coe x = x #-}

-- Builtin QNames.
data QName = QName { QName -> Integer
nameId, QName -> Integer
moduleId :: Integer, QName -> String
qnameString :: String, QName -> Fixity
qnameFixity :: Fixity }

data Assoc      = NonAssoc | LeftAssoc | RightAssoc
data Precedence = Unrelated | Related PrecedenceLevel
data Fixity     = Fixity Assoc Precedence
type PrecedenceLevel = Double

instance Eq QName where
  QName Integer
a Integer
b String
_ Fixity
_ == :: QName -> QName -> Bool
== QName Integer
c Integer
d String
_ Fixity
_ = (Integer
a, Integer
b) (Integer, Integer) -> (Integer, Integer) -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer
c, Integer
d)

instance Ord QName where
  compare :: QName -> QName -> Ordering
compare (QName Integer
a Integer
b String
_ Fixity
_) (QName Integer
c Integer
d String
_ Fixity
_) = (Integer, Integer) -> (Integer, Integer) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer
a, Integer
b) (Integer
c, Integer
d)

erased :: a
erased :: forall a. a
erased = (Any -> Any) -> a
forall a b. a -> b
coe (\ Any
_ -> Any
forall a. a
erased)

mazUnreachableError :: a
mazUnreachableError :: forall a. a
mazUnreachableError = String -> a
forall a. HasCallStack => String -> a
error (String
"Agda: unreachable code reached.")

mazHole :: String -> a
mazHole :: forall a. String -> a
mazHole String
s = String -> a
forall a. HasCallStack => String -> a
error (String
"Agda: reached hole: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)

addInt :: Integer -> Integer -> Integer
addInt :: Integer -> Integer -> Integer
addInt = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)

subInt :: Integer -> Integer -> Integer
subInt :: Integer -> Integer -> Integer
subInt = (-)

mulInt :: Integer -> Integer -> Integer
mulInt :: Integer -> Integer -> Integer
mulInt = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)

geqInt :: Integer -> Integer -> Bool
geqInt :: Integer -> Integer -> Bool
geqInt = Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(>=)

ltInt :: Integer -> Integer -> Bool
ltInt :: Integer -> Integer -> Bool
ltInt = Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<)

eqInt :: Integer -> Integer -> Bool
eqInt :: Integer -> Integer -> Bool
eqInt = Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(==)

quotInt :: Integer -> Integer -> Integer
quotInt :: Integer -> Integer -> Integer
quotInt = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
quot

remInt :: Integer -> Integer -> Integer
remInt :: Integer -> Integer -> Integer
remInt = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
rem

-- #4999: Data.Text maps surrogate code points (\xD800 - \xDFFF) to the replacement character
-- \xFFFD, so to keep strings isomorphic to list of characters we do the same for characters.
natToChar :: Integer -> Char
natToChar :: Integer -> Char
natToChar Integer
n | Char -> GeneralCategory
generalCategory Char
c GeneralCategory -> GeneralCategory -> Bool
forall a. Eq a => a -> a -> Bool
== GeneralCategory
Surrogate = Char
'\xFFFD'
            | Bool
otherwise                      = Char
c
  where c :: Char
c = Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> Int -> Char
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
n Integer
0x110000

-- Words --

type Word64 = Data.Word.Word64

word64ToNat :: Word64 -> Integer
word64ToNat :: Word64 -> Integer
word64ToNat = Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral

word64FromNat :: Integer -> Word64
word64FromNat :: Integer -> Word64
word64FromNat = Integer -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral

{-# INLINE add64 #-}
add64 :: Word64 -> Word64 -> Word64
add64 :: Word64 -> Word64 -> Word64
add64 = Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+)

{-# INLINE sub64 #-}
sub64 :: Word64 -> Word64 -> Word64
sub64 :: Word64 -> Word64 -> Word64
sub64 = (-)

{-# INLINE mul64 #-}
mul64 :: Word64 -> Word64 -> Word64
mul64 :: Word64 -> Word64 -> Word64
mul64 = Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(*)

{-# INLINE quot64 #-}
quot64 :: Word64 -> Word64 -> Word64
quot64 :: Word64 -> Word64 -> Word64
quot64 = Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
quot

{-# INLINE rem64 #-}
rem64 :: Word64 -> Word64 -> Word64
rem64 :: Word64 -> Word64 -> Word64
rem64 = Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
rem

{-# INLINE eq64 #-}
eq64 :: Word64 -> Word64 -> Bool
eq64 :: Word64 -> Word64 -> Bool
eq64 = Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
(==)

{-# INLINE lt64 #-}
lt64 :: Word64 -> Word64 -> Bool
lt64 :: Word64 -> Word64 -> Bool
lt64 = Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
(<)

-- Support for musical coinduction.

data Inf                      a = Sharp { forall a. Inf a -> a
flat :: a }
type Infinity (level :: Type) a = Inf a