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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.SizedTypes.Syntax

Contents

- Syntax
- Polarities to specify solutions.
- Solutions.
- Constraint simplification
- Printing
- Wellformedness
- Computing variable sets

Description

Syntax of size expressions and constraints.

Synopsis

- newtype Offset = O Int
- newtype Rigid = RigidId {
  - rigidId :: String
  }
- newtype Flex = FlexId {
  - flexId :: String
  }
- data SizeExpr' rigid flex
  - = Const {
    - offset :: Offset
    }
  - | Rigid {
    - rigid :: rigid
    - offset :: Offset
    }
  - | Infty
  - | Flex {
    - flex :: flex
    - offset :: Offset
    }
- type SizeExpr = SizeExpr' Rigid Flex
- data Cmp
  - = Lt
  - | Le
- data Constraint' rigid flex = Constraint {
  - leftExpr :: SizeExpr' rigid flex
  - cmp :: Cmp
  - rightExpr :: SizeExpr' rigid flex
  }
- type Constraint = Constraint' Rigid Flex
- data Polarity
  - = Least
  - | Greatest
- data PolarityAssignment flex = PolarityAssignment Polarity flex
- type Polarities flex = Map flex Polarity
- emptyPolarities :: Polarities flex
- polaritiesFromAssignments :: Ord flex => [PolarityAssignment flex] -> Polarities flex
- getPolarity :: Ord flex => Polarities flex -> flex -> Polarity
- newtype Solution rigid flex = Solution {
  - theSolution :: Map flex (SizeExpr' rigid flex)
  }
- emptySolution :: Solution r f
- class Substitute r f a where
  - subst :: Solution r f -> a -> a
- type CTrans r f = Constraint' r f -> Maybe [Constraint' r f]
- simplify1 :: (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
- ifLe :: Cmp -> a -> a -> a
- compareOffset :: Offset -> Cmp -> Offset -> Bool
- class ValidOffset a where
  - validOffset :: a -> Bool
- class TruncateOffset a where
  - truncateOffset :: a -> a
- class Ord (RigidOf a) => Rigids a where
  - type RigidOf a
  - rigids :: a -> Set (RigidOf a)
- class Ord (FlexOf a) => Flexs a where
  - type FlexOf a
  - flexs :: a -> Set (FlexOf a)
- data NamedRigid = NamedRigid {
  - rigidName :: String
  - rigidIndex :: Int
  }
- data SizeMeta = SizeMeta {
  - sizeMetaId :: MetaId
  - sizeMetaArgs :: [Int]
  }
- type DBSizeExpr = SizeExpr' NamedRigid SizeMeta
- type SizeConstraint = Constraint' NamedRigid SizeMeta
- data HypSizeConstraint = HypSizeConstraint {
  - sizeContext :: Context
  - sizeHypIds :: [Nat]
  - sizeHypotheses :: [SizeConstraint]
  - sizeConstraint :: SizeConstraint
  }

# Syntax

newtype Offset Source #

Constant finite sizes `n >= 0`.

Constructors

O Int |

#### Instances

Instances details

Pretty Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Offset -> Doc Source # prettyPrec :: Int -> Offset -> Doc Source # prettyList :: [Offset] -> Doc Source #
TruncateOffset Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods truncateOffset :: Offset -> Offset Source #
ValidOffset Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods validOffset :: Offset -> Bool Source #
MeetSemiLattice Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods meet :: Offset -> Offset -> Offset Source #
Negative Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods negative :: Offset -> Bool Source #
NFData Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods rnf :: Offset -> () Source #
Enum Offset Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

succ :: Offset -> Offset Source #

pred :: Offset -> Offset Source #

toEnum :: Int -> Offset Source #

fromEnum :: Offset -> Int Source #

enumFrom :: Offset -> [Offset] Source #

enumFromThen :: Offset -> Offset -> [Offset] Source #

enumFromTo :: Offset -> Offset -> [Offset] Source #

enumFromThenTo :: Offset -> Offset -> Offset -> [Offset] Source #

Generic Offset Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type Rep Offset |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type Rep Offset = D1 ('MetaData "Offset" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "O" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

Methods

from :: Offset -> Rep Offset x Source #

to :: Rep Offset x -> Offset Source #

Num Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (+) :: Offset -> Offset -> Offset Source # (-) :: Offset -> Offset -> Offset Source # (*) :: Offset -> Offset -> Offset Source # negate :: Offset -> Offset Source # abs :: Offset -> Offset Source # signum :: Offset -> Offset Source # fromInteger :: Integer -> Offset Source #
Show Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> Offset -> ShowS Source # show :: Offset -> String Source # showList :: [Offset] -> ShowS Source #
Eq Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: Offset -> Offset -> Bool Source # (/=) :: Offset -> Offset -> Bool Source #
Ord Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods compare :: Offset -> Offset -> Ordering Source # (<) :: Offset -> Offset -> Bool Source # (<=) :: Offset -> Offset -> Bool Source # (>) :: Offset -> Offset -> Bool Source # (>=) :: Offset -> Offset -> Bool Source # max :: Offset -> Offset -> Offset Source # min :: Offset -> Offset -> Offset Source #
Plus Offset Offset Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods plus :: Offset -> Offset -> Offset Source #
Plus Offset Weight Weight Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods plus :: Offset -> Weight -> Weight Source #
Plus Weight Offset Weight Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods plus :: Weight -> Offset -> Weight Source #
Plus (SizeExpr' r f) Offset (SizeExpr' r f) Source # | Add offset to size expression.
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods plus :: SizeExpr' r f -> Offset -> SizeExpr' r f Source #
type Rep Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type Rep Offset = D1 ('MetaData "Offset" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "O" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

newtype Rigid Source #

Fixed size variables `i`.

Constructors

RigidId |

Fields

- rigidId :: String

#### Instances

Instances details

Pretty Rigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Rigid -> Doc Source # prettyPrec :: Int -> Rigid -> Doc Source # prettyList :: [Rigid] -> Doc Source #
Show Rigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> Rigid -> ShowS Source # show :: Rigid -> String Source # showList :: [Rigid] -> ShowS Source #
Eq Rigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: Rigid -> Rigid -> Bool Source # (/=) :: Rigid -> Rigid -> Bool Source #
Ord Rigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods compare :: Rigid -> Rigid -> Ordering Source # (<) :: Rigid -> Rigid -> Bool Source # (<=) :: Rigid -> Rigid -> Bool Source # (>) :: Rigid -> Rigid -> Bool Source # (>=) :: Rigid -> Rigid -> Bool Source # max :: Rigid -> Rigid -> Rigid Source # min :: Rigid -> Rigid -> Rigid Source #

newtype Flex Source #

Size meta variables `X` to solve for.

Constructors

FlexId |

Fields

- flexId :: String

#### Instances

Instances details

Pretty Flex Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Flex -> Doc Source # prettyPrec :: Int -> Flex -> Doc Source # prettyList :: [Flex] -> Doc Source #
Show Flex Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> Flex -> ShowS Source # show :: Flex -> String Source # showList :: [Flex] -> ShowS Source #
Eq Flex Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: Flex -> Flex -> Bool Source # (/=) :: Flex -> Flex -> Bool Source #
Ord Flex Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods compare :: Flex -> Flex -> Ordering Source # (<) :: Flex -> Flex -> Bool Source # (<=) :: Flex -> Flex -> Bool Source # (>) :: Flex -> Flex -> Bool Source # (>=) :: Flex -> Flex -> Bool Source # max :: Flex -> Flex -> Flex Source # min :: Flex -> Flex -> Flex Source #

data SizeExpr' rigid flex Source #

Size expressions appearing in constraints.

Constructors

Const | Constant number `n`.

Fields

- offset :: Offset

Rigid | Variable plus offset `i + n`.

Fields

- rigid :: rigid
- offset :: Offset

Infty | Infinity `∞`.
Flex | Meta variable `X + n`.

Fields

- flex :: flex
- offset :: Offset

#### Instances

Instances details

Ord f => Substitute r f (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> SizeExpr' r f -> SizeExpr' r f Source #
Functor (SizeExpr' rigid) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods fmap :: (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b Source # (<$) :: a -> SizeExpr' rigid b -> SizeExpr' rigid a Source #
Foldable (SizeExpr' rigid) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

fold :: Monoid m => SizeExpr' rigid m -> m Source #

foldMap :: Monoid m => (a -> m) -> SizeExpr' rigid a -> m Source #

foldMap' :: Monoid m => (a -> m) -> SizeExpr' rigid a -> m Source #

foldr :: (a -> b -> b) -> b -> SizeExpr' rigid a -> b Source #

foldr' :: (a -> b -> b) -> b -> SizeExpr' rigid a -> b Source #

foldl :: (b -> a -> b) -> b -> SizeExpr' rigid a -> b Source #

foldl' :: (b -> a -> b) -> b -> SizeExpr' rigid a -> b Source #

foldr1 :: (a -> a -> a) -> SizeExpr' rigid a -> a Source #

foldl1 :: (a -> a -> a) -> SizeExpr' rigid a -> a Source #

toList :: SizeExpr' rigid a -> [a] Source #

null :: SizeExpr' rigid a -> Bool Source #

length :: SizeExpr' rigid a -> Int Source #

elem :: Eq a => a -> SizeExpr' rigid a -> Bool Source #

maximum :: Ord a => SizeExpr' rigid a -> a Source #

minimum :: Ord a => SizeExpr' rigid a -> a Source #

sum :: Num a => SizeExpr' rigid a -> a Source #

product :: Num a => SizeExpr' rigid a -> a Source #

Traversable (SizeExpr' rigid) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b) Source #

sequenceA :: Applicative f => SizeExpr' rigid (f a) -> f (SizeExpr' rigid a) Source #

mapM :: Monad m => (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b) Source #

sequence :: Monad m => SizeExpr' rigid (m a) -> m (SizeExpr' rigid a) Source #

(Pretty r, Pretty f) => Pretty (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: SizeExpr' r f -> Doc Source # prettyPrec :: Int -> SizeExpr' r f -> Doc Source # prettyList :: [SizeExpr' r f] -> Doc Source #
Ord flex => Flexs (SizeExpr' rigid flex) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (SizeExpr' rigid flex) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf (SizeExpr' rigid flex) = flex

Methods

flexs :: SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex)) Source #

Ord r => Rigids (SizeExpr' r f) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (SizeExpr' r f) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type RigidOf (SizeExpr' r f) = r

Methods

rigids :: SizeExpr' r f -> Set (RigidOf (SizeExpr' r f)) Source #

TruncateOffset (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods truncateOffset :: SizeExpr' r f -> SizeExpr' r f Source #
ValidOffset (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods validOffset :: SizeExpr' r f -> Bool Source #
Subst (SizeExpr' NamedRigid SizeMeta) Source # | Only for `raise`.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg (SizeExpr' NamedRigid SizeMeta) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

Methods

applySubst :: Substitution' (SubstArg (SizeExpr' NamedRigid SizeMeta)) -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #

(NFData r, NFData f) => NFData (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods rnf :: SizeExpr' r f -> () Source #
Generic (SizeExpr' rigid flex) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type Rep (SizeExpr' rigid flex) |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep (SizeExpr' rigid flex) = D1 ('MetaData "SizeExpr'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "Const" 'PrefixI 'True) (S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Offset)) :+: C1 ('MetaCons "Rigid" 'PrefixI 'True) (S1 ('MetaSel ('Just "rigid") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 rigid) :*: S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Offset))) :+: (C1 ('MetaCons "Infty" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Flex" 'PrefixI 'True) (S1 ('MetaSel ('Just "flex") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 flex) :*: S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Offset))))

Methods

from :: SizeExpr' rigid flex -> Rep (SizeExpr' rigid flex) x Source #

to :: Rep (SizeExpr' rigid flex) x -> SizeExpr' rigid flex Source #

(Show rigid, Show flex) => Show (SizeExpr' rigid flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> SizeExpr' rigid flex -> ShowS Source # show :: SizeExpr' rigid flex -> String Source # showList :: [SizeExpr' rigid flex] -> ShowS Source #
(Eq rigid, Eq flex) => Eq (SizeExpr' rigid flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool Source # (/=) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool Source #
(Ord rigid, Ord flex) => Ord (SizeExpr' rigid flex) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering Source #

(<) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool Source #

(<=) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool Source #

(>) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool Source #

(>=) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool Source #

max :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> SizeExpr' rigid flex Source #

min :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> SizeExpr' rigid flex Source #

Plus (SizeExpr' r f) Offset (SizeExpr' r f) Source # | Add offset to size expression.
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods plus :: SizeExpr' r f -> Offset -> SizeExpr' r f Source #
Plus (SizeExpr' r f) Label (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods plus :: SizeExpr' r f -> Label -> SizeExpr' r f Source #
Plus (SizeExpr' r f) Weight (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods plus :: SizeExpr' r f -> Weight -> SizeExpr' r f Source #
type FlexOf (SizeExpr' rigid flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf (SizeExpr' rigid flex) = flex
type RigidOf (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type RigidOf (SizeExpr' r f) = r
type SubstArg (SizeExpr' NamedRigid SizeMeta) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term
type Rep (SizeExpr' rigid flex) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep (SizeExpr' rigid flex) = D1 ('MetaData "SizeExpr'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "Const" 'PrefixI 'True) (S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Offset)) :+: C1 ('MetaCons "Rigid" 'PrefixI 'True) (S1 ('MetaSel ('Just "rigid") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 rigid) :*: S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Offset))) :+: (C1 ('MetaCons "Infty" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Flex" 'PrefixI 'True) (S1 ('MetaSel ('Just "flex") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 flex) :*: S1 ('MetaSel ('Just "offset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Offset))))

type SizeExpr = SizeExpr' Rigid Flex Source #

data Cmp Source #

Comparison operator, e.g. for size expression.

Constructors

Lt | `<`.
Le | `≤`.

#### Instances

Instances details

Pretty Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Cmp -> Doc Source # prettyPrec :: Int -> Cmp -> Doc Source # prettyList :: [Cmp] -> Doc Source #
Dioid Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods compose :: Cmp -> Cmp -> Cmp Source # unitCompose :: Cmp Source #
MeetSemiLattice Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods meet :: Cmp -> Cmp -> Cmp Source #
Top Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods top :: Cmp Source # isTop :: Cmp -> Bool Source #
NFData Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods rnf :: Cmp -> () Source #
Bounded Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods minBound :: Cmp Source # maxBound :: Cmp Source #
Enum Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods succ :: Cmp -> Cmp Source # pred :: Cmp -> Cmp Source # toEnum :: Int -> Cmp Source # fromEnum :: Cmp -> Int Source # enumFrom :: Cmp -> [Cmp] Source # enumFromThen :: Cmp -> Cmp -> [Cmp] Source # enumFromTo :: Cmp -> Cmp -> [Cmp] Source # enumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp] Source #
Generic Cmp Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type Rep Cmp |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type Rep Cmp = D1 ('MetaData "Cmp" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Lt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Le" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: Cmp -> Rep Cmp x Source #

to :: Rep Cmp x -> Cmp Source #

Show Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> Cmp -> ShowS Source # show :: Cmp -> String Source # showList :: [Cmp] -> ShowS Source #
Eq Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: Cmp -> Cmp -> Bool Source # (/=) :: Cmp -> Cmp -> Bool Source #
Ord Cmp Source # | Comparison operator is ordered ``Lt` < `Le``.
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods compare :: Cmp -> Cmp -> Ordering Source # (<) :: Cmp -> Cmp -> Bool Source # (<=) :: Cmp -> Cmp -> Bool Source # (>) :: Cmp -> Cmp -> Bool Source # (>=) :: Cmp -> Cmp -> Bool Source # max :: Cmp -> Cmp -> Cmp Source # min :: Cmp -> Cmp -> Cmp Source #
type Rep Cmp Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type Rep Cmp = D1 ('MetaData "Cmp" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Lt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Le" 'PrefixI 'False) (U1 :: Type -> Type))

data Constraint' rigid flex Source #

Constraint: an inequation between size expressions, e.g. `X < ∞` or `i + 3 ≤ j`.

Constructors

Constraint |

Fields

- leftExpr :: SizeExpr' rigid flex
- cmp :: Cmp
- rightExpr :: SizeExpr' rigid flex

#### Instances

Instances details

PrettyTCM SizeConstraint Source # | Assumes we are in the right context.
Instance details Defined in Agda.TypeChecking.SizedTypes.Pretty Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #
Subst SizeConstraint Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeConstraint |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeConstraint = Term

Methods

applySubst :: Substitution' (SubstArg SizeConstraint) -> SizeConstraint -> SizeConstraint Source #

Ord f => Substitute r f (Constraint' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> Constraint' r f -> Constraint' r f Source #
Functor (Constraint' rigid) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods fmap :: (a -> b) -> Constraint' rigid a -> Constraint' rigid b Source # (<$) :: a -> Constraint' rigid b -> Constraint' rigid a Source #
Foldable (Constraint' rigid) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

fold :: Monoid m => Constraint' rigid m -> m Source #

foldMap :: Monoid m => (a -> m) -> Constraint' rigid a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Constraint' rigid a -> m Source #

foldr :: (a -> b -> b) -> b -> Constraint' rigid a -> b Source #

foldr' :: (a -> b -> b) -> b -> Constraint' rigid a -> b Source #

foldl :: (b -> a -> b) -> b -> Constraint' rigid a -> b Source #

foldl' :: (b -> a -> b) -> b -> Constraint' rigid a -> b Source #

foldr1 :: (a -> a -> a) -> Constraint' rigid a -> a Source #

foldl1 :: (a -> a -> a) -> Constraint' rigid a -> a Source #

toList :: Constraint' rigid a -> [a] Source #

null :: Constraint' rigid a -> Bool Source #

length :: Constraint' rigid a -> Int Source #

elem :: Eq a => a -> Constraint' rigid a -> Bool Source #

maximum :: Ord a => Constraint' rigid a -> a Source #

minimum :: Ord a => Constraint' rigid a -> a Source #

sum :: Num a => Constraint' rigid a -> a Source #

product :: Num a => Constraint' rigid a -> a Source #

Traversable (Constraint' rigid) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

traverse :: Applicative f => (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b) Source #

sequenceA :: Applicative f => Constraint' rigid (f a) -> f (Constraint' rigid a) Source #

mapM :: Monad m => (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b) Source #

sequence :: Monad m => Constraint' rigid (m a) -> m (Constraint' rigid a) Source #

(Pretty r, Pretty f) => Pretty (Constraint' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Constraint' r f -> Doc Source # prettyPrec :: Int -> Constraint' r f -> Doc Source # prettyList :: [Constraint' r f] -> Doc Source #
Ord flex => Flexs (Constraint' rigid flex) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (Constraint' rigid flex) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf (Constraint' rigid flex) = flex

Methods

flexs :: Constraint' rigid flex -> Set (FlexOf (Constraint' rigid flex)) Source #

Ord r => Rigids (Constraint' r f) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (Constraint' r f) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type RigidOf (Constraint' r f) = r

Methods

rigids :: Constraint' r f -> Set (RigidOf (Constraint' r f)) Source #

(NFData r, NFData f) => NFData (Constraint' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods rnf :: Constraint' r f -> () Source #
Generic (Constraint' rigid flex) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type Rep (Constraint' rigid flex) |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep (Constraint' rigid flex) = D1 ('MetaData "Constraint'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Constraint" 'PrefixI 'True) (S1 ('MetaSel ('Just "leftExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SizeExpr' rigid flex)) :*: (S1 ('MetaSel ('Just "cmp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cmp) :*: S1 ('MetaSel ('Just "rightExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SizeExpr' rigid flex)))))

Methods

from :: Constraint' rigid flex -> Rep (Constraint' rigid flex) x Source #

to :: Rep (Constraint' rigid flex) x -> Constraint' rigid flex Source #

(Show rigid, Show flex) => Show (Constraint' rigid flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> Constraint' rigid flex -> ShowS Source # show :: Constraint' rigid flex -> String Source # showList :: [Constraint' rigid flex] -> ShowS Source #
type SubstArg SizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeConstraint = Term
type FlexOf (Constraint' rigid flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf (Constraint' rigid flex) = flex
type RigidOf (Constraint' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type RigidOf (Constraint' r f) = r
type Rep (Constraint' rigid flex) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep (Constraint' rigid flex) = D1 ('MetaData "Constraint'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Constraint" 'PrefixI 'True) (S1 ('MetaSel ('Just "leftExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SizeExpr' rigid flex)) :*: (S1 ('MetaSel ('Just "cmp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cmp) :*: S1 ('MetaSel ('Just "rightExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SizeExpr' rigid flex)))))

type Constraint = Constraint' Rigid Flex Source #

# Polarities to specify solutions.

data Polarity Source #

What type of solution are we looking for?

Constructors

Least |
Greatest |

#### Instances

Instances details

Pretty Polarity Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Polarity -> Doc Source # prettyPrec :: Int -> Polarity -> Doc Source # prettyList :: [Polarity] -> Doc Source #
Eq Polarity Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: Polarity -> Polarity -> Bool Source # (/=) :: Polarity -> Polarity -> Bool Source #
Ord Polarity Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: Polarity -> Polarity -> Ordering Source #

(<) :: Polarity -> Polarity -> Bool Source #

(<=) :: Polarity -> Polarity -> Bool Source #

(>) :: Polarity -> Polarity -> Bool Source #

(>=) :: Polarity -> Polarity -> Bool Source #

max :: Polarity -> Polarity -> Polarity Source #

min :: Polarity -> Polarity -> Polarity Source #

data PolarityAssignment flex Source #

Assigning a polarity to a flexible variable.

Constructors

PolarityAssignment Polarity flex |

#### Instances

Instances details

Pretty flex => Pretty (PolarityAssignment flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: PolarityAssignment flex -> Doc Source # prettyPrec :: Int -> PolarityAssignment flex -> Doc Source # prettyList :: [PolarityAssignment flex] -> Doc Source #

type Polarities flex = Map flex Polarity Source #

Type of solution wanted for each flexible.

emptyPolarities :: Polarities flex Source #

polaritiesFromAssignments :: Ord flex => [PolarityAssignment flex] -> Polarities flex Source #

getPolarity :: Ord flex => Polarities flex -> flex -> Polarity Source #

Default polarity is `Least`.

# Solutions.

newtype Solution rigid flex Source #

Partial substitution from flexible variables to size expression.

Constructors

Solution |

Fields

- theSolution :: Map flex (SizeExpr' rigid flex)

#### Instances

Instances details

Ord f => Substitute r f (Solution r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> Solution r f -> Solution r f Source #
(Pretty r, Pretty f) => Pretty (Solution r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: Solution r f -> Doc Source # prettyPrec :: Int -> Solution r f -> Doc Source # prettyList :: [Solution r f] -> Doc Source #
Null (Solution rigid flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods empty :: Solution rigid flex Source # null :: Solution rigid flex -> Bool Source #
(Show flex, Show rigid) => Show (Solution rigid flex) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> Solution rigid flex -> ShowS Source # show :: Solution rigid flex -> String Source # showList :: [Solution rigid flex] -> ShowS Source #

emptySolution :: Solution r f Source #

class Substitute r f a where Source #

Executing a substitution.

Methods

subst :: Solution r f -> a -> a Source #

#### Instances

Instances details

Substitute r f a => Substitute r f [a] Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> [a] -> [a] Source #
Ord f => Substitute r f (Constraint' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> Constraint' r f -> Constraint' r f Source #
Ord f => Substitute r f (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> SizeExpr' r f -> SizeExpr' r f Source #
Ord f => Substitute r f (Solution r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> Solution r f -> Solution r f Source #
Substitute r f a => Substitute r f (Map k a) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> Map k a -> Map k a Source #

# Constraint simplification

type CTrans r f = Constraint' r f -> Maybe [Constraint' r f] Source #

simplify1 :: (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f Source #

Returns `Nothing` if the constraint is contradictory.

ifLe :: Cmp -> a -> a -> a Source #

`Le` acts as `True`, `Lt` as `False`.

compareOffset :: Offset -> Cmp -> Offset -> Bool Source #

Interpret `Cmp` as relation on `Offset`.

# Printing

# Wellformedness

class ValidOffset a where Source #

Offsets `+ n` must be non-negative

Methods

validOffset :: a -> Bool Source #

#### Instances

Instances details

ValidOffset Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods validOffset :: Offset -> Bool Source #
ValidOffset (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods validOffset :: SizeExpr' r f -> Bool Source #

class TruncateOffset a where Source #

Make offsets non-negative by rounding up.

Methods

truncateOffset :: a -> a Source #

#### Instances

Instances details

TruncateOffset Offset Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods truncateOffset :: Offset -> Offset Source #
TruncateOffset (SizeExpr' r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods truncateOffset :: SizeExpr' r f -> SizeExpr' r f Source #

# Computing variable sets

class Ord (RigidOf a) => Rigids a where Source #

The rigid variables contained in a pice of syntax.

Associated Types

type RigidOf a Source #

Methods

rigids :: a -> Set (RigidOf a) Source #

#### Instances

Instances details

Rigids a => Rigids [a] Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf [a] |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type RigidOf [a] = RigidOf a

Methods

rigids :: [a] -> Set (RigidOf [a]) Source #

Ord r => Rigids (Constraint' r f) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (Constraint' r f) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type RigidOf (Constraint' r f) = r

Methods

rigids :: Constraint' r f -> Set (RigidOf (Constraint' r f)) Source #

Ord r => Rigids (SizeExpr' r f) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type RigidOf (SizeExpr' r f) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type RigidOf (SizeExpr' r f) = r

Methods

rigids :: SizeExpr' r f -> Set (RigidOf (SizeExpr' r f)) Source #

class Ord (FlexOf a) => Flexs a where Source #

The flexibe variables contained in a pice of syntax.

Associated Types

type FlexOf a Source #

Methods

flexs :: a -> Set (FlexOf a) Source #

#### Instances

Instances details

Flexs HypSizeConstraint Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf HypSizeConstraint |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf HypSizeConstraint = SizeMeta

Methods

flexs :: HypSizeConstraint -> Set (FlexOf HypSizeConstraint) Source #

Flexs a => Flexs [a] Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf [a] |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf [a] = FlexOf a

Methods

flexs :: [a] -> Set (FlexOf [a]) Source #

Ord flex => Flexs (Constraint' rigid flex) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (Constraint' rigid flex) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf (Constraint' rigid flex) = flex

Methods

flexs :: Constraint' rigid flex -> Set (FlexOf (Constraint' rigid flex)) Source #

Ord flex => Flexs (SizeExpr' rigid flex) Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf (SizeExpr' rigid flex) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf (SizeExpr' rigid flex) = flex

Methods

flexs :: SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex)) Source #

data NamedRigid Source #

Identifiers for rigid variables.

Constructors

NamedRigid |

Fields

- rigidName :: String

  Name for printing in debug messages.

- rigidIndex :: Int

  De Bruijn index.

#### Instances

Instances details

Pretty NamedRigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: NamedRigid -> Doc Source # prettyPrec :: Int -> NamedRigid -> Doc Source # prettyList :: [NamedRigid] -> Doc Source #
PrettyTCM SizeConstraint Source # | Assumes we are in the right context.
Instance details Defined in Agda.TypeChecking.SizedTypes.Pretty Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #
Subst SizeConstraint Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeConstraint |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeConstraint = Term

Methods

applySubst :: Substitution' (SubstArg SizeConstraint) -> SizeConstraint -> SizeConstraint Source #

NFData NamedRigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods rnf :: NamedRigid -> () Source #
Generic NamedRigid Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type Rep NamedRigid |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep NamedRigid = D1 ('MetaData "NamedRigid" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NamedRigid" 'PrefixI 'True) (S1 ('MetaSel ('Just "rigidName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "rigidIndex") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

Methods

from :: NamedRigid -> Rep NamedRigid x Source #

to :: Rep NamedRigid x -> NamedRigid Source #

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

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: NamedRigid -> NamedRigid -> Ordering Source #

(<) :: NamedRigid -> NamedRigid -> Bool Source #

(<=) :: NamedRigid -> NamedRigid -> Bool Source #

(>) :: NamedRigid -> NamedRigid -> Bool Source #

(>=) :: NamedRigid -> NamedRigid -> Bool Source #

max :: NamedRigid -> NamedRigid -> NamedRigid Source #

min :: NamedRigid -> NamedRigid -> NamedRigid Source #

Plus NamedRigid Int NamedRigid Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods plus :: NamedRigid -> Int -> NamedRigid Source #
Subst (SizeExpr' NamedRigid SizeMeta) Source # | Only for `raise`.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg (SizeExpr' NamedRigid SizeMeta) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

Methods

applySubst :: Substitution' (SubstArg (SizeExpr' NamedRigid SizeMeta)) -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #

type SubstArg SizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeConstraint = Term
type Rep NamedRigid Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep NamedRigid = D1 ('MetaData "NamedRigid" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NamedRigid" 'PrefixI 'True) (S1 ('MetaSel ('Just "rigidName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "rigidIndex") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

type SubstArg (SizeExpr' NamedRigid SizeMeta) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

data SizeMeta Source #

Size metas in size expressions.

Constructors

SizeMeta |

Fields

- sizeMetaId :: MetaId
- sizeMetaArgs :: [Int]

  De Bruijn indices.

#### Instances

Instances details

Pretty SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods pretty :: SizeMeta -> Doc Source # prettyPrec :: Int -> SizeMeta -> Doc Source # prettyList :: [SizeMeta] -> Doc Source #
PrettyTCM SizeConstraint Source # | Assumes we are in the right context.
Instance details Defined in Agda.TypeChecking.SizedTypes.Pretty Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #
PrettyTCM SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Pretty Methods prettyTCM :: MonadPretty m => SizeMeta -> m Doc Source #
Subst SizeConstraint Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeConstraint |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeConstraint = Term

Methods

applySubst :: Substitution' (SubstArg SizeConstraint) -> SizeConstraint -> SizeConstraint Source #

Subst SizeMeta Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeMeta |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeMeta = Term

Methods

applySubst :: Substitution' (SubstArg SizeMeta) -> SizeMeta -> SizeMeta Source #

NFData SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods rnf :: SizeMeta -> () Source #
Generic SizeMeta Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type Rep SizeMeta |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep SizeMeta = D1 ('MetaData "SizeMeta" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "SizeMeta" 'PrefixI 'True) (S1 ('MetaSel ('Just "sizeMetaId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId) :*: S1 ('MetaSel ('Just "sizeMetaArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])))

Methods

from :: SizeMeta -> Rep SizeMeta x Source #

to :: Rep SizeMeta x -> SizeMeta Source #

Show SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> SizeMeta -> ShowS Source # show :: SizeMeta -> String Source # showList :: [SizeMeta] -> ShowS Source #
Eq SizeMeta Source # | An equality which ignores the meta arguments.
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: SizeMeta -> SizeMeta -> Bool Source # (/=) :: SizeMeta -> SizeMeta -> Bool Source #
Ord SizeMeta Source # | An order which ignores the meta arguments.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

compare :: SizeMeta -> SizeMeta -> Ordering Source #

(<) :: SizeMeta -> SizeMeta -> Bool Source #

(<=) :: SizeMeta -> SizeMeta -> Bool Source #

(>) :: SizeMeta -> SizeMeta -> Bool Source #

(>=) :: SizeMeta -> SizeMeta -> Bool Source #

max :: SizeMeta -> SizeMeta -> SizeMeta Source #

min :: SizeMeta -> SizeMeta -> SizeMeta Source #

Subst (SizeExpr' NamedRigid SizeMeta) Source # | Only for `raise`.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg (SizeExpr' NamedRigid SizeMeta) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

Methods

applySubst :: Substitution' (SubstArg (SizeExpr' NamedRigid SizeMeta)) -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #

type SubstArg SizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeConstraint = Term
type SubstArg SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeMeta = Term
type Rep SizeMeta Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep SizeMeta = D1 ('MetaData "SizeMeta" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "SizeMeta" 'PrefixI 'True) (S1 ('MetaSel ('Just "sizeMetaId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId) :*: S1 ('MetaSel ('Just "sizeMetaArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])))

type SubstArg (SizeExpr' NamedRigid SizeMeta) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

type DBSizeExpr = SizeExpr' NamedRigid SizeMeta Source #

Size expression with de Bruijn indices.

type SizeConstraint = Constraint' NamedRigid SizeMeta Source #

data HypSizeConstraint Source #

Size constraint with de Bruijn indices.

Constructors

HypSizeConstraint |

Fields

- sizeContext :: Context
- sizeHypIds :: [Nat]

  DeBruijn indices

- sizeHypotheses :: [SizeConstraint]

  Living in `Context`.

- sizeConstraint :: SizeConstraint

  Living in `Context`.

#### Instances

Instances details

PrettyTCM HypSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Pretty Methods prettyTCM :: MonadPretty m => HypSizeConstraint -> m Doc Source #
Flexs HypSizeConstraint Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type FlexOf HypSizeConstraint |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf HypSizeConstraint = SizeMeta

Methods

flexs :: HypSizeConstraint -> Set (FlexOf HypSizeConstraint) Source #

NFData HypSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods rnf :: HypSizeConstraint -> () Source #
Generic HypSizeConstraint Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Associated Types

type Rep HypSizeConstraint |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep HypSizeConstraint = D1 ('MetaData "HypSizeConstraint" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "HypSizeConstraint" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sizeContext") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Context) :*: S1 ('MetaSel ('Just "sizeHypIds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Nat])) :*: (S1 ('MetaSel ('Just "sizeHypotheses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SizeConstraint]) :*: S1 ('MetaSel ('Just "sizeConstraint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SizeConstraint))))

Methods

from :: HypSizeConstraint -> Rep HypSizeConstraint x Source #

to :: Rep HypSizeConstraint x -> HypSizeConstraint Source #

Show HypSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> HypSizeConstraint -> ShowS Source # show :: HypSizeConstraint -> String Source # showList :: [HypSizeConstraint] -> ShowS Source #
type FlexOf HypSizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax type FlexOf HypSizeConstraint = SizeMeta
type Rep HypSizeConstraint Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

type Rep HypSizeConstraint = D1 ('MetaData "HypSizeConstraint" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "HypSizeConstraint" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sizeContext") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Context) :*: S1 ('MetaSel ('Just "sizeHypIds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Nat])) :*: (S1 ('MetaSel ('Just "sizeHypotheses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SizeConstraint]) :*: S1 ('MetaSel ('Just "sizeConstraint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SizeConstraint))))