------------------------------------------------------------------------
-- | Handling of the INFINITY, SHARP and FLAT builtins.
------------------------------------------------------------------------

module Agda.TypeChecking.Rules.Builtin.Coinduction where

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.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.Builtin
import Agda.TypeChecking.Rules.Term

import Agda.Utils.Lens

-- | The type of @∞@.

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)

-- | The type of @♯_@.

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)

-- | The type of @♭@.

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)

-- | Binds the INFINITY builtin, but does not change the type's
-- definition.

bindBuiltinInf :: ResolvedName -> TCM ()
bindBuiltinInf :: ResolvedName -> TCM ()
bindBuiltinInf ResolvedName
x = ArgName
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName ArgName
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 []

-- | Binds the SHARP builtin, and changes the definitions of INFINITY
-- and SHARP.

-- The following (no longer supported) definition is used:
--
-- codata ∞ {a} (A : Set a) : Set a where
--   ♯_ : (x : A) → ∞ A

bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinSharp ResolvedName
x =
  ArgName
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName ArgName
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
    QName -> Definition -> TCM ()
addConstant (Definition -> QName
defName Definition
infDefn) forall a b. (a -> b) -> a -> b
$
      Definition
infDefn { defPolarity :: [Polarity]
defPolarity       = [] -- not monotone
              , 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 []  -- flat is added later
                  , recNamedCon :: Bool
recNamedCon       = Bool
True
                  , recFields :: [Dom QName]
recFields         = []  -- flat is added later
                  , 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  -- not recursive
                  , 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 [] -- flat is added as field later
                    , conData :: QName
conData   = Definition -> QName
defName Definition
infDefn
                    , conAbstr :: IsAbstract
conAbstr  = IsAbstract
ConcreteDef
                    , conInd :: Induction
conInd    = Induction
CoInductive
                    , 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
                    }
                }
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
sharp []

-- | Binds the FLAT builtin, and changes its definition.

-- The following (no longer supported) definition is used:
--
--   ♭ : ∀ {a} {A : Set a} → ∞ A → A
--   ♭ (♯ x) = x

bindBuiltinFlat :: ResolvedName -> TCM ()
bindBuiltinFlat :: ResolvedName -> TCM ()
bindBuiltinFlat ResolvedName
x =
  ArgName
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName ArgName
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" ]
          }
    QName -> Definition -> TCM ()
addConstant QName
flat forall a b. (a -> b) -> a -> b
$
      Definition
flatDefn { defPolarity :: [Polarity]
defPolarity       = []
               , defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
StrictPos]  -- changing that to [Mixed] destroys monotonicity of 'Rec' in test/succeed/GuardednessPreservingTypeConstructors
               , defCopatternLHS :: Bool
defCopatternLHS = CompiledClauses' Term -> Bool
hasProjectionPatterns CompiledClauses' Term
cc
               , theDef :: Defn
theDef = FunctionData -> Defn
FunctionDefn FunctionData
emptyFunctionData
                   { _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
                   }
                }

    -- register flat as record field for constructor sharp
    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 i o. Lens' i o -> LensMap i o
over Lens' ConstructorData Defn
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 i o. Lens' i o -> LensMap i o
over Lens' RecordData Defn
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 []

-- The coinductive primitives.
-- moved to TypeChecking.Monad.Builtin