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 = do
kit <- requireLevels
return $
El Inf (Pi (argH $ El (Type (Lit (LitLevel noRange 0))) (levelType kit))
(Abs "a" $ El (Type (levelSuc kit (Var 0 [])))
(Pi (argN $ El (Type (levelSuc kit (Var 0 [])))
(Sort (Type (Var 0 []))))
(Abs "A" $ El (Type (levelSuc kit (Var 1 [])))
(Sort (Type (Var 1 [])))))))
typeOfSharp :: TCM Type
typeOfSharp = do
kit <- requireLevels
inf <- (\t -> case t of
Def q _ -> q
_ -> __IMPOSSIBLE__)
<$> primInf
return $
El Inf (Pi (argH $ El (Type (Lit (LitLevel noRange 0))) (levelType kit))
(Abs "a" $ El (Lub (Type (levelSuc kit (Var 0 []))) (Type (Var 0 [])))
(Pi (argH $ El (Type (levelSuc kit (Var 0 []))) (Sort (Type (Var 0 []))))
(Abs "A" $ El (Type (Var 1 []))
(Pi (argN $ El (Type (Var 1 [])) (Var 0 []))
(Abs "x" $ El (Type (Var 2 []))
(Def inf [argH (Var 2 []), argN (Var 1 [])])))))))
typeOfFlat :: TCM Type
typeOfFlat = do
kit <- requireLevels
inf <- (\t -> case t of
Def q _ -> q
_ -> __IMPOSSIBLE__)
<$> primInf
return $
El Inf (Pi (argH $ El (Type (Lit (LitLevel noRange 0))) (levelType kit))
(Abs "a" $ El (Lub (Type (levelSuc kit (Var 0 []))) (Type (Var 0 [])))
(Pi (argH $ El (Type (levelSuc kit (Var 0 []))) (Sort (Type (Var 0 []))))
(Abs "A" $ El (Type (Var 1 []))
(Fun (argN $ El (Type (Var 1 []))
(Def inf [argH (Var 1 []), argN (Var 0 [])]))
(El (Type (Var 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 = Type (Var 1 [])
, dataPolarity = [Invariant, Invariant]
, dataArgOccurrences = [Unused, Positive]
, dataHsType = Nothing
, dataAbstr = ConcreteDef
}
}
addConstant sharp $
sharpDefn { theDef = Constructor
{ conPars = 2
, conSrcCon = sharp
, conData = defName infDefn
, conHsCode = Nothing
, 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 (Type (Lit (LitLevel noRange 0))) (Def (typeName kit) [])))
(Abs "a" (ExtendTel (argH (El (Type (Con (sucName kit) [argN (Var 0 [])]))
(Sort (Type (Var 0 [])))))
(Abs "A" (ExtendTel (argN (El (Type (Var 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 = [Clauses Nothing clause]
, funCompiled = Case 2 (Branches (Map.singleton sharp (Done 3 (Var 0 [])))
Map.empty
Nothing)
, funInv = NotInjective
, funPolarity = [Invariant, Invariant, Invariant]
, funArgOccurrences = [Unused, Unused, Positive]
, funAbstr = ConcreteDef
, funDelayed = NotDelayed
, funProjection = Nothing
}
}
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