{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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 (Int -> SomeBuiltin -> ShowS
[SomeBuiltin] -> ShowS
SomeBuiltin -> String
(Int -> SomeBuiltin -> ShowS)
-> (SomeBuiltin -> String)
-> ([SomeBuiltin] -> ShowS)
-> Show SomeBuiltin
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SomeBuiltin -> ShowS
showsPrec :: Int -> SomeBuiltin -> ShowS
$cshow :: SomeBuiltin -> String
show :: SomeBuiltin -> String
$cshowList :: [SomeBuiltin] -> ShowS
showList :: [SomeBuiltin] -> ShowS
Show, SomeBuiltin -> SomeBuiltin -> Bool
(SomeBuiltin -> SomeBuiltin -> Bool)
-> (SomeBuiltin -> SomeBuiltin -> Bool) -> Eq SomeBuiltin
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SomeBuiltin -> SomeBuiltin -> Bool
== :: SomeBuiltin -> SomeBuiltin -> Bool
$c/= :: SomeBuiltin -> SomeBuiltin -> Bool
/= :: SomeBuiltin -> SomeBuiltin -> Bool
Eq, Eq SomeBuiltin
Eq SomeBuiltin =>
(SomeBuiltin -> SomeBuiltin -> Ordering)
-> (SomeBuiltin -> SomeBuiltin -> Bool)
-> (SomeBuiltin -> SomeBuiltin -> Bool)
-> (SomeBuiltin -> SomeBuiltin -> Bool)
-> (SomeBuiltin -> SomeBuiltin -> Bool)
-> (SomeBuiltin -> SomeBuiltin -> SomeBuiltin)
-> (SomeBuiltin -> SomeBuiltin -> SomeBuiltin)
-> Ord SomeBuiltin
SomeBuiltin -> SomeBuiltin -> Bool
SomeBuiltin -> SomeBuiltin -> Ordering
SomeBuiltin -> SomeBuiltin -> SomeBuiltin
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SomeBuiltin -> SomeBuiltin -> Ordering
compare :: SomeBuiltin -> SomeBuiltin -> Ordering
$c< :: SomeBuiltin -> SomeBuiltin -> Bool
< :: SomeBuiltin -> SomeBuiltin -> Bool
$c<= :: SomeBuiltin -> SomeBuiltin -> Bool
<= :: SomeBuiltin -> SomeBuiltin -> Bool
$c> :: SomeBuiltin -> SomeBuiltin -> Bool
> :: SomeBuiltin -> SomeBuiltin -> Bool
$c>= :: SomeBuiltin -> SomeBuiltin -> Bool
>= :: SomeBuiltin -> SomeBuiltin -> Bool
$cmax :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin
max :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin
$cmin :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin
min :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin
Ord, (forall x. SomeBuiltin -> Rep SomeBuiltin x)
-> (forall x. Rep SomeBuiltin x -> SomeBuiltin)
-> Generic SomeBuiltin
forall x. Rep SomeBuiltin x -> SomeBuiltin
forall x. SomeBuiltin -> Rep SomeBuiltin x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SomeBuiltin -> Rep SomeBuiltin x
from :: forall x. SomeBuiltin -> Rep SomeBuiltin x
$cto :: forall x. Rep SomeBuiltin x -> SomeBuiltin
to :: forall x. Rep SomeBuiltin x -> SomeBuiltin
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 :: SomeBuiltin -> SomeBuiltin
someBuiltin = SomeBuiltin -> SomeBuiltin
forall a. a -> a
id

  getBuiltinId :: SomeBuiltin -> String
getBuiltinId (BuiltinName BuiltinId
x) = BuiltinId -> String
forall a. IsBuiltin a => a -> String
getBuiltinId BuiltinId
x
  getBuiltinId (PrimitiveName PrimitiveId
x) = PrimitiveId -> String
forall a. IsBuiltin a => a -> String
getBuiltinId PrimitiveId
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
  | BuiltinId
  | BuiltinReflId
  | 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
  | BuiltinAgdaTCMRunSpeculative
  | BuiltinAgdaTCMExec
  | BuiltinAgdaTCMGetInstances
  | BuiltinAgdaTCMPragmaForeign
  | BuiltinAgdaTCMPragmaCompile
  | BuiltinAgdaBlocker
  | BuiltinAgdaBlockerAny
  | BuiltinAgdaBlockerAll
  | BuiltinAgdaBlockerMeta
  deriving (Int -> BuiltinId -> ShowS
[BuiltinId] -> ShowS
BuiltinId -> String
(Int -> BuiltinId -> ShowS)
-> (BuiltinId -> String)
-> ([BuiltinId] -> ShowS)
-> Show BuiltinId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BuiltinId -> ShowS
showsPrec :: Int -> BuiltinId -> ShowS
$cshow :: BuiltinId -> String
show :: BuiltinId -> String
$cshowList :: [BuiltinId] -> ShowS
showList :: [BuiltinId] -> ShowS
Show, BuiltinId -> BuiltinId -> Bool
(BuiltinId -> BuiltinId -> Bool)
-> (BuiltinId -> BuiltinId -> Bool) -> Eq BuiltinId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BuiltinId -> BuiltinId -> Bool
== :: BuiltinId -> BuiltinId -> Bool
$c/= :: BuiltinId -> BuiltinId -> Bool
/= :: BuiltinId -> BuiltinId -> Bool
Eq, Eq BuiltinId
Eq BuiltinId =>
(BuiltinId -> BuiltinId -> Ordering)
-> (BuiltinId -> BuiltinId -> Bool)
-> (BuiltinId -> BuiltinId -> Bool)
-> (BuiltinId -> BuiltinId -> Bool)
-> (BuiltinId -> BuiltinId -> Bool)
-> (BuiltinId -> BuiltinId -> BuiltinId)
-> (BuiltinId -> BuiltinId -> BuiltinId)
-> Ord BuiltinId
BuiltinId -> BuiltinId -> Bool
BuiltinId -> BuiltinId -> Ordering
BuiltinId -> BuiltinId -> BuiltinId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BuiltinId -> BuiltinId -> Ordering
compare :: BuiltinId -> BuiltinId -> Ordering
$c< :: BuiltinId -> BuiltinId -> Bool
< :: BuiltinId -> BuiltinId -> Bool
$c<= :: BuiltinId -> BuiltinId -> Bool
<= :: BuiltinId -> BuiltinId -> Bool
$c> :: BuiltinId -> BuiltinId -> Bool
> :: BuiltinId -> BuiltinId -> Bool
$c>= :: BuiltinId -> BuiltinId -> Bool
>= :: BuiltinId -> BuiltinId -> Bool
$cmax :: BuiltinId -> BuiltinId -> BuiltinId
max :: BuiltinId -> BuiltinId -> BuiltinId
$cmin :: BuiltinId -> BuiltinId -> BuiltinId
min :: BuiltinId -> BuiltinId -> BuiltinId
Ord, BuiltinId
BuiltinId -> BuiltinId -> Bounded BuiltinId
forall a. a -> a -> Bounded a
$cminBound :: BuiltinId
minBound :: BuiltinId
$cmaxBound :: BuiltinId
maxBound :: BuiltinId
Bounded, Int -> BuiltinId
BuiltinId -> Int
BuiltinId -> [BuiltinId]
BuiltinId -> BuiltinId
BuiltinId -> BuiltinId -> [BuiltinId]
BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId]
(BuiltinId -> BuiltinId)
-> (BuiltinId -> BuiltinId)
-> (Int -> BuiltinId)
-> (BuiltinId -> Int)
-> (BuiltinId -> [BuiltinId])
-> (BuiltinId -> BuiltinId -> [BuiltinId])
-> (BuiltinId -> BuiltinId -> [BuiltinId])
-> (BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId])
-> Enum BuiltinId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: BuiltinId -> BuiltinId
succ :: BuiltinId -> BuiltinId
$cpred :: BuiltinId -> BuiltinId
pred :: BuiltinId -> BuiltinId
$ctoEnum :: Int -> BuiltinId
toEnum :: Int -> BuiltinId
$cfromEnum :: BuiltinId -> Int
fromEnum :: BuiltinId -> Int
$cenumFrom :: BuiltinId -> [BuiltinId]
enumFrom :: BuiltinId -> [BuiltinId]
$cenumFromThen :: BuiltinId -> BuiltinId -> [BuiltinId]
enumFromThen :: BuiltinId -> BuiltinId -> [BuiltinId]
$cenumFromTo :: BuiltinId -> BuiltinId -> [BuiltinId]
enumFromTo :: BuiltinId -> BuiltinId -> [BuiltinId]
$cenumFromThenTo :: BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId]
enumFromThenTo :: BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId]
Enum, (forall x. BuiltinId -> Rep BuiltinId x)
-> (forall x. Rep BuiltinId x -> BuiltinId) -> Generic BuiltinId
forall x. Rep BuiltinId x -> BuiltinId
forall x. BuiltinId -> Rep BuiltinId x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BuiltinId -> Rep BuiltinId x
from :: forall x. BuiltinId -> Rep BuiltinId x
$cto :: forall x. Rep BuiltinId x -> BuiltinId
to :: forall x. Rep BuiltinId x -> BuiltinId
Generic)

instance NFData BuiltinId

instance Hashable BuiltinId where
  Int
s hashWithSalt :: Int -> BuiltinId -> Int
`hashWithSalt` BuiltinId
b = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` BuiltinId -> Int
forall a. Enum a => a -> Int
fromEnum BuiltinId
b

instance KillRange BuiltinId where
  killRange :: BuiltinId -> BuiltinId
killRange = BuiltinId -> BuiltinId
forall a. a -> a
id

instance Pretty BuiltinId where
  pretty :: BuiltinId -> Doc
pretty = String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> (BuiltinId -> String) -> BuiltinId -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinId -> String
forall a. IsBuiltin a => a -> String
getBuiltinId

instance IsBuiltin BuiltinId where
  someBuiltin :: BuiltinId -> SomeBuiltin
someBuiltin = BuiltinId -> SomeBuiltin
BuiltinName

  getBuiltinId :: BuiltinId -> String
getBuiltinId = \case
    BuiltinId
BuiltinNat                               -> String
"NATURAL"
    BuiltinId
BuiltinSuc                               -> String
"SUC"
    BuiltinId
BuiltinZero                              -> String
"ZERO"
    BuiltinId
BuiltinNatPlus                           -> String
"NATPLUS"
    BuiltinId
BuiltinNatMinus                          -> String
"NATMINUS"
    BuiltinId
BuiltinNatTimes                          -> String
"NATTIMES"
    BuiltinId
BuiltinNatDivSucAux                      -> String
"NATDIVSUCAUX"
    BuiltinId
BuiltinNatModSucAux                      -> String
"NATMODSUCAUX"
    BuiltinId
BuiltinNatEquals                         -> String
"NATEQUALS"
    BuiltinId
BuiltinNatLess                           -> String
"NATLESS"
    BuiltinId
BuiltinWord64                            -> String
"WORD64"
    BuiltinId
BuiltinInteger                           -> String
"INTEGER"
    BuiltinId
BuiltinIntegerPos                        -> String
"INTEGERPOS"
    BuiltinId
BuiltinIntegerNegSuc                     -> String
"INTEGERNEGSUC"
    BuiltinId
BuiltinFloat                             -> String
"FLOAT"
    BuiltinId
BuiltinChar                              -> String
"CHAR"
    BuiltinId
BuiltinString                            -> String
"STRING"
    BuiltinId
BuiltinUnit                              -> String
"UNIT"
    BuiltinId
BuiltinUnitUnit                          -> String
"UNITUNIT"
    BuiltinId
BuiltinSigma                             -> String
"SIGMA"
    BuiltinId
BuiltinSigmaCon                          -> String
"SIGMACON"
    BuiltinId
BuiltinBool                              -> String
"BOOL"
    BuiltinId
BuiltinTrue                              -> String
"TRUE"
    BuiltinId
BuiltinFalse                             -> String
"FALSE"
    BuiltinId
BuiltinList                              -> String
"LIST"
    BuiltinId
BuiltinNil                               -> String
"NIL"
    BuiltinId
BuiltinCons                              -> String
"CONS"
    BuiltinId
BuiltinMaybe                             -> String
"MAYBE"
    BuiltinId
BuiltinNothing                           -> String
"NOTHING"
    BuiltinId
BuiltinJust                              -> String
"JUST"
    BuiltinId
BuiltinIO                                -> String
"IO"
    BuiltinId
BuiltinId                                -> String
"ID"
    BuiltinId
BuiltinReflId                            -> String
"REFLID"
    BuiltinId
BuiltinPath                              -> String
"PATH"
    BuiltinId
BuiltinPathP                             -> String
"PATHP"
    BuiltinId
BuiltinIntervalUniv                      -> String
"CUBEINTERVALUNIV"
    BuiltinId
BuiltinInterval                          -> String
"INTERVAL"
    BuiltinId
BuiltinIZero                             -> String
"IZERO"
    BuiltinId
BuiltinIOne                              -> String
"IONE"
    BuiltinId
BuiltinPartial                           -> String
"PARTIAL"
    BuiltinId
BuiltinPartialP                          -> String
"PARTIALP"
    BuiltinId
BuiltinIsOne                             -> String
"ISONE"
    BuiltinId
BuiltinItIsOne                           -> String
"ITISONE"
    BuiltinId
BuiltinEquiv                             -> String
"EQUIV"
    BuiltinId
BuiltinEquivFun                          -> String
"EQUIVFUN"
    BuiltinId
BuiltinEquivProof                        -> String
"EQUIVPROOF"
    BuiltinId
BuiltinTranspProof                       -> String
"TRANSPPROOF"
    BuiltinId
BuiltinIsOne1                            -> String
"ISONE1"
    BuiltinId
BuiltinIsOne2                            -> String
"ISONE2"
    BuiltinId
BuiltinIsOneEmpty                        -> String
"ISONEEMPTY"
    BuiltinId
BuiltinSub                               -> String
"SUB"
    BuiltinId
BuiltinSubIn                             -> String
"SUBIN"
    BuiltinId
BuiltinSizeUniv                          -> String
"SIZEUNIV"
    BuiltinId
BuiltinSize                              -> String
"SIZE"
    BuiltinId
BuiltinSizeLt                            -> String
"SIZELT"
    BuiltinId
BuiltinSizeSuc                           -> String
"SIZESUC"
    BuiltinId
BuiltinSizeInf                           -> String
"SIZEINF"
    BuiltinId
BuiltinSizeMax                           -> String
"SIZEMAX"
    BuiltinId
BuiltinInf                               -> String
"INFINITY"
    BuiltinId
BuiltinSharp                             -> String
"SHARP"
    BuiltinId
BuiltinFlat                              -> String
"FLAT"
    BuiltinId
BuiltinEquality                          -> String
"EQUALITY"
    BuiltinId
BuiltinRefl                              -> String
"REFL"
    BuiltinId
BuiltinRewrite                           -> String
"REWRITE"
    BuiltinId
BuiltinLevelMax                          -> String
"LEVELMAX"
    BuiltinId
BuiltinLevel                             -> String
"LEVEL"
    BuiltinId
BuiltinLevelZero                         -> String
"LEVELZERO"
    BuiltinId
BuiltinLevelSuc                          -> String
"LEVELSUC"
    BuiltinId
BuiltinProp                              -> String
"PROP"
    BuiltinId
BuiltinSet                               -> String
"TYPE"
    BuiltinId
BuiltinStrictSet                         -> String
"STRICTSET"
    BuiltinId
BuiltinPropOmega                         -> String
"PROPOMEGA"
    BuiltinId
BuiltinSetOmega                          -> String
"SETOMEGA"
    BuiltinId
BuiltinSSetOmega                         -> String
"STRICTSETOMEGA"
    BuiltinId
BuiltinLevelUniv                         -> String
"LEVELUNIV"
    BuiltinId
BuiltinFromNat                           -> String
"FROMNAT"
    BuiltinId
BuiltinFromNeg                           -> String
"FROMNEG"
    BuiltinId
BuiltinFromString                        -> String
"FROMSTRING"
    BuiltinId
BuiltinQName                             -> String
"QNAME"
    BuiltinId
BuiltinAgdaSort                          -> String
"AGDASORT"
    BuiltinId
BuiltinAgdaSortSet                       -> String
"AGDASORTSET"
    BuiltinId
BuiltinAgdaSortLit                       -> String
"AGDASORTLIT"
    BuiltinId
BuiltinAgdaSortProp                      -> String
"AGDASORTPROP"
    BuiltinId
BuiltinAgdaSortPropLit                   -> String
"AGDASORTPROPLIT"
    BuiltinId
BuiltinAgdaSortInf                       -> String
"AGDASORTINF"
    BuiltinId
BuiltinAgdaSortUnsupported               -> String
"AGDASORTUNSUPPORTED"
    BuiltinId
BuiltinHiding                            -> String
"HIDING"
    BuiltinId
BuiltinHidden                            -> String
"HIDDEN"
    BuiltinId
BuiltinInstance                          -> String
"INSTANCE"
    BuiltinId
BuiltinVisible                           -> String
"VISIBLE"
    BuiltinId
BuiltinRelevance                         -> String
"RELEVANCE"
    BuiltinId
BuiltinRelevant                          -> String
"RELEVANT"
    BuiltinId
BuiltinIrrelevant                        -> String
"IRRELEVANT"
    BuiltinId
BuiltinQuantity                          -> String
"QUANTITY"
    BuiltinId
BuiltinQuantity0                         -> String
"QUANTITY-0"
    BuiltinId
BuiltinQuantityω                         -> String
"QUANTITY-ω"
    BuiltinId
BuiltinModality                          -> String
"MODALITY"
    BuiltinId
BuiltinModalityConstructor               -> String
"MODALITY-CONSTRUCTOR"
    BuiltinId
BuiltinAssoc                             -> String
"ASSOC"
    BuiltinId
BuiltinAssocLeft                         -> String
"ASSOCLEFT"
    BuiltinId
BuiltinAssocRight                        -> String
"ASSOCRIGHT"
    BuiltinId
BuiltinAssocNon                          -> String
"ASSOCNON"
    BuiltinId
BuiltinPrecedence                        -> String
"PRECEDENCE"
    BuiltinId
BuiltinPrecRelated                       -> String
"PRECRELATED"
    BuiltinId
BuiltinPrecUnrelated                     -> String
"PRECUNRELATED"
    BuiltinId
BuiltinFixity                            -> String
"FIXITY"
    BuiltinId
BuiltinFixityFixity                      -> String
"FIXITYFIXITY"
    BuiltinId
BuiltinArg                               -> String
"ARG"
    BuiltinId
BuiltinArgInfo                           -> String
"ARGINFO"
    BuiltinId
BuiltinArgArgInfo                        -> String
"ARGARGINFO"
    BuiltinId
BuiltinArgArg                            -> String
"ARGARG"
    BuiltinId
BuiltinAbs                               -> String
"ABS"
    BuiltinId
BuiltinAbsAbs                            -> String
"ABSABS"
    BuiltinId
BuiltinAgdaTerm                          -> String
"AGDATERM"
    BuiltinId
BuiltinAgdaTermVar                       -> String
"AGDATERMVAR"
    BuiltinId
BuiltinAgdaTermLam                       -> String
"AGDATERMLAM"
    BuiltinId
BuiltinAgdaTermExtLam                    -> String
"AGDATERMEXTLAM"
    BuiltinId
BuiltinAgdaTermDef                       -> String
"AGDATERMDEF"
    BuiltinId
BuiltinAgdaTermCon                       -> String
"AGDATERMCON"
    BuiltinId
BuiltinAgdaTermPi                        -> String
"AGDATERMPI"
    BuiltinId
BuiltinAgdaTermSort                      -> String
"AGDATERMSORT"
    BuiltinId
BuiltinAgdaTermLit                       -> String
"AGDATERMLIT"
    BuiltinId
BuiltinAgdaTermUnsupported               -> String
"AGDATERMUNSUPPORTED"
    BuiltinId
BuiltinAgdaTermMeta                      -> String
"AGDATERMMETA"
    BuiltinId
BuiltinAgdaErrorPart                     -> String
"AGDAERRORPART"
    BuiltinId
BuiltinAgdaErrorPartString               -> String
"AGDAERRORPARTSTRING"
    BuiltinId
BuiltinAgdaErrorPartTerm                 -> String
"AGDAERRORPARTTERM"
    BuiltinId
BuiltinAgdaErrorPartPatt                 -> String
"AGDAERRORPARTPATT"
    BuiltinId
BuiltinAgdaErrorPartName                 -> String
"AGDAERRORPARTNAME"
    BuiltinId
BuiltinAgdaLiteral                       -> String
"AGDALITERAL"
    BuiltinId
BuiltinAgdaLitNat                        -> String
"AGDALITNAT"
    BuiltinId
BuiltinAgdaLitWord64                     -> String
"AGDALITWORD64"
    BuiltinId
BuiltinAgdaLitFloat                      -> String
"AGDALITFLOAT"
    BuiltinId
BuiltinAgdaLitChar                       -> String
"AGDALITCHAR"
    BuiltinId
BuiltinAgdaLitString                     -> String
"AGDALITSTRING"
    BuiltinId
BuiltinAgdaLitQName                      -> String
"AGDALITQNAME"
    BuiltinId
BuiltinAgdaLitMeta                       -> String
"AGDALITMETA"
    BuiltinId
BuiltinAgdaClause                        -> String
"AGDACLAUSE"
    BuiltinId
BuiltinAgdaClauseClause                  -> String
"AGDACLAUSECLAUSE"
    BuiltinId
BuiltinAgdaClauseAbsurd                  -> String
"AGDACLAUSEABSURD"
    BuiltinId
BuiltinAgdaPattern                       -> String
"AGDAPATTERN"
    BuiltinId
BuiltinAgdaPatVar                        -> String
"AGDAPATVAR"
    BuiltinId
BuiltinAgdaPatCon                        -> String
"AGDAPATCON"
    BuiltinId
BuiltinAgdaPatDot                        -> String
"AGDAPATDOT"
    BuiltinId
BuiltinAgdaPatLit                        -> String
"AGDAPATLIT"
    BuiltinId
BuiltinAgdaPatProj                       -> String
"AGDAPATPROJ"
    BuiltinId
BuiltinAgdaPatAbsurd                     -> String
"AGDAPATABSURD"
    BuiltinId
BuiltinAgdaDefinitionFunDef              -> String
"AGDADEFINITIONFUNDEF"
    BuiltinId
BuiltinAgdaDefinitionDataDef             -> String
"AGDADEFINITIONDATADEF"
    BuiltinId
BuiltinAgdaDefinitionRecordDef           -> String
"AGDADEFINITIONRECORDDEF"
    BuiltinId
BuiltinAgdaDefinitionDataConstructor     -> String
"AGDADEFINITIONDATACONSTRUCTOR"
    BuiltinId
BuiltinAgdaDefinitionPostulate           -> String
"AGDADEFINITIONPOSTULATE"
    BuiltinId
BuiltinAgdaDefinitionPrimitive           -> String
"AGDADEFINITIONPRIMITIVE"
    BuiltinId
BuiltinAgdaDefinition                    -> String
"AGDADEFINITION"
    BuiltinId
BuiltinAgdaMeta                          -> String
"AGDAMETA"
    BuiltinId
BuiltinAgdaTCM                           -> String
"AGDATCM"
    BuiltinId
BuiltinAgdaTCMReturn                     -> String
"AGDATCMRETURN"
    BuiltinId
BuiltinAgdaTCMBind                       -> String
"AGDATCMBIND"
    BuiltinId
BuiltinAgdaTCMUnify                      -> String
"AGDATCMUNIFY"
    BuiltinId
BuiltinAgdaTCMTypeError                  -> String
"AGDATCMTYPEERROR"
    BuiltinId
BuiltinAgdaTCMInferType                  -> String
"AGDATCMINFERTYPE"
    BuiltinId
BuiltinAgdaTCMCheckType                  -> String
"AGDATCMCHECKTYPE"
    BuiltinId
BuiltinAgdaTCMNormalise                  -> String
"AGDATCMNORMALISE"
    BuiltinId
BuiltinAgdaTCMReduce                     -> String
"AGDATCMREDUCE"
    BuiltinId
BuiltinAgdaTCMCatchError                 -> String
"AGDATCMCATCHERROR"
    BuiltinId
BuiltinAgdaTCMGetContext                 -> String
"AGDATCMGETCONTEXT"
    BuiltinId
BuiltinAgdaTCMExtendContext              -> String
"AGDATCMEXTENDCONTEXT"
    BuiltinId
BuiltinAgdaTCMInContext                  -> String
"AGDATCMINCONTEXT"
    BuiltinId
BuiltinAgdaTCMFreshName                  -> String
"AGDATCMFRESHNAME"
    BuiltinId
BuiltinAgdaTCMDeclareDef                 -> String
"AGDATCMDECLAREDEF"
    BuiltinId
BuiltinAgdaTCMDeclarePostulate           -> String
"AGDATCMDECLAREPOSTULATE"
    BuiltinId
BuiltinAgdaTCMDeclareData                -> String
"AGDATCMDECLAREDATA"
    BuiltinId
BuiltinAgdaTCMDefineData                 -> String
"AGDATCMDEFINEDATA"
    BuiltinId
BuiltinAgdaTCMDefineFun                  -> String
"AGDATCMDEFINEFUN"
    BuiltinId
BuiltinAgdaTCMGetType                    -> String
"AGDATCMGETTYPE"
    BuiltinId
BuiltinAgdaTCMGetDefinition              -> String
"AGDATCMGETDEFINITION"
    BuiltinId
BuiltinAgdaTCMBlock                      -> String
"AGDATCMBLOCK"
    BuiltinId
BuiltinAgdaTCMCommit                     -> String
"AGDATCMCOMMIT"
    BuiltinId
BuiltinAgdaTCMQuoteTerm                  -> String
"AGDATCMQUOTETERM"
    BuiltinId
BuiltinAgdaTCMUnquoteTerm                -> String
"AGDATCMUNQUOTETERM"
    BuiltinId
BuiltinAgdaTCMQuoteOmegaTerm             -> String
"AGDATCMQUOTEOMEGATERM"
    BuiltinId
BuiltinAgdaTCMIsMacro                    -> String
"AGDATCMISMACRO"
    BuiltinId
BuiltinAgdaTCMWithNormalisation          -> String
"AGDATCMWITHNORMALISATION"
    BuiltinId
BuiltinAgdaTCMWithReconstructed          -> String
"AGDATCMWITHRECONSTRUCTED"
    BuiltinId
BuiltinAgdaTCMWithExpandLast             -> String
"AGDATCMWITHEXPANDLAST"
    BuiltinId
BuiltinAgdaTCMWithReduceDefs             -> String
"AGDATCMWITHREDUCEDEFS"
    BuiltinId
BuiltinAgdaTCMAskNormalisation           -> String
"AGDATCMASKNORMALISATION"
    BuiltinId
BuiltinAgdaTCMAskReconstructed           -> String
"AGDATCMASKRECONSTRUCTED"
    BuiltinId
BuiltinAgdaTCMAskExpandLast              -> String
"AGDATCMASKEXPANDLAST"
    BuiltinId
BuiltinAgdaTCMAskReduceDefs              -> String
"AGDATCMASKREDUCEDEFS"
    BuiltinId
BuiltinAgdaTCMFormatErrorParts           -> String
"AGDATCMFORMATERRORPARTS"
    BuiltinId
BuiltinAgdaTCMDebugPrint                 -> String
"AGDATCMDEBUGPRINT"
    BuiltinId
BuiltinAgdaTCMNoConstraints              -> String
"AGDATCMNOCONSTRAINTS"
    BuiltinId
BuiltinAgdaTCMRunSpeculative             -> String
"AGDATCMRUNSPECULATIVE"
    BuiltinId
BuiltinAgdaTCMExec                       -> String
"AGDATCMEXEC"
    BuiltinId
BuiltinAgdaTCMGetInstances               -> String
"AGDATCMGETINSTANCES"
    BuiltinId
BuiltinAgdaTCMPragmaForeign              -> String
"AGDATCMPRAGMAFOREIGN"
    BuiltinId
BuiltinAgdaTCMPragmaCompile              -> String
"AGDATCMPRAGMACOMPILE"
    BuiltinId
BuiltinAgdaBlocker                       -> String
"AGDABLOCKER"
    BuiltinId
BuiltinAgdaBlockerAny                    -> String
"AGDABLOCKERANY"
    BuiltinId
BuiltinAgdaBlockerAll                    -> String
"AGDABLOCKERALL"
    BuiltinId
BuiltinAgdaBlockerMeta                   -> String
"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 :: BuiltinId -> Bool
isBuiltinNoDef = [BuiltinId] -> BuiltinId -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [BuiltinId]
builtinsNoDef

builtinsNoDef :: [BuiltinId]
builtinsNoDef :: [BuiltinId]
builtinsNoDef =
  [BuiltinId]
sizeBuiltins [BuiltinId] -> [BuiltinId] -> [BuiltinId]
forall a. [a] -> [a] -> [a]
++
   -- builtinConId,
  [ BuiltinId
builtinIntervalUniv
  , BuiltinId
builtinId
  , BuiltinId
builtinReflId
  , BuiltinId
builtinInterval
  , BuiltinId
builtinPartial
  , BuiltinId
builtinPartialP
  , BuiltinId
builtinIsOne
  , BuiltinId
builtinSub
  , BuiltinId
builtinIZero
  , BuiltinId
builtinIOne
  , BuiltinId
builtinProp
  , BuiltinId
builtinSet
  , BuiltinId
builtinStrictSet
  , BuiltinId
builtinPropOmega
  , BuiltinId
builtinSetOmega
  , BuiltinId
builtinSSetOmega
  , BuiltinId
builtinLevelUniv
  ]

sizeBuiltins :: [BuiltinId]
sizeBuiltins :: [BuiltinId]
sizeBuiltins =
  [ BuiltinId
builtinSizeUniv
  , BuiltinId
builtinSize
  , BuiltinId
builtinSizeLt
  , BuiltinId
builtinSizeSuc
  , BuiltinId
builtinSizeInf
  , BuiltinId
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,
  builtinId, builtinReflId,
  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,
  builtinAgdaTCMRunSpeculative,
  builtinAgdaTCMExec,
  builtinAgdaTCMGetInstances,
  builtinAgdaTCMPragmaForeign,
  builtinAgdaTCMPragmaCompile
  :: BuiltinId

builtinNat :: BuiltinId
builtinNat                               = BuiltinId
BuiltinNat
builtinSuc :: BuiltinId
builtinSuc                               = BuiltinId
BuiltinSuc
builtinZero :: BuiltinId
builtinZero                              = BuiltinId
BuiltinZero
builtinNatPlus :: BuiltinId
builtinNatPlus                           = BuiltinId
BuiltinNatPlus
builtinNatMinus :: BuiltinId
builtinNatMinus                          = BuiltinId
BuiltinNatMinus
builtinNatTimes :: BuiltinId
builtinNatTimes                          = BuiltinId
BuiltinNatTimes
builtinNatDivSucAux :: BuiltinId
builtinNatDivSucAux                      = BuiltinId
BuiltinNatDivSucAux
builtinNatModSucAux :: BuiltinId
builtinNatModSucAux                      = BuiltinId
BuiltinNatModSucAux
builtinNatEquals :: BuiltinId
builtinNatEquals                         = BuiltinId
BuiltinNatEquals
builtinNatLess :: BuiltinId
builtinNatLess                           = BuiltinId
BuiltinNatLess
builtinWord64 :: BuiltinId
builtinWord64                            = BuiltinId
BuiltinWord64
builtinInteger :: BuiltinId
builtinInteger                           = BuiltinId
BuiltinInteger
builtinIntegerPos :: BuiltinId
builtinIntegerPos                        = BuiltinId
BuiltinIntegerPos
builtinIntegerNegSuc :: BuiltinId
builtinIntegerNegSuc                     = BuiltinId
BuiltinIntegerNegSuc
builtinFloat :: BuiltinId
builtinFloat                             = BuiltinId
BuiltinFloat
builtinChar :: BuiltinId
builtinChar                              = BuiltinId
BuiltinChar
builtinString :: BuiltinId
builtinString                            = BuiltinId
BuiltinString
builtinUnit :: BuiltinId
builtinUnit                              = BuiltinId
BuiltinUnit
builtinUnitUnit :: BuiltinId
builtinUnitUnit                          = BuiltinId
BuiltinUnitUnit
builtinSigma :: BuiltinId
builtinSigma                             = BuiltinId
BuiltinSigma
builtinBool :: BuiltinId
builtinBool                              = BuiltinId
BuiltinBool
builtinTrue :: BuiltinId
builtinTrue                              = BuiltinId
BuiltinTrue
builtinFalse :: BuiltinId
builtinFalse                             = BuiltinId
BuiltinFalse
builtinList :: BuiltinId
builtinList                              = BuiltinId
BuiltinList
builtinNil :: BuiltinId
builtinNil                               = BuiltinId
BuiltinNil
builtinCons :: BuiltinId
builtinCons                              = BuiltinId
BuiltinCons
builtinMaybe :: BuiltinId
builtinMaybe                             = BuiltinId
BuiltinMaybe
builtinNothing :: BuiltinId
builtinNothing                           = BuiltinId
BuiltinNothing
builtinJust :: BuiltinId
builtinJust                              = BuiltinId
BuiltinJust
builtinIO :: BuiltinId
builtinIO                                = BuiltinId
BuiltinIO
builtinId :: BuiltinId
builtinId                                = BuiltinId
BuiltinId
builtinReflId :: BuiltinId
builtinReflId                            = BuiltinId
BuiltinReflId
builtinPath :: BuiltinId
builtinPath                              = BuiltinId
BuiltinPath
builtinPathP :: BuiltinId
builtinPathP                             = BuiltinId
BuiltinPathP
builtinIntervalUniv :: BuiltinId
builtinIntervalUniv                      = BuiltinId
BuiltinIntervalUniv
builtinInterval :: BuiltinId
builtinInterval                          = BuiltinId
BuiltinInterval
builtinIZero :: BuiltinId
builtinIZero                             = BuiltinId
BuiltinIZero
builtinIOne :: BuiltinId
builtinIOne                              = BuiltinId
BuiltinIOne
builtinPartial :: BuiltinId
builtinPartial                           = BuiltinId
BuiltinPartial
builtinPartialP :: BuiltinId
builtinPartialP                          = BuiltinId
BuiltinPartialP
builtinIsOne :: BuiltinId
builtinIsOne                             = BuiltinId
BuiltinIsOne
builtinItIsOne :: BuiltinId
builtinItIsOne                           = BuiltinId
BuiltinItIsOne
builtinEquiv :: BuiltinId
builtinEquiv                             = BuiltinId
BuiltinEquiv
builtinEquivFun :: BuiltinId
builtinEquivFun                          = BuiltinId
BuiltinEquivFun
builtinEquivProof :: BuiltinId
builtinEquivProof                        = BuiltinId
BuiltinEquivProof
builtinTranspProof :: BuiltinId
builtinTranspProof                       = BuiltinId
BuiltinTranspProof
builtinIsOne1 :: BuiltinId
builtinIsOne1                            = BuiltinId
BuiltinIsOne1
builtinIsOne2 :: BuiltinId
builtinIsOne2                            = BuiltinId
BuiltinIsOne2
builtinIsOneEmpty :: BuiltinId
builtinIsOneEmpty                        = BuiltinId
BuiltinIsOneEmpty
builtinSub :: BuiltinId
builtinSub                               = BuiltinId
BuiltinSub
builtinSubIn :: BuiltinId
builtinSubIn                             = BuiltinId
BuiltinSubIn
builtinSizeUniv :: BuiltinId
builtinSizeUniv                          = BuiltinId
BuiltinSizeUniv
builtinSize :: BuiltinId
builtinSize                              = BuiltinId
BuiltinSize
builtinSizeLt :: BuiltinId
builtinSizeLt                            = BuiltinId
BuiltinSizeLt
builtinSizeSuc :: BuiltinId
builtinSizeSuc                           = BuiltinId
BuiltinSizeSuc
builtinSizeInf :: BuiltinId
builtinSizeInf                           = BuiltinId
BuiltinSizeInf
builtinSizeMax :: BuiltinId
builtinSizeMax                           = BuiltinId
BuiltinSizeMax
builtinInf :: BuiltinId
builtinInf                               = BuiltinId
BuiltinInf
builtinSharp :: BuiltinId
builtinSharp                             = BuiltinId
BuiltinSharp
builtinFlat :: BuiltinId
builtinFlat                              = BuiltinId
BuiltinFlat
builtinEquality :: BuiltinId
builtinEquality                          = BuiltinId
BuiltinEquality
builtinRefl :: BuiltinId
builtinRefl                              = BuiltinId
BuiltinRefl
builtinRewrite :: BuiltinId
builtinRewrite                           = BuiltinId
BuiltinRewrite
builtinLevelMax :: BuiltinId
builtinLevelMax                          = BuiltinId
BuiltinLevelMax
builtinLevel :: BuiltinId
builtinLevel                             = BuiltinId
BuiltinLevel
builtinLevelZero :: BuiltinId
builtinLevelZero                         = BuiltinId
BuiltinLevelZero
builtinLevelSuc :: BuiltinId
builtinLevelSuc                          = BuiltinId
BuiltinLevelSuc
builtinProp :: BuiltinId
builtinProp                              = BuiltinId
BuiltinProp
builtinSet :: BuiltinId
builtinSet                               = BuiltinId
BuiltinSet
builtinStrictSet :: BuiltinId
builtinStrictSet                         = BuiltinId
BuiltinStrictSet
builtinPropOmega :: BuiltinId
builtinPropOmega                         = BuiltinId
BuiltinPropOmega
builtinSetOmega :: BuiltinId
builtinSetOmega                          = BuiltinId
BuiltinSetOmega
builtinSSetOmega :: BuiltinId
builtinSSetOmega                         = BuiltinId
BuiltinSSetOmega
builtinLevelUniv :: BuiltinId
builtinLevelUniv                         = BuiltinId
BuiltinLevelUniv
builtinFromNat :: BuiltinId
builtinFromNat                           = BuiltinId
BuiltinFromNat
builtinFromNeg :: BuiltinId
builtinFromNeg                           = BuiltinId
BuiltinFromNeg
builtinFromString :: BuiltinId
builtinFromString                        = BuiltinId
BuiltinFromString
builtinQName :: BuiltinId
builtinQName                             = BuiltinId
BuiltinQName
builtinAgdaSort :: BuiltinId
builtinAgdaSort                          = BuiltinId
BuiltinAgdaSort
builtinAgdaSortSet :: BuiltinId
builtinAgdaSortSet                       = BuiltinId
BuiltinAgdaSortSet
builtinAgdaSortLit :: BuiltinId
builtinAgdaSortLit                       = BuiltinId
BuiltinAgdaSortLit
builtinAgdaSortProp :: BuiltinId
builtinAgdaSortProp                      = BuiltinId
BuiltinAgdaSortProp
builtinAgdaSortPropLit :: BuiltinId
builtinAgdaSortPropLit                   = BuiltinId
BuiltinAgdaSortPropLit
builtinAgdaSortInf :: BuiltinId
builtinAgdaSortInf                       = BuiltinId
BuiltinAgdaSortInf
builtinAgdaSortUnsupported :: BuiltinId
builtinAgdaSortUnsupported               = BuiltinId
BuiltinAgdaSortUnsupported
builtinHiding :: BuiltinId
builtinHiding                            = BuiltinId
BuiltinHiding
builtinHidden :: BuiltinId
builtinHidden                            = BuiltinId
BuiltinHidden
builtinInstance :: BuiltinId
builtinInstance                          = BuiltinId
BuiltinInstance
builtinVisible :: BuiltinId
builtinVisible                           = BuiltinId
BuiltinVisible
builtinRelevance :: BuiltinId
builtinRelevance                         = BuiltinId
BuiltinRelevance
builtinRelevant :: BuiltinId
builtinRelevant                          = BuiltinId
BuiltinRelevant
builtinIrrelevant :: BuiltinId
builtinIrrelevant                        = BuiltinId
BuiltinIrrelevant
builtinQuantity :: BuiltinId
builtinQuantity                          = BuiltinId
BuiltinQuantity
builtinQuantity0 :: BuiltinId
builtinQuantity0                         = BuiltinId
BuiltinQuantity0
builtinQuantityω :: BuiltinId
builtinQuantityω                         = BuiltinId
BuiltinQuantityω
builtinModality :: BuiltinId
builtinModality                          = BuiltinId
BuiltinModality
builtinModalityConstructor :: BuiltinId
builtinModalityConstructor               = BuiltinId
BuiltinModalityConstructor
builtinAssoc :: BuiltinId
builtinAssoc                             = BuiltinId
BuiltinAssoc
builtinAssocLeft :: BuiltinId
builtinAssocLeft                         = BuiltinId
BuiltinAssocLeft
builtinAssocRight :: BuiltinId
builtinAssocRight                        = BuiltinId
BuiltinAssocRight
builtinAssocNon :: BuiltinId
builtinAssocNon                          = BuiltinId
BuiltinAssocNon
builtinPrecedence :: BuiltinId
builtinPrecedence                        = BuiltinId
BuiltinPrecedence
builtinPrecRelated :: BuiltinId
builtinPrecRelated                       = BuiltinId
BuiltinPrecRelated
builtinPrecUnrelated :: BuiltinId
builtinPrecUnrelated                     = BuiltinId
BuiltinPrecUnrelated
builtinFixity :: BuiltinId
builtinFixity                            = BuiltinId
BuiltinFixity
builtinFixityFixity :: BuiltinId
builtinFixityFixity                      = BuiltinId
BuiltinFixityFixity
builtinArg :: BuiltinId
builtinArg                               = BuiltinId
BuiltinArg
builtinArgInfo :: BuiltinId
builtinArgInfo                           = BuiltinId
BuiltinArgInfo
builtinArgArgInfo :: BuiltinId
builtinArgArgInfo                        = BuiltinId
BuiltinArgArgInfo
builtinArgArg :: BuiltinId
builtinArgArg                            = BuiltinId
BuiltinArgArg
builtinAbs :: BuiltinId
builtinAbs                               = BuiltinId
BuiltinAbs
builtinAbsAbs :: BuiltinId
builtinAbsAbs                            = BuiltinId
BuiltinAbsAbs
builtinAgdaTerm :: BuiltinId
builtinAgdaTerm                          = BuiltinId
BuiltinAgdaTerm
builtinAgdaTermVar :: BuiltinId
builtinAgdaTermVar                       = BuiltinId
BuiltinAgdaTermVar
builtinAgdaTermLam :: BuiltinId
builtinAgdaTermLam                       = BuiltinId
BuiltinAgdaTermLam
builtinAgdaTermExtLam :: BuiltinId
builtinAgdaTermExtLam                    = BuiltinId
BuiltinAgdaTermExtLam
builtinAgdaTermDef :: BuiltinId
builtinAgdaTermDef                       = BuiltinId
BuiltinAgdaTermDef
builtinAgdaTermCon :: BuiltinId
builtinAgdaTermCon                       = BuiltinId
BuiltinAgdaTermCon
builtinAgdaTermPi :: BuiltinId
builtinAgdaTermPi                        = BuiltinId
BuiltinAgdaTermPi
builtinAgdaTermSort :: BuiltinId
builtinAgdaTermSort                      = BuiltinId
BuiltinAgdaTermSort
builtinAgdaTermLit :: BuiltinId
builtinAgdaTermLit                       = BuiltinId
BuiltinAgdaTermLit
builtinAgdaTermUnsupported :: BuiltinId
builtinAgdaTermUnsupported               = BuiltinId
BuiltinAgdaTermUnsupported
builtinAgdaTermMeta :: BuiltinId
builtinAgdaTermMeta                      = BuiltinId
BuiltinAgdaTermMeta
builtinAgdaErrorPart :: BuiltinId
builtinAgdaErrorPart                     = BuiltinId
BuiltinAgdaErrorPart
builtinAgdaErrorPartString :: BuiltinId
builtinAgdaErrorPartString               = BuiltinId
BuiltinAgdaErrorPartString
builtinAgdaErrorPartTerm :: BuiltinId
builtinAgdaErrorPartTerm                 = BuiltinId
BuiltinAgdaErrorPartTerm
builtinAgdaErrorPartPatt :: BuiltinId
builtinAgdaErrorPartPatt                 = BuiltinId
BuiltinAgdaErrorPartPatt
builtinAgdaErrorPartName :: BuiltinId
builtinAgdaErrorPartName                 = BuiltinId
BuiltinAgdaErrorPartName
builtinAgdaLiteral :: BuiltinId
builtinAgdaLiteral                       = BuiltinId
BuiltinAgdaLiteral
builtinAgdaLitNat :: BuiltinId
builtinAgdaLitNat                        = BuiltinId
BuiltinAgdaLitNat
builtinAgdaLitWord64 :: BuiltinId
builtinAgdaLitWord64                     = BuiltinId
BuiltinAgdaLitWord64
builtinAgdaLitFloat :: BuiltinId
builtinAgdaLitFloat                      = BuiltinId
BuiltinAgdaLitFloat
builtinAgdaLitChar :: BuiltinId
builtinAgdaLitChar                       = BuiltinId
BuiltinAgdaLitChar
builtinAgdaLitString :: BuiltinId
builtinAgdaLitString                     = BuiltinId
BuiltinAgdaLitString
builtinAgdaLitQName :: BuiltinId
builtinAgdaLitQName                      = BuiltinId
BuiltinAgdaLitQName
builtinAgdaLitMeta :: BuiltinId
builtinAgdaLitMeta                       = BuiltinId
BuiltinAgdaLitMeta
builtinAgdaClause :: BuiltinId
builtinAgdaClause                        = BuiltinId
BuiltinAgdaClause
builtinAgdaClauseClause :: BuiltinId
builtinAgdaClauseClause                  = BuiltinId
BuiltinAgdaClauseClause
builtinAgdaClauseAbsurd :: BuiltinId
builtinAgdaClauseAbsurd                  = BuiltinId
BuiltinAgdaClauseAbsurd
builtinAgdaPattern :: BuiltinId
builtinAgdaPattern                       = BuiltinId
BuiltinAgdaPattern
builtinAgdaPatVar :: BuiltinId
builtinAgdaPatVar                        = BuiltinId
BuiltinAgdaPatVar
builtinAgdaPatCon :: BuiltinId
builtinAgdaPatCon                        = BuiltinId
BuiltinAgdaPatCon
builtinAgdaPatDot :: BuiltinId
builtinAgdaPatDot                        = BuiltinId
BuiltinAgdaPatDot
builtinAgdaPatLit :: BuiltinId
builtinAgdaPatLit                        = BuiltinId
BuiltinAgdaPatLit
builtinAgdaPatProj :: BuiltinId
builtinAgdaPatProj                       = BuiltinId
BuiltinAgdaPatProj
builtinAgdaPatAbsurd :: BuiltinId
builtinAgdaPatAbsurd                     = BuiltinId
BuiltinAgdaPatAbsurd
builtinAgdaDefinitionFunDef :: BuiltinId
builtinAgdaDefinitionFunDef              = BuiltinId
BuiltinAgdaDefinitionFunDef
builtinAgdaDefinitionDataDef :: BuiltinId
builtinAgdaDefinitionDataDef             = BuiltinId
BuiltinAgdaDefinitionDataDef
builtinAgdaDefinitionRecordDef :: BuiltinId
builtinAgdaDefinitionRecordDef           = BuiltinId
BuiltinAgdaDefinitionRecordDef
builtinAgdaDefinitionDataConstructor :: BuiltinId
builtinAgdaDefinitionDataConstructor     = BuiltinId
BuiltinAgdaDefinitionDataConstructor
builtinAgdaDefinitionPostulate :: BuiltinId
builtinAgdaDefinitionPostulate           = BuiltinId
BuiltinAgdaDefinitionPostulate
builtinAgdaDefinitionPrimitive :: BuiltinId
builtinAgdaDefinitionPrimitive           = BuiltinId
BuiltinAgdaDefinitionPrimitive
builtinAgdaDefinition :: BuiltinId
builtinAgdaDefinition                    = BuiltinId
BuiltinAgdaDefinition
builtinAgdaMeta :: BuiltinId
builtinAgdaMeta                          = BuiltinId
BuiltinAgdaMeta
builtinAgdaTCM :: BuiltinId
builtinAgdaTCM                           = BuiltinId
BuiltinAgdaTCM
builtinAgdaTCMReturn :: BuiltinId
builtinAgdaTCMReturn                     = BuiltinId
BuiltinAgdaTCMReturn
builtinAgdaTCMBind :: BuiltinId
builtinAgdaTCMBind                       = BuiltinId
BuiltinAgdaTCMBind
builtinAgdaTCMUnify :: BuiltinId
builtinAgdaTCMUnify                      = BuiltinId
BuiltinAgdaTCMUnify
builtinAgdaTCMTypeError :: BuiltinId
builtinAgdaTCMTypeError                  = BuiltinId
BuiltinAgdaTCMTypeError
builtinAgdaTCMInferType :: BuiltinId
builtinAgdaTCMInferType                  = BuiltinId
BuiltinAgdaTCMInferType
builtinAgdaTCMCheckType :: BuiltinId
builtinAgdaTCMCheckType                  = BuiltinId
BuiltinAgdaTCMCheckType
builtinAgdaTCMNormalise :: BuiltinId
builtinAgdaTCMNormalise                  = BuiltinId
BuiltinAgdaTCMNormalise
builtinAgdaTCMReduce :: BuiltinId
builtinAgdaTCMReduce                     = BuiltinId
BuiltinAgdaTCMReduce
builtinAgdaTCMCatchError :: BuiltinId
builtinAgdaTCMCatchError                 = BuiltinId
BuiltinAgdaTCMCatchError
builtinAgdaTCMGetContext :: BuiltinId
builtinAgdaTCMGetContext                 = BuiltinId
BuiltinAgdaTCMGetContext
builtinAgdaTCMExtendContext :: BuiltinId
builtinAgdaTCMExtendContext              = BuiltinId
BuiltinAgdaTCMExtendContext
builtinAgdaTCMInContext :: BuiltinId
builtinAgdaTCMInContext                  = BuiltinId
BuiltinAgdaTCMInContext
builtinAgdaTCMFreshName :: BuiltinId
builtinAgdaTCMFreshName                  = BuiltinId
BuiltinAgdaTCMFreshName
builtinAgdaTCMDeclareDef :: BuiltinId
builtinAgdaTCMDeclareDef                 = BuiltinId
BuiltinAgdaTCMDeclareDef
builtinAgdaTCMDeclarePostulate :: BuiltinId
builtinAgdaTCMDeclarePostulate           = BuiltinId
BuiltinAgdaTCMDeclarePostulate
builtinAgdaTCMDeclareData :: BuiltinId
builtinAgdaTCMDeclareData                = BuiltinId
BuiltinAgdaTCMDeclareData
builtinAgdaTCMDefineData :: BuiltinId
builtinAgdaTCMDefineData                 = BuiltinId
BuiltinAgdaTCMDefineData
builtinAgdaTCMDefineFun :: BuiltinId
builtinAgdaTCMDefineFun                  = BuiltinId
BuiltinAgdaTCMDefineFun
builtinAgdaTCMGetType :: BuiltinId
builtinAgdaTCMGetType                    = BuiltinId
BuiltinAgdaTCMGetType
builtinAgdaTCMGetDefinition :: BuiltinId
builtinAgdaTCMGetDefinition              = BuiltinId
BuiltinAgdaTCMGetDefinition
builtinAgdaTCMBlock :: BuiltinId
builtinAgdaTCMBlock                      = BuiltinId
BuiltinAgdaTCMBlock
builtinAgdaTCMCommit :: BuiltinId
builtinAgdaTCMCommit                     = BuiltinId
BuiltinAgdaTCMCommit
builtinAgdaTCMQuoteTerm :: BuiltinId
builtinAgdaTCMQuoteTerm                  = BuiltinId
BuiltinAgdaTCMQuoteTerm
builtinAgdaTCMUnquoteTerm :: BuiltinId
builtinAgdaTCMUnquoteTerm                = BuiltinId
BuiltinAgdaTCMUnquoteTerm
builtinAgdaTCMQuoteOmegaTerm :: BuiltinId
builtinAgdaTCMQuoteOmegaTerm             = BuiltinId
BuiltinAgdaTCMQuoteOmegaTerm
builtinAgdaTCMIsMacro :: BuiltinId
builtinAgdaTCMIsMacro                    = BuiltinId
BuiltinAgdaTCMIsMacro
builtinAgdaTCMWithNormalisation :: BuiltinId
builtinAgdaTCMWithNormalisation          = BuiltinId
BuiltinAgdaTCMWithNormalisation
builtinAgdaTCMWithReconstructed :: BuiltinId
builtinAgdaTCMWithReconstructed          = BuiltinId
BuiltinAgdaTCMWithReconstructed
builtinAgdaTCMWithExpandLast :: BuiltinId
builtinAgdaTCMWithExpandLast             = BuiltinId
BuiltinAgdaTCMWithExpandLast
builtinAgdaTCMWithReduceDefs :: BuiltinId
builtinAgdaTCMWithReduceDefs             = BuiltinId
BuiltinAgdaTCMWithReduceDefs
builtinAgdaTCMAskNormalisation :: BuiltinId
builtinAgdaTCMAskNormalisation           = BuiltinId
BuiltinAgdaTCMAskNormalisation
builtinAgdaTCMAskReconstructed :: BuiltinId
builtinAgdaTCMAskReconstructed           = BuiltinId
BuiltinAgdaTCMAskReconstructed
builtinAgdaTCMAskExpandLast :: BuiltinId
builtinAgdaTCMAskExpandLast              = BuiltinId
BuiltinAgdaTCMAskExpandLast
builtinAgdaTCMAskReduceDefs :: BuiltinId
builtinAgdaTCMAskReduceDefs              = BuiltinId
BuiltinAgdaTCMAskReduceDefs
builtinAgdaTCMFormatErrorParts :: BuiltinId
builtinAgdaTCMFormatErrorParts           = BuiltinId
BuiltinAgdaTCMFormatErrorParts
builtinAgdaTCMDebugPrint :: BuiltinId
builtinAgdaTCMDebugPrint                 = BuiltinId
BuiltinAgdaTCMDebugPrint
builtinAgdaTCMNoConstraints :: BuiltinId
builtinAgdaTCMNoConstraints              = BuiltinId
BuiltinAgdaTCMNoConstraints
builtinAgdaTCMRunSpeculative :: BuiltinId
builtinAgdaTCMRunSpeculative             = BuiltinId
BuiltinAgdaTCMRunSpeculative
builtinAgdaTCMExec :: BuiltinId
builtinAgdaTCMExec                       = BuiltinId
BuiltinAgdaTCMExec
builtinAgdaTCMGetInstances :: BuiltinId
builtinAgdaTCMGetInstances               = BuiltinId
BuiltinAgdaTCMGetInstances
builtinAgdaTCMPragmaForeign :: BuiltinId
builtinAgdaTCMPragmaForeign              = BuiltinId
BuiltinAgdaTCMPragmaForeign
builtinAgdaTCMPragmaCompile :: BuiltinId
builtinAgdaTCMPragmaCompile              = BuiltinId
BuiltinAgdaTCMPragmaCompile
builtinAgdaBlocker :: BuiltinId
builtinAgdaBlocker                       = BuiltinId
BuiltinAgdaBlocker
builtinAgdaBlockerAny :: BuiltinId
builtinAgdaBlockerAny                    = BuiltinId
BuiltinAgdaBlockerAny
builtinAgdaBlockerAll :: BuiltinId
builtinAgdaBlockerAll                    = BuiltinId
BuiltinAgdaBlockerAll
builtinAgdaBlockerMeta :: BuiltinId
builtinAgdaBlockerMeta                   = BuiltinId
BuiltinAgdaBlockerMeta

-- | Lookup a builtin by the string used in the @BUILTIN@ pragma.
builtinById :: String -> Maybe BuiltinId
builtinById :: String -> Maybe BuiltinId
builtinById = (String -> Map String BuiltinId -> Maybe BuiltinId)
-> Map String BuiltinId -> String -> Maybe BuiltinId
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> Map String BuiltinId -> Maybe BuiltinId
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Map String BuiltinId
m where
  m :: Map String BuiltinId
m = [(String, BuiltinId)] -> Map String BuiltinId
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(BuiltinId -> String
forall a. IsBuiltin a => a -> String
getBuiltinId BuiltinId
x, BuiltinId
x) | BuiltinId
x <- [(BuiltinId
forall a. Bounded a => a
minBound :: BuiltinId)..]]

-- * Primitives

-- | A primitive name, defined by the @primitive@ block.
data PrimitiveId
  -- Cubical
  = PrimConId
  | PrimIdElim
  | PrimIMin
  | PrimIMax
  | PrimINeg
  | PrimPartial
  | PrimPartialP
  | PrimSubOut
  | PrimGlue
  | Prim_glue
  | Prim_unglue
  | Prim_glueU
  | Prim_unglueU
  | PrimFaceForall
  | PrimComp
  | PrimPOr
  | PrimTrans
  | PrimDepIMin
  | PrimIdFace
  | PrimIdPath
  | 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 (Int -> PrimitiveId -> ShowS
[PrimitiveId] -> ShowS
PrimitiveId -> String
(Int -> PrimitiveId -> ShowS)
-> (PrimitiveId -> String)
-> ([PrimitiveId] -> ShowS)
-> Show PrimitiveId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PrimitiveId -> ShowS
showsPrec :: Int -> PrimitiveId -> ShowS
$cshow :: PrimitiveId -> String
show :: PrimitiveId -> String
$cshowList :: [PrimitiveId] -> ShowS
showList :: [PrimitiveId] -> ShowS
Show, PrimitiveId -> PrimitiveId -> Bool
(PrimitiveId -> PrimitiveId -> Bool)
-> (PrimitiveId -> PrimitiveId -> Bool) -> Eq PrimitiveId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PrimitiveId -> PrimitiveId -> Bool
== :: PrimitiveId -> PrimitiveId -> Bool
$c/= :: PrimitiveId -> PrimitiveId -> Bool
/= :: PrimitiveId -> PrimitiveId -> Bool
Eq, Eq PrimitiveId
Eq PrimitiveId =>
(PrimitiveId -> PrimitiveId -> Ordering)
-> (PrimitiveId -> PrimitiveId -> Bool)
-> (PrimitiveId -> PrimitiveId -> Bool)
-> (PrimitiveId -> PrimitiveId -> Bool)
-> (PrimitiveId -> PrimitiveId -> Bool)
-> (PrimitiveId -> PrimitiveId -> PrimitiveId)
-> (PrimitiveId -> PrimitiveId -> PrimitiveId)
-> Ord PrimitiveId
PrimitiveId -> PrimitiveId -> Bool
PrimitiveId -> PrimitiveId -> Ordering
PrimitiveId -> PrimitiveId -> PrimitiveId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: PrimitiveId -> PrimitiveId -> Ordering
compare :: PrimitiveId -> PrimitiveId -> Ordering
$c< :: PrimitiveId -> PrimitiveId -> Bool
< :: PrimitiveId -> PrimitiveId -> Bool
$c<= :: PrimitiveId -> PrimitiveId -> Bool
<= :: PrimitiveId -> PrimitiveId -> Bool
$c> :: PrimitiveId -> PrimitiveId -> Bool
> :: PrimitiveId -> PrimitiveId -> Bool
$c>= :: PrimitiveId -> PrimitiveId -> Bool
>= :: PrimitiveId -> PrimitiveId -> Bool
$cmax :: PrimitiveId -> PrimitiveId -> PrimitiveId
max :: PrimitiveId -> PrimitiveId -> PrimitiveId
$cmin :: PrimitiveId -> PrimitiveId -> PrimitiveId
min :: PrimitiveId -> PrimitiveId -> PrimitiveId
Ord, PrimitiveId
PrimitiveId -> PrimitiveId -> Bounded PrimitiveId
forall a. a -> a -> Bounded a
$cminBound :: PrimitiveId
minBound :: PrimitiveId
$cmaxBound :: PrimitiveId
maxBound :: PrimitiveId
Bounded, Int -> PrimitiveId
PrimitiveId -> Int
PrimitiveId -> [PrimitiveId]
PrimitiveId -> PrimitiveId
PrimitiveId -> PrimitiveId -> [PrimitiveId]
PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId]
(PrimitiveId -> PrimitiveId)
-> (PrimitiveId -> PrimitiveId)
-> (Int -> PrimitiveId)
-> (PrimitiveId -> Int)
-> (PrimitiveId -> [PrimitiveId])
-> (PrimitiveId -> PrimitiveId -> [PrimitiveId])
-> (PrimitiveId -> PrimitiveId -> [PrimitiveId])
-> (PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId])
-> Enum PrimitiveId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: PrimitiveId -> PrimitiveId
succ :: PrimitiveId -> PrimitiveId
$cpred :: PrimitiveId -> PrimitiveId
pred :: PrimitiveId -> PrimitiveId
$ctoEnum :: Int -> PrimitiveId
toEnum :: Int -> PrimitiveId
$cfromEnum :: PrimitiveId -> Int
fromEnum :: PrimitiveId -> Int
$cenumFrom :: PrimitiveId -> [PrimitiveId]
enumFrom :: PrimitiveId -> [PrimitiveId]
$cenumFromThen :: PrimitiveId -> PrimitiveId -> [PrimitiveId]
enumFromThen :: PrimitiveId -> PrimitiveId -> [PrimitiveId]
$cenumFromTo :: PrimitiveId -> PrimitiveId -> [PrimitiveId]
enumFromTo :: PrimitiveId -> PrimitiveId -> [PrimitiveId]
$cenumFromThenTo :: PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId]
enumFromThenTo :: PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId]
Enum, (forall x. PrimitiveId -> Rep PrimitiveId x)
-> (forall x. Rep PrimitiveId x -> PrimitiveId)
-> Generic PrimitiveId
forall x. Rep PrimitiveId x -> PrimitiveId
forall x. PrimitiveId -> Rep PrimitiveId x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PrimitiveId -> Rep PrimitiveId x
from :: forall x. PrimitiveId -> Rep PrimitiveId x
$cto :: forall x. Rep PrimitiveId x -> PrimitiveId
to :: forall x. Rep PrimitiveId x -> PrimitiveId
Generic)

instance NFData PrimitiveId

instance Hashable PrimitiveId where
  Int
s hashWithSalt :: Int -> PrimitiveId -> Int
`hashWithSalt` PrimitiveId
b = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` PrimitiveId -> Int
forall a. Enum a => a -> Int
fromEnum PrimitiveId
b

instance KillRange PrimitiveId where
  killRange :: PrimitiveId -> PrimitiveId
killRange = PrimitiveId -> PrimitiveId
forall a. a -> a
id

instance Pretty PrimitiveId where
  pretty :: PrimitiveId -> Doc
pretty = String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> (PrimitiveId -> String) -> PrimitiveId -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimitiveId -> String
forall a. IsBuiltin a => a -> String
getBuiltinId

instance IsBuiltin PrimitiveId where
  someBuiltin :: PrimitiveId -> SomeBuiltin
someBuiltin = PrimitiveId -> SomeBuiltin
PrimitiveName

  getBuiltinId :: PrimitiveId -> String
getBuiltinId = \case
    -- Cubical
    PrimitiveId
PrimConId                             -> String
"primConId"
    PrimitiveId
PrimIdElim                            -> String
"primIdElim"
    PrimitiveId
PrimIMin                              -> String
"primIMin"
    PrimitiveId
PrimIMax                              -> String
"primIMax"
    PrimitiveId
PrimINeg                              -> String
"primINeg"
    PrimitiveId
PrimPartial                           -> String
"primPartial"
    PrimitiveId
PrimPartialP                          -> String
"primPartialP"
    PrimitiveId
PrimSubOut                            -> String
"primSubOut"
    PrimitiveId
PrimGlue                              -> String
"primGlue"
    PrimitiveId
Prim_glue                             -> String
"prim^glue"
    PrimitiveId
Prim_unglue                           -> String
"prim^unglue"
    PrimitiveId
Prim_glueU                            -> String
"prim^glueU"
    PrimitiveId
Prim_unglueU                          -> String
"prim^unglueU"
    PrimitiveId
PrimFaceForall                        -> String
"primFaceForall"
    PrimitiveId
PrimComp                              -> String
"primComp"
    PrimitiveId
PrimPOr                               -> String
"primPOr"
    PrimitiveId
PrimTrans                             -> String
"primTransp"
    PrimitiveId
PrimDepIMin                           -> String
"primDepIMin"
    PrimitiveId
PrimIdFace                            -> String
"primIdFace"
    PrimitiveId
PrimIdPath                            -> String
"primIdPath"
    PrimitiveId
PrimHComp                             -> String
"primHComp"
    --  Integer
    PrimitiveId
PrimShowInteger                       -> String
"primShowInteger"
    -- Natural
    PrimitiveId
PrimNatPlus                           -> String
"primNatPlus"
    PrimitiveId
PrimNatMinus                          -> String
"primNatMinus"
    PrimitiveId
PrimNatTimes                          -> String
"primNatTimes"
    PrimitiveId
PrimNatDivSucAux                      -> String
"primNatDivSucAux"
    PrimitiveId
PrimNatModSucAux                      -> String
"primNatModSucAux"
    PrimitiveId
PrimNatEquality                       -> String
"primNatEquality"
    PrimitiveId
PrimNatLess                           -> String
"primNatLess"
    PrimitiveId
PrimShowNat                           -> String
"primShowNat"
    -- Word64
    PrimitiveId
PrimWord64FromNat                     -> String
"primWord64FromNat"
    PrimitiveId
PrimWord64ToNat                       -> String
"primWord64ToNat"
    PrimitiveId
PrimWord64ToNatInjective              -> String
"primWord64ToNatInjective"
    -- Level
    PrimitiveId
PrimLevelZero                         -> String
"primLevelZero"
    PrimitiveId
PrimLevelSuc                          -> String
"primLevelSuc"
    PrimitiveId
PrimLevelMax                          -> String
"primLevelMax"
    -- Float
    PrimitiveId
PrimFloatEquality                     -> String
"primFloatEquality"
    PrimitiveId
PrimFloatInequality                   -> String
"primFloatInequality"
    PrimitiveId
PrimFloatLess                         -> String
"primFloatLess"
    PrimitiveId
PrimFloatIsInfinite                   -> String
"primFloatIsInfinite"
    PrimitiveId
PrimFloatIsNaN                        -> String
"primFloatIsNaN"
    PrimitiveId
PrimFloatIsNegativeZero               -> String
"primFloatIsNegativeZero"
    PrimitiveId
PrimFloatIsSafeInteger                -> String
"primFloatIsSafeInteger"
    PrimitiveId
PrimFloatToWord64                     -> String
"primFloatToWord64"
    PrimitiveId
PrimFloatToWord64Injective            -> String
"primFloatToWord64Injective"
    PrimitiveId
PrimNatToFloat                        -> String
"primNatToFloat"
    PrimitiveId
PrimIntToFloat                        -> String
"primIntToFloat"
    PrimitiveId
PrimFloatRound                        -> String
"primFloatRound"
    PrimitiveId
PrimFloatFloor                        -> String
"primFloatFloor"
    PrimitiveId
PrimFloatCeiling                      -> String
"primFloatCeiling"
    PrimitiveId
PrimFloatToRatio                      -> String
"primFloatToRatio"
    PrimitiveId
PrimRatioToFloat                      -> String
"primRatioToFloat"
    PrimitiveId
PrimFloatDecode                       -> String
"primFloatDecode"
    PrimitiveId
PrimFloatEncode                       -> String
"primFloatEncode"
    PrimitiveId
PrimShowFloat                         -> String
"primShowFloat"
    PrimitiveId
PrimFloatPlus                         -> String
"primFloatPlus"
    PrimitiveId
PrimFloatMinus                        -> String
"primFloatMinus"
    PrimitiveId
PrimFloatTimes                        -> String
"primFloatTimes"
    PrimitiveId
PrimFloatNegate                       -> String
"primFloatNegate"
    PrimitiveId
PrimFloatDiv                          -> String
"primFloatDiv"
    PrimitiveId
PrimFloatPow                          -> String
"primFloatPow"
    PrimitiveId
PrimFloatSqrt                         -> String
"primFloatSqrt"
    PrimitiveId
PrimFloatExp                          -> String
"primFloatExp"
    PrimitiveId
PrimFloatLog                          -> String
"primFloatLog"
    PrimitiveId
PrimFloatSin                          -> String
"primFloatSin"
    PrimitiveId
PrimFloatCos                          -> String
"primFloatCos"
    PrimitiveId
PrimFloatTan                          -> String
"primFloatTan"
    PrimitiveId
PrimFloatASin                         -> String
"primFloatASin"
    PrimitiveId
PrimFloatACos                         -> String
"primFloatACos"
    PrimitiveId
PrimFloatATan                         -> String
"primFloatATan"
    PrimitiveId
PrimFloatATan2                        -> String
"primFloatATan2"
    PrimitiveId
PrimFloatSinh                         -> String
"primFloatSinh"
    PrimitiveId
PrimFloatCosh                         -> String
"primFloatCosh"
    PrimitiveId
PrimFloatTanh                         -> String
"primFloatTanh"
    PrimitiveId
PrimFloatASinh                        -> String
"primFloatASinh"
    PrimitiveId
PrimFloatACosh                        -> String
"primFloatACosh"
    PrimitiveId
PrimFloatATanh                        -> String
"primFloatATanh"
    -- Character
    PrimitiveId
PrimCharEquality                      -> String
"primCharEquality"
    PrimitiveId
PrimIsLower                           -> String
"primIsLower"
    PrimitiveId
PrimIsDigit                           -> String
"primIsDigit"
    PrimitiveId
PrimIsAlpha                           -> String
"primIsAlpha"
    PrimitiveId
PrimIsSpace                           -> String
"primIsSpace"
    PrimitiveId
PrimIsAscii                           -> String
"primIsAscii"
    PrimitiveId
PrimIsLatin1                          -> String
"primIsLatin1"
    PrimitiveId
PrimIsPrint                           -> String
"primIsPrint"
    PrimitiveId
PrimIsHexDigit                        -> String
"primIsHexDigit"
    PrimitiveId
PrimToUpper                           -> String
"primToUpper"
    PrimitiveId
PrimToLower                           -> String
"primToLower"
    PrimitiveId
PrimCharToNat                         -> String
"primCharToNat"
    PrimitiveId
PrimCharToNatInjective                -> String
"primCharToNatInjective"
    PrimitiveId
PrimNatToChar                         -> String
"primNatToChar"
    PrimitiveId
PrimShowChar                          -> String
"primShowChar"
    -- String
    PrimitiveId
PrimStringToList                      -> String
"primStringToList"
    PrimitiveId
PrimStringToListInjective             -> String
"primStringToListInjective"
    PrimitiveId
PrimStringFromList                    -> String
"primStringFromList"
    PrimitiveId
PrimStringFromListInjective           -> String
"primStringFromListInjective"
    PrimitiveId
PrimStringAppend                      -> String
"primStringAppend"
    PrimitiveId
PrimStringEquality                    -> String
"primStringEquality"
    PrimitiveId
PrimShowString                        -> String
"primShowString"
    PrimitiveId
PrimStringUncons                      -> String
"primStringUncons"
    -- "Other stuff"
    PrimitiveId
PrimErase                             -> String
"primErase"
    PrimitiveId
PrimEraseEquality                     -> String
"primEraseEquality"
    PrimitiveId
PrimForce                             -> String
"primForce"
    PrimitiveId
PrimForceLemma                        -> String
"primForceLemma"
    PrimitiveId
PrimQNameEquality                     -> String
"primQNameEquality"
    PrimitiveId
PrimQNameLess                         -> String
"primQNameLess"
    PrimitiveId
PrimShowQName                         -> String
"primShowQName"
    PrimitiveId
PrimQNameFixity                       -> String
"primQNameFixity"
    PrimitiveId
PrimQNameToWord64s                    -> String
"primQNameToWord64s"
    PrimitiveId
PrimQNameToWord64sInjective           -> String
"primQNameToWord64sInjective"
    PrimitiveId
PrimMetaEquality                      -> String
"primMetaEquality"
    PrimitiveId
PrimMetaLess                          -> String
"primMetaLess"
    PrimitiveId
PrimShowMeta                          -> String
"primShowMeta"
    PrimitiveId
PrimMetaToNat                         -> String
"primMetaToNat"
    PrimitiveId
PrimMetaToNatInjective                -> String
"primMetaToNatInjective"
    PrimitiveId
PrimLockUniv                          -> String
"primLockUniv"

builtinConId, builtinIdElim, builtinSubOut,
  builtinIMin, builtinIMax, builtinINeg,
  builtinGlue, builtin_glue, builtin_unglue, builtin_glueU, builtin_unglueU,
  builtinFaceForall, builtinComp, builtinPOr,
  builtinTrans,  builtinDepIMin,
  builtinIdFace, builtinIdPath, builtinHComp, builtinLockUniv
  :: PrimitiveId
builtinConId :: PrimitiveId
builtinConId                             = PrimitiveId
PrimConId
builtinIdElim :: PrimitiveId
builtinIdElim                            = PrimitiveId
PrimIdElim
builtinIMin :: PrimitiveId
builtinIMin                              = PrimitiveId
PrimIMin
builtinIMax :: PrimitiveId
builtinIMax                              = PrimitiveId
PrimIMax
builtinINeg :: PrimitiveId
builtinINeg                              = PrimitiveId
PrimINeg
builtinSubOut :: PrimitiveId
builtinSubOut                            = PrimitiveId
PrimSubOut
builtinGlue :: PrimitiveId
builtinGlue                              = PrimitiveId
PrimGlue
builtin_glue :: PrimitiveId
builtin_glue                             = PrimitiveId
Prim_glue
builtin_unglue :: PrimitiveId
builtin_unglue                           = PrimitiveId
Prim_unglue
builtin_glueU :: PrimitiveId
builtin_glueU                            = PrimitiveId
Prim_glueU
builtin_unglueU :: PrimitiveId
builtin_unglueU                          = PrimitiveId
Prim_unglueU
builtinFaceForall :: PrimitiveId
builtinFaceForall                        = PrimitiveId
PrimFaceForall
builtinComp :: PrimitiveId
builtinComp                              = PrimitiveId
PrimComp
builtinPOr :: PrimitiveId
builtinPOr                               = PrimitiveId
PrimPOr
builtinTrans :: PrimitiveId
builtinTrans                             = PrimitiveId
PrimTrans
builtinDepIMin :: PrimitiveId
builtinDepIMin                           = PrimitiveId
PrimDepIMin
builtinIdFace :: PrimitiveId
builtinIdFace                            = PrimitiveId
PrimIdFace
builtinIdPath :: PrimitiveId
builtinIdPath                            = PrimitiveId
PrimIdPath
builtinHComp :: PrimitiveId
builtinHComp                             = PrimitiveId
PrimHComp
builtinLockUniv :: PrimitiveId
builtinLockUniv                          = PrimitiveId
PrimLockUniv

-- | Lookup a primitive by its identifier.
primitiveById :: String -> Maybe PrimitiveId
primitiveById :: String -> Maybe PrimitiveId
primitiveById = (String -> Map String PrimitiveId -> Maybe PrimitiveId)
-> Map String PrimitiveId -> String -> Maybe PrimitiveId
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> Map String PrimitiveId -> Maybe PrimitiveId
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Map String PrimitiveId
m where
  m :: Map String PrimitiveId
m = [(String, PrimitiveId)] -> Map String PrimitiveId
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(PrimitiveId -> String
forall a. IsBuiltin a => a -> String
getBuiltinId PrimitiveId
x, PrimitiveId
x) | PrimitiveId
x <- [(PrimitiveId
forall a. Bounded a => a
minBound :: PrimitiveId)..]]