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

Safe Haskell | None

Agda.TypeChecking.Monad.SizedTypes

Contents

- Testing for type `Size`
- Constructors
- Viewing and unviewing sizes
- View on sizes where maximum is pulled to the top

Synopsis

- data BoundedSize
  - = BoundedLt Term
  - | BoundedNo
- isSizeType :: Type -> TCM (Maybe BoundedSize)
- isSizeTypeTest :: TCM (Type -> Maybe BoundedSize)
- getBuiltinDefName :: String -> TCM (Maybe QName)
- getBuiltinSize :: TCM (Maybe QName, Maybe QName)
- isSizeNameTest :: TCM (QName -> Bool)
- isSizeNameTestRaw :: TCM (QName -> Bool)
- sizeType :: TCM Type
- sizeSucName :: TCM (Maybe QName)
- sizeSuc :: Nat -> Term -> TCM Term
- sizeSuc_ :: QName -> Term -> Term
- sizeMax :: [Term] -> TCM Term
- data SizeView
  - = SizeInf
  - | SizeSuc Term
  - | OtherSize Term
- sizeView :: Term -> TCM SizeView
- type Offset = Nat
- data DeepSizeView
  - = DSizeInf
  - | DSizeVar Nat Offset
  - | DSizeMeta MetaId Args Offset
  - | DOtherSize Term
- data SizeViewComparable a
  - = NotComparable
  - | YesAbove DeepSizeView a
  - | YesBelow DeepSizeView a
- sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable ()
- sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
- sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView
- sizeViewOffset :: DeepSizeView -> Maybe Offset
- removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
- unSizeView :: SizeView -> TCM Term
- unDeepSizeView :: DeepSizeView -> TCM Term
- type SizeMaxView = [DeepSizeView]
- maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView
- maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView
- sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView
- maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
- unMaxView :: SizeMaxView -> TCM Term

# 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 |
Show BoundedSize |

isSizeType :: Type -> TCM (Maybe BoundedSize)

Check if a type is the `primSize` type. The argument should be `reduce`d.

isSizeTypeTest :: TCM (Type -> Maybe BoundedSize)

getBuiltinDefName :: String -> TCM (Maybe QName)

getBuiltinSize :: TCM (Maybe QName, Maybe QName)

isSizeNameTest :: TCM (QName -> Bool)

isSizeNameTestRaw :: TCM (QName -> Bool)

# Constructors

sizeType :: TCM Type

sizeSucName :: TCM (Maybe QName)

sizeSuc :: Nat -> Term -> TCM Term

sizeSuc_ :: QName -> Term -> Term

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.

Constructors

SizeInf |
SizeSuc Term |
OtherSize Term |

sizeView :: Term -> TCM SizeView

type Offset = Nat

data DeepSizeView

A deep view on sizes.

Constructors

DSizeInf |
DSizeVar Nat Offset |
DSizeMeta MetaId Args Offset |
DOtherSize Term |

data SizeViewComparable a

Constructors

NotComparable |
YesAbove DeepSizeView a |
YesBelow DeepSizeView a |

Instances

Functor SizeViewComparable |

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 = [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