module Agda.Compiler.UHC.Primitives
( primFunNm
, primFunctions
)
where
import Agda.Compiler.UHC.CompileState
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import qualified Agda.Syntax.Internal as T
import Control.Monad.Trans
#include "undefined.h"
import Agda.Utils.Impossible
#if __GLASGOW_HASKELL__ <= 708
import Control.Applicative
#endif
import qualified Data.Map as M
import Data.Maybe
import Agda.Compiler.UHC.Bridge
primFunNm :: String -> HsName
primFunNm = mkHsName ["UHC", "Agda", "Builtins"]
primFunctions :: M.Map String ((CompileT TCM) CExpr)
primFunctions = M.fromList $
[(n, return $ mkVar (primFunNm n)) | n <-
[
"primLevelMax"
, "primLevelZero"
, "primLevelSuc"
, "primShowInteger"
, "primNatPlus"
, "primNatTimes"
, "primNatMinus"
, "primNatDivSuc"
, "primNatDivSucAux"
, "primNatModSuc"
, "primNatModSucAux"
, "primNatToInteger"
, "primNatEquality"
, "primNatLess"
, "primIntegerToNat"
, "primStringAppend"
, "primStringEquality"
, "primStringFromList"
, "primStringToList"
, "primShowString"
, "primCharToNat"
, "primCharEquality"
, "primShowChar"
, "primIsLower"
, "primIsDigit"
, "primIsAlpha"
, "primIsSpace"
, "primIsAscii"
, "primIsLatin1"
, "primIsPrint"
, "primIsHexDigit"
, "primToUpper"
, "primToLower"
, "primNatToChar"
, "primShowFloat"
, "primFloatEquality"
, "primFloatLess"
, "primNatToFloat"
, "primFloatPlus"
, "primFloatMinus"
, "primFloatTimes"
, "primFloatDiv"
, "primFloatSqrt"
, "primRound"
, "primFloor"
, "primCeiling"
, "primExp"
, "primLog"
, "primSin"
, "primQNameEquality"
, "primQNameLess"
, "primShowQName"
, "primMetaEquality"
, "primMetaLess"
, "primShowMeta"
]
] ++ [
("primTrustMe", mkTrustMe)
]
where mkTrustMe = do
bt <- fromMaybe __IMPOSSIBLE__ <$> (lift $ getBuiltin' builtinRefl)
let reflNm = case T.ignoreSharing bt of
(T.Con conHd []) -> T.conName conHd
_ -> __IMPOSSIBLE__
mkVar <$> getConstrFun reflNm