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, MonadTCError m) => m Type
levelType' :: HasBuiltins m => m Type
isLevelType :: PureTCM m => Type -> m Bool
builtinLevelKit :: HasBuiltins m => m LevelKit
requireLevels :: (HasBuiltins m, MonadTCError 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 :: PureTCM m => Term -> m Level
levelView' :: PureTCM m => Term -> m Level
levelPlusView :: Level -> (Integer, Level)
levelLowerBound :: Level -> Integer
subLevel :: Integer -> Level -> Maybe Level
levelMaxDiff :: Level -> Level -> Maybe Level
data SingleLevel' t
- = SingleClosed Integer
- | SinglePlus (PlusLevel' t)
type SingleLevel = SingleLevel' Term
unSingleLevel :: SingleLevel' t -> Level' t
unSingleLevels :: [SingleLevel] -> Level
levelMaxView :: Level' t -> List1 (SingleLevel' t)
singleLevelView :: Level' t -> Maybe (SingleLevel' t)

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, MonadTCError m) => m Type Source #

Get the primLevel as a Type. Aborts if any of the level BUILTINs is undefined.

levelType' :: HasBuiltins m => m Type Source #

Get the primLevel as a Type. Unsafe, crashes if the BUILTIN LEVEL is undefined.

isLevelType :: PureTCM m => Type -> m Bool Source #

builtinLevelKit :: HasBuiltins m => m LevelKit Source #

requireLevels :: (HasBuiltins m, MonadTCError 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 :: PureTCM m => Term -> m Level Source #

levelView' :: PureTCM 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' t Source #

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

Constructors