Agda-2.6.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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
Eq BoundedSize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

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

Show BoundedSize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

showsPrec :: Int -> BoundedSize -> ShowS

show :: BoundedSize -> String

showList :: [BoundedSize] -> ShowS

class IsSizeType a where Source #

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

Methods

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

Instances

Instances details
IsSizeType Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

IsSizeType CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

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

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

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

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

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

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 #

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

getBuiltinSize :: HasBuiltins m => m (Maybe QName, Maybe QName) 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 :: String -> 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) => NonEmpty 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, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Term -> m SizeView Source #

Expects argument to be reduced.

data DeepSizeView Source #

A deep view on sizes.

Instances

Instances details
Show DeepSizeView Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

showsPrec :: Int -> DeepSizeView -> ShowS

show :: DeepSizeView -> String

showList :: [DeepSizeView] -> ShowS

Pretty DeepSizeView Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

data SizeViewComparable a Source #

Instances

Instances details
Functor SizeViewComparable Source # 
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.