Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Level

Synopsis

data LevelKit = LevelKit {
- lvlType :: Term
- lvlSuc :: Term -> Term
- lvlMax :: Term -> Term -> Term
- lvlZero :: Term
- typeName :: QName
- sucName :: QName
- maxName :: QName
- zeroName :: QName
}
levelType :: HasBuiltins m => m Type
isLevelType :: (HasBuiltins m, MonadReduce m) => Type -> m Bool
levelSucFunction :: TCM (Term -> Term)
builtinLevelKit :: HasBuiltins m => m LevelKit
requireLevels :: HasBuiltins m => m LevelKit
haveLevels :: HasBuiltins m => m Bool
unLevel :: HasBuiltins m => Term -> m Term
reallyUnLevelView :: HasBuiltins m => Level -> m Term
unlevelWithKit :: LevelKit -> Level -> Term
unConstV :: Term -> (Term -> Term) -> Integer -> Term
unPlusV :: (Term -> Term) -> PlusLevel -> Term
maybePrimCon :: TCM Term -> TCM (Maybe ConHead)
maybePrimDef :: TCM Term -> TCM (Maybe QName)
levelView :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level
levelView' :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level
levelPlusView :: Level -> (Integer, Level)
levelLowerBound :: Level -> Integer
subLevel :: Integer -> Level -> Maybe Level
levelMaxDiff :: Level -> Level -> Maybe Level
data SingleLevel
- = SingleClosed Integer
- | SinglePlus PlusLevel
unSingleLevel :: SingleLevel -> Level
unSingleLevels :: [SingleLevel] -> Level
levelMaxView :: Level -> NonEmpty SingleLevel
singleLevelView :: Level -> Maybe SingleLevel

Documentation

data LevelKit Source #

Constructors

LevelKit
Fields lvlType :: Term lvlSuc :: Term -> Term lvlMax :: Term -> Term -> Term lvlZero :: Term typeName :: QName sucName :: QName maxName :: QName zeroName :: QName

levelType :: HasBuiltins m => m Type Source #

Get the primLevel as a Type.

isLevelType :: (HasBuiltins m, MonadReduce m) => Type -> m Bool Source #

levelSucFunction :: TCM (Term -> Term) Source #

builtinLevelKit :: HasBuiltins m => m LevelKit Source #

requireLevels :: HasBuiltins m => m LevelKit Source #

Raises an error if no level kit is available.

haveLevels :: HasBuiltins m => m Bool Source #

Checks whether level kit is fully available.

unLevel :: HasBuiltins m => Term -> m Term Source #

reallyUnLevelView :: HasBuiltins m => Level -> m Term Source #

unlevelWithKit :: LevelKit -> Level -> Term Source #

unConstV :: Term -> (Term -> Term) -> Integer -> Term Source #

unPlusV :: (Term -> Term) -> PlusLevel -> Term Source #

maybePrimCon :: TCM Term -> TCM (Maybe ConHead) Source #

maybePrimDef :: TCM Term -> TCM (Maybe QName) Source #

levelView :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level Source #

levelView' :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level Source #

levelPlusView :: Level -> (Integer, Level) Source #

Given a level l, find the maximum constant n such that l = n + l'

levelLowerBound :: Level -> Integer Source #

Given a level l, find the biggest constant n such that n <= l

subLevel :: Integer -> Level -> Maybe Level Source #

Given a constant n and a level l, find the level l' such that l = n + l' (or Nothing if there is no such level). Operates on levels in canonical form.

levelMaxDiff :: Level -> Level -> Maybe Level Source #

Given two levels a and b, try to decompose the first one as a = a' ⊔ b (for the minimal value of a').

data SingleLevel Source #

A SingleLevel is a Level that cannot be further decomposed as a maximum a ⊔ b.

Constructors

SingleClosed Integer
SinglePlus PlusLevel

Instances

Instances details

Eq SingleLevel Source #
Instance details Defined in Agda.TypeChecking.Level Methods (==) :: SingleLevel -> SingleLevel -> Bool # (/=) :: SingleLevel -> SingleLevel -> Bool #
Show SingleLevel Source #
Instance details Defined in Agda.TypeChecking.Level Methods showsPrec :: Int -> SingleLevel -> ShowS # show :: SingleLevel -> String # showList :: [SingleLevel] -> ShowS #
Free SingleLevel Source #
Instance details Defined in Agda.TypeChecking.Level Methods freeVars' :: IsVarSet a c => SingleLevel -> FreeM a c Source #
Subst Term SingleLevel Source #
Instance details Defined in Agda.TypeChecking.Level Methods applySubst :: Substitution' Term -> SingleLevel -> SingleLevel Source #

unSingleLevel :: SingleLevel -> Level Source #

unSingleLevels :: [SingleLevel] -> Level Source #

Return the maximum of the given SingleLevels

levelMaxView :: Level -> NonEmpty SingleLevel Source #

singleLevelView :: Level -> Maybe SingleLevel Source #