{-# 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
checkDataDef :: A.DefInfo -> QName -> UniverseCheck -> A.DataDefParams -> [A.Constructor] -> TCM ()
checkDataDef :: DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Constructor]
-> TCM ()
checkDataDef DefInfo
i QName
name UniverseCheck
uc (A.DataDefParams Set Name
gpars [LamBinding]
ps) [Constructor]
cs =
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> [LamBinding] -> [Constructor] -> Call
CheckDataDef (forall a. HasRange a => a -> Range
getRange QName
name) QName
name [LamBinding]
ps [Constructor]
cs) forall a b. (a -> b) -> a -> b
$ do
ModuleName -> TCM ()
addSection (QName -> ModuleName
qnameToMName QName
name)
Definition
def <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
Type
t <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
let npars :: Nat
npars =
case Definition -> Defn
theDef Definition
def of
DataOrRecSig Nat
n -> Nat
n
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
let unTelV :: TelV Type -> Type
unTelV (TelV Tele (Dom Type)
tel Type
a) = Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
tel Type
a
Type
t <- TelV Type -> Type
unTelV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
[Maybe Name]
parNames <- Set Name -> QName -> TCM [Maybe Name]
getGeneralizedParameters Set Name
gpars QName
name
Nat
freeVars <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
Defn
dataDef <- forall a.
[Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [Maybe Name]
parNames Type
t forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
gtel Type
t0 ->
forall a.
Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters (Nat
npars forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Maybe Name]
parNames) [LamBinding]
ps Type
t0 forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
ptel Type
t0 -> do
let tel :: Tele (Dom Type)
tel = forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
gtel Tele (Dom Type)
ptel
tel' :: Tele (Dom Type)
tel' = forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom Type)
tel
let TelV Tele (Dom Type)
ixTel Type
s0 = Type -> TelV Type
telView' Type
t0
nofIxs :: Nat
nofIxs = forall a. Sized a => a -> Nat
size Tele (Dom Type)
ixTel
Sort' Term
s <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ do
Sort' Term
s <- TCMT IO (Sort' Term)
newSortMetaBelowInf
forall a. TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
ixTel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
s0 forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
nofIxs forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort Sort' Term
s) forall a b. (a -> b) -> a -> b
$ \ TCErr
err ->
if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Free a => Nat -> a -> Bool
`freeIn` Type
s0) [Nat
0..Nat
nofIxs forall a. Num a => a -> a -> a
- Nat
1] then forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ TCMT IO Doc
"The sort of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name
, TCMT IO Doc
"cannot depend on its indices in the type"
, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0
]
else forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort' Term
s
let s' :: Sort' Term
s' = case Sort' Term
s of
Prop Level
l -> forall t. Level' t -> Sort' t
Type Level
l
Sort' Term
_ -> Sort' Term
s
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (UniverseCheck
uc forall a. Eq a => a -> a -> Bool
== UniverseCheck
NoUniverseCheck) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
withoutKOption forall a b. (a -> b) -> a -> b
$ Sort' Term -> Tele (Dom Type) -> TCM ()
checkIndexSorts Sort' Term
s' Tele (Dom Type)
ixTel
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.sort" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"checking datatype" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"type (parameters instantiated): " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0
, TCMT IO Doc
"type (full): " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
, TCMT IO Doc
"sort: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort' Term
s
, TCMT IO Doc
"indices:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Nat
nofIxs)
, TCMT IO Doc
"gparams:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show [Maybe Name]
parNames)
, TCMT IO Doc
"params: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. ExprLike a => a -> a
deepUnscope [LamBinding]
ps)
]
]
let npars :: Nat
npars = forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel
let dataDef :: Defn
dataDef = Datatype
{ dataPars :: Nat
dataPars = Nat
npars
, dataIxs :: Nat
dataIxs = Nat
nofIxs
, dataClause :: Maybe Clause
dataClause = forall a. Maybe a
Nothing
, dataCons :: [QName]
dataCons = []
, dataSort :: Sort' Term
dataSort = Sort' Term
s
, dataAbstr :: IsAbstract
dataAbstr = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
, dataMutual :: Maybe [QName]
dataMutual = forall a. Maybe a
Nothing
, dataPathCons :: [QName]
dataPathCons = []
}
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
npars forall a b. (a -> b) -> a -> b
$ do
QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
name ArgInfo
defaultArgInfo QName
name Type
t Defn
dataDef
[Maybe QName]
pathCons <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Constructor]
cs forall a b. (a -> b) -> a -> b
$ \ Constructor
c -> do
IsPathCons
isPathCons <- QName
-> UniverseCheck
-> Tele (Dom Type)
-> Nat
-> Sort' Term
-> Constructor
-> TCM IsPathCons
checkConstructor QName
name UniverseCheck
uc Tele (Dom Type)
tel' Nat
nofIxs Sort' Term
s Constructor
c
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if IsPathCons
isPathCons forall a. Eq a => a -> a -> Bool
== IsPathCons
PathCons then forall a. a -> Maybe a
Just (Constructor -> QName
A.axiomName Constructor
c) else forall a. Maybe a
Nothing
forall (m :: * -> *) a. Monad m => a -> m a
return Defn
dataDef{ dataPathCons :: [QName]
dataPathCons = forall a. [Maybe a] -> [a]
catMaybes [Maybe QName]
pathCons }
let cons :: [QName]
cons = forall a b. (a -> b) -> [a] -> [b]
map Constructor -> QName
A.axiomName [Constructor]
cs
QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
name ArgInfo
defaultArgInfo QName
name Type
t forall a b. (a -> b) -> a -> b
$
Defn
dataDef{ dataCons :: [QName]
dataCons = [QName]
cons }
forceSort :: Type -> TCM Sort
forceSort :: Type -> TCMT IO (Sort' Term)
forceSort Type
t = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Sort Sort' Term
s -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
Term
_ -> do
Sort' Term
s <- TCMT IO (Sort' Term)
newSortMetaBelowInf
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t (Sort' Term -> Type
sort Sort' Term
s)
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
checkConstructor
:: QName
-> UniverseCheck
-> Telescope
-> Nat
-> Sort
-> A.Constructor
-> TCM IsPathCons
checkConstructor :: QName
-> UniverseCheck
-> Tele (Dom Type)
-> Nat
-> Sort' Term
-> Constructor
-> TCM IsPathCons
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Nat
nofIxs Sort' Term
s (A.ScopedDecl ScopeInfo
scope [Constructor
con]) = do
ScopeInfo -> TCM ()
setScope ScopeInfo
scope
QName
-> UniverseCheck
-> Tele (Dom Type)
-> Nat
-> Sort' Term
-> Constructor
-> TCM IsPathCons
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Nat
nofIxs Sort' Term
s Constructor
con
checkConstructor QName
d UniverseCheck
uc Tele (Dom Type)
tel Nat
nofIxs Sort' Term
s con :: Constructor
con@(A.Axiom KindOfName
_ DefInfo
i ArgInfo
ai Maybe [Occurrence]
Nothing QName
c Expr
e) =
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Tele (Dom Type) -> Sort' Term -> Constructor -> Call
CheckConstructor QName
d Tele (Dom Type)
tel Sort' Term
s Constructor
con) forall a b. (a -> b) -> a -> b
$ do
forall {m :: * -> *} {a} {a}.
(MonadDebug m, PrettyTCM a, PrettyTCM a) =>
a -> a -> m ()
debugEnter QName
c Expr
e
case forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai of
Relevance
Relevant -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Relevance
Irrelevant -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ ArgName
"Irrelevant constructors are not supported"
Relevance
NonStrict -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ ArgName
"Shape-irrelevant constructors are not supported"
case forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai of
Quantityω{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Quantity0{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Quantity1{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ ArgName
"Quantity-restricted constructors are not supported"
(Type
t, IsPathCons
isPathCons) <- forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext ArgInfo
ai forall a b. (a -> b) -> a -> b
$
Expr -> QName -> TCMT IO (Type, IsPathCons)
checkConstructorType Expr
e QName
d
[IsForced]
forcedArgs <- if IsPathCons
isPathCons forall a. Eq a => a -> a -> Bool
== IsPathCons
PointCons
then QName -> Type -> TCM [IsForced]
computeForcingAnnotations QName
c Type
t
else forall (m :: * -> *) a. Monad m => a -> m a
return []
forall {m :: * -> *} {a}. (MonadDebug m, PrettyTCM a) => a -> m ()
debugFitsIn Sort' Term
s
let s' :: Sort' Term
s' = case Sort' Term
s of
Prop Level
l -> forall t. Level' t -> Sort' t
Type Level
l
Sort' Term
_ -> Sort' Term
s
Nat
arity <- forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Type -> Sort' Term -> Call
CheckConstructorFitsIn QName
c Type
t Sort' Term
s') forall a b. (a -> b) -> a -> b
$
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext ArgInfo
ai forall a b. (a -> b) -> a -> b
$
UniverseCheck -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn UniverseCheck
uc [IsForced]
forcedArgs Type
t Sort' Term
s'
Sort' Term
s <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort' Term
s
forall {m :: * -> *} {a} {a}.
(MonadDebug m, PrettyTCM a, PrettyTCM a) =>
a -> a -> m ()
debugAdd QName
c Type
t
(TelV Tele (Dom Type)
fields Type
_, Boundary
boundary) <- forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundaryP (-Nat
1) Type
t
Tele (Dom Type)
params <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
(ConHead
con, CompKit
comp, Maybe [QName]
projNames) <- do
[QName]
names <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Nat
0 .. forall a. Sized a => a -> Nat
size Tele (Dom Type)
fields forall a. Num a => a -> a -> a
- Nat
1] forall a b. (a -> b) -> a -> b
$ \ Nat
i ->
ArgName -> TCMT IO QName
freshAbstractQName'_ forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> ArgName
P.prettyShow (QName -> Name
A.qnameName QName
c) forall a. [a] -> [a] -> [a]
++ ArgName
"-" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Nat
i
let dataT :: Type
dataT = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
params
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con.comp" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"params =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Tele (Dom Type)
params
, TCMT IO Doc
"dataT =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
dataT
, TCMT IO Doc
"fields =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Tele (Dom Type)
fields
, TCMT IO Doc
"names =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [QName]
names
]
let con :: ConHead
con = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c DataOrRecord
IsData Induction
Inductive forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [QName]
names forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
fields
QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> TCM ()
defineProjections QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fields Type
dataT
CompKit
comp <- if Nat
nofIxs forall a. Eq a => a -> a -> Bool
/= Nat
0 Bool -> Bool -> Bool
|| (forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef)
then forall (m :: * -> *) a. Monad m => a -> m a
return CompKit
emptyCompKit
else forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO CompKit
defineCompData QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fields Type
dataT Boundary
boundary
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead
con, CompKit
comp, forall a. a -> Maybe a
Just [QName]
names)
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) forall a b. (a -> b) -> a -> b
$ do
QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
c ArgInfo
ai QName
c (Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
tel Type
t) forall a b. (a -> b) -> a -> b
$ Constructor
{ conPars :: Nat
conPars = forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel
, conArity :: Nat
conArity = Nat
arity
, conSrcCon :: ConHead
conSrcCon = ConHead
con
, conData :: QName
conData = QName
d
, conAbstr :: IsAbstract
conAbstr = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
, conInd :: Induction
conInd = Induction
Inductive
, conComp :: CompKit
conComp = CompKit
comp
, conProj :: Maybe [QName]
conProj = Maybe [QName]
projNames
, conForced :: [IsForced]
conForced = [IsForced]
forcedArgs
, conErased :: Maybe [Bool]
conErased = forall a. Maybe a
Nothing
}
case forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
i of
InstanceDef Range
_r -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
c forall a b. (a -> b) -> a -> b
$ do
QName -> Type -> TCM ()
addTypedInstance QName
c Type
t
IsInstance
NotInstanceDef -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
forall (m :: * -> *) a. Monad m => a -> m a
return IsPathCons
isPathCons
where
checkConstructorType :: Expr -> QName -> TCMT IO (Type, IsPathCons)
checkConstructorType (A.ScopedExpr ScopeInfo
s Expr
e) QName
d = forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
withScope_ ScopeInfo
s forall a b. (a -> b) -> a -> b
$ Expr -> QName -> TCMT IO (Type, IsPathCons)
checkConstructorType Expr
e QName
d
checkConstructorType Expr
e QName
d = do
let check :: Nat -> Expr -> TCMT IO (Type, IsPathCons)
check Nat
k Expr
e = do
Type
t <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO Type
isType_ Expr
e
Nat
n <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
forall {m :: * -> *} {a} {a} {a}.
(MonadDebug m, PrettyTCM a, PrettyTCM a, Show a) =>
a -> a -> a -> m ()
debugEndsIn Type
t QName
d (Nat
n forall a. Num a => a -> a -> a
- Nat
k)
IsPathCons
isPathCons <- Nat -> Nat -> Type -> QName -> TCM IsPathCons
constructs (Nat
n forall a. Num a => a -> a -> a
- Nat
k) Nat
k Type
t QName
d
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, IsPathCons
isPathCons)
case Expr
e of
A.Generalized Set QName
s Expr
e -> do
([Maybe QName]
_, Type
t, IsPathCons
isPathCons) <- forall a.
Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' Set QName
s (Nat -> Expr -> TCMT IO (Type, IsPathCons)
check Nat
1 Expr
e)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, IsPathCons
isPathCons)
Expr
_ -> Nat -> Expr -> TCMT IO (Type, IsPathCons)
check Nat
0 Expr
e
debugEnter :: a -> a -> m ()
debugEnter a
c a
e =
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"checking constructor" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
e
]
debugEndsIn :: a -> a -> a -> m ()
debugEndsIn a
t a
d a
n =
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"checking that"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t
, TCMT IO Doc
"ends in" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
d
]
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"nofPars =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show a
n)
]
debugFitsIn :: a -> m ()
debugFitsIn a
s =
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"checking that the type fits in"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
s
]
debugAdd :: a -> a -> m ()
debugAdd a
c a
t =
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.con" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"adding constructor" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t
]
checkConstructor QName
_ UniverseCheck
_ Tele (Dom Type)
_ Nat
_ Sort' Term
_ Constructor
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
defineCompData :: QName
-> ConHead
-> Telescope
-> [QName]
-> Telescope
-> Type
-> Boundary
-> TCM CompKit
defineCompData :: QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO CompKit
defineCompData QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary = do
[Maybe Term]
required <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getTerm'
[ ArgName
builtinInterval
, ArgName
builtinIZero
, ArgName
builtinIOne
, ArgName
builtinIMin
, ArgName
builtinIMax
, ArgName
builtinINeg
, ArgName
builtinPOr
, ArgName
builtinItIsOne
]
if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust [Maybe Term]
required) then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CompKit
emptyCompKit else do
Maybe QName
hcomp <- forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
whenDefined (forall a. Null a => a -> Bool
null Boundary
boundary) [ArgName
builtinHComp,ArgName
builtinTrans] (TranspOrHComp
-> QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO (Maybe QName)
defineTranspOrHCompD TranspOrHComp
DoHComp QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary)
Maybe QName
transp <- forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
whenDefined Bool
True [ArgName
builtinTrans] (TranspOrHComp
-> QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO (Maybe QName)
defineTranspOrHCompD TranspOrHComp
DoTransp QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CompKit
{ nameOfTransp :: Maybe QName
nameOfTransp = Maybe QName
transp
, nameOfHComp :: Maybe QName
nameOfHComp = Maybe QName
hcomp
}
where
sub :: a -> Substitution' Term
sub a
tel = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [ Nat -> Term
var Nat
n forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0] | Nat
n <- [Nat
1..forall a. Sized a => a -> Nat
size a
tel] ]
withArgInfo :: Tele (Dom t) -> [b] -> [Arg b]
withArgInfo Tele (Dom t)
tel = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall e. ArgInfo -> e -> Arg e
Arg (forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> ArgInfo
domInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList forall a b. (a -> b) -> a -> b
$ Tele (Dom t)
tel)
defineTranspOrHCompD :: TranspOrHComp
-> QName
-> ConHead
-> Tele (Dom Type)
-> [QName]
-> Tele (Dom Type)
-> Type
-> Boundary
-> TCMT IO (Maybe QName)
defineTranspOrHCompD TranspOrHComp
cmd QName
d ConHead
con Tele (Dom Type)
params [QName]
names Tele (Dom Type)
fsT Type
t Boundary
boundary = do
let project :: Term -> QName -> Term
project = (\ Term
t QName
p -> forall t. Apply t => t -> [Arg Term] -> t
apply (QName -> Elims -> Term
Def QName
p []) [forall e. e -> Arg e
argN Term
t])
Maybe
((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
Substitution' Term)
stuff <- TranspOrHComp
-> Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom Type)
-> [Arg QName]
-> Type
-> TCM
(Maybe
((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
Substitution' Term))
defineTranspOrHCompForFields TranspOrHComp
cmd
(forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null Boundary
boundary) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. a -> Maybe a
Just (ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem forall a b. (a -> b) -> a -> b
$ forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
teleElims Tele (Dom Type)
fsT Boundary
boundary))
Term -> QName -> Term
project QName
d Tele (Dom Type)
params Tele (Dom Type)
fsT (forall a b. (a -> b) -> [a] -> [b]
map forall e. e -> Arg e
argN [QName]
names) Type
t
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe
((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
Substitution' Term)
stuff (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ ((QName
theName, Tele (Dom Type)
gamma , Type
ty, [Dom Type]
_cl_types , [Term]
bodies), Substitution' Term
theSub) -> do
Term
iz <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
Term
body <- do
case TranspOrHComp
cmd of
TranspOrHComp
DoHComp -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall {t} {b}. Tele (Dom t) -> [b] -> [Arg b]
withArgInfo Tele (Dom Type)
fsT [Term]
bodies)
TranspOrHComp
DoTransp | forall a. Null a => a -> Bool
null Boundary
boundary -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall {t} {b}. Tele (Dom t) -> [b] -> [Arg b]
withArgInfo Tele (Dom Type)
fsT [Term]
bodies)
| Bool
otherwise -> do
Term
io <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
Term
tIMax <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax
Term
tIMin <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin
Term
tINeg <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
Term
tPOr <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getTerm' ArgName
builtinPOr
Term
tHComp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp
let
u :: Term
u = ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem forall a b. (a -> b) -> a -> b
$ forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
teleElims Tele (Dom Type)
fsT Boundary
boundary
the_u :: Term
the_u = forall a. Nat -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u
where
d0 :: Substitution
d0 :: Substitution' Term
d0 = forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
1
(forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
iz forall a. Substitution' a
IdS forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params)
the_phi :: Term
the_phi = forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0
sigma :: Substitution' Term
sigma = forall a. [a] -> [a]
reverse [Term]
bodies forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Substitution' Term
d1
where
d1 :: Substitution
d1 :: Substitution' Term
d1 = forall a. Nat -> Substitution' a -> Substitution' a
wkS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
params)
(forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
io forall a. Substitution' a
IdS forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params)
bs :: Boundary
bs = Tele (Dom Type) -> Boundary -> Boundary
fullBoundary Tele (Dom Type)
fsT Boundary
boundary
w1' :: Term
w1' = ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem forall a b. (a -> b) -> a -> b
$ Substitution' Term
sigma forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
teleElims Tele (Dom Type)
fsT Boundary
boundary
imax :: NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax NamesT (TCMT IO) Term
x NamesT (TCMT IO) Term
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y
ineg :: NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
r = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tINeg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
r
lvlOfType :: Type -> Term
lvlOfType = (\ (Type Level
l) -> Level -> Term
Level Level
l) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSort a => a -> Sort' Term
getSort
pOr :: NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
pOr NamesT (TCMT IO) Type
la NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
j NamesT (TCMT IO) Term
u0 NamesT (TCMT IO) Term
u1 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPOr forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Type -> Term
lvlOfType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" (\ NamesT (TCMT IO) Term
_ -> forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
u0 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
u1
absAp :: m (Abs r) -> m (SubstArg r) -> m r
absAp m (Abs r)
x m (SubstArg r)
y = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. Subst a => Abs a -> SubstArg a -> a
absApp m (Abs r)
x m (SubstArg r)
y
mkFace :: (Term, (Term, Term)) -> TCMT IO (Abs (Term, Term))
mkFace (Term
r,(Term
u1,Term
u2)) = forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
NamesT (TCMT IO) Term
phi <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
the_phi
NamesT (TCMT IO) (Abs Type)
ty <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a b. (a -> b) -> a -> b
$ (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
params)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
t)
forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i -> do
[NamesT (TCMT IO) Term
r,NamesT (TCMT IO) Term
u1,NamesT (TCMT IO) Term
u2] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
theSub) [Term
r,Term
u1,Term
u2]
Term
psi <- NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax NamesT (TCMT IO) Term
r (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
r)
let
squeeze :: NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
squeeze NamesT (TCMT IO) Term
u = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"j" (\ NamesT (TCMT IO) Term
j -> Type -> Term
lvlOfType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
ty forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
j))
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"j" (\ NamesT (TCMT IO) Term
j -> forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
ty forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax NamesT (TCMT IO) Term
i NamesT (TCMT IO) Term
j))
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
phi NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
`imax` NamesT (TCMT IO) Term
i)
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
u
Term
alpha <- NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
pOr (NamesT (TCMT IO) (Abs Type)
ty forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` NamesT (TCMT IO) Term
i)
(NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
r)
NamesT (TCMT IO) Term
r
(forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
squeeze NamesT (TCMT IO) Term
u1) (forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
squeeze NamesT (TCMT IO) Term
u2)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Term
psi, Term
alpha)
[Abs (Term, Term)]
faces <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term, (Term, Term)) -> TCMT IO (Abs (Term, Term))
mkFace Boundary
bs
forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
NamesT (TCMT IO) Term
w1' <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
w1'
NamesT (TCMT IO) Term
phi <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
the_phi
NamesT (TCMT IO) Term
u <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
the_u
NamesT (TCMT IO) Type
ty <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Type
ty
[(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
faces <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Abs (Term, Term)
x -> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Impossible -> Abs a -> a
noabsApp forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst Abs (Term, Term)
x) (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd Abs (Term, Term)
x)) [Abs (Term, Term)]
faces
let
thePsi :: NamesT (TCMT IO) Term
thePsi = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
faces)
hcomp :: NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
hcomp NamesT (TCMT IO) Type
ty NamesT (TCMT IO) Term
phi NamesT (TCMT IO) Term
sys NamesT (TCMT IO) Term
a0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Type -> Term
lvlOfType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
ty)
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Type
ty)
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
phi
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
sys
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a0
let
sys :: NamesT (TCMT IO) Term
sys = forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i -> do
let
recurse :: [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
-> NamesT (TCMT IO) Term
recurse [(NamesT (TCMT IO) Term
psi,NamesT (TCMT IO) (Abs Term)
alpha)] = NamesT (TCMT IO) (Abs Term)
alpha forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
i)
recurse ((NamesT (TCMT IO) Term
psi,NamesT (TCMT IO) (Abs Term)
alpha):[(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
xs) = NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
pOr NamesT (TCMT IO) Type
ty
NamesT (TCMT IO) Term
psi NamesT (TCMT IO) Term
theOr
(NamesT (TCMT IO) (Abs Term)
alpha forall {m :: * -> *} {r}.
(Monad m, Subst r) =>
m (Abs r) -> m (SubstArg r) -> m r
`absAp` (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
ineg NamesT (TCMT IO) Term
i)) ([(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
-> NamesT (TCMT IO) Term
recurse [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
xs)
where
theOr :: NamesT (TCMT IO) Term
theOr = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
imax (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
xs)
recurse [] = forall a. HasCallStack => a
__IMPOSSIBLE__
sys_alpha :: NamesT (TCMT IO) Term
sys_alpha = [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
-> NamesT (TCMT IO) Term
recurse [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
faces
NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
pOr NamesT (TCMT IO) Type
ty
NamesT (TCMT IO) Term
thePsi NamesT (TCMT IO) Term
phi
NamesT (TCMT IO) Term
sys_alpha (forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
u)
NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term
hcomp NamesT (TCMT IO) Type
ty (NamesT (TCMT IO) Term
thePsi NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
`imax` NamesT (TCMT IO) Term
phi) NamesT (TCMT IO) Term
sys NamesT (TCMT IO) Term
w1'
let
d0 :: Substitution
d0 :: Substitution' Term
d0 = forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
1
(forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
iz forall a. Substitution' a
IdS forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params)
up :: Pattern' DBPatVar
up = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con (PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
defaultPatternInfo Bool
False Bool
False forall a. Maybe a
Nothing Bool
False) forall a b. (a -> b) -> a -> b
$
forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
telePatterns (Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom Type)
fsT) (forall a. Nat -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Boundary
boundary)
let
pats :: [NamedArg (Pattern' DBPatVar)]
pats | forall a. Null a => a -> Bool
null Boundary
boundary = forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
gamma
| Bool
otherwise = forall a. Nat -> [a] -> [a]
take (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) (forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
gamma) forall a. [a] -> [a] -> [a]
++ [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ forall a name. a -> Named name a
unnamed forall a b. (a -> b) -> a -> b
$ Pattern' DBPatVar
up]
clause :: Clause
clause = Clause
{ clauseTel :: Tele (Dom Type)
clauseTel = Tele (Dom Type)
gamma
, clauseType :: Maybe (Arg Type)
clauseType = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Type
ty
, namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
, clauseFullRange :: Range
clauseFullRange = forall a. Range' a
noRange
, clauseLHSRange :: Range
clauseLHSRange = forall a. Range' a
noRange
, clauseCatchall :: Bool
clauseCatchall = Bool
False
, clauseBody :: Maybe Term
clauseBody = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term
body
, clauseExact :: Maybe Bool
clauseExact = forall a. a -> Maybe a
Just Bool
True
, clauseRecursive :: Maybe Bool
clauseRecursive = forall a. Maybe a
Nothing
, clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
}
cs :: [Clause]
cs = [Clause
clause]
QName -> [Clause] -> TCM ()
addClauses QName
theName [Clause]
cs
(Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses forall a. Maybe a
Nothing [Clause]
cs)
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe SplitTree
mst forall a b. (a -> b) -> a -> b
$ QName -> SplitTree -> TCM ()
setSplitTree QName
theName
QName -> CompiledClauses -> TCM ()
setCompiledClauses QName
theName CompiledClauses
cc
QName -> Bool -> TCM ()
setTerminates QName
theName Bool
True
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
theName
whenDefined :: Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
whenDefined Bool
False t ArgName
_ m (Maybe a)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
whenDefined Bool
True t ArgName
xs m (Maybe a)
m = do
t (Maybe Term)
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getTerm' t ArgName
xs
if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust t (Maybe Term)
xs then m (Maybe a)
m else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
defineProjections :: QName
-> ConHead
-> Telescope
-> [QName]
-> Telescope
-> 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
fieldTypes :: [Dom Type]
fieldTypes = ([ QName -> Elims -> Term
Def QName
f [] forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0] | QName
f <- forall a. [a] -> [a]
reverse [QName]
names ] forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Nat -> Substitution' a
raiseS Nat
1) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
fsT
projTel :: Tele (Dom Type)
projTel = forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
params (forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall a. a -> Dom a
defaultDom Type
t) (forall a. ArgName -> a -> Abs a
Abs ArgName
"d" forall a. Tele a
EmptyTel))
np :: Nat
np = forall a. Sized a => a -> Nat
size Tele (Dom Type)
params
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 (forall a. Integral a => a -> [a]
downFrom (forall a. Sized a => a -> Nat
size [Dom Type]
fieldTypes)) [QName]
names [Dom Type]
fieldTypes) forall a b. (a -> b) -> a -> b
$ \ (Nat
i,QName
projName,Dom Type
ty) -> do
let
projType :: Dom Type
projType = forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
projTel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
ty
cpi :: ConPatternInfo
cpi = PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
defaultPatternInfo Bool
False Bool
False (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT) Type
t) Bool
False
conp :: NamedArg (Pattern' DBPatVar)
conp = forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
cpi forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
fsT
sigma :: Substitution' Term
sigma = ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
fsT) forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
`consS` forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
fsT)
clause :: Clause
clause = forall a. Null a => a
empty
{ clauseTel :: Tele (Dom Type)
clauseTel = forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
params Tele (Dom Type)
fsT
, namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [ NamedArg (Pattern' DBPatVar)
conp ]
, clauseBody :: Maybe Term
clauseBody = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
i
, clauseType :: Maybe (Arg Type)
clauseType = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sigma forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
ty
, clauseRecursive :: Maybe Bool
clauseRecursive = forall a. a -> Maybe a
Just Bool
False
, clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
}
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.proj" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"proj" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Nat
i,Dom Type
ty)
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
projName, TCMT IO Doc
":", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
projType ]
]
forall a. TCM a -> TCM a
noMutualBlock forall a b. (a -> b) -> a -> b
$ do
let cs :: [Clause]
cs = [ Clause
clause ]
(Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses forall a. Maybe a
Nothing [Clause]
cs
let fun :: Defn
fun = Defn
emptyFunction
{ funClauses :: [Clause]
funClauses = [Clause]
cs
, funCompiled :: Maybe CompiledClauses
funCompiled = forall a. a -> Maybe a
Just CompiledClauses
cc
, funSplitTree :: Maybe SplitTree
funSplitTree = Maybe SplitTree
mst
, funProjection :: Maybe Projection
funProjection = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Projection
{ projProper :: Maybe QName
projProper = forall a. Maybe a
Nothing
, projOrig :: QName
projOrig = QName
projName
, projFromType :: Arg QName
projFromType = forall e. ArgInfo -> e -> Arg e
Arg (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom Type
ty) QName
dataName
, projIndex :: Nat
projIndex = Nat
np forall a. Num a => a -> a -> a
+ Nat
1
, projLams :: ProjLams
projLams = [Arg ArgName] -> ProjLams
ProjLams forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t a. Dom' t a -> Arg a
argFromDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
projTel
}
, funMutual :: Maybe [QName]
funMutual = forall a. a -> Maybe a
Just []
, funTerminates :: Maybe Bool
funTerminates = forall a. a -> Maybe a
Just Bool
True
}
Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
projName forall a b. (a -> b) -> a -> b
$
(ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
projName (forall t e. Dom' t e -> e
unDom Dom Type
projType) Language
lang Defn
fun)
{ defNoCompilation :: Bool
defNoCompilation = Bool
True
, defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
StrictPos]
}
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.proj.fun" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"proj" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Nat
i
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Defn
fun
]
freshAbstractQName'_ :: String -> TCM QName
freshAbstractQName'_ :: ArgName -> TCMT IO QName
freshAbstractQName'_ = Fixity' -> Name -> TCMT IO QName
freshAbstractQName Fixity'
noFixity' forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Name
C.simpleName
data LType = LEl Level Term deriving (LType -> LType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LType -> LType -> Bool
$c/= :: LType -> LType -> Bool
== :: LType -> LType -> Bool
$c== :: LType -> LType -> Bool
Eq,Nat -> LType -> ShowS
[LType] -> ShowS
LType -> ArgName
forall a.
(Nat -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LType] -> ShowS
$cshowList :: [LType] -> ShowS
show :: LType -> ArgName
$cshow :: LType -> ArgName
showsPrec :: Nat -> LType -> ShowS
$cshowsPrec :: Nat -> LType -> ShowS
Show)
fromLType :: LType -> Type
fromLType :: LType -> Type
fromLType (LEl Level
l Term
t) = forall t a. Sort' t -> a -> Type'' t a
El (forall t. Level' t -> Sort' t
Type Level
l) Term
t
lTypeLevel :: LType -> Level
lTypeLevel :: LType -> Level
lTypeLevel (LEl Level
l Term
t) = Level
l
toLType :: MonadReduce m => Type -> m (Maybe LType)
toLType :: forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType Type
ty = do
Sort' Term
sort <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort' Term
getSort Type
ty
case Sort' Term
sort of
Type Level
l -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Level -> Term -> LType
LEl Level
l (forall t a. Type'' t a -> a
unEl Type
ty)
Sort' Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
instance Subst LType where
type SubstArg LType = Term
applySubst :: Substitution' (SubstArg LType) -> LType -> LType
applySubst Substitution' (SubstArg LType)
rho (LEl Level
l Term
t) = Level -> Term -> LType
LEl (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg LType)
rho Level
l) (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg LType)
rho Term
t)
data CType = ClosedType Sort QName | LType LType deriving (CType -> CType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CType -> CType -> Bool
$c/= :: CType -> CType -> Bool
== :: CType -> CType -> Bool
$c== :: CType -> CType -> Bool
Eq,Nat -> CType -> ShowS
[CType] -> ShowS
CType -> ArgName
forall a.
(Nat -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [CType] -> ShowS
$cshowList :: [CType] -> ShowS
show :: CType -> ArgName
$cshow :: CType -> ArgName
showsPrec :: Nat -> CType -> ShowS
$cshowsPrec :: Nat -> CType -> ShowS
Show)
fromCType :: CType -> Type
fromCType :: CType -> Type
fromCType (ClosedType Sort' Term
s QName
q) = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (QName -> Elims -> Term
Def QName
q [])
fromCType (LType LType
t) = LType -> Type
fromLType LType
t
toCType :: MonadReduce m => Type -> m (Maybe CType)
toCType :: forall (m :: * -> *). MonadReduce m => Type -> m (Maybe CType)
toCType Type
ty = do
Sort' Term
sort <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort' Term
getSort Type
ty
case Sort' Term
sort of
Type Level
l -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ LType -> CType
LType (Level -> Term -> LType
LEl Level
l (forall t a. Type'' t a -> a
unEl Type
ty))
SSet Level
l -> do
Term
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
ty)
case Term
t of
Def QName
q [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Sort' Term -> QName -> CType
ClosedType (forall t. Level' t -> Sort' t
SSet Level
l) QName
q
Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
Sort' Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
instance Subst CType where
type SubstArg CType = Term
applySubst :: Substitution' (SubstArg CType) -> CType -> CType
applySubst Substitution' (SubstArg CType)
rho (ClosedType Sort' Term
s QName
t) = Sort' Term -> QName -> CType
ClosedType (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg CType)
rho Sort' Term
s) QName
t
applySubst Substitution' (SubstArg CType)
rho (LType LType
t) = LType -> CType
LType forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg CType)
rho LType
t
defineTranspOrHCompForFields
:: TranspOrHComp
-> (Maybe Term)
-> (Term -> QName -> Term)
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
defineTranspOrHCompForFields :: TranspOrHComp
-> Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom Type)
-> [Arg QName]
-> Type
-> TCM
(Maybe
((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
Substitution' Term))
defineTranspOrHCompForFields TranspOrHComp
cmd Maybe Term
pathCons Term -> QName -> Term
project QName
name Tele (Dom Type)
params Tele (Dom Type)
fsT [Arg QName]
fns Type
rect =
case TranspOrHComp
cmd of
TranspOrHComp
DoTransp -> forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
Tele (Dom CType)
fsT' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadReduce m => Type -> m (Maybe CType)
toCType)) Tele (Dom Type)
fsT
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom CType)
-> [Arg QName]
-> Type
-> TCM
((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
Substitution' Term)
defineTranspForFields Maybe Term
pathCons Term -> QName -> Term
project QName
name Tele (Dom Type)
params Tele (Dom CType)
fsT' [Arg QName]
fns Type
rect
TranspOrHComp
DoHComp -> forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
Tele (Dom LType)
fsT' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType)) Tele (Dom Type)
fsT
LType
rect' <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
toLType Type
rect
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom LType)
-> [Arg QName]
-> LType
-> TCM
((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
Substitution' Term)
defineHCompForFields Term -> QName -> Term
project QName
name Tele (Dom Type)
params Tele (Dom LType)
fsT' [Arg QName]
fns LType
rect'
defineTranspForFields
:: (Maybe Term)
-> (Term -> QName -> Term)
-> QName
-> Telescope
-> Tele (Dom CType)
-> [Arg QName]
-> Type
-> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
defineTranspForFields :: Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom CType)
-> [Arg QName]
-> Type
-> TCM
((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
Substitution' Term)
defineTranspForFields Maybe Term
pathCons Term -> QName -> Term
applyProj QName
name Tele (Dom Type)
params Tele (Dom CType)
fsT [Arg QName]
fns Type
rect = do
Type
interval <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
let deltaI :: Tele (Dom Type)
deltaI = Type -> Tele (Dom Type) -> Tele (Dom Type)
expTelescope Type
interval Tele (Dom Type)
params
Term
iz <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
Term
io <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
Term
imin <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMin"
Term
imax <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMax"
Term
ineg <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primINeg"
Term
transp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
builtinTrans
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom Type)
params
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom Type)
deltaI
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom CType)
fsT
let thePrefix :: ArgName
thePrefix = ArgName
"transp-"
QName
theName <- ArgName -> TCMT IO QName
freshAbstractQName'_ forall a b. (a -> b) -> a -> b
$ ArgName
thePrefix forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
P.prettyShow (QName -> Name
A.qnameName QName
name)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"trans.rec" Nat
5 forall a b. (a -> b) -> a -> b
$ (ArgName
"Generated name: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show QName
theName forall a. [a] -> [a] -> [a]
++ ArgName
" " forall a. [a] -> [a] -> [a]
++ QName -> ArgName
showQNameId QName
theName)
Type
theType <- (forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
deltaI forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
NamesT (TCMT IO) (Abs Type)
rect' <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) b a.
(MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
x -> let NamesT Fail Term
_ = NamesT Fail Term
x forall a. a -> a -> a
`asTypeOf` forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. HasCallStack => a
undefined :: Term) in
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
rect')
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
"phi" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
(forall a. Subst a => Abs a -> SubstArg a -> a
absApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
rect' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (forall a. Subst a => Abs a -> SubstArg a -> a
absApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) (Abs Type)
rect' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
theType
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"trans.rec" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"sort = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall a. LensSort a => a -> Sort' Term
getSort Type
rect')
Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
forall a. TCM a -> TCM a
noMutualBlock forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
theName forall a b. (a -> b) -> a -> b
$
(ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
theName Type
theType Language
lang
(Defn
emptyFunction { funTerminates :: Maybe Bool
funTerminates = forall a. a -> Maybe a
Just Bool
True }))
{ defNoCompilation :: Bool
defNoCompilation = Bool
True }
TelV Tele (Dom Type)
gamma Type
rtype <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
theType
let
theTerm :: Term
theTerm = QName -> Elims -> Term
Def QName
theName [] forall t. Apply t => t -> [Arg Term] -> t
`apply` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma
clause_types :: [Dom CType]
clause_types = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Term
theTerm Term -> QName -> Term
`applyProj` (forall e. Arg e -> e
unArg Arg QName
fn)
| Arg QName
fn <- forall a. [a] -> [a]
reverse [Arg QName]
fns] forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
0 Term
io forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom CType)
fsT')
delta_i :: Substitution' Term
delta_i = (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
deltaI)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params)
fsT' :: Tele (Dom CType)
fsT' = (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
deltaI)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
Tele (Dom CType)
fsT
lam_i :: Term -> Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ArgName -> a -> Abs a
Abs ArgName
"i"
gamma' :: Tele (Dom Type)
gamma' = ListTel -> Tele (Dom Type)
telFromList forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
take (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- Nat
1) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
gamma
d0 :: Substitution
d0 :: Substitution' Term
d0 = forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
1
(forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
iz forall a. Substitution' a
IdS forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params)
(Tele (Dom Type)
tel,Substitution' Term
theta,Term
the_phi,Term
the_u0, [Term]
the_fields) =
case Maybe Term
pathCons of
Just Term
u -> (forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
gamma' (Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CType -> Type
fromCType) Tele (Dom CType)
fsT)
, (forall a. Nat -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Nat
size Tele (Dom CType)
fsT) Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u) forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
`consS` forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom CType)
fsT)
, forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Tele (Dom CType)
fsT) (Nat -> Term
var Nat
0)
, (forall a. Nat -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Nat
size Tele (Dom CType)
fsT) Substitution' Term
d0 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u)
, forall a. Nat -> [a] -> [a]
drop (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma') forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel)
Maybe Term
Nothing -> (Tele (Dom Type)
gamma, forall a. Substitution' a
IdS, Nat -> Term
var Nat
1, Nat -> Term
var Nat
0, forall a b. (a -> b) -> [a] -> [b]
map (\ Arg QName
fname -> Nat -> Term
var Nat
0 Term -> QName -> Term
`applyProj` forall e. Arg e -> e
unArg Arg QName
fname) [Arg QName]
fns )
fsT_tel :: Tele (Dom CType)
fsT_tel = (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
deltaI)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom CType)
fsT
iMin :: Term -> Term -> Term
iMin Term
x Term
y = Term
imin forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
x, forall e. e -> Arg e
argN Term
y]
iMax :: Term -> Term -> Term
iMax Term
x Term
y = Term
imax forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
x, forall e. e -> Arg e
argN Term
y]
iNeg :: Term -> Term
iNeg Term
x = Term
ineg forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
x]
mkBody :: (Term, Dom CType) -> TCMT IO Term
mkBody (Term
field, Dom CType
filled_ty') = do
let
filled_ty :: Term
filled_ty = Term -> Term
lam_i forall a b. (a -> b) -> a -> b
$ (forall t a. Type'' t a -> a
unEl forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
fromCType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Dom CType
filled_ty'
case forall t e. Dom' t e -> e
unDom Dom CType
filled_ty' of
LType (LEl Level
l Term
_) -> do
let lvl :: Term
lvl = Term -> Term
lam_i forall a b. (a -> b) -> a -> b
$ Level -> Term
Level Level
l
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ do
NamesT Fail Term
lvl <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
lvl
[NamesT Fail Term
phi,NamesT Fail Term
field] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
the_phi,Term
field]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
transp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT Fail Term
lvl forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
filled_ty
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
phi
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
field
ClosedType{} ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ do
[NamesT Fail Term
field] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
field]
NamesT Fail Term
field
let
tau :: Substitution' Term
tau = forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$ [Term]
us forall a. [a] -> [a] -> [a]
++ (Term
phi Term -> Term -> Term
`iMax` Term -> Term
iNeg (Nat -> Term
var Nat
0))
forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (\ Term
d -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
d forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Term
iMin (Nat -> Term
var Nat
0) (Nat -> Term
var Nat
1))]) [Term]
ds
where
([Term]
us, Term
phi:[Term]
ds) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma') forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse (forall a. Subst a => Nat -> a -> a
raise Nat
1 (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg (forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel)))
let
go :: [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
go [Term]
acc [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
go [Term]
acc ((Term
fname,Dom CType
field_ty) : [(Term, Dom CType)]
ps) = do
let
filled_ty :: Dom CType
filled_ty = forall a. DeBruijn a => [a] -> Substitution' a
parallelS (Substitution' Term
tau forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Term]
acc) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Dom CType
field_ty
Term
b <- (Term, Dom CType) -> TCMT IO Term
mkBody (Term
fname,Dom CType
filled_ty)
[Term]
bs <- [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
go (Term
b forall a. a -> [a] -> [a]
: [Term]
acc) [(Term, Dom CType)]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term
b forall a. a -> [a] -> [a]
: [Term]
bs
[Term]
bodys <- [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
go [] (forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
the_fields (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom CType)
fsT_tel))
let
theSubst :: Substitution' Term
theSubst = forall a. [a] -> [a]
reverse (Substitution' Term
tau forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Term]
bodys) forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# (forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
deltaI)) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ((QName
theName, Tele (Dom Type)
tel, Substitution' Term
theta forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
rtype, forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CType -> Type
fromCType) [Dom CType]
clause_types, [Term]
bodys), Substitution' Term
theSubst)
where
rect' :: Type
rect' = forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
params forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
rect
sub :: a -> Substitution' Term
sub a
tel = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [ Nat -> Term
var Nat
n forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0] | Nat
n <- [Nat
1..forall a. Sized a => a -> Nat
size a
tel] ]
expTelescope :: Type -> Telescope -> Telescope
expTelescope :: Type -> Tele (Dom Type) -> Tele (Dom Type)
expTelescope Type
int Tele (Dom Type)
tel = [ArgName] -> [Dom Type] -> Tele (Dom Type)
unflattenTel [ArgName]
names [Dom Type]
ys
where
xs :: [Dom Type]
xs = forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
names :: [ArgName]
names = Tele (Dom Type) -> [ArgName]
teleNames Tele (Dom Type)
tel
t :: Tele (Dom Type)
t = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall a. a -> Dom a
defaultDom forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) Type
int) (forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a. Tele a
EmptyTel)
s :: Substitution' Term
s = forall {a}. Sized a => a -> Substitution' Term
sub Tele (Dom Type)
tel
ys :: [Dom Type]
ys = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
s) [Dom Type]
xs
defineHCompForFields
:: (Term -> QName -> Term)
-> QName
-> Telescope
-> Tele (Dom LType)
-> [Arg QName]
-> LType
-> TCM ((QName, Telescope, Type, [Dom Type], [Term]),Substitution)
defineHCompForFields :: (Term -> QName -> Term)
-> QName
-> Tele (Dom Type)
-> Tele (Dom LType)
-> [Arg QName]
-> LType
-> TCM
((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
Substitution' Term)
defineHCompForFields Term -> QName -> Term
applyProj QName
name Tele (Dom Type)
params Tele (Dom LType)
fsT [Arg QName]
fns LType
rect = do
Type
interval <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
let delta :: Tele (Dom Type)
delta = Tele (Dom Type)
params
Term
iz <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
Term
io <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
Term
imin <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMin"
Term
imax <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMax"
Term
tIMax <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primIMax"
Term
ineg <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primINeg"
Term
hcomp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
builtinHComp
Term
transp <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
builtinTrans
Term
por <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m Term
getPrimitiveTerm ArgName
"primPOr"
Term
one <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"comp.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom Type)
params
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"comp.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom Type)
delta
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"comp.rec" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Tele (Dom LType)
fsT
let thePrefix :: ArgName
thePrefix = ArgName
"hcomp-"
QName
theName <- ArgName -> TCMT IO QName
freshAbstractQName'_ forall a b. (a -> b) -> a -> b
$ ArgName
thePrefix forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
P.prettyShow (QName -> Name
A.qnameName QName
name)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> ArgName -> m ()
reportSLn ArgName
"hcomp.rec" Nat
5 forall a b. (a -> b) -> a -> b
$ (ArgName
"Generated name: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show QName
theName forall a. [a] -> [a] -> [a]
++ ArgName
" " forall a. [a] -> [a] -> [a]
++ QName -> ArgName
showQNameId QName
theName)
Type
theType <- (forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
delta forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
NamesT (TCMT IO) Type
rect <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ LType -> Type
fromLType LType
rect
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
"phi" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
ArgName
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' ArgName
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType (\ NamesT (TCMT IO) Term
i ->
forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
ArgName
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' ArgName
"o" NamesT (TCMT IO) Term
phi forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Type
rect) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
NamesT (TCMT IO) Type
rect forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> NamesT (TCMT IO) Type
rect
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
theType
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"sort = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (LType -> Level
lTypeLevel LType
rect)
Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
forall a. TCM a -> TCM a
noMutualBlock forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM ()
addConstant QName
theName forall a b. (a -> b) -> a -> b
$
(ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
theName Type
theType Language
lang
(Defn
emptyFunction { funTerminates :: Maybe Bool
funTerminates = forall a. a -> Maybe a
Just Bool
True }))
{ defNoCompilation :: Bool
defNoCompilation = Bool
True }
TelV Tele (Dom Type)
gamma Type
rtype <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
theType
let
drect_gamma :: LType
drect_gamma = forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` LType
rect
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"sort = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (LType -> Level
lTypeLevel LType
drect_gamma)
let
compTerm :: Term
compTerm = QName -> Elims -> Term
Def QName
theName [] forall t. Apply t => t -> [Arg Term] -> t
`apply` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma
the_phi :: Term
the_phi = Nat -> Term
var Nat
2
the_u :: Term
the_u = Nat -> Term
var Nat
1
the_u0 :: Term
the_u0 = Nat -> Term
var Nat
0
fillTerm :: Term
fillTerm = forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ do
NamesT Fail Term
rect <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Type'' t a -> a
unEl forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Type
fromLType forall a b. (a -> b) -> a -> b
$ LType
drect_gamma
NamesT Fail Term
lvl <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level -> Term
Level forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Level
lTypeLevel forall a b. (a -> b) -> a -> b
$ LType
drect_gamma
[NamesT Fail (Arg Term)]
params <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
take (forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma
[NamesT Fail Term
phi,NamesT Fail Term
w,NamesT Fail Term
w0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
the_phi,Term
the_u,Term
the_u0]
forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
i -> do
[Arg Term]
args <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [NamesT Fail (Arg Term)]
params
Term
psi <- forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
imax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i)
Term
u <- forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"j" (\ NamesT Fail Term
j -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
por forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT Fail Term
lvl
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
phi
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
ineg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i)
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"_" (\ NamesT Fail Term
o -> NamesT Fail Term
rect)
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT Fail Term
w forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
imin forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
j))
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"_" (\ NamesT Fail Term
o -> NamesT Fail Term
w0)
)
Term
u0 <- NamesT Fail Term
w0
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
theName [] forall t. Apply t => t -> [Arg Term] -> t
`apply` ([Arg Term]
args forall a. [a] -> [a] -> [a]
++ [forall e. e -> Arg e
argN Term
psi, forall e. e -> Arg e
argN Term
u, forall e. e -> Arg e
argN Term
u0])
clause_types :: [Dom LType]
clause_types = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Term
compTerm Term -> QName -> Term
`applyProj` (forall e. Arg e -> e
unArg Arg QName
fn)
| Arg QName
fn <- forall a. [a] -> [a]
reverse [Arg QName]
fns] forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (forall a. Nat -> Substitution' a
raiseS (forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom LType)
fsT)
fsT' :: Tele (Dom LType)
fsT' = forall a. Nat -> Substitution' a
raiseS ((forall a. Sized a => a -> Nat
size Tele (Dom Type)
gamma forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size Tele (Dom Type)
delta) forall a. Num a => a -> a -> a
+ Nat
1) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom LType)
fsT
filled_types :: [Dom LType]
filled_types = forall a. DeBruijn a => [a] -> Substitution' a
parallelS [forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
fillTerm forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
0] Term -> QName -> Term
`applyProj` (forall e. Arg e -> e
unArg Arg QName
fn)
| Arg QName
fn <- forall a. [a] -> [a]
reverse [Arg QName]
fns] forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom LType)
fsT'
NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
comp <- do
let
imax :: NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
imax NamesT Fail Term
i NamesT Fail Term
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
j
let forward :: NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
forward NamesT Fail Term
la NamesT Fail Term
bA NamesT Fail Term
r NamesT Fail Term
u = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
transp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT Fail Term
i -> NamesT Fail Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT Fail Term
i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
`imax` NamesT Fail Term
r))
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT Fail Term
i -> NamesT Fail Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT Fail Term
i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
`imax` NamesT Fail Term
r))
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
r
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
u
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
la NamesT Fail Term
bA NamesT Fail Term
phi NamesT Fail Term
u NamesT Fail Term
u0 ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
hcomp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT Fail Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT Fail Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT Fail Term
phi
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" (\ NamesT Fail Term
i -> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
o ->
NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
forward NamesT Fail Term
la NamesT Fail Term
bA NamesT Fail Term
i (NamesT Fail Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT Fail Term
o))
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
forward NamesT Fail Term
la NamesT Fail Term
bA (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz) NamesT Fail Term
u0
let
mkBody :: (Arg QName, Dom LType) -> TCMT IO Term
mkBody (Arg QName
fname, Dom LType
filled_ty') = do
let
proj :: NamesT Fail Term -> NamesT Fail Term
proj NamesT Fail Term
t = (Term -> QName -> Term
`applyProj` forall e. Arg e -> e
unArg Arg QName
fname) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT Fail Term
t
filled_ty :: Term
filled_ty = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a b. (a -> b) -> a -> b
$ (forall t a. Type'' t a -> a
unEl forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Type
fromLType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Dom LType
filled_ty')
Level
l <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ LType -> Level
lTypeLevel forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom LType
filled_ty'
let lvl :: Term
lvl = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (forall a. ArgName -> a -> Abs a
Abs ArgName
"i" forall a b. (a -> b) -> a -> b
$ Level -> Term
Level Level
l)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [ArgName] -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ do
NamesT Fail Term
lvl <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
lvl
[NamesT Fail Term
phi,NamesT Fail Term
w,NamesT Fail Term
w0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open [Term
the_phi,Term
the_u,Term
the_u0]
NamesT Fail Term
filled_ty <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
filled_ty
NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
-> NamesT Fail Term
comp NamesT Fail Term
lvl
NamesT Fail Term
filled_ty
NamesT Fail Term
phi
(forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
i -> forall (m :: * -> *).
MonadFail m =>
ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam ArgName
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT Fail Term
o -> NamesT Fail Term -> NamesT Fail Term
proj forall a b. (a -> b) -> a -> b
$ NamesT Fail Term
w forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT Fail Term
o)
(NamesT Fail Term -> NamesT Fail Term
proj NamesT Fail Term
w0)
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"hcomp.rec" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"filled_types sorts:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensSort a => a -> Sort' Term
getSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. LType -> Type
fromLType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom LType]
filled_types)
[Term]
bodys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Arg QName, Dom LType) -> TCMT IO Term
mkBody (forall a b. [a] -> [b] -> [(a, b)]
zip [Arg QName]
fns [Dom LType]
filled_types)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ((QName
theName, Tele (Dom Type)
gamma, Type
rtype, forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LType -> Type
fromLType) [Dom LType]
clause_types, [Term]
bodys),forall a. Substitution' a
IdS)
getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]
getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]
getGeneralizedParameters Set Name
gpars QName
name | forall a. Set a -> Bool
Set.null Set Name
gpars = forall (m :: * -> *) a. Monad m => a -> m a
return []
getGeneralizedParameters Set Name
gpars QName
name = do
let inscope :: Name -> Maybe Name
inscope Name
x = Name
x forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a. Ord a => a -> Set a -> Bool
Set.member Name
x Set Name
gpars)
forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> Maybe Name
inscope) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> [Maybe Name]
defGeneralizedParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name)
bindGeneralizedParameters :: [Maybe Name] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindGeneralizedParameters :: forall a.
[Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [] Type
t Tele (Dom Type) -> Type -> TCM a
ret = Tele (Dom Type) -> Type -> TCM a
ret forall a. Tele a
EmptyTel Type
t
bindGeneralizedParameters (Maybe Name
name : [Maybe Name]
names) Type
t Tele (Dom Type) -> Type -> TCM a
ret =
case forall t a. Type'' t a -> a
unEl Type
t of
Pi Dom Type
a Abs Type
b -> TCM a -> TCM a
ext forall a b. (a -> b) -> a -> b
$ forall a.
[Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [Maybe Name]
names (forall a. Abs a -> a
unAbs Abs Type
b) forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
tel Type
t -> Tele (Dom Type) -> Type -> TCM a
ret (forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Tele (Dom Type)
tel forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Abs Type
b)) Type
t
where
ext :: TCM a -> TCM a
ext | Just Name
x <- Maybe Name
name = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Name
x, Dom Type
a)
| Bool
otherwise = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. Abs a -> ArgName
absName Abs Type
b, Dom Type
a)
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
bindParameters
:: Int
-> [A.LamBinding]
-> Type
-> (Telescope -> Type -> TCM a)
-> TCM a
bindParameters :: forall a.
Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters Nat
0 [] Type
a Tele (Dom Type) -> Type -> TCM a
ret = Tele (Dom Type) -> Type -> TCM a
ret forall a. Tele a
EmptyTel Type
a
bindParameters Nat
0 (LamBinding
par : [LamBinding]
_) Type
_ Tele (Dom Type) -> Type -> TCM a
_ = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Unexpected parameter" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LamBinding
par
bindParameters Nat
npars [] Type
t Tele (Dom Type) -> Type -> TCM a
ret =
case forall t a. Type'' t a -> a
unEl Type
t of
Pi Dom Type
a Abs Type
b | Bool -> Bool
not (forall a. LensHiding a => a -> Bool
visible Dom Type
a) -> do
Name
x <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (forall a. Abs a -> ArgName
absName Abs Type
b)
forall a.
Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Nat
npars [] Name
x Dom Type
a Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret
| Bool
otherwise ->
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Expected binding for parameter"
, forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Abs a -> ArgName
absName Abs Type
b) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t e. Dom' t e -> e
unDom Dom Type
a) ]
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
bindParameters Nat
npars par :: [LamBinding]
par@(A.DomainFull (A.TBind Range
_ TacticAttr
_ List1 (NamedArg Binder)
xs Expr
e) : [LamBinding]
bs) Type
a Tele (Dom Type) -> Type -> TCM a
ret =
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange [LamBinding]
par forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
let s :: ArgName
s | forall (t :: * -> *) a. Foldable t => t a -> Nat
length List1 (NamedArg Binder)
xs forall a. Ord a => a -> a -> Bool
> Nat
1 = ArgName
"s"
| Bool
otherwise = ArgName
""
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"Unexpected type signature for parameter" forall a. [a] -> [a] -> [a]
++ ArgName
s) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg Binder)
xs)
bindParameters Nat
_ (A.DomainFull A.TLet{} : [LamBinding]
_) Type
_ Tele (Dom Type) -> Type -> TCM a
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
bindParameters Nat
_ (par :: LamBinding
par@(A.DomainFree TacticAttr
_ NamedArg Binder
arg) : [LamBinding]
ps) Type
_ Tele (Dom Type) -> Type -> TCM a
_
| forall a. LensModality a => a -> Modality
getModality NamedArg Binder
arg forall a. Eq a => a -> a -> Bool
/= Modality
defaultModality = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Unexpected modality/relevance annotation in" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LamBinding
par
bindParameters Nat
npars ps0 :: [LamBinding]
ps0@(par :: LamBinding
par@(A.DomainFree TacticAttr
_ NamedArg Binder
arg) : [LamBinding]
ps) Type
t Tele (Dom Type) -> Type -> TCM a
ret = do
let x :: Binder
x = forall a. NamedArg a -> a
namedArg NamedArg Binder
arg
TelV Tele (Dom Type)
tel Type
_ = Type -> TelV Type
telView' Type
t
case forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg Binder
arg forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel of
ImplicitInsertion
NoInsertNeeded -> [LamBinding] -> Name -> TCM a
continue [LamBinding]
ps forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind forall a b. (a -> b) -> a -> b
$ forall a. Binder' a -> a
A.binderName Binder
x
ImpInsert [Dom ()]
_ -> [LamBinding] -> Name -> TCM a
continue [LamBinding]
ps0 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (forall a. Abs a -> ArgName
absName Abs Type
b)
ImplicitInsertion
BadImplicits -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Unexpected parameter" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LamBinding
par
NoSuchName ArgName
x -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange LamBinding
par forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"No parameter of name " forall a. [a] -> [a] -> [a]
++ ArgName
x)
where
Pi dom :: Dom Type
dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info', unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b = forall t a. Type'' t a -> a
unEl Type
t
continue :: [LamBinding] -> Name -> TCM a
continue [LamBinding]
ps Name
x = forall a.
Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Nat
npars [LamBinding]
ps Name
x Dom Type
dom Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret
bindParameter :: Int -> [A.LamBinding] -> Name -> Dom Type -> Abs Type -> (Telescope -> Type -> TCM a) -> TCM a
bindParameter :: forall a.
Nat
-> [LamBinding]
-> Name
-> Dom Type
-> Abs Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameter Nat
npars [LamBinding]
ps Name
x Dom Type
a Abs Type
b Tele (Dom Type) -> Type -> TCM a
ret =
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Name
x, Dom Type
a) forall a b. (a -> b) -> a -> b
$
forall a.
Nat
-> [LamBinding]
-> Type
-> (Tele (Dom Type) -> Type -> TCM a)
-> TCM a
bindParameters (Nat
npars forall a. Num a => a -> a -> a
- Nat
1) [LamBinding]
ps (forall a. Subst a => Abs a -> a
absBody Abs Type
b) forall a b. (a -> b) -> a -> b
$ \ Tele (Dom Type)
tel Type
s ->
Tele (Dom Type) -> Type -> TCM a
ret (forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs (Name -> ArgName
nameToArgName Name
x) Tele (Dom Type)
tel) Type
s
fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Int
fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn UniverseCheck
uc [IsForced]
forceds Type
t Sort' Term
s = do
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.data.fits" Nat
10 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"does" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
, TCMT IO Doc
"of sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. LensSort a => a -> Sort' Term
getSort Type
t)
, TCMT IO Doc
"fit in" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort' Term
s forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"?"
]
Bool
withoutK <- forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
withoutK forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant Sort' Term
s) forall a b. (a -> b) -> a -> b
$ do
Quantity
q <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Quantity TCEnv
eQuantity
MonadConstraint (TCMT IO) => Modality -> Term -> TCM ()
usableAtModality (forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
q Modality
defaultModality) (forall t a. Type'' t a -> a
unEl Type
t)
Bool -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn' Bool
withoutK [IsForced]
forceds Type
t Sort' Term
s
where
fitsIn' :: Bool -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn' Bool
withoutK [IsForced]
forceds Type
t Sort' Term
s = do
Maybe (Bool, Dom Type, Abs Type)
vt <- do
Either (Dom Type, Abs Type) Type
t <- forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi Type
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Either (Dom Type, Abs Type) Type
t of
Left (Dom Type
a,Abs Type
b) -> forall a. a -> Maybe a
Just (Bool
True ,Dom Type
a,Abs Type
b)
Right (El Sort' Term
_ Term
t) | Pi Dom Type
a Abs Type
b <- Term
t
-> forall a. a -> Maybe a
Just (Bool
False,Dom Type
a,Abs Type
b)
Either (Dom Type, Abs Type) Type
_ -> forall a. Maybe a
Nothing
case Maybe (Bool, Dom Type, Abs Type)
vt of
Just (Bool
isPath, Dom Type
dom, Abs Type
b) -> do
let (IsForced
forced,[IsForced]
forceds') = [IsForced] -> (IsForced, [IsForced])
nextIsForced [IsForced]
forceds
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IsForced -> Bool
isForced IsForced
forced Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
withoutK) forall a b. (a -> b) -> a -> b
$ do
Sort' Term
sa <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort' Term
getSort Dom Type
dom
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
isPath Bool -> Bool -> Bool
|| UniverseCheck
uc forall a. Eq a => a -> a -> Bool
== UniverseCheck
NoUniverseCheck Bool -> Bool -> Bool
|| Sort' Term
sa forall a. Eq a => a -> a -> Bool
== forall t. Sort' t
SizeUniv) forall a b. (a -> b) -> a -> b
$
Sort' Term
sa forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
`leqSort` Sort' Term
s
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. Abs a -> ArgName
absName Abs Type
b, Dom Type
dom) forall a b. (a -> b) -> a -> b
$ do
forall a. Enum a => a -> a
succ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [IsForced] -> Type -> Sort' Term -> TCMT IO Nat
fitsIn' Bool
withoutK [IsForced]
forceds' (forall a. Subst a => Abs a -> a
absBody Abs Type
b) (forall a. Subst a => Nat -> a -> a
raise Nat
1 Sort' Term
s)
Maybe (Bool, Dom Type, Abs Type)
_ -> do
forall a. LensSort a => a -> Sort' Term
getSort Type
t forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
`leqSort` Sort' Term
s
forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0
checkIndexSorts :: Sort -> Telescope -> TCM ()
checkIndexSorts :: Sort' Term -> Tele (Dom Type) -> TCM ()
checkIndexSorts Sort' Term
s = \case
Tele (Dom Type)
EmptyTel -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel' -> do
let sa :: Sort' Term
sa = forall a. LensSort a => a -> Sort' Term
getSort Dom Type
a
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Sort' Term
sa forall a. Eq a => a -> a -> Bool
== forall t. Sort' t
SizeUniv) forall a b. (a -> b) -> a -> b
$ Sort' Term
sa forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
`leqSort` Sort' Term
s
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs (Tele (Dom Type))
tel' forall a b. (a -> b) -> a -> b
$ Sort' Term -> Tele (Dom Type) -> TCM ()
checkIndexSorts (forall a. Subst a => Nat -> a -> a
raise Nat
1 Sort' Term
s)
data IsPathCons = PathCons | PointCons
deriving (IsPathCons -> IsPathCons -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsPathCons -> IsPathCons -> Bool
$c/= :: IsPathCons -> IsPathCons -> Bool
== :: IsPathCons -> IsPathCons -> Bool
$c== :: IsPathCons -> IsPathCons -> Bool
Eq,Nat -> IsPathCons -> ShowS
[IsPathCons] -> ShowS
IsPathCons -> ArgName
forall a.
(Nat -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [IsPathCons] -> ShowS
$cshowList :: [IsPathCons] -> ShowS
show :: IsPathCons -> ArgName
$cshow :: IsPathCons -> ArgName
showsPrec :: Nat -> IsPathCons -> ShowS
$cshowsPrec :: Nat -> IsPathCons -> ShowS
Show)
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
constrT :: Nat -> Type -> TCM IsPathCons
constrT :: Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
t = do
Type
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pathV <- forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf
case forall t a. Type'' t a -> a
unEl Type
t of
Pi Dom Type
_ (NoAbs ArgName
_ Type
b) -> Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
b
Pi Dom Type
a Abs Type
b -> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b forall a b. (a -> b) -> a -> b
$ Nat -> Type -> TCM IsPathCons
constrT (Nat
n forall a. Num a => a -> a -> a
+ Nat
1)
Term
_ | Left ((Dom Type
a,Abs Type
b),(Term, Term)
_) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pathV Type
t -> do
IsPathCons
_ <- case Abs Type
b of
NoAbs ArgName
_ Type
b -> Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
b
Abs Type
b -> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs Type
b forall a b. (a -> b) -> a -> b
$ Nat -> Type -> TCM IsPathCons
constrT (Nat
n forall a. Num a => a -> a -> a
+ Nat
1)
forall (m :: * -> *) a. Monad m => a -> m a
return IsPathCons
PathCons
Def QName
d Elims
es | QName
d forall a. Eq a => a -> a -> Bool
== QName
q -> do
let vs :: [Arg Term]
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
let ([Arg Term]
pars, [Arg Term]
ixs) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
nofPars [Arg Term]
vs
forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh Nat m) =>
Nat -> [Arg Term] -> m ()
checkParams Nat
n [Arg Term]
pars
forall (m :: * -> *) a. Monad m => a -> m a
return IsPathCons
PointCons
MetaV{} -> do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
let td :: Type
td = Definition -> Type
defType Definition
def
TelV Tele (Dom Type)
tel Type
core <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
td
let us :: [Arg Term]
us = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg ArgName
arg Nat
x -> Nat -> Term
var Nat
x forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg ArgName
arg ) (forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Tele (Dom Type)
tel) forall a b. (a -> b) -> a -> b
$
forall a. Nat -> [a] -> [a]
take Nat
nofPars forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom (Nat
nofPars forall a. Num a => a -> a -> a
+ Nat
n)
[Arg Term]
xs <- forall (m :: * -> *). MonadMetaSolver m => Type -> m [Arg Term]
newArgsMeta forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
td [Arg Term]
us
let t' :: Type
t' = forall t a. Sort' t -> a -> Type'' t a
El (forall a. Subst a => Nat -> a -> a
raise Nat
n forall a b. (a -> b) -> a -> b
$ Defn -> Sort' Term
dataSort forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ [Arg Term]
us forall a. [a] -> [a] -> [a]
++ [Arg Term]
xs
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t Type
t')
(Nat -> Type -> TCM IsPathCons
constrT Nat
n Type
t')
(forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldEndInApplicationOfTheDatatype Type
t)
Term
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldEndInApplicationOfTheDatatype Type
t
checkParams :: Nat -> [Arg Term] -> m ()
checkParams Nat
n [Arg Term]
vs = forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh Nat m) =>
Arg Term -> Nat -> m ()
sameVar [Arg Term]
vs [Nat]
ps
where
nvs :: Nat
nvs = forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Term]
vs
ps :: [Nat]
ps = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
take Nat
nvs [Nat
n..]
sameVar :: Arg Term -> Nat -> m ()
sameVar Arg Term
arg Nat
i
| forall a. LensRelevance a => a -> Bool
isIrrelevant Arg Term
arg = forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = do
Type
t <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Type
typeOfBV Nat
i
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t (forall e. Arg e -> e
unArg Arg Term
arg) (Nat -> Term
var Nat
i)
isCoinductive :: Type -> TCM (Maybe Bool)
isCoinductive :: Type -> TCM (Maybe Bool)
isCoinductive Type
t = do
El Sort' Term
s Term
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
case Term
t of
Def QName
q Elims
_ -> do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
case Definition -> Defn
theDef Definition
def of
Axiom {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
DataOrRecSig{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Function {} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Datatype {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
Record { recInduction :: Defn -> Maybe Induction
recInduction = Just Induction
CoInductive } -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
True)
Record { recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
_ } -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
GeneralizableVar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Constructor {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Primitive {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
PrimitiveSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
AbstractDefn{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Var {} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Lam {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Lit {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Level {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Con {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Pi {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
Sort {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
MetaV {} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
DontCare{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Dummy ArgName
s Elims
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
ArgName -> m a
__IMPOSSIBLE_VERBOSE__ ArgName
s