module Agda.TypeChecking.Primitive.Base where
import Control.Monad.Fail (MonadFail)
import qualified Data.Map as Map
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Names
import {-# SOURCE #-} Agda.TypeChecking.Primitive
import Agda.TypeChecking.Reduce ( reduce )
import Agda.TypeChecking.Monad.Signature
import Agda.TypeChecking.Substitute
import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.Maybe
import Agda.Utils.Pretty ( prettyShow )
infixr 4 -->
infixr 4 .-->
infixr 4 ..-->
(-->), (.-->), (..-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type
a --> b = garr id a b
a .--> b = garr (const $ Irrelevant) a b
a ..--> b = garr (const $ NonStrict) a b
garr :: Monad m => (Relevance -> Relevance) -> m Type -> m Type -> m Type
garr f a b = do
a' <- a
b' <- b
return $ El (funSort (defaultDom a') (getSort b')) $
Pi (mapRelevance f $ defaultDom a') (NoAbs "_" b')
gpi :: (MonadAddContext m, MonadDebug m)
=> ArgInfo -> String -> m Type -> m Type -> m Type
gpi info name a b = do
a <- a
let dom :: Dom Type
dom = defaultNamedArgDom info name a
b <- addContext (name, dom) b
let y = stringToArgName name
return $ El (piSort dom (Abs y (getSort b)))
(Pi dom (Abs y b))
hPi, nPi :: (MonadAddContext m, MonadDebug m)
=> String -> m Type -> m Type -> m Type
hPi = gpi $ setHiding Hidden defaultArgInfo
nPi = gpi defaultArgInfo
hPi', nPi' :: (MonadFail m, MonadAddContext m, MonadDebug m)
=> String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
hPi' s a b = hPi s a (bind' s b)
nPi' s a b = nPi s a (bind' s b)
pPi' :: (MonadAddContext m, HasBuiltins m, MonadDebug m)
=> String -> NamesT m Term -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
pPi' n phi b = toFinitePi <$> nPi' n (elInf $ cl isOne <@> phi) b
where
toFinitePi :: Type -> Type
toFinitePi (El s (Pi d b)) = El s $ Pi (setRelevance Irrelevant $ d { domFinite = True }) b
toFinitePi _ = __IMPOSSIBLE__
isOne = fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIsOne
el' :: Monad m => m Term -> m Term -> m Type
el' l a = El <$> (tmSort <$> l) <*> a
elInf :: Functor m => m Term -> m Type
elInf t = (El Inf <$> t)
nolam :: Term -> Term
nolam = Lam defaultArgInfo . NoAbs "_"
varM :: Monad tcm => Int -> tcm Term
varM = return . var
infixl 9 <@>, <#>
gApply :: Monad tcm => Hiding -> tcm Term -> tcm Term -> tcm Term
gApply h a b = gApply' (setHiding h defaultArgInfo) a b
gApply' :: Monad tcm => ArgInfo -> tcm Term -> tcm Term -> tcm Term
gApply' info a b = do
x <- a
y <- b
return $ x `apply` [Arg info y]
(<@>),(<#>),(<..>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term
(<@>) = gApply NotHidden
(<#>) = gApply Hidden
(<..>) = gApply' (setRelevance Irrelevant defaultArgInfo)
(<@@>) :: Monad tcm => tcm Term -> (tcm Term,tcm Term,tcm Term) -> tcm Term
t <@@> (x,y,r) = do
t <- t
x <- x
y <- y
r <- r
return $ t `applyE` [IApply x y r]
list :: TCM Term -> TCM Term
list t = primList <@> t
io :: TCM Term -> TCM Term
io t = primIO <@> t
path :: TCM Term -> TCM Term
path t = primPath <@> t
el :: Functor tcm => tcm Term -> tcm Type
el t = El (mkType 0) <$> t
tset :: Monad tcm => tcm Type
tset = return $ sort (mkType 0)
sSizeUniv :: Sort
sSizeUniv = mkType 0
tSizeUniv :: Monad tcm => tcm Type
tSizeUniv = tset
argN :: e -> Arg e
argN = Arg defaultArgInfo
domN :: e -> Dom e
domN = defaultDom
argH :: e -> Arg e
argH = Arg $ setHiding Hidden defaultArgInfo
domH :: e -> Dom e
domH = setHiding Hidden . defaultDom
lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
lookupPrimitiveFunction x =
fromMaybe (typeError $ NoSuchPrimitiveFunction x)
(Map.lookup x primitiveFunctions)
lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl)
lookupPrimitiveFunctionQ q = do
let s = case qnameName q of
Name _ x _ _ _ -> prettyShow x
PrimImpl t pf <- lookupPrimitiveFunction s
return (s, PrimImpl t $ pf { primFunName = q })
getBuiltinName :: String -> TCM (Maybe QName)
getBuiltinName b = do
caseMaybeM (getBuiltin' b) (return Nothing) (Just <.> getName)
where
getName v = do
v <- reduce v
case unSpine $ v of
Def x _ -> return x
Con x _ _ -> return $ conName x
Lam _ b -> getName $ unAbs b
_ -> __IMPOSSIBLE__
isBuiltin :: QName -> String -> TCM Bool
isBuiltin q b = (Just q ==) <$> getBuiltinName b
data SigmaKit = SigmaKit
{ sigmaName :: QName
, sigmaCon :: ConHead
, sigmaFst :: QName
, sigmaSnd :: QName
}
deriving (Eq,Show)
getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)
getSigmaKit = do
ms <- getBuiltinName' builtinSigma
case ms of
Nothing -> return Nothing
Just sigma -> do
def <- theDef <$> getConstInfo sigma
case def of
Record { recFields = [fst,snd], recConHead = con } -> do
return . Just $ SigmaKit
{ sigmaName = sigma
, sigmaCon = con
, sigmaFst = unDom fst
, sigmaSnd = unDom snd
}
_ -> __IMPOSSIBLE__