{-# LANGUAGE ApplicativeDo #-}

module Agda.TypeChecking.Primitive.Base where

-- Control.Monad.Fail import is redundant since GHC 8.8.1
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.Pretty
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 )

-- Type combinators

infixr 4 -->
infixr 4 .-->
infixr 4 ..-->

(-->), (.-->), (..-->) :: Applicative m => m Type -> m Type -> m Type
m Type
a --> :: m Type -> m Type -> m Type
--> m Type
b = (Relevance -> Relevance) -> m Type -> m Type -> m Type
forall (m :: * -> *).
Applicative m =>
(Relevance -> Relevance) -> m Type -> m Type -> m Type
garr Relevance -> Relevance
forall a. a -> a
id m Type
a m Type
b
m Type
a .--> :: m Type -> m Type -> m Type
.--> m Type
b = (Relevance -> Relevance) -> m Type -> m Type -> m Type
forall (m :: * -> *).
Applicative m =>
(Relevance -> Relevance) -> m Type -> m Type -> m Type
garr (Relevance -> Relevance -> Relevance
forall a b. a -> b -> a
const (Relevance -> Relevance -> Relevance)
-> Relevance -> Relevance -> Relevance
forall a b. (a -> b) -> a -> b
$ Relevance
Irrelevant) m Type
a m Type
b
m Type
a ..--> :: m Type -> m Type -> m Type
..--> m Type
b = (Relevance -> Relevance) -> m Type -> m Type -> m Type
forall (m :: * -> *).
Applicative m =>
(Relevance -> Relevance) -> m Type -> m Type -> m Type
garr (Relevance -> Relevance -> Relevance
forall a b. a -> b -> a
const (Relevance -> Relevance -> Relevance)
-> Relevance -> Relevance -> Relevance
forall a b. (a -> b) -> a -> b
$ Relevance
NonStrict) m Type
a m Type
b

garr :: Applicative m => (Relevance -> Relevance) -> m Type -> m Type -> m Type
garr :: (Relevance -> Relevance) -> m Type -> m Type -> m Type
garr Relevance -> Relevance
f m Type
a m Type
b = do
  Type
a' <- m Type
a
  Type
b' <- m Type
b
  pure $ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort' Term -> Sort' Term -> Sort' Term
funSort (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
a') (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
b')) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$
    Dom Type -> Abs Type -> Term
Pi ((Relevance -> Relevance) -> Dom Type -> Dom Type
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
f (Dom Type -> Dom Type) -> Dom Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
a') (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
NoAbs ArgName
"_" Type
b')

gpi :: (MonadAddContext m, MonadDebug m)
    => ArgInfo -> String -> m Type -> m Type -> m Type
gpi :: ArgInfo -> ArgName -> m Type -> m Type -> m Type
gpi ArgInfo
info ArgName
name m Type
a m Type
b = do
  Type
a <- m Type
a
  let dom :: Dom Type
      dom :: Dom Type
dom = ArgInfo -> ArgName -> Type -> Dom Type
forall a. ArgInfo -> ArgName -> a -> Dom a
defaultNamedArgDom ArgInfo
info ArgName
name Type
a
  Type
b <- (ArgName, Dom Type) -> m Type -> m Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (ArgName
name, Dom Type
dom) m Type
b
  let y :: ArgName
y = ArgName -> ArgName
stringToArgName ArgName
name
  Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Dom Type -> Abs Type -> Sort' Term
mkPiSort Dom Type
dom (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
y Type
b))
              (Dom Type -> Abs Type -> Term
Pi Dom Type
dom (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
y Type
b))

hPi, nPi :: (MonadAddContext m, MonadDebug m)
         => String -> m Type -> m Type -> m Type
hPi :: ArgName -> m Type -> m Type -> m Type
hPi = ArgInfo -> ArgName -> m Type -> m Type -> m Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgInfo -> ArgName -> m Type -> m Type -> m Type
gpi (ArgInfo -> ArgName -> m Type -> m Type -> m Type)
-> ArgInfo -> ArgName -> m Type -> m Type -> m Type
forall a b. (a -> b) -> a -> b
$ Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo
nPi :: ArgName -> m Type -> m Type -> m Type
nPi = ArgInfo -> ArgName -> m Type -> m Type -> m Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgInfo -> ArgName -> m Type -> m Type -> m Type
gpi ArgInfo
defaultArgInfo

hPi', nPi' :: (MonadFail m, MonadAddContext m, MonadDebug m)
           => String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
hPi' :: ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' ArgName
s NamesT m Type
a NamesT m Term -> NamesT m Type
b = ArgName -> NamesT m Type -> NamesT m Type -> NamesT m Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
s NamesT m Type
a (ArgName -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
ArgName -> (NamesT m b -> NamesT m a) -> NamesT m a
bind' ArgName
s NamesT m Term -> NamesT m Type
b)
nPi' :: ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
s NamesT m Type
a NamesT m Term -> NamesT m Type
b = ArgName -> NamesT m Type -> NamesT m Type -> NamesT m Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
nPi ArgName
s NamesT m Type
a (ArgName -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
ArgName -> (NamesT m b -> NamesT m a) -> NamesT m a
bind' ArgName
s NamesT m Term -> NamesT m Type
b)

pPi' :: (MonadAddContext m, HasBuiltins m, MonadDebug m)
     => String -> NamesT m Term -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
pPi' :: ArgName
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' ArgName
n NamesT m Term
phi NamesT m Term -> NamesT m Type
b = Type -> Type
toFinitePi (Type -> Type) -> NamesT m Type -> NamesT m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
n (NamesT m Term -> NamesT m Type
forall (m :: * -> *). Functor m => m Term -> m Type
elSSet (NamesT m Term -> NamesT m Type) -> NamesT m Term -> NamesT m Type
forall a b. (a -> b) -> a -> b
$ m Term -> NamesT m Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl m Term
isOne NamesT m Term -> NamesT m Term -> NamesT m Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
phi) NamesT m Term -> NamesT m Type
b
 where
   toFinitePi :: Type -> Type
   toFinitePi :: Type -> Type
toFinitePi (El Sort' Term
s (Pi Dom Type
d Abs Type
b)) = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi (Relevance -> Dom Type -> Dom Type
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant (Dom Type -> Dom Type) -> Dom Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Dom Type
d { domFinite :: Bool
domFinite = Bool
True }) Abs Type
b
   toFinitePi Type
_               = Type
forall a. HasCallStack => a
__IMPOSSIBLE__

   isOne :: m Term
isOne = Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getBuiltin' ArgName
builtinIsOne

el' :: Applicative m => m Term -> m Term -> m Type
el' :: m Term -> m Term -> m Type
el' m Term
l m Term
a = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort' Term -> Term -> Type) -> m (Sort' Term) -> m (Term -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Sort' Term
tmSort (Term -> Sort' Term) -> m Term -> m (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
l) m (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Term
a

el's :: Applicative m => m Term -> m Term -> m Type
el's :: m Term -> m Term -> m Type
el's m Term
l m Term
a = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort' Term -> Term -> Type) -> m (Sort' Term) -> m (Term -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
SSet (Level' Term -> Sort' Term)
-> (Term -> Level' Term) -> Term -> Sort' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Level' Term
forall t. t -> Level' t
atomicLevel (Term -> Sort' Term) -> m Term -> m (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
l) m (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Term
a

elInf :: Functor m => m Term -> m Type
elInf :: m Term -> m Type
elInf m Term
t = (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (IsFibrant -> Integer -> Sort' Term
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
0) (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
t)

elSSet :: Functor m => m Term -> m Type
elSSet :: m Term -> m Type
elSSet m Term
t = (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
SSet (Level' Term -> Sort' Term) -> Level' Term -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level' Term
ClosedLevel Integer
0) (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
t)

nolam :: Term -> Term
nolam :: Term -> Term
nolam = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
NoAbs ArgName
"_"

varM :: Applicative m => Int -> m Term
varM :: Int -> m Term
varM = Term -> m Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> m Term) -> (Int -> Term) -> Int -> m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var

infixl 9 <@>, <#>

gApply :: Applicative m => Hiding -> m Term -> m Term -> m Term
gApply :: Hiding -> m Term -> m Term -> m Term
gApply Hiding
h m Term
a m Term
b = ArgInfo -> m Term -> m Term -> m Term
forall (m :: * -> *).
Applicative m =>
ArgInfo -> m Term -> m Term -> m Term
gApply' (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h ArgInfo
defaultArgInfo) m Term
a m Term
b

gApply' :: Applicative m => ArgInfo -> m Term -> m Term -> m Term
gApply' :: ArgInfo -> m Term -> m Term -> m Term
gApply' ArgInfo
info m Term
a m Term
b = do
    Term
x <- m Term
a
    Term
y <- m Term
b
    pure $ Term
x Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
y]

(<@>),(<#>),(<..>) :: Applicative m => m Term -> m Term -> m Term
<@> :: m Term -> m Term -> m Term
(<@>) = Hiding -> m Term -> m Term -> m Term
forall (m :: * -> *).
Applicative m =>
Hiding -> m Term -> m Term -> m Term
gApply Hiding
NotHidden
<#> :: m Term -> m Term -> m Term
(<#>) = Hiding -> m Term -> m Term -> m Term
forall (m :: * -> *).
Applicative m =>
Hiding -> m Term -> m Term -> m Term
gApply Hiding
Hidden
<..> :: m Term -> m Term -> m Term
(<..>) = ArgInfo -> m Term -> m Term -> m Term
forall (m :: * -> *).
Applicative m =>
ArgInfo -> m Term -> m Term -> m Term
gApply' (Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo)

(<@@>) :: Applicative m => m Term -> (m Term,m Term,m Term) -> m Term
m Term
t <@@> :: m Term -> (m Term, m Term, m Term) -> m Term
<@@> (m Term
x,m Term
y,m Term
r) = do
  Term
t <- m Term
t
  Term
x <- m Term
x
  Term
y <- m Term
y
  Term
r <- m Term
r
  pure $ Term
t Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply Term
x Term
y Term
r]

list :: TCM Term -> TCM Term
list :: TCM Term -> TCM Term
list TCM Term
t = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primList TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term
t

tMaybe :: TCM Term -> TCM Term
tMaybe :: TCM Term -> TCM Term
tMaybe TCM Term
t = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primMaybe TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term
t

io :: TCM Term -> TCM Term
io :: TCM Term -> TCM Term
io TCM Term
t = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIO TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term
t

path :: TCM Term -> TCM Term
path :: TCM Term -> TCM Term
path TCM Term
t = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term
t

el :: Functor m => m Term -> m Type
el :: m Term -> m Type
el m Term
t = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort' Term
mkType Integer
0) (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
t

tset :: Applicative m => m Type
tset :: m Type
tset = Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkType Integer
0)

sSizeUniv :: Sort
-- sSizeUniv = mkType 0
-- Andreas, 2016-04-14 switching off SizeUniv, unfixing issue #1428
sSizeUniv :: Sort' Term
sSizeUniv = Sort' Term
forall t. Sort' t
SizeUniv

tSizeUniv :: Applicative m => m Type
-- tSizeUniv = tset
-- Andreas, 2016-04-14 switching off SizeUniv, unfixing issue #1428
-- tSizeUniv = return $ El sSizeUniv $ Sort sSizeUniv
-- Andreas, 2015-03-16 Since equality checking for types
-- includes equality checking for sorts, we cannot put
-- SizeUniv in Setω.  (SizeUniv : Setω) == (_0 : suc _0)
-- will first instantiate _0 := Setω, which is wrong.
tSizeUniv :: m Type
tSizeUniv = Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort Sort' Term
sSizeUniv

-- | Abbreviation: @argN = 'Arg' 'defaultArgInfo'@.
argN :: e -> Arg e
argN :: e -> Arg e
argN = ArgInfo -> e -> Arg e
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo

domN :: e -> Dom e
domN :: e -> Dom e
domN = e -> Dom e
forall a. a -> Dom a
defaultDom

-- | Abbreviation: @argH = 'hide' 'Arg' 'defaultArgInfo'@.
argH :: e -> Arg e
argH :: e -> Arg e
argH = ArgInfo -> e -> Arg e
forall e. ArgInfo -> e -> Arg e
Arg (ArgInfo -> e -> Arg e) -> ArgInfo -> e -> Arg e
forall a b. (a -> b) -> a -> b
$ Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo

domH :: e -> Dom e
domH :: e -> Dom e
domH = Hiding -> Dom e -> Dom e
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden (Dom e -> Dom e) -> (e -> Dom e) -> e -> Dom e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Dom e
forall a. a -> Dom a
defaultDom

---------------------------------------------------------------------------
-- * Accessing the primitive functions
---------------------------------------------------------------------------

lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
lookupPrimitiveFunction :: ArgName -> TCM PrimitiveImpl
lookupPrimitiveFunction ArgName
x =
  TCM PrimitiveImpl -> Maybe (TCM PrimitiveImpl) -> TCM PrimitiveImpl
forall a. a -> Maybe a -> a
fromMaybe (do
                ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.prim" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Lookup of primitive function" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"failed"
                TypeError -> TCM PrimitiveImpl
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM PrimitiveImpl) -> TypeError -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
NoSuchPrimitiveFunction ArgName
x)
            (ArgName
-> Map ArgName (TCM PrimitiveImpl) -> Maybe (TCM PrimitiveImpl)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ArgName
x Map ArgName (TCM PrimitiveImpl)
primitiveFunctions)

lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl)
lookupPrimitiveFunctionQ :: QName -> TCM (ArgName, PrimitiveImpl)
lookupPrimitiveFunctionQ QName
q = do
  let s :: ArgName
s = Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Name -> Name
nameCanonical (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q)
  PrimImpl Type
t PrimFun
pf <- ArgName -> TCM PrimitiveImpl
lookupPrimitiveFunction ArgName
s
  (ArgName, PrimitiveImpl) -> TCM (ArgName, PrimitiveImpl)
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgName
s, Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ PrimFun
pf { primFunName :: QName
primFunName = QName
q })

getBuiltinName :: (HasBuiltins m, MonadReduce m) => String -> m (Maybe QName)
getBuiltinName :: ArgName -> m (Maybe QName)
getBuiltinName ArgName
b = do
  m (Maybe Term)
-> m (Maybe QName) -> (Term -> m (Maybe QName)) -> m (Maybe QName)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ArgName -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getBuiltin' ArgName
b) (Maybe QName -> m (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing) (QName -> Maybe QName
forall a. a -> Maybe a
Just (QName -> Maybe QName)
-> (Term -> m QName) -> Term -> m (Maybe QName)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Term -> m QName
forall (m :: * -> *). MonadReduce m => Term -> m QName
getName)
  where
  getName :: Term -> m QName
getName Term
v = do
    Term
v <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
    case Term -> Term
unSpine (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
v of
      Def QName
x Elims
_   -> QName -> m QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
      Con ConHead
x ConInfo
_ Elims
_ -> QName -> m QName
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> m QName) -> QName -> m QName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
x
      Lam ArgInfo
_ Abs Term
b   -> Term -> m QName
getName (Term -> m QName) -> Term -> m QName
forall a b. (a -> b) -> a -> b
$ Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b
      Term
_ -> m QName
forall a. HasCallStack => a
__IMPOSSIBLE__

isBuiltin :: (HasBuiltins m, MonadReduce m) => QName -> String -> m Bool
isBuiltin :: QName -> ArgName -> m Bool
isBuiltin QName
q ArgName
b = (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe QName -> Bool) -> m (Maybe QName) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
ArgName -> m (Maybe QName)
getBuiltinName ArgName
b

------------------------------------------------------------------------
-- * Builtin Sigma
------------------------------------------------------------------------

data SigmaKit = SigmaKit
  { SigmaKit -> QName
sigmaName :: QName
  , SigmaKit -> ConHead
sigmaCon  :: ConHead
  , SigmaKit -> QName
sigmaFst  :: QName
  , SigmaKit -> QName
sigmaSnd  :: QName
  }
  deriving (SigmaKit -> SigmaKit -> Bool
(SigmaKit -> SigmaKit -> Bool)
-> (SigmaKit -> SigmaKit -> Bool) -> Eq SigmaKit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SigmaKit -> SigmaKit -> Bool
$c/= :: SigmaKit -> SigmaKit -> Bool
== :: SigmaKit -> SigmaKit -> Bool
$c== :: SigmaKit -> SigmaKit -> Bool
Eq,Int -> SigmaKit -> ArgName -> ArgName
[SigmaKit] -> ArgName -> ArgName
SigmaKit -> ArgName
(Int -> SigmaKit -> ArgName -> ArgName)
-> (SigmaKit -> ArgName)
-> ([SigmaKit] -> ArgName -> ArgName)
-> Show SigmaKit
forall a.
(Int -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
showList :: [SigmaKit] -> ArgName -> ArgName
$cshowList :: [SigmaKit] -> ArgName -> ArgName
show :: SigmaKit -> ArgName
$cshow :: SigmaKit -> ArgName
showsPrec :: Int -> SigmaKit -> ArgName -> ArgName
$cshowsPrec :: Int -> SigmaKit -> ArgName -> ArgName
Show)

getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)
getSigmaKit :: m (Maybe SigmaKit)
getSigmaKit = do
  Maybe QName
ms <- ArgName -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe QName)
getBuiltinName' ArgName
builtinSigma
  case Maybe QName
ms of
    Maybe QName
Nothing -> Maybe SigmaKit -> m (Maybe SigmaKit)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SigmaKit
forall a. Maybe a
Nothing
    Just QName
sigma -> do
      Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
sigma
      case Defn
def of
        Record { recFields :: Defn -> [Dom QName]
recFields = [Dom QName
fst,Dom QName
snd], recConHead :: Defn -> ConHead
recConHead = ConHead
con } -> do
          Maybe SigmaKit -> m (Maybe SigmaKit)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe SigmaKit -> m (Maybe SigmaKit))
-> (SigmaKit -> Maybe SigmaKit) -> SigmaKit -> m (Maybe SigmaKit)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigmaKit -> Maybe SigmaKit
forall a. a -> Maybe a
Just (SigmaKit -> m (Maybe SigmaKit)) -> SigmaKit -> m (Maybe SigmaKit)
forall a b. (a -> b) -> a -> b
$ SigmaKit :: QName -> ConHead -> QName -> QName -> SigmaKit
SigmaKit
            { sigmaName :: QName
sigmaName = QName
sigma
            , sigmaCon :: ConHead
sigmaCon  = ConHead
con
            , sigmaFst :: QName
sigmaFst  = Dom QName -> QName
forall t e. Dom' t e -> e
unDom Dom QName
fst
            , sigmaSnd :: QName
sigmaSnd  = Dom QName -> QName
forall t e. Dom' t e -> e
unDom Dom QName
snd
            }
        Defn
_ -> m (Maybe SigmaKit)
forall a. HasCallStack => a
__IMPOSSIBLE__