{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE CPP #-}
#define OPTIMIZE_WQO
module Language.REST.WQOConstraints.ADT
( ConstraintsADT(..)
, addConstraint
, adtOC
, intersect
, union
)
where
import GHC.Generics (Generic)
import Data.Hashable
import Control.Monad.State.Lazy
import qualified Data.Set as S
import qualified Data.Maybe as Mb
import qualified Data.Map.Strict as M
import qualified Language.REST.Internal.WQO as WQO
import qualified Language.REST.WQOConstraints as OC
import Language.REST.SMT
import Language.REST.Op
import System.IO (Handle)
import Text.Printf
type WQO = WQO.WQO
data ConstraintsADT a =
Sat (WQO a)
| Unsat
| Union (ConstraintsADT a) (ConstraintsADT a)
| Intersect (ConstraintsADT a) (ConstraintsADT a)
deriving (ConstraintsADT a -> ConstraintsADT a -> Bool
(ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> Eq (ConstraintsADT a)
forall a. Eq a => ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => ConstraintsADT a -> ConstraintsADT a -> Bool
== :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c/= :: forall a. Eq a => ConstraintsADT a -> ConstraintsADT a -> Bool
/= :: ConstraintsADT a -> ConstraintsADT a -> Bool
Eq, Eq (ConstraintsADT a)
Eq (ConstraintsADT a) =>
(ConstraintsADT a -> ConstraintsADT a -> Ordering)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a)
-> (ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a)
-> Ord (ConstraintsADT a)
ConstraintsADT a -> ConstraintsADT a -> Bool
ConstraintsADT a -> ConstraintsADT a -> Ordering
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT 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 (ConstraintsADT a)
forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Ordering
forall a.
Ord a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
$ccompare :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Ordering
compare :: ConstraintsADT a -> ConstraintsADT a -> Ordering
$c< :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
< :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c<= :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
<= :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c> :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
> :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c>= :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
>= :: ConstraintsADT a -> ConstraintsADT a -> Bool
$cmax :: forall a.
Ord a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
max :: ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
$cmin :: forall a.
Ord a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
min :: ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
Ord, (forall x. ConstraintsADT a -> Rep (ConstraintsADT a) x)
-> (forall x. Rep (ConstraintsADT a) x -> ConstraintsADT a)
-> Generic (ConstraintsADT a)
forall x. Rep (ConstraintsADT a) x -> ConstraintsADT a
forall x. ConstraintsADT a -> Rep (ConstraintsADT a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (ConstraintsADT a) x -> ConstraintsADT a
forall a x. ConstraintsADT a -> Rep (ConstraintsADT a) x
$cfrom :: forall a x. ConstraintsADT a -> Rep (ConstraintsADT a) x
from :: forall x. ConstraintsADT a -> Rep (ConstraintsADT a) x
$cto :: forall a x. Rep (ConstraintsADT a) x -> ConstraintsADT a
to :: forall x. Rep (ConstraintsADT a) x -> ConstraintsADT a
Generic, Eq (ConstraintsADT a)
Eq (ConstraintsADT a) =>
(Int -> ConstraintsADT a -> Int)
-> (ConstraintsADT a -> Int) -> Hashable (ConstraintsADT a)
Int -> ConstraintsADT a -> Int
ConstraintsADT a -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall a. Hashable a => Eq (ConstraintsADT a)
forall a. Hashable a => Int -> ConstraintsADT a -> Int
forall a. Hashable a => ConstraintsADT a -> Int
$chashWithSalt :: forall a. Hashable a => Int -> ConstraintsADT a -> Int
hashWithSalt :: Int -> ConstraintsADT a -> Int
$chash :: forall a. Hashable a => ConstraintsADT a -> Int
hash :: ConstraintsADT a -> Int
Hashable)
instance {-# OVERLAPPING #-} (ToSMTVar a Int) => ToSMT (ConstraintsADT a) Bool where
toSMT :: ConstraintsADT a -> SMTExpr Bool
toSMT (Sat WQO a
w) = WQO a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT WQO a
w
toSMT ConstraintsADT a
Unsat = SMTExpr Bool
smtFalse
toSMT (Union ConstraintsADT a
w1 ConstraintsADT a
w2) = [SMTExpr Bool] -> SMTExpr Bool
Or [ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w1, ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w2]
toSMT (Intersect ConstraintsADT a
w1 ConstraintsADT a
w2) = [SMTExpr Bool] -> SMTExpr Bool
And [ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w1, ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w2]
{-# SPECIALIZE cost :: ConstraintsADT Op -> Int #-}
cost :: (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost :: forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost (Union ConstraintsADT a
lhs ConstraintsADT a
rhs) = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs) (ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs)
cost (Intersect ConstraintsADT a
lhs ConstraintsADT a
rhs) = ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs
cost (Sat WQO a
wqo) = Set a -> Int
forall a. Set a -> Int
S.size (Set a -> Int) -> Set a -> Int
forall a b. (a -> b) -> a -> b
$ WQO a -> Set a
forall a. Ord a => WQO a -> Set a
WQO.elems WQO a
wqo
cost ConstraintsADT a
Unsat = Int
100
intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
#ifdef OPTIMIZE_WQO
intersect :: forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect (Sat WQO a
t) (Sat WQO a
u) =
ConstraintsADT a
-> (WQO a -> ConstraintsADT a) -> Maybe (WQO a) -> ConstraintsADT a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ConstraintsADT a
forall a. ConstraintsADT a
Unsat WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat (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
t WQO a
u)
#endif
intersect (Sat WQO a
w) ConstraintsADT a
v | WQO a
w WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = ConstraintsADT a
v
intersect ConstraintsADT a
v (Sat WQO a
w) | WQO a
w WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = ConstraintsADT a
v
intersect ConstraintsADT a
_ ConstraintsADT a
Unsat = ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect ConstraintsADT a
Unsat ConstraintsADT a
_ = ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect ConstraintsADT a
t1 ConstraintsADT a
t2 | ConstraintsADT a
t1 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
t2 = ConstraintsADT a
t1
intersect ConstraintsADT a
t1 (Union ConstraintsADT a
t2 ConstraintsADT a
t3) | ConstraintsADT a
t1 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
t2 Bool -> Bool -> Bool
|| ConstraintsADT a
t1 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
t3 = ConstraintsADT a
t1
#ifdef OPTIMIZE_WQO
intersect (Sat WQO a
w1) (Intersect (Sat WQO a
w2) ConstraintsADT a
t2) =
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
w1 WQO a
w2 of
Just WQO a
w' -> WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w' ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`intersect` ConstraintsADT a
t2
Maybe (WQO a)
Nothing -> ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect (Sat WQO a
w1) (Intersect ConstraintsADT a
t2 (Sat WQO a
w2)) =
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
w1 WQO a
w2 of
Just WQO a
w' -> WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w' ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`intersect` ConstraintsADT a
t2
Maybe (WQO a)
Nothing -> ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect (Intersect ConstraintsADT a
t1 (Sat WQO a
w1)) (Sat WQO a
w2) =
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
w1 WQO a
w2 of
Just WQO a
w' -> ConstraintsADT a
t1 ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`intersect` WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w'
Maybe (WQO a)
Nothing -> ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect (Intersect (Sat WQO a
w1) ConstraintsADT a
t1) (Sat WQO a
w2) =
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
w1 WQO a
w2 of
Just WQO a
w' -> ConstraintsADT a
t1 ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`intersect` WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w'
Maybe (WQO a)
Nothing -> ConstraintsADT a
forall a. ConstraintsADT a
Unsat
#endif
intersect ConstraintsADT a
t1 ConstraintsADT a
t2 = ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a. ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
Intersect ConstraintsADT a
t1 ConstraintsADT a
t2
union :: Eq a => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union :: forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union (Sat WQO a
w) ConstraintsADT a
_ | WQO a
w WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w
union ConstraintsADT a
_ (Sat WQO a
w) | WQO a
w WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w
union (Intersect ConstraintsADT a
a ConstraintsADT a
b) ConstraintsADT a
c | ConstraintsADT a
a ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c Bool -> Bool -> Bool
|| ConstraintsADT a
b ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c = ConstraintsADT a
c
union ConstraintsADT a
a (Intersect ConstraintsADT a
b ConstraintsADT a
c) | ConstraintsADT a
a ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
b Bool -> Bool -> Bool
|| ConstraintsADT a
a ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c = ConstraintsADT a
a
union ConstraintsADT a
a (Union ConstraintsADT a
b ConstraintsADT a
c) | ConstraintsADT a
a ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
b = ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union ConstraintsADT a
a ConstraintsADT a
c
union ConstraintsADT a
Unsat ConstraintsADT a
s = ConstraintsADT a
s
union ConstraintsADT a
s ConstraintsADT a
Unsat = ConstraintsADT a
s
union ConstraintsADT a
c1 ConstraintsADT a
c2 | ConstraintsADT a
c1 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c2 = ConstraintsADT a
c1
union ConstraintsADT a
c1 ConstraintsADT a
c2 = ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a. ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
Union ConstraintsADT a
c1 ConstraintsADT a
c2
addConstraint
:: (Ord a, Hashable a) => WQO a -> ConstraintsADT a -> ConstraintsADT a
addConstraint :: forall a.
(Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
addConstraint WQO a
o = ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect (WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
o)
notStrongerThan
:: (Eq a, ToSMTVar a Int)
=> ConstraintsADT a
-> ConstraintsADT a
-> SMTExpr Bool
notStrongerThan :: forall a.
(Eq a, ToSMTVar a Int) =>
ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool
notStrongerThan ConstraintsADT a
t1 ConstraintsADT a
t2 | ConstraintsADT a
t1 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
t2 = SMTExpr Bool
smtTrue
notStrongerThan ConstraintsADT a
t1 ConstraintsADT a
_ | ConstraintsADT a
t1 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
forall a. ConstraintsADT a
noConstraints = SMTExpr Bool
smtTrue
notStrongerThan ConstraintsADT a
t1 ConstraintsADT a
t2 = SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool
Implies (ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
t2) (ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
t1)
noConstraints :: ConstraintsADT a
noConstraints :: forall a. ConstraintsADT a
noConstraints = WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
forall a. WQO a
WQO.empty
unsatisfiable :: ConstraintsADT a
unsatisfiable :: forall a. ConstraintsADT a
unsatisfiable = ConstraintsADT a
forall a. ConstraintsADT a
Unsat
{-# SPECIALIZE getConstraints :: ConstraintsADT Op -> [WQO Op] #-}
getConstraints :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> [WQO a]
getConstraints :: forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> [WQO a]
getConstraints ConstraintsADT a
adt =
State (GCState a) [WQO a] -> GCState a -> [WQO a]
forall s a. State s a -> s -> a
evalState (ConstraintsADT a -> State (GCState a) [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
adt) (Map (ConstraintsADT a) [WQO a]
-> Map (WQO a, WQO a) (Maybe (WQO a)) -> GCState a
forall a.
Map (ConstraintsADT a) (GCResult a)
-> Map (WQO a, WQO a) (Maybe (WQO a)) -> GCState a
GCState Map (ConstraintsADT a) [WQO a]
forall k a. Map k a
M.empty Map (WQO a, WQO a) (Maybe (WQO a))
forall k a. Map k a
M.empty)
data GCState a = GCState {
forall a. GCState a -> Map (ConstraintsADT a) (GCResult a)
cs :: M.Map (ConstraintsADT a) (GCResult a)
, forall a. GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
ms :: M.Map (WQO a, WQO a) (Maybe (WQO a))
}
type GCResult a = [WQO a]
type GCMonad a = State (GCState a) (GCResult a)
cached :: (Ord a) => ConstraintsADT a -> GCMonad a -> GCMonad a
cached :: forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
key GCMonad a
thunk = do
Map (ConstraintsADT a) (GCResult a)
cache <- (GCState a -> Map (ConstraintsADT a) (GCResult a))
-> StateT
(GCState a) Identity (Map (ConstraintsADT a) (GCResult a))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets GCState a -> Map (ConstraintsADT a) (GCResult a)
forall a. GCState a -> Map (ConstraintsADT a) (GCResult a)
cs
case ConstraintsADT a
-> Map (ConstraintsADT a) (GCResult a) -> Maybe (GCResult a)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ConstraintsADT a
key Map (ConstraintsADT a) (GCResult a)
cache of
Just GCResult a
result -> String -> GCMonad a -> GCMonad a
forall {p} {p}. p -> p -> p
trace'' String
"ADT Cache hit" (GCMonad a -> GCMonad a) -> GCMonad a -> GCMonad a
forall a b. (a -> b) -> a -> b
$ GCResult a -> GCMonad a
forall a. a -> StateT (GCState a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return GCResult a
result
Maybe (GCResult a)
Nothing -> String -> GCMonad a -> GCMonad a
forall {p} {p}. p -> p -> p
trace'' String
"ADT Cache miss" (GCMonad a -> GCMonad a) -> GCMonad a -> GCMonad a
forall a b. (a -> b) -> a -> b
$ do
GCResult a
result <- String -> GCMonad a -> GCMonad a
forall {p} {p}. p -> p -> p
trace'' String
"Do thunk" GCMonad a
thunk
String
-> StateT (GCState a) Identity () -> StateT (GCState a) Identity ()
forall {p} {p}. p -> p -> p
trace'' String
"Done" (StateT (GCState a) Identity () -> StateT (GCState a) Identity ())
-> StateT (GCState a) Identity () -> StateT (GCState a) Identity ()
forall a b. (a -> b) -> a -> b
$ (GCState a -> GCState a) -> StateT (GCState a) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\GCState a
st -> GCState a
st{cs = M.insert key result (cs st)})
GCResult a -> GCMonad a
forall a. a -> StateT (GCState a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return GCResult a
result
where
trace'' :: p -> p -> p
trace'' p
_ p
x = p
x
cached' :: (Hashable a, Show a, Ord a) => (WQO a, WQO a) -> Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
cached' :: forall a.
(Hashable a, Show a, Ord a) =>
(WQO a, WQO a)
-> Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
cached' (WQO a
lhs, WQO a
rhs) Maybe (WQO a)
thunk = do
Map (WQO a, WQO a) (Maybe (WQO a))
cache <- (GCState a -> Map (WQO a, WQO a) (Maybe (WQO a)))
-> StateT (GCState a) Identity (Map (WQO a, WQO a) (Maybe (WQO a)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
forall a. GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
ms
case (WQO a, WQO a)
-> Map (WQO a, WQO a) (Maybe (WQO a)) -> Maybe (Maybe (WQO a))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (WQO a
lhs, WQO a
rhs) Map (WQO a, WQO a) (Maybe (WQO a))
cache of
Just Maybe (WQO a)
result -> String
-> State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a))
forall {p} {p}. p -> p -> p
trace'' String
"WQO Cache hit" (State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a)))
-> State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a))
forall a b. (a -> b) -> a -> b
$ Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
forall a. a -> StateT (GCState a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (WQO a)
result
Maybe (Maybe (WQO a))
Nothing -> String
-> State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a))
forall {p} {p}. p -> p -> p
trace'' (String
"WQO Cache miss" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (WQO a, WQO a) -> String
forall a. Show a => a -> String
show (WQO a
lhs, WQO a
rhs)) (State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a)))
-> State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a))
forall a b. (a -> b) -> a -> b
$ do
String
-> StateT (GCState a) Identity () -> StateT (GCState a) Identity ()
forall {p} {p}. p -> p -> p
trace'' String
"Done" (StateT (GCState a) Identity () -> StateT (GCState a) Identity ())
-> StateT (GCState a) Identity () -> StateT (GCState a) Identity ()
forall a b. (a -> b) -> a -> b
$ (GCState a -> GCState a) -> StateT (GCState a) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\GCState a
st -> GCState a
st{ms = M.insert (rhs, lhs) thunk $ M.insert (lhs, rhs) thunk (ms st)})
Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
forall a. a -> StateT (GCState a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (WQO a)
thunk
where
trace'' :: p -> p -> p
trace'' p
_ p
x = p
x
getConstraints' :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' :: forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' (Sat WQO a
w) = [WQO a] -> StateT (GCState a) Identity [WQO a]
forall a. a -> StateT (GCState a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [WQO a
w]
getConstraints' ConstraintsADT a
Unsat = [WQO a] -> StateT (GCState a) Identity [WQO a]
forall a. a -> StateT (GCState a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
getConstraints' c :: ConstraintsADT a
c@(Union ConstraintsADT a
lhs ConstraintsADT a
rhs) =
ConstraintsADT a
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c (StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a])
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a b. (a -> b) -> a -> b
$ do
[WQO a]
c1' <- ConstraintsADT a
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c1 (StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a])
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a b. (a -> b) -> a -> b
$ ConstraintsADT a -> StateT (GCState a) Identity [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c1
[WQO a]
c2' <- ConstraintsADT a
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c2 (StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a])
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a b. (a -> b) -> a -> b
$ ConstraintsADT a -> StateT (GCState a) Identity [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c2
[WQO a] -> StateT (GCState a) Identity [WQO a]
forall a. a -> StateT (GCState a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([WQO a] -> StateT (GCState a) Identity [WQO a])
-> [WQO a] -> StateT (GCState a) Identity [WQO a]
forall a b. (a -> b) -> a -> b
$ [WQO a]
c1' [WQO a] -> [WQO a] -> [WQO a]
forall a. [a] -> [a] -> [a]
++ [WQO a]
c2'
where
(ConstraintsADT a
c1, ConstraintsADT a
c2) =
if ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs
then (ConstraintsADT a
lhs, ConstraintsADT a
rhs)
else (ConstraintsADT a
rhs, ConstraintsADT a
lhs)
getConstraints' c :: ConstraintsADT a
c@(Intersect ConstraintsADT a
lhs ConstraintsADT a
rhs) = ConstraintsADT a
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c (StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a])
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a b. (a -> b) -> a -> b
$ do
[WQO a]
c1' <- ConstraintsADT a
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c1 (StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a])
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a b. (a -> b) -> a -> b
$ ConstraintsADT a -> StateT (GCState a) Identity [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c1
if [WQO a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [WQO a]
c1'
then [WQO a] -> StateT (GCState a) Identity [WQO a]
forall a. a -> StateT (GCState a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
else ConstraintsADT a
-> StateT (GCState a) Identity [WQO a]
-> StateT (GCState a) Identity [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c2 (ConstraintsADT a -> StateT (GCState a) Identity [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c2) StateT (GCState a) Identity [WQO a]
-> ([WQO a] -> StateT (GCState a) Identity [WQO a])
-> StateT (GCState a) Identity [WQO a]
forall a b.
StateT (GCState a) Identity a
-> (a -> StateT (GCState a) Identity b)
-> StateT (GCState a) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [WQO a] -> [WQO a] -> StateT (GCState a) Identity [WQO a]
go [WQO a]
c1'
where
go :: [WQO a] -> [WQO a] -> State (GCState a) [WQO a]
go :: [WQO a] -> [WQO a] -> StateT (GCState a) Identity [WQO a]
go [WQO a]
c1' [WQO a]
c2' = [Maybe (WQO a)] -> [WQO a]
forall {a}. [Maybe a] -> [a]
flatten ([Maybe (WQO a)] -> [WQO a])
-> StateT (GCState a) Identity [Maybe (WQO a)]
-> StateT (GCState a) Identity [WQO a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
[StateT (GCState a) Identity (Maybe (WQO a))]
-> StateT (GCState a) Identity [Maybe (WQO a)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence (do
WQO a
wqo1 <- [WQO a]
c1'
WQO a
wqo2 <- [WQO a]
c2'
StateT (GCState a) Identity (Maybe (WQO a))
-> [StateT (GCState a) Identity (Maybe (WQO a))]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ((WQO a, WQO a)
-> Maybe (WQO a) -> StateT (GCState a) Identity (Maybe (WQO a))
forall a.
(Hashable a, Show a, Ord a) =>
(WQO a, WQO a)
-> Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
cached' (WQO a
wqo1, WQO a
wqo2) (Maybe (WQO a) -> StateT (GCState a) Identity (Maybe (WQO a)))
-> Maybe (WQO a) -> StateT (GCState a) Identity (Maybe (WQO a))
forall a b. (a -> b) -> a -> b
$ 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
wqo1 WQO a
wqo2))
flatten :: [Maybe a] -> [a]
flatten = [Maybe a] -> [a]
forall {a}. [Maybe a] -> [a]
Mb.catMaybes
(ConstraintsADT a
c1, ConstraintsADT a
c2) =
if ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs
then (ConstraintsADT a
lhs, ConstraintsADT a
rhs)
else (ConstraintsADT a
rhs, ConstraintsADT a
lhs)
permits
:: (Ord a, Hashable a, Show a)
=> ConstraintsADT a
-> WQO.WQO a
-> Bool
permits :: forall a.
(Ord a, Hashable a, Show a) =>
ConstraintsADT a -> WQO a -> Bool
permits ConstraintsADT a
adt WQO a
wqo = (WQO a -> Bool) -> [WQO a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (WQO a -> WQO a -> Bool
forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
wqo) (ConstraintsADT a -> [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> [WQO a]
getConstraints ConstraintsADT a
adt)
isSatisfiable :: (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => ConstraintsADT a -> SMTExpr Bool
isSatisfiable :: forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> SMTExpr Bool
isSatisfiable = ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT
instance (Eq a, Hashable a, Show a) => Show (ConstraintsADT a) where
show :: ConstraintsADT a -> String
show (Sat WQO a
w) = WQO a -> String
forall a. Show a => a -> String
show WQO a
w
show ConstraintsADT a
Unsat = String
"⊥"
show (Union ConstraintsADT a
w ConstraintsADT a
t ) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"(%s ∨\n %s)" (ConstraintsADT a -> String
forall a. Show a => a -> String
show ConstraintsADT a
w) (ConstraintsADT a -> String
forall a. Show a => a -> String
show ConstraintsADT a
t)
show (Intersect ConstraintsADT a
w ConstraintsADT a
t) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"(%s ∧ %s)" (ConstraintsADT a -> String
forall a. Show a => a -> String
show ConstraintsADT a
w) (ConstraintsADT a -> String
forall a. Show a => a -> String
show ConstraintsADT a
t)
adtOC :: (Handle, Handle) -> OC.WQOConstraints ConstraintsADT IO
adtOC :: (Handle, Handle) -> WQOConstraints ConstraintsADT IO
adtOC (Handle, Handle)
z3 = (SMTExpr Bool -> IO Bool)
-> WQOConstraints ConstraintsADT SMTExpr
-> WQOConstraints ConstraintsADT IO
forall (m :: * -> *) (m' :: * -> *) (impl :: * -> *).
(m Bool -> m' Bool)
-> WQOConstraints impl m -> WQOConstraints impl m'
OC.liftC ((Handle, Handle) -> SMTExpr Bool -> IO Bool
checkSat' (Handle, Handle)
z3) WQOConstraints ConstraintsADT SMTExpr
adtOC'
adtOC' :: OC.WQOConstraints ConstraintsADT SMTExpr
adtOC' :: WQOConstraints ConstraintsADT SMTExpr
adtOC' = (forall a.
(Eq a, Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a)
-> (forall a.
(Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a)
-> (forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> SMTExpr Bool)
-> (forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool)
-> (forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a)
-> (forall a.
(Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> WQO a -> Bool)
-> (forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a)
-> (forall a. ConstraintsADT a)
-> (forall a. ConstraintsADT a -> Maybe (WQO a))
-> WQOConstraints ConstraintsADT SMTExpr
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
WQO a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
addConstraint
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect
ConstraintsADT a -> SMTExpr Bool
forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> SMTExpr Bool
isSatisfiable
ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool
forall a.
(Eq a, ToSMTVar a Int) =>
ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool
forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool
notStrongerThan
ConstraintsADT a
forall a. ConstraintsADT a
forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a
noConstraints
ConstraintsADT a -> WQO a -> Bool
forall a.
(Ord a, Hashable a, Show a) =>
ConstraintsADT a -> WQO a -> Bool
forall a.
(Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> WQO a -> Bool
permits
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union
ConstraintsADT a
forall a. ConstraintsADT a
unsatisfiable
ConstraintsADT a -> Maybe (WQO a)
forall a. ConstraintsADT a -> Maybe (WQO a)
forall a. HasCallStack => a
undefined