-- | This module defines the names of all BUILTINs.
module Agda.Syntax.Builtin where

builtinNat, builtinSuc, builtinZero, builtinNatPlus, builtinNatMinus,
  builtinNatTimes, builtinNatDivSucAux, builtinNatModSucAux, builtinNatEquals,
  builtinNatLess, builtinInteger, builtinIntegerPos, builtinIntegerNegSuc,
  builtinWord64,
  builtinFloat, builtinChar, builtinString, builtinUnit, builtinUnitUnit,
  builtinSigma,
  builtinBool, builtinTrue, builtinFalse,
  builtinList, builtinNil, builtinCons, builtinIO,
  builtinPath, builtinPathP, builtinInterval, builtinIZero, builtinIOne, builtinPartial, builtinPartialP,
  builtinIMin, builtinIMax, builtinINeg,
  builtinIsOne,  builtinItIsOne, builtinIsOne1, builtinIsOne2, builtinIsOneEmpty,
  builtinComp, builtinPOr,
  builtinTrans, builtinHComp,
  builtinSub, builtinSubIn, builtinSubOut,
  builtinEquiv, builtinEquivFun, builtinEquivProof,
  builtinTranspProof,
  builtinGlue, builtin_glue, builtin_unglue,
  builtin_glueU, builtin_unglueU,
  builtinFaceForall,
  builtinId, builtinConId, builtinIdElim,
  builtinSizeUniv, builtinSize, builtinSizeLt,
  builtinSizeSuc, builtinSizeInf, builtinSizeMax,
  builtinInf, builtinSharp, builtinFlat,
  builtinEquality, builtinRefl, builtinRewrite, builtinLevelMax,
  builtinLevel, builtinLevelZero, builtinLevelSuc,
  builtinSetOmega,
  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,
  builtinAgdaTCMNoConstraints,
  builtinAgdaTCMRunSpeculative
  :: String

builtinNat :: String
builtinNat                               = String
"NATURAL"
builtinSuc :: String
builtinSuc                               = String
"SUC"
builtinZero :: String
builtinZero                              = String
"ZERO"
builtinNatPlus :: String
builtinNatPlus                           = String
"NATPLUS"
builtinNatMinus :: String
builtinNatMinus                          = String
"NATMINUS"
builtinNatTimes :: String
builtinNatTimes                          = String
"NATTIMES"
builtinNatDivSucAux :: String
builtinNatDivSucAux                      = String
"NATDIVSUCAUX"
builtinNatModSucAux :: String
builtinNatModSucAux                      = String
"NATMODSUCAUX"
builtinNatEquals :: String
builtinNatEquals                         = String
"NATEQUALS"
builtinNatLess :: String
builtinNatLess                           = String
"NATLESS"
builtinWord64 :: String
builtinWord64                            = String
"WORD64"
builtinInteger :: String
builtinInteger                           = String
"INTEGER"
builtinIntegerPos :: String
builtinIntegerPos                        = String
"INTEGERPOS"
builtinIntegerNegSuc :: String
builtinIntegerNegSuc                     = String
"INTEGERNEGSUC"
builtinFloat :: String
builtinFloat                             = String
"FLOAT"
builtinChar :: String
builtinChar                              = String
"CHAR"
builtinString :: String
builtinString                            = String
"STRING"
builtinUnit :: String
builtinUnit                              = String
"UNIT"
builtinUnitUnit :: String
builtinUnitUnit                          = String
"UNITUNIT"
builtinSigma :: String
builtinSigma                             = String
"SIGMA"
builtinBool :: String
builtinBool                              = String
"BOOL"
builtinTrue :: String
builtinTrue                              = String
"TRUE"
builtinFalse :: String
builtinFalse                             = String
"FALSE"
builtinList :: String
builtinList                              = String
"LIST"
builtinNil :: String
builtinNil                               = String
"NIL"
builtinCons :: String
builtinCons                              = String
"CONS"
builtinIO :: String
builtinIO                                = String
"IO"
builtinId :: String
builtinId                                = String
"ID"
builtinConId :: String
builtinConId                             = String
"CONID"
builtinIdElim :: String
builtinIdElim                            = String
"primIdElim"
builtinPath :: String
builtinPath                              = String
"PATH"
builtinPathP :: String
builtinPathP                             = String
"PATHP"
builtinInterval :: String
builtinInterval                          = String
"INTERVAL"
builtinIMin :: String
builtinIMin                              = String
"primIMin"
builtinIMax :: String
builtinIMax                              = String
"primIMax"
builtinINeg :: String
builtinINeg                              = String
"primINeg"
builtinIZero :: String
builtinIZero                             = String
"IZERO"
builtinIOne :: String
builtinIOne                              = String
"IONE"
builtinPartial :: String
builtinPartial                           = String
"PARTIAL"
builtinPartialP :: String
builtinPartialP                          = String
"PARTIALP"
builtinIsOne :: String
builtinIsOne                             = String
"ISONE"
builtinItIsOne :: String
builtinItIsOne                           = String
"ITISONE"
builtinEquiv :: String
builtinEquiv                             = String
"EQUIV"
builtinEquivFun :: String
builtinEquivFun                          = String
"EQUIVFUN"
builtinEquivProof :: String
builtinEquivProof                        = String
"EQUIVPROOF"
builtinTranspProof :: String
builtinTranspProof                       = String
"TRANSPPROOF"
builtinGlue :: String
builtinGlue                              = String
"primGlue"
builtin_glue :: String
builtin_glue                             = String
"prim^glue"
builtin_unglue :: String
builtin_unglue                           = String
"prim^unglue"
builtin_glueU :: String
builtin_glueU                            = String
"prim^glueU"
builtin_unglueU :: String
builtin_unglueU                          = String
"prim^unglueU"
builtinFaceForall :: String
builtinFaceForall                        = String
"primFaceForall"
builtinIsOne1 :: String
builtinIsOne1                            = String
"ISONE1"
builtinIsOne2 :: String
builtinIsOne2                            = String
"ISONE2"
builtinIsOneEmpty :: String
builtinIsOneEmpty                        = String
"ISONEEMPTY"
builtinComp :: String
builtinComp                              = String
"primComp"
builtinPOr :: String
builtinPOr                               = String
"primPOr"
builtinTrans :: String
builtinTrans                             = String
"primTransp"
builtinHComp :: String
builtinHComp                             = String
"primHComp"
builtinSub :: String
builtinSub                               = String
"SUB"
builtinSubIn :: String
builtinSubIn                             = String
"SUBIN"
builtinSubOut :: String
builtinSubOut                            = String
"primSubOut"
builtinSizeUniv :: String
builtinSizeUniv                          = String
"SIZEUNIV"
builtinSize :: String
builtinSize                              = String
"SIZE"
builtinSizeLt :: String
builtinSizeLt                            = String
"SIZELT"
builtinSizeSuc :: String
builtinSizeSuc                           = String
"SIZESUC"
builtinSizeInf :: String
builtinSizeInf                           = String
"SIZEINF"
builtinSizeMax :: String
builtinSizeMax                           = String
"SIZEMAX"
builtinInf :: String
builtinInf                               = String
"INFINITY"
builtinSharp :: String
builtinSharp                             = String
"SHARP"
builtinFlat :: String
builtinFlat                              = String
"FLAT"
builtinEquality :: String
builtinEquality                          = String
"EQUALITY"
builtinRefl :: String
builtinRefl                              = String
"REFL"
builtinRewrite :: String
builtinRewrite                           = String
"REWRITE"
builtinLevelMax :: String
builtinLevelMax                          = String
"LEVELMAX"
builtinLevel :: String
builtinLevel                             = String
"LEVEL"
builtinLevelZero :: String
builtinLevelZero                         = String
"LEVELZERO"
builtinLevelSuc :: String
builtinLevelSuc                          = String
"LEVELSUC"
builtinSetOmega :: String
builtinSetOmega                          = String
"SETOMEGA"
builtinFromNat :: String
builtinFromNat                           = String
"FROMNAT"
builtinFromNeg :: String
builtinFromNeg                           = String
"FROMNEG"
builtinFromString :: String
builtinFromString                        = String
"FROMSTRING"
builtinQName :: String
builtinQName                             = String
"QNAME"
builtinAgdaSort :: String
builtinAgdaSort                          = String
"AGDASORT"
builtinAgdaSortSet :: String
builtinAgdaSortSet                       = String
"AGDASORTSET"
builtinAgdaSortLit :: String
builtinAgdaSortLit                       = String
"AGDASORTLIT"
builtinAgdaSortUnsupported :: String
builtinAgdaSortUnsupported               = String
"AGDASORTUNSUPPORTED"
builtinHiding :: String
builtinHiding                            = String
"HIDING"
builtinHidden :: String
builtinHidden                            = String
"HIDDEN"
builtinInstance :: String
builtinInstance                          = String
"INSTANCE"
builtinVisible :: String
builtinVisible                           = String
"VISIBLE"
builtinRelevance :: String
builtinRelevance                         = String
"RELEVANCE"
builtinRelevant :: String
builtinRelevant                          = String
"RELEVANT"
builtinIrrelevant :: String
builtinIrrelevant                        = String
"IRRELEVANT"
builtinAssoc :: String
builtinAssoc                             = String
"ASSOC"
builtinAssocLeft :: String
builtinAssocLeft                         = String
"ASSOCLEFT"
builtinAssocRight :: String
builtinAssocRight                        = String
"ASSOCRIGHT"
builtinAssocNon :: String
builtinAssocNon                          = String
"ASSOCNON"
builtinPrecedence :: String
builtinPrecedence                        = String
"PRECEDENCE"
builtinPrecRelated :: String
builtinPrecRelated                       = String
"PRECRELATED"
builtinPrecUnrelated :: String
builtinPrecUnrelated                     = String
"PRECUNRELATED"
builtinFixity :: String
builtinFixity                            = String
"FIXITY"
builtinFixityFixity :: String
builtinFixityFixity                      = String
"FIXITYFIXITY"
builtinArg :: String
builtinArg                               = String
"ARG"
builtinArgInfo :: String
builtinArgInfo                           = String
"ARGINFO"
builtinArgArgInfo :: String
builtinArgArgInfo                        = String
"ARGARGINFO"
builtinArgArg :: String
builtinArgArg                            = String
"ARGARG"
builtinAbs :: String
builtinAbs                               = String
"ABS"
builtinAbsAbs :: String
builtinAbsAbs                            = String
"ABSABS"
builtinAgdaTerm :: String
builtinAgdaTerm                          = String
"AGDATERM"
builtinAgdaTermVar :: String
builtinAgdaTermVar                       = String
"AGDATERMVAR"
builtinAgdaTermLam :: String
builtinAgdaTermLam                       = String
"AGDATERMLAM"
builtinAgdaTermExtLam :: String
builtinAgdaTermExtLam                    = String
"AGDATERMEXTLAM"
builtinAgdaTermDef :: String
builtinAgdaTermDef                       = String
"AGDATERMDEF"
builtinAgdaTermCon :: String
builtinAgdaTermCon                       = String
"AGDATERMCON"
builtinAgdaTermPi :: String
builtinAgdaTermPi                        = String
"AGDATERMPI"
builtinAgdaTermSort :: String
builtinAgdaTermSort                      = String
"AGDATERMSORT"
builtinAgdaTermLit :: String
builtinAgdaTermLit                       = String
"AGDATERMLIT"
builtinAgdaTermUnsupported :: String
builtinAgdaTermUnsupported               = String
"AGDATERMUNSUPPORTED"
builtinAgdaTermMeta :: String
builtinAgdaTermMeta                      = String
"AGDATERMMETA"
builtinAgdaErrorPart :: String
builtinAgdaErrorPart                     = String
"AGDAERRORPART"
builtinAgdaErrorPartString :: String
builtinAgdaErrorPartString               = String
"AGDAERRORPARTSTRING"
builtinAgdaErrorPartTerm :: String
builtinAgdaErrorPartTerm                 = String
"AGDAERRORPARTTERM"
builtinAgdaErrorPartName :: String
builtinAgdaErrorPartName                 = String
"AGDAERRORPARTNAME"
builtinAgdaLiteral :: String
builtinAgdaLiteral                       = String
"AGDALITERAL"
builtinAgdaLitNat :: String
builtinAgdaLitNat                        = String
"AGDALITNAT"
builtinAgdaLitWord64 :: String
builtinAgdaLitWord64                     = String
"AGDALITWORD64"
builtinAgdaLitFloat :: String
builtinAgdaLitFloat                      = String
"AGDALITFLOAT"
builtinAgdaLitChar :: String
builtinAgdaLitChar                       = String
"AGDALITCHAR"
builtinAgdaLitString :: String
builtinAgdaLitString                     = String
"AGDALITSTRING"
builtinAgdaLitQName :: String
builtinAgdaLitQName                      = String
"AGDALITQNAME"
builtinAgdaLitMeta :: String
builtinAgdaLitMeta                       = String
"AGDALITMETA"
builtinAgdaClause :: String
builtinAgdaClause                        = String
"AGDACLAUSE"
builtinAgdaClauseClause :: String
builtinAgdaClauseClause                  = String
"AGDACLAUSECLAUSE"
builtinAgdaClauseAbsurd :: String
builtinAgdaClauseAbsurd                  = String
"AGDACLAUSEABSURD"
builtinAgdaPattern :: String
builtinAgdaPattern                       = String
"AGDAPATTERN"
builtinAgdaPatVar :: String
builtinAgdaPatVar                        = String
"AGDAPATVAR"
builtinAgdaPatCon :: String
builtinAgdaPatCon                        = String
"AGDAPATCON"
builtinAgdaPatDot :: String
builtinAgdaPatDot                        = String
"AGDAPATDOT"
builtinAgdaPatLit :: String
builtinAgdaPatLit                        = String
"AGDAPATLIT"
builtinAgdaPatProj :: String
builtinAgdaPatProj                       = String
"AGDAPATPROJ"
builtinAgdaPatAbsurd :: String
builtinAgdaPatAbsurd                     = String
"AGDAPATABSURD"
builtinAgdaDefinitionFunDef :: String
builtinAgdaDefinitionFunDef              = String
"AGDADEFINITIONFUNDEF"
builtinAgdaDefinitionDataDef :: String
builtinAgdaDefinitionDataDef             = String
"AGDADEFINITIONDATADEF"
builtinAgdaDefinitionRecordDef :: String
builtinAgdaDefinitionRecordDef           = String
"AGDADEFINITIONRECORDDEF"
builtinAgdaDefinitionDataConstructor :: String
builtinAgdaDefinitionDataConstructor     = String
"AGDADEFINITIONDATACONSTRUCTOR"
builtinAgdaDefinitionPostulate :: String
builtinAgdaDefinitionPostulate           = String
"AGDADEFINITIONPOSTULATE"
builtinAgdaDefinitionPrimitive :: String
builtinAgdaDefinitionPrimitive           = String
"AGDADEFINITIONPRIMITIVE"
builtinAgdaDefinition :: String
builtinAgdaDefinition                    = String
"AGDADEFINITION"
builtinAgdaMeta :: String
builtinAgdaMeta                          = String
"AGDAMETA"
builtinAgdaTCM :: String
builtinAgdaTCM                           = String
"AGDATCM"
builtinAgdaTCMReturn :: String
builtinAgdaTCMReturn                     = String
"AGDATCMRETURN"
builtinAgdaTCMBind :: String
builtinAgdaTCMBind                       = String
"AGDATCMBIND"
builtinAgdaTCMUnify :: String
builtinAgdaTCMUnify                      = String
"AGDATCMUNIFY"
builtinAgdaTCMTypeError :: String
builtinAgdaTCMTypeError                  = String
"AGDATCMTYPEERROR"
builtinAgdaTCMInferType :: String
builtinAgdaTCMInferType                  = String
"AGDATCMINFERTYPE"
builtinAgdaTCMCheckType :: String
builtinAgdaTCMCheckType                  = String
"AGDATCMCHECKTYPE"
builtinAgdaTCMNormalise :: String
builtinAgdaTCMNormalise                  = String
"AGDATCMNORMALISE"
builtinAgdaTCMReduce :: String
builtinAgdaTCMReduce                     = String
"AGDATCMREDUCE"
builtinAgdaTCMCatchError :: String
builtinAgdaTCMCatchError                 = String
"AGDATCMCATCHERROR"
builtinAgdaTCMGetContext :: String
builtinAgdaTCMGetContext                 = String
"AGDATCMGETCONTEXT"
builtinAgdaTCMExtendContext :: String
builtinAgdaTCMExtendContext              = String
"AGDATCMEXTENDCONTEXT"
builtinAgdaTCMInContext :: String
builtinAgdaTCMInContext                  = String
"AGDATCMINCONTEXT"
builtinAgdaTCMFreshName :: String
builtinAgdaTCMFreshName                  = String
"AGDATCMFRESHNAME"
builtinAgdaTCMDeclareDef :: String
builtinAgdaTCMDeclareDef                 = String
"AGDATCMDECLAREDEF"
builtinAgdaTCMDeclarePostulate :: String
builtinAgdaTCMDeclarePostulate           = String
"AGDATCMDECLAREPOSTULATE"
builtinAgdaTCMDefineFun :: String
builtinAgdaTCMDefineFun                  = String
"AGDATCMDEFINEFUN"
builtinAgdaTCMGetType :: String
builtinAgdaTCMGetType                    = String
"AGDATCMGETTYPE"
builtinAgdaTCMGetDefinition :: String
builtinAgdaTCMGetDefinition              = String
"AGDATCMGETDEFINITION"
builtinAgdaTCMBlockOnMeta :: String
builtinAgdaTCMBlockOnMeta                = String
"AGDATCMBLOCKONMETA"
builtinAgdaTCMCommit :: String
builtinAgdaTCMCommit                     = String
"AGDATCMCOMMIT"
builtinAgdaTCMQuoteTerm :: String
builtinAgdaTCMQuoteTerm                  = String
"AGDATCMQUOTETERM"
builtinAgdaTCMUnquoteTerm :: String
builtinAgdaTCMUnquoteTerm                = String
"AGDATCMUNQUOTETERM"
builtinAgdaTCMIsMacro :: String
builtinAgdaTCMIsMacro                    = String
"AGDATCMISMACRO"
builtinAgdaTCMWithNormalisation :: String
builtinAgdaTCMWithNormalisation          = String
"AGDATCMWITHNORMALISATION"
builtinAgdaTCMDebugPrint :: String
builtinAgdaTCMDebugPrint                 = String
"AGDATCMDEBUGPRINT"
builtinAgdaTCMNoConstraints :: String
builtinAgdaTCMNoConstraints              = String
"AGDATCMNOCONSTRAINTS"
builtinAgdaTCMRunSpeculative :: String
builtinAgdaTCMRunSpeculative             = String
"AGDATCMRUNSPECULATIVE"

-- | Builtins that come without a definition in Agda syntax.
--   These are giving names to Agda internal concepts which
--   cannot be assigned an Agda type.
--
--   An example would be a user-defined name for @Set@.
--
--     {-# BUILTIN TYPE Type #-}
--
--   The type of @Type@ would be @Type : Level → Setω@
--   which is not valid Agda.

builtinsNoDef :: [String]
builtinsNoDef :: [String]
builtinsNoDef =
  [String]
sizeBuiltins [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
builtinConId
  , String
builtinInterval
  , String
builtinPartial
  , String
builtinPartialP
  , String
builtinIsOne
  , String
builtinSub
  , String
builtinIZero
  , String
builtinIOne
  , String
builtinSetOmega
  ]

sizeBuiltins :: [String]
sizeBuiltins :: [String]
sizeBuiltins =
  [ String
builtinSizeUniv
  , String
builtinSize
  , String
builtinSizeLt
  , String
builtinSizeSuc
  , String
builtinSizeInf
  , String
builtinSizeMax
  ]