{-# 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 = ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (TCMT IO Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
(Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort (Sort -> TCM Type) -> Sort -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort (Sort -> TCM Type) -> Sort -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0)
typeOfSharp :: TCM Type
typeOfSharp :: TCM Type
typeOfSharp = ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (TCMT IO Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"A" (Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort (Sort -> TCM Type) -> Sort -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
(Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
(Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0)
typeOfFlat :: TCM Type
typeOfFlat :: TCM Type
typeOfFlat = ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (TCMT IO Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"A" (Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort (Sort -> TCM Type) -> Sort -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
(Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
(Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Term
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 ((QName -> Definition -> TCMT IO Term) -> TCM ())
-> (QName -> Definition -> TCMT IO Term) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \QName
inf Definition
_ -> do
_ <- Expr -> Type -> TCMT IO Term
checkExpr (QName -> Expr
A.Def QName
inf) (Type -> TCMT IO Term) -> TCM Type -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
typeOfInf
return $ Def inf []
bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinSharp ResolvedName
x =
BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtinSharp ResolvedName
x ((QName -> Definition -> TCMT IO Term) -> TCM ())
-> (QName -> Definition -> TCMT IO Term) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \QName
sharp Definition
sharpDefn -> do
sharpType <- TCM Type
typeOfSharp
TelV fieldTel _ <- telView sharpType
_ <- checkExpr (A.Def sharp) sharpType
Def inf _ <- primInf
infDefn <- getConstInfo inf
erasure <- optErasure <$> pragmaOptions
addConstant (defName infDefn) $
infDefn { defPolarity = []
, defArgOccurrences = [Unused, StrictPos]
, theDef = Record
{ recPars = 2
, recInduction = Just CoInductive
, recClause = Nothing
, recConHead = ConHead sharp (IsRecord CopatternMatching) CoInductive []
, recNamedCon = True
, recFields = []
, recTel = fieldTel
, recEtaEquality' = Inferred $ NoEta CopatternMatching
, recPatternMatching= CopatternMatching
, recMutual = Just []
, recTerminates = Just True
, recAbstr = ConcreteDef
, recComp = emptyCompKit
}
}
addConstant sharp $
sharpDefn { theDef = Constructor
{ conPars = 2
, conArity = 1
, conSrcCon = ConHead sharp (IsRecord CopatternMatching) CoInductive []
, conData = defName infDefn
, conAbstr = ConcreteDef
, conComp = emptyCompKit
, conProj = Nothing
, conForced = []
, conErased = Nothing
, conErasure = erasure
, conInline = True
}
}
return $ Def sharp []
bindBuiltinFlat :: ResolvedName -> TCM ()
bindBuiltinFlat :: ResolvedName -> TCM ()
bindBuiltinFlat ResolvedName
x =
BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtinFlat ResolvedName
x ((QName -> Definition -> TCMT IO Term) -> TCM ())
-> (QName -> Definition -> TCMT IO Term) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
flat Definition
flatDefn -> do
_ <- Expr -> Type -> TCMT IO Term
checkExpr (QName -> Expr
A.Def QName
flat) (Type -> TCMT IO Term) -> TCM Type -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
typeOfFlat
Def sharp _ <- primSharp
kit <- requireLevels
Def inf _ <- primInf
let sharpCon = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
sharp (PatternOrCopattern -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
CopatternMatching) Induction
CoInductive [QName -> Arg QName
forall a. a -> Arg a
defaultArg QName
flat]
level = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def (LevelKit -> QName
typeName LevelKit
kit) []
tel :: Telescope
tel = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall e. e -> Dom e
domH (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Type
level) (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
"a" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$
Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall e. e -> Dom e
domH (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
"A" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$
Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall e. e -> Dom e
domN (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0) (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
"x" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$
Tele (Dom Type)
forall a. Tele a
EmptyTel
infA = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
2) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
inf [ Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
1 ]
cpi = ConPatternInfo
noConPatternInfo { conPType = Just $ defaultArg infA
, conPLazy = True }
let clause = Clause
{ clauseLHSRange :: Range
clauseLHSRange = Range
forall a. Range' a
noRange
, clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
, clauseTel :: Tele (Dom Type)
clauseTel = Tele (Dom Type)
tel
, namedClausePats :: NAPs
namedClausePats = [ Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
forall a. a -> Arg a
argN (Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar)))
-> Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
forall a b. (a -> b) -> a -> b
$ Maybe NamedName -> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
forall a. Maybe a
Nothing (Pattern' DBPatVar -> Named_ (Pattern' DBPatVar))
-> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$
ConHead -> ConPatternInfo -> NAPs -> Pattern' DBPatVar
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
sharpCon ConPatternInfo
cpi [ Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
forall a. a -> Arg a
argN (Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar)))
-> Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
forall a b. (a -> b) -> a -> b
$ Maybe NamedName -> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
forall a. Maybe a
Nothing (Pattern' DBPatVar -> Named_ (Pattern' DBPatVar))
-> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ ArgName -> Int -> Pattern' DBPatVar
forall a. DeBruijn a => ArgName -> Int -> a
debruijnNamedVar ArgName
"x" Int
0 ] ]
, clauseBody :: Maybe Term
clauseBody = Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
, clauseType :: Maybe (Arg Type)
clauseType = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Type -> Arg Type
forall a. a -> Arg a
defaultArg (Type -> Arg Type) -> Type -> Arg Type
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
2) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
1
, clauseCatchall :: Bool
clauseCatchall = Bool
False
, clauseExact :: Maybe Bool
clauseExact = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
, clauseRecursive :: Maybe Bool
clauseRecursive = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
, clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
}
cc = Arg Int -> Case (CompiledClauses' Term) -> CompiledClauses' Term
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (Int -> Arg Int
forall a. a -> Arg a
defaultArg Int
0) (Case (CompiledClauses' Term) -> CompiledClauses' Term)
-> Case (CompiledClauses' Term) -> CompiledClauses' Term
forall a b. (a -> b) -> a -> b
$ QName
-> Bool
-> WithArity (CompiledClauses' Term)
-> Case (CompiledClauses' Term)
forall c. QName -> Bool -> WithArity c -> Case c
conCase QName
sharp Bool
False (WithArity (CompiledClauses' Term) -> Case (CompiledClauses' Term))
-> WithArity (CompiledClauses' Term)
-> Case (CompiledClauses' Term)
forall a b. (a -> b) -> a -> b
$ Int -> CompiledClauses' Term -> WithArity (CompiledClauses' Term)
forall c. Int -> c -> WithArity c
WithArity Int
1 (CompiledClauses' Term -> WithArity (CompiledClauses' Term))
-> CompiledClauses' Term -> WithArity (CompiledClauses' Term)
forall a b. (a -> b) -> a -> b
$ [Arg ArgName] -> Term -> CompiledClauses' Term
forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done [ArgName -> Arg ArgName
forall a. a -> Arg a
defaultArg ArgName
"x"] (Term -> CompiledClauses' Term) -> Term -> CompiledClauses' Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
projection = Projection
{ projProper :: Maybe QName
projProper = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
inf
, projOrig :: QName
projOrig = QName
flat
, projFromType :: Arg QName
projFromType = QName -> Arg QName
forall a. a -> Arg a
defaultArg QName
inf
, projIndex :: Int
projIndex = Int
3
, projLams :: ProjLams
projLams = [Arg ArgName] -> ProjLams
ProjLams ([Arg ArgName] -> ProjLams) -> [Arg ArgName] -> ProjLams
forall a b. (a -> b) -> a -> b
$ [ ArgName -> Arg ArgName
forall a. a -> Arg a
argH ArgName
"a" , ArgName -> Arg ArgName
forall a. a -> Arg a
argH ArgName
"A" , ArgName -> Arg ArgName
forall a. a -> Arg a
argN ArgName
"x" ]
}
fun <- emptyFunctionData
addConstant flat $
flatDefn { defPolarity = []
, defArgOccurrences = [StrictPos]
, defCopatternLHS = hasProjectionPatterns cc
, theDef = FunctionDefn fun
{ _funClauses = [clause]
, _funCompiled = Just $ cc
, _funProjection = Right projection
, _funMutual = Just []
, _funTerminates = Just True
}
}
modifySignature $ updateDefinition sharp $ updateTheDef $ over lensConstructor $ \ ConstructorData
def ->
ConstructorData
def { _conSrcCon = sharpCon }
modifySignature $ updateDefinition inf $ updateTheDef $ over lensRecord $ \ RecordData
def ->
RecordData
def { _recConHead = sharpCon, _recFields = [defaultDom flat] }
return $ Def flat []