module Agda.TypeChecking.Rules.Builtin.Coinduction where
import Control.Applicative
import Control.Monad.Error
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) <$> var 0) -->
(El (varSort 1) <$> primInf <#> var 1 <@> var 0)
typeOfFlat :: TCM Type
typeOfFlat = hPi "a" (el primLevel) $
hPi "A" (return . sort $ varSort 0) $
(El (varSort 1) <$> primInf <#> var 1 <@> var 0) -->
(El (varSort 1) <$> var 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
inf <- primInf
infDefn <- case inf of
Def inf _ -> getConstInfo inf
_ -> __IMPOSSIBLE__
addConstant (defName infDefn) $
infDefn { theDef = Datatype
{ dataPars = 2
, dataIxs = 0
, dataInduction = CoInductive
, dataClause = Nothing
, dataCons = [sharp]
, dataSort = varSort 1
, dataPolarity = [Invariant, Invariant]
, dataArgOccurrences = [Unused, Positive]
, 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
sharp <- (\t -> case t of
Def q _ -> q
_ -> __IMPOSSIBLE__)
<$> primSharp
kit <- requireLevels
let clause = Clause { clauseRange = noRange
, clauseTel = ExtendTel (argH (El (mkType 0) (Def (typeName kit) [])))
(Abs "a" (ExtendTel (argH $ sort $ varSort 0)
(Abs "A" (ExtendTel (argN (El (varSort 1) (Var 0 [])))
(Abs "x" EmptyTel)))))
, clausePerm = idP 3
, clausePats = [ argH (VarP "a")
, argH (VarP "A")
, argN (ConP sharp Nothing [argN (VarP "x")])
]
, clauseBody = Bind $ Abs "h0" $
Bind $ Abs "h1" $
Bind $ Abs "h2" $ Body (Var 0 [])
}
addConstant flat $
flatDefn { theDef = Function
{ funClauses = [clause]
, funCompiled =
let hid = Arg Hidden Relevant
nohid = defaultArg in
Case 2 (Branches (Map.singleton sharp
(Done [hid "a", hid "A", nohid "x"] (Var 0 [])))
Map.empty
Nothing)
, funInv = NotInjective
, funPolarity = [Invariant, Invariant, Invariant]
, funArgOccurrences = [Unused, Unused, Positive]
, funAbstr = ConcreteDef
, funDelayed = NotDelayed
, funProjection = Nothing
, funStatic = False
}
}
return flatE
data CoinductionKit = CoinductionKit
{ nameOfInf :: QName
, nameOfSharp :: QName
, nameOfFlat :: QName
}
coinductionKit :: TCM (Maybe CoinductionKit)
coinductionKit = (do
Def inf _ <- primInf
Def sharp _ <- primSharp
Def flat _ <- primFlat
return $ Just $ CoinductionKit
{ nameOfInf = inf
, nameOfSharp = sharp
, nameOfFlat = flat
})
`catchError` \_ -> return Nothing