Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.SizedTypes.Syntax
Contents
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
- type SizeExpr = SizeExpr' Rigid Flex
- data Cmp
- data Constraint' rigid flex = Constraint {}
- type Constraint = Constraint' Rigid Flex
- data Polarity
- 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
- type CTrans r f = Constraint' r f -> Either String [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 Rigids r a where
- rigids :: a -> Set r
- class Flexs flex a | a -> flex where
- flexs :: a -> Set flex
Syntax
Constant finite sizes n >= 0
.
Constructors
O Int |
Instances
Enum Offset Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax | |
Eq Offset Source # | |
Num Offset Source # | |
Ord Offset Source # | |
Show Offset Source # | |
MeetSemiLattice Offset Source # | |
Pretty Offset Source # | |
TruncateOffset Offset Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods truncateOffset :: Offset -> Offset Source # | |
ValidOffset Offset Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods validOffset :: Offset -> Bool Source # | |
Negative Offset Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver | |
Plus Offset Offset Offset Source # | |
Plus Offset Weight Weight Source # | |
Plus Weight Offset Weight Source # | |
Plus (SizeExpr' r f) Offset (SizeExpr' r f) Source # | Add offset to size expression. |
Fixed size variables i
.
Size meta variables X
to solve for.
data SizeExpr' rigid flex Source #
Size expressions appearing in constraints.
Constructors
Const | Constant number |
Rigid | Variable plus offset |
Infty | Infinity |
Flex | Meta variable |
Instances
Ord f => Substitute r f (SizeExpr' r f) Source # | |
Flexs flex (SizeExpr' rigid flex) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax | |
Rigids r (SizeExpr' r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax | |
Subst Term (SizeExpr' NamedRigid SizeMeta) Source # | Only for |
Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source # | |
Functor (SizeExpr' rigid) Source # | |
Foldable (SizeExpr' rigid) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax 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 | |
Traversable (SizeExpr' rigid) Source # | |
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) | |
(Eq rigid, Eq flex) => Eq (SizeExpr' rigid flex) Source # | |
(Ord rigid, Ord flex) => Ord (SizeExpr' rigid flex) Source # | |
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 | |
(Show rigid, Show flex) => Show (SizeExpr' rigid flex) Source # | |
(Pretty r, Pretty f) => Pretty (SizeExpr' r f) Source # | |
TruncateOffset (SizeExpr' r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods truncateOffset :: SizeExpr' r f -> SizeExpr' r f Source # | |
ValidOffset (SizeExpr' r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods validOffset :: SizeExpr' r f -> Bool Source # | |
Plus (SizeExpr' r f) Offset (SizeExpr' r f) Source # | Add offset to size expression. |
Plus (SizeExpr' r f) Label (SizeExpr' r f) Source # | |
Plus (SizeExpr' r f) Weight (SizeExpr' r f) Source # | |
Comparison operator, e.g. for size expression.
data Constraint' rigid flex Source #
Constraint: an inequation between size expressions,
e.g. X < ∞
or i + 3 ≤ j
.
Constructors
Constraint | |
Instances
PrettyTCM SizeConstraint Source # | Assumes we are in the right context. |
Defined in Agda.TypeChecking.SizedTypes.Solve | |
Subst Term SizeConstraint Source # | |
Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint Source # | |
Ord f => Substitute r f (Constraint' r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods subst :: Solution r f -> Constraint' r f -> Constraint' r f Source # | |
Ord flex => Flexs flex (Constraint' rigid flex) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods flexs :: Constraint' rigid flex -> Set flex Source # | |
Ord r => Rigids r (Constraint' r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods rigids :: Constraint' r f -> Set r Source # | |
Functor (Constraint' rigid) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods fmap :: (a -> b) -> Constraint' rigid a -> Constraint' rigid b (<$) :: a -> Constraint' rigid b -> Constraint' rigid a # | |
Foldable (Constraint' rigid) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax 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) Source # | |
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) | |
(Show rigid, Show flex) => Show (Constraint' rigid flex) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods showsPrec :: Int -> Constraint' rigid flex -> ShowS show :: Constraint' rigid flex -> String showList :: [Constraint' rigid flex] -> ShowS | |
(Pretty r, Pretty f) => Pretty (Constraint' r f) Source # | |
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 # |
type Constraint = Constraint' Rigid Flex Source #
Polarities to specify solutions.
What type of solution are we looking for?
data PolarityAssignment flex Source #
Assigning a polarity to a flexible variable.
Constructors
PolarityAssignment Polarity flex |
Instances
Pretty flex => Pretty (PolarityAssignment flex) Source # | |
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
|
emptySolution :: Solution r f Source #
class Substitute r f a where Source #
Executing a substitution.
Instances
Substitute r f a => Substitute r f [a] Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax | |
Ord f => Substitute r f (Solution r f) Source # | |
Substitute r f a => Substitute r f (Map k a) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax | |
Ord f => Substitute r f (Constraint' r f) Source # | |
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 # | |
Constraint simplification
type CTrans r f = Constraint' r f -> Either String [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.
Printing
Wellformedness
class ValidOffset a where Source #
Offsets + n
must be non-negative
Methods
validOffset :: a -> Bool Source #
Instances
ValidOffset Offset Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods validOffset :: Offset -> Bool Source # | |
ValidOffset (SizeExpr' r f) Source # | |
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
TruncateOffset Offset Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods truncateOffset :: Offset -> Offset Source # | |
TruncateOffset (SizeExpr' r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods truncateOffset :: SizeExpr' r f -> SizeExpr' r f Source # |
Computing variable sets
class Rigids r a where Source #
The rigid variables contained in a pice of syntax.
Instances
(Ord r, Rigids r a) => Rigids r [a] Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax | |
Ord r => Rigids r (Constraint' r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods rigids :: Constraint' r f -> Set r Source # | |
Rigids r (SizeExpr' r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax |
class Flexs flex a | a -> flex where Source #
The flexibe variables contained in a pice of syntax.
Instances
Flexs SizeMeta HypSizeConstraint Source # | |
Defined in Agda.TypeChecking.SizedTypes.Solve Methods flexs :: HypSizeConstraint -> Set SizeMeta Source # | |
(Ord flex, Flexs flex a) => Flexs flex [a] Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax | |
Ord flex => Flexs flex (Constraint' rigid flex) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax Methods flexs :: Constraint' rigid flex -> Set flex Source # | |
Flexs flex (SizeExpr' rigid flex) Source # | |
Defined in Agda.TypeChecking.SizedTypes.Syntax |