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

-- | 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@.
data OCAlgebra c a m = OCAlgebra
  { forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
isSat  :: c -> m Bool       -- ^ Checks if the constraints are satisfiable
  , forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine :: c -> a -> a -> c  -- ^ @refine c t u@ strengthens @c@ to permit @t >= u@
  , forall c a (m :: * -> *). OCAlgebra c a m -> c
top    :: c                 -- ^ Initial constraints for use in REST

  , forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
union  :: c -> c -> c       -- ^ Computes the union of constraints; used in 'ExploredTerms' as an optimization
                                --   A safe default implementation is @union c1 c2 = c2@

  , forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
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 n@ is an OCA that permits @n@ rewrite steps
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 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@
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 to from oca@ yields an oca using @d@ to track constraints; @to@ and @from@ should
--   define an isomorphism between c and d
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)