{-# 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 :: Nat
npars =
              case Definition -> Defn
theDef Definition
def of
                DataOrRecSig Nat
n -> Nat
n
                Defn
_              -> Nat
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
        Nat
freeVars <- TCMT IO Nat
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
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 ->
                   Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM Defn)
-> TCM Defn
forall a.
Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters (Nat
npars Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- [Maybe Name] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
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 :: Nat
nofIxs = Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
ixTel

            Sort' Term
s <- TCMT IO (Sort' Term) -> TCMT IO (Sort' Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO (Sort' Term) -> TCMT IO (Sort' Term))
-> TCMT IO (Sort' Term) -> TCMT IO (Sort' Term)
forall a b. (a -> b) -> a -> b
$ do
              -- Andreas, 2016-11-02 issue #2290
              -- Trying to unify the sort with a fresh sort meta which is
              -- defined outside the index telescope is the most robust way
              -- to check independence of the indices.
              -- However, it might give the dreaded "Cannot instantiate meta..."
              -- error which we replace by a more understandable error
              -- in case of a suspected dependency.
              Sort' Term
s <- TCMT IO (Sort' Term)
newSortMetaBelowInf
              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
$ Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise Nat
nofIxs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort Sort' Term
s) ((TCErr -> TCM ()) -> TCM ()) -> (TCErr -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ TCErr
err ->
                  if (Nat -> Bool) -> [Nat] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Nat -> Type -> Bool
forall a. Free a => Nat -> a -> Bool
`freeIn` Type
s0) [Nat
0..Nat
nofIxs Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
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' Term -> TCMT IO (Sort' Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort' Term
s

            -- when `--without-K`, all the indices should fit in the
            -- sort of the datatype (see #3420).
            let s' :: Sort' Term
s' = case Sort' Term
s of
                  Prop Level
l -> Level -> Sort' Term
forall t. Level' t -> Sort' t
Type Level
l
                  Sort' Term
_      -> Sort' Term
s
            -- Andreas, 2019-07-16, issue #3916:
            -- NoUniverseCheck should also disable the index sort check!
            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' Term -> Tele (Dom Type) -> TCM ()
checkIndexSorts Sort' Term
s' Tele (Dom Type)
ixTel

            ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.sort" Nat
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
              , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort' Term
s
                , TCMT IO Doc
"indices:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Nat -> ArgName
forall a. Show a => a -> ArgName
show Nat
nofIxs)
                , TCMT IO Doc
"gparams:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ([Maybe Name] -> ArgName
forall a. Show a => a -> ArgName
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
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ([LamBinding] -> ArgName
forall a. Show a => a -> ArgName
show ([LamBinding] -> ArgName) -> [LamBinding] -> ArgName
forall a b. (a -> b) -> a -> b
$ [LamBinding] -> [LamBinding]
forall a. ExprLike a => a -> a
deepUnscope [LamBinding]
ps)
                ]
              ]
            let npars :: Nat
npars = Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel

            -- Change the datatype from an axiom to a datatype with no constructors.
            let dataDef :: Defn
dataDef = Datatype
                  { dataPars :: Nat
dataPars       = Nat
npars
                  , dataIxs :: Nat
dataIxs        = Nat
nofIxs
                  , dataClause :: Maybe Clause
dataClause     = Maybe Clause
forall a. Maybe a
Nothing
                  , dataCons :: [QName]
dataCons       = []     -- Constructors are added later
                  , dataSort :: Sort' Term
dataSort       = Sort' Term
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 -> Nat -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible Nat
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)
-> Nat
-> Sort' Term
-> Constructor
-> TCM IsPathCons
checkConstructor QName
name UniverseCheck
uc Tele (Dom Type)
tel' Nat
nofIxs Sort' Term
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' Term)
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' Term)) -> TCMT IO (Sort' Term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Sort Sort' Term
s -> Sort' Term -> TCMT IO (Sort' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
  Term
_      -> do
    Sort' Term
s <- TCMT IO (Sort' Term)
newSortMetaBelowInf
    Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t (Sort' Term -> Type
sort Sort' Term
s)
    Sort' Term -> TCMT IO (Sort' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s


-- | Type check a constructor declaration. Checks that the constructor targets
--   the datatype and that it fits inside the declared sort.
--   Returns the non-linear parameters.
checkConstructor
  :: QName         -- ^ Name of data type.
  -> UniverseCheck -- ^ Check universes?
  -> Telescope     -- ^ Parameter telescope.
  -> Nat           -- ^ Number of indices of the data type.
  -> Sort          -- ^ Sort of the data type.
  -> A.Constructor -- ^ Constructor declaration (type signature).
  -> TCM IsPathCons
checkConstructor :: QName
-> UniverseCheck
-> Tele (Dom Type)
-> Nat
-> Sort' Term
-> Constructor
-> TCM IsPathCons
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Nat
nofIxs Sort' Term
s (A.ScopedDecl ScopeInfo
scope [Constructor
con]) = do
  ScopeInfo -> TCM ()
setScope ScopeInfo
scope
  QName
-> UniverseCheck
-> Tele (Dom Type)
-> Nat
-> Sort' Term
-> Constructor
-> TCM IsPathCons
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Nat
nofIxs Sort' Term
s Constructor
con
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Nat
nofIxs Sort' Term
s con :: Constructor
con@(A.Axiom KindOfName
_ DefInfo
i ArgInfo
ai Maybe [Occurrence]
Nothing QName
c Expr
e) =
    Call -> TCM IsPathCons -> TCM IsPathCons
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Tele (Dom Type) -> Sort' Term -> Constructor -> Call
CheckConstructor QName
d Tele (Dom Type)
tel Sort' Term
s Constructor
con) (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
$ ArgName -> TypeError
GenericError (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$ ArgName
"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
$ ArgName -> TypeError
GenericError (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$ ArgName
"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
$ ArgName -> TypeError
GenericError (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$ ArgName
"Quantity-restricted constructors are not supported"
        -- check that the type of the constructor is well-formed
        (Type
t, IsPathCons
isPathCons) <- 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' Term -> TCM ()
forall {m :: * -> *} {a}. (MonadDebug m, PrettyTCM a) => a -> m ()
debugFitsIn Sort' Term
s
        -- To allow propositional squash, we turn @Prop ℓ@ into @Set ℓ@
        -- for the purpose of checking the type of the constructors.
        let s' :: Sort' Term
s' = case Sort' Term
s of
              Prop Level
l -> Level -> Sort' Term
forall t. Level' t -> Sort' t
Type Level
l
              Sort' Term
_      -> Sort' Term
s
        Nat
arity <- Call -> TCMT IO Nat -> TCMT IO Nat
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Type -> Sort' Term -> Call
CheckConstructorFitsIn QName
c Type
t Sort' Term
s') (TCMT IO Nat -> TCMT IO Nat) -> TCMT IO Nat -> TCMT IO Nat
forall a b. (a -> b) -> a -> b
$
                 ArgInfo -> TCMT IO Nat -> TCMT IO Nat
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext ArgInfo
ai (TCMT IO Nat -> TCMT IO Nat) -> TCMT IO Nat -> TCMT IO Nat
forall a b. (a -> b) -> a -> b
$
                 UniverseCheck -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn UniverseCheck
uc [IsForced]
forcedArgs Type
t Sort' Term
s'
        -- this may have instantiated some metas in s, so we reduce
        Sort' Term
s <- Sort' Term -> TCMT IO (Sort' Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort' Term
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) <- Nat -> Type -> TCMT IO (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundaryP (-Nat
1) Type
t

        -- We assume that the current context matches the parameters
        -- of the datatype in an empty context (c.f. getContextSize above).
        Tele (Dom Type)
params <- 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 <- [Nat] -> (Nat -> TCMT IO QName) -> TCMT IO [QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Nat
0 .. Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
fields Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1] ((Nat -> TCMT IO QName) -> TCMT IO [QName])
-> (Nat -> TCMT IO QName) -> TCMT IO [QName]
forall a b. (a -> b) -> a -> b
$ \ Nat
i ->
              ArgName -> TCMT IO QName
freshAbstractQName'_ (ArgName -> TCMT IO QName) -> ArgName -> TCMT IO QName
forall a b. (a -> b) -> a -> b
$ Name -> ArgName
forall a. Pretty a => a -> ArgName
P.prettyShow (QName -> Name
A.qnameName QName
c) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
"-" ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Nat -> ArgName
forall a. Show a => a -> ArgName
show Nat
i

            -- nofIxs == 0 means the data type can be reconstructed
            -- by appling the QName d to the parameters.
            let dataT :: Type
dataT = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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

            ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con.comp" Nat
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 (ArgName, Type) -> Arg QName)
-> [QName] -> [Arg (ArgName, Type)] -> [Arg QName]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith QName -> Arg (ArgName, Type) -> Arg QName
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [QName]
names ([Arg (ArgName, Type)] -> [Arg QName])
-> [Arg (ArgName, Type)] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ (Dom' Term (ArgName, Type) -> Arg (ArgName, Type))
-> [Dom' Term (ArgName, Type)] -> [Arg (ArgName, Type)]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (ArgName, Type) -> Arg (ArgName, Type)
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term (ArgName, Type)] -> [Arg (ArgName, Type)])
-> [Dom' Term (ArgName, Type)] -> [Arg (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
fields

            QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> TCM ()
defineProjections QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fields Type
dataT
            -- Cannot compose indexed inductive types yet.
            CompKit
comp <- if Nat
nofIxs Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
/= Nat
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 -> Nat -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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
              { conPars :: Nat
conPars   = Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel
              , conArity :: Nat
conArity  = Nat
arity
              , conSrcCon :: ConHead
conSrcCon = ConHead
con
              , conData :: QName
conData   = QName
d
              , conAbstr :: IsAbstract
conAbstr  = 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 :: Nat -> Expr -> TCMT IO (Type, IsPathCons)
check Nat
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
            Nat
n <- TCMT IO Nat
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
            Type -> QName -> Nat -> TCM ()
forall {m :: * -> *} {a} {a} {a}.
(MonadDebug m, PrettyTCM a, PrettyTCM a, Show a) =>
a -> a -> a -> m ()
debugEndsIn Type
t QName
d (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
k)
            IsPathCons
isPathCons <- Nat -> Nat -> Type -> QName -> TCM IsPathCons
constructs (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
k) Nat
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 (Nat -> Expr -> TCMT IO (Type, IsPathCons)
check Nat
1 Expr
e)
          (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, IsPathCons
isPathCons)
        Expr
_ -> Nat -> Expr -> TCMT IO (Type, IsPathCons)
check Nat
0 Expr
e

    debugEnter :: a -> a -> m ()
debugEnter a
c a
e =
      ArgName -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
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 =
      ArgName -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
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"
              , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
              ]
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (a -> ArgName
forall a. Show a => a -> ArgName
show a
n)
        ]
    debugFitsIn :: a -> m ()
debugFitsIn a
s =
      ArgName -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
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"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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 =
      ArgName -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
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)
_ Nat
_ Sort' Term
_ 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 <- (ArgName -> TCMT IO (Maybe Term))
-> [ArgName] -> TCMT IO [Maybe Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ArgName -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getTerm'
    [ ArgName
builtinInterval
    , ArgName
builtinIZero
    , ArgName
builtinIOne
    , ArgName
builtinIMin
    , ArgName
builtinIMax
    , ArgName
builtinINeg
    , ArgName
builtinPOr
    , ArgName
builtinItIsOne
    ]
  if Bool -> Bool
not ((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 -> [ArgName] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
whenDefined (Boundary -> Bool
forall a. Null a => a -> Bool
null Boundary
boundary) [ArgName
builtinHComp,ArgName
builtinTrans] (TranspOrHComp
-> QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO (Maybe QName)
defineTranspOrHCompD TranspOrHComp
DoHComp  QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary)
    Maybe QName
transp <- Bool -> [ArgName] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
whenDefined Bool
True            [ArgName
builtinTrans]              (TranspOrHComp
-> QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO (Maybe QName)
defineTranspOrHCompD TranspOrHComp
DoTransp QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary)
    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
      { 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 [ Nat -> Term
var Nat
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
$ Nat -> Term
var Nat
0] | Nat
n <- [Nat
1..a -> Nat
forall a. Sized a => a -> Nat
size a
tel] ]
    withArgInfo :: Tele (Dom t) -> [b] -> [Arg b]
withArgInfo Tele (Dom t)
tel = (ArgInfo -> b -> Arg b) -> [ArgInfo] -> [b] -> [Arg b]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ArgInfo -> b -> Arg b
forall e. ArgInfo -> e -> Arg e
Arg ((Dom' Term (ArgName, t) -> ArgInfo)
-> [Dom' Term (ArgName, t)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (ArgName, t) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo ([Dom' Term (ArgName, t)] -> [ArgInfo])
-> (Tele (Dom t) -> [Dom' Term (ArgName, t)])
-> Tele (Dom t)
-> [ArgInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom t) -> [Dom' Term (ArgName, t)]
forall t. Tele (Dom t) -> [Dom (ArgName, 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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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} {b}. Tele (Dom t) -> [b] -> [Arg b]
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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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} {b}. Tele (Dom t) -> [b] -> [Arg b]
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
<$> ArgName -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getTerm' ArgName
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 = Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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 = Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
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 = Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
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 = Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
wkS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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
l) -> Level -> Term
Level Level
l) (Sort' Term -> Term) -> (Type -> Sort' Term) -> Type -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort
              pOr :: NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
pOr NamesT (TCMT IO) Type
la NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
j NamesT (TCMT IO) Term
u0 NamesT (TCMT IO) Term
u1 = 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
<#> ArgName
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"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)) = [ArgName]
-> NamesT (TCMT IO) (Abs (Term, Term))
-> TCMT IO (Abs (Term, Term))
forall (m :: * -> *) a. [ArgName] -> 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 (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
"i" (Type -> Abs Type) -> Type -> Abs Type
forall a b. (a -> b) -> a -> b
$ (Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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)

                ArgName
-> (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) =>
ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind ArgName
"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
<#> ArgName
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"j" (\ NamesT (TCMT IO) Term
j -> Type -> Term
lvlOfType (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
<@> ArgName
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"j" (\ NamesT (TCMT IO) Term
j -> Type -> Term
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
                           (ArgName
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"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) (ArgName
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"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

            [ArgName] -> NamesT (TCMT IO) Term -> TCMT IO Term
forall (m :: * -> *) a. [ArgName] -> 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 = ArgName
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"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 (ArgName
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"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 = Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
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) (Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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     = Nat
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a. Nat -> [a] -> [a]
take (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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_ (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
forall e. e -> Arg e
argN (Named_ (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar))
-> Named_ (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall a name. a -> Named name a
unnamed (Pattern' DBPatVar -> Named_ (Pattern' DBPatVar))
-> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ Pattern' DBPatVar
up]
        clause :: Clause
clause = Clause
          { clauseTel :: Tele (Dom Type)
clauseTel         = Tele (Dom Type)
gamma
          , clauseType :: Maybe (Arg Type)
clauseType        = 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 ArgName -> m (Maybe a) -> m (Maybe a)
whenDefined Bool
False t ArgName
_ 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 ArgName
xs m (Maybe a)
m = do
      t (Maybe Term)
xs <- (ArgName -> m (Maybe Term)) -> t ArgName -> m (t (Maybe Term))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ArgName -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getTerm' t ArgName
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
$ Nat -> Term
var Nat
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
++# Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS Nat
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) (ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
"d" Tele (Dom Type)
forall a. Tele a
EmptyTel))
    np :: Nat
np         = Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
params

  [(Nat, QName, Dom Type)]
-> ((Nat, QName, Dom Type) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Nat] -> [QName] -> [Dom Type] -> [(Nat, QName, Dom Type)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom ([Dom Type] -> Nat
forall a. Sized a => a -> Nat
size [Dom Type]
fieldTypes)) [QName]
names [Dom Type]
fieldTypes) (((Nat, QName, Dom Type) -> TCM ()) -> TCM ())
-> ((Nat, QName, Dom Type) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (Nat
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
$ Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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` Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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
$ Nat -> Term
var Nat
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
          }

    ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.proj" Nat
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
<+> (Nat, Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Nat
i,Dom Type
ty)
      , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
                    { 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 :: Nat
projIndex    = Nat
np Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1
                    , projLams :: ProjLams
projLams     = [Arg ArgName] -> ProjLams
ProjLams ([Arg ArgName] -> ProjLams) -> [Arg ArgName] -> ProjLams
forall a b. (a -> b) -> a -> b
$ (Dom' Term (ArgName, Type) -> Arg ArgName)
-> [Dom' Term (ArgName, Type)] -> [Arg ArgName]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term ArgName -> Arg ArgName
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term ArgName -> Arg ArgName)
-> (Dom' Term (ArgName, Type) -> Dom' Term ArgName)
-> Dom' Term (ArgName, Type)
-> Arg ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ArgName, Type) -> ArgName)
-> Dom' Term (ArgName, Type) -> Dom' Term ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst) ([Dom' Term (ArgName, Type)] -> [Arg ArgName])
-> [Dom' Term (ArgName, Type)] -> [Arg ArgName]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, 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]
          }

      ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.proj.fun" Nat
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
<+> Nat -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Nat
i
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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'_ :: ArgName -> TCMT IO QName
freshAbstractQName'_ = Fixity' -> Name -> TCMT IO QName
freshAbstractQName Fixity'
noFixity' (Name -> TCMT IO QName)
-> (ArgName -> Name) -> ArgName -> TCMT IO QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Name
C.simpleName


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

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

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

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

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

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

toCType :: MonadReduce m => Type -> m (Maybe CType)
toCType :: forall (m :: * -> *). MonadReduce m => Type -> m (Maybe CType)
toCType Type
ty = do
  Sort' Term
sort <- Sort' Term -> m (Sort' Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Sort' Term -> m (Sort' Term)) -> Sort' Term -> m (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
ty
  case Sort' Term
sort of
    Type Level
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 -> LType
LEl Level
l (Type -> Term
forall t a. Type'' t a -> a
unEl Type
ty))
    SSet Level
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' Term -> QName -> CType
ClosedType (Level -> Sort' Term
forall t. Level' t -> Sort' t
SSet Level
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' 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

instance Subst CType where
  type SubstArg CType = Term
  applySubst :: Substitution' (SubstArg CType) -> CType -> CType
applySubst Substitution' (SubstArg CType)
rho (ClosedType Sort' Term
s QName
t) = Sort' Term -> QName -> CType
ClosedType (Substitution' (SubstArg (Sort' Term)) -> Sort' Term -> Sort' Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' Term))
Substitution' (SubstArg CType)
rho Sort' Term
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 CType)
fsT' <- (Dom Type -> MaybeT (TCMT IO) (Dom CType))
-> Tele (Dom Type) -> MaybeT (TCMT IO) (Tele (Dom 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 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 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 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 LType)
fsT' <- (Dom Type -> MaybeT (TCMT IO) (Dom LType))
-> Tele (Dom Type) -> MaybeT (TCMT IO) (Tele (Dom 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 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 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 LType)
fsT' [Arg QName]
fns LType
rect'


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

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

  ArgName -> Nat -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"trans.rec" Nat
5 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ (ArgName
"Generated name: " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Show a => a -> ArgName
show QName
theName ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
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
$ [ArgName] -> NamesT (TCMT IO) Type -> TCMT IO Type
forall (m :: * -> *) a. [ArgName] -> 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 ([ArgName] -> NamesT Fail (Abs Type) -> Abs Type
forall a. [ArgName] -> NamesT Fail a -> a
runNames [] (NamesT Fail (Abs Type) -> Abs Type)
-> NamesT Fail (Abs Type) -> Abs Type
forall a b. (a -> b) -> a -> b
$ ArgName
-> (NamesT Fail Term -> NamesT Fail Type) -> NamesT Fail (Abs Type)
forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind ArgName
"i" ((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')
              ArgName
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
"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)

  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
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
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"sort = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Sort' Term -> ArgName
forall a. Show a => a -> ArgName
show (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
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 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 CType]) -> [Dom CType] -> [Dom CType]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
                       Tele (Dom CType) -> [Dom CType]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (Nat -> Term -> Substitution' Term
forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
0 Term
io Substitution' (SubstArg (Tele (Dom CType)))
-> Tele (Dom CType) -> Tele (Dom CType)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom CType)
fsT') -- Γ, Φ[δ i1] ⊢ flatten Φ[δ i1]

      -- Γ, i : I ⊢ [δ i] : Δ
      delta_i :: Substitution' Term
delta_i = (Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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 CType)
fsT' = (Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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 CType)))
-> Tele (Dom CType) -> Tele (Dom CType)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
               Tele (Dom CType)
fsT -- Δ ⊢ Φ
      lam_i :: Term -> Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
"i"



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

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

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

      fsT_tel :: Tele (Dom CType)
fsT_tel = (Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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 CType)))
-> Tele (Dom CType) -> Tele (Dom CType)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom CType)
fsT

      iMin :: Term -> Term -> Term
iMin Term
x Term
y = Term
imin 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 CType) -> TCMT IO Term
mkBody (Term
field, Dom 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 CType -> Type) -> Dom CType -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
fromCType (CType -> Type) -> (Dom CType -> CType) -> Dom CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom CType -> CType
forall t e. Dom' t e -> e
unDom) Dom CType
filled_ty'
          -- Γ ⊢ l : I -> Level of filled_ty
        -- sort <- reduce $ getSort $ unDom filled_ty'
        case Dom CType -> CType
forall t e. Dom' t e -> e
unDom Dom CType
filled_ty' of
          LType (LEl Level
l Term
_) -> do
            let lvl :: Term
lvl = Term -> Term
lam_i (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Level -> Term
Level Level
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
$ [ArgName] -> NamesT Fail Term -> Term
forall a. [ArgName] -> 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
$ [ArgName] -> NamesT Fail Term -> Term
forall a. [ArgName] -> 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 (Nat -> Term
var Nat
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
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
"i" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
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 (Nat -> Term
var Nat
0) (Nat -> Term
var Nat
1))]) [Term]
ds
         where
          -- Ξ, i : I
          ([Term]
us, Term
phi:[Term]
ds) = Nat -> [Term] -> ([Term], [Term])
forall a. Nat -> [a] -> ([a], [a])
splitAt (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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 (Nat -> [Term] -> [Term]
forall a. Subst a => Nat -> a -> a
raise Nat
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 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 CType
field_ty) : [(Term, Dom CType)]
ps) = do
      -- Ξ, i : I, Φ[δ i]|_f ⊢ Φ_f = field_ty
      -- Ξ ⊢ b : field_ty [i := i1][acc]
      -- Ξ ⊢ parallesS acc : Φ[δ i1]|_f
      -- Ξ , i : I ⊢ τ = [(\ j → δ (i ∨ j), φ ∨ ~ i, us] : Ξ
      -- Ξ , i : I ⊢ parallesS (acc[τ]) : Φ[δ i1]|_f
      -- Ξ, i : I ⊢ field_ty [parallesS (acc[τ])]
      let
        filled_ty :: Dom CType
filled_ty = [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 CType)) -> Dom CType -> Dom CType
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Dom CType
field_ty
      Term
b <- (Term, Dom CType) -> TCMT IO Term
mkBody (Term
fname,Dom CType
filled_ty)
      [Term]
bs <- [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
go (Term
b Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
acc) [(Term, Dom 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 CType)] -> TCMT IO [Term]
go [] ([Term] -> [Dom CType] -> [(Term, Dom CType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
the_fields ((Dom' Term (ArgName, CType) -> Dom CType)
-> [Dom' Term (ArgName, CType)] -> [Dom CType]
forall a b. (a -> b) -> [a] -> [b]
map (((ArgName, CType) -> CType)
-> Dom' Term (ArgName, CType) -> Dom CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, CType) -> CType
forall a b. (a, b) -> b
snd) ([Dom' Term (ArgName, CType)] -> [Dom CType])
-> [Dom' Term (ArgName, CType)] -> [Dom CType]
forall a b. (a -> b) -> a -> b
$ Tele (Dom CType) -> [Dom' Term (ArgName, CType)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom CType)
fsT_tel)) -- ∀ f.  Ξ, i : I, Φ[δ i]|_f ⊢ Φ[δ i]_f
  let
    -- Ξ, i : I ⊢ ... : Δ.Φ
    theSubst :: Substitution' Term
theSubst = [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
++# (Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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 CType -> Dom Type) -> [Dom CType] -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map ((CType -> Type) -> Dom CType -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CType -> Type
fromCType) [Dom CType]
clause_types, [Term]
bodys), Substitution' Term
theSubst)
  where
    -- record type in 'exponentiated' context
    -- (params : Δ^I), i : I |- T[params i]
    rect' :: Type
rect' = 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 [ Nat -> Term
var Nat
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
$ Nat -> Term
var Nat
0] | Nat
n <- [Nat
1..a -> Nat
forall a. Sized a => a -> Nat
size a
tel] ]
    -- given I type, and Δ telescope, build Δ^I such that
    -- (x : A, y : B x, ...)^I = (x : I → A, y : (i : I) → B (x i), ...)
    expTelescope :: Type -> Telescope -> Telescope
    expTelescope :: Type -> Tele (Dom Type) -> Tele (Dom Type)
expTelescope Type
int Tele (Dom Type)
tel = [ArgName] -> [Dom Type] -> Tele (Dom Type)
unflattenTel [ArgName]
names [Dom Type]
ys
      where
        xs :: [Dom Type]
xs = Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
        names :: [ArgName]
names = Tele (Dom Type) -> [ArgName]
teleNames Tele (Dom Type)
tel
        t :: Tele (Dom Type)
t = 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
$ Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) Type
int) (ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
"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 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 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 <- ArgName -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMin"
  Term
imax <- ArgName -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMax"
  Term
tIMax <- ArgName -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMax"
  Term
ineg <- ArgName -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primINeg"
  Term
hcomp <- ArgName -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
builtinHComp
  Term
transp <- ArgName -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
builtinTrans
  Term
por <- ArgName -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primPOr"
  Term
one <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"comp.rec" Nat
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> ArgName
forall a. Show a => a -> ArgName
show Tele (Dom Type)
params
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"comp.rec" Nat
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> ArgName
forall a. Show a => a -> ArgName
show Tele (Dom Type)
delta
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"comp.rec" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom LType) -> ArgName
forall a. Show a => a -> ArgName
show Tele (Dom LType)
fsT

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

  ArgName -> Nat -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"hcomp.rec" Nat
5 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ (ArgName
"Generated name: " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Show a => a -> ArgName
show QName
theName ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
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
$ [ArgName] -> NamesT (TCMT IO) Type -> TCMT IO Type
forall (m :: * -> *) a. [ArgName] -> 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
              ArgName
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
"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 ->
               ArgName
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
"i" NamesT (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType (\ NamesT (TCMT IO) Term
i ->
                ArgName
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
ArgName
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' ArgName
"o" NamesT (TCMT IO) Term
phi ((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

  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
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
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"sort = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Level -> ArgName
forall a. Show a => a -> ArgName
show (LType -> Level
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 = Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) Substitution' (SubstArg LType) -> LType -> LType
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` LType
rect

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

  let

      -- (γ : Γ) ⊢ hcompR γ : rtype
      compTerm :: Term
compTerm = QName -> Elims -> Term
Def QName
theName [] 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 = Nat -> Term
var Nat
2
      -- (δ, φ, u, u0) : Γ ⊢ u : (i : I) → [φ] → R (δ i)
      the_u :: Term
the_u   = Nat -> Term
var Nat
1
      -- (δ, φ, u, u0) : Γ ⊢ u0 : R (δ i0)
      the_u0 :: Term
the_u0  = Nat -> Term
var Nat
0

      -- ' (δ, φ, u, u0) : Γ ⊢ fillR Γ : (i : I) → rtype[ δ ↦ (\ j → δ (i ∧ j))]
      fillTerm :: Term
fillTerm = [ArgName] -> NamesT Fail Term -> Term
forall a. [ArgName] -> 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
Level (Level -> Term) -> (LType -> Level) -> LType -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Level
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
$ Nat -> [Arg Term] -> [Arg Term]
forall a. Nat -> [a] -> [a]
take (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
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
        ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"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 <- ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"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
<#> ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"_" (\ NamesT Fail Term
o -> NamesT Fail Term
rect)
                                        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
<@> ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"_" (\ NamesT Fail Term
o -> NamesT Fail Term
w0) -- TODO wait for i = 0
                       )
          Term
u0 <- NamesT Fail Term
w0
          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 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 LType]) -> [Dom LType] -> [Dom LType]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
                       Tele (Dom LType) -> [Dom LType]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) Substitution' (SubstArg (Tele (Dom LType)))
-> Tele (Dom LType) -> Tele (Dom LType)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom LType)
fsT) -- Γ, Φ ⊢ flatten Φ
      -- Δ ⊢ Φ = fsT
      -- Γ, i : I ⊢ Φ'
      fsT' :: Tele (Dom LType)
fsT' = Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS ((Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) Substitution' (SubstArg (Tele (Dom LType)))
-> Tele (Dom LType) -> Tele (Dom LType)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom LType)
fsT

      -- Γ, i : I ⊢ (flatten Φ')[n ↦ f_n (fillR Γ i)]
      filled_types :: [Dom LType]
filled_types = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
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
$ Nat -> Term
var Nat
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 LType]) -> [Dom LType] -> [Dom LType]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
                       Tele (Dom LType) -> [Dom LType]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom LType)
fsT' -- Γ, i : I, Φ' ⊢ flatten Φ'


  NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
comp <- do
        let
          imax :: NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
imax NamesT Fail Term
i NamesT Fail Term
j = 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
<#> ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT Fail Term
i -> NamesT Fail Term
la 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
<@> ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT Fail Term
i -> NamesT Fail Term
bA 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
<@> ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT Fail Term
i -> ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"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 LType) -> TCMT IO Term
mkBody (Arg QName
fname, Dom LType
filled_ty') = do
        let
          proj :: NamesT Fail Term -> NamesT Fail Term
proj NamesT Fail Term
t = (Term -> QName -> Term
`applyProj` 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 (ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
"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 LType -> Type) -> Dom LType -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Type
fromLType (LType -> Type) -> (Dom LType -> LType) -> Dom LType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom LType -> LType
forall t e. Dom' t e -> e
unDom) Dom LType
filled_ty')
          -- Γ ⊢ l : I -> Level of filled_ty
        Level
l <- Level -> TCMT IO Level
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Level -> TCMT IO Level) -> Level -> TCMT IO Level
forall a b. (a -> b) -> a -> b
$ LType -> Level
lTypeLevel (LType -> Level) -> LType -> Level
forall a b. (a -> b) -> a -> b
$ Dom LType -> LType
forall t e. Dom' t e -> e
unDom Dom LType
filled_ty'
        let lvl :: Term
lvl = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
"i" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Level -> Term
Level Level
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
$ [ArgName] -> NamesT Fail Term -> Term
forall a. [ArgName] -> 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
                  (ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"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 -> ArgName
-> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"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)

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

  [Term]
bodys <- ((Arg QName, Dom LType) -> TCMT IO Term)
-> [(Arg QName, Dom 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 LType) -> TCMT IO Term
mkBody ([Arg QName] -> [Dom LType] -> [(Arg QName, Dom LType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Arg QName]
fns [Dom 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 LType -> Dom Type) -> [Dom LType] -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map ((LType -> Type) -> Dom LType -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LType -> Type
fromLType) [Dom 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 :: forall a.
[Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [] Type
t Tele (Dom Type) -> Type -> TCM a
ret = Tele (Dom Type) -> Type -> TCM a
ret 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      = (ArgName, Dom Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> ArgName
forall a. Abs a -> ArgName
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 :: forall a.
Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters Nat
0 [] Type
a Tele (Dom Type) -> Type -> TCM a
ret = Tele (Dom Type) -> Type -> TCM a
ret Tele (Dom Type)
forall a. Tele a
EmptyTel Type
a

bindParameters Nat
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
    ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"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 Nat
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 <- ArgName -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b)
              Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
forall a.
Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Nat
npars [] Name
x Dom Type
a Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret
           | Bool
otherwise ->
              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"
                    , ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
":" 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 Nat
npars par :: [LamBinding]
par@(A.DomainFull (A.TBind Range
_ TacticAttr
_ List1 (NamedArg Binder)
xs Expr
e) : [LamBinding]
bs) Type
a Tele (Dom Type) -> Type -> TCM a
ret =
  [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 :: ArgName
s | List1 (NamedArg Binder) -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length List1 (NamedArg Binder)
xs Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
1 = ArgName
"s"
          | Bool
otherwise     = ArgName
""
    ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"Unexpected type signature for parameter" ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
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 Nat
_ (A.DomainFull A.TLet{} : [LamBinding]
_) Type
_ Tele (Dom Type) -> Type -> TCM a
_ = TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__

bindParameters Nat
_ (par :: LamBinding
par@(A.DomainFree TacticAttr
_ NamedArg Binder
arg) : [LamBinding]
ps) Type
_ Tele (Dom Type) -> Type -> TCM a
_
  | 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
       ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"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 Nat
npars ps0 :: [LamBinding]
ps0@(par :: LamBinding
par@(A.DomainFree TacticAttr
_ NamedArg Binder
arg) : [LamBinding]
ps) Type
t Tele (Dom Type) -> Type -> TCM a
ret = do
  let x :: Binder
x          = 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 (ArgName, Type)] -> ImplicitInsertion
forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg Binder
arg ([Dom' Term (ArgName, Type)] -> ImplicitInsertion)
-> [Dom' Term (ArgName, Type)] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, 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
=<< ArgName -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (Abs Type -> ArgName
forall a. Abs a -> ArgName
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
       ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"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 ArgName
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
        ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"No parameter of name " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
x)
  where
    Pi dom :: Dom Type
dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info', unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b = 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 = Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
forall a.
Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Nat
npars [LamBinding]
ps Name
x Dom Type
dom Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret

bindParameter :: Int -> [A.LamBinding] -> Name -> Dom Type -> Abs Type -> (Telescope -> Type -> TCM a) -> TCM a
bindParameter :: forall a.
Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Nat
npars [LamBinding]
ps Name
x Dom Type
a Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret =
  (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
$
    Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
forall a.
Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters (Nat
npars Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
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
$ ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs (Name -> ArgName
nameToArgName Name
x) Tele (Dom Type)
tel) Type
s

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

fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Int
fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn UniverseCheck
uc [IsForced]
forceds Type
t Sort' Term
s = do
  ArgName -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.fits" Nat
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' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
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' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort' Term
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' Term -> TCMT IO Bool
forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant Sort' Term
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' Term -> TCMT IO Nat
fitsIn' Bool
withoutK [IsForced]
forceds Type
t Sort' Term
s
  where
  fitsIn' :: Bool -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn' Bool
withoutK [IsForced]
forceds Type
t Sort' Term
s = do
    Maybe (Bool, Dom Type, Abs Type)
vt <- do
      Either (Dom Type, Abs Type) Type
t <- 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
_ 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' Term
sa <- Sort' Term -> TCMT IO (Sort' Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Sort' Term -> TCMT IO (Sort' Term))
-> Sort' Term -> TCMT IO (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
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' Term
sa Sort' Term -> Sort' Term -> Bool
forall a. Eq a => a -> a -> Bool
== Sort' Term
forall t. Sort' t
SizeUniv) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            Sort' Term
sa Sort' Term -> Sort' Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
`leqSort` Sort' Term
s
        (ArgName, Dom Type) -> TCMT IO Nat -> TCMT IO Nat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b, Dom Type
dom) (TCMT IO Nat -> TCMT IO Nat) -> TCMT IO Nat -> TCMT IO Nat
forall a b. (a -> b) -> a -> b
$ do
          Nat -> Nat
forall a. Enum a => a -> a
succ (Nat -> Nat) -> TCMT IO Nat -> TCMT IO Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn' Bool
withoutK [IsForced]
forceds' (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) (Nat -> Sort' Term -> Sort' Term
forall a. Subst a => Nat -> a -> a
raise Nat
1 Sort' Term
s)
      Maybe (Bool, Dom Type, Abs Type)
_ -> do
        Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
t Sort' Term -> Sort' Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
`leqSort` Sort' Term
s
        Nat -> TCMT IO Nat
forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0

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

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

data IsPathCons = PathCons | PointCons
  deriving (IsPathCons -> IsPathCons -> Bool
(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,Nat -> IsPathCons -> ArgName -> ArgName
[IsPathCons] -> ArgName -> ArgName
IsPathCons -> ArgName
(Nat -> IsPathCons -> ArgName -> ArgName)
-> (IsPathCons -> ArgName)
-> ([IsPathCons] -> ArgName -> ArgName)
-> Show IsPathCons
forall a.
(Nat -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
showList :: [IsPathCons] -> ArgName -> ArgName
$cshowList :: [IsPathCons] -> ArgName -> ArgName
show :: IsPathCons -> ArgName
$cshow :: IsPathCons -> ArgName
showsPrec :: Nat -> IsPathCons -> ArgName -> ArgName
$cshowsPrec :: Nat -> IsPathCons -> ArgName -> ArgName
Show)

-- | Check that a type constructs something of the given datatype. The first
--   argument is the number of parameters to the datatype and the second the
--   number of additional non-parameters in the context (1 when generalizing, 0
--   otherwise).
--
constructs :: Int -> Int -> Type -> QName -> TCM IsPathCons
constructs :: Nat -> Nat -> Type -> QName -> TCM IsPathCons
constructs Nat
nofPars Nat
nofExtraVars Type
t QName
q = Nat -> Type -> TCM IsPathCons
constrT Nat
nofExtraVars Type
t
    where
        -- The number n counts the proper (non-parameter) constructor arguments.
        constrT :: Nat -> Type -> TCM IsPathCons
        constrT :: Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
t = do
            Type
t <- 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 ArgName
_ Type
b)  -> Nat -> Type -> TCM IsPathCons
constrT Nat
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
$ Nat -> Type -> TCM IsPathCons
constrT (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1)
                  -- OR: addCxtString (absName b) a $ constrT (n + 1) (absBody b)
                Term
_ | Left ((Dom Type
a,Abs Type
b),(Term, Term)
_) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pathV Type
t -> do
                      IsPathCons
_ <- case Abs Type
b of
                             NoAbs ArgName
_ Type
b -> Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
b
                             Abs Type
b         -> 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
$ Nat -> Type -> TCM IsPathCons
constrT (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
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) = Nat -> [Arg Term] -> ([Arg Term], [Arg Term])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
nofPars [Arg Term]
vs
                  -- check that the constructor parameters are the data parameters
                  Nat -> [Arg Term] -> TCM ()
forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh Nat m) =>
Nat -> [Arg Term] -> m ()
checkParams Nat
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 ArgName -> Nat -> Arg Term)
-> [Arg ArgName] -> [Nat] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg ArgName
arg Nat
x -> Nat -> Term
var Nat
x Term -> Arg ArgName -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg ArgName
arg ) (Tele (Dom Type) -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Tele (Dom Type)
tel) ([Nat] -> [Arg Term]) -> [Nat] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$
                             Nat -> [Nat] -> [Nat]
forall a. Nat -> [a] -> [a]
take Nat
nofPars ([Nat] -> [Nat]) -> [Nat] -> [Nat]
forall a b. (a -> b) -> a -> b
$ Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Nat
nofPars Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
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 -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Nat -> Sort' Term -> Sort' Term
forall a. Subst a => Nat -> a -> a
raise Nat
n (Sort' Term -> Sort' Term) -> Sort' Term -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Defn -> Sort' Term
dataSort (Defn -> Sort' Term) -> Defn -> Sort' Term
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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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')
                      (Nat -> Type -> TCM IsPathCons
constrT Nat
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 :: Nat -> [Arg Term] -> m ()
checkParams Nat
n [Arg Term]
vs = (Arg Term -> Nat -> m ()) -> [Arg Term] -> [Nat] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Arg Term -> Nat -> m ()
forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh Nat m) =>
Arg Term -> Nat -> m ()
sameVar [Arg Term]
vs [Nat]
ps
            where
                nvs :: Nat
nvs = [Arg Term] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Term]
vs
                ps :: [Nat]
ps  = [Nat] -> [Nat]
forall a. [a] -> [a]
reverse ([Nat] -> [Nat]) -> [Nat] -> [Nat]
forall a b. (a -> b) -> a -> b
$ Nat -> [Nat] -> [Nat]
forall a. Nat -> [a] -> [a]
take Nat
nvs [Nat
n..]

                sameVar :: Arg Term -> Nat -> m ()
sameVar Arg Term
arg Nat
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 <- Nat -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Type
typeOfBV Nat
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) (Nat -> Term
var Nat
i)


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

isCoinductive :: Type -> TCM (Maybe Bool)
isCoinductive :: Type -> TCM (Maybe Bool)
isCoinductive Type
t = do
  El Sort' Term
s Term
t <- 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 ArgName
s Elims
_  -> ArgName -> TCM (Maybe Bool)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
ArgName -> m a
__IMPOSSIBLE_VERBOSE__ ArgName
s