Safe Haskell	Safe-Inferred
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 :: PureTCM 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 :: 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 -> NonEmpty (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 => m Type Source #

Get the primLevel as a Type.

isLevelType :: PureTCM 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 :: 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

SingleClosed Integer
SinglePlus (PlusLevel' t)

Instances

Instances details

Foldable SingleLevel' Source #
Instance details Defined in Agda.TypeChecking.Level Methods fold :: Monoid m => SingleLevel' m -> m # foldMap :: Monoid m => (a -> m) -> SingleLevel' a -> m # foldMap' :: Monoid m => (a -> m) -> SingleLevel' a -> m # foldr :: (a -> b -> b) -> b -> SingleLevel' a -> b # foldr' :: (a -> b -> b) -> b -> SingleLevel' a -> b # foldl :: (b -> a -> b) -> b -> SingleLevel' a -> b # foldl' :: (b -> a -> b) -> b -> SingleLevel' a -> b # foldr1 :: (a -> a -> a) -> SingleLevel' a -> a # foldl1 :: (a -> a -> a) -> SingleLevel' a -> a # toList :: SingleLevel' a -> [a] # null :: SingleLevel' a -> Bool # length :: SingleLevel' a -> Int # elem :: Eq a => a -> SingleLevel' a -> Bool # maximum :: Ord a => SingleLevel' a -> a # minimum :: Ord a => SingleLevel' a -> a # sum :: Num a => SingleLevel' a -> a # product :: Num a => SingleLevel' a -> a #
Traversable SingleLevel' Source #
Instance details Defined in Agda.TypeChecking.Level Methods traverse :: Applicative f => (a -> f b) -> SingleLevel' a -> f (SingleLevel' b) # sequenceA :: Applicative f => SingleLevel' (f a) -> f (SingleLevel' a) # mapM :: Monad m => (a -> m b) -> SingleLevel' a -> m (SingleLevel' b) # sequence :: Monad m => SingleLevel' (m a) -> m (SingleLevel' a) #
Functor SingleLevel' Source #
Instance details Defined in Agda.TypeChecking.Level Methods fmap :: (a -> b) -> SingleLevel' a -> SingleLevel' b # (<$) :: a -> SingleLevel' b -> SingleLevel' a #
Eq SingleLevel Source #
Instance details Defined in Agda.TypeChecking.Level Methods (==) :: SingleLevel -> SingleLevel -> Bool # (/=) :: SingleLevel -> SingleLevel -> Bool #
Free t => Free (SingleLevel' t) Source #
Instance details Defined in Agda.TypeChecking.Level Methods freeVars' :: IsVarSet a c => SingleLevel' t -> FreeM a c Source #
Subst t => Subst (SingleLevel' t) Source #
Instance details Defined in Agda.TypeChecking.Level Associated Types type SubstArg (SingleLevel' t) Source # Methods applySubst :: Substitution' (SubstArg (SingleLevel' t)) -> SingleLevel' t -> SingleLevel' t Source #
Show t => Show (SingleLevel' t) Source #
Instance details Defined in Agda.TypeChecking.Level Methods showsPrec :: Int -> SingleLevel' t -> ShowS # show :: SingleLevel' t -> String # showList :: [SingleLevel' t] -> ShowS #
type SubstArg (SingleLevel' t) Source #
Instance details Defined in Agda.TypeChecking.Level type SubstArg (SingleLevel' t) = SubstArg t

type SingleLevel = SingleLevel' Term Source #

unSingleLevel :: SingleLevel' t -> Level' t Source #

unSingleLevels :: [SingleLevel] -> Level Source #

Return the maximum of the given SingleLevels

levelMaxView :: Level' t -> NonEmpty (SingleLevel' t) Source #

singleLevelView :: Level' t -> Maybe (SingleLevel' t) Source #