Agda.TypeChecking.Monad.SizedTypes

Stuff for sized types that does not require modules Agda.TypeChecking.Reduce or Agda.TypeChecking.Constraints (which import Agda.TypeChecking.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

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

(==) :: BoundedSize -> BoundedSize -> Bool

(/=) :: BoundedSize -> BoundedSize -> Bool

Show BoundedSize

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

showsPrec :: Int -> BoundedSize -> ShowS

show :: BoundedSize -> String

showList :: [BoundedSize] -> ShowS

class IsSizeType a where

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

Methods

isSizeType :: a -> TCM (Maybe BoundedSize)

Instances

IsSizeType Term

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: Term -> TCM (Maybe BoundedSize)

IsSizeType a => IsSizeType (Dom a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: Dom a -> TCM (Maybe BoundedSize)

IsSizeType a => IsSizeType (Type' a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: Type' a -> TCM (Maybe BoundedSize)

IsSizeType a => IsSizeType (b, a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (b, a) -> TCM (Maybe BoundedSize)

isSizeTypeTest :: TCM (Term -> 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.

haveSizeLt :: TCM Bool

Test whether the SIZELT builtin is defined.

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

Add polarity info to a SIZE builtin.

Constructors

sizeSort :: Sort

The sort of built-in types SIZE and SIZELT.

sizeUniv :: Type

The type of built-in types SIZE and SIZELT.

sizeType_ :: QName -> Type

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

sizeType :: TCM Type

The built-in type SIZE.

sizeSucName :: TCM (Maybe QName)

The name of SIZESUC.

sizeSuc :: Nat -> Term -> TCM Term

sizeSuc_ :: QName -> Term -> Term

sizeMax :: NonemptyList 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

Expects argument to be reduced.

type Offset = Nat

data DeepSizeView

A deep view on sizes.

Constructors

DSizeInf

DSizeVar Nat Offset

DSizeMeta MetaId Elims Offset

DOtherSize Term

Instances

Show DeepSizeView

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

showsPrec :: Int -> DeepSizeView -> ShowS

show :: DeepSizeView -> String

showList :: [DeepSizeView] -> ShowS

Pretty DeepSizeView

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

pretty :: DeepSizeView -> Doc

prettyPrec :: Int -> DeepSizeView -> Doc

prettyList :: [DeepSizeView] -> Doc

data SizeViewComparable a

Constructors

NotComparable

YesAbove DeepSizeView a

YesBelow DeepSizeView a

Instances

Functor SizeViewComparable

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

fmap :: (a -> b) -> SizeViewComparable a -> SizeViewComparable b

(<$) :: a -> SizeViewComparable b -> SizeViewComparable a

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 = NonemptyList DeepSizeView

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