{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.TypeChecking.Rules.Builtin.Coinduction where
import Agda.Interaction.Options.Base
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.Builtin
import Agda.TypeChecking.Rules.Term
import Agda.Utils.Lens
typeOfInf :: TCM Type
typeOfInf :: TCM Type
typeOfInf = forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$
(forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0)
typeOfSharp :: TCM Type
typeOfSharp :: TCM Type
typeOfSharp = forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"A" (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) forall a b. (a -> b) -> a -> b
$
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0)
typeOfFlat :: TCM Type
typeOfFlat :: TCM Type
typeOfFlat = forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"A" (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) forall a b. (a -> b) -> a -> b
$
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0)
bindBuiltinInf :: ResolvedName -> TCM ()
bindBuiltinInf :: ResolvedName -> TCM ()
bindBuiltinInf ResolvedName
x = BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtinInf ResolvedName
x forall a b. (a -> b) -> a -> b
$ \QName
inf Definition
_ -> do
Term
_ <- Expr -> Type -> TCMT IO Term
checkExpr (QName -> Expr
A.Def QName
inf) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
typeOfInf
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
inf []
bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinSharp ResolvedName
x =
BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtinSharp ResolvedName
x forall a b. (a -> b) -> a -> b
$ \QName
sharp Definition
sharpDefn -> do
Type
sharpType <- TCM Type
typeOfSharp
TelV Tele (Dom Type)
fieldTel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
sharpType
Term
_ <- Expr -> Type -> TCMT IO Term
checkExpr (QName -> Expr
A.Def QName
sharp) Type
sharpType
Def QName
inf Elims
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf
Definition
infDefn <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
inf
Bool
erasure <- PragmaOptions -> Bool
optErasure forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
QName -> Definition -> TCM ()
addConstant (Definition -> QName
defName Definition
infDefn) forall a b. (a -> b) -> a -> b
$
Definition
infDefn { defPolarity :: [Polarity]
defPolarity = []
, defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
Unused, Occurrence
StrictPos]
, theDef :: Defn
theDef = Record
{ recPars :: Int
recPars = Int
2
, recInduction :: Maybe Induction
recInduction = forall a. a -> Maybe a
Just Induction
CoInductive
, recClause :: Maybe Clause
recClause = forall a. Maybe a
Nothing
, recConHead :: ConHead
recConHead = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
sharp (PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
CopatternMatching) Induction
CoInductive []
, recNamedCon :: Bool
recNamedCon = Bool
True
, recFields :: [Dom QName]
recFields = []
, recTel :: Tele (Dom Type)
recTel = Tele (Dom Type)
fieldTel
, recEtaEquality' :: EtaEquality
recEtaEquality' = HasEta -> EtaEquality
Inferred forall a b. (a -> b) -> a -> b
$ forall a. a -> HasEta' a
NoEta PatternOrCopattern
CopatternMatching
, recPatternMatching :: PatternOrCopattern
recPatternMatching= PatternOrCopattern
CopatternMatching
, recMutual :: Maybe [QName]
recMutual = forall a. a -> Maybe a
Just []
, recTerminates :: Maybe Bool
recTerminates = forall a. a -> Maybe a
Just Bool
True
, recAbstr :: IsAbstract
recAbstr = IsAbstract
ConcreteDef
, recComp :: CompKit
recComp = CompKit
emptyCompKit
}
}
QName -> Definition -> TCM ()
addConstant QName
sharp forall a b. (a -> b) -> a -> b
$
Definition
sharpDefn { theDef :: Defn
theDef = Constructor
{ conPars :: Int
conPars = Int
2
, conArity :: Int
conArity = Int
1
, conSrcCon :: ConHead
conSrcCon = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
sharp (PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
CopatternMatching) Induction
CoInductive []
, conData :: QName
conData = Definition -> QName
defName Definition
infDefn
, conAbstr :: IsAbstract
conAbstr = IsAbstract
ConcreteDef
, 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
, conErasure :: Bool
conErasure = Bool
erasure
, conInline :: Bool
conInline = Bool
True
}
}
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
sharp []
bindBuiltinFlat :: ResolvedName -> TCM ()
bindBuiltinFlat :: ResolvedName -> TCM ()
bindBuiltinFlat ResolvedName
x =
BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtinFlat ResolvedName
x forall a b. (a -> b) -> a -> b
$ \ QName
flat Definition
flatDefn -> do
Term
_ <- Expr -> Type -> TCMT IO Term
checkExpr (QName -> Expr
A.Def QName
flat) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
typeOfFlat
Def QName
sharp Elims
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSharp
LevelKit
kit <- forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m LevelKit
requireLevels
Def QName
inf Elims
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf
let sharpCon :: ConHead
sharpCon = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
sharp (PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
CopatternMatching) Induction
CoInductive [forall a. a -> Arg a
defaultArg QName
flat]
level :: Type
level = forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def (LevelKit -> QName
typeName LevelKit
kit) []
tel :: Telescope
tel :: Tele (Dom Type)
tel = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall e. e -> Dom e
domH forall a b. (a -> b) -> a -> b
$ Type
level) forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs ArgName
"a" forall a b. (a -> b) -> a -> b
$
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall e. e -> Dom e
domH forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs ArgName
"A" forall a b. (a -> b) -> a -> b
$
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall e. e -> Dom e
domN forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0) forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs ArgName
"x" forall a b. (a -> b) -> a -> b
$
forall a. Tele a
EmptyTel
infA :: Type
infA = forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
2) forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
inf [ forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
1 ]
cpi :: ConPatternInfo
cpi = ConPatternInfo
noConPatternInfo { conPType :: Maybe (Arg Type)
conPType = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Type
infA
, conPLazy :: Bool
conPLazy = Bool
True }
let clause :: Clause
clause = Clause
{ clauseLHSRange :: Range
clauseLHSRange = forall a. Range' a
noRange
, clauseFullRange :: Range
clauseFullRange = forall a. Range' a
noRange
, clauseTel :: Tele (Dom Type)
clauseTel = Tele (Dom Type)
tel
, namedClausePats :: NAPs
namedClausePats = [ forall a. a -> Arg a
argN forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
sharpCon ConPatternInfo
cpi [ forall a. a -> Arg a
argN forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => ArgName -> Int -> a
debruijnNamedVar ArgName
"x" Int
0 ] ]
, clauseBody :: Maybe Term
clauseBody = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
, clauseType :: Maybe (Arg Type)
clauseType = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
2) forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
1
, 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
}
cc :: CompiledClauses' Term
cc = forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (forall a. a -> Arg a
defaultArg Int
0) forall a b. (a -> b) -> a -> b
$ forall c. QName -> Bool -> WithArity c -> Case c
conCase QName
sharp Bool
False forall a b. (a -> b) -> a -> b
$ forall c. Int -> c -> WithArity c
WithArity Int
1 forall a b. (a -> b) -> a -> b
$ forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done [forall a. a -> Arg a
defaultArg ArgName
"x"] forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
projection :: Projection
projection = Projection
{ projProper :: Maybe QName
projProper = forall a. a -> Maybe a
Just QName
inf
, projOrig :: QName
projOrig = QName
flat
, projFromType :: Arg QName
projFromType = forall a. a -> Arg a
defaultArg QName
inf
, projIndex :: Int
projIndex = Int
3
, projLams :: ProjLams
projLams = [Arg ArgName] -> ProjLams
ProjLams forall a b. (a -> b) -> a -> b
$ [ forall a. a -> Arg a
argH ArgName
"a" , forall a. a -> Arg a
argH ArgName
"A" , forall a. a -> Arg a
argN ArgName
"x" ]
}
FunctionData
fun <- forall (m :: * -> *). HasOptions m => m FunctionData
emptyFunctionData
QName -> Definition -> TCM ()
addConstant QName
flat forall a b. (a -> b) -> a -> b
$
Definition
flatDefn { defPolarity :: [Polarity]
defPolarity = []
, defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
StrictPos]
, defCopatternLHS :: Bool
defCopatternLHS = CompiledClauses' Term -> Bool
hasProjectionPatterns CompiledClauses' Term
cc
, theDef :: Defn
theDef = FunctionData -> Defn
FunctionDefn FunctionData
fun
{ _funClauses :: [Clause]
_funClauses = [Clause
clause]
, _funCompiled :: Maybe (CompiledClauses' Term)
_funCompiled = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ CompiledClauses' Term
cc
, _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
}
}
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
sharp forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensMap o i
over Lens' Defn ConstructorData
lensConstructor forall a b. (a -> b) -> a -> b
$ \ ConstructorData
def ->
ConstructorData
def { _conSrcCon :: ConHead
_conSrcCon = ConHead
sharpCon }
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
inf forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensMap o i
over Lens' Defn RecordData
lensRecord forall a b. (a -> b) -> a -> b
$ \ RecordData
def ->
RecordData
def { _recConHead :: ConHead
_recConHead = ConHead
sharpCon, _recFields :: [Dom QName]
_recFields = [forall e. e -> Dom e
defaultDom QName
flat] }
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
flat []