{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Record where
import Prelude hiding (null)
import Control.Monad
import Data.Maybe
import qualified Data.Set as Set
import Agda.Interaction.Options
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Position
import qualified Agda.Syntax.Info as Info
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Rewriting.Confluence
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.CompiledClause (hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Rules.Data
( getGeneralizedParameters, bindGeneralizedParameters, bindParameters
, checkDataSort, fitsIn, forceSort
, defineCompData, defineKanOperationForFields
)
import Agda.TypeChecking.Rules.Term ( isType_ )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkDecl)
import Agda.Utils.List (headWithDefault)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.POMonoid
import Agda.Utils.Pretty (render)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.WithDefault
import Agda.Utils.Impossible
checkRecDef
:: A.DefInfo
-> QName
-> UniverseCheck
-> A.RecordDirectives
-> A.DataDefParams
-> A.Expr
-> [A.Field]
-> TCM ()
checkRecDef :: DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Field]
-> TCM ()
checkRecDef DefInfo
i QName
name UniverseCheck
uc (RecordDirectives Maybe (Ranged Induction)
ind Maybe HasEta0
eta0 Maybe Range
pat Maybe QName
con) (A.DataDefParams Set Name
gpars [LamBinding]
ps) Expr
contel0 [Field]
fields = do
Expr
aType <- QName -> Expr
A.Def forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinSet
let contel :: Expr
contel = PiView -> Expr
A.unPiView forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ (A.PiView [(ExprInfo, Telescope1)]
tels Expr
_) -> [(ExprInfo, Telescope1)] -> Expr -> PiView
A.PiView [(ExprInfo, Telescope1)]
tels Expr
aType) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> PiView
A.piView forall a b. (a -> b) -> a -> b
$ Expr
contel0
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> [LamBinding] -> [Field] -> Call
CheckRecDef (forall a. HasRange a => a -> Range
getRange QName
name) QName
name [LamBinding]
ps [Field]
fields) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"checking record def" 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
$ TCMT IO Doc
"ps =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [LamBinding]
ps)
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"contel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
contel
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"fields =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Constr a
Constr [Field]
fields)
]
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__
[Maybe Name]
parNames <- Set Name -> QName -> TCM [Maybe Name]
getGeneralizedParameters Set Name
gpars QName
name
forall a.
[Maybe Name] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [Maybe Name]
parNames Type
t forall a b. (a -> b) -> a -> b
$ \ Telescope
gtel Type
t0 ->
forall a.
Nat
-> [LamBinding] -> Type -> (Telescope -> 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
$ \ Telescope
ptel Type
t0 -> do
let tel :: Telescope
tel = forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gtel Telescope
ptel
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking fields"
Type
contype <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCMT IO Type
isType_ Expr
contel
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" 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
"contype = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
contype ]
let TelV Telescope
ftel Type
_ = Type -> TelV Type
telView' Type
contype
TelV Telescope
idxTel Type
s <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t0
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null Telescope
idxTel) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort Type
t0
Sort
s <- Type -> TCM Sort
forceSort Type
s
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ do
Telescope
gamma <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
TCMT IO Doc
"gamma = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma)
Type
rect <- forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Elims -> Term
Def QName
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
let contype :: Type
contype = Telescope -> Type -> Type
telePi_ Telescope
ftel (forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Telescope
ftel) Type
rect)
(Bool
hasNamedCon, QName
conName) <- case Maybe QName
con of
Just QName
c -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, QName
c)
Maybe QName
Nothing -> do
ModuleName
m <- forall a. KillRange a => KillRangeT a
killRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
let r :: Doc
r = forall a. Pretty a => a -> Doc
P.pretty forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
name
QName
c <- ModuleName -> Name -> QName
qualify ModuleName
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (Doc -> [Char]
render Doc
r forall a. [a] -> [a] -> [a]
++ [Char]
".constructor")
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, QName
c)
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"adding record type to signature"
Bool
etaenabled <- forall (m :: * -> *). HasOptions m => m Bool
etaEnabled
let getName :: A.Declaration -> [Dom QName]
getName :: Field -> [Dom' Term QName]
getName (A.Field DefInfo
_ QName
x Arg Expr
arg) = [QName
x forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall a. Arg a -> Dom a
domFromArg Arg Expr
arg]
getName (A.ScopedDecl ScopeInfo
_ [Field
f]) = Field -> [Dom' Term QName]
getName Field
f
getName Field
_ = []
setTactic :: Dom' t e -> Dom' t e -> Dom' t e
setTactic Dom' t e
dom Dom' t e
f = Dom' t e
f { domTactic :: Maybe t
domTactic = forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
dom }
fs :: [Dom' Term QName]
fs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {t} {e} {t} {e}. Dom' t e -> Dom' t e -> Dom' t e
setTactic (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
ftel) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Field -> [Dom' Term QName]
getName [Field]
fields
indCo :: Maybe Induction
indCo = forall a. Ranged a -> a
rangedThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Ranged Induction)
ind
conInduction :: Induction
conInduction = forall a. a -> Maybe a -> a
fromMaybe Induction
Inductive Maybe Induction
indCo
haveEta :: EtaEquality
haveEta = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (HasEta -> EtaEquality
Inferred forall a b. (a -> b) -> a -> b
$ forall a. a -> HasEta' a
NoEta PatternOrCopattern
patCopat) HasEta -> EtaEquality
Specified Maybe HasEta
eta
con :: ConHead
con = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
conName (PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
patCopat) Induction
conInduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom' Term QName]
fs
recordRelevance :: Relevance
recordRelevance
| Just NoEta{} <- Maybe HasEta
eta = Relevance
Relevant
| Induction
CoInductive <- Induction
conInduction = Relevance
Relevant
| Bool
otherwise = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall a b. (a -> b) -> a -> b
$ Relevance
Irrelevant forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. LensRelevance a => a -> Relevance
getRelevance (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
ftel)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Induction
conInduction forall a. Eq a => a -> a -> Bool
== Induction
CoInductive Bool -> Bool -> Bool
&& EtaEquality -> HasEta
theEtaEquality EtaEquality
haveEta forall a. Eq a => a -> a -> Bool
== forall a. HasEta' a
YesEta) forall a b. (a -> b) -> a -> b
$ do
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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Agda doesn't like coinductive records with eta-equality."
, TCMT IO Doc
"If you must, use pragma"
, TCMT IO Doc
"{-# ETA" 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 :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"#-}"
]
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"record constructor is " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
con
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Induction
conInduction forall a. Eq a => a -> a -> Bool
== Induction
CoInductive) forall a b. (a -> b) -> a -> b
$ do
Bool
guardedness <- forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optGuardedness forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
Bool
sizedTypes <- forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optSizedTypes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
guardedness Bool -> Bool -> Bool
|| Bool
sizedTypes) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ QName -> Warning
NoGuardednessFlag QName
name
let npars :: Nat
npars = forall a. Sized a => a -> Nat
size Telescope
tel
telh :: Telescope
telh = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams Telescope
tel
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 forall a b. (a -> b) -> a -> b
$
Record
{ recPars :: Nat
recPars = Nat
npars
, recClause :: Maybe Clause
recClause = forall a. Maybe a
Nothing
, recConHead :: ConHead
recConHead = ConHead
con
, recNamedCon :: Bool
recNamedCon = Bool
hasNamedCon
, recFields :: [Dom' Term QName]
recFields = [Dom' Term QName]
fs
, recTel :: Telescope
recTel = Telescope
telh forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ftel
, recAbstr :: IsAbstract
recAbstr = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
, recEtaEquality' :: EtaEquality
recEtaEquality' = EtaEquality
haveEta
, recPatternMatching :: PatternOrCopattern
recPatternMatching= PatternOrCopattern
patCopat
, recInduction :: Maybe Induction
recInduction = Maybe Induction
indCo
, recMutual :: Maybe [QName]
recMutual = forall a. Maybe a
Nothing
, recTerminates :: Maybe Bool
recTerminates = forall a. Maybe a
Nothing
, recComp :: CompKit
recComp = CompKit
emptyCompKit
}
QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
conName ArgInfo
defaultArgInfo QName
conName
(forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. LensQuantity a => Quantity -> a -> a
applyQuantity Quantity
zeroQuantity) Telescope
telh
forall t. Abstract t => Telescope -> t -> t
`abstract` Type
contype) forall a b. (a -> b) -> a -> b
$
Constructor
{ conPars :: Nat
conPars = Nat
npars
, conArity :: Nat
conArity = forall a. Sized a => a -> Nat
size [Dom' Term QName]
fs
, conSrcCon :: ConHead
conSrcCon = ConHead
con
, conData :: QName
conData = QName
name
, conAbstr :: IsAbstract
conAbstr = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
, conInd :: Induction
conInd = Induction
conInduction
, conComp :: CompKit
conComp = CompKit
emptyCompKit
, conProj :: Maybe [QName]
conProj = forall a. Maybe a
Nothing
, conForced :: [IsForced]
conForced = []
, 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 Range
r forall a b. (a -> b) -> a -> b
$ do
QName -> Type -> TCM ()
addTypedInstance QName
conName Type
contype
IsInstance
NotInstanceDef -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Nat
_ <- UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Nat
fitsIn UniverseCheck
uc [] Type
contype Sort
s
QName -> Sort -> TCM ()
checkDataSort QName
name Sort
s
let info :: ArgInfo
info = forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
recordRelevance ArgInfo
defaultArgInfo
addRecordVar :: TCM () -> TCM ()
addRecordVar =
forall (m :: * -> *) b.
(MonadAddContext m, MonadFresh NameId m) =>
Dom Type -> m b -> m b
addRecordNameContext (forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom Type
rect)
let m :: ModuleName
m = QName -> ModuleName
qnameToMName QName
name
Bool
eraseRecordParameters <- PragmaOptions -> Bool
optEraseRecordParameters forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
let maybeErase :: forall a. LensQuantity a => a -> a
maybeErase :: forall a. LensQuantity a => a -> a
maybeErase | Bool
eraseRecordParameters = forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
zeroQuantity
| Bool
otherwise = forall a. a -> a
id
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo (forall a. LensHiding a => a -> a
hideOrKeepInstance forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensQuantity a => a -> a
maybeErase) forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
addRecordVar forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.def" 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
"record section:"
, 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 ModuleName
m forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
, forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
P.pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
. Field -> [Dom' Term QName]
getName) [Field]
fields
]
]
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.def" Nat
15 forall a b. (a -> b) -> a -> b
$ 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
"field tel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
1 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ftel)
]
ModuleName -> TCM ()
addSection ModuleName
m
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo (forall a. LensHiding a => a -> a
hideOrKeepInstance forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensQuantity a => a -> a
maybeErase) forall a b. (a -> b) -> a -> b
$ do
[ContextEntry]
params <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. LensQuantity a => Quantity -> a -> a
applyQuantity Quantity
zeroQuantity) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext
TCM () -> TCM ()
addRecordVar forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule ModuleName
m forall a b. (a -> b) -> a -> b
$ do
Telescope
tel' <- do
ContextEntry
r <- forall a. a -> [a] -> a
headWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> [Char]) -> ListTel' a -> Telescope
telFromList' Name -> [Char]
nameToArgName forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ ContextEntry
r forall a. a -> [a] -> [a]
: [ContextEntry]
params
ModuleName -> TCM ()
setModuleCheckpoint ModuleName
m
ModuleName
-> QName
-> Bool
-> ConHead
-> Telescope
-> Telescope
-> [Field]
-> TCM ()
checkRecordProjections ModuleName
m QName
name Bool
hasNamedCon ConHead
con Telescope
tel' Telescope
ftel [Field]
fields
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
-> ConHead
-> Telescope
-> [Arg QName]
-> Telescope
-> Type
-> TCM ()
addCompositionForRecord QName
name ConHead
con Telescope
tel (forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom' Term QName]
fs) Telescope
ftel Type
rect
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
conName forall a b. (a -> b) -> a -> b
$ \Definition
def ->
Definition
def { defMatchable :: Set QName
defMatchable = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom [Dom' Term QName]
fs }
where
patCopat :: PatternOrCopattern
patCopat = forall b a. b -> (a -> b) -> Maybe a -> b
maybe PatternOrCopattern
CopatternMatching (forall a b. a -> b -> a
const PatternOrCopattern
PatternMatching) Maybe Range
pat
eta :: Maybe HasEta
eta = (PatternOrCopattern
patCopat forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe HasEta0
eta0
addCompositionForRecord
:: QName
-> ConHead
-> Telescope
-> [Arg QName]
-> Telescope
-> Type
-> TCM ()
addCompositionForRecord :: QName
-> ConHead
-> Telescope
-> [Arg QName]
-> Telescope
-> Type
-> TCM ()
addCompositionForRecord QName
name ConHead
con Telescope
tel [Arg QName]
fs Telescope
ftel Type
rect = do
Telescope
cxt <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
if forall a. Null a => a -> Bool
null [Arg QName]
fs then do
CompKit
kit <- QName
-> ConHead
-> Telescope
-> [QName]
-> Telescope
-> Type
-> Boundary
-> TCM CompKit
defineCompData QName
name ConHead
con (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
cxt Telescope
tel) [] Telescope
ftel Type
rect []
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition (ConHead -> QName
conName ConHead
con) forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
r :: Defn
r@Constructor{} -> Defn
r { conComp :: CompKit
conComp = CompKit
kit, conProj :: Maybe [QName]
conProj = forall a. a -> Maybe a
Just [] }
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
else do
CompKit
kit <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. LensRelevance a => a -> Bool
isIrrelevant [Arg QName]
fs)
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` do Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optIrrelevantProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(forall (m :: * -> *) a. Monad m => a -> m a
return CompKit
emptyCompKit)
(QName
-> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
defineCompKitR QName
name (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
cxt Telescope
tel) Telescope
ftel [Arg QName]
fs Type
rect)
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
name forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
r :: Defn
r@Record{} -> Defn
r { recComp :: CompKit
recComp = CompKit
kit }
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
defineCompKitR ::
QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM CompKit
defineCompKitR :: QName
-> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
defineCompKitR QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect = 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 => [Char] -> m (Maybe Term)
getTerm'
[ [Char]
builtinInterval
, [Char]
builtinIZero
, [Char]
builtinIOne
, [Char]
builtinIMin
, [Char]
builtinIMax
, [Char]
builtinINeg
, [Char]
builtinPOr
, [Char]
builtinItIsOne
]
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.cxt" Nat
30 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
params
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.cxt" Nat
30 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
fsT
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.cxt" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
rect
if Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ 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
transp <- forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
t [Char] -> m (Maybe a) -> m (Maybe a)
whenDefined [[Char]
builtinTrans] (Command
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe QName)
defineKanOperationR Command
DoTransp QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect)
Maybe QName
hcomp <- forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
t [Char] -> m (Maybe a) -> m (Maybe a)
whenDefined [[Char]
builtinTrans,[Char]
builtinHComp] (Command
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe QName)
defineKanOperationR Command
DoHComp QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect)
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
whenDefined :: t [Char] -> m (Maybe a) -> m (Maybe a)
whenDefined t [Char]
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 => [Char] -> m (Maybe Term)
getTerm' t [Char]
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
defineKanOperationR
:: Command
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe QName)
defineKanOperationR :: Command
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe QName)
defineKanOperationR Command
cmd QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect = do
let project :: Term -> QName -> Term
project = (\ Term
t QName
fn -> Term
t forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fn])
Maybe (QName, Telescope, Type, [Dom Type], [Term])
stuff <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Command
-> Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM
(Maybe
((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
defineKanOperationForFields Command
cmd forall a. Maybe a
Nothing Term -> QName -> Term
project QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (QName, Telescope, Type, [Dom Type], [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, Telescope
gamma, Type
rtype, [Dom Type]
clause_types, [Term]
bodies) -> do
Clause
c' <- do
Term
io <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
Just QName
io_name <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinIOne
Term
one <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
Type
tInterval <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
let
(Nat
ix,Term
rhs) =
case Command
cmd of
Command
DoTransp -> (Nat
1,Nat -> Elims -> Term
Var Nat
0 [])
Command
DoHComp -> (Nat
2,Nat -> Elims -> Term
Var Nat
1 [] forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
io, forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN Term
one])
p :: Pattern' DBPatVar
p = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
io_name DataOrRecord
IsData Induction
Inductive [])
(ConPatternInfo
noConPatternInfo { conPType :: Maybe (Arg Type)
conPType = forall a. a -> Maybe a
Just (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo Type
tInterval)
, conPFallThrough :: Bool
conPFallThrough = Bool
True })
[]
s :: Substitution' (Pattern' DBPatVar)
s = forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
ix Pattern' DBPatVar
p
pats :: [NamedArg DeBruijnPattern]
pats :: [NamedArg (Pattern' DBPatVar)]
pats = Substitution' (Pattern' DBPatVar)
s forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
gamma
t :: Type
t :: Type
t = Substitution' (Pattern' DBPatVar)
s forall a.
TermSubst a =>
Substitution' (Pattern' DBPatVar) -> a -> a
`applyPatSubst` Type
rtype
gamma' :: Telescope
gamma' :: Telescope
gamma' = [[Char]] -> [Dom Type] -> Telescope
unflattenTel ([[Char]]
ns0 forall a. [a] -> [a] -> [a]
++ [[Char]]
ns1) forall a b. (a -> b) -> a -> b
$ Substitution' (Pattern' DBPatVar)
s forall a.
TermSubst a =>
Substitution' (Pattern' DBPatVar) -> a -> a
`applyPatSubst` ([Dom Type]
g0 forall a. [a] -> [a] -> [a]
++ [Dom Type]
g1)
where
([Dom Type]
g0,Dom Type
_:[Dom Type]
g1) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Nat
size Telescope
gamma forall a. Num a => a -> a -> a
- Nat
1 forall a. Num a => a -> a -> a
- Nat
ix) forall a b. (a -> b) -> a -> b
$ forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
gamma
([[Char]]
ns0,[Char]
_:[[Char]]
ns1) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Nat
size Telescope
gamma forall a. Num a => a -> a -> a
- Nat
1 forall a. Num a => a -> a -> a
- Nat
ix) forall a b. (a -> b) -> a -> b
$ Telescope -> [[Char]]
teleNames Telescope
gamma
c :: Clause
c = Clause { clauseFullRange :: Range
clauseFullRange = forall a. Range' a
noRange
, clauseLHSRange :: Range
clauseLHSRange = forall a. Range' a
noRange
, clauseTel :: Telescope
clauseTel = Telescope
gamma'
, namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
, clauseBody :: Maybe Term
clauseBody = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term
rhs
, clauseType :: Maybe (Arg Type)
clauseType = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN Type
t
, clauseCatchall :: Bool
clauseCatchall = Bool
False
, clauseExact :: Maybe Bool
clauseExact = forall a. a -> Maybe a
Just Bool
True
, clauseRecursive :: Maybe Bool
clauseRecursive = forall a. a -> Maybe a
Just Bool
False
, clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
}
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec.face" Nat
17 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Clause
c
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c
[Clause]
cs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Arg QName]
fns [Dom Type]
clause_types [Term]
bodies) forall a b. (a -> b) -> a -> b
$ \ (Arg QName
fname, Dom Type
clause_ty, Term
body) -> do
let
pats :: [NamedArg (Pattern' DBPatVar)]
pats = forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
gamma forall a. [a] -> [a] -> [a]
++ [forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
ProjSystem forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg QName
fname]
c :: Clause
c = Clause { clauseFullRange :: Range
clauseFullRange = forall a. Range' a
noRange
, clauseLHSRange :: Range
clauseLHSRange = forall a. Range' a
noRange
, clauseTel :: Telescope
clauseTel = Telescope
gamma
, namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
, clauseBody :: Maybe Term
clauseBody = forall a. a -> Maybe a
Just Term
body
, 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 t e. Dom' t e -> e
unDom Dom Type
clause_ty)
, clauseCatchall :: Bool
clauseCatchall = Bool
False
, 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
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
}
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
17 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Clause
c
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
16 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"type =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show (Clause -> Maybe (Arg Type)
clauseType Clause
c))
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma (forall t e. Dom' t e -> e
unDom Dom Type
clause_ty)
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"body =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma Term
body)
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c
forall (m :: * -> *).
(MonadConstraint m, MonadTCState m) =>
QName -> [Clause] -> m ()
addClauses QName
theName forall a b. (a -> b) -> a -> b
$ Clause
c' forall a. a -> [a] -> [a]
: [Clause]
cs
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"compiling clauses for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show QName
theName
(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
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"compiled"
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
theName
checkRecordProjections ::
ModuleName -> QName -> Bool -> ConHead -> Telescope -> Telescope ->
[A.Declaration] -> TCM ()
checkRecordProjections :: ModuleName
-> QName
-> Bool
-> ConHead
-> Telescope
-> Telescope
-> [Field]
-> TCM ()
checkRecordProjections ModuleName
m QName
r Bool
hasNamedCon ConHead
con Telescope
tel Telescope
ftel [Field]
fs = do
Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs forall a. Tele a
EmptyTel Telescope
ftel [] [Field]
fs
where
checkProjs :: Telescope -> Telescope -> [Term] -> [A.Declaration] -> TCM ()
checkProjs :: Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs Telescope
_ Telescope
_ [Term]
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs (A.ScopedDecl ScopeInfo
scope [Field]
fs' : [Field]
fs) =
ScopeInfo -> TCM ()
setScope ScopeInfo
scope forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs ([Field]
fs' forall a. [a] -> [a] -> [a]
++ [Field]
fs)
checkProjs Telescope
ftel1 (ExtendTel (dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai,unDom :: forall t e. Dom' t e -> e
unDom = Type
t}) Abs Telescope
ftel2) [Term]
vs (A.Field DefInfo
info QName
x Arg Expr
_ : [Field]
fs) =
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> Type -> Call
CheckProjection (forall a. HasRange a => a -> Range
getRange DefInfo
info) QName
x Type
t) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"checking projection" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x
, 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
"top =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
, TCMT IO Doc
"tel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Telescope
tel)
]
]
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
5 forall a b. (a -> b) -> a -> b
$ 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
"ftel1 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
1 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ftel1)
, TCMT IO Doc
"t =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
1 (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ftel1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t)
, TCMT IO Doc
"ftel2 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
1 (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ftel1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Telescope
ftel2 forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM)
]
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
55 forall a b. (a -> b) -> a -> b
$ 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
"ftel1 (raw) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
ftel1
, TCMT IO Doc
"t (raw) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
, TCMT IO Doc
"ftel2 (raw) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Abs Telescope
ftel2
]
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
5 forall a b. (a -> b) -> a -> b
$ 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
"vs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs)
, TCMT IO Doc
"abstr =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) (forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
info)
, TCMT IO Doc
"quant =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) (forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai)
, TCMT IO Doc
"coh =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)
]
if forall a. LeftClosedPOMonoid a => a -> Bool
hasLeftAdjoint (forall t. t -> UnderComposition t
UnderComposition (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai))
then forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai forall a. Eq a => a -> a -> Bool
== Cohesion
Continuous)
forall a. HasCallStack => a
__IMPOSSIBLE__
else forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot have record fields with modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)
let t' :: Type
t' = forall a. Subst a => Nat -> Nat -> a -> a
raiseFrom (forall a. Sized a => a -> Nat
size Telescope
ftel1) Nat
1 Type
t
t'' :: Type
t'' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Term]
vs) Type
t'
finalt :: Type
finalt = Telescope -> Type -> Type
telePi (forall a. [Char] -> Tele a -> Tele a
replaceEmptyName [Char]
"r" Telescope
tel) Type
t''
projname :: QName
projname = ModuleName -> Name -> QName
qualify ModuleName
m forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
projcall :: ProjOrigin -> Term
projcall ProjOrigin
o = Nat -> Elims -> Term
Var Nat
0 [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
projname]
rel :: Relevance
rel = forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai
recurse :: TCM ()
recurse = Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
ftel1 forall a b. (a -> b) -> a -> b
$ forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
dom
forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
Abs (Name -> [Char]
nameToArgName forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
projname) forall a. Tele a
EmptyTel)
(forall a. Subst a => Abs a -> a
absBody Abs Telescope
ftel2) (ProjOrigin -> Term
projcall ProjOrigin
ProjSystem forall a. a -> [a] -> [a]
: [Term]
vs) [Field]
fs
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
25 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"finalt=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
finalt
do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" 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
"adding projection"
, 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 QName
projname forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
finalt)
]
let bodyMod :: Term -> Term
bodyMod = case Relevance
rel of
Relevance
Relevant -> forall a. a -> a
id
Relevance
NonStrict -> forall a. a -> a
id
Relevance
Irrelevant -> Term -> Term
dontCare
let
telList :: [Dom ([Char], Type)]
telList = forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel
([Dom ([Char], Type)]
ptelList,[Dom ([Char], Type)
rt]) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Nat
size Telescope
tel forall a. Num a => a -> a -> a
- Nat
1) [Dom ([Char], Type)]
telList
ptel :: Telescope
ptel = [Dom ([Char], Type)] -> Telescope
telFromList [Dom ([Char], Type)]
ptelList
cpo :: PatOrigin
cpo = if Bool
hasNamedCon then PatOrigin
PatOCon else PatOrigin
PatORec
cpi :: ConPatternInfo
cpi = ConPatternInfo { conPInfo :: PatternInfo
conPInfo = PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
cpo []
, conPRecord :: Bool
conPRecord = Bool
True
, conPFallThrough :: Bool
conPFallThrough = Bool
False
, conPType :: Maybe (Arg Type)
conPType = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t a. Dom' t a -> Arg a
argFromDom 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 Dom ([Char], Type)
rt
, conPLazy :: Bool
conPLazy = Bool
True }
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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
ftel
body :: Maybe Term
body = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term -> Term
bodyMod forall a b. (a -> b) -> a -> b
$ Nat -> Term
var (forall a. Sized a => a -> Nat
size Abs Telescope
ftel2)
cltel :: Telescope
cltel = Telescope
ptel forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ftel
cltype :: Maybe (Arg Type)
cltype = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise (Nat
1 forall a. Num a => a -> a -> a
+ forall a. Sized a => a -> Nat
size Abs Telescope
ftel2) Type
t
clause :: Clause
clause = Clause { clauseLHSRange :: Range
clauseLHSRange = forall a. HasRange a => a -> Range
getRange DefInfo
info
, clauseFullRange :: Range
clauseFullRange = forall a. HasRange a => a -> Range
getRange DefInfo
info
, clauseTel :: Telescope
clauseTel = forall a. KillRange a => KillRangeT a
killRange Telescope
cltel
, namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)
conp]
, clauseBody :: Maybe Term
clauseBody = Maybe Term
body
, clauseType :: Maybe (Arg Type)
clauseType = Maybe (Arg Type)
cltype
, clauseCatchall :: Bool
clauseCatchall = Bool
False
, clauseExact :: Maybe Bool
clauseExact = forall a. a -> Maybe a
Just Bool
True
, clauseRecursive :: Maybe Bool
clauseRecursive = forall a. a -> Maybe a
Just Bool
False
, clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
}
let projection :: Projection
projection = Projection
{ projProper :: Maybe QName
projProper = forall a. a -> Maybe a
Just QName
r
, projOrig :: QName
projOrig = QName
projname
, projFromType :: Arg QName
projFromType = forall e. e -> Arg e
defaultArg QName
r
, projIndex :: Nat
projIndex = forall a. Sized a => a -> Nat
size Telescope
tel
, projLams :: ProjLams
projLams = [Arg [Char]] -> 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) [Dom ([Char], Type)]
telList
}
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
70 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"adding projection"
, 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 QName
projname forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Clause
clause
]
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" 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
"adding projection"
, 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 (forall a. QName -> a -> QNamed a
QNamed QName
projname Clause
clause)
]
(Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses forall a. Maybe a
Nothing [Clause
clause]
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc" Nat
60 forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"compiled clauses of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
projname
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show CompiledClauses
cc)
]
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible (forall a. Sized a => a -> Nat
size Telescope
tel) forall a b. (a -> b) -> a -> b
$ do
Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
QName -> Definition -> TCM ()
addConstant QName
projname forall a b. (a -> b) -> a -> b
$
(ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
ai QName
projname (forall a. KillRange a => KillRangeT a
killRange Type
finalt) Language
lang forall a b. (a -> b) -> a -> b
$ FunctionData -> Defn
FunctionDefn
FunctionData
emptyFunctionData
{ _funClauses :: [Clause]
_funClauses = [Clause
clause]
, _funCompiled :: Maybe CompiledClauses
_funCompiled = forall a. a -> Maybe a
Just CompiledClauses
cc
, _funSplitTree :: Maybe SplitTree
_funSplitTree = Maybe SplitTree
mst
, _funProjection :: Either ProjectionLikenessMissing Projection
_funProjection = forall a b. b -> Either a b
Right Projection
projection
, _funMutual :: Maybe [QName]
_funMutual = forall a. a -> Maybe a
Just []
, _funTerminates :: Maybe Bool
_funTerminates = forall a. a -> Maybe a
Just Bool
True
})
{ defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
StrictPos]
, defCopatternLHS :: Bool
defCopatternLHS = CompiledClauses -> Bool
hasProjectionPatterns CompiledClauses
cc
}
forall (m :: * -> *).
(HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m,
MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m,
MonadDebug m, MonadPretty m) =>
[QName] -> m ()
computePolarity [QName
projname]
case forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
info of
InstanceDef Range
_r -> QName -> Type -> TCM ()
addTypedInstance QName
projname Type
t
IsInstance
NotInstanceDef -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
TCM ()
recurse
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs (Field
d : [Field]
fs) = do
Field -> TCM ()
checkDecl Field
d
Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs [Field]
fs