Syntax

Methods

(+) :: Offset -> Offset -> Offset

(-) :: Offset -> Offset -> Offset

(*) :: Offset -> Offset -> Offset

negate :: Offset -> Offset

abs :: Offset -> Offset

signum :: Offset -> Offset

fromInteger :: Integer -> Offset

Show Offset Source #

Instance details

Methods

showsPrec :: Int -> Offset -> ShowS

show :: Offset -> String

showList :: [Offset] -> ShowS

Eq Offset Source #

Instance details

Methods

(==) :: Offset -> Offset -> Bool

(/=) :: Offset -> Offset -> Bool

Ord Offset Source #

Instance details

Methods

compare :: Offset -> Offset -> Ordering

(<) :: Offset -> Offset -> Bool

(<=) :: Offset -> Offset -> Bool

(>) :: Offset -> Offset -> Bool

(>=) :: Offset -> Offset -> Bool

max :: Offset -> Offset -> Offset

min :: Offset -> Offset -> Offset

Plus Offset Offset Offset Source #

Instance details

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

Methods

plus :: SizeExpr' r f -> Offset -> SizeExpr' r f Source #

type Rep Offset Source #

Instance details

type Rep Offset = D1 ('MetaData "Offset" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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 show :: Rigid -> String showList :: [Rigid] -> ShowS
Eq Rigid Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: Rigid -> Rigid -> Bool (/=) :: Rigid -> Rigid -> Bool
Ord Rigid Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods compare :: Rigid -> Rigid -> Ordering (<) :: Rigid -> Rigid -> Bool (<=) :: Rigid -> Rigid -> Bool (>) :: Rigid -> Rigid -> Bool (>=) :: Rigid -> Rigid -> Bool max :: Rigid -> Rigid -> Rigid min :: Rigid -> Rigid -> Rigid

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 show :: Flex -> String showList :: [Flex] -> ShowS
Eq Flex Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: Flex -> Flex -> Bool (/=) :: Flex -> Flex -> Bool
Ord Flex Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods compare :: Flex -> Flex -> Ordering (<) :: Flex -> Flex -> Bool (<=) :: Flex -> Flex -> Bool (>) :: Flex -> Flex -> Bool (>=) :: Flex -> Flex -> Bool max :: Flex -> Flex -> Flex min :: Flex -> Flex -> Flex

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

Methods

subst :: Solution r f -> SizeExpr' r f -> SizeExpr' r f Source #

Functor (SizeExpr' rigid) Source #

Instance details

Methods

fmap :: (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b

(<$) :: a -> SizeExpr' rigid b -> SizeExpr' rigid a #

Foldable (SizeExpr' rigid) Source #

Instance details

Methods

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

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

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

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

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

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

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

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

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

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

null :: SizeExpr' rigid a -> Bool

length :: SizeExpr' rigid a -> Int

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

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

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

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

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

Traversable (SizeExpr' rigid) Source #

Instance details

Methods

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

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

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

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

(Pretty r, Pretty f) => Pretty (SizeExpr' r f) Source #

Instance details

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

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

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

Methods

truncateOffset :: SizeExpr' r f -> SizeExpr' r f Source #

ValidOffset (SizeExpr' r f) Source #

Instance details

Methods

validOffset :: SizeExpr' r f -> Bool Source #

Subst (SizeExpr' NamedRigid SizeMeta) Source #

Only for raise.

Instance details

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

Methods

rnf :: SizeExpr' r f -> ()

Generic (SizeExpr' rigid flex) Source #

Instance details

Associated Types

type Rep (SizeExpr' rigid flex)

Instance details

type Rep (SizeExpr' rigid flex) = D1 ('MetaData "SizeExpr'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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

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

(Show rigid, Show flex) => Show (SizeExpr' rigid flex) Source #

Instance details

Methods

showsPrec :: Int -> SizeExpr' rigid flex -> ShowS

show :: SizeExpr' rigid flex -> String

showList :: [SizeExpr' rigid flex] -> ShowS

(Eq rigid, Eq flex) => Eq (SizeExpr' rigid flex) Source #

Instance details

Methods

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

(/=) :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool

(Ord rigid, Ord flex) => Ord (SizeExpr' rigid flex) Source #

Instance details

Methods

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

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

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

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

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

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

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

Plus (SizeExpr' r f) Offset (SizeExpr' r f) Source #

Add offset to size expression.

Instance details

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

type FlexOf (SizeExpr' rigid flex) = flex

type RigidOf (SizeExpr' r f) Source #

Instance details

type RigidOf (SizeExpr' r f) = r

type SubstArg (SizeExpr' NamedRigid SizeMeta) Source #

Instance details

type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

type Rep (SizeExpr' rigid flex) Source #

Instance details

type Rep (SizeExpr' rigid flex) = D1 ('MetaData "SizeExpr'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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

Methods

pretty :: Cmp -> Doc Source #

prettyPrec :: Int -> Cmp -> Doc Source #

prettyList :: [Cmp] -> Doc Source #

Dioid Cmp Source #

Instance details

Methods

compose :: Cmp -> Cmp -> Cmp Source #

unitCompose :: Cmp Source #

MeetSemiLattice Cmp Source #

Instance details

Methods

meet :: Cmp -> Cmp -> Cmp Source #

Top Cmp Source #

Instance details

Methods

top :: Cmp Source #

isTop :: Cmp -> Bool Source #

NFData Cmp Source #

Instance details

Methods

rnf :: Cmp -> ()

Bounded Cmp Source #

Instance details

Methods

minBound :: Cmp

maxBound :: Cmp

Enum Cmp Source #

Instance details

Methods

succ :: Cmp -> Cmp

pred :: Cmp -> Cmp

toEnum :: Int -> Cmp

fromEnum :: Cmp -> Int

enumFrom :: Cmp -> [Cmp]

enumFromThen :: Cmp -> Cmp -> [Cmp]

enumFromTo :: Cmp -> Cmp -> [Cmp]

enumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]

Generic Cmp Source #

Instance details

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.6.20240731-inplace" 'False) (C1 ('MetaCons "Lt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Le" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: Cmp -> Rep Cmp x

to :: Rep Cmp x -> Cmp

Show Cmp Source #

Instance details

Methods

showsPrec :: Int -> Cmp -> ShowS

show :: Cmp -> String

showList :: [Cmp] -> ShowS

Eq Cmp Source #

Instance details

Methods

(==) :: Cmp -> Cmp -> Bool

(/=) :: Cmp -> Cmp -> Bool

Ord Cmp Source #

Comparison operator is ordered Lt < Le.

Instance details

Methods

compare :: Cmp -> Cmp -> Ordering

(<) :: Cmp -> Cmp -> Bool

(<=) :: Cmp -> Cmp -> Bool

(>) :: Cmp -> Cmp -> Bool

(>=) :: Cmp -> Cmp -> Bool

max :: Cmp -> Cmp -> Cmp

min :: Cmp -> Cmp -> Cmp

type Rep Cmp Source #

Instance details

type Rep Cmp = D1 ('MetaData "Cmp" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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

Methods

prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #

Subst SizeConstraint Source #

Instance details

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

Methods

subst :: Solution r f -> Constraint' r f -> Constraint' r f Source #

Functor (Constraint' rigid) Source #

Instance details

Methods

fmap :: (a -> b) -> Constraint' rigid a -> Constraint' rigid b

(<$) :: a -> Constraint' rigid b -> Constraint' rigid a #

Foldable (Constraint' rigid) Source #

Instance details

Methods

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

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

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

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

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

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

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

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

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

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

null :: Constraint' rigid a -> Bool

length :: Constraint' rigid a -> Int

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

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

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

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

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

Traversable (Constraint' rigid) Source #

Instance details

Methods

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

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

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

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

(Pretty r, Pretty f) => Pretty (Constraint' r f) Source #

Instance details

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

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

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

Methods

rnf :: Constraint' r f -> ()

Generic (Constraint' rigid flex) Source #

Instance details

Associated Types

type Rep (Constraint' rigid flex)

Instance details

type Rep (Constraint' rigid flex) = D1 ('MetaData "Constraint'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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

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

(Show rigid, Show flex) => Show (Constraint' rigid flex) Source #

Instance details

Methods

showsPrec :: Int -> Constraint' rigid flex -> ShowS

show :: Constraint' rigid flex -> String

showList :: [Constraint' rigid flex] -> ShowS

type SubstArg SizeConstraint Source #

Instance details

type SubstArg SizeConstraint = Term

type FlexOf (Constraint' rigid flex) Source #

Instance details

type FlexOf (Constraint' rigid flex) = flex

type RigidOf (Constraint' r f) Source #

Instance details

type RigidOf (Constraint' r f) = r

type Rep (Constraint' rigid flex) Source #

Instance details

type Rep (Constraint' rigid flex) = D1 ('MetaData "Constraint'" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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 (/=) :: Polarity -> Polarity -> Bool
Ord Polarity Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods compare :: Polarity -> Polarity -> Ordering (<) :: Polarity -> Polarity -> Bool (<=) :: Polarity -> Polarity -> Bool (>) :: Polarity -> Polarity -> Bool (>=) :: Polarity -> Polarity -> Bool max :: Polarity -> Polarity -> Polarity min :: Polarity -> Polarity -> Polarity

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 show :: Solution rigid flex -> String showList :: [Solution rigid flex] -> ShowS

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

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

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

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

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

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

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

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

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

Methods

prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #

Subst SizeConstraint Source #

Instance details

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

Methods

rnf :: NamedRigid -> ()

Generic NamedRigid Source #

Instance details

Associated Types

type Rep NamedRigid

Instance details

type Rep NamedRigid = D1 ('MetaData "NamedRigid" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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

to :: Rep NamedRigid x -> NamedRigid

Show NamedRigid Source #

Instance details

Methods

showsPrec :: Int -> NamedRigid -> ShowS

show :: NamedRigid -> String

showList :: [NamedRigid] -> ShowS

Eq NamedRigid Source #

Instance details

Methods

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

(/=) :: NamedRigid -> NamedRigid -> Bool

Ord NamedRigid Source #

Instance details

Methods

compare :: NamedRigid -> NamedRigid -> Ordering

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

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

(>) :: NamedRigid -> NamedRigid -> Bool

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

max :: NamedRigid -> NamedRigid -> NamedRigid

min :: NamedRigid -> NamedRigid -> NamedRigid

Plus NamedRigid Int NamedRigid Source #

Instance details

Methods

plus :: NamedRigid -> Int -> NamedRigid Source #

Subst (SizeExpr' NamedRigid SizeMeta) Source #

Only for raise.

Instance details

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

type SubstArg SizeConstraint = Term

type Rep NamedRigid Source #

Instance details

type Rep NamedRigid = D1 ('MetaData "NamedRigid" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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

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

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

Methods

prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #

PrettyTCM SizeMeta Source #

Instance details

Methods

prettyTCM :: MonadPretty m => SizeMeta -> m Doc Source #

Subst SizeConstraint Source #

Instance details

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

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

Methods

rnf :: SizeMeta -> ()

Generic SizeMeta Source #

Instance details

Associated Types

type Rep SizeMeta

Instance details

type Rep SizeMeta = D1 ('MetaData "SizeMeta" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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

to :: Rep SizeMeta x -> SizeMeta

Show SizeMeta Source #

Instance details

Methods

showsPrec :: Int -> SizeMeta -> ShowS

show :: SizeMeta -> String

showList :: [SizeMeta] -> ShowS

Eq SizeMeta Source #

An equality which ignores the meta arguments.

Instance details

Methods

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

(/=) :: SizeMeta -> SizeMeta -> Bool

Ord SizeMeta Source #

An order which ignores the meta arguments.

Instance details

Methods

compare :: SizeMeta -> SizeMeta -> Ordering

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

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

(>) :: SizeMeta -> SizeMeta -> Bool

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

max :: SizeMeta -> SizeMeta -> SizeMeta

min :: SizeMeta -> SizeMeta -> SizeMeta

Subst (SizeExpr' NamedRigid SizeMeta) Source #

Only for raise.

Instance details

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

type SubstArg SizeConstraint = Term

type SubstArg SizeMeta Source #

Instance details

type SubstArg SizeMeta = Term

type Rep SizeMeta Source #

Instance details

type Rep SizeMeta = D1 ('MetaData "SizeMeta" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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

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

Methods

prettyTCM :: MonadPretty m => HypSizeConstraint -> m Doc Source #

Flexs HypSizeConstraint Source #

Instance details

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

Methods

rnf :: HypSizeConstraint -> ()

Generic HypSizeConstraint Source #

Instance details

Associated Types

type Rep HypSizeConstraint

Instance details

type Rep HypSizeConstraint = D1 ('MetaData "HypSizeConstraint" "Agda.TypeChecking.SizedTypes.Syntax" "Agda-2.6.20240731-inplace" '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

to :: Rep HypSizeConstraint x -> HypSizeConstraint

Show HypSizeConstraint Source #

Instance details

Methods

showsPrec :: Int -> HypSizeConstraint -> ShowS

show :: HypSizeConstraint -> String

showList :: [HypSizeConstraint] -> ShowS

type FlexOf HypSizeConstraint Source #

Instance details

type FlexOf HypSizeConstraint = SizeMeta

type Rep HypSizeConstraint Source #

Instance details