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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.SizedTypes

Contents

- Builtins
- 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

- requireOptionSizedTypes :: (HasCallStack, HasOptions m, MonadTCError m) => String -> m ()
- getBuiltinSize :: HasBuiltins m => m (Maybe QName, Maybe QName)
- haveSizeLt :: TCM Bool
- builtinSizeHook :: BuiltinId -> QName -> Type -> TCM ()
- data BoundedSize
  - = BoundedLt Term
  - | BoundedNo
- class IsSizeType a where
  - isSizeType :: (HasOptions m, HasBuiltins m) => a -> m (Maybe BoundedSize)
- isSizeTypeTest :: (HasOptions m, HasBuiltins m) => m (Term -> Maybe BoundedSize)
- isSizeNameTest :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
- isSizeNameTestRaw :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
- sizeSort :: Sort
- sizeUniv :: Type
- sizeType_ :: QName -> Type
- sizeType :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => m Type
- sizeSucName :: (HasBuiltins m, HasOptions m) => m (Maybe QName)
- sizeSuc :: HasBuiltins m => Nat -> Term -> m Term
- sizeSuc_ :: QName -> Term -> Term
- sizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => List1 Term -> m Term
- data SizeView
  - = SizeInf
  - | SizeSuc Term
  - | OtherSize Term
- sizeView :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => Term -> m SizeView
- data ProjectedVar = ProjectedVar {
  - pvIndex :: Int
  - prProjs :: [(ProjOrigin, QName)]
  }
- viewProjectedVar :: Term -> Maybe ProjectedVar
- unviewProjectedVar :: ProjectedVar -> Term
- type Offset = Nat
- data DeepSizeView
  - = DSizeInf
  - | DSizeVar ProjectedVar 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 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => DeepSizeView -> m Term
- type SizeMaxView = List1 DeepSizeView
- type SizeMaxView' = [DeepSizeView]
- maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView
- maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView
- sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView'
- maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
- unMaxView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => SizeMaxView -> m Term

# Builtins

requireOptionSizedTypes :: (HasCallStack, HasOptions m, MonadTCError m) => String -> m () Source #

Ensure that option `--sized-types` is on, for the given reason.

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

haveSizeLt :: TCM Bool Source #

Test whether the SIZELT builtin is defined.

builtinSizeHook :: BuiltinId -> QName -> Type -> TCM () Source #

Add polarity info to a SIZE builtin.

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

class IsSizeType a where Source #

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

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 (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 (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 (b, a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => (b, a) -> m (Maybe BoundedSize) Source #

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

isSizeNameTest :: (HasOptions m, HasBuiltins m) => m (QName -> Bool) Source #

isSizeNameTestRaw :: (HasOptions m, HasBuiltins m) => m (QName -> Bool) Source #

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

sizeSuc :: HasBuiltins m => Nat -> Term -> m Term Source #

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

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.

Constructors

SizeInf |
SizeSuc Term |
OtherSize Term |

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

Expects argument to be `reduce`d.

data ProjectedVar Source #

A de Bruijn index under some projections.

Constructors

ProjectedVar |

Fields

- pvIndex :: Int
- prProjs :: [(ProjOrigin, QName)]

#### Instances

Instances details

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

viewProjectedVar :: Term -> Maybe ProjectedVar Source #

unviewProjectedVar :: ProjectedVar -> Term Source #

type Offset = Nat Source #

data DeepSizeView Source #

A deep view on sizes.

Constructors

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

#### Instances

Instances details

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

data SizeViewComparable a Source #

Constructors

NotComparable |
YesAbove DeepSizeView a |
YesBelow DeepSizeView a |

#### Instances

Instances details

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 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => DeepSizeView -> m Term Source #

# View on sizes where maximum is pulled to the top

type SizeMaxView = List1 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 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => SizeMaxView -> m Term Source #