Intensional.Constraints

Atomic constraints and sets of atomic constraints, represented as antichains. Saturation and restriction.

Documentation

data CInfo

Type type of auxilliary information attached to constraints c:

• prov c is the module in which the constraint was created
• span c is the originating location of the rhs of the constraint

INV: CInfo does not determine equality of constraints.

Constructors

CInfo

Fields

• prov :: Module
• sspn :: SrcSpan

Instances

Eq CInfo

Defined in Intensional.Constraints

Methods

(==) :: CInfo -> CInfo -> Bool

(/=) :: CInfo -> CInfo -> Bool

Ord CInfo

Defined in Intensional.Constraints

Methods

compare :: CInfo -> CInfo -> Ordering

(<) :: CInfo -> CInfo -> Bool

(<=) :: CInfo -> CInfo -> Bool

(>) :: CInfo -> CInfo -> Bool

(>=) :: CInfo -> CInfo -> Bool

max :: CInfo -> CInfo -> CInfo

min :: CInfo -> CInfo -> CInfo

Binary CInfo

Defined in Intensional.Constraints

Methods

put_ :: BinHandle -> CInfo -> IO ()

put :: BinHandle -> CInfo -> IO (Bin CInfo)

get :: BinHandle -> IO CInfo

Outputable CInfo

Defined in Intensional.Constraints

Methods

ppr :: CInfo -> SDoc

pprPrec :: Rational -> CInfo -> SDoc

type Atomic = Constraint 'L 'R

The type of constraints c of shape guard c ? left c ⊆ right c that originated from the source at srcSpan c.

data Constraint l r

Constructors

Constraint

Fields

• left :: K l
• right :: K r
• guard :: Guard
• cinfo :: CInfo

Instances

Semigroup ConstraintSet

Defined in Intensional.Constraints

Methods

(<>) :: ConstraintSet -> ConstraintSet -> ConstraintSet

sconcat :: NonEmpty ConstraintSet -> ConstraintSet

stimes :: Integral b => b -> ConstraintSet -> ConstraintSet

Monoid ConstraintSet

Defined in Intensional.Constraints

Methods

mempty :: ConstraintSet

mappend :: ConstraintSet -> ConstraintSet -> ConstraintSet

mconcat :: [ConstraintSet] -> ConstraintSet

Binary ConstraintSet

Defined in Intensional.Constraints

Methods

put_ :: BinHandle -> ConstraintSet -> IO ()

put :: BinHandle -> ConstraintSet -> IO (Bin ConstraintSet)

get :: BinHandle -> IO ConstraintSet

Outputable ConstraintSet

Defined in Intensional.Constraints

Methods

ppr :: ConstraintSet -> SDoc

pprPrec :: Rational -> ConstraintSet -> SDoc

Refined ConstraintSet

Defined in Intensional.Constraints

Methods

domain :: ConstraintSet -> Domain

rename :: RVar -> RVar -> ConstraintSet -> ConstraintSet

prpr :: (RVar -> SDoc) -> ConstraintSet -> SDoc

Eq (Constraint l r)

Defined in Intensional.Constraints

Methods

(==) :: Constraint l r -> Constraint l r -> Bool

(/=) :: Constraint l r -> Constraint l r -> Bool

(Binary (K l), Binary (K r)) => Binary (Constraint l r)

Defined in Intensional.Constraints

Methods

put_ :: BinHandle -> Constraint l r -> IO ()

put :: BinHandle -> Constraint l r -> IO (Bin (Constraint l r))

get :: BinHandle -> IO (Constraint l r)

Outputable (Constraint l r)

Defined in Intensional.Constraints

Methods

ppr :: Constraint l r -> SDoc

pprPrec :: Rational -> Constraint l r -> SDoc

Refined (Constraint l r)

Defined in Intensional.Constraints

Methods

domain :: Constraint l r -> Domain

rename :: RVar -> RVar -> Constraint l r -> Constraint l r

prpr :: (RVar -> SDoc) -> Constraint l r -> SDoc

modInfo :: Atomic -> Module

spanInfo :: Atomic -> SrcSpan

isTriviallyUnsat :: Atomic -> Bool

Given an atomic constraint a, isTriviallyUnsat a just if a is of the form G ? k in {}.

headVar :: Atomic -> Maybe (Int, Name)

bodyVars :: Atomic -> Set (Int, Name)

impliedBy :: Atomic -> Atomic -> Bool

Given two atomic constraints a and b, a impliedBy b just if a and b have the same body and the guard of a is implied by the guard of b.

tautology :: Atomic -> Bool

Given an atomic constraint a, tautology a just if a is satisfied in every assignment.

resolve :: CInfo -> Atomic -> Atomic -> Maybe Atomic

When m is the current module: Given atomic constraints a and b, resolve m a b is:

• Nothing if the resolvant of a and b is a tautology
• Just r otherwise, where r is the resolvant as an atomic constraint

data ConstraintSetF a

Constructors

ConstraintSetF

Fields

• definiteVV :: IntMap (NameEnv (HashMap Int [a]))
• definiteKV :: IntMap (NameEnv (HashMap Name [a]))
• goal :: [a]
• revMap :: Map (Int, Name) [Atomic]

Instances

Semigroup ConstraintSet

Defined in Intensional.Constraints

Methods

(<>) :: ConstraintSet -> ConstraintSet -> ConstraintSet

sconcat :: NonEmpty ConstraintSet -> ConstraintSet

stimes :: Integral b => b -> ConstraintSet -> ConstraintSet

Monoid ConstraintSet

Defined in Intensional.Constraints

Methods

mempty :: ConstraintSet

mappend :: ConstraintSet -> ConstraintSet -> ConstraintSet

mconcat :: [ConstraintSet] -> ConstraintSet

Binary ConstraintSet

Defined in Intensional.Constraints

Methods

put_ :: BinHandle -> ConstraintSet -> IO ()

put :: BinHandle -> ConstraintSet -> IO (Bin ConstraintSet)

get :: BinHandle -> IO ConstraintSet

Outputable ConstraintSet

Defined in Intensional.Constraints

Methods

ppr :: ConstraintSet -> SDoc

pprPrec :: Rational -> ConstraintSet -> SDoc

Refined ConstraintSet

Defined in Intensional.Constraints

Methods

domain :: ConstraintSet -> Domain

rename :: RVar -> RVar -> ConstraintSet -> ConstraintSet

prpr :: (RVar -> SDoc) -> ConstraintSet -> SDoc

type ConstraintSet = ConstraintSetF Atomic

The type of sets of constraints.

We say that a set of constraints cs is reduced just if, for all X, d, Y, k: definiteVV cs X d Y, definiteKV cs X d k and goal cs are non-increasing lists wrt impliedBy.

We say that a set of constraints cs is an antichain just if each of these lists are also non-decreasing.

Most sets of constraints we process are reduced, but we allow non-reduced constraint sets to occur as a consequence of renaming of variables.

Many sets of constraints are also antichains, for example, when filtering a reduced constraint set one can guarantee the new constraint set will be an antichain by using insert and constructing the new constraint set in the reverse order. Constraint sets returned from saturation will always be antichains.

fromList :: [Atomic] -> ConstraintSet

Given a list of atomic constraints cs, fromList cs is largest antichain contained in cs

empty :: ConstraintSet

empty is the empty constraint set

unsats :: ConstraintSet -> ConstraintSet

Given a constraint set cs, unsats cs is the constraint set consisting of just those trivially unsatisfiable constraints in cs.

size :: ConstraintSet -> Int

When cs is a constraint set, size cs is its cardinality.

unsafeInsert :: Atomic -> ConstraintSet -> ConstraintSet

When a is an atomic constraint and cs a constraint set, unsafeInsert a cs is the constraint set obtained by inserting a into cs.

Note: unsafeInsert a cs may not be reduced even if cs is.

insert' :: Atomic -> ConstraintSet -> Maybe ConstraintSet

When a is an atomic constraint and cs is a constraint antichain insert a cs is:

• Nothing just if a is already implied by some constraint in cs.
• Just ds otherwise, where ds is the constraint antichain obtained by inserting a into cs. Note: ds may be smaller than cs.

insert :: Atomic -> ConstraintSet -> ConstraintSet

When a is an atomic constraint and cs is a constraint set insert a cs is the constraint set obtained by inserting a into cs.

If cs is reduced then so is insert a cs. However, insert a cs may not be an antichain even when cs is.

guardWith :: Guard -> ConstraintSet -> ConstraintSet

When g is a guard and cs a set of constraints, guardWith g cs is the set of constraints obtained from cs by appending g to every guard of every constraint.

saturate :: CInfo -> IntSet -> ConstraintSet -> ConstraintSet

When iface is a set of interface variables and ci is the current ctx and cs is a constraint set, saturate ci iface cs is the constraint set obtained from cs by saturation and restriction to iface.

eligible :: IntSet -> Atomic -> Bool

Given a set of interface variables exts and a constraint c, eligible exts c just if there are no interface variables in the head of c and only interface variables elsewhere in c.

(This means it is eligible to be used as the left-constraint in a resolution step.)

cexs :: CInfo -> ConstraintSet -> ConstraintSet

Given some context ci and constraints cs attempt to build a model of cs. cexs ci cs is the set of trivially unsatisfiable constrants obtained from the candidate model.

fix :: CInfo -> IntSet -> State (ConstraintSet, ConstraintSet) ()

When exts is the set of interface variables and ci is the current ctx fix ci exts is the stateful computation that transforms an initial state (ls, rs) where ls are all unit constraints modulo exts and ls is contained in rs, into a final state (ls', rs') in which ls is empty and rs' is the saturation of rs.

saturate1 :: CInfo -> IntSet -> State (ConstraintSet, ConstraintSet) ()

When exts is a set of interface variables and ci is the current ctx saturate1 ci exts is the stateful computation that takes an initial state (ls, rs) consisting of a pair of constraint sets with ls being unit clauses modulo exts and ls being contained in rs to a final state (ls', rs') in which:

• ls' is those constraints in rs' that are not in rs and which are unit modulo exts.
• rs' contains all the constraints obtained from rs by resolving on the left with each clauses from ls once.

Orphan instances

Foldable UniqFM

Methods

fold :: Monoid m => UniqFM m -> m

foldMap :: Monoid m => (a -> m) -> UniqFM a -> m

foldMap' :: Monoid m => (a -> m) -> UniqFM a -> m

foldr :: (a -> b -> b) -> b -> UniqFM a -> b

foldr' :: (a -> b -> b) -> b -> UniqFM a -> b

foldl :: (b -> a -> b) -> b -> UniqFM a -> b

foldl' :: (b -> a -> b) -> b -> UniqFM a -> b

foldr1 :: (a -> a -> a) -> UniqFM a -> a

foldl1 :: (a -> a -> a) -> UniqFM a -> a

toList :: UniqFM a -> [a]

null :: UniqFM a -> Bool

length :: UniqFM a -> Int

elem :: Eq a => a -> UniqFM a -> Bool

maximum :: Ord a => UniqFM a -> a

minimum :: Ord a => UniqFM a -> a

sum :: Num a => UniqFM a -> a

product :: Num a => UniqFM a -> a