Agda-2.8.0: A dependently typed functional programming language and proof assistant

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
- 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 #

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

Functor SingleLevel' Source # |
Instance details Defined in Agda.TypeChecking.Level Methods fmap :: (a -> b) -> SingleLevel' a -> SingleLevel' b Source # (<$) :: a -> SingleLevel' b -> SingleLevel' a Source #
Foldable SingleLevel' Source # |

Instance details

Defined in Agda.TypeChecking.Level

Methods

fold :: Monoid m => SingleLevel' m -> m Source #

foldMap :: Monoid m => (a -> m) -> SingleLevel' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> SingleLevel' a -> m Source #

foldr :: (a -> b -> b) -> b -> SingleLevel' a -> b Source #

foldr' :: (a -> b -> b) -> b -> SingleLevel' a -> b Source #

foldl :: (b -> a -> b) -> b -> SingleLevel' a -> b Source #

foldl' :: (b -> a -> b) -> b -> SingleLevel' a -> b Source #

foldr1 :: (a -> a -> a) -> SingleLevel' a -> a Source #

foldl1 :: (a -> a -> a) -> SingleLevel' a -> a Source #

toList :: SingleLevel' a -> [a] Source #

null :: SingleLevel' a -> Bool Source #

length :: SingleLevel' a -> Int Source #

elem :: Eq a => a -> SingleLevel' a -> Bool Source #

maximum :: Ord a => SingleLevel' a -> a Source #

minimum :: Ord a => SingleLevel' a -> a Source #

sum :: Num a => SingleLevel' a -> a Source #

product :: Num a => SingleLevel' a -> a Source #

Traversable SingleLevel' Source # |
Instance details Defined in Agda.TypeChecking.Level Methods traverse :: Applicative f => (a -> f b) -> SingleLevel' a -> f (SingleLevel' b) Source # sequenceA :: Applicative f => SingleLevel' (f a) -> f (SingleLevel' a) Source # mapM :: Monad m => (a -> m b) -> SingleLevel' a -> m (SingleLevel' b) Source # sequence :: Monad m => SingleLevel' (m a) -> m (SingleLevel' a) Source #
Eq SingleLevel Source # |
Instance details Defined in Agda.TypeChecking.Level Methods (==) :: SingleLevel -> SingleLevel -> Bool Source # (/=) :: SingleLevel -> SingleLevel -> Bool Source #
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) |
Instance details Defined in Agda.TypeChecking.Level type SubstArg (SingleLevel' t) = SubstArg t

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 Source # show :: SingleLevel' t -> String Source # showList :: [SingleLevel' t] -> ShowS Source #
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 `SingleLevel`s

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

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