{-# 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 Mikan.Syntax.Builtin where

import GHC.Generics (Generic)

import Control.DeepSeq (NFData)

import Data.Map qualified as M
import Data.Hashable
import Data.Text.Short (ShortText)

import Mikan.Syntax.Common.Pretty
import Mikan.Syntax.Position

import Mikan.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 -> ShortText

instance IsBuiltin SomeBuiltin where
  someBuiltin :: SomeBuiltin -> SomeBuiltin
someBuiltin = SomeBuiltin -> SomeBuiltin
forall a. a -> a
id

  getBuiltinId :: SomeBuiltin -> ShortText
getBuiltinId (BuiltinName BuiltinId
x) = BuiltinId -> ShortText
forall a. IsBuiltin a => a -> ShortText
getBuiltinId BuiltinId
x
  getBuiltinId (PrimitiveName PrimitiveId
x) = PrimitiveId -> ShortText
forall a. IsBuiltin a => a -> ShortText
getBuiltinId PrimitiveId
x

-- * Builtins

-- | A builtin name, defined by the @BUILTIN@ pragma.
data BuiltinId
  = BuiltinNat
  | BuiltinSuc
  | BuiltinZero
  | BuiltinNatPlus
  | BuiltinNatMinus
  | BuiltinNatTimes
  | BuiltinNatDivSucAux
  | BuiltinNatModSucAux
  | BuiltinNatEquals
  | BuiltinNatLess
  | BuiltinInteger
  | BuiltinIntegerPos
  | BuiltinIntegerNegSuc
  | BuiltinFloat
  | BuiltinChar
  | BuiltinString
  | BuiltinUnit
  | BuiltinUnitUnit
  | BuiltinSigma
  | BuiltinSigmaCon
  | BuiltinBool
  | BuiltinTrue
  | BuiltinFalse
  | BuiltinList
  | BuiltinNil
  | BuiltinCons
  | BuiltinMaybe
  | BuiltinNothing
  | BuiltinJust
  | BuiltinPath
  | BuiltinPathP
  | BuiltinIntervalUniv
  | BuiltinInterval
  | BuiltinIZero
  | BuiltinIOne
  | BuiltinPartial
  | BuiltinPartialP
  | BuiltinIsOne
  | BuiltinItIsOne
  | BuiltinEquiv
  | BuiltinEquivFun
  | BuiltinEquivProof
  | BuiltinTranspProof
  | BuiltinIsOne1
  | BuiltinIsOne2
  | BuiltinIsOneEmpty
  | BuiltinSub
  | BuiltinSubIn
  | BuiltinEquality
  | BuiltinRefl
  | BuiltinLevelMax
  | BuiltinLevel
  | BuiltinLevelZero
  | BuiltinLevelSuc
  | BuiltinProp
  | BuiltinType
  | BuiltinStrictSet
  | BuiltinPropOmega
  | BuiltinTypeOmega
  | BuiltinSSetOmega
  | BuiltinLevelUniv
  | BuiltinCofUniv
  | BuiltinFromNat
  | BuiltinFromNeg
  | BuiltinFromString
  | BuiltinQName
  | BuiltinAgdaSort
  | BuiltinAgdaSortType
  | BuiltinAgdaSortLit
  | BuiltinAgdaSortProp
  | BuiltinAgdaSortPropLit
  | BuiltinAgdaSortInf
  | BuiltinAgdaSortUnsupported
  | BuiltinHiding
  | BuiltinHidden
  | BuiltinInstance
  | BuiltinVisible
  | 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
  | 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
  | BuiltinAgdaTCMCheckFromString
  | BuiltinAgdaTCMGetInstances
  | BuiltinAgdaTCMSolveInstances
  | 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 = ShortText -> Doc
forall a. Pretty a => a -> Doc
pretty (ShortText -> Doc) -> (BuiltinId -> ShortText) -> BuiltinId -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinId -> ShortText
forall a. IsBuiltin a => a -> ShortText
getBuiltinId

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

  getBuiltinId :: BuiltinId -> ShortText
getBuiltinId = \case
    BuiltinId
BuiltinNat                               -> ShortText
"NATURAL"
    BuiltinId
BuiltinSuc                               -> ShortText
"SUC"
    BuiltinId
BuiltinZero                              -> ShortText
"ZERO"
    BuiltinId
BuiltinNatPlus                           -> ShortText
"NATPLUS"
    BuiltinId
BuiltinNatMinus                          -> ShortText
"NATMINUS"
    BuiltinId
BuiltinNatTimes                          -> ShortText
"NATTIMES"
    BuiltinId
BuiltinNatDivSucAux                      -> ShortText
"NATDIVSUCAUX"
    BuiltinId
BuiltinNatModSucAux                      -> ShortText
"NATMODSUCAUX"
    BuiltinId
BuiltinNatEquals                         -> ShortText
"NATEQUALS"
    BuiltinId
BuiltinNatLess                           -> ShortText
"NATLESS"
    BuiltinId
BuiltinInteger                           -> ShortText
"INTEGER"
    BuiltinId
BuiltinIntegerPos                        -> ShortText
"INTEGERPOS"
    BuiltinId
BuiltinIntegerNegSuc                     -> ShortText
"INTEGERNEGSUC"
    BuiltinId
BuiltinFloat                             -> ShortText
"FLOAT"
    BuiltinId
BuiltinChar                              -> ShortText
"CHAR"
    BuiltinId
BuiltinString                            -> ShortText
"STRING"
    BuiltinId
BuiltinUnit                              -> ShortText
"UNIT"
    BuiltinId
BuiltinUnitUnit                          -> ShortText
"UNITUNIT"
    BuiltinId
BuiltinSigma                             -> ShortText
"SIGMA"
    BuiltinId
BuiltinSigmaCon                          -> ShortText
"SIGMACON"
    BuiltinId
BuiltinBool                              -> ShortText
"BOOL"
    BuiltinId
BuiltinTrue                              -> ShortText
"TRUE"
    BuiltinId
BuiltinFalse                             -> ShortText
"FALSE"
    BuiltinId
BuiltinList                              -> ShortText
"LIST"
    BuiltinId
BuiltinNil                               -> ShortText
"NIL"
    BuiltinId
BuiltinCons                              -> ShortText
"CONS"
    BuiltinId
BuiltinMaybe                             -> ShortText
"MAYBE"
    BuiltinId
BuiltinNothing                           -> ShortText
"NOTHING"
    BuiltinId
BuiltinJust                              -> ShortText
"JUST"
    BuiltinId
BuiltinPath                              -> ShortText
"PATH"
    BuiltinId
BuiltinPathP                             -> ShortText
"PATHP"
    BuiltinId
BuiltinIntervalUniv                      -> ShortText
"CUBEINTERVALUNIV"
    BuiltinId
BuiltinInterval                          -> ShortText
"INTERVAL"
    BuiltinId
BuiltinIZero                             -> ShortText
"IZERO"
    BuiltinId
BuiltinIOne                              -> ShortText
"IONE"
    BuiltinId
BuiltinPartial                           -> ShortText
"PARTIAL"
    BuiltinId
BuiltinPartialP                          -> ShortText
"PARTIALP"
    BuiltinId
BuiltinIsOne                             -> ShortText
"ISONE"
    BuiltinId
BuiltinItIsOne                           -> ShortText
"ITISONE"
    BuiltinId
BuiltinEquiv                             -> ShortText
"EQUIV"
    BuiltinId
BuiltinEquivFun                          -> ShortText
"EQUIVFUN"
    BuiltinId
BuiltinEquivProof                        -> ShortText
"EQUIVPROOF"
    BuiltinId
BuiltinTranspProof                       -> ShortText
"TRANSPPROOF"
    BuiltinId
BuiltinIsOne1                            -> ShortText
"ISONE1"
    BuiltinId
BuiltinIsOne2                            -> ShortText
"ISONE2"
    BuiltinId
BuiltinIsOneEmpty                        -> ShortText
"ISONEEMPTY"
    BuiltinId
BuiltinSub                               -> ShortText
"SUB"
    BuiltinId
BuiltinSubIn                             -> ShortText
"SUBIN"
    BuiltinId
BuiltinEquality                          -> ShortText
"EQUALITY"
    BuiltinId
BuiltinRefl                              -> ShortText
"REFL"
    BuiltinId
BuiltinLevelMax                          -> ShortText
"LEVELMAX"
    BuiltinId
BuiltinLevel                             -> ShortText
"LEVEL"
    BuiltinId
BuiltinLevelZero                         -> ShortText
"LEVELZERO"
    BuiltinId
BuiltinLevelSuc                          -> ShortText
"LEVELSUC"
    BuiltinId
BuiltinProp                              -> ShortText
"PROP"
    BuiltinId
BuiltinType                              -> ShortText
"TYPE"
    BuiltinId
BuiltinStrictSet                         -> ShortText
"STRICTSET"
    BuiltinId
BuiltinPropOmega                         -> ShortText
"PROPOMEGA"
    BuiltinId
BuiltinTypeOmega                         -> ShortText
"TYPEOMEGA"
    BuiltinId
BuiltinSSetOmega                         -> ShortText
"STRICTSETOMEGA"
    BuiltinId
BuiltinLevelUniv                         -> ShortText
"LEVELUNIV"
    BuiltinId
BuiltinCofUniv                           -> ShortText
"COFUNIV"
    BuiltinId
BuiltinFromNat                           -> ShortText
"FROMNAT"
    BuiltinId
BuiltinFromNeg                           -> ShortText
"FROMNEG"
    BuiltinId
BuiltinFromString                        -> ShortText
"FROMSTRING"
    BuiltinId
BuiltinQName                             -> ShortText
"QNAME"
    BuiltinId
BuiltinAgdaSort                          -> ShortText
"AGDASORT"
    BuiltinId
BuiltinAgdaSortType                      -> ShortText
"AGDASORTTYPE"
    BuiltinId
BuiltinAgdaSortLit                       -> ShortText
"AGDASORTLIT"
    BuiltinId
BuiltinAgdaSortProp                      -> ShortText
"AGDASORTPROP"
    BuiltinId
BuiltinAgdaSortPropLit                   -> ShortText
"AGDASORTPROPLIT"
    BuiltinId
BuiltinAgdaSortInf                       -> ShortText
"AGDASORTINF"
    BuiltinId
BuiltinAgdaSortUnsupported               -> ShortText
"AGDASORTUNSUPPORTED"
    BuiltinId
BuiltinHiding                            -> ShortText
"HIDING"
    BuiltinId
BuiltinHidden                            -> ShortText
"HIDDEN"
    BuiltinId
BuiltinInstance                          -> ShortText
"INSTANCE"
    BuiltinId
BuiltinVisible                           -> ShortText
"VISIBLE"
    BuiltinId
BuiltinAssoc                             -> ShortText
"ASSOC"
    BuiltinId
BuiltinAssocLeft                         -> ShortText
"ASSOCLEFT"
    BuiltinId
BuiltinAssocRight                        -> ShortText
"ASSOCRIGHT"
    BuiltinId
BuiltinAssocNon                          -> ShortText
"ASSOCNON"
    BuiltinId
BuiltinPrecedence                        -> ShortText
"PRECEDENCE"
    BuiltinId
BuiltinPrecRelated                       -> ShortText
"PRECRELATED"
    BuiltinId
BuiltinPrecUnrelated                     -> ShortText
"PRECUNRELATED"
    BuiltinId
BuiltinFixity                            -> ShortText
"FIXITY"
    BuiltinId
BuiltinFixityFixity                      -> ShortText
"FIXITYFIXITY"
    BuiltinId
BuiltinArg                               -> ShortText
"ARG"
    BuiltinId
BuiltinArgInfo                           -> ShortText
"ARGINFO"
    BuiltinId
BuiltinArgArgInfo                        -> ShortText
"ARGARGINFO"
    BuiltinId
BuiltinArgArg                            -> ShortText
"ARGARG"
    BuiltinId
BuiltinAbs                               -> ShortText
"ABS"
    BuiltinId
BuiltinAbsAbs                            -> ShortText
"ABSABS"
    BuiltinId
BuiltinAgdaTerm                          -> ShortText
"AGDATERM"
    BuiltinId
BuiltinAgdaTermVar                       -> ShortText
"AGDATERMVAR"
    BuiltinId
BuiltinAgdaTermLam                       -> ShortText
"AGDATERMLAM"
    BuiltinId
BuiltinAgdaTermExtLam                    -> ShortText
"AGDATERMEXTLAM"
    BuiltinId
BuiltinAgdaTermDef                       -> ShortText
"AGDATERMDEF"
    BuiltinId
BuiltinAgdaTermCon                       -> ShortText
"AGDATERMCON"
    BuiltinId
BuiltinAgdaTermPi                        -> ShortText
"AGDATERMPI"
    BuiltinId
BuiltinAgdaTermSort                      -> ShortText
"AGDATERMSORT"
    BuiltinId
BuiltinAgdaTermLit                       -> ShortText
"AGDATERMLIT"
    BuiltinId
BuiltinAgdaTermUnsupported               -> ShortText
"AGDATERMUNSUPPORTED"
    BuiltinId
BuiltinAgdaTermMeta                      -> ShortText
"AGDATERMMETA"
    BuiltinId
BuiltinAgdaErrorPart                     -> ShortText
"AGDAERRORPART"
    BuiltinId
BuiltinAgdaErrorPartString               -> ShortText
"AGDAERRORPARTSTRING"
    BuiltinId
BuiltinAgdaErrorPartTerm                 -> ShortText
"AGDAERRORPARTTERM"
    BuiltinId
BuiltinAgdaErrorPartPatt                 -> ShortText
"AGDAERRORPARTPATT"
    BuiltinId
BuiltinAgdaErrorPartName                 -> ShortText
"AGDAERRORPARTNAME"
    BuiltinId
BuiltinAgdaLiteral                       -> ShortText
"AGDALITERAL"
    BuiltinId
BuiltinAgdaLitNat                        -> ShortText
"AGDALITNAT"
    BuiltinId
BuiltinAgdaLitFloat                      -> ShortText
"AGDALITFLOAT"
    BuiltinId
BuiltinAgdaLitChar                       -> ShortText
"AGDALITCHAR"
    BuiltinId
BuiltinAgdaLitString                     -> ShortText
"AGDALITSTRING"
    BuiltinId
BuiltinAgdaLitQName                      -> ShortText
"AGDALITQNAME"
    BuiltinId
BuiltinAgdaLitMeta                       -> ShortText
"AGDALITMETA"
    BuiltinId
BuiltinAgdaClause                        -> ShortText
"AGDACLAUSE"
    BuiltinId
BuiltinAgdaClauseClause                  -> ShortText
"AGDACLAUSECLAUSE"
    BuiltinId
BuiltinAgdaClauseAbsurd                  -> ShortText
"AGDACLAUSEABSURD"
    BuiltinId
BuiltinAgdaPattern                       -> ShortText
"AGDAPATTERN"
    BuiltinId
BuiltinAgdaPatVar                        -> ShortText
"AGDAPATVAR"
    BuiltinId
BuiltinAgdaPatCon                        -> ShortText
"AGDAPATCON"
    BuiltinId
BuiltinAgdaPatDot                        -> ShortText
"AGDAPATDOT"
    BuiltinId
BuiltinAgdaPatLit                        -> ShortText
"AGDAPATLIT"
    BuiltinId
BuiltinAgdaPatProj                       -> ShortText
"AGDAPATPROJ"
    BuiltinId
BuiltinAgdaPatAbsurd                     -> ShortText
"AGDAPATABSURD"
    BuiltinId
BuiltinAgdaDefinitionFunDef              -> ShortText
"AGDADEFINITIONFUNDEF"
    BuiltinId
BuiltinAgdaDefinitionDataDef             -> ShortText
"AGDADEFINITIONDATADEF"
    BuiltinId
BuiltinAgdaDefinitionRecordDef           -> ShortText
"AGDADEFINITIONRECORDDEF"
    BuiltinId
BuiltinAgdaDefinitionDataConstructor     -> ShortText
"AGDADEFINITIONDATACONSTRUCTOR"
    BuiltinId
BuiltinAgdaDefinitionPostulate           -> ShortText
"AGDADEFINITIONPOSTULATE"
    BuiltinId
BuiltinAgdaDefinitionPrimitive           -> ShortText
"AGDADEFINITIONPRIMITIVE"
    BuiltinId
BuiltinAgdaDefinition                    -> ShortText
"AGDADEFINITION"
    BuiltinId
BuiltinAgdaMeta                          -> ShortText
"AGDAMETA"
    BuiltinId
BuiltinAgdaTCM                           -> ShortText
"AGDATCM"
    BuiltinId
BuiltinAgdaTCMReturn                     -> ShortText
"AGDATCMRETURN"
    BuiltinId
BuiltinAgdaTCMBind                       -> ShortText
"AGDATCMBIND"
    BuiltinId
BuiltinAgdaTCMUnify                      -> ShortText
"AGDATCMUNIFY"
    BuiltinId
BuiltinAgdaTCMTypeError                  -> ShortText
"AGDATCMTYPEERROR"
    BuiltinId
BuiltinAgdaTCMInferType                  -> ShortText
"AGDATCMINFERTYPE"
    BuiltinId
BuiltinAgdaTCMCheckType                  -> ShortText
"AGDATCMCHECKTYPE"
    BuiltinId
BuiltinAgdaTCMNormalise                  -> ShortText
"AGDATCMNORMALISE"
    BuiltinId
BuiltinAgdaTCMReduce                     -> ShortText
"AGDATCMREDUCE"
    BuiltinId
BuiltinAgdaTCMCatchError                 -> ShortText
"AGDATCMCATCHERROR"
    BuiltinId
BuiltinAgdaTCMGetContext                 -> ShortText
"AGDATCMGETCONTEXT"
    BuiltinId
BuiltinAgdaTCMExtendContext              -> ShortText
"AGDATCMEXTENDCONTEXT"
    BuiltinId
BuiltinAgdaTCMInContext                  -> ShortText
"AGDATCMINCONTEXT"
    BuiltinId
BuiltinAgdaTCMFreshName                  -> ShortText
"AGDATCMFRESHNAME"
    BuiltinId
BuiltinAgdaTCMDeclareDef                 -> ShortText
"AGDATCMDECLAREDEF"
    BuiltinId
BuiltinAgdaTCMDeclarePostulate           -> ShortText
"AGDATCMDECLAREPOSTULATE"
    BuiltinId
BuiltinAgdaTCMDeclareData                -> ShortText
"AGDATCMDECLAREDATA"
    BuiltinId
BuiltinAgdaTCMDefineData                 -> ShortText
"AGDATCMDEFINEDATA"
    BuiltinId
BuiltinAgdaTCMDefineFun                  -> ShortText
"AGDATCMDEFINEFUN"
    BuiltinId
BuiltinAgdaTCMGetType                    -> ShortText
"AGDATCMGETTYPE"
    BuiltinId
BuiltinAgdaTCMGetDefinition              -> ShortText
"AGDATCMGETDEFINITION"
    BuiltinId
BuiltinAgdaTCMBlock                      -> ShortText
"AGDATCMBLOCK"
    BuiltinId
BuiltinAgdaTCMCommit                     -> ShortText
"AGDATCMCOMMIT"
    BuiltinId
BuiltinAgdaTCMQuoteTerm                  -> ShortText
"AGDATCMQUOTETERM"
    BuiltinId
BuiltinAgdaTCMUnquoteTerm                -> ShortText
"AGDATCMUNQUOTETERM"
    BuiltinId
BuiltinAgdaTCMQuoteOmegaTerm             -> ShortText
"AGDATCMQUOTEOMEGATERM"
    BuiltinId
BuiltinAgdaTCMIsMacro                    -> ShortText
"AGDATCMISMACRO"
    BuiltinId
BuiltinAgdaTCMWithNormalisation          -> ShortText
"AGDATCMWITHNORMALISATION"
    BuiltinId
BuiltinAgdaTCMWithReconstructed          -> ShortText
"AGDATCMWITHRECONSTRUCTED"
    BuiltinId
BuiltinAgdaTCMWithExpandLast             -> ShortText
"AGDATCMWITHEXPANDLAST"
    BuiltinId
BuiltinAgdaTCMWithReduceDefs             -> ShortText
"AGDATCMWITHREDUCEDEFS"
    BuiltinId
BuiltinAgdaTCMAskNormalisation           -> ShortText
"AGDATCMASKNORMALISATION"
    BuiltinId
BuiltinAgdaTCMAskReconstructed           -> ShortText
"AGDATCMASKRECONSTRUCTED"
    BuiltinId
BuiltinAgdaTCMAskExpandLast              -> ShortText
"AGDATCMASKEXPANDLAST"
    BuiltinId
BuiltinAgdaTCMAskReduceDefs              -> ShortText
"AGDATCMASKREDUCEDEFS"
    BuiltinId
BuiltinAgdaTCMFormatErrorParts           -> ShortText
"AGDATCMFORMATERRORPARTS"
    BuiltinId
BuiltinAgdaTCMDebugPrint                 -> ShortText
"AGDATCMDEBUGPRINT"
    BuiltinId
BuiltinAgdaTCMNoConstraints              -> ShortText
"AGDATCMNOCONSTRAINTS"
    BuiltinId
BuiltinAgdaTCMRunSpeculative             -> ShortText
"AGDATCMRUNSPECULATIVE"
    BuiltinId
BuiltinAgdaTCMExec                       -> ShortText
"AGDATCMEXEC"
    BuiltinId
BuiltinAgdaTCMCheckFromString            -> ShortText
"AGDATCMCHECKFROMSTRING"
    BuiltinId
BuiltinAgdaTCMGetInstances               -> ShortText
"AGDATCMGETINSTANCES"
    BuiltinId
BuiltinAgdaTCMSolveInstances             -> ShortText
"AGDATCMSOLVEINSTANCES"
    BuiltinId
BuiltinAgdaTCMPragmaForeign              -> ShortText
"AGDATCMPRAGMAFOREIGN"
    BuiltinId
BuiltinAgdaTCMPragmaCompile              -> ShortText
"AGDATCMPRAGMACOMPILE"
    BuiltinId
BuiltinAgdaBlocker                       -> ShortText
"AGDABLOCKER"
    BuiltinId
BuiltinAgdaBlockerAny                    -> ShortText
"AGDABLOCKERANY"
    BuiltinId
BuiltinAgdaBlockerAll                    -> ShortText
"AGDABLOCKERALL"
    BuiltinId
BuiltinAgdaBlockerMeta                   -> ShortText
"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 @Type@.
--
--     {-# BUILTIN TYPE Type #-}
--
--   The type of @Type@ would be @Type : Level → Typeω@
--   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
builtinIntervalUniv
  , BuiltinId
builtinInterval
  , BuiltinId
builtinPartial
  , BuiltinId
builtinPartialP
  , BuiltinId
builtinIsOne
  , BuiltinId
builtinSub
  , BuiltinId
builtinIZero
  , BuiltinId
builtinIOne
  , BuiltinId
builtinProp
  , BuiltinId
builtinType
  , BuiltinId
builtinStrictSet
  , BuiltinId
builtinPropOmega
  , BuiltinId
builtinTypeOmega
  , BuiltinId
builtinSSetOmega
  , BuiltinId
builtinLevelUniv
  , BuiltinId
builtinCofUniv
  ]

builtinNat, builtinSuc, builtinZero, builtinNatPlus, builtinNatMinus,
  builtinNatTimes, builtinNatDivSucAux, builtinNatModSucAux, builtinNatEquals,
  builtinNatLess, builtinInteger, builtinIntegerPos, builtinIntegerNegSuc,
  builtinFloat, builtinChar, builtinString, builtinUnit, builtinUnitUnit,
  builtinSigma,
  builtinBool, builtinTrue, builtinFalse,
  builtinList, builtinNil, builtinCons,
  builtinMaybe, builtinNothing, builtinJust,
  builtinPath, builtinPathP, builtinInterval, builtinIZero, builtinIOne, builtinPartial, builtinPartialP,
  builtinIsOne,  builtinItIsOne, builtinIsOne1, builtinIsOne2, builtinIsOneEmpty,
  builtinSub, builtinSubIn,
  builtinEquiv, builtinEquivFun, builtinEquivProof,
  builtinTranspProof,
  builtinEquality, builtinRefl, builtinLevelMax,
  builtinLevel, builtinLevelZero, builtinLevelSuc,
  builtinProp, builtinType, builtinStrictSet,
  builtinPropOmega, builtinTypeOmega, builtinSSetOmega,
  builtinLevelUniv,
  builtinCofUniv,
  builtinIntervalUniv,
  builtinFromNat, builtinFromNeg, builtinFromString,
  builtinQName, builtinAgdaSort, builtinAgdaSortType, builtinAgdaSortLit,
  builtinAgdaSortProp, builtinAgdaSortPropLit, builtinAgdaSortInf,
  builtinAgdaSortUnsupported,
  builtinHiding, builtinHidden, builtinInstance, builtinVisible,
  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, 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,
  builtinAgdaTCMCheckFromString,
  builtinAgdaTCMGetInstances,
  builtinAgdaTCMSolveInstances,
  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
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
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
builtinEquality :: BuiltinId
builtinEquality                          = BuiltinId
BuiltinEquality
builtinRefl :: BuiltinId
builtinRefl                              = BuiltinId
BuiltinRefl
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
builtinType :: BuiltinId
builtinType                              = BuiltinId
BuiltinType
builtinStrictSet :: BuiltinId
builtinStrictSet                         = BuiltinId
BuiltinStrictSet
builtinPropOmega :: BuiltinId
builtinPropOmega                         = BuiltinId
BuiltinPropOmega
builtinTypeOmega :: BuiltinId
builtinTypeOmega                         = BuiltinId
BuiltinTypeOmega
builtinSSetOmega :: BuiltinId
builtinSSetOmega                         = BuiltinId
BuiltinSSetOmega
builtinLevelUniv :: BuiltinId
builtinLevelUniv                         = BuiltinId
BuiltinLevelUniv
builtinCofUniv :: BuiltinId
builtinCofUniv                           = BuiltinId
BuiltinCofUniv
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
builtinAgdaSortType :: BuiltinId
builtinAgdaSortType                      = BuiltinId
BuiltinAgdaSortType
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
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
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
builtinAgdaTCMCheckFromString :: BuiltinId
builtinAgdaTCMCheckFromString            = BuiltinId
BuiltinAgdaTCMCheckFromString
builtinAgdaTCMGetInstances :: BuiltinId
builtinAgdaTCMGetInstances               = BuiltinId
BuiltinAgdaTCMGetInstances
builtinAgdaTCMSolveInstances :: BuiltinId
builtinAgdaTCMSolveInstances             = BuiltinId
BuiltinAgdaTCMSolveInstances
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 :: ShortText -> Maybe BuiltinId
builtinById :: ShortText -> Maybe BuiltinId
builtinById = (ShortText -> Map ShortText BuiltinId -> Maybe BuiltinId)
-> Map ShortText BuiltinId -> ShortText -> Maybe BuiltinId
forall a b c. (a -> b -> c) -> b -> a -> c
flip ShortText -> Map ShortText BuiltinId -> Maybe BuiltinId
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Map ShortText BuiltinId
m where
  m :: Map ShortText BuiltinId
m = [(ShortText, BuiltinId)] -> Map ShortText BuiltinId
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(BuiltinId -> ShortText
forall a. IsBuiltin a => a -> ShortText
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
  = 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
  -- Level
  | PrimLevelZero
  | PrimLevelSuc
  | PrimLevelMax
  -- Float
  | PrimFloatEquality
  | PrimFloatInequality
  | PrimFloatLess
  | PrimFloatIsInfinite
  | PrimFloatIsNaN
  | PrimFloatIsNegativeZero
  | PrimFloatIsSafeInteger
  | 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"
  | PrimForce
  | PrimForceLemma
  | PrimQNameEquality
  | PrimQNameLess
  | PrimShowQName
  | PrimQNameFixity
  | PrimMetaEquality
  | PrimMetaLess
  | PrimShowMeta
  | PrimMetaToNat
  | PrimMetaToNatInjective
  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 = ShortText -> Doc
forall a. Pretty a => a -> Doc
pretty (ShortText -> Doc)
-> (PrimitiveId -> ShortText) -> PrimitiveId -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimitiveId -> ShortText
forall a. IsBuiltin a => a -> ShortText
getBuiltinId

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

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

builtinSubOut,
  builtinIMin, builtinIMax, builtinINeg,
  builtinGlue, builtin_glue, builtin_unglue, builtin_glueU, builtin_unglueU,
  builtinFaceForall, builtinComp, builtinPOr,
  builtinTrans,  builtinHComp
  :: PrimitiveId
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
builtinHComp :: PrimitiveId
builtinHComp                             = PrimitiveId
PrimHComp

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