{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Data where

import Prelude hiding (null)

import Control.Monad
import Control.Monad.Except
import Control.Monad.Trans
import Control.Monad.Trans.Maybe

import Data.Set (Set)
import qualified Data.Set as Set

import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Abstract.Views (deepUnscope)
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.Syntax.Position
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Scope.Monad

import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Generalize
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Names
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Positivity.Occurrence (Occurrence(StrictPos))
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Free
import Agda.TypeChecking.Forcing
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Telescope

import {-# SOURCE #-} Agda.TypeChecking.Rules.Term ( isType_ )

import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Datatypes
---------------------------------------------------------------------------

-- | Type check a datatype definition. Assumes that the type has already been
--   checked.
checkDataDef :: A.DefInfo -> QName -> UniverseCheck -> A.DataDefParams -> [A.Constructor] -> TCM ()
checkDataDef :: DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Constructor]
-> TCM ()
checkDataDef DefInfo
i QName
name UniverseCheck
uc (A.DataDefParams Set Name
gpars [LamBinding]
ps) [Constructor]
cs =
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> [LamBinding] -> [Constructor] -> Call
CheckDataDef (forall a. HasRange a => a -> Range
getRange QName
name) QName
name [LamBinding]
ps [Constructor]
cs) forall a b. (a -> b) -> a -> b
$ do

        -- Add the datatype module
        ModuleName -> TCM ()
addSection (QName -> ModuleName
qnameToMName QName
name)

        -- Look up the type of the datatype.
        Definition
def <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
        Type
t   <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
        let npars :: Nat
npars =
              case Definition -> Defn
theDef Definition
def of
                DataOrRecSig Nat
n -> Nat
n
                Defn
_              -> forall a. HasCallStack => a
__IMPOSSIBLE__

        -- Make sure the shape of the type is visible
        let unTelV :: TelV Type -> Type
unTelV (TelV Tele (Dom Type)
tel Type
a) = Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
tel Type
a
        Type
t <- TelV Type -> Type
unTelV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t

        [Maybe Name]
parNames <- Set Name -> QName -> TCM [Maybe Name]
getGeneralizedParameters Set Name
gpars QName
name

        -- Top level free vars
        Nat
freeVars <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize

        -- The parameters are in scope when checking the constructors.
        Defn
dataDef <- forall a.
[Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [Maybe Name]
parNames Type
t forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
gtel Type
t0 ->
                   forall a.
Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters (Nat
npars forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Maybe Name]
parNames) [LamBinding]
ps Type
t0 forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
ptel Type
t0 -> do

            -- Parameters are always hidden in constructors
            let tel :: Tele (Dom Type)
tel  = forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
gtel Tele (Dom Type)
ptel
                tel' :: Tele (Dom Type)
tel' = forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom Type)
tel
            -- let tel' = hideTel tel

            -- The type we get from bindParameters is Θ -> s where Θ is the type of
            -- the indices. We count the number of indices and return s.
            -- We check that s is a sort.
            let TelV Tele (Dom Type)
ixTel Type
s0 = Type -> TelV Type
telView' Type
t0
                nofIxs :: Nat
nofIxs = forall a. Sized a => a -> Nat
size Tele (Dom Type)
ixTel

            Sort' Term
s <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ do
              -- Andreas, 2016-11-02 issue #2290
              -- Trying to unify the sort with a fresh sort meta which is
              -- defined outside the index telescope is the most robust way
              -- to check independence of the indices.
              -- However, it might give the dreaded "Cannot instantiate meta..."
              -- error which we replace by a more understandable error
              -- in case of a suspected dependency.
              Sort' Term
s <- TCMT IO (Sort' Term)
newSortMetaBelowInf
              forall a. TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
ixTel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
s0 forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
nofIxs forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort Sort' Term
s) forall a b. (a -> b) -> a -> b
$ \ TCErr
err ->
                  if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Free a => Nat -> a -> Bool
`freeIn` Type
s0) [Nat
0..Nat
nofIxs forall a. Num a => a -> a -> a
- Nat
1] then forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                     forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ TCMT IO Doc
"The sort of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name
                          , TCMT IO Doc
"cannot depend on its indices in the type"
                          , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0
                          ]
                  else forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
              forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort' Term
s

            -- when `--without-K`, all the indices should fit in the
            -- sort of the datatype (see #3420).
            let s' :: Sort' Term
s' = case Sort' Term
s of
                  Prop Level
l -> forall t. Level' t -> Sort' t
Type Level
l
                  Sort' Term
_      -> Sort' Term
s
            -- Andreas, 2019-07-16, issue #3916:
            -- NoUniverseCheck should also disable the index sort check!
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (UniverseCheck
uc forall a. Eq a => a -> a -> Bool
== UniverseCheck
NoUniverseCheck) forall a b. (a -> b) -> a -> b
$
              forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
withoutKOption forall a b. (a -> b) -> a -> b
$ Sort' Term -> Tele (Dom Type) -> TCM ()
checkIndexSorts Sort' Term
s' Tele (Dom Type)
ixTel

            forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.sort" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"checking datatype" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name
              , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                [ TCMT IO Doc
"type (parameters instantiated):   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0
                , TCMT IO Doc
"type (full):   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
                , TCMT IO Doc
"sort:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort' Term
s
                , TCMT IO Doc
"indices:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Nat
nofIxs)
                , TCMT IO Doc
"gparams:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show [Maybe Name]
parNames)
                , TCMT IO Doc
"params: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. ExprLike a => a -> a
deepUnscope [LamBinding]
ps)
                ]
              ]
            let npars :: Nat
npars = forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel

            -- Change the datatype from an axiom to a datatype with no constructors.
            let dataDef :: Defn
dataDef = Datatype
                  { dataPars :: Nat
dataPars       = Nat
npars
                  , dataIxs :: Nat
dataIxs        = Nat
nofIxs
                  , dataClause :: Maybe Clause
dataClause     = forall a. Maybe a
Nothing
                  , dataCons :: [QName]
dataCons       = []     -- Constructors are added later
                  , dataSort :: Sort' Term
dataSort       = Sort' Term
s
                  , dataAbstr :: IsAbstract
dataAbstr      = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
                  , dataMutual :: Maybe [QName]
dataMutual     = forall a. Maybe a
Nothing
                  , dataPathCons :: [QName]
dataPathCons   = []     -- Path constructors are added later
                  }

            forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
npars forall a b. (a -> b) -> a -> b
$ do
              QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
name ArgInfo
defaultArgInfo QName
name Type
t Defn
dataDef
                -- polarity and argOcc.s determined by the positivity checker

            -- Check the types of the constructors
            [Maybe QName]
pathCons <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Constructor]
cs forall a b. (a -> b) -> a -> b
$ \ Constructor
c -> do
              IsPathCons
isPathCons <- QName
-> UniverseCheck
-> Tele (Dom Type)
-> Nat
-> Sort' Term
-> Constructor
-> TCM IsPathCons
checkConstructor QName
name UniverseCheck
uc Tele (Dom Type)
tel' Nat
nofIxs Sort' Term
s Constructor
c
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if IsPathCons
isPathCons forall a. Eq a => a -> a -> Bool
== IsPathCons
PathCons then forall a. a -> Maybe a
Just (Constructor -> QName
A.axiomName Constructor
c) else forall a. Maybe a
Nothing

            -- Return the data definition
            forall (m :: * -> *) a. Monad m => a -> m a
return Defn
dataDef{ dataPathCons :: [QName]
dataPathCons = forall a. [Maybe a] -> [a]
catMaybes [Maybe QName]
pathCons }

        let cons :: [QName]
cons   = forall a b. (a -> b) -> [a] -> [b]
map Constructor -> QName
A.axiomName [Constructor]
cs  -- get constructor names

        -- Add the datatype to the signature with its constructors.
        -- It was previously added without them.
        QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
name ArgInfo
defaultArgInfo QName
name Type
t forall a b. (a -> b) -> a -> b
$
            Defn
dataDef{ dataCons :: [QName]
dataCons = [QName]
cons }


-- | Ensure that the type is a sort.
--   If it is not directly a sort, compare it to a 'newSortMetaBelowInf'.
forceSort :: Type -> TCM Sort
forceSort :: Type -> TCMT IO (Sort' Term)
forceSort Type
t = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Sort Sort' Term
s -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
  Term
_      -> do
    Sort' Term
s <- TCMT IO (Sort' Term)
newSortMetaBelowInf
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t (Sort' Term -> Type
sort Sort' Term
s)
    forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s


-- | Type check a constructor declaration. Checks that the constructor targets
--   the datatype and that it fits inside the declared sort.
--   Returns the non-linear parameters.
checkConstructor
  :: QName         -- ^ Name of data type.
  -> UniverseCheck -- ^ Check universes?
  -> Telescope     -- ^ Parameter telescope.
  -> Nat           -- ^ Number of indices of the data type.
  -> Sort          -- ^ Sort of the data type.
  -> A.Constructor -- ^ Constructor declaration (type signature).
  -> TCM IsPathCons
checkConstructor :: QName
-> UniverseCheck
-> Tele (Dom Type)
-> Nat
-> Sort' Term
-> Constructor
-> TCM IsPathCons
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Nat
nofIxs Sort' Term
s (A.ScopedDecl ScopeInfo
scope [Constructor
con]) = do
  ScopeInfo -> TCM ()
setScope ScopeInfo
scope
  QName
-> UniverseCheck
-> Tele (Dom Type)
-> Nat
-> Sort' Term
-> Constructor
-> TCM IsPathCons
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Nat
nofIxs Sort' Term
s Constructor
con
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Nat
nofIxs Sort' Term
s con :: Constructor
con@(A.Axiom KindOfName
_ DefInfo
i ArgInfo
ai Maybe [Occurrence]
Nothing QName
c Expr
e) =
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Tele (Dom Type) -> Sort' Term -> Constructor -> Call
CheckConstructor QName
d Tele (Dom Type)
tel Sort' Term
s Constructor
con) forall a b. (a -> b) -> a -> b
$ do
{- WRONG
      -- Andreas, 2011-04-26: the following happens to the right of ':'
      -- we may use irrelevant arguments in a non-strict way in types
      t' <- workOnTypes $ do
-}
        forall {m :: * -> *} {a} {a}.
(MonadDebug m, PrettyTCM a, PrettyTCM a) =>
a -> a -> m ()
debugEnter QName
c Expr
e
        -- check that we are relevant
        case forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai of
          Relevance
Relevant   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Relevance
Irrelevant -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ ArgName
"Irrelevant constructors are not supported"
          Relevance
NonStrict  -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ ArgName
"Shape-irrelevant constructors are not supported"
        case forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai of
          Quantityω{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Quantity0{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Quantity1{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ ArgName
"Quantity-restricted constructors are not supported"
        -- check that the type of the constructor is well-formed
        (Type
t, IsPathCons
isPathCons) <- forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext ArgInfo
ai forall a b. (a -> b) -> a -> b
$
                           Expr -> QName -> TCMT IO (Type, IsPathCons)
checkConstructorType Expr
e QName
d

        -- compute which constructor arguments are forced (only point constructors)
        [IsForced]
forcedArgs <- if IsPathCons
isPathCons forall a. Eq a => a -> a -> Bool
== IsPathCons
PointCons
                      then QName -> Type -> TCM [IsForced]
computeForcingAnnotations QName
c Type
t
                      else forall (m :: * -> *) a. Monad m => a -> m a
return []
        -- check that the sort (universe level) of the constructor type
        -- is contained in the sort of the data type
        -- (to avoid impredicative existential types)
        forall {m :: * -> *} {a}. (MonadDebug m, PrettyTCM a) => a -> m ()
debugFitsIn Sort' Term
s
        -- To allow propositional squash, we turn @Prop ℓ@ into @Set ℓ@
        -- for the purpose of checking the type of the constructors.
        let s' :: Sort' Term
s' = case Sort' Term
s of
              Prop Level
l -> forall t. Level' t -> Sort' t
Type Level
l
              Sort' Term
_      -> Sort' Term
s
        Nat
arity <- forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Type -> Sort' Term -> Call
CheckConstructorFitsIn QName
c Type
t Sort' Term
s') forall a b. (a -> b) -> a -> b
$
                 forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext ArgInfo
ai forall a b. (a -> b) -> a -> b
$
                 UniverseCheck -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn UniverseCheck
uc [IsForced]
forcedArgs Type
t Sort' Term
s'
        -- this may have instantiated some metas in s, so we reduce
        Sort' Term
s <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort' Term
s
        forall {m :: * -> *} {a} {a}.
(MonadDebug m, PrettyTCM a, PrettyTCM a) =>
a -> a -> m ()
debugAdd QName
c Type
t

        (TelV Tele (Dom Type)
fields Type
_, Boundary
boundary) <- forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundaryP (-Nat
1) Type
t

        -- We assume that the current context matches the parameters
        -- of the datatype in an empty context (c.f. getContextSize above).
        Tele (Dom Type)
params <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope

        (ConHead
con, CompKit
comp, Maybe [QName]
projNames) <- do
            -- Name for projection of ith field of constructor c is just c-i
            [QName]
names <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Nat
0 .. forall a. Sized a => a -> Nat
size Tele (Dom Type)
fields forall a. Num a => a -> a -> a
- Nat
1] forall a b. (a -> b) -> a -> b
$ \ Nat
i ->
              ArgName -> TCMT IO QName
freshAbstractQName'_ forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> ArgName
P.prettyShow (QName -> Name
A.qnameName QName
c) forall a. [a] -> [a] -> [a]
++ ArgName
"-" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Nat
i

            -- nofIxs == 0 means the data type can be reconstructed
            -- by appling the QName d to the parameters.
            let dataT :: Type
dataT = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
params

            forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con.comp" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
              [ TCMT IO Doc
"params =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Tele (Dom Type)
params
              , TCMT IO Doc
"dataT  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
dataT
              , TCMT IO Doc
"fields =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Tele (Dom Type)
fields
              , TCMT IO Doc
"names  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [QName]
names
              ]

            let con :: ConHead
con = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c DataOrRecord
IsData Induction
Inductive forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [QName]
names forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
fields

            QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> TCM ()
defineProjections QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fields Type
dataT
            -- Cannot compose indexed inductive types yet.
            CompKit
comp <- if Nat
nofIxs forall a. Eq a => a -> a -> Bool
/= Nat
0 Bool -> Bool -> Bool
|| (forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef)
                    then forall (m :: * -> *) a. Monad m => a -> m a
return CompKit
emptyCompKit
                    else forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO CompKit
defineCompData QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fields Type
dataT Boundary
boundary
            forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead
con, CompKit
comp, forall a. a -> Maybe a
Just [QName]
names)

        -- add parameters to constructor type and put into signature
        forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) forall a b. (a -> b) -> a -> b
$ do

          QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
c ArgInfo
ai QName
c (Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
tel Type
t) forall a b. (a -> b) -> a -> b
$ Constructor
              { conPars :: Nat
conPars   = forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel
              , conArity :: Nat
conArity  = Nat
arity
              , conSrcCon :: ConHead
conSrcCon = ConHead
con
              , conData :: QName
conData   = QName
d
              , conAbstr :: IsAbstract
conAbstr  = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
              , conInd :: Induction
conInd    = Induction
Inductive
              , conComp :: CompKit
conComp   = CompKit
comp
              , conProj :: Maybe [QName]
conProj   = Maybe [QName]
projNames
              , conForced :: [IsForced]
conForced = [IsForced]
forcedArgs
              , conErased :: Maybe [Bool]
conErased = forall a. Maybe a
Nothing  -- computed during compilation to treeless
              }

        -- Add the constructor to the instance table, if needed
        case forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
i of
          InstanceDef Range
_r -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
c forall a b. (a -> b) -> a -> b
$ do
            -- Including the range of the @instance@ keyword, like
            -- @(getRange (r,c))@, does not produce good results.
            -- Andreas, 2020-01-28, issue #4360:
            -- Use addTypedInstance instead of addNamedInstance
            -- to detect unusable instances.
            QName -> Type -> TCM ()
addTypedInstance QName
c Type
t
            -- addNamedInstance c d
          IsInstance
NotInstanceDef -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

        forall (m :: * -> *) a. Monad m => a -> m a
return IsPathCons
isPathCons

  where
    -- Issue 3362: we need to do the `constructs` call inside the
    -- generalization, so unpack the A.Generalize
    checkConstructorType :: Expr -> QName -> TCMT IO (Type, IsPathCons)
checkConstructorType (A.ScopedExpr ScopeInfo
s Expr
e) QName
d = forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
withScope_ ScopeInfo
s forall a b. (a -> b) -> a -> b
$ Expr -> QName -> TCMT IO (Type, IsPathCons)
checkConstructorType Expr
e QName
d
    checkConstructorType Expr
e QName
d = do
      let check :: Nat -> Expr -> TCMT IO (Type, IsPathCons)
check Nat
k Expr
e = do
            Type
t <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO Type
isType_ Expr
e
            -- check that the type of the constructor ends in the data type
            Nat
n <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
            forall {m :: * -> *} {a} {a} {a}.
(MonadDebug m, PrettyTCM a, PrettyTCM a, Show a) =>
a -> a -> a -> m ()
debugEndsIn Type
t QName
d (Nat
n forall a. Num a => a -> a -> a
- Nat
k)
            IsPathCons
isPathCons <- Nat -> Nat -> Type -> QName -> TCM IsPathCons
constructs (Nat
n forall a. Num a => a -> a -> a
- Nat
k) Nat
k Type
t QName
d
            forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, IsPathCons
isPathCons)

      case Expr
e of
        A.Generalized Set QName
s Expr
e -> do
          ([Maybe QName]
_, Type
t, IsPathCons
isPathCons) <- forall a.
Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' Set QName
s (Nat -> Expr -> TCMT IO (Type, IsPathCons)
check Nat
1 Expr
e)
          forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, IsPathCons
isPathCons)
        Expr
_ -> Nat -> Expr -> TCMT IO (Type, IsPathCons)
check Nat
0 Expr
e

    debugEnter :: a -> a -> m ()
debugEnter a
c a
e =
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"checking constructor" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
e
        ]
    debugEndsIn :: a -> a -> a -> m ()
debugEndsIn a
t a
d a
n =
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"checking that"
              , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t
              , TCMT IO Doc
"ends in" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
d
              ]
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"nofPars =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show a
n)
        ]
    debugFitsIn :: a -> m ()
debugFitsIn a
s =
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"checking that the type fits in"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
s
        ]
    debugAdd :: a -> a -> m ()
debugAdd a
c a
t =
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"adding constructor" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t
        ]
checkConstructor QName
_ UniverseCheck
_ Tele (Dom Type)
_ Nat
_ Sort' Term
_ Constructor
_ = forall a. HasCallStack => a
__IMPOSSIBLE__ -- constructors are axioms

defineCompData :: QName      -- datatype name
               -> ConHead
               -> Telescope  -- Γ parameters
               -> [QName]    -- projection names
               -> Telescope  -- Γ ⊢ Φ field types
               -> Type       -- Γ ⊢ T target type
               -> Boundary   -- [(i,t_i,b_i)],  Γ.Φ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : B_i
               -> TCM CompKit
defineCompData :: QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO CompKit
defineCompData QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary = do
  [Maybe Term]
required <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getTerm'
    [ ArgName
builtinInterval
    , ArgName
builtinIZero
    , ArgName
builtinIOne
    , ArgName
builtinIMin
    , ArgName
builtinIMax
    , ArgName
builtinINeg
    , ArgName
builtinPOr
    , ArgName
builtinItIsOne
    ]
  if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust [Maybe Term]
required) then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CompKit
emptyCompKit else do
    Maybe QName
hcomp  <- forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
whenDefined (forall a. Null a => a -> Bool
null Boundary
boundary) [ArgName
builtinHComp,ArgName
builtinTrans] (TranspOrHComp
-> QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO (Maybe QName)
defineTranspOrHCompD TranspOrHComp
DoHComp  QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary)
    Maybe QName
transp <- forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
whenDefined Bool
True            [ArgName
builtinTrans]              (TranspOrHComp
-> QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO (Maybe QName)
defineTranspOrHCompD TranspOrHComp
DoTransp QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CompKit
      { nameOfTransp :: Maybe QName
nameOfTransp = Maybe QName
transp
      , nameOfHComp :: Maybe QName
nameOfHComp  = Maybe QName
hcomp
      }
  where
    -- Δ^I, i : I |- sub Δ : Δ
    sub :: a -> Substitution' Term
sub a
tel = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [ Nat -> Term
var Nat
n forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0] | Nat
n <- [Nat
1..forall a. Sized a => a -> Nat
size a
tel] ]
    withArgInfo :: Tele (Dom t) -> [b] -> [Arg b]
withArgInfo Tele (Dom t)
tel = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall e. ArgInfo -> e -> Arg e
Arg (forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> ArgInfo
domInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList forall a b. (a -> b) -> a -> b
$ Tele (Dom t)
tel)

    defineTranspOrHCompD :: TranspOrHComp
-> QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO (Maybe QName)
defineTranspOrHCompD TranspOrHComp
cmd QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary = do
      let project :: Term -> QName -> Term
project = (\ Term
t QName
p -> forall t. Apply t => t -> [Arg Term] -> t
apply (QName -> Elims -> Term
Def QName
p []) [forall e. e -> Arg e
argN Term
t])
      Maybe
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
   Substitution' Term)
stuff <- TranspOrHComp
-> Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom Type)
-> [Arg QName]
-> Type
-> TCM
     (Maybe
        ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
         Substitution' Term))
defineTranspOrHCompForFields TranspOrHComp
cmd
                 (forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null Boundary
boundary) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. a -> Maybe a
Just (ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem forall a b. (a -> b) -> a -> b
$ forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
teleElims Tele (Dom Type)
fsT Boundary
boundary))
                 Term -> QName -> Term
project QName
d Tele (Dom Type)
params Tele (Dom Type)
fsT (forall a b. (a -> b) -> [a] -> [b]
map forall e. e -> Arg e
argN [QName]
names) Type
t
      forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
   Substitution' Term)
stuff (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ ((QName
theName, Tele (Dom Type)
gamma , Type
ty, [Dom Type]
_cl_types , [Term]
bodies), Substitution' Term
theSub) -> do

      Term
iz <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
      Term
body <- do
        case TranspOrHComp
cmd of
          TranspOrHComp
DoHComp -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall {t} {b}. Tele (Dom t) -> [b] -> [Arg b]
withArgInfo Tele (Dom Type)
fsT [Term]
bodies)
          TranspOrHComp
DoTransp | forall a. Null a => a -> Bool
null Boundary
boundary -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall {t} {b}. Tele (Dom t) -> [b] -> [Arg b]
withArgInfo Tele (Dom Type)
fsT [Term]
bodies)
                   | Bool
otherwise -> do
            Term
io <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
            Term
tIMax <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax
            Term
tIMin <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin
            Term
tINeg <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
            Term
tPOr  <- 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 => ArgName -> m (Maybe Term)
getTerm' ArgName
builtinPOr
            Term
tHComp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp
            -- Δ = params
            -- Δ ⊢ Φ = fsT
            -- (δ : Δ) ⊢ T = R δ
            -- (δ : Δ) ⊢ con : Φ → R δ  -- no indexing
            -- boundary = [(i,t_i,u_i)]
            -- Δ.Φ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : B_i
            -- Δ.Φ | PiPath Φ boundary (R δ) |- teleElims fsT boundary : R δ
            -- Γ = ((δ : Δ^I), φ, us : Φ[δ 0]) = gamma
            -- Γ ⊢ ty = R (δ i1)
            -- (γ : Γ) ⊢ cl_types = (flatten Φ)[n ↦ f_n (transpR γ)]
            -- Γ ⊢ bodies : Φ[δ i1]
            -- Γ ⊢ t : ty
            -- Γ, i : I ⊢ theSub : Δ.Φ
            let

              -- Δ.Φ ⊢ u = Con con ConOSystem $ teleElims fsT boundary : R δ
              u :: Term
u = ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem forall a b. (a -> b) -> a -> b
$ forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
teleElims Tele (Dom Type)
fsT Boundary
boundary
              -- Γ ⊢ u
              the_u :: Term
the_u = forall a. Nat -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u
                where
                  -- δ : Δ^I, φ : F ⊢ [δ 0] : Δ
                  d0 :: Substitution
                  d0 :: Substitution' Term
d0 = forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
1 -- Δ^I, φ : F ⊢ Δ
                             (forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
iz forall a. Substitution' a
IdS forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) -- Δ^I ⊢ Δ
                                       -- Δ^I , i:I ⊢ sub params : Δ
              the_phi :: Term
the_phi = forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0
              -- Γ ⊢ sigma : Δ.Φ
              -- sigma = [δ i1,bodies]
              sigma :: Substitution' Term
sigma = forall a. [a] -> [a]
reverse [Term]
bodies forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Substitution' Term
d1
               where
                -- δ i1
                d1 :: Substitution
                d1 :: Substitution' Term
d1 = forall a. Nat -> Substitution' a -> Substitution' a
wkS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
params) -- Γ ⊢ Δ
                       (forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
io forall a. Substitution' a
IdS forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) -- Δ^I ⊢ Δ
                                 -- Δ^I , i:I ⊢ sub params : Δ

              -- Δ.Φ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : R δ
              bs :: Boundary
bs = Tele (Dom Type) -> Boundary -> Boundary
fullBoundary Tele (Dom Type)
fsT Boundary
boundary
              -- ψ = sigma `applySubst` map (\ i → i ∨ ~ i) . map fst $ boundary
              -- Γ ⊢ t : R (δ i1)
              w1' :: Term
w1' = ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem forall a b. (a -> b) -> a -> b
$ Substitution' Term
sigma forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
teleElims Tele (Dom Type)
fsT Boundary
boundary
              -- (δ, φ, u0) : Γ ⊢
              -- w1 = hcomp (\ i → R (δ i1))
              --            (\ i → [ ψ ↦ α (~ i), φ ↦ u0])
              --            w1'
              imax :: NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax NamesT (TCMT IO) Term
x NamesT (TCMT IO) Term
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y
              ineg :: NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
r = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tINeg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
r
              lvlOfType :: Type -> Term
lvlOfType = (\ (Type Level
l) -> Level -> Term
Level Level
l) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSort a => a -> Sort' Term
getSort
              pOr :: NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
pOr NamesT (TCMT IO) Type
la NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
j NamesT (TCMT IO) Term
u0 NamesT (TCMT IO) Term
u1 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPOr forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Type -> Term
lvlOfType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j
                                           forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" (\ NamesT (TCMT IO) Term
_ -> forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
u0 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
u1
              absAp :: m (Abs r) -> m (SubstArg r) -> m r
absAp m (Abs r)
x m (SubstArg r)
y = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. Subst a => Abs a -> SubstArg a -> a
absApp m (Abs r)
x m (SubstArg r)
y

              mkFace :: (Term, (Term, Term)) -> TCMT IO (Abs (Term, Term))
mkFace (Term
r,(Term
u1,Term
u2)) = forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
                -- Γ
                NamesT (TCMT IO) Term
phi <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
the_phi  -- (δ , φ , us) ⊢ φ
                -- Γ ⊢ ty = Abs i. R (δ i)
                NamesT (TCMT IO) (Abs Type)
ty <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a b. (a -> b) -> a -> b
$ (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
params)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
t)

                forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i -> do
                  -- Γ, i
                  [NamesT (TCMT IO) Term
r,NamesT (TCMT IO) Term
u1,NamesT (TCMT IO) Term
u2] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
theSub) [Term
r,Term
u1,Term
u2]
                  Term
psi <- NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax NamesT (TCMT IO) Term
r (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
r)
                  let
                    -- Γ, i ⊢ squeeze u = primTrans (\ j -> ty [i := i ∨ j]) (φ ∨ i) u
                    squeeze :: NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
squeeze NamesT (TCMT IO) Term
u = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans
                                          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"j" (\ NamesT (TCMT IO) Term
j -> Type -> Term
lvlOfType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
ty forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
j))
                                          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"j" (\ NamesT (TCMT IO) Term
j -> forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
ty forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
j))
                                          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
phi NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
`imax` NamesT (TCMT IO) Term
i)
                                          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
u
                  Term
alpha <- NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
pOr (NamesT (TCMT IO) (Abs Type)
ty forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` NamesT (TCMT IO) Term
i)
                              (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
r)
                              NamesT (TCMT IO) Term
r
                           (forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
squeeze NamesT (TCMT IO) Term
u1) (forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
squeeze NamesT (TCMT IO) Term
u2)
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Term
psi, Term
alpha)

            -- Γ ⊢ Abs i. [(ψ_n,α_n : [ψ] → R (δ i))]
            [Abs (Term, Term)]
faces <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term, (Term, Term)) -> TCMT IO (Abs (Term, Term))
mkFace Boundary
bs

            forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
                -- Γ
                NamesT (TCMT IO) Term
w1' <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
w1'
                NamesT (TCMT IO) Term
phi <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
the_phi
                NamesT (TCMT IO) Term
u   <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
the_u
                -- R (δ i1)
                NamesT (TCMT IO) Type
ty <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Type
ty
                [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
faces <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Abs (Term, Term)
x -> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Impossible -> Abs a -> a
noabsApp forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst Abs (Term, Term)
x) (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd Abs (Term, Term)
x)) [Abs (Term, Term)]
faces
                let
                  thePsi :: NamesT (TCMT IO) Term
thePsi = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
faces)
                  hcomp :: NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
hcomp NamesT (TCMT IO) Type
ty NamesT (TCMT IO) Term
phi NamesT (TCMT IO) Term
sys NamesT (TCMT IO) Term
a0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Type -> Term
lvlOfType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
ty)
                                                    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
ty)
                                                    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
phi
                                                    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
sys
                                                    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a0
                let
                 sys :: NamesT (TCMT IO) Term
sys = forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i -> do
                  let
                    recurse :: [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
-> NamesT (TCMT IO) Term
recurse [(NamesT (TCMT IO) Term
psi,NamesT (TCMT IO) (Abs Term)
alpha)] = NamesT (TCMT IO) (Abs Term)
alpha forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
i)
                    recurse ((NamesT (TCMT IO) Term
psi,NamesT (TCMT IO) (Abs Term)
alpha):[(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
xs) = NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
pOr NamesT (TCMT IO) Type
ty
                                                   NamesT (TCMT IO) Term
psi  NamesT (TCMT IO) Term
theOr
                                                   (NamesT (TCMT IO) (Abs Term)
alpha forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
i)) ([(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
-> NamesT (TCMT IO) Term
recurse [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
xs)
                      where
                        theOr :: NamesT (TCMT IO) Term
theOr = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
xs)
                    recurse [] = forall a. HasCallStack => a
__IMPOSSIBLE__
                    sys_alpha :: NamesT (TCMT IO) Term
sys_alpha = [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
-> NamesT (TCMT IO) Term
recurse [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
faces
                  NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
pOr NamesT (TCMT IO) Type
ty
                                                   NamesT (TCMT IO) Term
thePsi    NamesT (TCMT IO) Term
phi
                                                   NamesT (TCMT IO) Term
sys_alpha (forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
u)
                NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
hcomp NamesT (TCMT IO) Type
ty (NamesT (TCMT IO) Term
thePsi NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
`imax` NamesT (TCMT IO) Term
phi) NamesT (TCMT IO) Term
sys NamesT (TCMT IO) Term
w1'


      let

        -- δ : Δ^I, φ : F ⊢ [δ 0] : Δ
        d0 :: Substitution
        d0 :: Substitution' Term
d0 = forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
1 -- Δ^I, φ : F ⊢ Δ
                       (forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
iz forall a. Substitution' a
IdS forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) -- Δ^I ⊢ Δ
                                 -- Δ^I , i:I ⊢ sub params : Δ

        -- Δ.Φ ⊢ u = Con con ConOSystem $ teleElims fsT boundary : R δ
--        u = Con con ConOSystem $ teleElims fsT boundary
        up :: Pattern' DBPatVar
up = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con (PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
defaultPatternInfo Bool
False Bool
False forall a. Maybe a
Nothing Bool
False) forall a b. (a -> b) -> a -> b
$
               forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
telePatterns (Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom Type)
fsT) (forall a. Nat -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Boundary
boundary)
--        gamma' = telFromList $ take (size gamma - 1) $ telToList gamma

        -- (δ , φ , fs : Φ[d0]) ⊢ u[liftS Φ d0]
        -- (δ , φ, u) : Γ ⊢ body
        -- Δ ⊢ Φ = fsT
        -- (δ , φ , fs : Φ[d0]) ⊢ u[liftS Φ d0] `consS` raiseS Φ : Γ
--        (tel',theta) = (abstract gamma' (d0 `applySubst` fsT), (liftS (size fsT) d0 `applySubst` u) `consS` raiseS (size fsT))

      let
        pats :: [NamedArg (Pattern' DBPatVar)]
pats | forall a. Null a => a -> Bool
null Boundary
boundary = forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
gamma
             | Bool
otherwise     = forall a. Nat -> [a] -> [a]
take (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) (forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
gamma) forall a. [a] -> [a] -> [a]
++ [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ forall a name. a -> Named name a
unnamed forall a b. (a -> b) -> a -> b
$ Pattern' DBPatVar
up]
        clause :: Clause
clause = Clause
          { clauseTel :: Tele (Dom Type)
clauseTel         = Tele (Dom Type)
gamma
          , clauseType :: Maybe (Arg Type)
clauseType        = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Type
ty
          , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats   = [NamedArg (Pattern' DBPatVar)]
pats
          , clauseFullRange :: Range
clauseFullRange   = forall a. Range' a
noRange
          , clauseLHSRange :: Range
clauseLHSRange    = forall a. Range' a
noRange
          , clauseCatchall :: Bool
clauseCatchall    = Bool
False
          , clauseBody :: Maybe Term
clauseBody        = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term
body
          , clauseExact :: Maybe Bool
clauseExact       = forall a. a -> Maybe a
Just Bool
True
          , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. Maybe a
Nothing
              -- Andreas 2020-02-06 TODO
              -- Or: Just False;  is it known to be non-recursive?
          , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
          , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
          }
        cs :: [Clause]
cs = [Clause
clause]
      QName -> [Clause] -> TCM ()
addClauses QName
theName [Clause]
cs
      (Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses forall a. Maybe a
Nothing [Clause]
cs)
      forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe SplitTree
mst forall a b. (a -> b) -> a -> b
$ QName -> SplitTree -> TCM ()
setSplitTree QName
theName
      QName -> CompiledClauses -> TCM ()
setCompiledClauses QName
theName CompiledClauses
cc
      QName -> Bool -> TCM ()
setTerminates QName
theName Bool
True
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
theName

    whenDefined :: Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
whenDefined Bool
False t ArgName
_ m (Maybe a)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    whenDefined Bool
True t ArgName
xs m (Maybe a)
m = do
      t (Maybe Term)
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getTerm' t ArgName
xs
      if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust t (Maybe Term)
xs then m (Maybe a)
m else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

-- Andrea: TODO handle Irrelevant fields somehow.
-- | Define projections for non-indexed data types (families don't work yet).
--   Of course, these projections are partial functions in general.
--
--   Precondition: we are in the context Γ of the data type parameters.
defineProjections :: QName      -- datatype name
                  -> ConHead
                  -> Telescope  -- Γ parameters
                  -> [QName]    -- projection names
                  -> Telescope  -- Γ ⊢ Φ field types
                  -> Type       -- Γ ⊢ T target type
                  -> TCM ()
defineProjections :: QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> TCM ()
defineProjections QName
dataName ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t = do
  let
    -- Γ , (d : T) ⊢ Φ[n ↦ proj n d]
    fieldTypes :: [Dom Type]
fieldTypes = ([ QName -> Elims -> Term
Def QName
f [] forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0] | QName
f <- forall a. [a] -> [a]
reverse [QName]
names ] forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Nat -> Substitution' a
raiseS Nat
1) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
                    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
fsT  -- Γ , Φ ⊢ Φ
    -- ⊢ Γ , (d : T)
    projTel :: Tele (Dom Type)
projTel    = forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
params (forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall a. a -> Dom a
defaultDom Type
t) (forall a. ArgName -> a -> Abs a
Abs ArgName
"d" forall a. Tele a
EmptyTel))
    np :: Nat
np         = forall a. Sized a => a -> Nat
size Tele (Dom Type)
params

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 (forall a. Integral a => a -> [a]
downFrom (forall a. Sized a => a -> Nat
size [Dom Type]
fieldTypes)) [QName]
names [Dom Type]
fieldTypes) forall a b. (a -> b) -> a -> b
$ \ (Nat
i,QName
projName,Dom Type
ty) -> do
    let
      projType :: Dom Type
projType = forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
projTel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
ty
      cpi :: ConPatternInfo
cpi    = PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
defaultPatternInfo Bool
False Bool
False (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) Type
t) Bool
False
      conp :: NamedArg (Pattern' DBPatVar)
conp   = forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
cpi forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
fsT
      sigma :: Substitution' Term
sigma  = ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
fsT) forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
`consS` forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT)
      clause :: Clause
clause = forall a. Null a => a
empty
          { clauseTel :: Tele (Dom Type)
clauseTel         = forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
params Tele (Dom Type)
fsT
          , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats   = [ NamedArg (Pattern' DBPatVar)
conp ]
          , clauseBody :: Maybe Term
clauseBody        = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
i
          , clauseType :: Maybe (Arg Type)
clauseType        = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sigma forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
ty
          , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. a -> Maybe a
Just Bool
False  -- non-recursive
          , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
          }

    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.proj" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"proj" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Nat
i,Dom Type
ty)
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
projName, TCMT IO Doc
":", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
projType ]
      ]

    -- Andreas, 2020-02-14, issue #4437
    -- Define data projections as projection-like from the start.
    forall a. TCM a -> TCM a
noMutualBlock forall a b. (a -> b) -> a -> b
$ do
      let cs :: [Clause]
cs = [ Clause
clause ]
      (Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses forall a. Maybe a
Nothing [Clause]
cs
      let fun :: Defn
fun = Defn
emptyFunction
                { funClauses :: [Clause]
funClauses    = [Clause]
cs
                , funCompiled :: Maybe CompiledClauses
funCompiled   = forall a. a -> Maybe a
Just CompiledClauses
cc
                , funSplitTree :: Maybe SplitTree
funSplitTree  = Maybe SplitTree
mst
                , funProjection :: Maybe Projection
funProjection = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Projection
                    { projProper :: Maybe QName
projProper   = forall a. Maybe a
Nothing
                    , projOrig :: QName
projOrig     = QName
projName
                    , projFromType :: Arg QName
projFromType = forall e. ArgInfo -> e -> Arg e
Arg (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom Type
ty) QName
dataName
                    , projIndex :: Nat
projIndex    = Nat
np forall a. Num a => a -> a -> a
+ Nat
1
                    , projLams :: ProjLams
projLams     = [Arg ArgName] -> ProjLams
ProjLams forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t a. Dom' t a -> Arg a
argFromDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
projTel
                    }
                , funMutual :: Maybe [QName]
funMutual     = forall a. a -> Maybe a
Just []
                , funTerminates :: Maybe Bool
funTerminates = forall a. a -> Maybe a
Just Bool
True
                }
      Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
      forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
projName forall a b. (a -> b) -> a -> b
$
        (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
projName (forall t e. Dom' t e -> e
unDom Dom Type
projType) Language
lang Defn
fun)
          { defNoCompilation :: Bool
defNoCompilation  = Bool
True
          , defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
StrictPos]
          }

      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.proj.fun" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"proj" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Nat
i
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Defn
fun
        ]


freshAbstractQName'_ :: String -> TCM QName
freshAbstractQName'_ :: ArgName -> TCMT IO QName
freshAbstractQName'_ = Fixity' -> Name -> TCMT IO QName
freshAbstractQName Fixity'
noFixity' forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Name
C.simpleName


-- * Special cases of Type
-----------------------------------------------------------

-- | A @Type@ with sort @Type l@
--   Such a type supports both hcomp and transp.
data LType = LEl Level Term deriving (LType -> LType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LType -> LType -> Bool
$c/= :: LType -> LType -> Bool
== :: LType -> LType -> Bool
$c== :: LType -> LType -> Bool
Eq,Nat -> LType -> ShowS
[LType] -> ShowS
LType -> ArgName
forall a.
(Nat -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LType] -> ShowS
$cshowList :: [LType] -> ShowS
show :: LType -> ArgName
$cshow :: LType -> ArgName
showsPrec :: Nat -> LType -> ShowS
$cshowsPrec :: Nat -> LType -> ShowS
Show)

fromLType :: LType -> Type
fromLType :: LType -> Type
fromLType (LEl Level
l Term
t) = forall t a. Sort' t -> a -> Type'' t a
El (forall t. Level' t -> Sort' t
Type Level
l) Term
t

lTypeLevel :: LType -> Level
lTypeLevel :: LType -> Level
lTypeLevel (LEl Level
l Term
t) = Level
l

toLType :: MonadReduce m => Type -> m (Maybe LType)
toLType :: forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType Type
ty = do
  Sort' Term
sort <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort' Term
getSort Type
ty
  case Sort' Term
sort of
    Type Level
l -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Level -> Term -> LType
LEl Level
l (forall t a. Type'' t a -> a
unEl Type
ty)
    Sort' Term
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing

instance Subst LType where
  type SubstArg LType = Term
  applySubst :: Substitution' (SubstArg LType) -> LType -> LType
applySubst Substitution' (SubstArg LType)
rho (LEl Level
l Term
t) = Level -> Term -> LType
LEl (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg LType)
rho Level
l) (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg LType)
rho Term
t)

-- | A @Type@ that either has sort @Type l@ or is a closed definition.
--   Such a type supports some version of transp.
--   In particular we want to allow the Interval as a @ClosedType@.
data CType = ClosedType Sort QName | LType LType deriving (CType -> CType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CType -> CType -> Bool
$c/= :: CType -> CType -> Bool
== :: CType -> CType -> Bool
$c== :: CType -> CType -> Bool
Eq,Nat -> CType -> ShowS
[CType] -> ShowS
CType -> ArgName
forall a.
(Nat -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [CType] -> ShowS
$cshowList :: [CType] -> ShowS
show :: CType -> ArgName
$cshow :: CType -> ArgName
showsPrec :: Nat -> CType -> ShowS
$cshowsPrec :: Nat -> CType -> ShowS
Show)

fromCType :: CType -> Type
fromCType :: CType -> Type
fromCType (ClosedType Sort' Term
s QName
q) = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (QName -> Elims -> Term
Def QName
q [])
fromCType (LType LType
t) = LType -> Type
fromLType LType
t

toCType :: MonadReduce m => Type -> m (Maybe CType)
toCType :: forall (m :: * -> *). MonadReduce m => Type -> m (Maybe CType)
toCType Type
ty = do
  Sort' Term
sort <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort' Term
getSort Type
ty
  case Sort' Term
sort of
    Type Level
l -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ LType -> CType
LType (Level -> Term -> LType
LEl Level
l (forall t a. Type'' t a -> a
unEl Type
ty))
    SSet Level
l  -> do
      Term
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
ty)
      case Term
t of
        Def QName
q [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Sort' Term -> QName -> CType
ClosedType (forall t. Level' t -> Sort' t
SSet Level
l) QName
q
        Term
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
    Sort' Term
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing

instance Subst CType where
  type SubstArg CType = Term
  applySubst :: Substitution' (SubstArg CType) -> CType -> CType
applySubst Substitution' (SubstArg CType)
rho (ClosedType Sort' Term
s QName
t) = Sort' Term -> QName -> CType
ClosedType (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg CType)
rho Sort' Term
s) QName
t
  applySubst Substitution' (SubstArg CType)
rho (LType LType
t) = LType -> CType
LType forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg CType)
rho LType
t


defineTranspOrHCompForFields
  :: TranspOrHComp
  -> (Maybe Term)            -- ^ PathCons, Δ.Φ ⊢ u : R δ
  -> (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
  -> QName       -- ^ some name, e.g. record name
  -> Telescope   -- ^ param types Δ
  -> Telescope   -- ^ fields' types Δ ⊢ Φ
  -> [Arg QName] -- ^ fields' names
  -> Type        -- ^ record type Δ ⊢ T
  -> TCM (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
defineTranspOrHCompForFields :: TranspOrHComp
-> Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom Type)
-> [Arg QName]
-> Type
-> TCM
     (Maybe
        ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
         Substitution' Term))
defineTranspOrHCompForFields TranspOrHComp
cmd Maybe Term
pathCons Term -> QName -> Term
project QName
name Tele (Dom Type)
params Tele (Dom Type)
fsT [Arg QName]
fns Type
rect =
   case TranspOrHComp
cmd of
       TranspOrHComp
DoTransp -> forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
         Tele (Dom CType)
fsT' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadReduce m => Type -> m (Maybe CType)
toCType)) Tele (Dom Type)
fsT
         forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom CType)
-> [Arg QName]
-> Type
-> TCM
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
defineTranspForFields Maybe Term
pathCons Term -> QName -> Term
project QName
name Tele (Dom Type)
params Tele (Dom CType)
fsT' [Arg QName]
fns Type
rect
       TranspOrHComp
DoHComp -> forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
         Tele (Dom LType)
fsT' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType)) Tele (Dom Type)
fsT
         LType
rect' <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType Type
rect
         forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom LType)
-> [Arg QName]
-> LType
-> TCM
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
defineHCompForFields Term -> QName -> Term
project QName
name Tele (Dom Type)
params Tele (Dom LType)
fsT' [Arg QName]
fns LType
rect'


-- invariant: resulting tel Γ is such that Γ = ... , (φ : I), (a0 : ...)
--            where a0 has type matching the arguments of primTrans.
defineTranspForFields
  :: (Maybe Term)            -- ^ PathCons, Δ.Φ ⊢ u : R δ
  -> (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
  -> QName       -- ^ some name, e.g. record name
  -> Telescope   -- ^ param types Δ
  -> Tele (Dom CType)   -- ^ fields' types Δ ⊢ Φ
  -> [Arg QName] -- ^ fields' names
  -> Type        -- ^ record type Δ ⊢ T
  -> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
defineTranspForFields :: Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom CType)
-> [Arg QName]
-> Type
-> TCM
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
defineTranspForFields Maybe Term
pathCons Term -> QName -> Term
applyProj QName
name Tele (Dom Type)
params Tele (Dom CType)
fsT [Arg QName]
fns Type
rect = do
  Type
interval <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
  let deltaI :: Tele (Dom Type)
deltaI = Type -> Tele (Dom Type) -> Tele (Dom Type)
expTelescope Type
interval Tele (Dom Type)
params
  Term
iz <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
  Term
io <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
  Term
imin <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMin"
  Term
imax <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMax"
  Term
ineg <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primINeg"
  Term
transp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
builtinTrans
  -- por <- getPrimitiveTerm "primPOr"
  -- one <- primItIsOne
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom Type)
params
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom Type)
deltaI
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom CType)
fsT

  let thePrefix :: ArgName
thePrefix = ArgName
"transp-"
  QName
theName <- ArgName -> TCMT IO QName
freshAbstractQName'_ forall a b. (a -> b) -> a -> b
$ ArgName
thePrefix forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
P.prettyShow (QName -> Name
A.qnameName QName
name)

  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"trans.rec" Nat
5 forall a b. (a -> b) -> a -> b
$ (ArgName
"Generated name: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show QName
theName forall a. [a] -> [a] -> [a]
++ ArgName
" " forall a. [a] -> [a] -> [a]
++ QName -> ArgName
showQNameId QName
theName)

  Type
theType <- (forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
deltaI forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
              NamesT (TCMT IO) (Abs Type)
rect' <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
x -> let NamesT Fail Term
_ = NamesT Fail Term
x forall a. a -> a -> a
`asTypeOf` forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. HasCallStack => a
undefined :: Term) in
                                                             forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
rect')
              forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
"phi" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
               (forall a. Subst a => Abs a -> SubstArg a -> a
absApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
rect' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (forall a. Subst a => Abs a -> SubstArg a -> a
absApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
rect' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)

  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
theType
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"sort = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall a. LensSort a => a -> Sort' Term
getSort Type
rect')

  Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
  forall a. TCM a -> TCM a
noMutualBlock forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
theName forall a b. (a -> b) -> a -> b
$
    (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
theName Type
theType Language
lang
       (Defn
emptyFunction { funTerminates :: Maybe Bool
funTerminates = forall a. a -> Maybe a
Just Bool
True }))
      { defNoCompilation :: Bool
defNoCompilation = Bool
True }
  -- ⊢ Γ = gamma = (δ : Δ^I) (φ : I) (u0 : R (δ i0))
  -- Γ ⊢     rtype = R (δ i1)
  TelV Tele (Dom Type)
gamma Type
rtype <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
theType


  let
      -- (γ : Γ) ⊢ transpR γ : rtype
      theTerm :: Term
theTerm = QName -> Elims -> Term
Def QName
theName [] forall t. Apply t => t -> [Arg Term] -> t
`apply` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma

      -- (γ : Γ) ⊢ (flatten Φ[δ i1])[n ↦ f_n (transpR γ)]
      clause_types :: [Dom CType]
clause_types = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Term
theTerm Term -> QName -> Term
`applyProj` (forall e. Arg e -> e
unArg Arg QName
fn)
                               | Arg QName
fn <- forall a. [a] -> [a]
reverse [Arg QName]
fns] forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
                       forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
0 Term
io forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom CType)
fsT') -- Γ, Φ[δ i1] ⊢ flatten Φ[δ i1]

      -- Γ, i : I ⊢ [δ i] : Δ
      delta_i :: Substitution' Term
delta_i = (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
deltaI)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) -- Defined but not used

      -- Γ, i : I ⊢ Φ[δ i]
      fsT' :: Tele (Dom CType)
fsT' = (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
deltaI)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params)  forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
               Tele (Dom CType)
fsT -- Δ ⊢ Φ
      lam_i :: Term -> Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ArgName -> a -> Abs a
Abs ArgName
"i"



      -- (δ , φ , u0) : Γ ⊢ φ : I
      -- the_phi = var 1
      -- -- (δ , φ , u0) : Γ ⊢ u0 : R (δ i0)
      -- the_u0  = var 0

      -- Γ' = (δ : Δ^I, φ : I)
      gamma' :: Tele (Dom Type)
gamma' = ListTel -> Tele (Dom Type)
telFromList forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
take (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- Nat
1) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
gamma

      -- δ : Δ^I, φ : F ⊢ [δ 0] : Δ
      d0 :: Substitution
      d0 :: Substitution' Term
d0 = forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
1 -- Δ^I, φ : F ⊢ Δ
                       (forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
iz forall a. Substitution' a
IdS forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) -- Δ^I ⊢ Δ
                                 -- Δ^I , i:I ⊢ sub params : Δ

      -- Ξ , Ξ ⊢ θ : Γ, Ξ ⊢ φ, Ξ ⊢ u : R (δ i0), Ξ ⊢ us : Φ[δ i0]
      (Tele (Dom Type)
tel,Substitution' Term
theta,Term
the_phi,Term
the_u0, [Term]
the_fields) =
        case Maybe Term
pathCons of
          -- (δ : Δ).Φ ⊢ u : R δ
          Just Term
u -> (forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
gamma' (Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CType -> Type
fromCType) Tele (Dom CType)
fsT) -- Ξ = δ : Δ^I, φ : F, _ : Φ[δ i0]
                    , (forall a. Nat -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Nat
size Tele (Dom CType)
fsT) Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u) forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
`consS` forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom CType)
fsT)
                    , forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Tele (Dom CType)
fsT) (Nat -> Term
var Nat
0)
                    , (forall a. Nat -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Nat
size Tele (Dom CType)
fsT) Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u)
                    , forall a. Nat -> [a] -> [a]
drop (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma') forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel)
          Maybe Term
Nothing -> (Tele (Dom Type)
gamma, forall a. Substitution' a
IdS, Nat -> Term
var Nat
1, Nat -> Term
var Nat
0, forall a b. (a -> b) -> [a] -> [b]
map (\ Arg QName
fname -> Nat -> Term
var Nat
0 Term -> QName -> Term
`applyProj` forall e. Arg e -> e
unArg Arg QName
fname) [Arg QName]
fns )

      fsT_tel :: Tele (Dom CType)
fsT_tel = (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
deltaI)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom CType)
fsT

      iMin :: Term -> Term -> Term
iMin Term
x Term
y = Term
imin forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
x, forall e. e -> Arg e
argN Term
y]
      iMax :: Term -> Term -> Term
iMax Term
x Term
y = Term
imax forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
x, forall e. e -> Arg e
argN Term
y]
      iNeg :: Term -> Term
iNeg Term
x = Term
ineg forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
x]

      -- .. ⊢ field : filled_ty' i0
      mkBody :: (Term, Dom CType) -> TCMT IO Term
mkBody (Term
field, Dom CType
filled_ty') = do
        let
          filled_ty :: Term
filled_ty = Term -> Term
lam_i forall a b. (a -> b) -> a -> b
$ (forall t a. Type'' t a -> a
unEl forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
fromCType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Dom CType
filled_ty'
          -- Γ ⊢ l : I -> Level of filled_ty
        -- sort <- reduce $ getSort $ unDom filled_ty'
        case forall t e. Dom' t e -> e
unDom Dom CType
filled_ty' of
          LType (LEl Level
l Term
_) -> do
            let lvl :: Term
lvl = Term -> Term
lam_i forall a b. (a -> b) -> a -> b
$ Level -> Term
Level Level
l
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ do
             NamesT Fail Term
lvl <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
lvl
             [NamesT Fail Term
phi,NamesT Fail Term
field] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
the_phi,Term
field]
             forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
transp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT Fail Term
lvl forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
filled_ty
                                 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
phi
                                 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
field
          -- interval arg
          ClosedType{}  ->
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ do
            [NamesT Fail Term
field] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
field]
            NamesT Fail Term
field

  let
        -- ' Ξ , i : I ⊢ τ = [(\ j → δ (i ∧ j)), φ ∨ ~ i, u] : Ξ
        tau :: Substitution' Term
tau = forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$ [Term]
us forall a. [a] -> [a] -> [a]
++ (Term
phi Term -> Term -> Term
`iMax` Term -> Term
iNeg (Nat -> Term
var Nat
0))
                        forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (\ Term
d -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
d forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Term
iMin (Nat -> Term
var Nat
0) (Nat -> Term
var Nat
1))]) [Term]
ds
         where
          -- Ξ, i : I
          ([Term]
us, Term
phi:[Term]
ds) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma') forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse (forall a. Subst a => Nat -> a -> a
raise Nat
1 (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg (forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel)))

  let
    go :: [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
go [Term]
acc [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
    go [Term]
acc ((Term
fname,Dom CType
field_ty) : [(Term, Dom CType)]
ps) = do
      -- Ξ, i : I, Φ[δ i]|_f ⊢ Φ_f = field_ty
      -- Ξ ⊢ b : field_ty [i := i1][acc]
      -- Ξ ⊢ parallesS acc : Φ[δ i1]|_f
      -- Ξ , i : I ⊢ τ = [(\ j → δ (i ∨ j), φ ∨ ~ i, us] : Ξ
      -- Ξ , i : I ⊢ parallesS (acc[τ]) : Φ[δ i1]|_f
      -- Ξ, i : I ⊢ field_ty [parallesS (acc[τ])]
      let
        filled_ty :: Dom CType
filled_ty = forall a. DeBruijn a => [a] -> Substitution' a
parallelS (Substitution' Term
tau forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Term]
acc) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Dom CType
field_ty
      Term
b <- (Term, Dom CType) -> TCMT IO Term
mkBody (Term
fname,Dom CType
filled_ty)
      [Term]
bs <- [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
go (Term
b forall a. a -> [a] -> [a]
: [Term]
acc) [(Term, Dom CType)]
ps
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term
b forall a. a -> [a] -> [a]
: [Term]
bs

  [Term]
bodys <- [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
go [] (forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
the_fields (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom CType)
fsT_tel)) -- ∀ f.  Ξ, i : I, Φ[δ i]|_f ⊢ Φ[δ i]_f
  let
    -- Ξ, i : I ⊢ ... : Δ.Φ
    theSubst :: Substitution' Term
theSubst = forall a. [a] -> [a]
reverse (Substitution' Term
tau forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Term]
bodys) forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
deltaI)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ((QName
theName, Tele (Dom Type)
tel, Substitution' Term
theta forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
rtype, forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CType -> Type
fromCType) [Dom CType]
clause_types, [Term]
bodys), Substitution' Term
theSubst)
  where
    -- record type in 'exponentiated' context
    -- (params : Δ^I), i : I |- T[params i]
    rect' :: Type
rect' = forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
rect
    -- Δ^I, i : I |- sub Δ : Δ
    sub :: a -> Substitution' Term
sub a
tel = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [ Nat -> Term
var Nat
n forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0] | Nat
n <- [Nat
1..forall a. Sized a => a -> Nat
size a
tel] ]
    -- given I type, and Δ telescope, build Δ^I such that
    -- (x : A, y : B x, ...)^I = (x : I → A, y : (i : I) → B (x i), ...)
    expTelescope :: Type -> Telescope -> Telescope
    expTelescope :: Type -> Tele (Dom Type) -> Tele (Dom Type)
expTelescope Type
int Tele (Dom Type)
tel = [ArgName] -> [Dom Type] -> Tele (Dom Type)
unflattenTel [ArgName]
names [Dom Type]
ys
      where
        xs :: [Dom Type]
xs = forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
        names :: [ArgName]
names = Tele (Dom Type) -> [ArgName]
teleNames Tele (Dom Type)
tel
        t :: Tele (Dom Type)
t = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall a. a -> Dom a
defaultDom forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) Type
int) (forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a. Tele a
EmptyTel)
        s :: Substitution' Term
s = forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
tel
        ys :: [Dom Type]
ys = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
s) [Dom Type]
xs

-- invariant: resulting tel Γ is such that Γ = (δ : Δ), (φ : I), (u : ...), (a0 : R δ))
--            where u and a0 have types matching the arguments of primHComp.
defineHCompForFields
  :: (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
  -> QName       -- ^ some name, e.g. record name
  -> Telescope   -- ^ param types Δ
  -> Tele (Dom LType)   -- ^ fields' types Δ ⊢ Φ
  -> [Arg QName] -- ^ fields' names
  -> LType        -- ^ record type (δ : Δ) ⊢ R[δ]
  -> TCM ((QName, Telescope, Type, [Dom Type], [Term]),Substitution)
defineHCompForFields :: (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom LType)
-> [Arg QName]
-> LType
-> TCM
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
defineHCompForFields Term -> QName -> Term
applyProj QName
name Tele (Dom Type)
params Tele (Dom LType)
fsT [Arg QName]
fns LType
rect = do
  Type
interval <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
  let delta :: Tele (Dom Type)
delta = Tele (Dom Type)
params
  Term
iz <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
  Term
io <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
  Term
imin <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMin"
  Term
imax <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMax"
  Term
tIMax <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMax"
  Term
ineg <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primINeg"
  Term
hcomp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
builtinHComp
  Term
transp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
builtinTrans
  Term
por <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primPOr"
  Term
one <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"comp.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom Type)
params
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"comp.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom Type)
delta
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"comp.rec" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom LType)
fsT

  let thePrefix :: ArgName
thePrefix = ArgName
"hcomp-"
  QName
theName <- ArgName -> TCMT IO QName
freshAbstractQName'_ forall a b. (a -> b) -> a -> b
$ ArgName
thePrefix forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
P.prettyShow (QName -> Name
A.qnameName QName
name)

  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"hcomp.rec" Nat
5 forall a b. (a -> b) -> a -> b
$ (ArgName
"Generated name: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show QName
theName forall a. [a] -> [a] -> [a]
++ ArgName
" " forall a. [a] -> [a] -> [a]
++ QName -> ArgName
showQNameId QName
theName)

  Type
theType <- (forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
delta forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
              NamesT (TCMT IO) Type
rect <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ LType -> Type
fromLType LType
rect
              forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
"phi" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType (\ NamesT (TCMT IO) Term
i ->
                forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
ArgName
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' ArgName
"o" NamesT (TCMT IO) Term
phi forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Type
rect) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
               NamesT (TCMT IO) Type
rect forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> NamesT (TCMT IO) Type
rect

  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
theType
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"sort = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (LType -> Level
lTypeLevel LType
rect)

  Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
  forall a. TCM a -> TCM a
noMutualBlock forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
theName forall a b. (a -> b) -> a -> b
$
    (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
theName Type
theType Language
lang
       (Defn
emptyFunction { funTerminates :: Maybe Bool
funTerminates = forall a. a -> Maybe a
Just Bool
True }))
      { defNoCompilation :: Bool
defNoCompilation = Bool
True }
  --   ⊢ Γ = gamma = (δ : Δ) (φ : I) (_ : (i : I) -> Partial φ (R δ)) (_ : R δ)
  -- Γ ⊢     rtype = R δ
  TelV Tele (Dom Type)
gamma Type
rtype <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
theType

  let -- Γ ⊢ R δ
      drect_gamma :: LType
drect_gamma = forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` LType
rect

  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"sort = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (LType -> Level
lTypeLevel LType
drect_gamma)

  let

      -- (γ : Γ) ⊢ hcompR γ : rtype
      compTerm :: Term
compTerm = QName -> Elims -> Term
Def QName
theName [] forall t. Apply t => t -> [Arg Term] -> t
`apply` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma

      -- (δ, φ, u, u0) : Γ ⊢ φ : I
      the_phi :: Term
the_phi = Nat -> Term
var Nat
2
      -- (δ, φ, u, u0) : Γ ⊢ u : (i : I) → [φ] → R (δ i)
      the_u :: Term
the_u   = Nat -> Term
var Nat
1
      -- (δ, φ, u, u0) : Γ ⊢ u0 : R (δ i0)
      the_u0 :: Term
the_u0  = Nat -> Term
var Nat
0

      -- ' (δ, φ, u, u0) : Γ ⊢ fillR Γ : (i : I) → rtype[ δ ↦ (\ j → δ (i ∧ j))]
      fillTerm :: Term
fillTerm = forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ do
        NamesT Fail Term
rect <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Type'' t a -> a
unEl  forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Type
fromLType  forall a b. (a -> b) -> a -> b
$ LType
drect_gamma
        NamesT Fail Term
lvl  <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level -> Term
Level forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Level
lTypeLevel forall a b. (a -> b) -> a -> b
$ LType
drect_gamma
        [NamesT Fail (Arg Term)]
params     <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
take (forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma
        [NamesT Fail Term
phi,NamesT Fail Term
w,NamesT Fail Term
w0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
the_phi,Term
the_u,Term
the_u0]
        -- (δ : Δ, φ : I, w : .., w0 : R δ) ⊢
        -- ' fillR Γ = λ i → hcompR δ (φ ∨ ~ i) (\ j → [ φ ↦ w (i ∧ j) , ~ i ↦ w0 ]) w0
        --           = hfillR δ φ w w0
        forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
i -> do
          [Arg Term]
args <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [NamesT Fail (Arg Term)]
params
          Term
psi  <- forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
imax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i)
          Term
u <- forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"j" (\ NamesT Fail Term
j -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
por forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT Fail Term
lvl
                                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
phi
                                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i)
                                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"_" (\ NamesT Fail Term
o -> NamesT Fail Term
rect)
                                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT Fail Term
w forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
imin forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
j))
                                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"_" (\ NamesT Fail Term
o -> NamesT Fail Term
w0) -- TODO wait for i = 0
                       )
          Term
u0 <- NamesT Fail Term
w0
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
theName [] forall t. Apply t => t -> [Arg Term] -> t
`apply` ([Arg Term]
args forall a. [a] -> [a] -> [a]
++ [forall e. e -> Arg e
argN Term
psi, forall e. e -> Arg e
argN Term
u, forall e. e -> Arg e
argN Term
u0])

      -- (γ : Γ) ⊢ (flatten Φ)[n ↦ f_n (compR γ)]
      clause_types :: [Dom LType]
clause_types = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Term
compTerm Term -> QName -> Term
`applyProj` (forall e. Arg e -> e
unArg Arg QName
fn)
                               | Arg QName
fn <- forall a. [a] -> [a]
reverse [Arg QName]
fns] forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
                       forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom LType)
fsT) -- Γ, Φ ⊢ flatten Φ
      -- Δ ⊢ Φ = fsT
      -- Γ, i : I ⊢ Φ'
      fsT' :: Tele (Dom LType)
fsT' = forall a. Nat -> Substitution' a
raiseS ((forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) forall a. Num a => a -> a -> a
+ Nat
1) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom LType)
fsT

      -- Γ, i : I ⊢ (flatten Φ')[n ↦ f_n (fillR Γ i)]
      filled_types :: [Dom LType]
filled_types = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
fillTerm forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0] Term -> QName -> Term
`applyProj` (forall e. Arg e -> e
unArg Arg QName
fn)
                               | Arg QName
fn <- forall a. [a] -> [a]
reverse [Arg QName]
fns] forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
                       forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom LType)
fsT' -- Γ, i : I, Φ' ⊢ flatten Φ'


  NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
comp <- do
        let
          imax :: NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
imax NamesT Fail Term
i NamesT Fail Term
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
j
        let forward :: NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
forward NamesT Fail Term
la NamesT Fail Term
bA NamesT Fail Term
r NamesT Fail Term
u = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
transp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT Fail Term
i -> NamesT Fail Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT Fail Term
i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
`imax` NamesT Fail Term
r))
                                            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT Fail Term
i -> NamesT Fail Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT Fail Term
i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
`imax` NamesT Fail Term
r))
                                            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
r
                                            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
u
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
la NamesT Fail Term
bA NamesT Fail Term
phi NamesT Fail Term
u NamesT Fail Term
u0 ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
hcomp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT Fail Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT Fail Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT Fail Term
phi
                      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT Fail Term
i -> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
o ->
                              NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
forward NamesT Fail Term
la NamesT Fail Term
bA NamesT Fail Term
i (NamesT Fail Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT Fail Term
o))
                      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
forward NamesT Fail Term
la NamesT Fail Term
bA (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) NamesT Fail Term
u0
  let
      mkBody :: (Arg QName, Dom LType) -> TCMT IO Term
mkBody (Arg QName
fname, Dom LType
filled_ty') = do
        let
          proj :: NamesT Fail Term -> NamesT Fail Term
proj NamesT Fail Term
t = (Term -> QName -> Term
`applyProj` forall e. Arg e -> e
unArg Arg QName
fname) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT Fail Term
t
          filled_ty :: Term
filled_ty = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a b. (a -> b) -> a -> b
$ (forall t a. Type'' t a -> a
unEl forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Type
fromLType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Dom LType
filled_ty')
          -- Γ ⊢ l : I -> Level of filled_ty
        Level
l <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ LType -> Level
lTypeLevel forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom LType
filled_ty'
        let lvl :: Term
lvl = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a b. (a -> b) -> a -> b
$ Level -> Term
Level Level
l)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ do
             NamesT Fail Term
lvl <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
lvl
             [NamesT Fail Term
phi,NamesT Fail Term
w,NamesT Fail Term
w0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
the_phi,Term
the_u,Term
the_u0]
             NamesT Fail Term
filled_ty <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
filled_ty

             NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
comp NamesT Fail Term
lvl
                  NamesT Fail Term
filled_ty
                  NamesT Fail Term
phi
                  (forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
i -> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
o -> NamesT Fail Term -> NamesT Fail Term
proj forall a b. (a -> b) -> a -> b
$ NamesT Fail Term
w forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
o) -- TODO wait for phi = 1
                  (NamesT Fail Term -> NamesT Fail Term
proj NamesT Fail Term
w0)

  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"filled_types sorts:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensSort a => a -> Sort' Term
getSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Type
fromLType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom LType]
filled_types)

  [Term]
bodys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Arg QName, Dom LType) -> TCMT IO Term
mkBody (forall a b. [a] -> [b] -> [(a, b)]
zip [Arg QName]
fns [Dom LType]
filled_types)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ((QName
theName, Tele (Dom Type)
gamma, Type
rtype, forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LType -> Type
fromLType) [Dom LType]
clause_types, [Term]
bodys),forall a. Substitution' a
IdS)


getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]
getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]
getGeneralizedParameters Set Name
gpars QName
name | forall a. Set a -> Bool
Set.null Set Name
gpars = forall (m :: * -> *) a. Monad m => a -> m a
return []
getGeneralizedParameters Set Name
gpars QName
name = do
  -- Drop the named parameters that shouldn't be in scope (if the user
  -- wrote a split data type)
  let inscope :: Name -> Maybe Name
inscope Name
x = Name
x forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a. Ord a => a -> Set a -> Bool
Set.member Name
x Set Name
gpars)
  forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> Maybe Name
inscope) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> [Maybe Name]
defGeneralizedParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name)

-- | Bind the named generalized parameters.
bindGeneralizedParameters :: [Maybe Name] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindGeneralizedParameters :: forall a.
[Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [] Type
t Tele (Dom Type) -> Type -> TCM a
ret = Tele (Dom Type) -> Type -> TCM a
ret forall a. Tele a
EmptyTel Type
t
bindGeneralizedParameters (Maybe Name
name : [Maybe Name]
names) Type
t Tele (Dom Type) -> Type -> TCM a
ret =
  case forall t a. Type'' t a -> a
unEl Type
t of
    Pi Dom Type
a Abs Type
b -> TCM a -> TCM a
ext forall a b. (a -> b) -> a -> b
$ forall a.
[Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [Maybe Name]
names (forall a. Abs a -> a
unAbs Abs Type
b) forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
tel Type
t -> Tele (Dom Type) -> Type -> TCM a
ret (forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Tele (Dom Type)
tel forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Abs Type
b)) Type
t
      where
        ext :: TCM a -> TCM a
ext | Just Name
x <- Maybe Name
name = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Name
x, Dom Type
a)
            | Bool
otherwise      = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. Abs a -> ArgName
absName Abs Type
b, Dom Type
a)
    Term
_      -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Bind the parameters of a datatype.
--
--   We allow omission of hidden parameters at the definition site.
--   Example:
--   @
--     data D {a} (A : Set a) : Set a
--     data D A where
--       c : A -> D A
--   @

bindParameters
  :: Int            -- ^ Number of parameters
  -> [A.LamBinding] -- ^ Bindings from definition site.
  -> Type           -- ^ Pi-type of bindings coming from signature site.
  -> (Telescope -> Type -> TCM a)
     -- ^ Continuation, accepting parameter telescope and rest of type.
     --   The parameters are part of the context when the continutation is invoked.
  -> TCM a

bindParameters :: forall a.
Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters Nat
0 [] Type
a Tele (Dom Type) -> Type -> TCM a
ret = Tele (Dom Type) -> Type -> TCM a
ret forall a. Tele a
EmptyTel Type
a

bindParameters Nat
0 (LamBinding
par : [LamBinding]
_) Type
_ Tele (Dom Type) -> Type -> TCM a
_ = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Unexpected parameter" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LamBinding
par

bindParameters Nat
npars [] Type
t Tele (Dom Type) -> Type -> TCM a
ret =
  case forall t a. Type'' t a -> a
unEl Type
t of
    Pi Dom Type
a Abs Type
b | Bool -> Bool
not (forall a. LensHiding a => a -> Bool
visible Dom Type
a) -> do
              Name
x <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (forall a. Abs a -> ArgName
absName Abs Type
b)
              forall a.
Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Nat
npars [] Name
x Dom Type
a Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret
           | Bool
otherwise ->
              forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Expected binding for parameter"
                    , forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Abs a -> ArgName
absName Abs Type
b) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t e. Dom' t e -> e
unDom Dom Type
a) ]
    Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

bindParameters Nat
npars par :: [LamBinding]
par@(A.DomainFull (A.TBind Range
_ TacticAttr
_ List1 (NamedArg Binder)
xs Expr
e) : [LamBinding]
bs) Type
a Tele (Dom Type) -> Type -> TCM a
ret =
  forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange [LamBinding]
par forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    let s :: ArgName
s | forall (t :: * -> *) a. Foldable t => t a -> Nat
length List1 (NamedArg Binder)
xs forall a. Ord a => a -> a -> Bool
> Nat
1 = ArgName
"s"
          | Bool
otherwise     = ArgName
""
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"Unexpected type signature for parameter" forall a. [a] -> [a] -> [a]
++ ArgName
s) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg Binder)
xs)

bindParameters Nat
_ (A.DomainFull A.TLet{} : [LamBinding]
_) Type
_ Tele (Dom Type) -> Type -> TCM a
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

bindParameters Nat
_ (par :: LamBinding
par@(A.DomainFree TacticAttr
_ NamedArg Binder
arg) : [LamBinding]
ps) Type
_ Tele (Dom Type) -> Type -> TCM a
_
  | forall a. LensModality a => a -> Modality
getModality NamedArg Binder
arg forall a. Eq a => a -> a -> Bool
/= Modality
defaultModality = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par forall a b. (a -> b) -> a -> b
$
     forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
       forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Unexpected modality/relevance annotation in" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LamBinding
par

bindParameters Nat
npars ps0 :: [LamBinding]
ps0@(par :: LamBinding
par@(A.DomainFree TacticAttr
_ NamedArg Binder
arg) : [LamBinding]
ps) Type
t Tele (Dom Type) -> Type -> TCM a
ret = do
  let x :: Binder
x          = forall a. NamedArg a -> a
namedArg NamedArg Binder
arg
      TelV Tele (Dom Type)
tel Type
_ = Type -> TelV Type
telView' Type
t
  case forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg Binder
arg forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel of
    ImplicitInsertion
NoInsertNeeded -> [LamBinding] -> Name -> TCM a
continue [LamBinding]
ps forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind forall a b. (a -> b) -> a -> b
$ forall a. Binder' a -> a
A.binderName Binder
x
    ImpInsert [Dom ()]
_    -> [LamBinding] -> Name -> TCM a
continue [LamBinding]
ps0 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (forall a. Abs a -> ArgName
absName Abs Type
b)
    ImplicitInsertion
BadImplicits   -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par forall a b. (a -> b) -> a -> b
$
     forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
       forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Unexpected parameter" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LamBinding
par
    NoSuchName ArgName
x   -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"No parameter of name " forall a. [a] -> [a] -> [a]
++ ArgName
x)
  where
    Pi dom :: Dom Type
dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info', unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b = forall t a. Type'' t a -> a
unEl Type
t -- TODO:: Defined but not used: info', a
    continue :: [LamBinding] -> Name -> TCM a
continue [LamBinding]
ps Name
x = forall a.
Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Nat
npars [LamBinding]
ps Name
x Dom Type
dom Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret

bindParameter :: Int -> [A.LamBinding] -> Name -> Dom Type -> Abs Type -> (Telescope -> Type -> TCM a) -> TCM a
bindParameter :: forall a.
Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Nat
npars [LamBinding]
ps Name
x Dom Type
a Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret =
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Name
x, Dom Type
a) forall a b. (a -> b) -> a -> b
$
    forall a.
Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters (Nat
npars forall a. Num a => a -> a -> a
- Nat
1) [LamBinding]
ps (forall a. Subst a => Abs a -> a
absBody Abs Type
b) forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
tel Type
s ->
      Tele (Dom Type) -> Type -> TCM a
ret (forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs (Name -> ArgName
nameToArgName Name
x) Tele (Dom Type)
tel) Type
s

-- | Check that the arguments to a constructor fits inside the sort of the datatype.
--   The third argument is the type of the constructor.
--
--   When @--without-K@ is active and the type is fibrant the
--   procedure also checks that the type is usable at the current
--   modality. See #4784 and #5434.
--
--   As a side effect, return the arity of the constructor.

fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Int
fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn UniverseCheck
uc [IsForced]
forceds Type
t Sort' Term
s = do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.fits" Nat
10 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"does" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        , TCMT IO Doc
"of sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. LensSort a => a -> Sort' Term
getSort Type
t)
        , TCMT IO Doc
"fit in" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort' Term
s forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"?"
        ]
  -- The code below would be simpler, but doesn't allow datatypes
  -- to be indexed by the universe level.
  -- s' <- instantiateFull (getSort t)
  -- noConstraints $ s' `leqSort` s

  Bool
withoutK <- forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
withoutK forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant Sort' Term
s) forall a b. (a -> b) -> a -> b
$ do
    Quantity
q <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Quantity TCEnv
eQuantity
    MonadConstraint (TCMT IO) => Modality -> Term -> TCM ()
usableAtModality (forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
q Modality
defaultModality) (forall t a. Type'' t a -> a
unEl Type
t)

  Bool -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn' Bool
withoutK [IsForced]
forceds Type
t Sort' Term
s
  where
  fitsIn' :: Bool -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn' Bool
withoutK [IsForced]
forceds Type
t Sort' Term
s = do
    Maybe (Bool, Dom Type, Abs Type)
vt <- do
      Either (Dom Type, Abs Type) Type
t <- forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi Type
t
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Either (Dom Type, Abs Type) Type
t of
                    Left (Dom Type
a,Abs Type
b)     -> forall a. a -> Maybe a
Just (Bool
True ,Dom Type
a,Abs Type
b)
                    Right (El Sort' Term
_ Term
t) | Pi Dom Type
a Abs Type
b <- Term
t
                                   -> forall a. a -> Maybe a
Just (Bool
False,Dom Type
a,Abs Type
b)
                    Either (Dom Type, Abs Type) Type
_              -> forall a. Maybe a
Nothing
    case Maybe (Bool, Dom Type, Abs Type)
vt of
      Just (Bool
isPath, Dom Type
dom, Abs Type
b) -> do
        let (IsForced
forced,[IsForced]
forceds') = [IsForced] -> (IsForced, [IsForced])
nextIsForced [IsForced]
forceds
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IsForced -> Bool
isForced IsForced
forced Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
withoutK) forall a b. (a -> b) -> a -> b
$ do
          Sort' Term
sa <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort' Term
getSort Dom Type
dom
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
isPath Bool -> Bool -> Bool
|| UniverseCheck
uc forall a. Eq a => a -> a -> Bool
== UniverseCheck
NoUniverseCheck Bool -> Bool -> Bool
|| Sort' Term
sa forall a. Eq a => a -> a -> Bool
== forall t. Sort' t
SizeUniv) forall a b. (a -> b) -> a -> b
$
            Sort' Term
sa forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
`leqSort` Sort' Term
s
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. Abs a -> ArgName
absName Abs Type
b, Dom Type
dom) forall a b. (a -> b) -> a -> b
$ do
          forall a. Enum a => a -> a
succ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn' Bool
withoutK [IsForced]
forceds' (forall a. Subst a => Abs a -> a
absBody Abs Type
b) (forall a. Subst a => Nat -> a -> a
raise Nat
1 Sort' Term
s)
      Maybe (Bool, Dom Type, Abs Type)
_ -> do
        forall a. LensSort a => a -> Sort' Term
getSort Type
t forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
`leqSort` Sort' Term
s
        forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0

-- | When --without-K is enabled, we should check that the sorts of
--   the index types fit into the sort of the datatype.
checkIndexSorts :: Sort -> Telescope -> TCM ()
checkIndexSorts :: Sort' Term -> Tele (Dom Type) -> TCM ()
checkIndexSorts Sort' Term
s = \case
  Tele (Dom Type)
EmptyTel -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel' -> do
    let sa :: Sort' Term
sa = forall a. LensSort a => a -> Sort' Term
getSort Dom Type
a
    -- Andreas, 2020-10-19, allow Size indices
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort' Term
sa forall a. Eq a => a -> a -> Bool
== forall t. Sort' t
SizeUniv) forall a b. (a -> b) -> a -> b
$ Sort' Term
sa forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
`leqSort` Sort' Term
s
    forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs (Tele (Dom Type))
tel' forall a b. (a -> b) -> a -> b
$ Sort' Term -> Tele (Dom Type) -> TCM ()
checkIndexSorts (forall a. Subst a => Nat -> a -> a
raise Nat
1 Sort' Term
s)

-- | Return the parameters that share variables with the indices
-- nonLinearParameters :: Int -> Type -> TCM [Int]
-- nonLinearParameters nPars t =

data IsPathCons = PathCons | PointCons
  deriving (IsPathCons -> IsPathCons -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsPathCons -> IsPathCons -> Bool
$c/= :: IsPathCons -> IsPathCons -> Bool
== :: IsPathCons -> IsPathCons -> Bool
$c== :: IsPathCons -> IsPathCons -> Bool
Eq,Nat -> IsPathCons -> ShowS
[IsPathCons] -> ShowS
IsPathCons -> ArgName
forall a.
(Nat -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [IsPathCons] -> ShowS
$cshowList :: [IsPathCons] -> ShowS
show :: IsPathCons -> ArgName
$cshow :: IsPathCons -> ArgName
showsPrec :: Nat -> IsPathCons -> ShowS
$cshowsPrec :: Nat -> IsPathCons -> ShowS
Show)

-- | Check that a type constructs something of the given datatype. The first
--   argument is the number of parameters to the datatype and the second the
--   number of additional non-parameters in the context (1 when generalizing, 0
--   otherwise).
--
constructs :: Int -> Int -> Type -> QName -> TCM IsPathCons
constructs :: Nat -> Nat -> Type -> QName -> TCM IsPathCons
constructs Nat
nofPars Nat
nofExtraVars Type
t QName
q = Nat -> Type -> TCM IsPathCons
constrT Nat
nofExtraVars Type
t
    where
        -- The number n counts the proper (non-parameter) constructor arguments.
        constrT :: Nat -> Type -> TCM IsPathCons
        constrT :: Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
t = do
            Type
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
            Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pathV <- forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf
            case forall t a. Type'' t a -> a
unEl Type
t of
                Pi Dom Type
_ (NoAbs ArgName
_ Type
b)  -> Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
b
                Pi Dom Type
a Abs Type
b            -> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b forall a b. (a -> b) -> a -> b
$ Nat -> Type -> TCM IsPathCons
constrT (Nat
n forall a. Num a => a -> a -> a
+ Nat
1)
                  -- OR: addCxtString (absName b) a $ constrT (n + 1) (absBody b)
                Term
_ | Left ((Dom Type
a,Abs Type
b),(Term, Term)
_) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pathV Type
t -> do
                      IsPathCons
_ <- case Abs Type
b of
                             NoAbs ArgName
_ Type
b -> Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
b
                             Abs Type
b         -> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b forall a b. (a -> b) -> a -> b
$ Nat -> Type -> TCM IsPathCons
constrT (Nat
n forall a. Num a => a -> a -> a
+ Nat
1)
                      forall (m :: * -> *) a. Monad m => a -> m a
return IsPathCons
PathCons
                Def QName
d Elims
es | QName
d forall a. Eq a => a -> a -> Bool
== QName
q -> do
                  let vs :: [Arg Term]
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
                  let ([Arg Term]
pars, [Arg Term]
ixs) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
nofPars [Arg Term]
vs
                  -- check that the constructor parameters are the data parameters
                  forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh Nat m) =>
Nat -> [Arg Term] -> m ()
checkParams Nat
n [Arg Term]
pars
                  forall (m :: * -> *) a. Monad m => a -> m a
return IsPathCons
PointCons
                MetaV{} -> do
                  Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
                  -- Analyse the type of q (name of the data type)
                  let td :: Type
td = Definition -> Type
defType Definition
def
                  TelV Tele (Dom Type)
tel Type
core <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
td
                  -- Construct the parameter arguments
                  -- The parameters are @n + nofPars - 1 .. n@
                  let us :: [Arg Term]
us = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg ArgName
arg Nat
x -> Nat -> Term
var Nat
x forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg ArgName
arg ) (forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Tele (Dom Type)
tel) forall a b. (a -> b) -> a -> b
$
                             forall a. Nat -> [a] -> [a]
take Nat
nofPars forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom (Nat
nofPars forall a. Num a => a -> a -> a
+ Nat
n)
                  -- The indices are fresh metas
                  [Arg Term]
xs <- forall (m :: * -> *). MonadMetaSolver m => Type -> m [Arg Term]
newArgsMeta forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
td [Arg Term]
us
                  let t' :: Type
t' = forall t a. Sort' t -> a -> Type'' t a
El (forall a. Subst a => Nat -> a -> a
raise Nat
n forall a b. (a -> b) -> a -> b
$ Defn -> Sort' Term
dataSort forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ [Arg Term]
us forall a. [a] -> [a] -> [a]
++ [Arg Term]
xs
                  -- Andreas, 2017-11-07, issue #2840
                  -- We should not postpone here, otherwise we might upset the positivity checker.
                  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t Type
t')
                      (Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
t')
                      (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldEndInApplicationOfTheDatatype Type
t)
                Term
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldEndInApplicationOfTheDatatype Type
t

        checkParams :: Nat -> [Arg Term] -> m ()
checkParams Nat
n [Arg Term]
vs = forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh Nat m) =>
Arg Term -> Nat -> m ()
sameVar [Arg Term]
vs [Nat]
ps
            where
                nvs :: Nat
nvs = forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Term]
vs
                ps :: [Nat]
ps  = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
take Nat
nvs [Nat
n..]

                sameVar :: Arg Term -> Nat -> m ()
sameVar Arg Term
arg Nat
i
                  -- skip irrelevant parameters
                  | forall a. LensRelevance a => a -> Bool
isIrrelevant Arg Term
arg = forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  | Bool
otherwise = do
                    Type
t <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Type
typeOfBV Nat
i
                    forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t (forall e. Arg e -> e
unArg Arg Term
arg) (Nat -> Term
var Nat
i)


-- | Is the type coinductive? Returns 'Nothing' if the answer cannot
-- be determined.

isCoinductive :: Type -> TCM (Maybe Bool)
isCoinductive :: Type -> TCM (Maybe Bool)
isCoinductive Type
t = do
  El Sort' Term
s Term
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  case Term
t of
    Def QName
q Elims
_ -> do
      Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      case Definition -> Defn
theDef Definition
def of
        Axiom       {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
        DataOrRecSig{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        Function    {} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        Datatype    {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
        Record      {  recInduction :: Defn -> Maybe Induction
recInduction = Just Induction
CoInductive } -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
True)
        Record      {  recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
_                } -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
        GeneralizableVar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        Constructor {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        Primitive   {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        PrimitiveSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        AbstractDefn{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Var   {} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Lam   {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Lit   {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Level {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Con   {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Pi    {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
    Sort  {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
    MetaV {} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    DontCare{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Dummy ArgName
s Elims
_  -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
ArgName -> m a
__IMPOSSIBLE_VERBOSE__ ArgName
s