module Agda.TypeChecking.Rules.Builtin.Coinduction where
import Control.Applicative
import qualified Data.Map as Map
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.Builtin
import Agda.TypeChecking.Rules.Term
import Agda.Utils.Impossible
import Agda.Utils.Permutation
#include "../../../undefined.h"
typeOfInf :: TCM Type
typeOfInf = hPi "a" (el primLevel) $
(return . sort $ varSort 0) --> (return . sort $ varSort 0)
typeOfSharp :: TCM Type
typeOfSharp = hPi "a" (el primLevel) $
hPi "A" (return . sort $ varSort 0) $
(El (varSort 1) <$> varM 0) -->
(El (varSort 1) <$> primInf <#> varM 1 <@> varM 0)
typeOfFlat :: TCM Type
typeOfFlat = hPi "a" (el primLevel) $
hPi "A" (return . sort $ varSort 0) $
(El (varSort 1) <$> primInf <#> varM 1 <@> varM 0) -->
(El (varSort 1) <$> varM 0)
bindBuiltinInf :: A.Expr -> TCM ()
bindBuiltinInf e = bindPostulatedName builtinInf e $ \inf _ ->
instantiateFull =<< checkExpr (A.Def inf) =<< typeOfInf
bindBuiltinSharp :: A.Expr -> TCM ()
bindBuiltinSharp e =
bindPostulatedName builtinSharp e $ \sharp sharpDefn -> do
sharpE <- instantiateFull =<< checkExpr (A.Def sharp) =<< typeOfSharp
Def inf _ <- ignoreSharing <$> primInf
infDefn <- getConstInfo inf
addConstant (defName infDefn) $
infDefn { defPolarity = []
, defArgOccurrences = [Unused, StrictPos]
, theDef = Datatype
{ dataPars = 2
, dataIxs = 0
, dataInduction = CoInductive
, dataClause = Nothing
, dataCons = [sharp]
, dataSort = varSort 1
, dataMutual = []
, dataAbstr = ConcreteDef
}
}
addConstant sharp $
sharpDefn { theDef = Constructor
{ conPars = 2
, conSrcCon = sharp
, conData = defName infDefn
, conAbstr = ConcreteDef
, conInd = CoInductive
}
}
return sharpE
bindBuiltinFlat :: A.Expr -> TCM ()
bindBuiltinFlat e =
bindPostulatedName builtinFlat e $ \flat flatDefn -> do
flatE <- instantiateFull =<< checkExpr (A.Def flat) =<< typeOfFlat
Def sharp _ <- ignoreSharing <$> primSharp
kit <- requireLevels
Def inf _ <- ignoreSharing <$> primInf
let clause = Clause { clauseRange = noRange
, clauseTel = ExtendTel (domH (El (mkType 0) (Def (typeName kit) [])))
(Abs "a" (ExtendTel (domH $ sort $ varSort 0)
(Abs "A" (ExtendTel (domN (El (varSort 1) (var 0)))
(Abs "x" EmptyTel)))))
, clausePerm = idP 1
, clausePats = [ argN (ConP sharp Nothing [argN (VarP "x")])
]
, clauseBody = Bind $ Abs "x" $ Body (var 0)
}
addConstant flat $
flatDefn { defPolarity = []
, defArgOccurrences = [StrictPos]
, theDef = Function
{ funClauses = [clause]
, funCompiled =
let hid = Arg Hidden Relevant
nohid = defaultArg in
Case 0 (Branches (Map.singleton sharp
(WithArity 1 (Done [nohid "x"] (var 0))))
Map.empty
Nothing)
, funInv = NotInjective
, funMutual = []
, funAbstr = ConcreteDef
, funDelayed = NotDelayed
, funProjection = Just (inf, 3)
, funStatic = False
, funCopy = False
, funTerminates = Just True
}
}
return flatE