Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.REST.WQOConstraints

Description

This module includes a typeclass for implementations of constraints on WQOs

Synopsis

data WQOConstraints impl m = OC {
- addConstraint :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
- intersect :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a
- isSatisfiable :: forall a. (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => impl a -> m Bool
- notStrongerThan :: forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool
- noConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a
- permits :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> WQO a -> Bool
- union :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a
- unsatisfiable :: forall a. impl a
- getOrdering :: forall a. impl a -> Maybe (WQO a)
}
type ConstraintGen oc base lifted m = forall m'. WQOConstraints oc m' -> Relation -> oc base -> lifted -> lifted -> m (oc base)
liftC :: (m Bool -> m' Bool) -> WQOConstraints impl m -> WQOConstraints impl m'
cmapConstraints :: (lifted' -> lifted) -> ConstraintGen oc base lifted m -> ConstraintGen oc base lifted' m
isUnsatisfiable :: (Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => WQOConstraints oc m -> oc a -> m Bool
intersectAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a
unionAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a
intersectRelation :: (Ord a, Eq a, Ord a, Hashable a, Show a) => WQOConstraints oc m -> oc a -> (a, a, Relation) -> oc a
runStateConstraints :: ConstraintGen oc base lifted (State a) -> a -> ConstraintGen oc base lifted Identity
singleton :: (Eq a, Ord a, Hashable a) => WQOConstraints oc m -> WQO a -> oc a

Documentation

data WQOConstraints impl m Source #

WQOConstraints impl m defines an implementation for tracking and checking satisfiability of constraints on arbitrary type a. Namely, instances of impl a are used to keep track of constraints. Satisfiability checking and other computations are embedded in a computational context m.

Constructors

OC

Fields

addConstraint :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
addConstraint wqo c adds constraints to c to also permit the WQO w.
intersect :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a
intersect c1 c2 returns constraints to permit only WQOs permitted by both c1 and c2. Therefore the resulting constraints are stronger (less likely to be satisifiable).
isSatisfiable :: forall a. (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => impl a -> m Bool
isSatisfiable c returns true iff c permits any WQO
notStrongerThan :: forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool
c1 notStrongerThan c2 iff any ordering permitted by c1 is also permitted by c2
noConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a
noConstraints returns an instance of constraints that permits any WQO
permits :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> WQO a -> Bool
union :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a
c1 union c2 returns constraints that permit WQOs permitted by either c1 or c2. The resulting constraints are therefore weaker (more likely to be satisfiable)
unsatisfiable :: forall a. impl a
unsatisfiable returns an instance of constraints that does not permit any WQO
getOrdering :: forall a. impl a -> Maybe (WQO a)
getOrdering c returns a concrete ordering satisfying the constraints, if one exists

type ConstraintGen oc base lifted m = forall m'. WQOConstraints oc m' -> Relation -> oc base -> lifted -> lifted -> m (oc base) Source #

ConstraintGen impl R >= t u returns the constraints on >= that guarantee the resulting relation >=', we have: 1. x >= y implies x >=' y 2. t lift(R(>=')) u Where R generates { == , >=, > } from the underlying ordering R is used to enable optimizations

liftC :: (m Bool -> m' Bool) -> WQOConstraints impl m -> WQOConstraints impl m' Source #

liftc f imp lifts the computations of imp from context m to context m'

cmapConstraints :: (lifted' -> lifted) -> ConstraintGen oc base lifted m -> ConstraintGen oc base lifted' m Source #

cmapConstraints takes a transformation f from lifted' to lifted, and transforms a constraint generator on terms of types lifted into one on terms of types lifted'

isUnsatisfiable :: (Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => WQOConstraints oc m -> oc a -> m Bool Source #

Returns true iff the constraints do not permit any WQO.

intersectAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a Source #

Given a list of constraints ocs, returns constraints that permit only the WQOs permitted by each oc in ocs

unionAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a Source #

Given a list of constraints ocs, returns constraints that permit the WQOs permitted by any oc in ocs

intersectRelation :: (Ord a, Eq a, Ord a, Hashable a, Show a) => WQOConstraints oc m -> oc a -> (a, a, Relation) -> oc a Source #

intersectRelation oc impl (f, g, r) strengthens constraints represented by impl to also ensure that f and g are related via relation r in permitted WQOs.

runStateConstraints :: ConstraintGen oc base lifted (State a) -> a -> ConstraintGen oc base lifted Identity Source #

singleton :: (Eq a, Ord a, Hashable a) => WQOConstraints oc m -> WQO a -> oc a Source #

Returns the constraints that permit a given WQO