Safe Haskell | None |
---|
Constraints.Set.Implementation
Contents
- data ConstraintError v c
- = NoSolution (Inclusion v c)
- | NoVariableLabel v
- data Variance
- data Inclusion v c
- data SetExpression v c
- = EmptySet
- | UniversalSet
- | SetVariable v
- | ConstructedTerm c [Variance] [SetExpression v c]
- data SolvedSystem v c
- emptySet :: SetExpression v c
- universalSet :: SetExpression v c
- setVariable :: v -> SetExpression v c
- atom :: c -> SetExpression v c
- term :: c -> [Variance] -> [SetExpression v c] -> SetExpression v c
- (<=!) :: SetExpression v c -> SetExpression v c -> Inclusion v c
- solveSystem :: (Failure (ConstraintError v c) m, Eq c, Eq v, Ord c, Ord v) => [Inclusion v c] -> m (SolvedSystem v c)
- leastSolution :: forall c m v. (Failure (ConstraintError v c) m, Ord v, Ord c) => SolvedSystem v c -> v -> m [SetExpression v c]
- data ConstraintEdge
- solvedSystemGraphElems :: (Eq v, Eq c) => SolvedSystem v c -> ([(Int, SetExpression v c)], [(Int, Int, ConstraintEdge)])
Documentation
data ConstraintError v c
The types of errors that can be encountered during constraint resolution
Constructors
NoSolution (Inclusion v c) | The system has no solution because of the given inclusion constraint |
NoVariableLabel v | When searching for a solution, the requested variable was not present in the constraint graph |
Instances
Typeable2 ConstraintError | |
(Eq v, Eq c) => Eq (ConstraintError v c) | |
(Eq (ConstraintError v c), Ord v, Ord c) => Ord (ConstraintError v c) | |
(Show v, Show c) => Show (ConstraintError v c) | |
(Typeable (ConstraintError v c), Show (ConstraintError v c), Typeable v, Typeable c, Show v, Show c) => Exception (ConstraintError v c) |
data Variance
Tags to mark term arguments as covariant or contravariant.
Constructors
Covariant | |
Contravariant |
data Inclusion v c
An inclusion is a constraint of the form se1 ⊆ se2
data SetExpression v c
Expressions in the language of set constraints.
Constructors
EmptySet | |
UniversalSet | |
SetVariable v | |
ConstructedTerm c [Variance] [SetExpression v c] |
Instances
(Eq v, Eq c) => Eq (SetExpression v c) | |
(Eq (SetExpression v c), Ord v, Ord c) => Ord (SetExpression v c) | |
(Show v, Show c) => Show (SetExpression v c) | |
NFData (SetExpression v c) |
emptySet :: SetExpression v c
Create a set expression representing the empty set
universalSet :: SetExpression v c
Create a set expression representing the universal set
setVariable :: v -> SetExpression v c
Create a new set variable with the given label
atom :: c -> SetExpression v c
Atomic terms have a label and arity zero. This is a shortcut for
term conLabel [] []
term :: c -> [Variance] -> [SetExpression v c] -> SetExpression v c
This returns a function to create terms from lists of SetExpressions. It is meant to be partially applied so that as many terms as possible can share the same reference to a label and signature.
The list of variances specifies the variance (Covariant or Contravariant) for each argument of the term. A mismatch in the length of the variance descriptor and the arguments to the term will result in a run-time error.
(<=!) :: SetExpression v c -> SetExpression v c -> Inclusion v c
Construct an inclusion relation between two set expressions.
This is equivalent to se1 ⊆ se2
.
solveSystem :: (Failure (ConstraintError v c) m, Eq c, Eq v, Ord c, Ord v) => [Inclusion v c] -> m (SolvedSystem v c)
Simplify and solve the system of set constraints
leastSolution :: forall c m v. (Failure (ConstraintError v c) m, Ord v, Ord c) => SolvedSystem v c -> v -> m [SetExpression v c]
Compute the least solution for the given variable. This can fail
if the requested variable is not present in the constraint system
(see ConstraintError
).
LS(y) = All source nodes with a predecessor edge to y, plus LS(x) for all x where x has a predecessor edge to y.
Debugging
data ConstraintEdge
Instances
solvedSystemGraphElems :: (Eq v, Eq c) => SolvedSystem v c -> ([(Int, SetExpression v c)], [(Int, Int, ConstraintEdge)])