{-# 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.Utils.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 = forall (m :: * -> *).
Applicative m =>
(Relevance -> Relevance) -> m Type -> m Type -> m Type
garr 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 = forall (m :: * -> *).
Applicative m =>
(Relevance -> Relevance) -> m Type -> m Type -> m Type
garr (forall a b. a -> b -> a
const 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 = forall (m :: * -> *).
Applicative m =>
(Relevance -> Relevance) -> m Type -> m Type -> m Type
garr (forall a b. a -> b -> a
const 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 $ forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Sort -> Sort
funSort (forall a. LensSort a => a -> Sort
getSort Type
a') (forall a. LensSort a => a -> Sort
getSort Type
b')) forall a b. (a -> b) -> a -> b
$
    Dom Type -> Abs Type -> Term
Pi (forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
f forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom Type
a') (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 = forall a. ArgInfo -> String -> a -> Dom a
defaultNamedArgDom ArgInfo
info String
name Type
a
  Type
b <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
name, Dom Type
dom) m Type
b
  let y :: String
y = String -> String
stringToArgName String
name
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El (Dom Type -> Abs Type -> Sort
mkPiSort Dom Type
dom (forall a. String -> a -> Abs a
Abs String
y Type
b))
              (Dom Type -> Abs Type -> Term
Pi Dom Type
dom (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 = forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgInfo -> String -> m Type -> m Type -> m Type
gpi forall a b. (a -> b) -> a -> b
$ 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 = 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 = forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
s NamesT m Type
a (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 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 = forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
nPi String
s NamesT m Type
a (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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
n (forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl m Term
isOne 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
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
s (Pi Dom Type
d Abs Type
b)) = forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi
  (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant forall a b. (a -> b) -> a -> b
$ Dom Type
d { domIsFinite :: Bool
domIsFinite = Bool
True })
  Abs Type
b
toFinitePi 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 = forall t a. Sort' t -> a -> Type'' t a
El forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
l) 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 = forall t a. Sort' t -> a -> Type'' t a
El forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall t. Level' t -> Sort' t
SSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. t -> Level' t
atomicLevel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
l) 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 = (forall t a. Sort' t -> a -> Type'' t a
El (forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
0) 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 = (forall t a. Sort' t -> a -> Type'' t a
El (forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> a -> Abs a
NoAbs String
"_"

varM :: Applicative m => Int -> m Term
varM :: forall (m :: * -> *). Applicative m => Int -> m Term
varM = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 = forall (m :: * -> *).
Applicative m =>
ArgInfo -> m Term -> m Term -> m Term
gApply' (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 forall t. Apply t => t -> Args -> t
`apply` [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
(<@>) = forall (m :: * -> *).
Applicative m =>
Hiding -> m Term -> m Term -> m Term
gApply Hiding
NotHidden
<#> :: forall (m :: * -> *). Applicative m => 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
(<..>) = forall (m :: * -> *).
Applicative m =>
ArgInfo -> m Term -> m Term -> m Term
gApply' (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 forall t. Apply t => t -> Elims -> t
`applyE` [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 = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primList 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 = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primMaybe 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 = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIO 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 = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath 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 = forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Integer -> Sort
mkType Integer
0)

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

-- | @SizeUniv@ as a type.
tSizeUniv :: Applicative m => m Type
tSizeUniv :: forall (m :: * -> *). Applicative m => m Type
tSizeUniv = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort Sort
sSizeUniv

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

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

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

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

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

lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
lookupPrimitiveFunction String
x =
  forall a. a -> Maybe a -> a
fromMaybe (do
                forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.prim" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Lookup of primitive function" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text String
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"failed"
                forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
NoSuchPrimitiveFunction String
x)
            (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 = forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameCanonical forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q)
  PrimImpl Type
t PrimFun
pf <- String -> TCM PrimitiveImpl
lookupPrimitiveFunction String
s
  forall (m :: * -> *) a. Monad m => a -> m a
return (String
s, Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t 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 = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
getQNameFromTerm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
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 <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
    case Term -> Term
unSpine Term
v of
      Def QName
x Elims
_   -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
      Con ConHead
x ConInfo
_ Elims
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
x
      Lam ArgInfo
_ Abs Term
b   -> forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
getQNameFromTerm forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs Term
b
      Term
_ -> 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 = (forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
String -> m (Maybe QName)
getBuiltinName String
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
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 -> String -> String
[SigmaKit] -> String -> String
SigmaKit -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [SigmaKit] -> String -> String
$cshowList :: [SigmaKit] -> String -> String
show :: SigmaKit -> String
$cshow :: SigmaKit -> String
showsPrec :: Int -> SigmaKit -> String -> String
$cshowsPrec :: Int -> 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 <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
builtinSigma
  case Maybe QName
ms of
    Maybe QName
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Just QName
sigma -> do
      Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
          forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ SigmaKit
            { sigmaName :: QName
sigmaName = QName
sigma
            , sigmaCon :: ConHead
sigmaCon  = ConHead
con
            , sigmaFst :: QName
sigmaFst  = forall t e. Dom' t e -> e
unDom Dom QName
fst
            , sigmaSnd :: QName
sigmaSnd  = forall t e. Dom' t e -> e
unDom Dom QName
snd
            }
        Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__