Agda-2.4.0.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Monad.SizedTypes

Contents

Description

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

Synopsis

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 

isSizeType :: Type -> TCM (Maybe BoundedSize)

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

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

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.

type Offset = Nat

data DeepSizeView

A deep view on sizes.

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

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

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.

View on sizes where maximum is pulled to the top

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.