{-# LANGUAGE ApplicativeDo #-}

module Agda.TypeChecking.Primitive.Base where

import Control.Monad             ( mzero )
import Control.Monad.Fail        ( MonadFail )
  -- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Trans.Maybe ( MaybeT(..), runMaybeT )

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.Syntax.Common.Pretty ( prettyShow )

-- Type combinators

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

(-->), (.-->), (..-->) :: Applicative m => m Type -> m Type -> m Type
m Type
a --> :: forall (m :: * -> *). Applicative m => 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 .--> :: forall (m :: * -> *). Applicative m => 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 ..--> :: forall (m :: * -> *). Applicative m => 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 :: forall (m :: * -> *).
Applicative m =>
(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 :: forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
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
forall (m :: * -> *) a.
MonadAddContext m =>
(ArgName, Dom Type) -> m a -> m a
addContext (ArgName
name, Dom Type
dom) m Type
b
  let y :: ArgName
y = ArgName -> ArgName
stringToArgName ArgName
name
  return $ 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 :: forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
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 :: forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
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' :: forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
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
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m Type)
-> NamesT m Type
forall (m :: * -> *) a.
MonadFail m =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' ArgName
s (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> NamesT m Term -> NamesT m Type
b NamesT m Term
forall b. (Subst b, DeBruijn b) => NamesT m b
x))
nPi' :: forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
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
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
    -> NamesT m Type)
-> NamesT m Type
forall (m :: * -> *) a.
MonadFail m =>
ArgName
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' ArgName
s (\ forall b. (Subst b, DeBruijn b) => NamesT m b
x -> NamesT m Term -> NamesT m Type
b NamesT m Term
forall b. (Subst b, DeBruijn b) => NamesT m b
x))

pPi' :: (MonadAddContext m, HasBuiltins m, MonadDebug m)
     => String -> NamesT m Term -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
pPi' :: forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
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
   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
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinIsOne

-- | Turn a 'Pi' type into one whose domain is annotated finite, i.e.,
-- one that represents a @Partial@ element rather than an actual
-- function.
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 { domIsFinite = True })
  Abs Type
b
toFinitePi Type
_ = Type
forall a. HasCallStack => a
__IMPOSSIBLE__

el' :: Applicative m => m Term -> m Term -> m Type
el' :: forall (m :: * -> *). Applicative m => 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 a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Term
a

els :: Applicative m => m Sort -> m Term -> m Type
els :: forall (m :: * -> *).
Applicative m =>
m (Sort' Term) -> m Term -> m Type
els m (Sort' 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
<$> m (Sort' Term)
l m (Term -> Type) -> m Term -> m Type
forall a b. m (a -> b) -> m a -> m b
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 :: forall (m :: * -> *). Applicative m => 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 a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Term
a

elInf :: Functor m => m Term -> m Type
elInf :: forall (m :: * -> *). Functor m => m Term -> m Type
elInf m Term
t = (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
UType 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 :: forall (m :: * -> *). Functor m => 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 :: forall (m :: * -> *). Applicative m => Int -> m Term
varM = Term -> m Term
forall a. a -> m a
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 :: forall (m :: * -> *).
Applicative m =>
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' :: forall (m :: * -> *).
Applicative m =>
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
<@> :: forall (m :: * -> *). Applicative m => 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
<#> :: forall (m :: * -> *). Applicative m => 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
<..> :: forall (m :: * -> *). Applicative m => 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 <@@> :: forall (m :: * -> *).
Applicative m =>
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 :: forall (m :: * -> *). Functor m => 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

-- | The universe @Set0@ as a type.
tset :: Applicative m => m Type
tset :: forall (m :: * -> *). Applicative m => m Type
tset = Type -> m Type
forall a. a -> m a
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)

-- | @SizeUniv@ as a sort.
sSizeUniv :: Sort
sSizeUniv :: Sort' Term
sSizeUniv = Sort' Term
forall t. Sort' t
SizeUniv

-- | @SizeUniv@ as a type.
tSizeUniv :: Applicative m => m Type
tSizeUniv :: forall (m :: * -> *). Applicative m => m Type
tSizeUniv = Type -> m Type
forall a. a -> m a
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

tLevelUniv :: Applicative m => m Type
tLevelUniv :: forall (m :: * -> *). Applicative m => m Type
tLevelUniv = Type -> m Type
forall a. a -> m a
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 -> Type) -> Sort' Term -> Type
forall a b. (a -> b) -> a -> b
$ Sort' Term
forall t. Sort' t
LevelUniv

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

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

-- | Abbreviation: @argH = 'hide' 'Arg' 'defaultArgInfo'@.
argH :: e -> Arg e
argH :: forall e. 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 :: forall a. a -> Dom a
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 :: PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction :: PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
x =
  TCM PrimitiveImpl -> Maybe (TCM PrimitiveImpl) -> TCM PrimitiveImpl
forall a. a -> Maybe a -> a
fromMaybe (do
                ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.prim" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Lookup of primitive function" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> PrimitiveId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty PrimitiveId
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO 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 (PrimitiveId -> ArgName
forall a. IsBuiltin a => a -> ArgName
getBuiltinId PrimitiveId
x))
            (PrimitiveId
-> Map PrimitiveId (TCM PrimitiveImpl) -> Maybe (TCM PrimitiveImpl)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimitiveId
x Map PrimitiveId (TCM PrimitiveImpl)
primitiveFunctions)

lookupPrimitiveFunctionQ :: QName -> TCM (PrimitiveId, PrimitiveImpl)
lookupPrimitiveFunctionQ :: QName -> TCM (PrimitiveId, 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)
  case ArgName -> Maybe PrimitiveId
primitiveById ArgName
s of
    Maybe PrimitiveId
Nothing -> TypeError -> TCM (PrimitiveId, PrimitiveImpl)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM (PrimitiveId, PrimitiveImpl))
-> TypeError -> TCM (PrimitiveId, PrimitiveImpl)
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
NoSuchPrimitiveFunction ArgName
s
    Just PrimitiveId
s -> do
      PrimImpl Type
t PrimFun
pf <- PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
s
      (PrimitiveId, PrimitiveImpl) -> TCM (PrimitiveId, PrimitiveImpl)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveId
s, Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ PrimFun
pf { primFunName = q })

getBuiltinName :: (HasBuiltins m, MonadReduce m) => BuiltinId -> m (Maybe QName)
getBuiltinName :: forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
b = MaybeT m QName -> m (Maybe QName)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m QName -> m (Maybe QName))
-> MaybeT m QName -> m (Maybe QName)
forall a b. (a -> b) -> a -> b
$ Term -> MaybeT m QName
forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
getQNameFromTerm (Term -> MaybeT m QName) -> MaybeT m Term -> MaybeT m QName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (Maybe Term) -> MaybeT m Term
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
b)

-- | Convert a name in 'Term' form back to 'QName'.
--
getQNameFromTerm :: MonadReduce m => Term -> MaybeT m QName
getQNameFromTerm :: forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
getQNameFromTerm Term
v = do
    Term
v <- Term -> MaybeT m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
    case Term -> Term
unSpine Term
v of
      Def QName
x Elims
_   -> QName -> MaybeT m QName
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
      Con ConHead
x ConInfo
_ Elims
_ -> QName -> MaybeT m QName
forall a. a -> MaybeT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> MaybeT m QName) -> QName -> MaybeT m QName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
x
      Lam ArgInfo
_ Abs Term
b   -> Term -> MaybeT m QName
forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
getQNameFromTerm (Term -> MaybeT m QName) -> Term -> MaybeT m QName
forall a b. (a -> b) -> a -> b
$ Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b
      Term
_ -> MaybeT m QName
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

isBuiltin :: (HasBuiltins m, MonadReduce m) => QName -> BuiltinId -> m Bool
isBuiltin :: forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> BuiltinId -> m Bool
isBuiltin QName
q BuiltinId
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
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
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
$c== :: SigmaKit -> SigmaKit -> Bool
== :: SigmaKit -> SigmaKit -> Bool
$c/= :: SigmaKit -> SigmaKit -> Bool
/= :: 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
$cshowsPrec :: Int -> SigmaKit -> ArgName -> ArgName
showsPrec :: Int -> SigmaKit -> ArgName -> ArgName
$cshow :: SigmaKit -> ArgName
show :: SigmaKit -> ArgName
$cshowList :: [SigmaKit] -> ArgName -> ArgName
showList :: [SigmaKit] -> ArgName -> ArgName
Show)

getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)
getSigmaKit :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit = do
  Maybe QName
ms <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinSigma
  case Maybe QName
ms of
    Maybe QName
Nothing -> Maybe SigmaKit -> m (Maybe SigmaKit)
forall a. a -> m a
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 a. a -> m a
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
            { 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__  -- This invariant is ensured in bindBuiltinSigma