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 )

-- Type combinators

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

(-->), (.-->), (..-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type
tcm Type
a --> :: tcm Type -> tcm Type -> tcm Type
--> tcm Type
b = (Relevance -> Relevance) -> tcm Type -> tcm Type -> tcm Type
forall (m :: * -> *).
Monad m =>
(Relevance -> Relevance) -> m Type -> m Type -> m Type
garr Relevance -> Relevance
forall a. a -> a
id tcm Type
a tcm Type
b
tcm Type
a .--> :: tcm Type -> tcm Type -> tcm Type
.--> tcm Type
b = (Relevance -> Relevance) -> tcm Type -> tcm Type -> tcm Type
forall (m :: * -> *).
Monad 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) tcm Type
a tcm Type
b
tcm Type
a ..--> :: tcm Type -> tcm Type -> tcm Type
..--> tcm Type
b = (Relevance -> Relevance) -> tcm Type -> tcm Type -> tcm Type
forall (m :: * -> *).
Monad 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) tcm Type
a tcm Type
b

garr :: Monad 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
  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 (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 (Sort' Term) -> Sort' Term
piSort Dom Type
dom (ArgName -> Sort' Term -> Abs (Sort' Term)
forall a. ArgName -> a -> Abs a
Abs ArgName
y (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort 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 :: * -> *) t' b t a.
(MonadFail m, Subst t' b, DeBruijn b, Subst t 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 :: * -> *) t' b t a.
(MonadFail m, Subst t' b, DeBruijn b, Subst t 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
elInf (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 (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm 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' :: Monad 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

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 Sort' Term
forall t. Sort' t
Inf (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 :: Monad tcm => Int -> tcm Term
varM :: Int -> tcm Term
varM = Term -> tcm Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> tcm Term) -> (Int -> Term) -> Int -> tcm Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var

infixl 9 <@>, <#>

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

gApply' :: Monad tcm => ArgInfo -> tcm Term -> tcm Term -> tcm Term
gApply' :: ArgInfo -> tcm Term -> tcm Term -> tcm Term
gApply' ArgInfo
info tcm Term
a tcm Term
b = do
    Term
x <- tcm Term
a
    Term
y <- tcm Term
b
    Term -> tcm Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> tcm Term) -> Term -> tcm Term
forall a b. (a -> b) -> a -> b
$ 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]

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

(<@@>) :: Monad tcm => tcm Term -> (tcm Term,tcm Term,tcm Term) -> tcm Term
tcm Term
t <@@> :: tcm Term -> (tcm Term, tcm Term, tcm Term) -> tcm Term
<@@> (tcm Term
x,tcm Term
y,tcm Term
r) = do
  Term
t <- tcm Term
t
  Term
x <- tcm Term
x
  Term
y <- tcm Term
y
  Term
r <- tcm Term
r
  Term -> tcm Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> tcm Term) -> Term -> tcm Term
forall a b. (a -> b) -> a -> b
$ 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 (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm 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 (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm 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 (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> TCM Term
t

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

tset :: Monad tcm => tcm Type
tset :: tcm Type
tset = Type -> tcm Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> tcm Type) -> Type -> tcm Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkType Integer
0)

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

tSizeUniv :: Monad tcm => tcm Type
tSizeUniv :: tcm Type
tSizeUniv = tcm Type
forall (tcm :: * -> *). Monad tcm => tcm Type
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 = return $ El Inf $ Sort SizeUniv

-- | 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 (TypeError -> TCM PrimitiveImpl
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 = case QName -> Name
qnameName QName
q of
            Name NameId
_ Name
x Range
_ Fixity'
_ Bool
_ -> Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow Name
x
  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 :: String -> TCM (Maybe QName)
getBuiltinName :: ArgName -> TCM (Maybe QName)
getBuiltinName ArgName
b = do
  TCMT IO (Maybe Term)
-> TCM (Maybe QName)
-> (Term -> TCM (Maybe QName))
-> TCM (Maybe QName)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ArgName -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getBuiltin' ArgName
b) (Maybe QName -> TCM (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 -> TCMT IO QName) -> Term -> TCM (Maybe QName)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Term -> TCMT IO 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 :: QName -> String -> TCM Bool
isBuiltin :: QName -> ArgName -> TCM 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) -> TCM (Maybe QName) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCM (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__