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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.SizedTypes

Contents

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

Description

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

Synopsis

- data BoundedSize
  - = BoundedLt Term
  - | BoundedNo
- class IsSizeType a where
  - isSizeType :: a -> TCM (Maybe BoundedSize)
- isSizeTypeTest :: TCM (Term -> Maybe BoundedSize)
- getBuiltinDefName :: String -> TCM (Maybe QName)
- getBuiltinSize :: TCM (Maybe QName, Maybe QName)
- isSizeNameTest :: TCM (QName -> Bool)
- isSizeNameTestRaw :: TCM (QName -> Bool)
- haveSizedTypes :: TCM Bool
- haveSizeLt :: TCM Bool
- builtinSizeHook :: String -> QName -> Type -> TCM ()
- sizeSort :: Sort
- sizeUniv :: Type
- sizeType_ :: QName -> Type
- sizeType :: TCM Type
- sizeSucName :: TCM (Maybe QName)
- sizeSuc :: Nat -> Term -> TCM Term
- sizeSuc_ :: QName -> Term -> Term
- sizeMax :: NonemptyList 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 Elims 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 = NonemptyList DeepSizeView
- 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 Source #

Result of querying whether size variable `i` is bounded by another size.

Constructors

BoundedLt Term | yes `i : Size< t`
BoundedNo |

Instances

Eq BoundedSize Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods (==) :: BoundedSize -> BoundedSize -> Bool Source # (/=) :: BoundedSize -> BoundedSize -> Bool Source #
Show BoundedSize Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods showsPrec :: Int -> BoundedSize -> ShowS Source # show :: BoundedSize -> String Source # showList :: [BoundedSize] -> ShowS Source #

class IsSizeType a where Source #

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

Methods

isSizeType :: a -> TCM (Maybe BoundedSize) Source #

Instances

IsSizeType Term Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: Term -> TCM (Maybe BoundedSize) Source #
IsSizeType a => IsSizeType (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: Dom a -> TCM (Maybe BoundedSize) Source #
IsSizeType a => IsSizeType (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: Type' a -> TCM (Maybe BoundedSize) Source #
IsSizeType a => IsSizeType (b, a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (b, a) -> TCM (Maybe BoundedSize) Source #

isSizeTypeTest :: TCM (Term -> Maybe BoundedSize) Source #

getBuiltinDefName :: String -> TCM (Maybe QName) Source #

getBuiltinSize :: TCM (Maybe QName, Maybe QName) Source #

isSizeNameTest :: TCM (QName -> Bool) Source #

isSizeNameTestRaw :: TCM (QName -> Bool) 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 :: TCM Type Source #

The built-in type `SIZE`.

sizeSucName :: TCM (Maybe QName) Source #

The name of `SIZESUC`.

sizeSuc :: Nat -> Term -> TCM Term Source #

sizeSuc_ :: QName -> Term -> Term Source #

sizeMax :: NonemptyList Term -> TCM 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.

Constructors

SizeInf |
SizeSuc Term |
OtherSize Term |

sizeView :: Term -> TCM SizeView Source #

Expects argument to be `reduce`d.

type Offset = Nat Source #

data DeepSizeView Source #

A deep view on sizes.

Constructors

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

Instances

Show DeepSizeView Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods showsPrec :: Int -> DeepSizeView -> ShowS Source # show :: DeepSizeView -> String Source # showList :: [DeepSizeView] -> ShowS Source #
Pretty DeepSizeView Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods pretty :: DeepSizeView -> Doc Source # prettyPrec :: Int -> DeepSizeView -> Doc Source # prettyList :: [DeepSizeView] -> Doc Source #

data SizeViewComparable a Source #

Constructors

NotComparable |
YesAbove DeepSizeView a |
YesBelow DeepSizeView a |

Instances

Functor SizeViewComparable Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods fmap :: (a -> b) -> SizeViewComparable a -> SizeViewComparable b Source # (<$) :: a -> SizeViewComparable b -> SizeViewComparable a Source #

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

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

sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView Source #

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.

unDeepSizeView :: DeepSizeView -> TCM Term Source #

# View on sizes where maximum is pulled to the top

type SizeMaxView = NonemptyList DeepSizeView Source #

type SizeMaxView' = [DeepSizeView] Source #

maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView Source #

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`.

maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView Source #

unMaxView :: SizeMaxView -> TCM Term Source #