| Safe Haskell | None |
|---|
Agda.TypeChecking.SizedTypes.Syntax
Contents
Description
Syntax of size expressions and constraints.
- type Offset = 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
- type Solution rigid flex = Map flex (SizeExpr' rigid flex)
- emptySolution :: Map k a
- class Substitute r f a where
- type CTrans r f = Constraint' r f -> Maybe [Constraint' r f]
- simplify1 :: 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
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) | |
| Ord flex => Flexs flex (SizeExpr' rigid flex) | |
| Rigids r (SizeExpr' r f) | |
| Functor (SizeExpr' rigid) | |
| Foldable (SizeExpr' rigid) | |
| Traversable (SizeExpr' rigid) | |
| (Eq rigid, Eq flex) => Eq (SizeExpr' rigid flex) | |
| (Ord rigid, Ord flex) => Ord (SizeExpr' rigid flex) | |
| (Show r, Show f) => Show (SizeExpr' r f) | |
| TruncateOffset (SizeExpr' r f) | |
| ValidOffset (SizeExpr' r f) | |
| Subst (SizeExpr' NamedRigid SizeMeta) | Only for |
| Plus (SizeExpr' r f) Offset (SizeExpr' r f) | Add offset to size expression. |
| Plus (SizeExpr' r f) Label (SizeExpr' r f) | |
| Plus (SizeExpr' r f) Weight (SizeExpr' r f) |
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
| Subst SizeConstraint | |
| PrettyTCM SizeConstraint | Assumes we are in the right context. |
| Ord f => Substitute r f (Constraint' r f) | |
| Ord flex => Flexs flex (Constraint' rigid flex) | |
| Ord r => Rigids r (Constraint' r f) | |
| Functor (Constraint' rigid) | |
| Foldable (Constraint' rigid) | |
| Traversable (Constraint' rigid) | |
| (Show r, Show f) => Show (Constraint' r f) |
type Constraint = Constraint' Rigid FlexSource
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
| Show flex => Show (PolarityAssignment flex) |
type Polarities flex = Map flex PolaritySource
Type of solution wanted for each flexible.
emptyPolarities :: Polarities flexSource
polaritiesFromAssignments :: Ord flex => [PolarityAssignment flex] -> Polarities flexSource
getPolarity :: Ord flex => Polarities flex -> flex -> PolaritySource
Default polarity is Least.
Solutions.
type Solution rigid flex = Map flex (SizeExpr' rigid flex)Source
Partial substitution from flexible variables to size expression.
emptySolution :: Map k aSource
class Substitute r f a whereSource
Executing a substitution.
Instances
| Substitute r f a => Substitute r f [a] | |
| Ord f => Substitute r f (Constraint' r f) | |
| Ord f => Substitute r f (SizeExpr' r f) |
Constraint simplification
type CTrans r f = Constraint' r f -> Maybe [Constraint' r f]Source
simplify1 :: Eq r => CTrans r f -> CTrans r fSource
Returns Nothing if we have a contradictory constraint.
Printing
Wellformedness
class ValidOffset a whereSource
Offsets + n must be non-negative
Methods
validOffset :: a -> BoolSource
Instances
class TruncateOffset a whereSource
Make offsets non-negative by rounding up.
Methods
truncateOffset :: a -> aSource
Instances
Computing variable sets
The rigid variables contained in a pice of syntax.