Safe Haskell	Safe-Inferred
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 Error = TCM Doc
type CTrans r f = Constraint' r f -> Either Error [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)

Syntax

newtype Offset Source #

Constant finite sizes n >= 0.

Constructors

O Int

Instances

Instances details

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

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

PrettyTCM Flex Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods prettyTCM :: MonadPretty m => Flex -> m Doc Source #
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 Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> SizeExpr' r f -> SizeExpr' r f Source #
Foldable (SizeExpr' rigid) Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax 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 Defined in Agda.TypeChecking.SizedTypes.Syntax 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) #
Functor (SizeExpr' rigid) Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods fmap :: (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b # (<$) :: a -> SizeExpr' rigid b -> SizeExpr' rigid a #
Ord flex => Flexs (SizeExpr' rigid flex) Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Associated Types type FlexOf (SizeExpr' rigid flex) Source # 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) Source # 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) Source # Methods applySubst :: Substitution' (SubstArg (SizeExpr' NamedRigid SizeMeta)) -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta 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 #
(Show rigid, Show flex) => Show (SizeExpr' rigid flex) Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax 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 Defined in Agda.TypeChecking.SizedTypes.Syntax 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 Defined in Agda.TypeChecking.SizedTypes.Syntax 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 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 SizeExpr = SizeExpr' Rigid Flex Source #

data Cmp Source #

Comparison operator, e.g. for size expression.

Constructors

Lt	`<`.
Le	`≤`.

Instances

Instances details

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 #
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 #
Bounded Cmp Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods minBound :: Cmp # maxBound :: Cmp #
Enum Cmp Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax 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] #
Show Cmp Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> Cmp -> ShowS # show :: Cmp -> String # showList :: [Cmp] -> ShowS #
Eq Cmp Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods (==) :: Cmp -> Cmp -> Bool # (/=) :: Cmp -> Cmp -> Bool #
Ord Cmp Source #	Comparison operator is ordered `Lt < Le`.
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax 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 #

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.Solve Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #
Subst SizeConstraint Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Associated Types type SubstArg SizeConstraint Source # 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 #
Foldable (Constraint' rigid) Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax 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 Defined in Agda.TypeChecking.SizedTypes.Syntax 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) #
Functor (Constraint' rigid) Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods fmap :: (a -> b) -> Constraint' rigid a -> Constraint' rigid b # (<$) :: a -> Constraint' rigid b -> Constraint' rigid a #
Ord flex => Flexs (Constraint' rigid flex) Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Associated Types type FlexOf (Constraint' rigid flex) Source # 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) Source # Methods rigids :: Constraint' r f -> Set (RigidOf (Constraint' r f)) 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 #
(Show rigid, Show flex) => Show (Constraint' rigid flex) Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> Constraint' rigid flex -> ShowS # show :: Constraint' rigid flex -> String # showList :: [Constraint' rigid flex] -> ShowS #
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 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 #
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 #
(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 #
(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 #

type Error = TCM Doc Source #

Error messages produced by the constraint simplification monad.

Constraint simplification

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

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

Returns an error message if we have a contradictory constraint.

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] Source # 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) Source # 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) Source # 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.Solve Associated Types type FlexOf HypSizeConstraint Source # 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] Source # 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) Source # 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) Source # Methods flexs :: SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex)) Source #