| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
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
- data BoundedSize
- class IsSizeType a where
- isSizeType :: (HasOptions m, HasBuiltins m) => a -> m (Maybe BoundedSize)
- isSizeTypeTest :: (HasOptions m, HasBuiltins m) => m (Term -> Maybe BoundedSize)
- getBuiltinDefName :: HasBuiltins m => String -> m (Maybe QName)
- getBuiltinSize :: HasBuiltins m => m (Maybe QName, Maybe QName)
- isSizeNameTest :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
- isSizeNameTestRaw :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
- haveSizedTypes :: TCM Bool
- haveSizeLt :: TCM Bool
- builtinSizeHook :: String -> QName -> Type -> TCM ()
- 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) => NonEmpty Term -> m Term
- data SizeView
- 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
- data SizeViewComparable 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 = NonEmpty 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
Testing for type Size
data BoundedSize Source #
Result of querying whether size variable i is bounded by another
size.
Instances
| Eq BoundedSize Source # | |
Defined in Agda.TypeChecking.Monad.SizedTypes | |
| Show BoundedSize Source # | |
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
| IsSizeType Term Source # | |
Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Term -> m (Maybe BoundedSize) Source # | |
| IsSizeType CompareAs Source # | |
Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => CompareAs -> m (Maybe BoundedSize) Source # | |
| IsSizeType a => IsSizeType (Type' a) Source # | |
Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Type' a -> m (Maybe BoundedSize) Source # | |
| IsSizeType a => IsSizeType (Dom a) Source # | |
Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize) Source # | |
| IsSizeType a => IsSizeType (b, a) Source # | |
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 #
getBuiltinDefName :: HasBuiltins m => String -> m (Maybe QName) Source #
getBuiltinSize :: HasBuiltins m => m (Maybe QName, Maybe QName) Source #
isSizeNameTest :: (HasOptions m, HasBuiltins m) => m (QName -> Bool) Source #
isSizeNameTestRaw :: (HasOptions m, HasBuiltins m) => m (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.
Constructors
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
sizeView :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => Term -> m SizeView Source #
Expects argument to be reduced.
data ProjectedVar Source #
A de Bruijn index under some projections.
Constructors
| ProjectedVar | |
Fields
| |
Instances
| Eq ProjectedVar Source # | Ignore |
Defined in Agda.TypeChecking.Monad.SizedTypes | |
| Show ProjectedVar Source # | |
Defined in Agda.TypeChecking.Monad.SizedTypes Methods showsPrec :: Int -> ProjectedVar -> ShowS # show :: ProjectedVar -> String # showList :: [ProjectedVar] -> ShowS # | |
viewProjectedVar :: Term -> Maybe ProjectedVar Source #
data DeepSizeView Source #
A deep view on sizes.
Constructors
| DSizeInf | |
| DSizeVar ProjectedVar Offset | |
| DSizeMeta MetaId Elims Offset | |
| DOtherSize Term |
Instances
| Show DeepSizeView Source # | |
Defined in Agda.TypeChecking.Monad.SizedTypes Methods showsPrec :: Int -> DeepSizeView -> ShowS # show :: DeepSizeView -> String # showList :: [DeepSizeView] -> ShowS # | |
| Pretty DeepSizeView Source # | |
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 # | |
Defined in Agda.TypeChecking.Monad.SizedTypes Methods fmap :: (a -> b) -> SizeViewComparable a -> SizeViewComparable b # (<$) :: a -> SizeViewComparable b -> SizeViewComparable a # | |
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.
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 = NonEmpty 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 #