{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Language.REST.WQOConstraints.Lazy (
lazyOC
, addConstraint
, intersect
, isSatisfiable
, noConstraints
, singleton
, union
, unsatisfiable
, LazyOC
) where
import Text.Printf
import GHC.Generics (Generic)
import Data.Hashable
import qualified Data.Set as S
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
(LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> Bool) -> Eq (LazyOC a)
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, Eq (LazyOC a)
Eq (LazyOC a)
-> (LazyOC a -> LazyOC a -> Ordering)
-> (LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> LazyOC a)
-> (LazyOC a -> LazyOC a -> LazyOC a)
-> Ord (LazyOC a)
LazyOC a -> LazyOC a -> Bool
LazyOC a -> LazyOC a -> Ordering
LazyOC a -> LazyOC a -> LazyOC a
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
$cp1Ord :: forall a. Ord a => Eq (LazyOC a)
Ord, (forall x. LazyOC a -> Rep (LazyOC a) x)
-> (forall x. Rep (LazyOC a) x -> LazyOC a) -> Generic (LazyOC a)
forall x. Rep (LazyOC a) x -> LazyOC a
forall x. LazyOC a -> Rep (LazyOC a) x
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, Int -> LazyOC a -> Int
LazyOC a -> Int
(Int -> LazyOC a -> Int)
-> (LazyOC a -> Int) -> Hashable (LazyOC a)
forall a. Hashable a => Int -> LazyOC a -> Int
forall a. Hashable a => LazyOC a -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
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 :: LazyOC a -> Maybe (WQO a)
getOrdering (Sat WQO a
wqo Thunk a
_) = WQO a -> Maybe (WQO a)
forall a. a -> Maybe a
Just WQO a
wqo
getOrdering LazyOC a
_ = Maybe (WQO a)
forall a. Maybe a
Nothing
eval :: (Eq a, Ord a, Hashable a) => ADT.ConstraintsADT a -> LazyOC a
eval :: ConstraintsADT a -> LazyOC a
eval (ADT.Sat WQO a
w) = WQO a -> ConstraintsADT a -> LazyOC a
forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
w ConstraintsADT a
forall a. ConstraintsADT a
ADT.Unsat
eval ConstraintsADT a
ADT.Unsat = LazyOC a
forall a. LazyOC a
Unsat
eval (ADT.Union ConstraintsADT a
lhs ConstraintsADT a
rhs) =
case ConstraintsADT a -> LazyOC a
forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
t1 of
Sat WQO a
w ConstraintsADT a
t1' -> WQO a -> ConstraintsADT a -> LazyOC a
forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
w (ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union ConstraintsADT a
t1' ConstraintsADT a
t2)
LazyOC a
Unsat -> ConstraintsADT a -> LazyOC a
forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
t2
where
(ConstraintsADT a
t1, ConstraintsADT a
t2) = (ConstraintsADT a
lhs, ConstraintsADT a
rhs)
eval (ADT.Intersect ConstraintsADT a
t1 ConstraintsADT a
t2) =
case (ConstraintsADT a -> LazyOC a
forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
t1, ConstraintsADT a -> LazyOC a
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 =
(ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect (WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
c1) ConstraintsADT a
t2') ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`ADT.union`
(ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect (WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
c2) ConstraintsADT a
t1') ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`ADT.union`
(ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect ConstraintsADT a
t1' ConstraintsADT a
t2')
in
case WQO a -> WQO a -> Maybe (WQO a)
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' -> WQO a -> ConstraintsADT a -> LazyOC a
forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
c' ConstraintsADT a
rest
Maybe (WQO a)
Nothing -> ConstraintsADT a -> LazyOC a
forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
rest
(LazyOC a, LazyOC a)
_ -> LazyOC a
forall a. LazyOC a
Unsat
toADT :: Eq a => LazyOC a -> ADT.ConstraintsADT a
toADT :: LazyOC a -> ConstraintsADT a
toADT LazyOC a
Unsat = ConstraintsADT a
forall a. ConstraintsADT a
ADT.Unsat
toADT (Sat WQO a
w ConstraintsADT a
r) = ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union (WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
w) ConstraintsADT 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) = String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"%s ∨ lazy(%s)" (WQO a -> String
forall a. Show a => a -> String
show WQO a
s) (Thunk a -> String
forall a. Show a => a -> String
show Thunk a
r)
noConstraints :: LazyOC a
noConstraints :: LazyOC a
noConstraints = WQO a -> Thunk a -> LazyOC a
forall a. WQO a -> Thunk a -> LazyOC a
Sat (WQO a
forall a. WQO a
WQO.empty) Thunk a
forall a. ConstraintsADT a
ADT.Unsat
unsatisfiable :: LazyOC a
unsatisfiable :: LazyOC a
unsatisfiable = LazyOC a
forall a. LazyOC a
Unsat
union :: Eq a => LazyOC a -> LazyOC a -> LazyOC a
union :: 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 WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = LazyOC a
forall a. LazyOC a
noConstraints
union LazyOC a
_ (Sat WQO a
s Thunk a
_) | WQO a
s WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = LazyOC a
forall a. LazyOC a
noConstraints
union (Sat WQO a
s1 Thunk a
r1) (Sat WQO a
s2 Thunk a
r2) = WQO a -> Thunk a -> LazyOC a
forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
s1 (Thunk a -> Thunk a -> Thunk a
forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union (WQO a -> Thunk a
forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
s2) (Thunk a -> Thunk a -> Thunk a
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 :: LazyOC a -> LazyOC a -> LazyOC a
intersect LazyOC a
t1 LazyOC a
t2 = ConstraintsADT a -> LazyOC a
forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval (ConstraintsADT a -> LazyOC a) -> ConstraintsADT a -> LazyOC a
forall a b. (a -> b) -> a -> b
$ ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect (LazyOC a -> ConstraintsADT a
forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
t1) (LazyOC a -> ConstraintsADT a
forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
t2)
isSatisfiable :: LazyOC a -> Bool
isSatisfiable :: LazyOC a -> Bool
isSatisfiable (Sat WQO a
_ Thunk a
_) = Bool
True
isSatisfiable LazyOC a
Unsat = Bool
False
singleton :: WQO a -> LazyOC a
singleton :: WQO a -> LazyOC a
singleton WQO a
c = WQO a -> Thunk a -> LazyOC a
forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
c Thunk a
forall a. ConstraintsADT a
ADT.Unsat
relevantConstraints
:: (Eq a, Ord a, Hashable a) => LazyOC a -> S.Set a -> S.Set a -> LazyOC a
relevantConstraints :: LazyOC a -> Set a -> Set a -> LazyOC a
relevantConstraints LazyOC a
c Set a
_ Set a
_ = LazyOC a
c
notStrongerThan :: (Monad m, Eq a) => LazyOC a -> LazyOC a -> m Bool
notStrongerThan :: LazyOC a -> LazyOC a -> m Bool
notStrongerThan LazyOC a
_ LazyOC a
Unsat = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
notStrongerThan LazyOC a
t1 LazyOC a
t2 = 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
$ LazyOC a
t1 LazyOC a -> LazyOC a -> Bool
forall a. Eq a => a -> a -> Bool
== LazyOC a
t2
addConstraint :: (Ord a, Hashable a) => ADT.WQO a -> LazyOC a -> LazyOC a
addConstraint :: WQO a -> LazyOC a -> LazyOC a
addConstraint WQO a
o LazyOC a
c = ConstraintsADT a -> LazyOC a
forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval (ConstraintsADT a -> LazyOC a) -> ConstraintsADT a -> LazyOC a
forall a b. (a -> b) -> a -> b
$ WQO a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
ADT.addConstraint WQO a
o (LazyOC a -> ConstraintsADT a
forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
c)
permits :: (Ord a, Hashable a) => LazyOC a -> WQO.WQO a -> Bool
permits :: 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 WQO a -> WQO a -> Bool
forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
wqo Bool -> Bool -> Bool
|| LazyOC a -> WQO a -> Bool
forall a. (Ord a, Hashable a) => LazyOC a -> WQO a -> Bool
permits (Thunk a -> LazyOC a
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 :: WQOConstraints LazyOC m
lazyOC = (forall a.
(Eq a, Ord a, Hashable a) =>
WQO a -> LazyOC a -> LazyOC a)
-> (forall a.
(Show a, Eq a, Ord a, Hashable a) =>
LazyOC a -> LazyOC a -> LazyOC a)
-> (forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
LazyOC a -> m Bool)
-> (forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
LazyOC a -> LazyOC a -> m Bool)
-> (forall a. (Eq a, Ord a, Hashable a) => LazyOC a)
-> (forall a.
(Show a, Eq a, Ord a, Hashable a) =>
LazyOC a -> WQO a -> Bool)
-> (forall a.
(Eq a, Ord a, Hashable a) =>
LazyOC a -> Set a -> Set a -> LazyOC a)
-> (forall a.
(Eq a, Ord a, Hashable a) =>
LazyOC a -> LazyOC a -> LazyOC a)
-> (forall a. LazyOC a)
-> (forall a. (Eq a, Ord a, Hashable a) => LazyOC a -> Set a)
-> (forall a. LazyOC a -> Maybe (WQO a))
-> (forall a. (Eq a, Ord a, Hashable a) => LazyOC a -> LazyOC a)
-> WQOConstraints LazyOC m
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 -> Set a -> Set a -> impl a)
-> (forall a.
(Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a)
-> (forall a. impl a)
-> (forall a. (Eq a, Ord a, Hashable a) => impl a -> Set a)
-> (forall a. impl a -> Maybe (WQO a))
-> (forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a)
-> WQOConstraints impl m
OC.OC
forall a.
(Eq a, Ord a, Hashable a) =>
WQO a -> LazyOC a -> LazyOC a
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
forall a.
(Show a, Eq a, Ord a, Hashable a) =>
LazyOC a -> LazyOC a -> LazyOC a
intersect
(Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> (LazyOC a -> Bool) -> LazyOC a -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LazyOC a -> Bool
forall a. LazyOC a -> Bool
isSatisfiable)
forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
LazyOC a -> LazyOC a -> m Bool
forall (m :: * -> *) a.
(Monad m, Eq a) =>
LazyOC a -> LazyOC a -> m Bool
notStrongerThan
forall a. LazyOC a
forall a. (Eq a, Ord a, Hashable a) => LazyOC a
noConstraints
forall a. (Ord a, Hashable a) => LazyOC a -> WQO a -> Bool
forall a.
(Show a, Eq a, Ord a, Hashable a) =>
LazyOC a -> WQO a -> Bool
permits
forall a.
(Eq a, Ord a, Hashable a) =>
LazyOC a -> Set a -> Set a -> LazyOC a
relevantConstraints
forall a.
(Eq a, Ord a, Hashable a) =>
LazyOC a -> LazyOC a -> LazyOC a
forall a. Eq a => LazyOC a -> LazyOC a -> LazyOC a
union
forall a. LazyOC a
unsatisfiable
forall a. (Eq a, Ord a, Hashable a) => LazyOC a -> Set a
forall a. HasCallStack => a
undefined
forall a. LazyOC a -> Maybe (WQO a)
getOrdering
forall a. a -> a
forall a. (Eq a, Ord a, Hashable a) => LazyOC a -> LazyOC a
id