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 :: (HasOptions m, HasBuiltins m) => a -> m (Maybe BoundedSize)

Instances

IsSizeType Term

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Term -> m (Maybe BoundedSize)

IsSizeType CompareAs

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => CompareAs -> m (Maybe BoundedSize)

IsSizeType a => IsSizeType (Type' a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Type' a -> m (Maybe BoundedSize)

IsSizeType a => IsSizeType (Dom a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize)

IsSizeType a => IsSizeType (b, a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => (b, a) -> m (Maybe BoundedSize)

isSizeTypeTest :: (HasOptions m, HasBuiltins m) => m (Term -> Maybe BoundedSize)

getBuiltinDefName :: HasBuiltins m => String -> m (Maybe QName)

getBuiltinSize :: HasBuiltins m => m (Maybe QName, Maybe QName)

isSizeNameTest :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)

isSizeNameTestRaw :: (HasOptions m, HasBuiltins m) => m (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 :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => m Type

The built-in type SIZE.

sizeSucName :: (HasBuiltins m, HasOptions m) => m (Maybe QName)

The name of SIZESUC.

sizeSuc :: HasBuiltins m => Nat -> Term -> m Term

sizeSuc_ :: QName -> Term -> Term

sizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => NonEmpty Term -> m 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 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Term -> m 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 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => DeepSizeView -> m Term

View on sizes where maximum is pulled to the top

type SizeMaxView = NonEmpty 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 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => SizeMaxView -> m Term