{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Monad.Builtin where
import Control.Monad.State
import Control.Monad.Trans.Maybe
import qualified Data.Map as Map
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Substitute
import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Maybe
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
class (Functor m, Applicative m, Monad m) => HasBuiltins m where
getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))
instance HasBuiltins m => HasBuiltins (MaybeT m) where
getBuiltinThing b = lift $ getBuiltinThing b
litType :: Literal -> TCM Type
litType l = case l of
LitNat _ n -> do
_ <- primZero
when (n > 0) $ void $ primSuc
el <$> primNat
LitWord64 _ _ -> el <$> primWord64
LitFloat _ _ -> el <$> primFloat
LitChar _ _ -> el <$> primChar
LitString _ _ -> el <$> primString
LitQName _ _ -> el <$> primQName
LitMeta _ _ _ -> el <$> primAgdaMeta
where
el t = El (mkType 0) t
instance MonadIO m => HasBuiltins (TCMT m) where
getBuiltinThing b = liftM2 mplus (Map.lookup b <$> use stLocalBuiltins)
(Map.lookup b <$> use stImportedBuiltins)
setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
setBuiltinThings b = stLocalBuiltins .= b
bindBuiltinName :: String -> Term -> TCM ()
bindBuiltinName b x = do
builtin <- getBuiltinThing b
case builtin of
Just (Builtin y) -> typeError $ DuplicateBuiltinBinding b y x
Just (Prim _) -> typeError $ NoSuchBuiltinName b
Nothing -> stLocalBuiltins %= Map.insert b (Builtin x)
bindPrimitive :: String -> PrimFun -> TCM ()
bindPrimitive b pf = do
builtin <- use stLocalBuiltins
setBuiltinThings $ Map.insert b (Prim pf) builtin
getBuiltin :: String -> TCM Term
getBuiltin x =
fromMaybeM (typeError $ NoBindingForBuiltin x) $ getBuiltin' x
getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)
getBuiltin' x = do
builtin <- getBuiltinThing x
case builtin of
Just (Builtin t) -> return $ Just $ killRange t
_ -> return Nothing
getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' x = (getPrim =<<) <$> getBuiltinThing x
where
getPrim (Prim pf) = return pf
getPrim _ = Nothing
getPrimitive :: String -> TCM PrimFun
getPrimitive x =
fromMaybeM (typeError $ NoSuchPrimitiveFunction x) $ getPrimitive' x
constructorForm :: Term -> TCM Term
constructorForm v = constructorForm' primZero primSuc v
constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
constructorForm' pZero pSuc v =
case v of
Lit (LitNat r n)
| n == 0 -> pZero
| n > 0 -> (`apply1` Lit (LitNat r $ n - 1)) <$> pSuc
| otherwise -> pure v
_ -> pure v
primInteger, primIntegerPos, primIntegerNegSuc,
primFloat, primChar, primString, primUnit, primUnitUnit, primBool, primTrue, primFalse,
primList, primNil, primCons, primIO, primNat, primSuc, primZero,
primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux,
primNatEquality, primNatLess,
primWord64,
primSizeUniv, primSize, primSizeLt, primSizeSuc, primSizeInf, primSizeMax,
primInf, primSharp, primFlat,
primEquality, primRefl,
primRewrite,
primLevel, primLevelZero, primLevelSuc, primLevelMax,
primFromNat, primFromNeg, primFromString,
primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAbs, primAbsAbs, primAgdaTerm, primAgdaTermVar,
primAgdaTermLam, primAgdaTermExtLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
primAgdaTermSort, primAgdaTermLit, primAgdaTermUnsupported, primAgdaTermMeta,
primAgdaErrorPart, primAgdaErrorPartString, primAgdaErrorPartTerm, primAgdaErrorPartName,
primHiding, primHidden, primInstance, primVisible,
primRelevance, primRelevant, primIrrelevant,
primAssoc, primAssocLeft, primAssocRight, primAssocNon,
primPrecedence, primPrecRelated, primPrecUnrelated,
primFixity, primFixityFixity,
primAgdaLiteral, primAgdaLitNat, primAgdaLitWord64, primAgdaLitFloat, primAgdaLitString, primAgdaLitChar, primAgdaLitQName, primAgdaLitMeta,
primAgdaSort, primAgdaSortSet, primAgdaSortLit, primAgdaSortUnsupported,
primAgdaDefinition, primAgdaDefinitionFunDef, primAgdaDefinitionDataDef, primAgdaDefinitionRecordDef,
primAgdaDefinitionPostulate, primAgdaDefinitionPrimitive, primAgdaDefinitionDataConstructor,
primAgdaClause, primAgdaClauseClause, primAgdaClauseAbsurd,
primAgdaPattern, primAgdaPatCon, primAgdaPatVar, primAgdaPatDot,
primAgdaPatLit, primAgdaPatProj,
primAgdaPatAbsurd,
primAgdaMeta,
primAgdaTCM, primAgdaTCMReturn, primAgdaTCMBind, primAgdaTCMUnify,
primAgdaTCMTypeError, primAgdaTCMInferType, primAgdaTCMCheckType,
primAgdaTCMNormalise, primAgdaTCMReduce,
primAgdaTCMCatchError, primAgdaTCMGetContext, primAgdaTCMExtendContext, primAgdaTCMInContext,
primAgdaTCMFreshName, primAgdaTCMDeclareDef, primAgdaTCMDeclarePostulate, primAgdaTCMDefineFun,
primAgdaTCMGetType, primAgdaTCMGetDefinition,
primAgdaTCMQuoteTerm, primAgdaTCMUnquoteTerm,
primAgdaTCMBlockOnMeta, primAgdaTCMCommit, primAgdaTCMIsMacro,
primAgdaTCMWithNormalisation, primAgdaTCMDebugPrint
:: TCM Term
primInteger = getBuiltin builtinInteger
primIntegerPos = getBuiltin builtinIntegerPos
primIntegerNegSuc = getBuiltin builtinIntegerNegSuc
primFloat = getBuiltin builtinFloat
primChar = getBuiltin builtinChar
primString = getBuiltin builtinString
primBool = getBuiltin builtinBool
primUnit = getBuiltin builtinUnit
primUnitUnit = getBuiltin builtinUnitUnit
primTrue = getBuiltin builtinTrue
primFalse = getBuiltin builtinFalse
primList = getBuiltin builtinList
primNil = getBuiltin builtinNil
primCons = getBuiltin builtinCons
primIO = getBuiltin builtinIO
primNat = getBuiltin builtinNat
primSuc = getBuiltin builtinSuc
primZero = getBuiltin builtinZero
primNatPlus = getBuiltin builtinNatPlus
primNatMinus = getBuiltin builtinNatMinus
primNatTimes = getBuiltin builtinNatTimes
primNatDivSucAux = getBuiltin builtinNatDivSucAux
primNatModSucAux = getBuiltin builtinNatModSucAux
primNatEquality = getBuiltin builtinNatEquals
primNatLess = getBuiltin builtinNatLess
primWord64 = getBuiltin builtinWord64
primSizeUniv = getBuiltin builtinSizeUniv
primSize = getBuiltin builtinSize
primSizeLt = getBuiltin builtinSizeLt
primSizeSuc = getBuiltin builtinSizeSuc
primSizeInf = getBuiltin builtinSizeInf
primSizeMax = getBuiltin builtinSizeMax
primInf = getBuiltin builtinInf
primSharp = getBuiltin builtinSharp
primFlat = getBuiltin builtinFlat
primEquality = getBuiltin builtinEquality
primRefl = getBuiltin builtinRefl
primRewrite = getBuiltin builtinRewrite
primLevel = getBuiltin builtinLevel
primLevelZero = getBuiltin builtinLevelZero
primLevelSuc = getBuiltin builtinLevelSuc
primLevelMax = getBuiltin builtinLevelMax
primFromNat = getBuiltin builtinFromNat
primFromNeg = getBuiltin builtinFromNeg
primFromString = getBuiltin builtinFromString
primQName = getBuiltin builtinQName
primArg = getBuiltin builtinArg
primArgArg = getBuiltin builtinArgArg
primAbs = getBuiltin builtinAbs
primAbsAbs = getBuiltin builtinAbsAbs
primAgdaSort = getBuiltin builtinAgdaSort
primHiding = getBuiltin builtinHiding
primHidden = getBuiltin builtinHidden
primInstance = getBuiltin builtinInstance
primVisible = getBuiltin builtinVisible
primRelevance = getBuiltin builtinRelevance
primRelevant = getBuiltin builtinRelevant
primIrrelevant = getBuiltin builtinIrrelevant
primAssoc = getBuiltin builtinAssoc
primAssocLeft = getBuiltin builtinAssocLeft
primAssocRight = getBuiltin builtinAssocRight
primAssocNon = getBuiltin builtinAssocNon
primPrecedence = getBuiltin builtinPrecedence
primPrecRelated = getBuiltin builtinPrecRelated
primPrecUnrelated = getBuiltin builtinPrecUnrelated
primFixity = getBuiltin builtinFixity
primFixityFixity = getBuiltin builtinFixityFixity
primArgInfo = getBuiltin builtinArgInfo
primArgArgInfo = getBuiltin builtinArgArgInfo
primAgdaSortSet = getBuiltin builtinAgdaSortSet
primAgdaSortLit = getBuiltin builtinAgdaSortLit
primAgdaSortUnsupported = getBuiltin builtinAgdaSortUnsupported
primAgdaTerm = getBuiltin builtinAgdaTerm
primAgdaTermVar = getBuiltin builtinAgdaTermVar
primAgdaTermLam = getBuiltin builtinAgdaTermLam
primAgdaTermExtLam = getBuiltin builtinAgdaTermExtLam
primAgdaTermDef = getBuiltin builtinAgdaTermDef
primAgdaTermCon = getBuiltin builtinAgdaTermCon
primAgdaTermPi = getBuiltin builtinAgdaTermPi
primAgdaTermSort = getBuiltin builtinAgdaTermSort
primAgdaTermLit = getBuiltin builtinAgdaTermLit
primAgdaTermUnsupported = getBuiltin builtinAgdaTermUnsupported
primAgdaTermMeta = getBuiltin builtinAgdaTermMeta
primAgdaErrorPart = getBuiltin builtinAgdaErrorPart
primAgdaErrorPartString = getBuiltin builtinAgdaErrorPartString
primAgdaErrorPartTerm = getBuiltin builtinAgdaErrorPartTerm
primAgdaErrorPartName = getBuiltin builtinAgdaErrorPartName
primAgdaLiteral = getBuiltin builtinAgdaLiteral
primAgdaLitNat = getBuiltin builtinAgdaLitNat
primAgdaLitWord64 = getBuiltin builtinAgdaLitWord64
primAgdaLitFloat = getBuiltin builtinAgdaLitFloat
primAgdaLitChar = getBuiltin builtinAgdaLitChar
primAgdaLitString = getBuiltin builtinAgdaLitString
primAgdaLitQName = getBuiltin builtinAgdaLitQName
primAgdaLitMeta = getBuiltin builtinAgdaLitMeta
primAgdaPattern = getBuiltin builtinAgdaPattern
primAgdaPatCon = getBuiltin builtinAgdaPatCon
primAgdaPatVar = getBuiltin builtinAgdaPatVar
primAgdaPatDot = getBuiltin builtinAgdaPatDot
primAgdaPatLit = getBuiltin builtinAgdaPatLit
primAgdaPatProj = getBuiltin builtinAgdaPatProj
primAgdaPatAbsurd = getBuiltin builtinAgdaPatAbsurd
primAgdaClause = getBuiltin builtinAgdaClause
primAgdaClauseClause = getBuiltin builtinAgdaClauseClause
primAgdaClauseAbsurd = getBuiltin builtinAgdaClauseAbsurd
primAgdaDefinitionFunDef = getBuiltin builtinAgdaDefinitionFunDef
primAgdaDefinitionDataDef = getBuiltin builtinAgdaDefinitionDataDef
primAgdaDefinitionRecordDef = getBuiltin builtinAgdaDefinitionRecordDef
primAgdaDefinitionDataConstructor = getBuiltin builtinAgdaDefinitionDataConstructor
primAgdaDefinitionPostulate = getBuiltin builtinAgdaDefinitionPostulate
primAgdaDefinitionPrimitive = getBuiltin builtinAgdaDefinitionPrimitive
primAgdaDefinition = getBuiltin builtinAgdaDefinition
primAgdaMeta = getBuiltin builtinAgdaMeta
primAgdaTCM = getBuiltin builtinAgdaTCM
primAgdaTCMReturn = getBuiltin builtinAgdaTCMReturn
primAgdaTCMBind = getBuiltin builtinAgdaTCMBind
primAgdaTCMUnify = getBuiltin builtinAgdaTCMUnify
primAgdaTCMTypeError = getBuiltin builtinAgdaTCMTypeError
primAgdaTCMInferType = getBuiltin builtinAgdaTCMInferType
primAgdaTCMCheckType = getBuiltin builtinAgdaTCMCheckType
primAgdaTCMNormalise = getBuiltin builtinAgdaTCMNormalise
primAgdaTCMReduce = getBuiltin builtinAgdaTCMReduce
primAgdaTCMCatchError = getBuiltin builtinAgdaTCMCatchError
primAgdaTCMGetContext = getBuiltin builtinAgdaTCMGetContext
primAgdaTCMExtendContext = getBuiltin builtinAgdaTCMExtendContext
primAgdaTCMInContext = getBuiltin builtinAgdaTCMInContext
primAgdaTCMFreshName = getBuiltin builtinAgdaTCMFreshName
primAgdaTCMDeclareDef = getBuiltin builtinAgdaTCMDeclareDef
primAgdaTCMDeclarePostulate = getBuiltin builtinAgdaTCMDeclarePostulate
primAgdaTCMDefineFun = getBuiltin builtinAgdaTCMDefineFun
primAgdaTCMGetType = getBuiltin builtinAgdaTCMGetType
primAgdaTCMGetDefinition = getBuiltin builtinAgdaTCMGetDefinition
primAgdaTCMQuoteTerm = getBuiltin builtinAgdaTCMQuoteTerm
primAgdaTCMUnquoteTerm = getBuiltin builtinAgdaTCMUnquoteTerm
primAgdaTCMBlockOnMeta = getBuiltin builtinAgdaTCMBlockOnMeta
primAgdaTCMCommit = getBuiltin builtinAgdaTCMCommit
primAgdaTCMIsMacro = getBuiltin builtinAgdaTCMIsMacro
primAgdaTCMWithNormalisation = getBuiltin builtinAgdaTCMWithNormalisation
primAgdaTCMDebugPrint = getBuiltin builtinAgdaTCMDebugPrint
builtinNat, builtinSuc, builtinZero, builtinNatPlus, builtinNatMinus,
builtinNatTimes, builtinNatDivSucAux, builtinNatModSucAux, builtinNatEquals,
builtinNatLess, builtinInteger, builtinIntegerPos, builtinIntegerNegSuc,
builtinWord64,
builtinFloat, builtinChar, builtinString, builtinUnit, builtinUnitUnit,
builtinBool, builtinTrue, builtinFalse,
builtinList, builtinNil, builtinCons, builtinIO,
builtinSizeUniv, builtinSize, builtinSizeLt,
builtinSizeSuc, builtinSizeInf, builtinSizeMax,
builtinInf, builtinSharp, builtinFlat,
builtinEquality, builtinRefl, builtinRewrite, builtinLevelMax,
builtinLevel, builtinLevelZero, builtinLevelSuc,
builtinFromNat, builtinFromNeg, builtinFromString,
builtinQName, builtinAgdaSort, builtinAgdaSortSet, builtinAgdaSortLit,
builtinAgdaSortUnsupported,
builtinHiding, builtinHidden, builtinInstance, builtinVisible,
builtinRelevance, builtinRelevant, builtinIrrelevant, builtinArg,
builtinAssoc, builtinAssocLeft, builtinAssocRight, builtinAssocNon,
builtinPrecedence, builtinPrecRelated, builtinPrecUnrelated,
builtinFixity, builtinFixityFixity,
builtinArgInfo, builtinArgArgInfo, builtinArgArg,
builtinAbs, builtinAbsAbs, builtinAgdaTerm,
builtinAgdaTermVar, builtinAgdaTermLam, builtinAgdaTermExtLam,
builtinAgdaTermDef, builtinAgdaTermCon, builtinAgdaTermPi,
builtinAgdaTermSort, builtinAgdaTermLit, builtinAgdaTermUnsupported, builtinAgdaTermMeta,
builtinAgdaErrorPart, builtinAgdaErrorPartString, builtinAgdaErrorPartTerm, builtinAgdaErrorPartName,
builtinAgdaLiteral, builtinAgdaLitNat, builtinAgdaLitWord64, builtinAgdaLitFloat,
builtinAgdaLitChar, builtinAgdaLitString, builtinAgdaLitQName, builtinAgdaLitMeta,
builtinAgdaClause, builtinAgdaClauseClause, builtinAgdaClauseAbsurd, builtinAgdaPattern,
builtinAgdaPatVar, builtinAgdaPatCon, builtinAgdaPatDot, builtinAgdaPatLit,
builtinAgdaPatProj, builtinAgdaPatAbsurd,
builtinAgdaDefinitionFunDef,
builtinAgdaDefinitionDataDef, builtinAgdaDefinitionRecordDef,
builtinAgdaDefinitionDataConstructor, builtinAgdaDefinitionPostulate,
builtinAgdaDefinitionPrimitive, builtinAgdaDefinition,
builtinAgdaMeta,
builtinAgdaTCM, builtinAgdaTCMReturn, builtinAgdaTCMBind, builtinAgdaTCMUnify,
builtinAgdaTCMTypeError, builtinAgdaTCMInferType,
builtinAgdaTCMCheckType, builtinAgdaTCMNormalise, builtinAgdaTCMReduce,
builtinAgdaTCMCatchError,
builtinAgdaTCMGetContext, builtinAgdaTCMExtendContext, builtinAgdaTCMInContext,
builtinAgdaTCMFreshName, builtinAgdaTCMDeclareDef, builtinAgdaTCMDeclarePostulate, builtinAgdaTCMDefineFun,
builtinAgdaTCMGetType, builtinAgdaTCMGetDefinition,
builtinAgdaTCMQuoteTerm, builtinAgdaTCMUnquoteTerm,
builtinAgdaTCMBlockOnMeta, builtinAgdaTCMCommit, builtinAgdaTCMIsMacro,
builtinAgdaTCMWithNormalisation, builtinAgdaTCMDebugPrint
:: String
builtinNat = "NATURAL"
builtinSuc = "SUC"
builtinZero = "ZERO"
builtinNatPlus = "NATPLUS"
builtinNatMinus = "NATMINUS"
builtinNatTimes = "NATTIMES"
builtinNatDivSucAux = "NATDIVSUCAUX"
builtinNatModSucAux = "NATMODSUCAUX"
builtinNatEquals = "NATEQUALS"
builtinNatLess = "NATLESS"
builtinWord64 = "WORD64"
builtinInteger = "INTEGER"
builtinIntegerPos = "INTEGERPOS"
builtinIntegerNegSuc = "INTEGERNEGSUC"
builtinFloat = "FLOAT"
builtinChar = "CHAR"
builtinString = "STRING"
builtinUnit = "UNIT"
builtinUnitUnit = "UNITUNIT"
builtinBool = "BOOL"
builtinTrue = "TRUE"
builtinFalse = "FALSE"
builtinList = "LIST"
builtinNil = "NIL"
builtinCons = "CONS"
builtinIO = "IO"
builtinSizeUniv = "SIZEUNIV"
builtinSize = "SIZE"
builtinSizeLt = "SIZELT"
builtinSizeSuc = "SIZESUC"
builtinSizeInf = "SIZEINF"
builtinSizeMax = "SIZEMAX"
builtinInf = "INFINITY"
builtinSharp = "SHARP"
builtinFlat = "FLAT"
builtinEquality = "EQUALITY"
builtinRefl = "REFL"
builtinRewrite = "REWRITE"
builtinLevelMax = "LEVELMAX"
builtinLevel = "LEVEL"
builtinLevelZero = "LEVELZERO"
builtinLevelSuc = "LEVELSUC"
builtinFromNat = "FROMNAT"
builtinFromNeg = "FROMNEG"
builtinFromString = "FROMSTRING"
builtinQName = "QNAME"
builtinAgdaSort = "AGDASORT"
builtinAgdaSortSet = "AGDASORTSET"
builtinAgdaSortLit = "AGDASORTLIT"
builtinAgdaSortUnsupported = "AGDASORTUNSUPPORTED"
builtinHiding = "HIDING"
builtinHidden = "HIDDEN"
builtinInstance = "INSTANCE"
builtinVisible = "VISIBLE"
builtinRelevance = "RELEVANCE"
builtinRelevant = "RELEVANT"
builtinIrrelevant = "IRRELEVANT"
builtinAssoc = "ASSOC"
builtinAssocLeft = "ASSOCLEFT"
builtinAssocRight = "ASSOCRIGHT"
builtinAssocNon = "ASSOCNON"
builtinPrecedence = "PRECEDENCE"
builtinPrecRelated = "PRECRELATED"
builtinPrecUnrelated = "PRECUNRELATED"
builtinFixity = "FIXITY"
builtinFixityFixity = "FIXITYFIXITY"
builtinArg = "ARG"
builtinArgInfo = "ARGINFO"
builtinArgArgInfo = "ARGARGINFO"
builtinArgArg = "ARGARG"
builtinAbs = "ABS"
builtinAbsAbs = "ABSABS"
builtinAgdaTerm = "AGDATERM"
builtinAgdaTermVar = "AGDATERMVAR"
builtinAgdaTermLam = "AGDATERMLAM"
builtinAgdaTermExtLam = "AGDATERMEXTLAM"
builtinAgdaTermDef = "AGDATERMDEF"
builtinAgdaTermCon = "AGDATERMCON"
builtinAgdaTermPi = "AGDATERMPI"
builtinAgdaTermSort = "AGDATERMSORT"
builtinAgdaTermLit = "AGDATERMLIT"
builtinAgdaTermUnsupported = "AGDATERMUNSUPPORTED"
builtinAgdaTermMeta = "AGDATERMMETA"
builtinAgdaErrorPart = "AGDAERRORPART"
builtinAgdaErrorPartString = "AGDAERRORPARTSTRING"
builtinAgdaErrorPartTerm = "AGDAERRORPARTTERM"
builtinAgdaErrorPartName = "AGDAERRORPARTNAME"
builtinAgdaLiteral = "AGDALITERAL"
builtinAgdaLitNat = "AGDALITNAT"
builtinAgdaLitWord64 = "AGDALITWORD64"
builtinAgdaLitFloat = "AGDALITFLOAT"
builtinAgdaLitChar = "AGDALITCHAR"
builtinAgdaLitString = "AGDALITSTRING"
builtinAgdaLitQName = "AGDALITQNAME"
builtinAgdaLitMeta = "AGDALITMETA"
builtinAgdaClause = "AGDACLAUSE"
builtinAgdaClauseClause = "AGDACLAUSECLAUSE"
builtinAgdaClauseAbsurd = "AGDACLAUSEABSURD"
builtinAgdaPattern = "AGDAPATTERN"
builtinAgdaPatVar = "AGDAPATVAR"
builtinAgdaPatCon = "AGDAPATCON"
builtinAgdaPatDot = "AGDAPATDOT"
builtinAgdaPatLit = "AGDAPATLIT"
builtinAgdaPatProj = "AGDAPATPROJ"
builtinAgdaPatAbsurd = "AGDAPATABSURD"
builtinAgdaDefinitionFunDef = "AGDADEFINITIONFUNDEF"
builtinAgdaDefinitionDataDef = "AGDADEFINITIONDATADEF"
builtinAgdaDefinitionRecordDef = "AGDADEFINITIONRECORDDEF"
builtinAgdaDefinitionDataConstructor = "AGDADEFINITIONDATACONSTRUCTOR"
builtinAgdaDefinitionPostulate = "AGDADEFINITIONPOSTULATE"
builtinAgdaDefinitionPrimitive = "AGDADEFINITIONPRIMITIVE"
builtinAgdaDefinition = "AGDADEFINITION"
builtinAgdaMeta = "AGDAMETA"
builtinAgdaTCM = "AGDATCM"
builtinAgdaTCMReturn = "AGDATCMRETURN"
builtinAgdaTCMBind = "AGDATCMBIND"
builtinAgdaTCMUnify = "AGDATCMUNIFY"
builtinAgdaTCMTypeError = "AGDATCMTYPEERROR"
builtinAgdaTCMInferType = "AGDATCMINFERTYPE"
builtinAgdaTCMCheckType = "AGDATCMCHECKTYPE"
builtinAgdaTCMNormalise = "AGDATCMNORMALISE"
builtinAgdaTCMReduce = "AGDATCMREDUCE"
builtinAgdaTCMCatchError = "AGDATCMCATCHERROR"
builtinAgdaTCMGetContext = "AGDATCMGETCONTEXT"
builtinAgdaTCMExtendContext = "AGDATCMEXTENDCONTEXT"
builtinAgdaTCMInContext = "AGDATCMINCONTEXT"
builtinAgdaTCMFreshName = "AGDATCMFRESHNAME"
builtinAgdaTCMDeclareDef = "AGDATCMDECLAREDEF"
builtinAgdaTCMDeclarePostulate = "AGDATCMDECLAREPOSTULATE"
builtinAgdaTCMDefineFun = "AGDATCMDEFINEFUN"
builtinAgdaTCMGetType = "AGDATCMGETTYPE"
builtinAgdaTCMGetDefinition = "AGDATCMGETDEFINITION"
builtinAgdaTCMBlockOnMeta = "AGDATCMBLOCKONMETA"
builtinAgdaTCMCommit = "AGDATCMCOMMIT"
builtinAgdaTCMQuoteTerm = "AGDATCMQUOTETERM"
builtinAgdaTCMUnquoteTerm = "AGDATCMUNQUOTETERM"
builtinAgdaTCMIsMacro = "AGDATCMISMACRO"
builtinAgdaTCMWithNormalisation = "AGDATCMWITHNORMALISATION"
builtinAgdaTCMDebugPrint = "AGDATCMDEBUGPRINT"
builtinsNoDef :: [String]
builtinsNoDef =
[ builtinSizeUniv
, builtinSize
, builtinSizeLt
, builtinSizeSuc
, builtinSizeInf
, builtinSizeMax
]
data CoinductionKit = CoinductionKit
{ nameOfInf :: QName
, nameOfSharp :: QName
, nameOfFlat :: QName
}
coinductionKit' :: TCM CoinductionKit
coinductionKit' = do
Def inf _ <- primInf
Def sharp _ <- primSharp
Def flat _ <- primFlat
return $ CoinductionKit
{ nameOfInf = inf
, nameOfSharp = sharp
, nameOfFlat = flat
}
coinductionKit :: TCM (Maybe CoinductionKit)
coinductionKit = tryMaybe coinductionKit'
primEqualityName :: TCM QName
primEqualityName = do
eq <- primEquality
let lamV (Lam i b) = mapFst (getHiding i :) $ lamV (unAbs b)
lamV v = ([], v)
return $ case lamV eq of
(_, Def equality _) -> equality
_ -> __IMPOSSIBLE__
equalityView :: Type -> TCM EqualityView
equalityView t0@(El s t) = do
equality <- primEqualityName
case t of
Def equality' es | equality' == equality -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
let n = length vs
unless (n >= 3) __IMPOSSIBLE__
let (pars, [ typ , lhs, rhs ]) = splitAt (n-3) vs
return $ EqualityType s equality pars typ lhs rhs
_ -> return $ OtherType t0
equalityUnview :: EqualityView -> Type
equalityUnview (OtherType t) = t
equalityUnview (EqualityType s equality l t lhs rhs) =
El s $ Def equality $ map Apply (l ++ [t, lhs, rhs])