ifscs-0.1.0.0: An inductive-form set constraint solver

Safe HaskellNone

Constraints.Set.Implementation

Contents

Synopsis

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

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

Instances

(Eq v, Eq c) => Eq (Inclusion v c) 
(Eq (Inclusion v c), Ord v, Ord c) => Ord (Inclusion v c) 
(Show v, Show c) => Show (Inclusion v c) 
NFData (Inclusion v c) 

data SetExpression v c

Expressions in the language of set constraints.

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) 

data SolvedSystem v c

The solved constraint system

Instances

(Eq v, Eq c) => Eq (SolvedSystem 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