module Agda.TypeChecking.Rules.Builtin.Coinduction where
import qualified Data.Map as Map
import qualified Data.Set as Set
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.Monad.Builtin
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.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 :: ResolvedName -> TCM ()
bindBuiltinInf x = bindPostulatedName builtinInf x $ \inf _ ->
instantiateFull =<< checkExpr (A.Def inf) =<< typeOfInf
bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinSharp x =
bindPostulatedName builtinSharp x $ \sharp sharpDefn -> do
sharpType <- typeOfSharp
TelV fieldTel _ <- telView sharpType
sharpE <- instantiateFull =<< checkExpr (A.Def sharp) sharpType
Def inf _ <- primInf
infDefn <- getConstInfo inf
addConstant (defName infDefn) $
infDefn { defPolarity = []
, defArgOccurrences = [Unused, StrictPos]
, theDef = Record
{ recPars = 2
, recInduction = Just CoInductive
, recClause = Nothing
, recConHead = ConHead sharp CoInductive []
, recNamedCon = True
, recFields = []
, recTel = fieldTel
, recEtaEquality' = Inferred NoEta
, recMutual = Just []
, recAbstr = ConcreteDef
}
}
addConstant sharp $
sharpDefn { theDef = Constructor
{ conPars = 2
, conArity = 1
, conSrcCon = ConHead sharp CoInductive []
, conData = defName infDefn
, conAbstr = ConcreteDef
, conInd = CoInductive
, conForced = []
, conErased = []
}
}
return sharpE
bindBuiltinFlat :: ResolvedName -> TCM ()
bindBuiltinFlat x =
bindPostulatedName builtinFlat x $ \ flat flatDefn -> do
flatE <- instantiateFull =<< checkExpr (A.Def flat) =<< typeOfFlat
Def sharp _ <- primSharp
kit <- requireLevels
Def inf _ <- primInf
let sharpCon = ConHead sharp CoInductive [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
infA = El (varSort 2) $ Def inf [ Apply $ defaultArg $ var 1 ]
cpi = noConPatternInfo { conPType = Just $ defaultArg infA
, conPLazy = True }
let clause = Clause
{ clauseLHSRange = noRange
, clauseFullRange = noRange
, clauseTel = tel
, namedClausePats = [ argN $ Named Nothing $
ConP sharpCon cpi [ argN $ Named Nothing $ debruijnNamedVar "x" 0 ] ]
, clauseBody = Just $ var 0
, clauseType = Just $ defaultArg $ El (varSort 2) $ var 1
, clauseCatchall = False
, clauseUnreachable = Just False
}
cc = Case (defaultArg 0) $ conCase sharp $ WithArity 1 $ Done [defaultArg "x"] $ var 0
projection = Projection
{ projProper = Just inf
, projOrig = flat
, projFromType = defaultArg inf
, projIndex = 3
, projLams = ProjLams $ [ argH "a" , argH "A" , argN "x" ]
}
addConstant flat $
flatDefn { defPolarity = []
, defArgOccurrences = [StrictPos]
, theDef = emptyFunction
{ funClauses = [clause]
, funCompiled = Just $ cc
, funProjection = Just projection
, funMutual = Just []
, funTerminates = Just True
, funCopatternLHS = hasProjectionPatterns cc
}
}
modifySignature $ updateDefinition sharp $ updateTheDef $ \ def ->
def { conSrcCon = sharpCon }
modifySignature $ updateDefinition inf $ updateTheDef $ \ def ->
def { recConHead = sharpCon, recFields = [defaultArg flat] }
return flatE