{-# OPTIONS_GHC -Wunused-imports #-}
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
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
class IsBuiltin a where
someBuiltin :: a -> SomeBuiltin
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
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
| BuiltinAgdaTCMWorkOnTypes
| BuiltinAgdaTCMRunSpeculative
| BuiltinAgdaTCMExec
| 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 = 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
BuiltinAgdaTCMWorkOnTypes -> String
"AGDATCMWORKONTYPES"
BuiltinId
BuiltinAgdaTCMRunSpeculative -> String
"AGDATCMRUNSPECULATIVE"
BuiltinId
BuiltinAgdaTCMExec -> String
"AGDATCMEXEC"
BuiltinId
BuiltinAgdaTCMGetInstances -> String
"AGDATCMGETINSTANCES"
BuiltinId
BuiltinAgdaTCMSolveInstances -> String
"AGDATCMSOLVEINSTANCES"
BuiltinId
BuiltinAgdaTCMPragmaForeign -> String
"AGDATCMPRAGMAFOREIGN"
BuiltinId
BuiltinAgdaTCMPragmaCompile -> String
"AGDATCMPRAGMACOMPILE"
BuiltinId
BuiltinAgdaBlocker -> String
"AGDABLOCKER"
BuiltinId
BuiltinAgdaBlockerAny -> String
"AGDABLOCKERANY"
BuiltinId
BuiltinAgdaBlockerAll -> String
"AGDABLOCKERALL"
BuiltinId
BuiltinAgdaBlockerMeta -> String
"AGDABLOCKERMETA"
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]
++
[ 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,
builtinAgdaTCMWorkOnTypes,
builtinAgdaTCMRunSpeculative,
builtinAgdaTCMExec,
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
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
builtinAgdaTCMWorkOnTypes :: BuiltinId
builtinAgdaTCMWorkOnTypes = BuiltinId
BuiltinAgdaTCMWorkOnTypes
builtinAgdaTCMRunSpeculative :: BuiltinId
builtinAgdaTCMRunSpeculative = BuiltinId
BuiltinAgdaTCMRunSpeculative
builtinAgdaTCMExec :: BuiltinId
builtinAgdaTCMExec = BuiltinId
BuiltinAgdaTCMExec
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
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)..]]
data PrimitiveId
= 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
| PrimShowInteger
| PrimNatPlus
| PrimNatMinus
| PrimNatTimes
| PrimNatDivSucAux
| PrimNatModSucAux
| PrimNatEquality
| PrimNatLess
| PrimShowNat
| PrimWord64FromNat
| PrimWord64ToNat
| PrimWord64ToNatInjective
| PrimLevelZero
| PrimLevelSuc
| PrimLevelMax
| 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
| PrimCharEquality
| PrimIsLower
| PrimIsDigit
| PrimIsAlpha
| PrimIsSpace
| PrimIsAscii
| PrimIsLatin1
| PrimIsPrint
| PrimIsHexDigit
| PrimToUpper
| PrimToLower
| PrimCharToNat
| PrimCharToNatInjective
| PrimNatToChar
| PrimShowChar
| PrimStringToList
| PrimStringToListInjective
| PrimStringFromList
| PrimStringFromListInjective
| PrimStringAppend
| PrimStringEquality
| PrimShowString
| PrimStringUncons
| 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
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"
PrimitiveId
PrimShowInteger -> String
"primShowInteger"
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"
PrimitiveId
PrimWord64FromNat -> String
"primWord64FromNat"
PrimitiveId
PrimWord64ToNat -> String
"primWord64ToNat"
PrimitiveId
PrimWord64ToNatInjective -> String
"primWord64ToNatInjective"
PrimitiveId
PrimLevelZero -> String
"primLevelZero"
PrimitiveId
PrimLevelSuc -> String
"primLevelSuc"
PrimitiveId
PrimLevelMax -> String
"primLevelMax"
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"
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"
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"
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
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)..]]