{-# 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 =
    Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> [LamBinding] -> [Constructor] -> Call
CheckDataDef (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
name) QName
name [LamBinding]
ps [Constructor]
cs) (TCM () -> TCM ()) -> TCM () -> TCM ()
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 <- Definition -> TCMT IO Definition
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef (Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
        Type
t   <- Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
        let npars :: Int
npars =
              case Definition -> Defn
theDef Definition
def of
                DataOrRecSig Int
n -> Int
n
                Defn
_              -> Int
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 (TelV Type -> Type) -> TCMT IO (TelV Type) -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (TelV Type)
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
        Int
freeVars <- TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize

        -- The parameters are in scope when checking the constructors.
        Defn
dataDef <- [Maybe Name]
-> Type -> (Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn
forall a.
[Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [Maybe Name]
parNames Type
t ((Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn)
-> (Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn
forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
gtel Type
t0 ->
                   Int
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM Defn)
-> TCM Defn
forall a.
Int
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters (Int
npars Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Maybe Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Maybe Name]
parNames) [LamBinding]
ps Type
t0 ((Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn)
-> (Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn
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  = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
gtel Tele (Dom Type)
ptel
                tel' :: Tele (Dom Type)
tel' = Dom Type -> Dom Type
forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams (Dom Type -> Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
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 :: Int
nofIxs = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
ixTel

            Sort
s <- TCMT IO Sort -> TCMT IO Sort
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO Sort -> TCMT IO Sort) -> TCMT IO Sort -> TCMT IO Sort
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
s <- TCMT IO Sort
newSortMetaBelowInf
              TCM () -> (TCErr -> TCM ()) -> TCM ()
forall a. TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ (Tele (Dom Type) -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
ixTel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
s0 (Type -> TCM ()) -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise Int
nofIxs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort Sort
s) ((TCErr -> TCM ()) -> TCM ()) -> (TCErr -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ TCErr
err ->
                  if (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Int -> Type -> Bool
forall a. Free a => Int -> a -> Bool
`freeIn` Type
s0) [Int
0..Int
nofIxs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] then TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                     [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ TCMT IO Doc
"The sort of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO 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"
                          , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0
                          ]
                  else TCErr -> TCM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
              Sort -> TCMT IO Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s

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

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

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

            Impossible -> Int -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible Int
npars (TCM () -> TCM ()) -> TCM () -> TCM ()
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 <- [Constructor]
-> (Constructor -> TCMT IO (Maybe QName)) -> TCMT IO [Maybe QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Constructor]
cs ((Constructor -> TCMT IO (Maybe QName)) -> TCMT IO [Maybe QName])
-> (Constructor -> TCMT IO (Maybe QName)) -> TCMT IO [Maybe QName]
forall a b. (a -> b) -> a -> b
$ \ Constructor
c -> do
              IsPathCons
isPathCons <- QName
-> UniverseCheck
-> Tele (Dom Type)
-> Int
-> Sort
-> Constructor
-> TCM IsPathCons
checkConstructor QName
name UniverseCheck
uc Tele (Dom Type)
tel' Int
nofIxs Sort
s Constructor
c
              Maybe QName -> TCMT IO (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName -> TCMT IO (Maybe QName))
-> Maybe QName -> TCMT IO (Maybe QName)
forall a b. (a -> b) -> a -> b
$ if IsPathCons
isPathCons IsPathCons -> IsPathCons -> Bool
forall a. Eq a => a -> a -> Bool
== IsPathCons
PathCons then QName -> Maybe QName
forall a. a -> Maybe a
Just (Constructor -> QName
A.axiomName Constructor
c) else Maybe QName
forall a. Maybe a
Nothing

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

        let cons :: [QName]
cons   = (Constructor -> QName) -> [Constructor] -> [QName]
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 (Defn -> TCM ()) -> Defn -> TCM ()
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
forceSort Type
t = Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) TCMT IO Term -> (Term -> TCMT IO Sort) -> TCMT IO Sort
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Sort Sort
s -> Sort -> TCMT IO Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
  Term
_      -> do
    Sort
s <- TCMT IO Sort
newSortMetaBelowInf
    Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t (Sort -> Type
sort Sort
s)
    Sort -> TCMT IO Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
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)
-> Int
-> Sort
-> Constructor
-> TCM IsPathCons
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Int
nofIxs Sort
s (A.ScopedDecl ScopeInfo
scope [Constructor
con]) = do
  ScopeInfo -> TCM ()
setScope ScopeInfo
scope
  QName
-> UniverseCheck
-> Tele (Dom Type)
-> Int
-> Sort
-> Constructor
-> TCM IsPathCons
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Int
nofIxs Sort
s Constructor
con
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Int
nofIxs Sort
s con :: Constructor
con@(A.Axiom KindOfName
_ DefInfo
i ArgInfo
ai Maybe [Occurrence]
Nothing QName
c Expr
e) =
    Call -> TCM IsPathCons -> TCM IsPathCons
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Tele (Dom Type) -> Sort -> Constructor -> Call
CheckConstructor QName
d Tele (Dom Type)
tel Sort
s Constructor
con) (TCM IsPathCons -> TCM IsPathCons)
-> TCM IsPathCons -> TCM IsPathCons
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
-}
        QName -> Expr -> TCM ()
forall (m :: * -> *) a a.
(MonadDebug m, PrettyTCM a, PrettyTCM a) =>
a -> a -> m ()
debugEnter QName
c Expr
e
        -- check that we are relevant
        case ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai of
          Relevance
Relevant   -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Relevance
Irrelevant -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Irrelevant constructors are not supported"
          Relevance
NonStrict  -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Shape-irrelevant constructors are not supported"
        case ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai of
          Quantityω{} -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Quantity0{} -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Quantity1{} -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError (VerboseKey -> TypeError) -> VerboseKey -> TypeError
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Quantity-restricted constructors are not supported"
        -- check that the type of the constructor is well-formed
        (Type
t, IsPathCons
isPathCons) <- ArgInfo -> TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext ArgInfo
ai (TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons))
-> TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
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 IsPathCons -> IsPathCons -> Bool
forall a. Eq a => a -> a -> Bool
== IsPathCons
PointCons
                      then QName -> Type -> TCM [IsForced]
computeForcingAnnotations QName
c Type
t
                      else [IsForced] -> TCM [IsForced]
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)
        Sort -> TCM ()
forall (m :: * -> *) a. (MonadDebug m, PrettyTCM a) => a -> m ()
debugFitsIn Sort
s
        -- To allow propositional squash, we turn @Prop ℓ@ into @Set ℓ@
        -- for the purpose of checking the type of the constructors.
        let s' :: Sort
s' = case Sort
s of
              Prop Level' Term
l -> Level' Term -> Sort
forall t. Level' t -> Sort' t
Type Level' Term
l
              Sort
_      -> Sort
s
        Int
arity <- Call -> TCMT IO Int -> TCMT IO Int
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Type -> Sort -> Call
CheckConstructorFitsIn QName
c Type
t Sort
s') (TCMT IO Int -> TCMT IO Int) -> TCMT IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$
                 ArgInfo -> TCMT IO Int -> TCMT IO Int
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext ArgInfo
ai (TCMT IO Int -> TCMT IO Int) -> TCMT IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$
                 UniverseCheck -> [IsForced] -> Type -> Sort -> TCMT IO Int
fitsIn UniverseCheck
uc [IsForced]
forcedArgs Type
t Sort
s'
        -- this may have instantiated some metas in s, so we reduce
        Sort
s <- Sort -> TCMT IO Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s
        QName -> Type -> TCM ()
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) <- Int -> Type -> TCMT IO (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundaryP (-Int
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 <- TCMT IO (Tele (Dom Type))
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 <- [Int] -> (Int -> TCMT IO QName) -> TCMT IO [QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
0 .. Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
fields Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] ((Int -> TCMT IO QName) -> TCMT IO [QName])
-> (Int -> TCMT IO QName) -> TCMT IO [QName]
forall a b. (a -> b) -> a -> b
$ \ Int
i ->
              VerboseKey -> TCMT IO QName
freshAbstractQName'_ (VerboseKey -> TCMT IO QName) -> VerboseKey -> TCMT IO QName
forall a b. (a -> b) -> a -> b
$ Name -> VerboseKey
forall a. Pretty a => a -> VerboseKey
P.prettyShow (QName -> Name
A.qnameName QName
c) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"-" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Int -> VerboseKey
forall a. Show a => a -> VerboseKey
show Int
i

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

            VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.data.con.comp" Int
5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
              [ TCMT IO Doc
"params =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Tele (Dom Type)
params
              , TCMT IO Doc
"dataT  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
dataT
              , TCMT IO Doc
"fields =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Tele (Dom Type)
fields
              , TCMT IO Doc
"names  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO 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 ([Arg QName] -> ConHead) -> [Arg QName] -> ConHead
forall a b. (a -> b) -> a -> b
$ (QName -> Arg (VerboseKey, Type) -> Arg QName)
-> [QName] -> [Arg (VerboseKey, Type)] -> [Arg QName]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith QName -> Arg (VerboseKey, Type) -> Arg QName
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [QName]
names ([Arg (VerboseKey, Type)] -> [Arg QName])
-> [Arg (VerboseKey, Type)] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ (Dom' Term (VerboseKey, Type) -> Arg (VerboseKey, Type))
-> [Dom' Term (VerboseKey, Type)] -> [Arg (VerboseKey, Type)]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (VerboseKey, Type) -> Arg (VerboseKey, Type)
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term (VerboseKey, Type)] -> [Arg (VerboseKey, Type)])
-> [Dom' Term (VerboseKey, Type)] -> [Arg (VerboseKey, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, 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 Int
nofIxs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
|| (DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef)
                    then CompKit -> TCMT IO CompKit
forall (m :: * -> *) a. Monad m => a -> m a
return CompKit
emptyCompKit
                    else TCMT IO CompKit -> TCMT IO CompKit
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO CompKit -> TCMT IO CompKit)
-> TCMT IO CompKit -> TCMT IO CompKit
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
            (ConHead, CompKit, Maybe [QName])
-> TCMT IO (ConHead, CompKit, Maybe [QName])
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead
con, CompKit
comp, [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just [QName]
names)

        -- add parameters to constructor type and put into signature
        Impossible -> Int -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) (TCM () -> TCM ()) -> TCM () -> TCM ()
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) (Defn -> TCM ()) -> Defn -> TCM ()
forall a b. (a -> b) -> a -> b
$ Constructor :: Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> Induction
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Defn
Constructor
              { conPars :: Int
conPars   = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
              , conArity :: Int
conArity  = Int
arity
              , conSrcCon :: ConHead
conSrcCon = ConHead
con
              , conData :: QName
conData   = QName
d
              , conAbstr :: IsAbstract
conAbstr  = DefInfo -> IsAbstract
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 = Maybe [Bool]
forall a. Maybe a
Nothing  -- computed during compilation to treeless
              }

        -- Add the constructor to the instance table, if needed
        case DefInfo -> IsInstance
forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
i of
          InstanceDef Range
_r -> QName -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
c (TCM () -> TCM ()) -> TCM () -> TCM ()
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 -> () -> TCM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

        IsPathCons -> TCM IsPathCons
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 = ScopeInfo
-> TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
withScope_ ScopeInfo
s (TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons))
-> TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
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 :: Int -> Expr -> TCMT IO (Type, IsPathCons)
check Int
k Expr
e = do
            Type
t <- TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
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
            Int
n <- TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
            Type -> QName -> Int -> TCM ()
forall (m :: * -> *) a a a.
(MonadDebug m, PrettyTCM a, PrettyTCM a, Show a) =>
a -> a -> a -> m ()
debugEndsIn Type
t QName
d (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k)
            IsPathCons
isPathCons <- Int -> Int -> Type -> QName -> TCM IsPathCons
constructs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) Int
k Type
t QName
d
            (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
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) <- Set QName
-> TCMT IO (Type, IsPathCons)
-> TCM ([Maybe QName], Type, IsPathCons)
forall a.
Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' Set QName
s (Int -> Expr -> TCMT IO (Type, IsPathCons)
check Int
1 Expr
e)
          (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, IsPathCons
isPathCons)
        Expr
_ -> Int -> Expr -> TCMT IO (Type, IsPathCons)
check Int
0 Expr
e

    debugEnter :: a -> a -> m ()
debugEnter a
c a
e =
      VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.data.con" Int
5 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"checking constructor" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO 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 =
      VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.data.con" Int
15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"checking that"
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t
              , TCMT IO Doc
"ends in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
d
              ]
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"nofPars =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (a -> VerboseKey
forall a. Show a => a -> VerboseKey
show a
n)
        ]
    debugFitsIn :: a -> m ()
debugFitsIn a
s =
      VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.data.con" Int
15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"checking that the type fits in"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
s
        ]
    debugAdd :: a -> a -> m ()
debugAdd a
c a
t =
      VerboseKey -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.data.con" Int
5 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"adding constructor" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t
        ]
checkConstructor QName
_ UniverseCheck
_ Tele (Dom Type)
_ Int
_ Sort
_ Constructor
_ = TCM IsPathCons
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 <- (VerboseKey -> TCMT IO (Maybe Term))
-> [VerboseKey] -> TCMT IO [Maybe Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VerboseKey -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getTerm'
    [ VerboseKey
builtinInterval
    , VerboseKey
builtinIZero
    , VerboseKey
builtinIOne
    , VerboseKey
builtinIMin
    , VerboseKey
builtinIMax
    , VerboseKey
builtinINeg
    , VerboseKey
builtinPOr
    , VerboseKey
builtinItIsOne
    ]
  if Bool -> Bool
not ((Maybe Term -> Bool) -> [Maybe Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Term]
required) then CompKit -> TCMT IO CompKit
forall (m :: * -> *) a. Monad m => a -> m a
return (CompKit -> TCMT IO CompKit) -> CompKit -> TCMT IO CompKit
forall a b. (a -> b) -> a -> b
$ CompKit
emptyCompKit else do
    Maybe QName
hcomp  <- Bool
-> [VerboseKey] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
forall (m :: * -> *) (t :: * -> *) a.
(Traversable t, HasBuiltins m) =>
Bool -> t VerboseKey -> m (Maybe a) -> m (Maybe a)
whenDefined (Boundary -> Bool
forall a. Null a => a -> Bool
null Boundary
boundary) [VerboseKey
builtinHComp,VerboseKey
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 <- Bool
-> [VerboseKey] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
forall (m :: * -> *) (t :: * -> *) a.
(Traversable t, HasBuiltins m) =>
Bool -> t VerboseKey -> m (Maybe a) -> m (Maybe a)
whenDefined Bool
True            [VerboseKey
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)
    CompKit -> TCMT IO CompKit
forall (m :: * -> *) a. Monad m => a -> m a
return (CompKit -> TCMT IO CompKit) -> CompKit -> TCMT IO CompKit
forall a b. (a -> b) -> a -> b
$ CompKit :: Maybe QName -> Maybe QName -> CompKit
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 = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS [ Int -> Term
var Int
n Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0] | Int
n <- [Int
1..a -> Int
forall a. Sized a => a -> Int
size a
tel] ]
    withArgInfo :: Tele (Dom t) -> [e] -> [Arg e]
withArgInfo Tele (Dom t)
tel = (ArgInfo -> e -> Arg e) -> [ArgInfo] -> [e] -> [Arg e]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ArgInfo -> e -> Arg e
forall e. ArgInfo -> e -> Arg e
Arg ((Dom' Term (VerboseKey, t) -> ArgInfo)
-> [Dom' Term (VerboseKey, t)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (VerboseKey, t) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo ([Dom' Term (VerboseKey, t)] -> [ArgInfo])
-> (Tele (Dom t) -> [Dom' Term (VerboseKey, t)])
-> Tele (Dom t)
-> [ArgInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom t) -> [Dom' Term (VerboseKey, t)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList (Tele (Dom t) -> [ArgInfo]) -> Tele (Dom t) -> [ArgInfo]
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 -> Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
apply (QName -> Elims -> Term
Def QName
p []) [Term -> Arg Term
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
                 (Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Boundary -> Bool
forall a. Null a => a -> Bool
null Boundary
boundary) Maybe () -> Maybe Term -> Maybe Term
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term -> Maybe Term
forall a. a -> Maybe a
Just (ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Boundary -> Elims
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 ((QName -> Arg QName) -> [QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map QName -> Arg QName
forall e. e -> Arg e
argN [QName]
names) Type
t
      Maybe
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
   Substitution' Term)
-> TCMT IO (Maybe QName)
-> (((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
     Substitution' Term)
    -> TCMT IO (Maybe QName))
-> TCMT IO (Maybe QName)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
   Substitution' Term)
stuff (Maybe QName -> TCMT IO (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing) ((((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
   Substitution' Term)
  -> TCMT IO (Maybe QName))
 -> TCMT IO (Maybe QName))
-> (((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
     Substitution' Term)
    -> TCMT IO (Maybe QName))
-> TCMT IO (Maybe QName)
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 <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
      Term
body <- do
        case TranspOrHComp
cmd of
          TranspOrHComp
DoHComp -> Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Term] -> [Arg Term]
forall t e. Tele (Dom t) -> [e] -> [Arg e]
withArgInfo Tele (Dom Type)
fsT [Term]
bodies)
          TranspOrHComp
DoTransp | Boundary -> Bool
forall a. Null a => a -> Bool
null Boundary
boundary -> Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Term] -> [Arg Term]
forall t e. Tele (Dom t) -> [e] -> [Arg e]
withArgInfo Tele (Dom Type)
fsT [Term]
bodies)
                   | Bool
otherwise -> do
            Term
io <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
            Term
tIMax <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax
            Term
tIMin <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin
            Term
tINeg <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
            Term
tPOr  <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> TCMT IO (Maybe Term) -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getTerm' VerboseKey
builtinPOr
            Term
tHComp <- TCMT IO Term
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 (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Boundary -> Elims
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 = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
fsT) Substitution' Term
d0 Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u
                where
                  -- δ : Δ^I, φ : F ⊢ [δ 0] : Δ
                  d0 :: Substitution
                  d0 :: Substitution' Term
d0 = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
wkS Int
1 -- Δ^I, φ : F ⊢ Δ
                             (Term -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
iz Substitution' Term
forall a. Substitution' a
IdS Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Tele (Dom Type) -> Substitution' Term
forall a. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) -- Δ^I ⊢ Δ
                                       -- Δ^I , i:I ⊢ sub params : Δ
              the_phi :: Term
the_phi = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
fsT) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
              -- Γ ⊢ sigma : Δ.Φ
              -- sigma = [δ i1,bodies]
              sigma :: Substitution' Term
sigma = [Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
bodies [Term] -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Substitution' Term
d1
               where
                -- δ i1
                d1 :: Substitution
                d1 :: Substitution' Term
d1 = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
wkS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
params) -- Γ ⊢ Δ
                       (Term -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
io Substitution' Term
forall a. Substitution' a
IdS Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Tele (Dom Type) -> Substitution' Term
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 (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Substitution' Term
Substitution' (SubstArg Elims)
sigma Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom Type) -> Boundary -> Elims
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 = Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tIMax NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
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 = Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tINeg NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
r
              lvlOfType :: Type -> Term
lvlOfType = (\ (Type Level' Term
l) -> Level' Term -> Term
Level Level' Term
l) (Sort -> Term) -> (Type -> Sort) -> Type -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Sort
forall a. LensSort a => a -> Sort
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 = Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPOr NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Type -> Term
lvlOfType (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
la) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j
                                           NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> VerboseKey
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam VerboseKey
"o" (\ NamesT (TCMT IO) Term
_ -> Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
la) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
u0 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
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 = (Abs r -> SubstArg r -> r) -> m (Abs r) -> m (SubstArg r) -> m r
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Abs r -> SubstArg r -> r
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)) = [VerboseKey]
-> NamesT (TCMT IO) (Abs (Term, Term))
-> TCMT IO (Abs (Term, Term))
forall (m :: * -> *) a. [VerboseKey] -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) (Abs (Term, Term)) -> TCMT IO (Abs (Term, Term)))
-> NamesT (TCMT IO) (Abs (Term, Term))
-> TCMT IO (Abs (Term, Term))
forall a b. (a -> b) -> a -> b
$ do
                -- Γ
                NamesT (TCMT IO) Term
phi <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
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 <- Abs Type -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Type))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (VerboseKey -> Type -> Abs Type
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
"i" (Type -> Abs Type) -> Type -> Abs Type
forall a b. (a -> b) -> a -> b
$ (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 (Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
params)) Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Tele (Dom Type) -> Substitution' Term
forall a. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
t)

                VerboseKey
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Term, Term))
-> NamesT (TCMT IO) (Abs (Term, Term))
forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
VerboseKey -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind VerboseKey
"i" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Term, Term))
 -> NamesT (TCMT IO) (Abs (Term, Term)))
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Term, Term))
-> NamesT (TCMT IO) (Abs (Term, Term))
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] <- (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> [Term] -> NamesT (TCMT IO) [NamesT (TCMT IO) Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> (Term -> Term)
-> Term
-> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg 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 = TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans
                                          NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> VerboseKey
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam VerboseKey
"j" (\ NamesT (TCMT IO) Term
j -> Type -> Term
lvlOfType (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
ty NamesT (TCMT IO) (Abs Type)
-> NamesT (TCMT IO) (SubstArg Type) -> NamesT (TCMT IO) Type
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))
                                          NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> VerboseKey
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam VerboseKey
"j" (\ NamesT (TCMT IO) Term
j -> Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
ty NamesT (TCMT IO) (Abs Type)
-> NamesT (TCMT IO) (SubstArg Type) -> NamesT (TCMT IO) Type
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))
                                          NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
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)
                                          NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
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 NamesT (TCMT IO) (Abs Type)
-> NamesT (TCMT IO) (SubstArg Type) -> NamesT (TCMT IO) Type
forall (m :: * -> *) r.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` NamesT (TCMT IO) Term
NamesT (TCMT IO) (SubstArg Type)
i)
                              (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
r)
                              NamesT (TCMT IO) Term
r
                           (VerboseKey
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam VerboseKey
"o" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
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) (VerboseKey
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam VerboseKey
"o" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
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)
                  (Term, Term) -> NamesT (TCMT IO) (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term, Term) -> NamesT (TCMT IO) (Term, Term))
-> (Term, Term) -> NamesT (TCMT IO) (Term, Term)
forall a b. (a -> b) -> a -> b
$ (Term
psi, Term
alpha)

            -- Γ ⊢ Abs i. [(ψ_n,α_n : [ψ] → R (δ i))]
            [Abs (Term, Term)]
faces <- ((Term, (Term, Term)) -> TCMT IO (Abs (Term, Term)))
-> Boundary -> TCMT IO [Abs (Term, Term)]
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

            [VerboseKey] -> NamesT (TCMT IO) Term -> TCMT IO Term
forall (m :: * -> *) a. [VerboseKey] -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Term -> TCMT IO Term)
-> NamesT (TCMT IO) Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ do
                -- Γ
                NamesT (TCMT IO) Term
w1' <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
w1'
                NamesT (TCMT IO) Term
phi <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
the_phi
                NamesT (TCMT IO) Term
u   <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
the_u
                -- R (δ i1)
                NamesT (TCMT IO) Type
ty <- Type -> NamesT (TCMT IO) (NamesT (TCMT IO) Type)
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 <- (Abs (Term, Term)
 -> NamesT
      (TCMT IO) (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term)))
-> [Abs (Term, Term)]
-> NamesT
     (TCMT IO) [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Abs (Term, Term)
x -> (NamesT (TCMT IO) Term
 -> NamesT (TCMT IO) (Abs Term)
 -> (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term)))
-> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Term))
-> NamesT
     (TCMT IO) (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> (Abs Term -> Term)
-> Abs Term
-> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Impossible -> Abs Term -> Term
forall a. Subst a => Impossible -> Abs a -> a
noabsApp Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ (Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall a b. (a -> b) -> a -> b
$ ((Term, Term) -> Term) -> Abs (Term, Term) -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Term
forall a b. (a, b) -> a
fst Abs (Term, Term)
x) (Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Term))
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Term)))
-> Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Term))
forall a b. (a -> b) -> a -> b
$ ((Term, Term) -> Term) -> Abs (Term, Term) -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Term
forall a b. (a, b) -> b
snd Abs (Term, Term)
x)) [Abs (Term, Term)]
faces
                let
                  thePsi :: NamesT (TCMT IO) Term
thePsi = (NamesT (TCMT IO) Term
 -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> [NamesT (TCMT IO) Term] -> NamesT (TCMT IO) Term
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 (((NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
 -> NamesT (TCMT IO) Term)
-> [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
-> [NamesT (TCMT IO) Term]
forall a b. (a -> b) -> [a] -> [b]
map (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
-> NamesT (TCMT IO) Term
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 = Term -> NamesT (TCMT IO) Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Type -> Term
lvlOfType (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
ty)
                                                    NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
ty)
                                                    NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
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
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
sys
                                                    NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a0
                let
                 sys :: NamesT (TCMT IO) Term
sys = VerboseKey
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam VerboseKey
"i" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
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 NamesT (TCMT IO) (Abs Term)
-> NamesT (TCMT IO) (SubstArg Term) -> NamesT (TCMT IO) Term
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 NamesT (TCMT IO) (Abs Term)
-> NamesT (TCMT IO) (SubstArg Term) -> NamesT (TCMT IO) Term
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 = (NamesT (TCMT IO) Term
 -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> [NamesT (TCMT IO) Term] -> NamesT (TCMT IO) Term
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 (((NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
 -> NamesT (TCMT IO) Term)
-> [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
-> [NamesT (TCMT IO) Term]
forall a b. (a -> b) -> [a] -> [b]
map (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
-> NamesT (TCMT IO) Term
forall a b. (a, b) -> a
fst [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
xs)
                    recurse [] = NamesT (TCMT IO) Term
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 (VerboseKey
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam VerboseKey
"o" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
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 = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
wkS Int
1 -- Δ^I, φ : F ⊢ Δ
                       (Term -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
iz Substitution' Term
forall a. Substitution' a
IdS Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Tele (Dom Type) -> Substitution' Term
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 = ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' DBPatVar)]
-> Pattern' DBPatVar
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 Maybe (Arg Type)
forall a. Maybe a
Nothing Bool
False) ([NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar)
-> [NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar
forall a b. (a -> b) -> a -> b
$
               Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' DBPatVar)]
forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
telePatterns (Substitution' Term
Substitution' (SubstArg (Tele (Dom Type)))
d0 Substitution' (SubstArg (Tele (Dom Type)))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom Type)
fsT) (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
fsT) Substitution' Term
d0 Substitution' (SubstArg Boundary) -> Boundary -> Boundary
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 | Boundary -> Bool
forall a. Null a => a -> Bool
null Boundary
boundary = Tele (Dom Type) -> [NamedArg (Pattern' DBPatVar)]
forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
gamma
             | Bool
otherwise     = Int
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a. Int -> [a] -> [a]
take (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
fsT) (Tele (Dom Type) -> [NamedArg (Pattern' DBPatVar)]
forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
gamma) [NamedArg (Pattern' DBPatVar)]
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a. [a] -> [a] -> [a]
++ [Named NamedName (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
forall e. e -> Arg e
argN (Named NamedName (Pattern' DBPatVar)
 -> NamedArg (Pattern' DBPatVar))
-> Named NamedName (Pattern' DBPatVar)
-> NamedArg (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar)
forall a name. a -> Named name a
unnamed (Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar))
-> Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ Pattern' DBPatVar
up]
        clause :: Clause
clause = Clause :: Range
-> Range
-> Tele (Dom Type)
-> [NamedArg (Pattern' DBPatVar)]
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause
          { clauseTel :: Tele (Dom Type)
clauseTel         = Tele (Dom Type)
gamma
          , clauseType :: Maybe (Arg Type)
clauseType        = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type))
-> (Type -> Arg Type) -> Type -> Maybe (Arg Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Arg Type
forall e. e -> Arg e
argN (Type -> Maybe (Arg Type)) -> Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Type
ty
          , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats   = [NamedArg (Pattern' DBPatVar)]
pats
          , clauseFullRange :: Range
clauseFullRange   = Range
forall a. Range' a
noRange
          , clauseLHSRange :: Range
clauseLHSRange    = Range
forall a. Range' a
noRange
          , clauseCatchall :: Bool
clauseCatchall    = Bool
False
          , clauseBody :: Maybe Term
clauseBody        = Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Term
body
          , clauseExact :: Maybe Bool
clauseExact       = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
          , clauseRecursive :: Maybe Bool
clauseRecursive   = Maybe Bool
forall a. Maybe a
Nothing
              -- Andreas 2020-02-06 TODO
              -- Or: Just False;  is it known to be non-recursive?
          , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
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) <- TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
-> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Maybe (QName, Type)
-> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
compileClauses Maybe (QName, Type)
forall a. Maybe a
Nothing [Clause]
cs)
      Maybe SplitTree -> (SplitTree -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe SplitTree
mst ((SplitTree -> TCM ()) -> TCM ())
-> (SplitTree -> TCM ()) -> TCM ()
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
      Maybe QName -> TCMT IO (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName -> TCMT IO (Maybe QName))
-> Maybe QName -> TCMT IO (Maybe QName)
forall a b. (a -> b) -> a -> b
$ QName -> Maybe QName
forall a. a -> Maybe a
Just QName
theName

    whenDefined :: Bool -> t VerboseKey -> m (Maybe a) -> m (Maybe a)
whenDefined Bool
False t VerboseKey
_ m (Maybe a)
_ = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
    whenDefined Bool
True t VerboseKey
xs m (Maybe a)
m = do
      t (Maybe Term)
xs <- (VerboseKey -> m (Maybe Term))
-> t VerboseKey -> m (t (Maybe Term))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VerboseKey -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getTerm' t VerboseKey
xs
      if (Maybe Term -> Bool) -> t (Maybe Term) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust t (Maybe Term)
xs then m (Maybe a)
m else Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
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 [] Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0] | QName
f <- [QName] -> [QName]
forall a. [a] -> [a]
reverse [QName]
names ] [Term] -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1) Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
                    Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
fsT  -- Γ , Φ ⊢ Φ
    -- ⊢ Γ , (d : T)
    projTel :: Tele (Dom Type)
projTel    = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
params (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
t) (VerboseKey -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
"d" Tele (Dom Type)
forall a. Tele a
EmptyTel))
    np :: Int
np         = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
params

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

    VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.data.proj" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"proj" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Int, Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int
i,Dom Type
ty)
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
projName, TCMT IO Doc
":", Dom Type -> 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.
    TCM () -> TCM ()
forall a. TCM a -> TCM a
noMutualBlock (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      let cs :: [Clause]
cs = [ Clause
clause ]
      (Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- Maybe (QName, Type)
-> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
compileClauses Maybe (QName, Type)
forall a. Maybe a
Nothing [Clause]
cs
      let fun :: Defn
fun = Defn
emptyFunction
                { funClauses :: [Clause]
funClauses    = [Clause]
cs
                , funCompiled :: Maybe CompiledClauses
funCompiled   = CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just CompiledClauses
cc
                , funSplitTree :: Maybe SplitTree
funSplitTree  = Maybe SplitTree
mst
                , funProjection :: Maybe Projection
funProjection = Projection -> Maybe Projection
forall a. a -> Maybe a
Just (Projection -> Maybe Projection) -> Projection -> Maybe Projection
forall a b. (a -> b) -> a -> b
$ Projection :: Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
Projection
                    { projProper :: Maybe QName
projProper   = Maybe QName
forall a. Maybe a
Nothing
                    , projOrig :: QName
projOrig     = QName
projName
                    , projFromType :: Arg QName
projFromType = ArgInfo -> QName -> Arg QName
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom Type
ty) QName
dataName
                    , projIndex :: Int
projIndex    = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
                    , projLams :: ProjLams
projLams     = [Arg VerboseKey] -> ProjLams
ProjLams ([Arg VerboseKey] -> ProjLams) -> [Arg VerboseKey] -> ProjLams
forall a b. (a -> b) -> a -> b
$ (Dom' Term (VerboseKey, Type) -> Arg VerboseKey)
-> [Dom' Term (VerboseKey, Type)] -> [Arg VerboseKey]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term VerboseKey -> Arg VerboseKey
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term VerboseKey -> Arg VerboseKey)
-> (Dom' Term (VerboseKey, Type) -> Dom' Term VerboseKey)
-> Dom' Term (VerboseKey, Type)
-> Arg VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VerboseKey, Type) -> VerboseKey)
-> Dom' Term (VerboseKey, Type) -> Dom' Term VerboseKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey, Type) -> VerboseKey
forall a b. (a, b) -> a
fst) ([Dom' Term (VerboseKey, Type)] -> [Arg VerboseKey])
-> [Dom' Term (VerboseKey, Type)] -> [Arg VerboseKey]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
projTel
                    }
                , funMutual :: Maybe [QName]
funMutual     = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just []
                , funTerminates :: Maybe Bool
funTerminates = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                }
      Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
      TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
projName (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
        (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
projName (Dom Type -> Type
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]
          }

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


freshAbstractQName'_ :: String -> TCM QName
freshAbstractQName'_ :: VerboseKey -> TCMT IO QName
freshAbstractQName'_ = Fixity' -> Name -> TCMT IO QName
freshAbstractQName Fixity'
noFixity' (Name -> TCMT IO QName)
-> (VerboseKey -> Name) -> VerboseKey -> TCMT IO QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> 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
(LType -> LType -> Bool) -> (LType -> LType -> Bool) -> Eq LType
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,Int -> LType -> VerboseKey -> VerboseKey
[LType] -> VerboseKey -> VerboseKey
LType -> VerboseKey
(Int -> LType -> VerboseKey -> VerboseKey)
-> (LType -> VerboseKey)
-> ([LType] -> VerboseKey -> VerboseKey)
-> Show LType
forall a.
(Int -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [LType] -> VerboseKey -> VerboseKey
$cshowList :: [LType] -> VerboseKey -> VerboseKey
show :: LType -> VerboseKey
$cshow :: LType -> VerboseKey
showsPrec :: Int -> LType -> VerboseKey -> VerboseKey
$cshowsPrec :: Int -> LType -> VerboseKey -> VerboseKey
Show)

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

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

toLType :: MonadReduce m => Type -> m (Maybe LType)
toLType :: Type -> m (Maybe LType)
toLType Type
ty = do
  Sort
sort <- Sort -> m Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
ty
  case Sort
sort of
    Type Level' Term
l -> Maybe LType -> m (Maybe LType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LType -> m (Maybe LType)) -> Maybe LType -> m (Maybe LType)
forall a b. (a -> b) -> a -> b
$ LType -> Maybe LType
forall a. a -> Maybe a
Just (LType -> Maybe LType) -> LType -> Maybe LType
forall a b. (a -> b) -> a -> b
$ Level' Term -> Term -> LType
LEl Level' Term
l (Type -> Term
forall t a. Type'' t a -> a
unEl Type
ty)
    Sort
_      -> Maybe LType -> m (Maybe LType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LType -> m (Maybe LType)) -> Maybe LType -> m (Maybe LType)
forall a b. (a -> b) -> a -> b
$ Maybe LType
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' Term
l Term
t) = Level' Term -> Term -> LType
LEl (Substitution' (SubstArg (Level' Term))
-> Level' Term -> Level' Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Level' Term))
Substitution' (SubstArg LType)
rho Level' Term
l) (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
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
(CType -> CType -> Bool) -> (CType -> CType -> Bool) -> Eq CType
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,Int -> CType -> VerboseKey -> VerboseKey
[CType] -> VerboseKey -> VerboseKey
CType -> VerboseKey
(Int -> CType -> VerboseKey -> VerboseKey)
-> (CType -> VerboseKey)
-> ([CType] -> VerboseKey -> VerboseKey)
-> Show CType
forall a.
(Int -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [CType] -> VerboseKey -> VerboseKey
$cshowList :: [CType] -> VerboseKey -> VerboseKey
show :: CType -> VerboseKey
$cshow :: CType -> VerboseKey
showsPrec :: Int -> CType -> VerboseKey -> VerboseKey
$cshowsPrec :: Int -> CType -> VerboseKey -> VerboseKey
Show)

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

toCType :: MonadReduce m => Type -> m (Maybe CType)
toCType :: Type -> m (Maybe CType)
toCType Type
ty = do
  Sort
sort <- Sort -> m Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
ty
  case Sort
sort of
    Type Level' Term
l -> Maybe CType -> m (Maybe CType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
forall a b. (a -> b) -> a -> b
$ CType -> Maybe CType
forall a. a -> Maybe a
Just (CType -> Maybe CType) -> CType -> Maybe CType
forall a b. (a -> b) -> a -> b
$ LType -> CType
LType (Level' Term -> Term -> LType
LEl Level' Term
l (Type -> Term
forall t a. Type'' t a -> a
unEl Type
ty))
    SSet Level' Term
l  -> do
      Term
t <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
ty)
      case Term
t of
        Def QName
q [] -> Maybe CType -> m (Maybe CType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
forall a b. (a -> b) -> a -> b
$ CType -> Maybe CType
forall a. a -> Maybe a
Just (CType -> Maybe CType) -> CType -> Maybe CType
forall a b. (a -> b) -> a -> b
$ Sort -> QName -> CType
ClosedType (Level' Term -> Sort
forall t. Level' t -> Sort' t
SSet Level' Term
l) QName
q
        Term
_        -> Maybe CType -> m (Maybe CType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
forall a b. (a -> b) -> a -> b
$ Maybe CType
forall a. Maybe a
Nothing
    Sort
_      -> Maybe CType -> m (Maybe CType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
forall a b. (a -> b) -> a -> b
$ Maybe CType
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
s QName
t) = Sort -> QName -> CType
ClosedType (Substitution' (SubstArg Sort) -> Sort -> Sort
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Sort)
Substitution' (SubstArg CType)
rho Sort
s) QName
t
  applySubst Substitution' (SubstArg CType)
rho (LType LType
t) = LType -> CType
LType (LType -> CType) -> LType -> CType
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg LType) -> LType -> LType
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg CType)
Substitution' (SubstArg LType)
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 -> MaybeT
  (TCMT IO)
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
   Substitution' Term)
-> TCM
     (Maybe
        ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
         Substitution' Term))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
   (TCMT IO)
   ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
    Substitution' Term)
 -> TCM
      (Maybe
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)))
-> MaybeT
     (TCMT IO)
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
-> TCM
     (Maybe
        ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
         Substitution' Term))
forall a b. (a -> b) -> a -> b
$ do
         Tele (Dom' Term CType)
fsT' <- (Dom Type -> MaybeT (TCMT IO) (Dom' Term CType))
-> Tele (Dom Type) -> MaybeT (TCMT IO) (Tele (Dom' Term CType))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Type -> MaybeT (TCMT IO) CType)
-> Dom Type -> MaybeT (TCMT IO) (Dom' Term CType)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TCMT IO (Maybe CType) -> MaybeT (TCMT IO) CType
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe CType) -> MaybeT (TCMT IO) CType)
-> (Type -> TCMT IO (Maybe CType))
-> Type
-> MaybeT (TCMT IO) CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TCMT IO (Maybe CType)
forall (m :: * -> *). MonadReduce m => Type -> m (Maybe CType)
toCType)) Tele (Dom Type)
fsT
         TCMT
  IO
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
   Substitution' Term)
-> MaybeT
     (TCMT IO)
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT
   IO
   ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
    Substitution' Term)
 -> MaybeT
      (TCMT IO)
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term))
-> TCMT
     IO
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
-> MaybeT
     (TCMT IO)
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
forall a b. (a -> b) -> a -> b
$ Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom' Term CType)
-> [Arg QName]
-> Type
-> TCMT
     IO
     ((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' Term CType)
fsT' [Arg QName]
fns Type
rect
       TranspOrHComp
DoHComp -> MaybeT
  (TCMT IO)
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
   Substitution' Term)
-> TCM
     (Maybe
        ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
         Substitution' Term))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
   (TCMT IO)
   ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
    Substitution' Term)
 -> TCM
      (Maybe
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)))
-> MaybeT
     (TCMT IO)
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
-> TCM
     (Maybe
        ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
         Substitution' Term))
forall a b. (a -> b) -> a -> b
$ do
         Tele (Dom' Term LType)
fsT' <- (Dom Type -> MaybeT (TCMT IO) (Dom' Term LType))
-> Tele (Dom Type) -> MaybeT (TCMT IO) (Tele (Dom' Term LType))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Type -> MaybeT (TCMT IO) LType)
-> Dom Type -> MaybeT (TCMT IO) (Dom' Term LType)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType)
-> (Type -> TCMT IO (Maybe LType))
-> Type
-> MaybeT (TCMT IO) LType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TCMT IO (Maybe LType)
forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType)) Tele (Dom Type)
fsT
         LType
rect' <- TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType)
-> TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (Maybe LType)
forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType Type
rect
         TCMT
  IO
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
   Substitution' Term)
-> MaybeT
     (TCMT IO)
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT
   IO
   ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
    Substitution' Term)
 -> MaybeT
      (TCMT IO)
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term))
-> TCMT
     IO
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
-> MaybeT
     (TCMT IO)
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
forall a b. (a -> b) -> a -> b
$ (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom' Term LType)
-> [Arg QName]
-> LType
-> TCMT
     IO
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
defineHCompForFields Term -> QName -> Term
project QName
name Tele (Dom Type)
params Tele (Dom' Term 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' Term CType)
-> [Arg QName]
-> Type
-> TCMT
     IO
     ((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' Term CType)
fsT [Arg QName]
fns Type
rect = do
  Type
interval <- TCMT IO Type
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 <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
  Term
io <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
  Term
imin <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
"primIMin"
  Term
imax <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
"primIMax"
  Term
ineg <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
"primINeg"
  Term
transp <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
builtinTrans
  -- por <- getPrimitiveTerm "primPOr"
  -- one <- primItIsOne
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"trans.rec" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCMT IO Doc) -> VerboseKey -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> VerboseKey
forall a. Show a => a -> VerboseKey
show Tele (Dom Type)
params
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"trans.rec" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCMT IO Doc) -> VerboseKey -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> VerboseKey
forall a. Show a => a -> VerboseKey
show Tele (Dom Type)
deltaI
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"trans.rec" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCMT IO Doc) -> VerboseKey -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term CType) -> VerboseKey
forall a. Show a => a -> VerboseKey
show Tele (Dom' Term CType)
fsT

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

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

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

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

  Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
  TCM () -> TCM ()
forall a. TCM a -> TCM a
noMutualBlock (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
theName (Definition -> TCM ()) -> Definition -> TCM ()
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 = Bool -> Maybe Bool
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 <- Type -> TCMT IO (TelV Type)
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 [] Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` Tele (Dom Type) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma

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

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

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



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

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

      -- δ : Δ^I, φ : F ⊢ [δ 0] : Δ
      d0 :: Substitution
      d0 :: Substitution' Term
d0 = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
wkS Int
1 -- Δ^I, φ : F ⊢ Δ
                       (Term -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
iz Substitution' Term
forall a. Substitution' a
IdS Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Tele (Dom Type) -> Substitution' Term
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 -> (Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
gamma' (Substitution' Term
Substitution' (SubstArg (Tele (Dom Type)))
d0 Substitution' (SubstArg (Tele (Dom Type)))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` (Dom' Term CType -> Dom Type)
-> Tele (Dom' Term CType) -> Tele (Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((CType -> Type) -> Dom' Term CType -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CType -> Type
fromCType) Tele (Dom' Term CType)
fsT) -- Ξ = δ : Δ^I, φ : F, _ : Φ[δ i0]
                    , (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom' Term CType) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term CType)
fsT) Substitution' Term
d0 Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u) Term -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
`consS` Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS (Tele (Dom' Term CType) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term CType)
fsT)
                    , Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Tele (Dom' Term CType) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term CType)
fsT) (Int -> Term
var Int
0)
                    , (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom' Term CType) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term CType)
fsT) Substitution' Term
d0 Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u)
                    , Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
drop (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma') ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel)
          Maybe Term
Nothing -> (Tele (Dom Type)
gamma, Substitution' Term
forall a. Substitution' a
IdS, Int -> Term
var Int
1, Int -> Term
var Int
0, (Arg QName -> Term) -> [Arg QName] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ Arg QName
fname -> Int -> Term
var Int
0 Term -> QName -> Term
`applyProj` Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
fname) [Arg QName]
fns )

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

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

      -- .. ⊢ field : filled_ty' i0
      mkBody :: (Term, Dom' Term CType) -> TCMT IO Term
mkBody (Term
field, Dom' Term CType
filled_ty') = do
        let
          filled_ty :: Term
filled_ty = Term -> Term
lam_i (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term)
-> (Dom' Term CType -> Type) -> Dom' Term CType -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
fromCType (CType -> Type)
-> (Dom' Term CType -> CType) -> Dom' Term CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term CType -> CType
forall t e. Dom' t e -> e
unDom) Dom' Term CType
filled_ty'
          -- Γ ⊢ l : I -> Level of filled_ty
        -- sort <- reduce $ getSort $ unDom filled_ty'
        case Dom' Term CType -> CType
forall t e. Dom' t e -> e
unDom Dom' Term CType
filled_ty' of
          LType (LEl Level' Term
l Term
_) -> do
            let lvl :: Term
lvl = Term -> Term
lam_i (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level Level' Term
l
            Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> NamesT Fail Term -> Term
forall a. [VerboseKey] -> NamesT Fail a -> a
runNames [] (NamesT Fail Term -> Term) -> NamesT Fail Term -> Term
forall a b. (a -> b) -> a -> b
$ do
             NamesT Fail Term
lvl <- Term -> NamesT Fail (NamesT Fail Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
lvl
             [NamesT Fail Term
phi,NamesT Fail Term
field] <- (Term -> NamesT Fail (NamesT Fail Term))
-> [Term] -> NamesT Fail [NamesT Fail Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> NamesT Fail (NamesT Fail Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
the_phi,Term
field]
             Term -> NamesT Fail Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
transp NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT Fail Term
lvl NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT Fail Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
filled_ty
                                 NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
phi
                                 NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
field
          -- interval arg
          ClosedType{}  ->
            Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> NamesT Fail Term -> Term
forall a. [VerboseKey] -> NamesT Fail a -> a
runNames [] (NamesT Fail Term -> Term) -> NamesT Fail Term -> Term
forall a b. (a -> b) -> a -> b
$ do
            [NamesT Fail Term
field] <- (Term -> NamesT Fail (NamesT Fail Term))
-> [Term] -> NamesT Fail [NamesT Fail Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> NamesT Fail (NamesT Fail Term)
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 = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [Term]
us [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ (Term
phi Term -> Term -> Term
`iMax` Term -> Term
iNeg (Int -> Term
var Int
0))
                        Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ Term
d -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Term -> Abs Term
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
"i" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
d Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Term
iMin (Int -> Term
var Int
0) (Int -> Term
var Int
1))]) [Term]
ds
         where
          -- Ξ, i : I
          ([Term]
us, Term
phi:[Term]
ds) = Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma') ([Term] -> ([Term], [Term])) -> [Term] -> ([Term], [Term])
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse (Int -> [Term] -> [Term]
forall a. Subst a => Int -> a -> a
raise Int
1 ((Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg (Tele (Dom Type) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel)))

  let
    go :: [Term] -> [(Term, Dom' Term CType)] -> TCMT IO [Term]
go [Term]
acc [] = [Term] -> TCMT IO [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    go [Term]
acc ((Term
fname,Dom' Term CType
field_ty) : [(Term, Dom' Term 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' Term CType
filled_ty = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS (Substitution' Term
Substitution' (SubstArg [Term])
tau Substitution' (SubstArg [Term]) -> [Term] -> [Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Term]
acc) Substitution' (SubstArg (Dom' Term CType))
-> Dom' Term CType -> Dom' Term CType
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Dom' Term CType
field_ty
      Term
b <- (Term, Dom' Term CType) -> TCMT IO Term
mkBody (Term
fname,Dom' Term CType
filled_ty)
      [Term]
bs <- [Term] -> [(Term, Dom' Term CType)] -> TCMT IO [Term]
go (Term
b Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
acc) [(Term, Dom' Term CType)]
ps
      [Term] -> TCMT IO [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$ Term
b Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
bs

  [Term]
bodys <- [Term] -> [(Term, Dom' Term CType)] -> TCMT IO [Term]
go [] ([Term] -> [Dom' Term CType] -> [(Term, Dom' Term CType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
the_fields ((Dom' Term (VerboseKey, CType) -> Dom' Term CType)
-> [Dom' Term (VerboseKey, CType)] -> [Dom' Term CType]
forall a b. (a -> b) -> [a] -> [b]
map (((VerboseKey, CType) -> CType)
-> Dom' Term (VerboseKey, CType) -> Dom' Term CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey, CType) -> CType
forall a b. (a, b) -> b
snd) ([Dom' Term (VerboseKey, CType)] -> [Dom' Term CType])
-> [Dom' Term (VerboseKey, CType)] -> [Dom' Term CType]
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term CType) -> [Dom' Term (VerboseKey, CType)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom' Term CType)
fsT_tel)) -- ∀ f.  Ξ, i : I, Φ[δ i]|_f ⊢ Φ[δ i]_f
  let
    -- Ξ, i : I ⊢ ... : Δ.Φ
    theSubst :: Substitution' Term
theSubst = [Term] -> [Term]
forall a. [a] -> [a]
reverse (Substitution' Term
Substitution' (SubstArg [Term])
tau Substitution' (SubstArg [Term]) -> [Term] -> [Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Term]
bodys) [Term] -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 (Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
deltaI)) Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Tele (Dom Type) -> Substitution' Term
forall a. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params)
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
 Substitution' Term)
-> TCMT
     IO
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
  Substitution' Term)
 -> TCMT
      IO
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term))
-> ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
    Substitution' Term)
-> TCMT
     IO
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
forall a b. (a -> b) -> a -> b
$ ((QName
theName, Tele (Dom Type)
tel, Substitution' Term
Substitution' (SubstArg Type)
theta Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
rtype, (Dom' Term CType -> Dom Type) -> [Dom' Term CType] -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map ((CType -> Type) -> Dom' Term CType -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CType -> Type
fromCType) [Dom' Term CType]
clause_types, [Term]
bodys), Substitution' Term
theSubst)
  where
    -- record type in 'exponentiated' context
    -- (params : Δ^I), i : I |- T[params i]
    rect' :: Type
rect' = Tele (Dom Type) -> Substitution' Term
forall a. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
rect
    -- Δ^I, i : I |- sub Δ : Δ
    sub :: a -> Substitution' Term
sub a
tel = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS [ Int -> Term
var Int
n Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0] | Int
n <- [Int
1..a -> Int
forall a. Sized a => a -> Int
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 = [VerboseKey] -> [Dom Type] -> Tele (Dom Type)
unflattenTel [VerboseKey]
names [Dom Type]
ys
      where
        xs :: [Dom Type]
xs = Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
        names :: [VerboseKey]
names = Tele (Dom Type) -> [VerboseKey]
teleNames Tele (Dom Type)
tel
        t :: Tele (Dom Type)
t = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall a. a -> Dom a
defaultDom (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) Type
int) (VerboseKey -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
"i" Tele (Dom Type)
forall a. Tele a
EmptyTel)
        s :: Substitution' Term
s = Tele (Dom Type) -> Substitution' Term
forall a. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
tel
        ys :: [Dom Type]
ys = (Dom Type -> Dom Type) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> Dom Type -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
t) (Dom Type -> Dom Type)
-> (Dom Type -> Dom Type) -> Dom Type -> Dom Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Dom Type))
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' Term LType)
-> [Arg QName]
-> LType
-> TCMT
     IO
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
defineHCompForFields Term -> QName -> Term
applyProj QName
name Tele (Dom Type)
params Tele (Dom' Term LType)
fsT [Arg QName]
fns LType
rect = do
  Type
interval <- TCMT IO Type
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 <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
  Term
io <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
  Term
imin <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
"primIMin"
  Term
imax <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
"primIMax"
  Term
tIMax <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
"primIMax"
  Term
ineg <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
"primINeg"
  Term
hcomp <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
builtinHComp
  Term
transp <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
builtinTrans
  Term
por <- VerboseKey -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
VerboseKey -> m Term
getPrimitiveTerm VerboseKey
"primPOr"
  Term
one <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"comp.rec" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCMT IO Doc) -> VerboseKey -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> VerboseKey
forall a. Show a => a -> VerboseKey
show Tele (Dom Type)
params
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"comp.rec" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCMT IO Doc) -> VerboseKey -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> VerboseKey
forall a. Show a => a -> VerboseKey
show Tele (Dom Type)
delta
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"comp.rec" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCMT IO Doc) -> VerboseKey -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term LType) -> VerboseKey
forall a. Show a => a -> VerboseKey
show Tele (Dom' Term LType)
fsT

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

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

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

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

  Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
  TCM () -> TCM ()
forall a. TCM a -> TCM a
noMutualBlock (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
theName (Definition -> TCM ()) -> Definition -> TCM ()
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 = Bool -> Maybe Bool
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 <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
theType

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

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

  let

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

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

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

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

      -- Γ, i : I ⊢ (flatten Φ')[n ↦ f_n (fillR Γ i)]
      filled_types :: [Dom' Term LType]
filled_types = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
fillTerm Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0] Term -> QName -> Term
`applyProj` (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
fn)
                               | Arg QName
fn <- [Arg QName] -> [Arg QName]
forall a. [a] -> [a]
reverse [Arg QName]
fns] Substitution' (SubstArg [Dom' Term LType])
-> [Dom' Term LType] -> [Dom' Term LType]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
                       Tele (Dom' Term LType) -> [Dom' Term LType]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom' Term 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 = Term -> NamesT Fail Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tIMax NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
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 = Term -> NamesT Fail Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
transp NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> VerboseKey
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam VerboseKey
"i" (\ NamesT Fail Term
i -> NamesT Fail Term
la NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
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))
                                            NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> VerboseKey
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam VerboseKey
"i" (\ NamesT Fail Term
i -> NamesT Fail Term
bA NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
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))
                                            NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
r
                                            NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
u
        (NamesT Fail Term
 -> NamesT Fail Term
 -> NamesT Fail Term
 -> NamesT Fail Term
 -> NamesT Fail Term
 -> NamesT Fail Term)
-> TCMT
     IO
     (NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((NamesT Fail Term
  -> NamesT Fail Term
  -> NamesT Fail Term
  -> NamesT Fail Term
  -> NamesT Fail Term
  -> NamesT Fail Term)
 -> TCMT
      IO
      (NamesT Fail Term
       -> NamesT Fail Term
       -> NamesT Fail Term
       -> NamesT Fail Term
       -> NamesT Fail Term
       -> NamesT Fail Term))
-> (NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term)
-> TCMT
     IO
     (NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term)
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 ->
          Term -> NamesT Fail Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
hcomp NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT Fail Term
la NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT Fail Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT Fail Term
bA NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> NamesT Fail Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT Fail Term
phi
                      NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> VerboseKey
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam VerboseKey
"i" (\ NamesT Fail Term
i -> VerboseKey
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam VerboseKey
"o" ((NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term)
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
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 NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT Fail Term
o))
                      NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
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 (Term -> NamesT Fail Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) NamesT Fail Term
u0
  let
      mkBody :: (Arg QName, Dom' Term LType) -> TCMT IO Term
mkBody (Arg QName
fname, Dom' Term LType
filled_ty') = do
        let
          proj :: NamesT Fail Term -> NamesT Fail Term
proj NamesT Fail Term
t = (Term -> QName -> Term
`applyProj` Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
fname) (Term -> Term) -> NamesT Fail Term -> NamesT Fail Term
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 (VerboseKey -> Term -> Abs Term
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
"i" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term)
-> (Dom' Term LType -> Type) -> Dom' Term LType -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Type
fromLType (LType -> Type)
-> (Dom' Term LType -> LType) -> Dom' Term LType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term LType -> LType
forall t e. Dom' t e -> e
unDom) Dom' Term LType
filled_ty')
          -- Γ ⊢ l : I -> Level of filled_ty
        Level' Term
l <- Level' Term -> TCMT IO (Level' Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Level' Term -> TCMT IO (Level' Term))
-> Level' Term -> TCMT IO (Level' Term)
forall a b. (a -> b) -> a -> b
$ LType -> Level' Term
lTypeLevel (LType -> Level' Term) -> LType -> Level' Term
forall a b. (a -> b) -> a -> b
$ Dom' Term LType -> LType
forall t e. Dom' t e -> e
unDom Dom' Term LType
filled_ty'
        let lvl :: Term
lvl = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (VerboseKey -> Term -> Abs Term
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
"i" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level Level' Term
l)
        Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> NamesT Fail Term -> Term
forall a. [VerboseKey] -> NamesT Fail a -> a
runNames [] (NamesT Fail Term -> Term) -> NamesT Fail Term -> Term
forall a b. (a -> b) -> a -> b
$ do
             NamesT Fail Term
lvl <- Term -> NamesT Fail (NamesT Fail Term)
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] <- (Term -> NamesT Fail (NamesT Fail Term))
-> [Term] -> NamesT Fail [NamesT Fail Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> NamesT Fail (NamesT Fail Term)
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 <- Term -> NamesT Fail (NamesT Fail Term)
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
                  (VerboseKey
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam VerboseKey
"i" ((NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term)
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
i -> VerboseKey
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
VerboseKey -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam VerboseKey
"o" ((NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term)
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
o -> NamesT Fail Term -> NamesT Fail Term
proj (NamesT Fail Term -> NamesT Fail Term)
-> NamesT Fail Term -> NamesT Fail Term
forall a b. (a -> b) -> a -> b
$ NamesT Fail Term
w NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
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)

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

  [Term]
bodys <- ((Arg QName, Dom' Term LType) -> TCMT IO Term)
-> [(Arg QName, Dom' Term LType)] -> TCMT IO [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Arg QName, Dom' Term LType) -> TCMT IO Term
mkBody ([Arg QName] -> [Dom' Term LType] -> [(Arg QName, Dom' Term LType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Arg QName]
fns [Dom' Term LType]
filled_types)
  ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
 Substitution' Term)
-> TCMT
     IO
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
  Substitution' Term)
 -> TCMT
      IO
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term))
-> ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
    Substitution' Term)
-> TCMT
     IO
     ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
forall a b. (a -> b) -> a -> b
$ ((QName
theName, Tele (Dom Type)
gamma, Type
rtype, (Dom' Term LType -> Dom Type) -> [Dom' Term LType] -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map ((LType -> Type) -> Dom' Term LType -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LType -> Type
fromLType) [Dom' Term LType]
clause_types, [Term]
bodys),Substitution' Term
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 | Set Name -> Bool
forall a. Set a -> Bool
Set.null Set Name
gpars = [Maybe Name] -> TCM [Maybe Name]
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 Name -> Maybe () -> Maybe Name
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name
x Set Name
gpars)
  (Maybe Name -> Maybe Name) -> [Maybe Name] -> [Maybe Name]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Name -> (Name -> Maybe Name) -> Maybe Name
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> Maybe Name
inscope) ([Maybe Name] -> [Maybe Name])
-> (Definition -> [Maybe Name]) -> Definition -> [Maybe Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> [Maybe Name]
defGeneralizedParams (Definition -> [Maybe Name])
-> TCMT IO Definition -> TCM [Maybe Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Definition -> TCMT IO Definition
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef (Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
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 :: [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 Tele (Dom Type)
forall a. Tele a
EmptyTel Type
t
bindGeneralizedParameters (Maybe Name
name : [Maybe Name]
names) Type
t Tele (Dom Type) -> Type -> TCM a
ret =
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Pi Dom Type
a Abs Type
b -> TCM a -> TCM a
ext (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ [Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
forall a.
[Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [Maybe Name]
names (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b) ((Tele (Dom Type) -> Type -> TCM a) -> TCM a)
-> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
tel Type
t -> Tele (Dom Type) -> Type -> TCM a
ret (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Tele (Dom Type)
tel Tele (Dom Type) -> Abs Type -> Abs (Tele (Dom Type))
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 = (Name, Dom Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Name
x, Dom Type
a)
            | Bool
otherwise      = (VerboseKey, Dom Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b, Dom Type
a)
    Term
_      -> TCM a
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 :: Int
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters Int
0 [] Type
a Tele (Dom Type) -> Type -> TCM a
ret = Tele (Dom Type) -> Type -> TCM a
ret Tele (Dom Type)
forall a. Tele a
EmptyTel Type
a

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

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

bindParameters Int
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 =
  [LamBinding] -> TCM a -> TCM a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange [LamBinding]
par (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
  TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    let s :: VerboseKey
s | List1 (NamedArg Binder) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 (NamedArg Binder)
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 = VerboseKey
"s"
          | Bool
otherwise     = VerboseKey
""
    VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"Unexpected type signature for parameter" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
s) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((NamedArg Binder -> TCMT IO Doc)
-> List1 (NamedArg Binder) -> NonEmpty (TCMT IO Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg Binder -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg Binder)
xs)

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

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

bindParameters Int
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          = NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
arg
      TelV Tele (Dom Type)
tel Type
_ = Type -> TelV Type
telView' Type
t
  case NamedArg Binder
-> [Dom' Term (VerboseKey, Type)] -> ImplicitInsertion
forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg Binder
arg ([Dom' Term (VerboseKey, Type)] -> ImplicitInsertion)
-> [Dom' Term (VerboseKey, Type)] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Tele (Dom Type)
tel of
    ImplicitInsertion
NoInsertNeeded -> [LamBinding] -> Name -> TCM a
continue [LamBinding]
ps (Name -> TCM a) -> Name -> TCM a
forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind (BindName -> Name) -> BindName -> Name
forall a b. (a -> b) -> a -> b
$ Binder -> BindName
forall a. Binder' a -> a
A.binderName Binder
x
    ImpInsert [Dom ()]
_    -> [LamBinding] -> Name -> TCM a
continue [LamBinding]
ps0 (Name -> TCM a) -> TCMT IO Name -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseKey -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b)
    ImplicitInsertion
BadImplicits   -> LamBinding -> TCM a -> TCM a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
     TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
       VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Unexpected parameter" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> LamBinding -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LamBinding
par
    NoSuchName VerboseKey
x   -> LamBinding -> TCM a -> TCM a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
      TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"No parameter of name " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
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 = Type -> Term
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 = Int
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
forall a.
Int
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Int
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 :: Int
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Int
npars [LamBinding]
ps Name
x Dom Type
a Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret =
  (Name, Dom Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Name
x, Dom Type
a) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
    Int
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
forall a.
Int
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters (Int
npars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [LamBinding]
ps (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) ((Tele (Dom Type) -> Type -> TCM a) -> TCM a)
-> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
tel Type
s ->
      Tele (Dom Type) -> Type -> TCM a
ret (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. VerboseKey -> a -> Abs a
Abs (Name -> VerboseKey
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 -> TCMT IO Int
fitsIn UniverseCheck
uc [IsForced]
forceds Type
t Sort
s = do
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.data.fits" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"does" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        , TCMT IO Doc
"of sort" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
t)
        , TCMT IO Doc
"fit in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
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 <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
withoutK (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Sort -> TCMT IO Bool
forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant Sort
s) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    Quantity
q <- Lens' Quantity TCEnv -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Quantity TCEnv
eQuantity
    Modality -> Term -> TCM ()
MonadConstraint (TCMT IO) => Modality -> Term -> TCM ()
usableAtModality (Quantity -> Modality -> Modality
forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
q Modality
defaultModality) (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t)

  Bool -> [IsForced] -> Type -> Sort -> TCMT IO Int
fitsIn' Bool
withoutK [IsForced]
forceds Type
t Sort
s
  where
  fitsIn' :: Bool -> [IsForced] -> Type -> Sort -> TCMT IO Int
fitsIn' Bool
withoutK [IsForced]
forceds Type
t Sort
s = do
    Maybe (Bool, Dom Type, Abs Type)
vt <- do
      Either (Dom Type, Abs Type) Type
t <- Type -> TCMT IO (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi Type
t
      Maybe (Bool, Dom Type, Abs Type)
-> TCMT IO (Maybe (Bool, Dom Type, Abs Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Bool, Dom Type, Abs Type)
 -> TCMT IO (Maybe (Bool, Dom Type, Abs Type)))
-> Maybe (Bool, Dom Type, Abs Type)
-> TCMT IO (Maybe (Bool, Dom Type, Abs Type))
forall a b. (a -> b) -> a -> b
$ case Either (Dom Type, Abs Type) Type
t of
                    Left (Dom Type
a,Abs Type
b)     -> (Bool, Dom Type, Abs Type) -> Maybe (Bool, Dom Type, Abs Type)
forall a. a -> Maybe a
Just (Bool
True ,Dom Type
a,Abs Type
b)
                    Right (El Sort
_ Term
t) | Pi Dom Type
a Abs Type
b <- Term
t
                                   -> (Bool, Dom Type, Abs Type) -> Maybe (Bool, Dom Type, Abs Type)
forall a. a -> Maybe a
Just (Bool
False,Dom Type
a,Abs Type
b)
                    Either (Dom Type, Abs Type) Type
_              -> Maybe (Bool, Dom Type, Abs 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
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IsForced -> Bool
isForced IsForced
forced Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
withoutK) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          Sort
sa <- Sort -> TCMT IO Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Sort -> TCMT IO Sort) -> Sort -> TCMT IO Sort
forall a b. (a -> b) -> a -> b
$ Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
dom
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
isPath Bool -> Bool -> Bool
|| UniverseCheck
uc UniverseCheck -> UniverseCheck -> Bool
forall a. Eq a => a -> a -> Bool
== UniverseCheck
NoUniverseCheck Bool -> Bool -> Bool
|| Sort
sa Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
forall t. Sort' t
SizeUniv) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            Sort
sa Sort -> Sort -> TCM ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
`leqSort` Sort
s
        (VerboseKey, Dom Type) -> TCMT IO Int -> TCMT IO Int
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b, Dom Type
dom) (TCMT IO Int -> TCMT IO Int) -> TCMT IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ do
          Int -> Int
forall a. Enum a => a -> a
succ (Int -> Int) -> TCMT IO Int -> TCMT IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [IsForced] -> Type -> Sort -> TCMT IO Int
fitsIn' Bool
withoutK [IsForced]
forceds' (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) (Int -> Sort -> Sort
forall a. Subst a => Int -> a -> a
raise Int
1 Sort
s)
      Maybe (Bool, Dom Type, Abs Type)
_ -> do
        Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
t Sort -> Sort -> TCM ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
`leqSort` Sort
s
        Int -> TCMT IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
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 -> Tele (Dom Type) -> TCM ()
checkIndexSorts Sort
s = \case
  Tele (Dom Type)
EmptyTel -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel' -> do
    let sa :: Sort
sa = Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a
    -- Andreas, 2020-10-19, allow Size indices
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort
sa Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
forall t. Sort' t
SizeUniv) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Sort
sa Sort -> Sort -> TCM ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
`leqSort` Sort
s
    Dom Type
-> Abs (Tele (Dom Type)) -> (Tele (Dom Type) -> TCM ()) -> TCM ()
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' ((Tele (Dom Type) -> TCM ()) -> TCM ())
-> (Tele (Dom Type) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Sort -> Tele (Dom Type) -> TCM ()
checkIndexSorts (Int -> Sort -> Sort
forall a. Subst a => Int -> a -> a
raise Int
1 Sort
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
(IsPathCons -> IsPathCons -> Bool)
-> (IsPathCons -> IsPathCons -> Bool) -> Eq IsPathCons
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,Int -> IsPathCons -> VerboseKey -> VerboseKey
[IsPathCons] -> VerboseKey -> VerboseKey
IsPathCons -> VerboseKey
(Int -> IsPathCons -> VerboseKey -> VerboseKey)
-> (IsPathCons -> VerboseKey)
-> ([IsPathCons] -> VerboseKey -> VerboseKey)
-> Show IsPathCons
forall a.
(Int -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [IsPathCons] -> VerboseKey -> VerboseKey
$cshowList :: [IsPathCons] -> VerboseKey -> VerboseKey
show :: IsPathCons -> VerboseKey
$cshow :: IsPathCons -> VerboseKey
showsPrec :: Int -> IsPathCons -> VerboseKey -> VerboseKey
$cshowsPrec :: Int -> IsPathCons -> VerboseKey -> VerboseKey
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 :: Int -> Int -> Type -> QName -> TCM IsPathCons
constructs Int
nofPars Int
nofExtraVars Type
t QName
q = Int -> Type -> TCM IsPathCons
constrT Int
nofExtraVars Type
t
    where
        -- The number n counts the proper (non-parameter) constructor arguments.
        constrT :: Nat -> Type -> TCM IsPathCons
        constrT :: Int -> Type -> TCM IsPathCons
constrT Int
n Type
t = do
            Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
            Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pathV <- TCMT IO (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf
            case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
                Pi Dom Type
_ (NoAbs VerboseKey
_ Type
b)  -> Int -> Type -> TCM IsPathCons
constrT Int
n Type
b
                Pi Dom Type
a Abs Type
b            -> Dom Type -> Abs Type -> (Type -> TCM IsPathCons) -> TCM IsPathCons
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b ((Type -> TCM IsPathCons) -> TCM IsPathCons)
-> (Type -> TCM IsPathCons) -> TCM IsPathCons
forall a b. (a -> b) -> a -> b
$ Int -> Type -> TCM IsPathCons
constrT (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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 VerboseKey
_ Type
b -> Int -> Type -> TCM IsPathCons
constrT Int
n Type
b
                             Abs Type
b         -> Dom Type -> Abs Type -> (Type -> TCM IsPathCons) -> TCM IsPathCons
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b ((Type -> TCM IsPathCons) -> TCM IsPathCons)
-> (Type -> TCM IsPathCons) -> TCM IsPathCons
forall a b. (a -> b) -> a -> b
$ Int -> Type -> TCM IsPathCons
constrT (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                      IsPathCons -> TCM IsPathCons
forall (m :: * -> *) a. Monad m => a -> m a
return IsPathCons
PathCons
                Def QName
d Elims
es | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
q -> do
                  let vs :: [Arg Term]
vs = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
                  let ([Arg Term]
pars, [Arg Term]
ixs) = Int -> [Arg Term] -> ([Arg Term], [Arg Term])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
nofPars [Arg Term]
vs
                  -- check that the constructor parameters are the data parameters
                  Int -> [Arg Term] -> TCM ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh Int m) =>
Int -> [Arg Term] -> m ()
checkParams Int
n [Arg Term]
pars
                  IsPathCons -> TCM IsPathCons
forall (m :: * -> *) a. Monad m => a -> m a
return IsPathCons
PointCons
                MetaV{} -> do
                  Definition
def <- QName -> TCMT IO Definition
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 <- Type -> TCMT IO (TelV Type)
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 = (Arg VerboseKey -> Int -> Arg Term)
-> [Arg VerboseKey] -> [Int] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg VerboseKey
arg Int
x -> Int -> Term
var Int
x Term -> Arg VerboseKey -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg VerboseKey
arg ) (Tele (Dom Type) -> [Arg VerboseKey]
forall a. TelToArgs a => a -> [Arg VerboseKey]
telToArgs Tele (Dom Type)
tel) ([Int] -> [Arg Term]) -> [Int] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$
                             Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
nofPars ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int
nofPars Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)
                  -- The indices are fresh metas
                  [Arg Term]
xs <- Type -> TCMT IO [Arg Term]
forall (m :: * -> *). MonadMetaSolver m => Type -> m [Arg Term]
newArgsMeta (Type -> TCMT IO [Arg Term]) -> TCMT IO Type -> TCMT IO [Arg Term]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> [Arg Term] -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
td [Arg Term]
us
                  let t' :: Type
t' = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort -> Sort
forall a. Subst a => Int -> a -> a
raise Int
n (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Defn -> Sort
dataSort (Defn -> Sort) -> Defn -> Sort
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
forall a b. (a -> b) -> a -> b
$ [Arg Term]
us [Arg Term] -> [Arg Term] -> [Arg Term]
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.
                  TCMT IO Bool -> TCM IsPathCons -> TCM IsPathCons -> TCM IsPathCons
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TCM () -> TCMT IO Bool
forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion (TCM () -> TCMT IO Bool) -> TCM () -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t Type
t')
                      (Int -> Type -> TCM IsPathCons
constrT Int
n Type
t')
                      (TypeError -> TCM IsPathCons
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM IsPathCons) -> TypeError -> TCM IsPathCons
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldEndInApplicationOfTheDatatype Type
t)
                Term
_ -> TypeError -> TCM IsPathCons
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM IsPathCons) -> TypeError -> TCM IsPathCons
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldEndInApplicationOfTheDatatype Type
t

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

                sameVar :: Arg Term -> Int -> m ()
sameVar Arg Term
arg Int
i
                  -- skip irrelevant parameters
                  | Arg Term -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Arg Term
arg = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  | Bool
otherwise = do
                    Type
t <- Int -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
                    Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg) (Int -> Term
var Int
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
s Term
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  case Term
t of
    Def QName
q Elims
_ -> do
      Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      case Definition -> Defn
theDef Definition
def of
        Axiom       {} -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
        DataOrRecSig{} -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
forall a. Maybe a
Nothing
        Function    {} -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
forall a. Maybe a
Nothing
        Datatype    {} -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
        Record      {  recInduction :: Defn -> Maybe Induction
recInduction = Just Induction
CoInductive } -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)
        Record      {  recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
_                } -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
        GeneralizableVar{} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
        Constructor {} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
        Primitive   {} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
        PrimitiveSort{} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
        AbstractDefn{} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Var   {} -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
forall a. Maybe a
Nothing
    Lam   {} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Lit   {} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Level {} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Con   {} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Pi    {} -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
    Sort  {} -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
    MetaV {} -> Maybe Bool -> TCM (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
forall a. Maybe a
Nothing
    DontCare{} -> TCM (Maybe Bool)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Dummy VerboseKey
s Elims
_  -> VerboseKey -> TCM (Maybe Bool)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s