Agda.TypeChecking.SizedTypes.Syntax

Syntax of size expressions and constraints.

Syntax

newtype Offset

Constant finite sizes n >= 0.

Constructors

O Int

Instances

Enum Offset

Methods

succ :: Offset -> Offset

pred :: Offset -> Offset

toEnum :: Int -> Offset

fromEnum :: Offset -> Int

enumFrom :: Offset -> [Offset]

enumFromThen :: Offset -> Offset -> [Offset]

enumFromTo :: Offset -> Offset -> [Offset]

enumFromThenTo :: Offset -> Offset -> Offset -> [Offset]

Eq Offset

Methods

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

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

Num Offset

Methods

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

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

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

negate :: Offset -> Offset

abs :: Offset -> Offset

signum :: Offset -> Offset

fromInteger :: Integer -> Offset

Ord Offset

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

Show Offset

Methods

showsPrec :: Int -> Offset -> ShowS

show :: Offset -> String

showList :: [Offset] -> ShowS

MeetSemiLattice Offset

Methods

meet :: Offset -> Offset -> Offset

TruncateOffset Offset

Methods

truncateOffset :: Offset -> Offset

ValidOffset Offset

Methods

validOffset :: Offset -> Bool

Negative Offset

Methods

negative :: Offset -> Bool

Plus Offset Offset Offset

Methods

plus :: Offset -> Offset -> Offset

Plus Offset Weight Weight

Methods

plus :: Offset -> Weight -> Weight

Plus Weight Offset Weight

Methods

plus :: Weight -> Offset -> Weight

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

Add offset to size expression.

Methods

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

newtype Rigid

Fixed size variables i.

Constructors

RigidId

Fields

• rigidId :: String

Instances

Eq Rigid

Methods

(==) :: Rigid -> Rigid -> Bool

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

Ord Rigid

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

Show Rigid

Methods

showsPrec :: Int -> Rigid -> ShowS

show :: Rigid -> String

showList :: [Rigid] -> ShowS

newtype Flex

Size meta variables X to solve for.

Constructors

FlexId

Fields

• flexId :: String

Instances

Eq Flex

Methods

(==) :: Flex -> Flex -> Bool

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

Ord Flex

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

Show Flex

Methods

showsPrec :: Int -> Flex -> ShowS

show :: Flex -> String

showList :: [Flex] -> ShowS

data SizeExpr' rigid flex

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

Ord f => Substitute r f (SizeExpr' r f)

Methods

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

Flexs flex (SizeExpr' rigid flex)

Methods

flexs :: SizeExpr' rigid flex -> Set flex

Rigids r (SizeExpr' r f)

Methods

rigids :: SizeExpr' r f -> Set r

Subst Term (SizeExpr' NamedRigid SizeMeta)

Only for raise.

Methods

applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta

Functor (SizeExpr' rigid)

Methods

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

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

Foldable (SizeExpr' rigid)

Methods

fold :: Monoid m => SizeExpr' rigid m -> 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)

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)

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

Methods

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

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

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

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

(Show r, Show f) => Show (SizeExpr' r f)

Methods

showsPrec :: Int -> SizeExpr' r f -> ShowS

show :: SizeExpr' r f -> String

showList :: [SizeExpr' r f] -> ShowS

TruncateOffset (SizeExpr' r f)

Methods

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

ValidOffset (SizeExpr' r f)

Methods

validOffset :: SizeExpr' r f -> Bool

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

Add offset to size expression.

Methods

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

Plus (SizeExpr' r f) Label (SizeExpr' r f)

Methods

plus :: SizeExpr' r f -> Label -> SizeExpr' r f

Plus (SizeExpr' r f) Weight (SizeExpr' r f)

Methods

plus :: SizeExpr' r f -> Weight -> SizeExpr' r f

type SizeExpr = SizeExpr' Rigid Flex

data Cmp

Comparison operator, e.g. for size expression.

Constructors

Lt

<.

Le

≤.

Instances

Bounded Cmp

Methods

minBound :: Cmp

maxBound :: Cmp

Enum Cmp

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]

Eq Cmp

Methods

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

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

Ord Cmp

Comparison operator is ordered Lt < Le.

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

Show Cmp

Methods

showsPrec :: Int -> Cmp -> ShowS

show :: Cmp -> String

showList :: [Cmp] -> ShowS

Dioid Cmp

Methods

compose :: Cmp -> Cmp -> Cmp

unitCompose :: Cmp

MeetSemiLattice Cmp

Methods

meet :: Cmp -> Cmp -> Cmp

Top Cmp

Methods

top :: Cmp

isTop :: Cmp -> Bool

data Constraint' rigid flex

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

PrettyTCM SizeConstraint

Assumes we are in the right context.

Methods

prettyTCM :: SizeConstraint -> TCM Doc

Subst Term SizeConstraint

Methods

applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint

Ord f => Substitute r f (Constraint' r f)

Methods

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

Ord flex => Flexs flex (Constraint' rigid flex)

Methods

flexs :: Constraint' rigid flex -> Set flex

Ord r => Rigids r (Constraint' r f)

Methods

rigids :: Constraint' r f -> Set r

Functor (Constraint' rigid)

Methods

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

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

Foldable (Constraint' rigid)

Methods

fold :: Monoid m => Constraint' rigid m -> 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)

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)

(Show r, Show f) => Show (Constraint' r f)

Methods

showsPrec :: Int -> Constraint' r f -> ShowS

show :: Constraint' r f -> String

showList :: [Constraint' r f] -> ShowS

type Constraint = Constraint' Rigid Flex

Polarities to specify solutions.

data Polarity

What type of solution are we looking for?

Constructors

Least

Greatest

Instances

Eq Polarity

Methods

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

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

Ord Polarity

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

Show Polarity

Methods

showsPrec :: Int -> Polarity -> ShowS

show :: Polarity -> String

showList :: [Polarity] -> ShowS

data PolarityAssignment flex

Assigning a polarity to a flexible variable.

Constructors

PolarityAssignment Polarity flex

Instances

Show flex => Show (PolarityAssignment flex)

Methods

showsPrec :: Int -> PolarityAssignment flex -> ShowS

show :: PolarityAssignment flex -> String

showList :: [PolarityAssignment flex] -> ShowS

type Polarities flex = Map flex Polarity

Type of solution wanted for each flexible.

emptyPolarities :: Polarities flex

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

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

Default polarity is Least.

Solutions.

type Solution rigid flex = Map flex (SizeExpr' rigid flex)

Partial substitution from flexible variables to size expression.

class Substitute r f a where

Executing a substitution.

Minimal complete definition

subst

Methods

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

Instances

Substitute r f a => Substitute r f [a]

Methods

subst :: Solution r f -> [a] -> [a]

Substitute r f a => Substitute r f (Map k a)

Methods

subst :: Solution r f -> Map k a -> Map k a

Ord f => Substitute r f (Constraint' r f)

Methods

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

Ord f => Substitute r f (SizeExpr' r f)

Methods

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

Constraint simplification

type CTrans r f = Constraint' r f -> Either String [Constraint' r f]

simplify1 :: (Show f, Show r, Eq r) => CTrans r f -> CTrans r f

Returns an error message if we have a contradictory constraint.

ifLe :: Cmp -> a -> a -> a

Le acts as True, Lt as False.

compareOffset :: Offset -> Cmp -> Offset -> Bool

Interpret Cmp as relation on Offset.

Printing

Wellformedness

class ValidOffset a where

Offsets + n must be non-negative

Minimal complete definition

validOffset

Methods

validOffset :: a -> Bool

Instances

ValidOffset Offset

Methods

validOffset :: Offset -> Bool

ValidOffset (SizeExpr' r f)

Methods

validOffset :: SizeExpr' r f -> Bool

class TruncateOffset a where

Make offsets non-negative by rounding up.

Minimal complete definition

truncateOffset

Methods

truncateOffset :: a -> a

Instances

TruncateOffset Offset

Methods

truncateOffset :: Offset -> Offset

TruncateOffset (SizeExpr' r f)

Methods

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

Computing variable sets

class Rigids r a where

The rigid variables contained in a pice of syntax.

Minimal complete definition

rigids

Methods

rigids :: a -> Set r

Instances

(Ord r, Rigids r a) => Rigids r [a]

Methods

rigids :: [a] -> Set r

Ord r => Rigids r (Constraint' r f)

Methods

rigids :: Constraint' r f -> Set r

Rigids r (SizeExpr' r f)

Methods

rigids :: SizeExpr' r f -> Set r

class Flexs flex a | a -> flex where

The flexibe variables contained in a pice of syntax.

Minimal complete definition

flexs

Methods

flexs :: a -> Set flex

Instances

Flexs SizeMeta HypSizeConstraint

Methods

flexs :: HypSizeConstraint -> Set SizeMeta

(Ord flex, Flexs flex a) => Flexs flex [a]

Methods

flexs :: [a] -> Set flex

Ord flex => Flexs flex (Constraint' rigid flex)

Methods

flexs :: Constraint' rigid flex -> Set flex

Flexs flex (SizeExpr' rigid flex)

Methods

flexs :: SizeExpr' rigid flex -> Set flex