Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.REST.OCAlgebra

Synopsis

data OCAlgebra c a m = OCAlgebra {
- isSat :: c -> m Bool
- refine :: c -> a -> a -> c
- top :: c
- union :: c -> c -> c
- notStrongerThan :: c -> c -> m Bool
}
fuelOC :: Monad m => Int -> OCAlgebra Int a m
contramap :: forall c a b m. (b -> a) -> OCAlgebra c a m -> OCAlgebra c b m
bimapConstraints :: forall c d a m. (c -> d) -> (d -> c) -> OCAlgebra c a m -> OCAlgebra d a m

Documentation

data OCAlgebra c a m Source #

The "Ordering Constraint Algebra", as described in section 4.2 of the paper. OCAlgebra c a m is an OCA with language of constraints c, applied to terms of type a. m is the computation context for isSat.

Constructors

OCAlgebra

Fields

isSat :: c -> m Bool
Checks if the constraints are satisfiable
refine :: c -> a -> a -> c
refine c t u strengthens c to permit t >= u
top :: c
Initial constraints for use in REST
union :: c -> c -> c
Computes the union of constraints; used in ExploredTerms as an optimization A safe default implementation is union c1 c2 = c2
notStrongerThan :: c -> c -> m Bool
c1 `notStrongerThan c2 if c1 permits all orderings allowed by c2 A safe default implementation is notStrongerThan _ _ = return false

fuelOC :: Monad m => Int -> OCAlgebra Int a m Source #

fuelOC n is an OCA that permits n rewrite steps

contramap :: forall c a b m. (b -> a) -> OCAlgebra c a m -> OCAlgebra c b m Source #

contramap f oca transforms an OCA of terms of type a terms of type b, by using f to convert terms of b to equivalent ones of a

bimapConstraints :: forall c d a m. (c -> d) -> (d -> c) -> OCAlgebra c a m -> OCAlgebra d a m Source #

bimapConstraints to from oca yields an oca using d to track constraints; to and from should define an isomorphism between c and d