{-# LANGUAGE FlexibleContexts #-}
{-# 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 :: 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 :: forall (impl :: * -> *) base lifted (m :: * -> *).
(ToSMTVar base Int, Ord base, Eq base, Hashable base, Show lifted,
Show base, Show (impl base)) =>
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 {
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 = 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 = 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' = 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
top' :: impl base
top' :: impl base
top' = 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 = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ ConstraintGen impl base lifted Identity
cgen WQOConstraints impl m
oc Relation
GTE impl base
top' lifted
t lifted
u
result :: impl base
result = 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