content: {-# OPTIONS_GHC -Wunused-imports #-}
  {-# OPTIONS_GHC -Wunused-matches #-}
  
  -- | This module defines the names of all builtin and primitives used in Agda.
  --
  -- See "Agda.TypeChecking.Monad.Builtin"
  module Agda.Syntax.Builtin where
  
  import GHC.Generics (Generic)
  
  import Control.DeepSeq (NFData)
  
  import qualified Data.Map as M
  import Data.Hashable
  
  import Agda.Syntax.Common.Pretty
  import Agda.Syntax.Position
  
  import Agda.Utils.List
  
  -- | Either a 'BuiltinId' or 'PrimitiveId', used for some lookups.
  data SomeBuiltin
    = BuiltinName !BuiltinId
    | PrimitiveName !PrimitiveId
    deriving (Show, Eq, Ord, Generic)
  
  instance Hashable SomeBuiltin
  instance NFData SomeBuiltin
  
  -- | The class of types which can be converted to 'SomeBuiltin'.
  class IsBuiltin a where
    -- | Convert this value to a builtin.
    someBuiltin :: a -> SomeBuiltin
  
    -- | Get the identifier for this builtin, generally used for error messages.
    getBuiltinId :: a -> String
  
  instance IsBuiltin SomeBuiltin where
    someBuiltin = id
  
    getBuiltinId (BuiltinName x) = getBuiltinId x
    getBuiltinId (PrimitiveName x) = getBuiltinId x
  
  -- * Builtins
  
  -- | A builtin name, defined by the @BUILTIN@ pragma.
  data BuiltinId
    = BuiltinNat
    | BuiltinSuc
    | BuiltinZero
    | BuiltinNatPlus
    | BuiltinNatMinus
    | BuiltinNatTimes
    | BuiltinNatDivSucAux
    | BuiltinNatModSucAux
    | BuiltinNatEquals
    | BuiltinNatLess
    | BuiltinWord64
    | BuiltinInteger
    | BuiltinIntegerPos
    | BuiltinIntegerNegSuc
    | BuiltinFloat
    | BuiltinChar
    | BuiltinString
    | BuiltinUnit
    | BuiltinUnitUnit
    | BuiltinSigma
    | BuiltinSigmaCon
    | BuiltinBool
    | BuiltinTrue
    | BuiltinFalse
    | BuiltinList
    | BuiltinNil
    | BuiltinCons
    | BuiltinMaybe
    | BuiltinNothing
    | BuiltinJust
    | BuiltinIO
    | BuiltinPath
    | BuiltinPathP
    | BuiltinIntervalUniv
    | BuiltinInterval
    | BuiltinIZero
    | BuiltinIOne
    | BuiltinPartial
    | BuiltinPartialP
    | BuiltinIsOne
    | BuiltinItIsOne
    | BuiltinEquiv
    | BuiltinEquivFun
    | BuiltinEquivProof
    | BuiltinTranspProof
    | BuiltinIsOne1
    | BuiltinIsOne2
    | BuiltinIsOneEmpty
    | BuiltinSub
    | BuiltinSubIn
    | BuiltinSizeUniv
    | BuiltinSize
    | BuiltinSizeLt
    | BuiltinSizeSuc
    | BuiltinSizeInf
    | BuiltinSizeMax
    | BuiltinInf
    | BuiltinSharp
    | BuiltinFlat
    | BuiltinEquality
    | BuiltinRefl
    | BuiltinRewrite
    | BuiltinLevelMax
    | BuiltinLevel
    | BuiltinLevelZero
    | BuiltinLevelSuc
    | BuiltinProp
    | BuiltinSet
    | BuiltinStrictSet
    | BuiltinPropOmega
    | BuiltinSetOmega
    | BuiltinSSetOmega
    | BuiltinLevelUniv
    | BuiltinFromNat
    | BuiltinFromNeg
    | BuiltinFromString
    | BuiltinQName
    | BuiltinAgdaSort
    | BuiltinAgdaSortSet
    | BuiltinAgdaSortLit
    | BuiltinAgdaSortProp
    | BuiltinAgdaSortPropLit
    | BuiltinAgdaSortInf
    | BuiltinAgdaSortUnsupported
    | BuiltinHiding
    | BuiltinHidden
    | BuiltinInstance
    | BuiltinVisible
    | BuiltinRelevance
    | BuiltinRelevant
    | BuiltinIrrelevant
    | BuiltinQuantity
    | BuiltinQuantity0
    | BuiltinQuantityω
    | BuiltinModality
    | BuiltinModalityConstructor
    | BuiltinAssoc
    | BuiltinAssocLeft
    | BuiltinAssocRight
    | BuiltinAssocNon
    | BuiltinPrecedence
    | BuiltinPrecRelated
    | BuiltinPrecUnrelated
    | BuiltinFixity
    | BuiltinFixityFixity
    | BuiltinArg
    | BuiltinArgInfo
    | BuiltinArgArgInfo
    | BuiltinArgArg
    | BuiltinAbs
    | BuiltinAbsAbs
    | BuiltinAgdaTerm
    | BuiltinAgdaTermVar
    | BuiltinAgdaTermLam
    | BuiltinAgdaTermExtLam
    | BuiltinAgdaTermDef
    | BuiltinAgdaTermCon
    | BuiltinAgdaTermPi
    | BuiltinAgdaTermSort
    | BuiltinAgdaTermLit
    | BuiltinAgdaTermUnsupported
    | BuiltinAgdaTermMeta
    | BuiltinAgdaErrorPart
    | BuiltinAgdaErrorPartString
    | BuiltinAgdaErrorPartTerm
    | BuiltinAgdaErrorPartPatt
    | 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
    | BuiltinAgdaTCMDeclareData
    | BuiltinAgdaTCMDefineData
    | BuiltinAgdaTCMDefineFun
    | BuiltinAgdaTCMGetType
    | BuiltinAgdaTCMGetDefinition
    | BuiltinAgdaTCMBlock
    | BuiltinAgdaTCMCommit
    | BuiltinAgdaTCMQuoteTerm
    | BuiltinAgdaTCMUnquoteTerm
    | BuiltinAgdaTCMQuoteOmegaTerm
    | BuiltinAgdaTCMIsMacro
    | BuiltinAgdaTCMWithNormalisation
    | BuiltinAgdaTCMWithReconstructed
    | BuiltinAgdaTCMWithExpandLast
    | BuiltinAgdaTCMWithReduceDefs
    | BuiltinAgdaTCMAskNormalisation
    | BuiltinAgdaTCMAskReconstructed
    | BuiltinAgdaTCMAskExpandLast
    | BuiltinAgdaTCMAskReduceDefs
    | BuiltinAgdaTCMFormatErrorParts
    | BuiltinAgdaTCMDebugPrint
    | BuiltinAgdaTCMNoConstraints
    | BuiltinAgdaTCMWorkOnTypes
    | BuiltinAgdaTCMRunSpeculative
    | BuiltinAgdaTCMExec
    | BuiltinAgdaTCMCheckFromString
    | BuiltinAgdaTCMGetInstances
    | BuiltinAgdaTCMSolveInstances
    | BuiltinAgdaTCMPragmaForeign
    | BuiltinAgdaTCMPragmaCompile
    | BuiltinAgdaBlocker
    | BuiltinAgdaBlockerAny
    | BuiltinAgdaBlockerAll
    | BuiltinAgdaBlockerMeta
    deriving (Show, Eq, Ord, Bounded, Enum, Generic)
  
  instance NFData BuiltinId
  
  instance Hashable BuiltinId where
    s `hashWithSalt` b = s `hashWithSalt` fromEnum b
  
  instance KillRange BuiltinId where
    killRange = id
  
  instance Pretty BuiltinId where
    pretty = text . getBuiltinId
  
  instance IsBuiltin BuiltinId where
    someBuiltin = BuiltinName
  
    getBuiltinId = \case
      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"
      BuiltinSigma                             -> "SIGMA"
      BuiltinSigmaCon                          -> "SIGMACON"
      BuiltinBool                              -> "BOOL"
      BuiltinTrue                              -> "TRUE"
      BuiltinFalse                             -> "FALSE"
      BuiltinList                              -> "LIST"
      BuiltinNil                               -> "NIL"
      BuiltinCons                              -> "CONS"
      BuiltinMaybe                             -> "MAYBE"
      BuiltinNothing                           -> "NOTHING"
      BuiltinJust                              -> "JUST"
      BuiltinIO                                -> "IO"
      BuiltinPath                              -> "PATH"
      BuiltinPathP                             -> "PATHP"
      BuiltinIntervalUniv                      -> "CUBEINTERVALUNIV"
      BuiltinInterval                          -> "INTERVAL"
      BuiltinIZero                             -> "IZERO"
      BuiltinIOne                              -> "IONE"
      BuiltinPartial                           -> "PARTIAL"
      BuiltinPartialP                          -> "PARTIALP"
      BuiltinIsOne                             -> "ISONE"
      BuiltinItIsOne                           -> "ITISONE"
      BuiltinEquiv                             -> "EQUIV"
      BuiltinEquivFun                          -> "EQUIVFUN"
      BuiltinEquivProof                        -> "EQUIVPROOF"
      BuiltinTranspProof                       -> "TRANSPPROOF"
      BuiltinIsOne1                            -> "ISONE1"
      BuiltinIsOne2                            -> "ISONE2"
      BuiltinIsOneEmpty                        -> "ISONEEMPTY"
      BuiltinSub                               -> "SUB"
      BuiltinSubIn                             -> "SUBIN"
      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"
      BuiltinProp                              -> "PROP"
      BuiltinSet                               -> "TYPE"
      BuiltinStrictSet                         -> "STRICTSET"
      BuiltinPropOmega                         -> "PROPOMEGA"
      BuiltinSetOmega                          -> "SETOMEGA"
      BuiltinSSetOmega                         -> "STRICTSETOMEGA"
      BuiltinLevelUniv                         -> "LEVELUNIV"
      BuiltinFromNat                           -> "FROMNAT"
      BuiltinFromNeg                           -> "FROMNEG"
      BuiltinFromString                        -> "FROMSTRING"
      BuiltinQName                             -> "QNAME"
      BuiltinAgdaSort                          -> "AGDASORT"
      BuiltinAgdaSortSet                       -> "AGDASORTSET"
      BuiltinAgdaSortLit                       -> "AGDASORTLIT"
      BuiltinAgdaSortProp                      -> "AGDASORTPROP"
      BuiltinAgdaSortPropLit                   -> "AGDASORTPROPLIT"
      BuiltinAgdaSortInf                       -> "AGDASORTINF"
      BuiltinAgdaSortUnsupported               -> "AGDASORTUNSUPPORTED"
      BuiltinHiding                            -> "HIDING"
      BuiltinHidden                            -> "HIDDEN"
      BuiltinInstance                          -> "INSTANCE"
      BuiltinVisible                           -> "VISIBLE"
      BuiltinRelevance                         -> "RELEVANCE"
      BuiltinRelevant                          -> "RELEVANT"
      BuiltinIrrelevant                        -> "IRRELEVANT"
      BuiltinQuantity                          -> "QUANTITY"
      BuiltinQuantity0                         -> "QUANTITY-0"
      BuiltinQuantityω                         -> "QUANTITY-ω"
      BuiltinModality                          -> "MODALITY"
      BuiltinModalityConstructor               -> "MODALITY-CONSTRUCTOR"
      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"
      BuiltinAgdaErrorPartPatt                 -> "AGDAERRORPARTPATT"
      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"
      BuiltinAgdaTCMDeclareData                -> "AGDATCMDECLAREDATA"
      BuiltinAgdaTCMDefineData                 -> "AGDATCMDEFINEDATA"
      BuiltinAgdaTCMDefineFun                  -> "AGDATCMDEFINEFUN"
      BuiltinAgdaTCMGetType                    -> "AGDATCMGETTYPE"
      BuiltinAgdaTCMGetDefinition              -> "AGDATCMGETDEFINITION"
      BuiltinAgdaTCMBlock                      -> "AGDATCMBLOCK"
      BuiltinAgdaTCMCommit                     -> "AGDATCMCOMMIT"
      BuiltinAgdaTCMQuoteTerm                  -> "AGDATCMQUOTETERM"
      BuiltinAgdaTCMUnquoteTerm                -> "AGDATCMUNQUOTETERM"
      BuiltinAgdaTCMQuoteOmegaTerm             -> "AGDATCMQUOTEOMEGATERM"
      BuiltinAgdaTCMIsMacro                    -> "AGDATCMISMACRO"
      BuiltinAgdaTCMWithNormalisation          -> "AGDATCMWITHNORMALISATION"
      BuiltinAgdaTCMWithReconstructed          -> "AGDATCMWITHRECONSTRUCTED"
      BuiltinAgdaTCMWithExpandLast             -> "AGDATCMWITHEXPANDLAST"
      BuiltinAgdaTCMWithReduceDefs             -> "AGDATCMWITHREDUCEDEFS"
      BuiltinAgdaTCMAskNormalisation           -> "AGDATCMASKNORMALISATION"
      BuiltinAgdaTCMAskReconstructed           -> "AGDATCMASKRECONSTRUCTED"
      BuiltinAgdaTCMAskExpandLast              -> "AGDATCMASKEXPANDLAST"
      BuiltinAgdaTCMAskReduceDefs              -> "AGDATCMASKREDUCEDEFS"
      BuiltinAgdaTCMFormatErrorParts           -> "AGDATCMFORMATERRORPARTS"
      BuiltinAgdaTCMDebugPrint                 -> "AGDATCMDEBUGPRINT"
      BuiltinAgdaTCMNoConstraints              -> "AGDATCMNOCONSTRAINTS"
      BuiltinAgdaTCMWorkOnTypes                -> "AGDATCMWORKONTYPES"
      BuiltinAgdaTCMRunSpeculative             -> "AGDATCMRUNSPECULATIVE"
      BuiltinAgdaTCMExec                       -> "AGDATCMEXEC"
      BuiltinAgdaTCMCheckFromString            -> "AGDATCMCHECKFROMSTRING"
      BuiltinAgdaTCMGetInstances               -> "AGDATCMGETINSTANCES"
      BuiltinAgdaTCMSolveInstances             -> "AGDATCMSOLVEINSTANCES"
      BuiltinAgdaTCMPragmaForeign              -> "AGDATCMPRAGMAFOREIGN"
      BuiltinAgdaTCMPragmaCompile              -> "AGDATCMPRAGMACOMPILE"
      BuiltinAgdaBlocker                       -> "AGDABLOCKER"
      BuiltinAgdaBlockerAny                    -> "AGDABLOCKERANY"
      BuiltinAgdaBlockerAll                    -> "AGDABLOCKERALL"
      BuiltinAgdaBlockerMeta                   -> "AGDABLOCKERMETA"
  
  -- | 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.
  isBuiltinNoDef :: BuiltinId -> Bool
  isBuiltinNoDef = hasElem builtinsNoDef
  
  builtinsNoDef :: [BuiltinId]
  builtinsNoDef =
    sizeBuiltins ++
     -- builtinConId,
    [ builtinIntervalUniv
    , builtinInterval
    , builtinPartial
    , builtinPartialP
    , builtinIsOne
    , builtinSub
    , builtinIZero
    , builtinIOne
    , builtinProp
    , builtinSet
    , builtinStrictSet
    , builtinPropOmega
    , builtinSetOmega
    , builtinSSetOmega
    , builtinLevelUniv
    ]
  
  sizeBuiltins :: [BuiltinId]
  sizeBuiltins =
    [ builtinSizeUniv
    , builtinSize
    , builtinSizeLt
    , builtinSizeSuc
    , builtinSizeInf
    , builtinSizeMax
    ]
  
  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,
    builtinMaybe, builtinNothing, builtinJust,
    builtinPath, builtinPathP, builtinInterval, builtinIZero, builtinIOne, builtinPartial, builtinPartialP,
    builtinIsOne,  builtinItIsOne, builtinIsOne1, builtinIsOne2, builtinIsOneEmpty,
    builtinSub, builtinSubIn,
    builtinEquiv, builtinEquivFun, builtinEquivProof,
    builtinTranspProof,
    builtinSizeUniv, builtinSize, builtinSizeLt,
    builtinSizeSuc, builtinSizeInf, builtinSizeMax,
    builtinInf, builtinSharp, builtinFlat,
    builtinEquality, builtinRefl, builtinRewrite, builtinLevelMax,
    builtinLevel, builtinLevelZero, builtinLevelSuc,
    builtinProp, builtinSet, builtinStrictSet,
    builtinPropOmega, builtinSetOmega, builtinSSetOmega,
    builtinLevelUniv,
    builtinIntervalUniv,
    builtinFromNat, builtinFromNeg, builtinFromString,
    builtinQName, builtinAgdaSort, builtinAgdaSortSet, builtinAgdaSortLit,
    builtinAgdaSortProp, builtinAgdaSortPropLit, builtinAgdaSortInf,
    builtinAgdaSortUnsupported,
    builtinHiding, builtinHidden, builtinInstance, builtinVisible,
    builtinRelevance, builtinRelevant, builtinIrrelevant,
    builtinQuantity, builtinQuantity0, builtinQuantityω,
    builtinModality, builtinModalityConstructor,
    builtinAssoc, builtinAssocLeft, builtinAssocRight, builtinAssocNon,
    builtinPrecedence, builtinPrecRelated, builtinPrecUnrelated,
    builtinFixity, builtinFixityFixity,
    builtinArgInfo, builtinArgArgInfo,
    builtinArg, builtinArgArg,
    builtinAbs, builtinAbsAbs, builtinAgdaTerm,
    builtinAgdaTermVar, builtinAgdaTermLam, builtinAgdaTermExtLam,
    builtinAgdaTermDef, builtinAgdaTermCon, builtinAgdaTermPi,
    builtinAgdaTermSort, builtinAgdaTermLit, builtinAgdaTermUnsupported, builtinAgdaTermMeta,
    builtinAgdaErrorPart, builtinAgdaErrorPartString, builtinAgdaErrorPartTerm, builtinAgdaErrorPartPatt, 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, builtinAgdaTCMDeclareData, builtinAgdaTCMDefineData, builtinAgdaTCMDefineFun,
    builtinAgdaTCMGetType, builtinAgdaTCMGetDefinition,
    builtinAgdaTCMQuoteTerm, builtinAgdaTCMUnquoteTerm, builtinAgdaTCMQuoteOmegaTerm,
    builtinAgdaTCMCommit, builtinAgdaTCMIsMacro, builtinAgdaTCMBlock,
    builtinAgdaBlocker, builtinAgdaBlockerAll, builtinAgdaBlockerAny, builtinAgdaBlockerMeta,
    builtinAgdaTCMFormatErrorParts, builtinAgdaTCMDebugPrint,
    builtinAgdaTCMWithNormalisation, builtinAgdaTCMWithReconstructed,
    builtinAgdaTCMWithExpandLast, builtinAgdaTCMWithReduceDefs,
    builtinAgdaTCMAskNormalisation, builtinAgdaTCMAskReconstructed,
    builtinAgdaTCMAskExpandLast, builtinAgdaTCMAskReduceDefs,
    builtinAgdaTCMNoConstraints,
    builtinAgdaTCMWorkOnTypes,
    builtinAgdaTCMRunSpeculative,
    builtinAgdaTCMExec,
    builtinAgdaTCMCheckFromString,
    builtinAgdaTCMGetInstances,
    builtinAgdaTCMSolveInstances,
    builtinAgdaTCMPragmaForeign,
    builtinAgdaTCMPragmaCompile
    :: BuiltinId
  
  builtinNat                               = BuiltinNat
  builtinSuc                               = BuiltinSuc
  builtinZero                              = BuiltinZero
  builtinNatPlus                           = BuiltinNatPlus
  builtinNatMinus                          = BuiltinNatMinus
  builtinNatTimes                          = BuiltinNatTimes
  builtinNatDivSucAux                      = BuiltinNatDivSucAux
  builtinNatModSucAux                      = BuiltinNatModSucAux
  builtinNatEquals                         = BuiltinNatEquals
  builtinNatLess                           = BuiltinNatLess
  builtinWord64                            = BuiltinWord64
  builtinInteger                           = BuiltinInteger
  builtinIntegerPos                        = BuiltinIntegerPos
  builtinIntegerNegSuc                     = BuiltinIntegerNegSuc
  builtinFloat                             = BuiltinFloat
  builtinChar                              = BuiltinChar
  builtinString                            = BuiltinString
  builtinUnit                              = BuiltinUnit
  builtinUnitUnit                          = BuiltinUnitUnit
  builtinSigma                             = BuiltinSigma
  builtinBool                              = BuiltinBool
  builtinTrue                              = BuiltinTrue
  builtinFalse                             = BuiltinFalse
  builtinList                              = BuiltinList
  builtinNil                               = BuiltinNil
  builtinCons                              = BuiltinCons
  builtinMaybe                             = BuiltinMaybe
  builtinNothing                           = BuiltinNothing
  builtinJust                              = BuiltinJust
  builtinIO                                = BuiltinIO
  builtinPath                              = BuiltinPath
  builtinPathP                             = BuiltinPathP
  builtinIntervalUniv                      = BuiltinIntervalUniv
  builtinInterval                          = BuiltinInterval
  builtinIZero                             = BuiltinIZero
  builtinIOne                              = BuiltinIOne
  builtinPartial                           = BuiltinPartial
  builtinPartialP                          = BuiltinPartialP
  builtinIsOne                             = BuiltinIsOne
  builtinItIsOne                           = BuiltinItIsOne
  builtinEquiv                             = BuiltinEquiv
  builtinEquivFun                          = BuiltinEquivFun
  builtinEquivProof                        = BuiltinEquivProof
  builtinTranspProof                       = BuiltinTranspProof
  builtinIsOne1                            = BuiltinIsOne1
  builtinIsOne2                            = BuiltinIsOne2
  builtinIsOneEmpty                        = BuiltinIsOneEmpty
  builtinSub                               = BuiltinSub
  builtinSubIn                             = BuiltinSubIn
  builtinSizeUniv                          = BuiltinSizeUniv
  builtinSize                              = BuiltinSize
  builtinSizeLt                            = BuiltinSizeLt
  builtinSizeSuc                           = BuiltinSizeSuc
  builtinSizeInf                           = BuiltinSizeInf
  builtinSizeMax                           = BuiltinSizeMax
  builtinInf                               = BuiltinInf
  builtinSharp                             = BuiltinSharp
  builtinFlat                              = BuiltinFlat
  builtinEquality                          = BuiltinEquality
  builtinRefl                              = BuiltinRefl
  builtinRewrite                           = BuiltinRewrite
  builtinLevelMax                          = BuiltinLevelMax
  builtinLevel                             = BuiltinLevel
  builtinLevelZero                         = BuiltinLevelZero
  builtinLevelSuc                          = BuiltinLevelSuc
  builtinProp                              = BuiltinProp
  builtinSet                               = BuiltinSet
  builtinStrictSet                         = BuiltinStrictSet
  builtinPropOmega                         = BuiltinPropOmega
  builtinSetOmega                          = BuiltinSetOmega
  builtinSSetOmega                         = BuiltinSSetOmega
  builtinLevelUniv                         = BuiltinLevelUniv
  builtinFromNat                           = BuiltinFromNat
  builtinFromNeg                           = BuiltinFromNeg
  builtinFromString                        = BuiltinFromString
  builtinQName                             = BuiltinQName
  builtinAgdaSort                          = BuiltinAgdaSort
  builtinAgdaSortSet                       = BuiltinAgdaSortSet
  builtinAgdaSortLit                       = BuiltinAgdaSortLit
  builtinAgdaSortProp                      = BuiltinAgdaSortProp
  builtinAgdaSortPropLit                   = BuiltinAgdaSortPropLit
  builtinAgdaSortInf                       = BuiltinAgdaSortInf
  builtinAgdaSortUnsupported               = BuiltinAgdaSortUnsupported
  builtinHiding                            = BuiltinHiding
  builtinHidden                            = BuiltinHidden
  builtinInstance                          = BuiltinInstance
  builtinVisible                           = BuiltinVisible
  builtinRelevance                         = BuiltinRelevance
  builtinRelevant                          = BuiltinRelevant
  builtinIrrelevant                        = BuiltinIrrelevant
  builtinQuantity                          = BuiltinQuantity
  builtinQuantity0                         = BuiltinQuantity0
  builtinQuantityω                         = BuiltinQuantityω
  builtinModality                          = BuiltinModality
  builtinModalityConstructor               = BuiltinModalityConstructor
  builtinAssoc                             = BuiltinAssoc
  builtinAssocLeft                         = BuiltinAssocLeft
  builtinAssocRight                        = BuiltinAssocRight
  builtinAssocNon                          = BuiltinAssocNon
  builtinPrecedence                        = BuiltinPrecedence
  builtinPrecRelated                       = BuiltinPrecRelated
  builtinPrecUnrelated                     = BuiltinPrecUnrelated
  builtinFixity                            = BuiltinFixity
  builtinFixityFixity                      = BuiltinFixityFixity
  builtinArg                               = BuiltinArg
  builtinArgInfo                           = BuiltinArgInfo
  builtinArgArgInfo                        = BuiltinArgArgInfo
  builtinArgArg                            = BuiltinArgArg
  builtinAbs                               = BuiltinAbs
  builtinAbsAbs                            = BuiltinAbsAbs
  builtinAgdaTerm                          = BuiltinAgdaTerm
  builtinAgdaTermVar                       = BuiltinAgdaTermVar
  builtinAgdaTermLam                       = BuiltinAgdaTermLam
  builtinAgdaTermExtLam                    = BuiltinAgdaTermExtLam
  builtinAgdaTermDef                       = BuiltinAgdaTermDef
  builtinAgdaTermCon                       = BuiltinAgdaTermCon
  builtinAgdaTermPi                        = BuiltinAgdaTermPi
  builtinAgdaTermSort                      = BuiltinAgdaTermSort
  builtinAgdaTermLit                       = BuiltinAgdaTermLit
  builtinAgdaTermUnsupported               = BuiltinAgdaTermUnsupported
  builtinAgdaTermMeta                      = BuiltinAgdaTermMeta
  builtinAgdaErrorPart                     = BuiltinAgdaErrorPart
  builtinAgdaErrorPartString               = BuiltinAgdaErrorPartString
  builtinAgdaErrorPartTerm                 = BuiltinAgdaErrorPartTerm
  builtinAgdaErrorPartPatt                 = BuiltinAgdaErrorPartPatt
  builtinAgdaErrorPartName                 = BuiltinAgdaErrorPartName
  builtinAgdaLiteral                       = BuiltinAgdaLiteral
  builtinAgdaLitNat                        = BuiltinAgdaLitNat
  builtinAgdaLitWord64                     = BuiltinAgdaLitWord64
  builtinAgdaLitFloat                      = BuiltinAgdaLitFloat
  builtinAgdaLitChar                       = BuiltinAgdaLitChar
  builtinAgdaLitString                     = BuiltinAgdaLitString
  builtinAgdaLitQName                      = BuiltinAgdaLitQName
  builtinAgdaLitMeta                       = BuiltinAgdaLitMeta
  builtinAgdaClause                        = BuiltinAgdaClause
  builtinAgdaClauseClause                  = BuiltinAgdaClauseClause
  builtinAgdaClauseAbsurd                  = BuiltinAgdaClauseAbsurd
  builtinAgdaPattern                       = BuiltinAgdaPattern
  builtinAgdaPatVar                        = BuiltinAgdaPatVar
  builtinAgdaPatCon                        = BuiltinAgdaPatCon
  builtinAgdaPatDot                        = BuiltinAgdaPatDot
  builtinAgdaPatLit                        = BuiltinAgdaPatLit
  builtinAgdaPatProj                       = BuiltinAgdaPatProj
  builtinAgdaPatAbsurd                     = BuiltinAgdaPatAbsurd
  builtinAgdaDefinitionFunDef              = BuiltinAgdaDefinitionFunDef
  builtinAgdaDefinitionDataDef             = BuiltinAgdaDefinitionDataDef
  builtinAgdaDefinitionRecordDef           = BuiltinAgdaDefinitionRecordDef
  builtinAgdaDefinitionDataConstructor     = BuiltinAgdaDefinitionDataConstructor
  builtinAgdaDefinitionPostulate           = BuiltinAgdaDefinitionPostulate
  builtinAgdaDefinitionPrimitive           = BuiltinAgdaDefinitionPrimitive
  builtinAgdaDefinition                    = BuiltinAgdaDefinition
  builtinAgdaMeta                          = BuiltinAgdaMeta
  builtinAgdaTCM                           = BuiltinAgdaTCM
  builtinAgdaTCMReturn                     = BuiltinAgdaTCMReturn
  builtinAgdaTCMBind                       = BuiltinAgdaTCMBind
  builtinAgdaTCMUnify                      = BuiltinAgdaTCMUnify
  builtinAgdaTCMTypeError                  = BuiltinAgdaTCMTypeError
  builtinAgdaTCMInferType                  = BuiltinAgdaTCMInferType
  builtinAgdaTCMCheckType                  = BuiltinAgdaTCMCheckType
  builtinAgdaTCMNormalise                  = BuiltinAgdaTCMNormalise
  builtinAgdaTCMReduce                     = BuiltinAgdaTCMReduce
  builtinAgdaTCMCatchError                 = BuiltinAgdaTCMCatchError
  builtinAgdaTCMGetContext                 = BuiltinAgdaTCMGetContext
  builtinAgdaTCMExtendContext              = BuiltinAgdaTCMExtendContext
  builtinAgdaTCMInContext                  = BuiltinAgdaTCMInContext
  builtinAgdaTCMFreshName                  = BuiltinAgdaTCMFreshName
  builtinAgdaTCMDeclareDef                 = BuiltinAgdaTCMDeclareDef
  builtinAgdaTCMDeclarePostulate           = BuiltinAgdaTCMDeclarePostulate
  builtinAgdaTCMDeclareData                = BuiltinAgdaTCMDeclareData
  builtinAgdaTCMDefineData                 = BuiltinAgdaTCMDefineData
  builtinAgdaTCMDefineFun                  = BuiltinAgdaTCMDefineFun
  builtinAgdaTCMGetType                    = BuiltinAgdaTCMGetType
  builtinAgdaTCMGetDefinition              = BuiltinAgdaTCMGetDefinition
  builtinAgdaTCMBlock                      = BuiltinAgdaTCMBlock
  builtinAgdaTCMCommit                     = BuiltinAgdaTCMCommit
  builtinAgdaTCMQuoteTerm                  = BuiltinAgdaTCMQuoteTerm
  builtinAgdaTCMUnquoteTerm                = BuiltinAgdaTCMUnquoteTerm
  builtinAgdaTCMQuoteOmegaTerm             = BuiltinAgdaTCMQuoteOmegaTerm
  builtinAgdaTCMIsMacro                    = BuiltinAgdaTCMIsMacro
  builtinAgdaTCMWithNormalisation          = BuiltinAgdaTCMWithNormalisation
  builtinAgdaTCMWithReconstructed          = BuiltinAgdaTCMWithReconstructed
  builtinAgdaTCMWithExpandLast             = BuiltinAgdaTCMWithExpandLast
  builtinAgdaTCMWithReduceDefs             = BuiltinAgdaTCMWithReduceDefs
  builtinAgdaTCMAskNormalisation           = BuiltinAgdaTCMAskNormalisation
  builtinAgdaTCMAskReconstructed           = BuiltinAgdaTCMAskReconstructed
  builtinAgdaTCMAskExpandLast              = BuiltinAgdaTCMAskExpandLast
  builtinAgdaTCMAskReduceDefs              = BuiltinAgdaTCMAskReduceDefs
  builtinAgdaTCMFormatErrorParts           = BuiltinAgdaTCMFormatErrorParts
  builtinAgdaTCMDebugPrint                 = BuiltinAgdaTCMDebugPrint
  builtinAgdaTCMNoConstraints              = BuiltinAgdaTCMNoConstraints
  builtinAgdaTCMWorkOnTypes                = BuiltinAgdaTCMWorkOnTypes
  builtinAgdaTCMRunSpeculative             = BuiltinAgdaTCMRunSpeculative
  builtinAgdaTCMExec                       = BuiltinAgdaTCMExec
  builtinAgdaTCMCheckFromString            = BuiltinAgdaTCMCheckFromString
  builtinAgdaTCMGetInstances               = BuiltinAgdaTCMGetInstances
  builtinAgdaTCMSolveInstances             = BuiltinAgdaTCMSolveInstances
  builtinAgdaTCMPragmaForeign              = BuiltinAgdaTCMPragmaForeign
  builtinAgdaTCMPragmaCompile              = BuiltinAgdaTCMPragmaCompile
  builtinAgdaBlocker                       = BuiltinAgdaBlocker
  builtinAgdaBlockerAny                    = BuiltinAgdaBlockerAny
  builtinAgdaBlockerAll                    = BuiltinAgdaBlockerAll
  builtinAgdaBlockerMeta                   = BuiltinAgdaBlockerMeta
  
  -- | Lookup a builtin by the string used in the @BUILTIN@ pragma.
  builtinById :: String -> Maybe BuiltinId
  builtinById = flip M.lookup m where
    m = M.fromList [(getBuiltinId x, x) | x <- [(minBound :: BuiltinId)..]]
  
  -- * Primitives
  
  -- | A primitive name, defined by the @primitive@ block.
  data PrimitiveId
    -- Cubical
    = PrimIMin
    | PrimIMax
    | PrimINeg
    | PrimPartial
    | PrimPartialP
    | PrimSubOut
    | PrimGlue
    | Prim_glue
    | Prim_unglue
    | Prim_glueU
    | Prim_unglueU
    | PrimFaceForall
    | PrimComp
    | PrimPOr
    | PrimTrans
    | PrimHComp
    --  Integer
    | PrimShowInteger
    -- Natural
    | PrimNatPlus
    | PrimNatMinus
    | PrimNatTimes
    | PrimNatDivSucAux
    | PrimNatModSucAux
    | PrimNatEquality
    | PrimNatLess
    | PrimShowNat
    -- Word64
    | PrimWord64FromNat
    | PrimWord64ToNat
    | PrimWord64ToNatInjective
    -- Level
    | PrimLevelZero
    | PrimLevelSuc
    | PrimLevelMax
    -- Float
    | PrimFloatEquality
    | PrimFloatInequality
    | PrimFloatLess
    | PrimFloatIsInfinite
    | PrimFloatIsNaN
    | PrimFloatIsNegativeZero
    | PrimFloatIsSafeInteger
    | PrimFloatToWord64
    | PrimFloatToWord64Injective
    | PrimNatToFloat
    | PrimIntToFloat
    | PrimFloatRound
    | PrimFloatFloor
    | PrimFloatCeiling
    | PrimFloatToRatio
    | PrimRatioToFloat
    | PrimFloatDecode
    | PrimFloatEncode
    | PrimShowFloat
    | PrimFloatPlus
    | PrimFloatMinus
    | PrimFloatTimes
    | PrimFloatNegate
    | PrimFloatDiv
    | PrimFloatPow
    | PrimFloatSqrt
    | PrimFloatExp
    | PrimFloatLog
    | PrimFloatSin
    | PrimFloatCos
    | PrimFloatTan
    | PrimFloatASin
    | PrimFloatACos
    | PrimFloatATan
    | PrimFloatATan2
    | PrimFloatSinh
    | PrimFloatCosh
    | PrimFloatTanh
    | PrimFloatASinh
    | PrimFloatACosh
    | PrimFloatATanh
    -- Character
    | PrimCharEquality
    | PrimIsLower
    | PrimIsDigit
    | PrimIsAlpha
    | PrimIsSpace
    | PrimIsAscii
    | PrimIsLatin1
    | PrimIsPrint
    | PrimIsHexDigit
    | PrimToUpper
    | PrimToLower
    | PrimCharToNat
    | PrimCharToNatInjective
    | PrimNatToChar
    | PrimShowChar
    -- String
    | PrimStringToList
    | PrimStringToListInjective
    | PrimStringFromList
    | PrimStringFromListInjective
    | PrimStringAppend
    | PrimStringEquality
    | PrimShowString
    | PrimStringUncons
    -- "Other stuff"
    | PrimErase
    | PrimEraseEquality
    | PrimForce
    | PrimForceLemma
    | PrimQNameEquality
    | PrimQNameLess
    | PrimShowQName
    | PrimQNameFixity
    | PrimQNameToWord64s
    | PrimQNameToWord64sInjective
    | PrimMetaEquality
    | PrimMetaLess
    | PrimShowMeta
    | PrimMetaToNat
    | PrimMetaToNatInjective
    | PrimLockUniv
    deriving (Show, Eq, Ord, Bounded, Enum, Generic)
  
  instance NFData PrimitiveId
  
  instance Hashable PrimitiveId where
    s `hashWithSalt` b = s `hashWithSalt` fromEnum b
  
  instance KillRange PrimitiveId where
    killRange = id
  
  instance Pretty PrimitiveId where
    pretty = text . getBuiltinId
  
  instance IsBuiltin PrimitiveId where
    someBuiltin = PrimitiveName
  
    getBuiltinId = \case
      -- Cubical
      PrimIMin                              -> "primIMin"
      PrimIMax                              -> "primIMax"
      PrimINeg                              -> "primINeg"
      PrimPartial                           -> "primPartial"
      PrimPartialP                          -> "primPartialP"
      PrimSubOut                            -> "primSubOut"
      PrimGlue                              -> "primGlue"
      Prim_glue                             -> "prim^glue"
      Prim_unglue                           -> "prim^unglue"
      Prim_glueU                            -> "prim^glueU"
      Prim_unglueU                          -> "prim^unglueU"
      PrimFaceForall                        -> "primFaceForall"
      PrimComp                              -> "primComp"
      PrimPOr                               -> "primPOr"
      PrimTrans                             -> "primTransp"
      PrimHComp                             -> "primHComp"
      --  Integer
      PrimShowInteger                       -> "primShowInteger"
      -- Natural
      PrimNatPlus                           -> "primNatPlus"
      PrimNatMinus                          -> "primNatMinus"
      PrimNatTimes                          -> "primNatTimes"
      PrimNatDivSucAux                      -> "primNatDivSucAux"
      PrimNatModSucAux                      -> "primNatModSucAux"
      PrimNatEquality                       -> "primNatEquality"
      PrimNatLess                           -> "primNatLess"
      PrimShowNat                           -> "primShowNat"
      -- Word64
      PrimWord64FromNat                     -> "primWord64FromNat"
      PrimWord64ToNat                       -> "primWord64ToNat"
      PrimWord64ToNatInjective              -> "primWord64ToNatInjective"
      -- Level
      PrimLevelZero                         -> "primLevelZero"
      PrimLevelSuc                          -> "primLevelSuc"
      PrimLevelMax                          -> "primLevelMax"
      -- Float
      PrimFloatEquality                     -> "primFloatEquality"
      PrimFloatInequality                   -> "primFloatInequality"
      PrimFloatLess                         -> "primFloatLess"
      PrimFloatIsInfinite                   -> "primFloatIsInfinite"
      PrimFloatIsNaN                        -> "primFloatIsNaN"
      PrimFloatIsNegativeZero               -> "primFloatIsNegativeZero"
      PrimFloatIsSafeInteger                -> "primFloatIsSafeInteger"
      PrimFloatToWord64                     -> "primFloatToWord64"
      PrimFloatToWord64Injective            -> "primFloatToWord64Injective"
      PrimNatToFloat                        -> "primNatToFloat"
      PrimIntToFloat                        -> "primIntToFloat"
      PrimFloatRound                        -> "primFloatRound"
      PrimFloatFloor                        -> "primFloatFloor"
      PrimFloatCeiling                      -> "primFloatCeiling"
      PrimFloatToRatio                      -> "primFloatToRatio"
      PrimRatioToFloat                      -> "primRatioToFloat"
      PrimFloatDecode                       -> "primFloatDecode"
      PrimFloatEncode                       -> "primFloatEncode"
      PrimShowFloat                         -> "primShowFloat"
      PrimFloatPlus                         -> "primFloatPlus"
      PrimFloatMinus                        -> "primFloatMinus"
      PrimFloatTimes                        -> "primFloatTimes"
      PrimFloatNegate                       -> "primFloatNegate"
      PrimFloatDiv                          -> "primFloatDiv"
      PrimFloatPow                          -> "primFloatPow"
      PrimFloatSqrt                         -> "primFloatSqrt"
      PrimFloatExp                          -> "primFloatExp"
      PrimFloatLog                          -> "primFloatLog"
      PrimFloatSin                          -> "primFloatSin"
      PrimFloatCos                          -> "primFloatCos"
      PrimFloatTan                          -> "primFloatTan"
      PrimFloatASin                         -> "primFloatASin"
      PrimFloatACos                         -> "primFloatACos"
      PrimFloatATan                         -> "primFloatATan"
      PrimFloatATan2                        -> "primFloatATan2"
      PrimFloatSinh                         -> "primFloatSinh"
      PrimFloatCosh                         -> "primFloatCosh"
      PrimFloatTanh                         -> "primFloatTanh"
      PrimFloatASinh                        -> "primFloatASinh"
      PrimFloatACosh                        -> "primFloatACosh"
      PrimFloatATanh                        -> "primFloatATanh"
      -- Character
      PrimCharEquality                      -> "primCharEquality"
      PrimIsLower                           -> "primIsLower"
      PrimIsDigit                           -> "primIsDigit"
      PrimIsAlpha                           -> "primIsAlpha"
      PrimIsSpace                           -> "primIsSpace"
      PrimIsAscii                           -> "primIsAscii"
      PrimIsLatin1                          -> "primIsLatin1"
      PrimIsPrint                           -> "primIsPrint"
      PrimIsHexDigit                        -> "primIsHexDigit"
      PrimToUpper                           -> "primToUpper"
      PrimToLower                           -> "primToLower"
      PrimCharToNat                         -> "primCharToNat"
      PrimCharToNatInjective                -> "primCharToNatInjective"
      PrimNatToChar                         -> "primNatToChar"
      PrimShowChar                          -> "primShowChar"
      -- String
      PrimStringToList                      -> "primStringToList"
      PrimStringToListInjective             -> "primStringToListInjective"
      PrimStringFromList                    -> "primStringFromList"
      PrimStringFromListInjective           -> "primStringFromListInjective"
      PrimStringAppend                      -> "primStringAppend"
      PrimStringEquality                    -> "primStringEquality"
      PrimShowString                        -> "primShowString"
      PrimStringUncons                      -> "primStringUncons"
      -- "Other stuff"
      PrimErase                             -> "primErase"
      PrimEraseEquality                     -> "primEraseEquality"
      PrimForce                             -> "primForce"
      PrimForceLemma                        -> "primForceLemma"
      PrimQNameEquality                     -> "primQNameEquality"
      PrimQNameLess                         -> "primQNameLess"
      PrimShowQName                         -> "primShowQName"
      PrimQNameFixity                       -> "primQNameFixity"
      PrimQNameToWord64s                    -> "primQNameToWord64s"
      PrimQNameToWord64sInjective           -> "primQNameToWord64sInjective"
      PrimMetaEquality                      -> "primMetaEquality"
      PrimMetaLess                          -> "primMetaLess"
      PrimShowMeta                          -> "primShowMeta"
      PrimMetaToNat                         -> "primMetaToNat"
      PrimMetaToNatInjective                -> "primMetaToNatInjective"
      PrimLockUniv                          -> "primLockUniv"
  
  builtinSubOut,
    builtinIMin, builtinIMax, builtinINeg,
    builtinGlue, builtin_glue, builtin_unglue, builtin_glueU, builtin_unglueU,
    builtinFaceForall, builtinComp, builtinPOr,
    builtinTrans,  builtinHComp, builtinLockUniv
    :: PrimitiveId
  builtinIMin                              = PrimIMin
  builtinIMax                              = PrimIMax
  builtinINeg                              = PrimINeg
  builtinSubOut                            = PrimSubOut
  builtinGlue                              = PrimGlue
  builtin_glue                             = Prim_glue
  builtin_unglue                           = Prim_unglue
  builtin_glueU                            = Prim_glueU
  builtin_unglueU                          = Prim_unglueU
  builtinFaceForall                        = PrimFaceForall
  builtinComp                              = PrimComp
  builtinPOr                               = PrimPOr
  builtinTrans                             = PrimTrans
  builtinHComp                             = PrimHComp
  builtinLockUniv                          = PrimLockUniv
  
  -- | Lookup a primitive by its identifier.
  primitiveById :: String -> Maybe PrimitiveId
  primitiveById = flip M.lookup m where
    m = M.fromList [(getBuiltinId x, x) | x <- [(minBound :: PrimitiveId)..]]
  