packages feed

Agda-2.3.2.2: src/rts/RTP.hs

module RTP where
import RTS
import Prelude ((.), Eq, (==), Show, show)
import qualified Prelude hiding ((.), Eq, (==))

import Data.Char

-- import qualified RTS

undefined = Prelude.undefined

data Nat = Zero | Suc Nat

data Bool = False | True

type Float = Prelude.Double
-- newtype Float = FloatT { unboxFloat :: Prelude.Float}
newtype Char = CharT { unboxChar :: Prelude.Char } deriving (Prelude.Eq)

_Integer = ()
_Float = ()
_String =  ()
_Char = ()

_primShowBool :: Bool -> Prelude.String
_primShowBool False = "False"
_primShowBool True = "True"

_primShowInteger :: Prelude.Integer -> Prelude.String
_primShowInteger = Prelude.show

_primIntZero :: Prelude.Integer
_primIntZero = (0::Prelude.Integer)

_primIntOne :: Prelude.Integer
_primIntOne = (1::Prelude.Integer)

_primIntAdd :: Prelude.Integer -> Prelude.Integer -> Prelude.Integer
_primIntAdd = (Prelude.+)

_primIntSub :: Prelude.Integer -> Prelude.Integer -> Prelude.Integer
_primIntSub = (Prelude.-)


_primIntMul :: Prelude.Integer -> Prelude.Integer -> Prelude.Integer
_primIntMul = (Prelude.*)

_primIntDiv :: Prelude.Integer -> Prelude.Integer -> Prelude.Integer
_primIntDiv = (Prelude.div)

_primIntMod :: Prelude.Integer -> Prelude.Integer -> Prelude.Integer
_primIntMod = (Prelude.mod)

_primIntEquality :: Prelude.Integer -> Prelude.Integer -> Prelude.Bool
_primIntEquality = (Prelude.==)

_primIntLess :: Prelude.Integer -> Prelude.Integer -> Prelude.Bool
_primIntLess = (Prelude.<)

_int = _primNatToInteger
_primNatToInteger Zero = (0::Prelude.Integer)
_primNatToInteger (Suc n) = ( _primIntAdd (1::Prelude.Integer)  ( (_primNatToInteger(cast n))))

_primIntegerAbs 0 = zero
_primIntegerAbs n | (Prelude.>) n (0 :: Prelude.Integer) = suc (cast (_primIntegerAbs (  _primIntSub n (1::Prelude.Integer))))
	| Prelude.otherwise = _primIntegerAbs (_primIntSub 0 n)
_abs = _primIntegerAbs

_primIntegerToNat n = _primIntegerAbs n

_primShowFloat :: Float -> Prelude.String
_primShowFloat f = Prelude.show f
-- _primShowFloat (FloatT f) = Prelude.show f

_primShowChar c = [ unboxChar c]

_primCharEquality c1 c2 = c1 == c2
_primIsLower = isLower . unboxChar
_primIsDigit = isDigit . unboxChar
_primIsAlpha = isAlpha . unboxChar
_primIsSpace = isSpace . unboxChar
_primIsAscii = isAscii . unboxChar
_primIsLatin1 = isLatin1 . unboxChar
_primIsPrint = isPrint . unboxChar
_primIsHexDigit = isHexDigit . unboxChar
_primToUpper = toUpper . unboxChar
_primToLower = toLower . unboxChar
_primCharToNat = CharT . chr
_primNatToChar = ord . unboxChar

_primStringAppend :: Prelude.String -> Prelude.String -> Prelude.String
_primStringAppend = (Prelude.++)

_primStringEquality :: Prelude.String -> Prelude.String -> Prelude.Bool
_primStringEquality = (Prelude.==)

_primShowString :: Prelude.String -> Prelude.String
_primShowString s = show s

_primStringReverse = Prelude.reverse
_primStringToList s = Prelude.map CharT s
_primStringFromList s = Prelude.map unboxChar s

_primNatPlus m n = _abs (_primIntAdd (_int m) (_int n))
_primNatMinus m n = _abs (_primIntSub (_int m) (_int n))
_primNatTimes m n = _abs (_primIntMul (_int m) (_int n))
_primNatDivSuc m n= _abs (_primIntDiv (_int m) (_int n))
_primNatModSuc m n = _abs (_primIntMod (_int m) (_int n))
_primNatLess m n = _primIntLess (_int m) (_int n)
_primNatEquality m n = _primIntEquality (_int m) (_int n)

-- For tests
zero = Zero
suc = Suc
one = suc zero
two = suc one