{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Language.REST.OCToAbstract where

import Data.Hashable

import Control.Monad.Identity

import Language.REST.OCAlgebra
import qualified Language.REST.WQOConstraints as OC
import Language.REST.Types
import Language.REST.SMT (ToSMTVar)

-- | @lift@ takes a representation of constraints on a WQO over @base@,
--   alongside a function used to generate constraints to permit a relation on terms @lifted@,
--   and returns the corresponding Ordering Constraints Algebra
lift :: forall impl base lifted m . (ToSMTVar base Int, Ord base, Eq base, Hashable base, Show lifted, Show base, Show (impl base)) =>
     OC.WQOConstraints impl m
  -> OC.ConstraintGen impl base lifted Identity
  -> OCAlgebra (impl base) lifted m
lift :: WQOConstraints impl m
-> ConstraintGen impl base lifted Identity
-> OCAlgebra (impl base) lifted m
lift WQOConstraints impl m
oc ConstraintGen impl base lifted Identity
cgen =
  OCAlgebra :: forall c a (m :: * -> *).
(c -> m Bool)
-> (c -> a -> a -> c)
-> c
-> (c -> c -> c)
-> (c -> c -> m Bool)
-> OCAlgebra c a m
OCAlgebra {
    isSat :: impl base -> m Bool
isSat  = impl base -> m Bool
isSat'
  , top :: impl base
top    = impl base
top'
  , refine :: impl base -> lifted -> lifted -> impl base
refine = impl base -> lifted -> lifted -> impl base
refine'
  , union :: impl base -> impl base -> impl base
union  = WQOConstraints impl m
-> forall a.
   (Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> impl a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
   (Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> impl a
OC.union WQOConstraints impl m
oc
  , notStrongerThan :: impl base -> impl base -> m Bool
notStrongerThan = WQOConstraints impl m
-> forall a.
   (ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> m Bool
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
   (ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> m Bool
OC.notStrongerThan WQOConstraints impl m
oc
  }
  where
    isSat' :: impl base -> m Bool
    isSat' :: impl base -> m Bool
isSat' impl base
aoc = WQOConstraints impl m -> impl base -> m Bool
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
   (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
   impl a -> m Bool
OC.isSatisfiable WQOConstraints impl m
oc impl base
aoc

    top' :: impl base
    top' :: impl base
top' = WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a
OC.noConstraints WQOConstraints impl m
oc

    refine' :: impl base -> lifted -> lifted -> impl base
    refine' :: impl base -> lifted -> lifted -> impl base
refine' impl base
c lifted
t lifted
u =
      let
        pair :: impl base
pair   = Identity (impl base) -> impl base
forall a. Identity a -> a
runIdentity (Identity (impl base) -> impl base)
-> Identity (impl base) -> impl base
forall a b. (a -> b) -> a -> b
$ WQOConstraints impl m
-> Relation
-> impl base
-> lifted
-> lifted
-> Identity (impl base)
ConstraintGen impl base lifted Identity
cgen WQOConstraints impl m
oc Relation
GTE impl base
top' lifted
t lifted
u
        result :: impl base
result = WQOConstraints impl m -> impl base -> impl base -> impl base
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
   (Show a, Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> impl a
OC.intersect WQOConstraints impl m
oc impl base
c impl base
pair
      in
        impl base
result