Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Monad.SizedTypes

Description

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

Instances details
Show BoundedSize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Eq BoundedSize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

class IsSizeType a where Source #

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

Instances

Instances details
IsSizeType Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

IsSizeType CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

IsSizeType a => IsSizeType (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

IsSizeType a => IsSizeType (Type' a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

IsSizeType a => IsSizeType (b, a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

haveSizedTypes :: TCM Bool Source #

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

haveSizeLt :: TCM Bool Source #

Test whether the SIZELT builtin is defined.

builtinSizeHook :: BuiltinId -> QName -> 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 :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => m Type Source #

The built-in type SIZE.

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

The name of SIZESUC.

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

sizeView :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => Term -> m SizeView Source #

Expects argument to be reduced.

data ProjectedVar Source #

A de Bruijn index under some projections.

Constructors

ProjectedVar 

Fields

Instances

Instances details
Show ProjectedVar Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Eq ProjectedVar Source #

Ignore ProjOrigin in equality test.

Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

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

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

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.

View on sizes where maximum is pulled to the top

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.