module Agda.TypeChecking.Monad.Builtin
( module Agda.TypeChecking.Monad.Builtin
, module Agda.Syntax.Builtin
) where
import qualified Control.Monad.Fail as Fail
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Maybe
import Control.Monad.Writer
import qualified Data.Map as Map
import Data.Function ( on )
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Builtin
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Substitute
import Agda.Utils.Except
import Agda.Utils.ListT
import Agda.Utils.Monad
import Agda.Utils.Maybe
import Agda.Utils.Tuple
import Agda.Utils.Impossible
class ( Functor m
, Applicative m
, Fail.MonadFail m
) => HasBuiltins m where
getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))
instance HasBuiltins m => HasBuiltins (MaybeT m) where
getBuiltinThing b = lift $ getBuiltinThing b
instance HasBuiltins m => HasBuiltins (ExceptT e m) where
getBuiltinThing b = lift $ getBuiltinThing b
instance HasBuiltins m => HasBuiltins (ListT m) where
getBuiltinThing b = lift $ getBuiltinThing b
instance HasBuiltins m => HasBuiltins (ReaderT e m) where
getBuiltinThing b = lift $ getBuiltinThing b
instance HasBuiltins m => HasBuiltins (StateT s m) where
getBuiltinThing b = lift $ getBuiltinThing b
instance (HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m) where
getBuiltinThing b = lift $ getBuiltinThing b
litType
:: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
=> Literal -> m Type
litType l = case l of
LitNat _ n -> do
_ <- primZero
when (n > 0) $ void $ primSuc
el <$> primNat
LitWord64 _ _ -> el <$> primWord64
LitFloat _ _ -> el <$> primFloat
LitChar _ _ -> el <$> primChar
LitString _ _ -> el <$> primString
LitQName _ _ -> el <$> primQName
LitMeta _ _ _ -> el <$> primAgdaMeta
where
el t = El (mkType 0) t
instance MonadIO m => HasBuiltins (TCMT m) where
getBuiltinThing b = liftM2 mplus (Map.lookup b <$> useTC stLocalBuiltins)
(Map.lookup b <$> useTC stImportedBuiltins)
setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
setBuiltinThings b = stLocalBuiltins `setTCLens` b
bindBuiltinName :: String -> Term -> TCM ()
bindBuiltinName b x = do
builtin <- getBuiltinThing b
case builtin of
Just (Builtin y) -> typeError $ DuplicateBuiltinBinding b y x
Just (Prim _) -> typeError $ NoSuchBuiltinName b
Nothing -> stLocalBuiltins `modifyTCLens` Map.insert b (Builtin x)
bindPrimitive :: String -> PrimFun -> TCM ()
bindPrimitive b pf = do
builtin <- getBuiltinThing b
case builtin of
Just (Builtin _) -> typeError $ NoSuchPrimitiveFunction b
Just (Prim x) -> typeError $ (DuplicatePrimitiveBinding b `on` primFunName) x pf
Nothing -> stLocalBuiltins `modifyTCLens` Map.insert b (Prim pf)
getBuiltin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
=> String -> m Term
getBuiltin x =
fromMaybeM (typeError $ NoBindingForBuiltin x) $ getBuiltin' x
getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)
getBuiltin' x = do
builtin <- getBuiltinThing x
case builtin of
Just (Builtin t) -> return $ Just $ killRange t
_ -> return Nothing
getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' x = (getPrim =<<) <$> getBuiltinThing x
where
getPrim (Prim pf) = return pf
getPrim _ = Nothing
getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
=> String -> m PrimFun
getPrimitive x =
fromMaybeM (typeError $ NoSuchPrimitiveFunction x) $ getPrimitive' x
getPrimitiveTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
=> String -> m Term
getPrimitiveTerm x = (`Def` []) <$> primFunName <$> getPrimitive x
getPrimitiveTerm' :: HasBuiltins m => String -> m (Maybe Term)
getPrimitiveTerm' x = fmap (`Def` []) <$> getPrimitiveName' x
getTerm' :: HasBuiltins m => String -> m (Maybe Term)
getTerm' x = mplus <$> getBuiltin' x <*> getPrimitiveTerm' x
getName' :: HasBuiltins m => String -> m (Maybe QName)
getName' x = mplus <$> getBuiltinName' x <*> getPrimitiveName' x
getTerm :: (HasBuiltins m) => String -> String -> m Term
getTerm use name = flip fromMaybeM (getTerm' name) $
return $! (throwImpossible $ ImpMissingDefinitions [name] use)
constructorForm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
=> Term -> m Term
constructorForm v = constructorForm' primZero primSuc v
constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
constructorForm' pZero pSuc v =
case v of
Lit (LitNat r n)
| n == 0 -> pZero
| n > 0 -> (`apply1` Lit (LitNat r $ n - 1)) <$> pSuc
| otherwise -> pure v
_ -> pure v
primInteger, primIntegerPos, primIntegerNegSuc,
primFloat, primChar, primString, primUnit, primUnitUnit, primBool, primTrue, primFalse,
primSigma,
primList, primNil, primCons, primIO, primNat, primSuc, primZero,
primPath, primPathP, primInterval, primIZero, primIOne, primPartial, primPartialP,
primIMin, primIMax, primINeg,
primIsOne, primItIsOne, primIsOne1, primIsOne2, primIsOneEmpty,
primSub, primSubIn, primSubOut,
primTrans, primHComp,
primId, primConId, primIdElim,
primEquiv, primEquivFun, primEquivProof,
primTranspProof,
primGlue, prim_glue, prim_unglue,
prim_glueU, prim_unglueU,
primFaceForall,
primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux,
primNatEquality, primNatLess,
primWord64,
primSizeUniv, primSize, primSizeLt, primSizeSuc, primSizeInf, primSizeMax,
primInf, primSharp, primFlat,
primEquality, primRefl,
primRewrite,
primLevel, primLevelZero, primLevelSuc, primLevelMax,
primSetOmega,
primFromNat, primFromNeg, primFromString,
primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAbs, primAbsAbs, primAgdaTerm, primAgdaTermVar,
primAgdaTermLam, primAgdaTermExtLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
primAgdaTermSort, primAgdaTermLit, primAgdaTermUnsupported, primAgdaTermMeta,
primAgdaErrorPart, primAgdaErrorPartString, primAgdaErrorPartTerm, primAgdaErrorPartName,
primHiding, primHidden, primInstance, primVisible,
primRelevance, primRelevant, primIrrelevant,
primAssoc, primAssocLeft, primAssocRight, primAssocNon,
primPrecedence, primPrecRelated, primPrecUnrelated,
primFixity, primFixityFixity,
primAgdaLiteral, primAgdaLitNat, primAgdaLitWord64, primAgdaLitFloat, primAgdaLitString, primAgdaLitChar, primAgdaLitQName, primAgdaLitMeta,
primAgdaSort, primAgdaSortSet, primAgdaSortLit, primAgdaSortUnsupported,
primAgdaDefinition, primAgdaDefinitionFunDef, primAgdaDefinitionDataDef, primAgdaDefinitionRecordDef,
primAgdaDefinitionPostulate, primAgdaDefinitionPrimitive, primAgdaDefinitionDataConstructor,
primAgdaClause, primAgdaClauseClause, primAgdaClauseAbsurd,
primAgdaPattern, primAgdaPatCon, primAgdaPatVar, primAgdaPatDot,
primAgdaPatLit, primAgdaPatProj,
primAgdaPatAbsurd,
primAgdaMeta,
primAgdaTCM, primAgdaTCMReturn, primAgdaTCMBind, primAgdaTCMUnify,
primAgdaTCMTypeError, primAgdaTCMInferType, primAgdaTCMCheckType,
primAgdaTCMNormalise, primAgdaTCMReduce,
primAgdaTCMCatchError, primAgdaTCMGetContext, primAgdaTCMExtendContext, primAgdaTCMInContext,
primAgdaTCMFreshName, primAgdaTCMDeclareDef, primAgdaTCMDeclarePostulate, primAgdaTCMDefineFun,
primAgdaTCMGetType, primAgdaTCMGetDefinition,
primAgdaTCMQuoteTerm, primAgdaTCMUnquoteTerm,
primAgdaTCMBlockOnMeta, primAgdaTCMCommit, primAgdaTCMIsMacro,
primAgdaTCMWithNormalisation, primAgdaTCMDebugPrint,
primAgdaTCMNoConstraints,
primAgdaTCMRunSpeculative
:: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primInteger = getBuiltin builtinInteger
primIntegerPos = getBuiltin builtinIntegerPos
primIntegerNegSuc = getBuiltin builtinIntegerNegSuc
primFloat = getBuiltin builtinFloat
primChar = getBuiltin builtinChar
primString = getBuiltin builtinString
primBool = getBuiltin builtinBool
primSigma = getBuiltin builtinSigma
primUnit = getBuiltin builtinUnit
primUnitUnit = getBuiltin builtinUnitUnit
primTrue = getBuiltin builtinTrue
primFalse = getBuiltin builtinFalse
primList = getBuiltin builtinList
primNil = getBuiltin builtinNil
primCons = getBuiltin builtinCons
primIO = getBuiltin builtinIO
primId = getBuiltin builtinId
primConId = getBuiltin builtinConId
primIdElim = getPrimitiveTerm builtinIdElim
primPath = getBuiltin builtinPath
primPathP = getBuiltin builtinPathP
primInterval = getBuiltin builtinInterval
primIZero = getBuiltin builtinIZero
primIOne = getBuiltin builtinIOne
primIMin = getPrimitiveTerm builtinIMin
primIMax = getPrimitiveTerm builtinIMax
primINeg = getPrimitiveTerm builtinINeg
primPartial = getPrimitiveTerm "primPartial"
primPartialP = getPrimitiveTerm "primPartialP"
primIsOne = getBuiltin builtinIsOne
primItIsOne = getBuiltin builtinItIsOne
primTrans = getPrimitiveTerm builtinTrans
primHComp = getPrimitiveTerm builtinHComp
primEquiv = getBuiltin builtinEquiv
primEquivFun = getBuiltin builtinEquivFun
primEquivProof = getBuiltin builtinEquivProof
primTranspProof = getBuiltin builtinTranspProof
prim_glueU = getPrimitiveTerm builtin_glueU
prim_unglueU = getPrimitiveTerm builtin_unglueU
primGlue = getPrimitiveTerm builtinGlue
prim_glue = getPrimitiveTerm builtin_glue
prim_unglue = getPrimitiveTerm builtin_unglue
primFaceForall = getPrimitiveTerm builtinFaceForall
primIsOne1 = getBuiltin builtinIsOne1
primIsOne2 = getBuiltin builtinIsOne2
primIsOneEmpty = getBuiltin builtinIsOneEmpty
primSub = getBuiltin builtinSub
primSubIn = getBuiltin builtinSubIn
primSubOut = getPrimitiveTerm builtinSubOut
primNat = getBuiltin builtinNat
primSuc = getBuiltin builtinSuc
primZero = getBuiltin builtinZero
primNatPlus = getBuiltin builtinNatPlus
primNatMinus = getBuiltin builtinNatMinus
primNatTimes = getBuiltin builtinNatTimes
primNatDivSucAux = getBuiltin builtinNatDivSucAux
primNatModSucAux = getBuiltin builtinNatModSucAux
primNatEquality = getBuiltin builtinNatEquals
primNatLess = getBuiltin builtinNatLess
primWord64 = getBuiltin builtinWord64
primSizeUniv = getBuiltin builtinSizeUniv
primSize = getBuiltin builtinSize
primSizeLt = getBuiltin builtinSizeLt
primSizeSuc = getBuiltin builtinSizeSuc
primSizeInf = getBuiltin builtinSizeInf
primSizeMax = getBuiltin builtinSizeMax
primInf = getBuiltin builtinInf
primSharp = getBuiltin builtinSharp
primFlat = getBuiltin builtinFlat
primEquality = getBuiltin builtinEquality
primRefl = getBuiltin builtinRefl
primRewrite = getBuiltin builtinRewrite
primLevel = getBuiltin builtinLevel
primLevelZero = getBuiltin builtinLevelZero
primLevelSuc = getBuiltin builtinLevelSuc
primLevelMax = getBuiltin builtinLevelMax
primSetOmega = getBuiltin builtinSetOmega
primFromNat = getBuiltin builtinFromNat
primFromNeg = getBuiltin builtinFromNeg
primFromString = getBuiltin builtinFromString
primQName = getBuiltin builtinQName
primArg = getBuiltin builtinArg
primArgArg = getBuiltin builtinArgArg
primAbs = getBuiltin builtinAbs
primAbsAbs = getBuiltin builtinAbsAbs
primAgdaSort = getBuiltin builtinAgdaSort
primHiding = getBuiltin builtinHiding
primHidden = getBuiltin builtinHidden
primInstance = getBuiltin builtinInstance
primVisible = getBuiltin builtinVisible
primRelevance = getBuiltin builtinRelevance
primRelevant = getBuiltin builtinRelevant
primIrrelevant = getBuiltin builtinIrrelevant
primAssoc = getBuiltin builtinAssoc
primAssocLeft = getBuiltin builtinAssocLeft
primAssocRight = getBuiltin builtinAssocRight
primAssocNon = getBuiltin builtinAssocNon
primPrecedence = getBuiltin builtinPrecedence
primPrecRelated = getBuiltin builtinPrecRelated
primPrecUnrelated = getBuiltin builtinPrecUnrelated
primFixity = getBuiltin builtinFixity
primFixityFixity = getBuiltin builtinFixityFixity
primArgInfo = getBuiltin builtinArgInfo
primArgArgInfo = getBuiltin builtinArgArgInfo
primAgdaSortSet = getBuiltin builtinAgdaSortSet
primAgdaSortLit = getBuiltin builtinAgdaSortLit
primAgdaSortUnsupported = getBuiltin builtinAgdaSortUnsupported
primAgdaTerm = getBuiltin builtinAgdaTerm
primAgdaTermVar = getBuiltin builtinAgdaTermVar
primAgdaTermLam = getBuiltin builtinAgdaTermLam
primAgdaTermExtLam = getBuiltin builtinAgdaTermExtLam
primAgdaTermDef = getBuiltin builtinAgdaTermDef
primAgdaTermCon = getBuiltin builtinAgdaTermCon
primAgdaTermPi = getBuiltin builtinAgdaTermPi
primAgdaTermSort = getBuiltin builtinAgdaTermSort
primAgdaTermLit = getBuiltin builtinAgdaTermLit
primAgdaTermUnsupported = getBuiltin builtinAgdaTermUnsupported
primAgdaTermMeta = getBuiltin builtinAgdaTermMeta
primAgdaErrorPart = getBuiltin builtinAgdaErrorPart
primAgdaErrorPartString = getBuiltin builtinAgdaErrorPartString
primAgdaErrorPartTerm = getBuiltin builtinAgdaErrorPartTerm
primAgdaErrorPartName = getBuiltin builtinAgdaErrorPartName
primAgdaLiteral = getBuiltin builtinAgdaLiteral
primAgdaLitNat = getBuiltin builtinAgdaLitNat
primAgdaLitWord64 = getBuiltin builtinAgdaLitWord64
primAgdaLitFloat = getBuiltin builtinAgdaLitFloat
primAgdaLitChar = getBuiltin builtinAgdaLitChar
primAgdaLitString = getBuiltin builtinAgdaLitString
primAgdaLitQName = getBuiltin builtinAgdaLitQName
primAgdaLitMeta = getBuiltin builtinAgdaLitMeta
primAgdaPattern = getBuiltin builtinAgdaPattern
primAgdaPatCon = getBuiltin builtinAgdaPatCon
primAgdaPatVar = getBuiltin builtinAgdaPatVar
primAgdaPatDot = getBuiltin builtinAgdaPatDot
primAgdaPatLit = getBuiltin builtinAgdaPatLit
primAgdaPatProj = getBuiltin builtinAgdaPatProj
primAgdaPatAbsurd = getBuiltin builtinAgdaPatAbsurd
primAgdaClause = getBuiltin builtinAgdaClause
primAgdaClauseClause = getBuiltin builtinAgdaClauseClause
primAgdaClauseAbsurd = getBuiltin builtinAgdaClauseAbsurd
primAgdaDefinitionFunDef = getBuiltin builtinAgdaDefinitionFunDef
primAgdaDefinitionDataDef = getBuiltin builtinAgdaDefinitionDataDef
primAgdaDefinitionRecordDef = getBuiltin builtinAgdaDefinitionRecordDef
primAgdaDefinitionDataConstructor = getBuiltin builtinAgdaDefinitionDataConstructor
primAgdaDefinitionPostulate = getBuiltin builtinAgdaDefinitionPostulate
primAgdaDefinitionPrimitive = getBuiltin builtinAgdaDefinitionPrimitive
primAgdaDefinition = getBuiltin builtinAgdaDefinition
primAgdaMeta = getBuiltin builtinAgdaMeta
primAgdaTCM = getBuiltin builtinAgdaTCM
primAgdaTCMReturn = getBuiltin builtinAgdaTCMReturn
primAgdaTCMBind = getBuiltin builtinAgdaTCMBind
primAgdaTCMUnify = getBuiltin builtinAgdaTCMUnify
primAgdaTCMTypeError = getBuiltin builtinAgdaTCMTypeError
primAgdaTCMInferType = getBuiltin builtinAgdaTCMInferType
primAgdaTCMCheckType = getBuiltin builtinAgdaTCMCheckType
primAgdaTCMNormalise = getBuiltin builtinAgdaTCMNormalise
primAgdaTCMReduce = getBuiltin builtinAgdaTCMReduce
primAgdaTCMCatchError = getBuiltin builtinAgdaTCMCatchError
primAgdaTCMGetContext = getBuiltin builtinAgdaTCMGetContext
primAgdaTCMExtendContext = getBuiltin builtinAgdaTCMExtendContext
primAgdaTCMInContext = getBuiltin builtinAgdaTCMInContext
primAgdaTCMFreshName = getBuiltin builtinAgdaTCMFreshName
primAgdaTCMDeclareDef = getBuiltin builtinAgdaTCMDeclareDef
primAgdaTCMDeclarePostulate = getBuiltin builtinAgdaTCMDeclarePostulate
primAgdaTCMDefineFun = getBuiltin builtinAgdaTCMDefineFun
primAgdaTCMGetType = getBuiltin builtinAgdaTCMGetType
primAgdaTCMGetDefinition = getBuiltin builtinAgdaTCMGetDefinition
primAgdaTCMQuoteTerm = getBuiltin builtinAgdaTCMQuoteTerm
primAgdaTCMUnquoteTerm = getBuiltin builtinAgdaTCMUnquoteTerm
primAgdaTCMBlockOnMeta = getBuiltin builtinAgdaTCMBlockOnMeta
primAgdaTCMCommit = getBuiltin builtinAgdaTCMCommit
primAgdaTCMIsMacro = getBuiltin builtinAgdaTCMIsMacro
primAgdaTCMWithNormalisation = getBuiltin builtinAgdaTCMWithNormalisation
primAgdaTCMDebugPrint = getBuiltin builtinAgdaTCMDebugPrint
primAgdaTCMNoConstraints = getBuiltin builtinAgdaTCMNoConstraints
primAgdaTCMRunSpeculative = getBuiltin builtinAgdaTCMRunSpeculative
data CoinductionKit = CoinductionKit
{ nameOfInf :: QName
, nameOfSharp :: QName
, nameOfFlat :: QName
}
coinductionKit' :: TCM CoinductionKit
coinductionKit' = do
Def inf _ <- primInf
Def sharp _ <- primSharp
Def flat _ <- primFlat
return $ CoinductionKit
{ nameOfInf = inf
, nameOfSharp = sharp
, nameOfFlat = flat
}
coinductionKit :: TCM (Maybe CoinductionKit)
coinductionKit = tryMaybe coinductionKit'
getPrimName :: Term -> QName
getPrimName ty = do
let lamV (Lam i b) = mapFst (getHiding i :) $ lamV (unAbs b)
lamV (Pi _ b) = lamV (unEl $ unAbs b)
lamV v = ([], v)
case lamV ty of
(_, Def path _) -> path
(_, Con nm _ _) -> conName nm
(_, _) -> __IMPOSSIBLE__
getBuiltinName', getPrimitiveName' :: HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' n = fmap getPrimName <$> getBuiltin' n
getPrimitiveName' n = fmap primFunName <$> getPrimitive' n
isPrimitive :: HasBuiltins m => String -> QName -> m Bool
isPrimitive n q = (Just q ==) <$> getPrimitiveName' n
intervalView' :: HasBuiltins m => m (Term -> IntervalView)
intervalView' = do
iz <- getBuiltinName' builtinIZero
io <- getBuiltinName' builtinIOne
imax <- getPrimitiveName' "primIMax"
imin <- getPrimitiveName' "primIMin"
ineg <- getPrimitiveName' "primINeg"
return $ \ t ->
case t of
Def q es ->
case es of
[Apply x,Apply y] | Just q == imin -> IMin x y
[Apply x,Apply y] | Just q == imax -> IMax x y
[Apply x] | Just q == ineg -> INeg x
_ -> OTerm t
Con q _ [] | Just (conName q) == iz -> IZero
| Just (conName q) == io -> IOne
_ -> OTerm t
intervalView :: HasBuiltins m => Term -> m IntervalView
intervalView t = do
f <- intervalView'
return (f t)
intervalUnview :: HasBuiltins m => IntervalView -> m Term
intervalUnview t = do
f <- intervalUnview'
return (f t)
intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
intervalUnview' = do
iz <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIZero
io <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIOne
imin <- (`Def` []) <$> fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' "primIMin"
imax <- (`Def` []) <$> fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' "primIMax"
ineg <- (`Def` []) <$> fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' "primINeg"
return $ \ v -> case v of
IZero -> iz
IOne -> io
IMin x y -> apply imin [x,y]
IMax x y -> apply imax [x,y]
INeg x -> apply ineg [x]
OTerm t -> t
pathView :: HasBuiltins m => Type -> m PathView
pathView t0 = do
view <- pathView'
return $ view t0
pathView' :: HasBuiltins m => m (Type -> PathView)
pathView' = do
mpath <- getBuiltinName' builtinPath
mpathp <- getBuiltinName' builtinPathP
return $ \ t0@(El s t) ->
case t of
Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ]
| Just path' == mpath, Just path <- mpathp -> PathType s path level (lam_i <$> typ) lhs rhs
where lam_i = Lam defaultArgInfo . NoAbs "_"
Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ]
| Just path' == mpathp, Just path <- mpathp -> PathType s path level typ lhs rhs
_ -> OType t0
idViewAsPath :: HasBuiltins m => Type -> m PathView
idViewAsPath t0@(El s t) = do
mid <- fmap getPrimName <$> getBuiltin' builtinId
mpath <- fmap getPrimName <$> getBuiltin' builtinPath
case mid of
Just path | isJust mpath -> case t of
Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ]
| path' == path -> return $ PathType s (fromJust mpath) level typ lhs rhs
_ -> return $ OType t0
_ -> return $ OType t0
boldPathView :: Type -> PathView
boldPathView t0@(El s t) = do
case t of
Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ]
-> PathType s path' level typ lhs rhs
_ -> OType t0
pathUnview :: PathView -> Type
pathUnview (OType t) = t
pathUnview (PathType s path l t lhs rhs) =
El s $ Def path $ map Apply [l, t, lhs, rhs]
primEqualityName :: TCM QName
primEqualityName = do
eq <- primEquality
let lamV (Lam i b) = mapFst (getHiding i :) $ lamV (unAbs b)
lamV v = ([], v)
return $ case lamV eq of
(_, Def equality _) -> equality
_ -> __IMPOSSIBLE__
equalityView :: Type -> TCM EqualityView
equalityView t0@(El s t) = do
equality <- primEqualityName
case t of
Def equality' es | equality' == equality -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
let n = length vs
unless (n >= 3) __IMPOSSIBLE__
let (pars, [ typ , lhs, rhs ]) = splitAt (n-3) vs
return $ EqualityType s equality pars typ lhs rhs
_ -> return $ OtherType t0
equalityUnview :: EqualityView -> Type
equalityUnview (OtherType t) = t
equalityUnview (EqualityType s equality l t lhs rhs) =
El s $ Def equality $ map Apply (l ++ [t, lhs, rhs])
constrainedPrims :: [String]
constrainedPrims =
[ builtinConId
, builtinPOr
, builtinComp
, builtinHComp
, builtinTrans
, builtin_glue
, builtin_glueU
]
getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName)
getNameOfConstrained s = do
unless (s `elem` constrainedPrims) __IMPOSSIBLE__
getName' s