{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Language.REST.OCAlgebra where
data OCAlgebra c a m = OCAlgebra
{ forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
isSat :: c -> m Bool
, forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine :: c -> a -> a -> c
, forall c a (m :: * -> *). OCAlgebra c a m -> c
top :: c
, forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
union :: c -> c -> c
, forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
notStrongerThan :: c -> c -> m Bool
}
fuelOC :: (Monad m) => Int -> OCAlgebra Int a m
fuelOC :: forall (m :: * -> *) a. Monad m => Int -> OCAlgebra Int a m
fuelOC Int
initFuel = forall c a (m :: * -> *).
(c -> m Bool)
-> (c -> a -> a -> c)
-> c
-> (c -> c -> c)
-> (c -> c -> m Bool)
-> OCAlgebra c a m
OCAlgebra forall {m :: * -> *} {a}. (Monad m, Ord a, Num a) => a -> m Bool
isSat' forall {a} {p} {p}. Num a => a -> p -> p -> a
refine' Int
initFuel Int -> Int -> Int
union' forall {m :: * -> *} {a}. (Monad m, Ord a) => a -> a -> m Bool
notStrongerThan'
where
isSat' :: a -> m Bool
isSat' a
c = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a
c forall a. Ord a => a -> a -> Bool
>= a
0
refine' :: a -> p -> p -> a
refine' a
c p
_ p
_ = a
c forall a. Num a => a -> a -> a
- a
1
union' :: Int -> Int -> Int
union' = forall a. Ord a => a -> a -> a
max
notStrongerThan' :: a -> a -> m Bool
notStrongerThan' a
c a
c' = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a
c forall a. Ord a => a -> a -> Bool
>= a
c'
contramap :: forall c a b m .
(b -> a)
-> OCAlgebra c a m
-> OCAlgebra c b m
contramap :: forall c a b (m :: * -> *).
(b -> a) -> OCAlgebra c a m -> OCAlgebra c b m
contramap b -> a
f OCAlgebra c a m
oca = OCAlgebra c a m
oca{refine :: c -> b -> b -> c
refine = c -> b -> b -> c
refine'}
where
refine' :: c -> b -> b -> c
refine' :: c -> b -> b -> c
refine' c
c b
t1 b
t2 = forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine OCAlgebra c a m
oca c
c (b -> a
f b
t1) (b -> a
f b
t2)
bimapConstraints :: forall c d a m .
(c -> d)
-> (d -> c)
-> OCAlgebra c a m
-> OCAlgebra d a m
bimapConstraints :: forall c d a (m :: * -> *).
(c -> d) -> (d -> c) -> OCAlgebra c a m -> OCAlgebra d a m
bimapConstraints c -> d
to d -> c
from OCAlgebra c a m
oca = forall c a (m :: * -> *).
(c -> m Bool)
-> (c -> a -> a -> c)
-> c
-> (c -> c -> c)
-> (c -> c -> m Bool)
-> OCAlgebra c a m
OCAlgebra d -> m Bool
isSat' d -> a -> a -> d
refine' (c -> d
to (forall c a (m :: * -> *). OCAlgebra c a m -> c
top OCAlgebra c a m
oca)) d -> d -> d
union' d -> d -> m Bool
notStrongerThan'
where
isSat' :: d -> m Bool
isSat' :: d -> m Bool
isSat' d
c = forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
isSat OCAlgebra c a m
oca (d -> c
from d
c)
refine' :: d -> a -> a -> d
refine' :: d -> a -> a -> d
refine' d
c a
t1 a
t2 = c -> d
to forall a b. (a -> b) -> a -> b
$ forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine OCAlgebra c a m
oca (d -> c
from d
c) a
t1 a
t2
union' :: d -> d -> d
union' :: d -> d -> d
union' d
c1 d
c2 = c -> d
to forall a b. (a -> b) -> a -> b
$ forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
union OCAlgebra c a m
oca (d -> c
from d
c1) (d -> c
from d
c2)
notStrongerThan' :: d -> d -> m Bool
notStrongerThan' :: d -> d -> m Bool
notStrongerThan' d
c1 d
c2 = forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
notStrongerThan OCAlgebra c a m
oca (d -> c
from d
c1) (d -> c
from d
c2)