Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Monad.SizedTypes

Contents

Testing for type Size
Constructors
Viewing and unviewing sizes
View on sizes where maximum is pulled to the top

Description

Stuff for sized types that does not require modules Reduce or Constraints (which import Monad).

Synopsis

Testing for type `Size`

data BoundedSize Source

Result of querying whether size variable i is bounded by another size.

Constructors

BoundedLt Term	yes `i : Size< t`
BoundedNo

Instances

Eq BoundedSize
Show BoundedSize

isSizeType :: Type -> TCM (Maybe BoundedSize) Source

Check if a type is the primSize type. The argument should be reduced.

isSizeTypeTest :: TCM (Type -> Maybe BoundedSize) Source

getBuiltinDefName :: String -> TCM (Maybe QName) Source

getBuiltinSize :: TCM (Maybe QName, Maybe QName) Source

isSizeNameTest :: TCM (QName -> Bool) Source

isSizeNameTestRaw :: TCM (QName -> Bool) Source

haveSizedTypes :: TCM Bool Source

Test whether OPTIONS --sized-types and whether the size built-ins are defined.

builtinSizeHook :: String -> QName -> Term -> Type -> TCM () Source

Add polarity info to a SIZE builtin.

Constructors

sizeSort :: Sort Source

The sort of built-in types SIZE and SIZELT.

sizeUniv :: Type Source

The type of built-in types SIZE and SIZELT.

sizeType_ :: QName -> Type Source

The built-in type SIZE with user-given name.

sizeType :: TCM Type Source

The built-in type SIZE.

sizeSucName :: TCM (Maybe QName) Source

The name of SIZESUC.

sizeSuc :: Nat -> Term -> TCM Term Source

sizeSuc_ :: QName -> Term -> Term Source

sizeMax :: [Term] -> TCM Term Source

Transform list of terms into a term build from binary maximum.

Viewing and unviewing sizes

data SizeView Source

A useful view on sizes.

Constructors

SizeInf
SizeSuc Term
OtherSize Term

sizeView :: Term -> TCM SizeView Source

type Offset = Nat Source

data DeepSizeView Source

A deep view on sizes.

Constructors

DSizeInf
DSizeVar Nat Offset
DSizeMeta MetaId Elims Offset
DOtherSize Term

data SizeViewComparable a Source

Constructors

NotComparable
YesAbove DeepSizeView a
YesBelow DeepSizeView a

Instances

Functor SizeViewComparable

sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable () Source

sizeViewComparable v w checks whether v >= w (then Left) or v <= w (then Right). If uncomparable, it returns NotComparable.

sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView Source

sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView Source

sizeViewPred k v decrements v by k (must be possible!).

sizeViewOffset :: DeepSizeView -> Maybe Offset Source

sizeViewOffset v returns the number of successors or Nothing when infty.

removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView) Source

Remove successors common to both sides.

unSizeView :: SizeView -> TCM Term Source

Turn a size view into a term.

unDeepSizeView :: DeepSizeView -> TCM Term Source

View on sizes where maximum is pulled to the top

type SizeMaxView = [DeepSizeView] Source

maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView Source

maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView Source

maxViewCons v ws = max v ws. It only adds v to ws if it is not subsumed by an element of ws.

sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView Source

sizeViewComparableWithMax v ws tries to find w in ws that compares with v and singles this out. Precondition: v /= DSizeInv.

maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView Source

unMaxView :: SizeMaxView -> TCM Term Source

Testing for type Size

Constructors

Viewing and unviewing sizes

View on sizes where maximum is pulled to the top

Testing for type `Size`