{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Language.REST.OCAlgebra where

data OCAlgebra c a m = OCAlgebra
  {
    OCAlgebra c a m -> c -> m Bool
isSat  :: c -> m Bool
  , OCAlgebra c a m -> c -> a -> a -> c
refine :: c -> a -> a -> c
  , OCAlgebra c a m -> c
top    :: c

  -- For explore optimizations, if not required just make it return 2nd param
  , OCAlgebra c a m -> c -> c -> c
union  :: c -> c -> c
  -- If not required return False
  , OCAlgebra c a m -> c -> c -> m Bool
notStrongerThan :: c -> c -> m Bool
  }

fuelOC :: (Monad m) => Int -> OCAlgebra Int a m
fuelOC :: Int -> OCAlgebra Int a m
fuelOC Int
initFuel = (Int -> m Bool)
-> (Int -> a -> a -> Int)
-> Int
-> (Int -> Int -> Int)
-> (Int -> Int -> m Bool)
-> OCAlgebra Int a m
forall c a (m :: * -> *).
(c -> m Bool)
-> (c -> a -> a -> c)
-> c
-> (c -> c -> c)
-> (c -> c -> m Bool)
-> OCAlgebra c a m
OCAlgebra Int -> m Bool
forall (m :: * -> *) a. (Monad m, Ord a, Num a) => a -> m Bool
isSat' Int -> a -> a -> Int
forall a p p. Num a => a -> p -> p -> a
refine' Int
initFuel Int -> Int -> Int
forall a. Ord a => a -> a -> a
union' Int -> Int -> m Bool
forall (m :: * -> *) a. (Monad m, Ord a) => a -> a -> m Bool
notStrongerThan'
  where
    isSat' :: a -> m Bool
isSat'  a
c             = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0
    refine' :: a -> p -> p -> a
refine' a
c p
_ p
_         = a
c a -> a -> a
forall a. Num a => a -> a -> a
- a
1
    union' :: a -> a -> a
union'  a
c a
c'          = a -> a -> a
forall a. Ord a => a -> a -> a
max a
c a
c'
    notStrongerThan' :: a -> a -> m Bool
notStrongerThan' a
c a
c' = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ a
c a -> a -> Bool
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 :: (b -> a) -> OCAlgebra c a m -> OCAlgebra c b m
contramap b -> a
f OCAlgebra c a m
aoc = OCAlgebra c a m
aoc{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 = OCAlgebra c a m -> c -> a -> a -> c
forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine OCAlgebra c a m
aoc 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 :: (c -> d) -> (d -> c) -> OCAlgebra c a m -> OCAlgebra d a m
bimapConstraints c -> d
to d -> c
from OCAlgebra c a m
aoc = (d -> m Bool)
-> (d -> a -> a -> d)
-> d
-> (d -> d -> d)
-> (d -> d -> m Bool)
-> OCAlgebra d a m
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 (OCAlgebra c a m -> c
forall c a (m :: * -> *). OCAlgebra c a m -> c
top OCAlgebra c a m
aoc)) d -> d -> d
union' d -> d -> m Bool
notStrongerThan'
  where
    isSat' :: d -> m Bool
    isSat' :: d -> m Bool
isSat' d
c = OCAlgebra c a m -> c -> m Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
isSat OCAlgebra c a m
aoc (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 (c -> d) -> c -> d
forall a b. (a -> b) -> a -> b
$ OCAlgebra c a m -> c -> a -> a -> c
forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine OCAlgebra c a m
aoc (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 (c -> d) -> c -> d
forall a b. (a -> b) -> a -> b
$ OCAlgebra c a m -> c -> c -> c
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
union OCAlgebra c a m
aoc (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 = OCAlgebra c a m -> c -> c -> m Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
notStrongerThan OCAlgebra c a m
aoc (d -> c
from d
c1) (d -> c
from d
c2)