{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Language.REST.WQOConstraints.Lazy (
lazyOC
, addConstraint
, isSatisfiable
, noConstraints
, LazyOC
) where
import Text.Printf
import GHC.Generics (Generic)
import Data.Hashable
import qualified Language.REST.Internal.WQO as WQO
import qualified Language.REST.WQOConstraints as OC
import qualified Language.REST.WQOConstraints.ADT as ADT
type WQO = WQO.WQO
type Thunk a = ADT.ConstraintsADT a
data LazyOC a =
Unsat
| Sat (WQO a) (Thunk a)
deriving (LazyOC a -> LazyOC a -> Bool
forall a. Eq a => LazyOC a -> LazyOC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LazyOC a -> LazyOC a -> Bool
$c/= :: forall a. Eq a => LazyOC a -> LazyOC a -> Bool
== :: LazyOC a -> LazyOC a -> Bool
$c== :: forall a. Eq a => LazyOC a -> LazyOC a -> Bool
Eq, LazyOC a -> LazyOC a -> Bool
LazyOC a -> LazyOC a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (LazyOC a)
forall a. Ord a => LazyOC a -> LazyOC a -> Bool
forall a. Ord a => LazyOC a -> LazyOC a -> Ordering
forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
min :: LazyOC a -> LazyOC a -> LazyOC a
$cmin :: forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
max :: LazyOC a -> LazyOC a -> LazyOC a
$cmax :: forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
>= :: LazyOC a -> LazyOC a -> Bool
$c>= :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
> :: LazyOC a -> LazyOC a -> Bool
$c> :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
<= :: LazyOC a -> LazyOC a -> Bool
$c<= :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
< :: LazyOC a -> LazyOC a -> Bool
$c< :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
compare :: LazyOC a -> LazyOC a -> Ordering
$ccompare :: forall a. Ord a => LazyOC a -> LazyOC a -> Ordering
Ord, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (LazyOC a) x -> LazyOC a
forall a x. LazyOC a -> Rep (LazyOC a) x
$cto :: forall a x. Rep (LazyOC a) x -> LazyOC a
$cfrom :: forall a x. LazyOC a -> Rep (LazyOC a) x
Generic, forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall {a}. Hashable a => Eq (LazyOC a)
forall a. Hashable a => Int -> LazyOC a -> Int
forall a. Hashable a => LazyOC a -> Int
hash :: LazyOC a -> Int
$chash :: forall a. Hashable a => LazyOC a -> Int
hashWithSalt :: Int -> LazyOC a -> Int
$chashWithSalt :: forall a. Hashable a => Int -> LazyOC a -> Int
Hashable)
getOrdering :: LazyOC a -> Maybe (WQO a)
getOrdering :: forall a. LazyOC a -> Maybe (WQO a)
getOrdering (Sat WQO a
wqo Thunk a
_) = forall a. a -> Maybe a
Just WQO a
wqo
getOrdering LazyOC a
_ = forall a. Maybe a
Nothing
eval :: (Eq a, Ord a, Hashable a) => ADT.ConstraintsADT a -> LazyOC a
eval :: forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval (ADT.Sat WQO a
w) = forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
w forall a. ConstraintsADT a
ADT.Unsat
eval ConstraintsADT a
ADT.Unsat = forall a. LazyOC a
Unsat
eval (ADT.Union ConstraintsADT a
lhs ConstraintsADT a
rhs) =
case forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
lhs of
Sat WQO a
w ConstraintsADT a
t1' -> forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
w (forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union ConstraintsADT a
t1' ConstraintsADT a
rhs)
LazyOC a
Unsat -> forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
rhs
eval (ADT.Intersect ConstraintsADT a
t1 ConstraintsADT a
t2) =
case (forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
t1, forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
t2) of
(Sat WQO a
c1 ConstraintsADT a
t1', Sat WQO a
c2 ConstraintsADT a
t2') ->
let
rest :: ConstraintsADT a
rest =
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect (forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
c1) ConstraintsADT a
t2' forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`ADT.union`
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect (forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
c2) ConstraintsADT a
t1' forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`ADT.union`
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect ConstraintsADT a
t1' ConstraintsADT a
t2'
in
case forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
c1 WQO a
c2 of
Just WQO a
c' -> forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
c' ConstraintsADT a
rest
Maybe (WQO a)
Nothing -> forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
rest
(LazyOC a, LazyOC a)
_ -> forall a. LazyOC a
Unsat
toADT :: Eq a => LazyOC a -> ADT.ConstraintsADT a
toADT :: forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
Unsat = forall a. ConstraintsADT a
ADT.Unsat
toADT (Sat WQO a
w Thunk a
r) = forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union (forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
w) Thunk a
r
instance (Show a, Eq a, Ord a, Hashable a) => Show (LazyOC a) where
show :: LazyOC a -> String
show LazyOC a
Unsat = String
"⊥"
show (Sat WQO a
s Thunk a
r) = forall r. PrintfType r => String -> r
printf String
"%s ∨ lazy(%s)" (forall a. Show a => a -> String
show WQO a
s) (forall a. Show a => a -> String
show Thunk a
r)
noConstraints :: LazyOC a
noConstraints :: forall a. LazyOC a
noConstraints = forall a. WQO a -> Thunk a -> LazyOC a
Sat forall a. WQO a
WQO.empty forall a. ConstraintsADT a
ADT.Unsat
unsatisfiable :: LazyOC a
unsatisfiable :: forall a. LazyOC a
unsatisfiable = forall a. LazyOC a
Unsat
union :: Eq a => LazyOC a -> LazyOC a -> LazyOC a
union :: forall a. Eq a => LazyOC a -> LazyOC a -> LazyOC a
union LazyOC a
Unsat LazyOC a
s = LazyOC a
s
union LazyOC a
s LazyOC a
Unsat = LazyOC a
s
union (Sat WQO a
s Thunk a
_) LazyOC a
_ | WQO a
s forall a. Eq a => a -> a -> Bool
== forall a. WQO a
WQO.empty = forall a. LazyOC a
noConstraints
union LazyOC a
_ (Sat WQO a
s Thunk a
_) | WQO a
s forall a. Eq a => a -> a -> Bool
== forall a. WQO a
WQO.empty = forall a. LazyOC a
noConstraints
union (Sat WQO a
s1 Thunk a
r1) (Sat WQO a
s2 Thunk a
r2) = forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
s1 (forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union (forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
s2) (forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union Thunk a
r1 Thunk a
r2))
intersect :: (Ord a, Hashable a) => LazyOC a -> LazyOC a -> LazyOC a
intersect :: forall a. (Ord a, Hashable a) => LazyOC a -> LazyOC a -> LazyOC a
intersect LazyOC a
t1 LazyOC a
t2 = forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval forall a b. (a -> b) -> a -> b
$ forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect (forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
t1) (forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
t2)
isSatisfiable :: LazyOC a -> Bool
isSatisfiable :: forall a. LazyOC a -> Bool
isSatisfiable (Sat WQO a
_ Thunk a
_) = Bool
True
isSatisfiable LazyOC a
Unsat = Bool
False
notStrongerThan :: (Monad m, Eq a) => LazyOC a -> LazyOC a -> m Bool
notStrongerThan :: forall (m :: * -> *) a.
(Monad m, Eq a) =>
LazyOC a -> LazyOC a -> m Bool
notStrongerThan LazyOC a
_ LazyOC a
Unsat = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
notStrongerThan LazyOC a
t1 LazyOC a
t2 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LazyOC a
t1 forall a. Eq a => a -> a -> Bool
== LazyOC a
t2
addConstraint :: (Ord a, Hashable a) => WQO a -> LazyOC a -> LazyOC a
addConstraint :: forall a. (Ord a, Hashable a) => WQO a -> LazyOC a -> LazyOC a
addConstraint WQO a
o LazyOC a
c = forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
ADT.addConstraint WQO a
o (forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
c)
permits :: (Ord a, Hashable a) => LazyOC a -> WQO.WQO a -> Bool
permits :: forall a. (Ord a, Hashable a) => LazyOC a -> WQO a -> Bool
permits LazyOC a
Unsat WQO a
_ = Bool
False
permits (Sat WQO a
s1 Thunk a
thunk) WQO a
wqo = WQO a
s1 forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
wqo Bool -> Bool -> Bool
|| forall a. (Ord a, Hashable a) => LazyOC a -> WQO a -> Bool
permits (forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval Thunk a
thunk) WQO a
wqo
lazyOC :: Monad m => OC.WQOConstraints LazyOC m
lazyOC :: forall (m :: * -> *). Monad m => WQOConstraints LazyOC m
lazyOC = forall (impl :: * -> *) (m :: * -> *).
(forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a)
-> (forall a.
(Show a, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a)
-> (forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
impl a -> m Bool)
-> (forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> m Bool)
-> (forall a. (Eq a, Ord a, Hashable a) => impl a)
-> (forall a.
(Show a, Eq a, Ord a, Hashable a) =>
impl a -> WQO a -> Bool)
-> (forall a.
(Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a)
-> (forall a. impl a)
-> (forall a. impl a -> Maybe (WQO a))
-> WQOConstraints impl m
OC.OC
forall a. (Ord a, Hashable a) => WQO a -> LazyOC a -> LazyOC a
addConstraint
forall a. (Ord a, Hashable a) => LazyOC a -> LazyOC a -> LazyOC a
intersect
(forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LazyOC a -> Bool
isSatisfiable)
forall (m :: * -> *) a.
(Monad m, Eq a) =>
LazyOC a -> LazyOC a -> m Bool
notStrongerThan
forall a. LazyOC a
noConstraints
forall a. (Ord a, Hashable a) => LazyOC a -> WQO a -> Bool
permits
forall a. Eq a => LazyOC a -> LazyOC a -> LazyOC a
union
forall a. LazyOC a
unsatisfiable
forall a. LazyOC a -> Maybe (WQO a)
getOrdering