{-# LANGUAGE ApplicativeDo #-}
module Agda.TypeChecking.Primitive.Base where
import Control.Monad ( mzero )
import Control.Monad.Fail ( MonadFail )
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.Utils.Pretty ( prettyShow )
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') (String -> Type -> Abs Type
forall a. String -> a -> Abs a
NoAbs String
"_" Type
b')
gpi :: (MonadAddContext m, MonadDebug m)
=> ArgInfo -> String -> m Type -> m Type -> m Type
gpi :: forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgInfo -> String -> m Type -> m Type -> m Type
gpi ArgInfo
info String
name m Type
a m Type
b = do
Type
a <- m Type
a
let dom :: Dom Type
dom :: Dom Type
dom = ArgInfo -> String -> Type -> Dom Type
forall a. ArgInfo -> String -> a -> Dom a
defaultNamedArgDom ArgInfo
info String
name Type
a
Type
b <- (String, Dom Type) -> m Type -> m Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
name, Dom Type
dom) m Type
b
let y :: String
y = String -> String
stringToArgName String
name
Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f 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 (String -> Type -> Abs Type
forall a. String -> a -> Abs a
Abs String
y Type
b))
(Dom Type -> Abs Type -> Term
Pi Dom Type
dom (String -> Type -> Abs Type
forall a. String -> a -> Abs a
Abs String
y Type
b))
hPi, nPi :: (MonadAddContext m, MonadDebug m)
=> String -> m Type -> m Type -> m Type
hPi :: forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi = ArgInfo -> String -> m Type -> m Type -> m Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgInfo -> String -> m Type -> m Type -> m Type
gpi (ArgInfo -> String -> m Type -> m Type -> m Type)
-> ArgInfo -> String -> 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) =>
String -> m Type -> m Type -> m Type
nPi = ArgInfo -> String -> m Type -> m Type -> m Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgInfo -> String -> 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) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
s NamesT m Type
a NamesT m Term -> NamesT m Type
b = String -> NamesT m Type -> NamesT m Type -> NamesT m Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
s NamesT m Type
a (String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
-> NamesT m Type)
-> NamesT m Type
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' String
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) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
s NamesT m Type
a NamesT m Term -> NamesT m Type
b = String -> NamesT m Type -> NamesT m Type -> NamesT m Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
nPi String
s NamesT m Type
a (String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b)
-> NamesT m Type)
-> NamesT m Type
forall (m :: * -> *) a.
MonadFail m =>
String
-> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
-> NamesT m a
bind' String
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) =>
String
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' String
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
<$> String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
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
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinIsOne
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 :: Bool
domIsFinite = Bool
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
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 (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 :: 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
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
NoAbs String
"_"
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
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)
sSizeUniv :: Sort
sSizeUniv :: Sort' Term
sSizeUniv = Sort' Term
forall t. Sort' t
SizeUniv
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
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
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
lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
lookupPrimitiveFunction String
x =
TCM PrimitiveImpl -> Maybe (TCM PrimitiveImpl) -> TCM PrimitiveImpl
forall a. a -> Maybe a -> a
fromMaybe (do
String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
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
$ String -> TypeError
NoSuchPrimitiveFunction String
x)
(String
-> Map String (TCM PrimitiveImpl) -> Maybe (TCM PrimitiveImpl)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
x Map String (TCM PrimitiveImpl)
primitiveFunctions)
lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl)
lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl)
lookupPrimitiveFunctionQ QName
q = do
let s :: String
s = Name -> String
forall a. Pretty a => a -> String
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 <- String -> TCM PrimitiveImpl
lookupPrimitiveFunction String
s
(String, PrimitiveImpl) -> TCM (String, PrimitiveImpl)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
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 :: forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
String -> m (Maybe QName)
getBuiltinName String
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 (String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
b)
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 -> String -> m Bool
isBuiltin :: forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> String -> m Bool
isBuiltin QName
q String
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
<$> String -> m (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
String -> m (Maybe QName)
getBuiltinName String
b
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 -> String -> String
[SigmaKit] -> String -> String
SigmaKit -> String
(Int -> SigmaKit -> String -> String)
-> (SigmaKit -> String)
-> ([SigmaKit] -> String -> String)
-> Show SigmaKit
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> SigmaKit -> String -> String
showsPrec :: Int -> SigmaKit -> String -> String
$cshow :: SigmaKit -> String
show :: SigmaKit -> String
$cshowList :: [SigmaKit] -> String -> String
showList :: [SigmaKit] -> String -> String
Show)
getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)
getSigmaKit :: forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit = do
Maybe QName
ms <- String -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
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__