Agda.TypeChecking.Monad.SizedTypes

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

Testing for type Size

data BoundedSize

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)

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

isSizeTypeTest :: TCM (Type -> Maybe BoundedSize)

getBuiltinDefName :: String -> TCM (Maybe QName)

getBuiltinSize :: TCM (Maybe QName, Maybe QName)

isSizeNameTest :: TCM (QName -> Bool)

isSizeNameTestRaw :: TCM (QName -> Bool)

haveSizedTypes :: TCM Bool

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

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

Add polarity info to a SIZE builtin.

Constructors

sizeType_ :: QName -> Type

sizeType :: TCM Type

sizeSucName :: TCM (Maybe QName)

sizeSuc :: Nat -> Term -> TCM Term

sizeSuc_ :: QName -> Term -> Term

sizeMax :: [Term] -> TCM Term

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

Viewing and unviewing sizes

data SizeView

A useful view on sizes.

Constructors

SizeInf

SizeSuc Term

OtherSize Term

sizeView :: Term -> TCM SizeView

type Offset = Nat

data DeepSizeView

A deep view on sizes.

Constructors

DSizeInf

DSizeVar Nat Offset

DSizeMeta MetaId Elims Offset

DOtherSize Term

data SizeViewComparable a

Constructors

NotComparable

YesAbove DeepSizeView a

YesBelow DeepSizeView a

Instances

Functor SizeViewComparable

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

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

sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView

sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView

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

sizeViewOffset :: DeepSizeView -> Maybe Offset

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

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

Remove successors common to both sides.

unSizeView :: SizeView -> TCM Term

Turn a size view into a term.

unDeepSizeView :: DeepSizeView -> TCM Term

View on sizes where maximum is pulled to the top

type SizeMaxView = [DeepSizeView]

maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView

maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView

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

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

maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView

unMaxView :: SizeMaxView -> TCM Term