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.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.Substitute
import Agda.TypeChecking.Rules.Builtin
import Agda.TypeChecking.Rules.Term
import Agda.Utils.Permutation
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
, dataSmallPars = Perm 2 []
, dataNonLinPars = Drop 0 $ Perm 2 []
, dataIxs = 0
, dataInduction = CoInductive
, dataClause = Nothing
, dataCons = [sharp]
, dataSort = varSort 1
, dataMutual = []
, dataAbstr = ConcreteDef
}
}
addConstant sharp $
sharpDefn { theDef = Constructor
{ conPars = 2
, conSrcCon = ConHead 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 sharpCon = ConHead sharp [flat]
level = El (mkType 0) $ Def (typeName kit) []
tel :: Telescope
tel = ExtendTel (domH $ level) $ Abs "a" $
ExtendTel (domH $ sort $ varSort 0) $ Abs "A" $
ExtendTel (domN $ El (varSort 1) $ var 0) $ Abs "x" $
EmptyTel
let clause = Clause
{ clauseRange = noRange
, clauseTel = tel
, clausePerm = idP 1
, namedClausePats = [ argN $ Named Nothing $ ConP sharpCon Nothing [ argN $ Named Nothing $ VarP "x" ] ]
, clauseBody = Bind $ Abs "x" $ Body $ var 0
, clauseType = Just $ defaultArg $ El (varSort 2) $ var 1
}
cc = Case 0 $ Branches (Map.singleton sharp
$ WithArity 1 $ Done [defaultArg "x"] $ var 0)
Map.empty
Nothing
projection = Projection
{ projProper = Nothing
, projFromType = inf
, projIndex = 3
, projDropPars = teleNoAbs (take 2 $ telToList tel) $ Def flat []
, projArgInfo = defaultArgInfo
}
addConstant flat $
flatDefn { defPolarity = []
, defArgOccurrences = [StrictPos]
, theDef = Function
{ funClauses = [clause]
, funCompiled = Just $ cc
, funInv = NotInjective
, funMutual = []
, funAbstr = ConcreteDef
, funDelayed = NotDelayed
, funProjection = Just projection
, funStatic = False
, funCopy = False
, funTerminates = Just True
, funExtLam = Nothing
, funWith = Nothing
}
}
modifySignature $ updateDefinition sharp $ updateTheDef $ \ def ->
def { conSrcCon = sharpCon }
return flatE