{-# 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

-- | Represents constraints over a WQO on @a@
data ConstraintsADT a =
 -- | @Sat wqo@ represents satisfiable constraints: those that permit each relation in @wqo@.
    Sat (WQO a)
  | Unsat
    -- | @Union c1 c2@ permits orderings of P1 and orderings of P2
  | Union (ConstraintsADT a) (ConstraintsADT a)
    -- | @Intersect c1 c2@ permits orderings iff permitted by P1 and permitted by P2
  | 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 c1 c2@ permits orderings iff permitted by P1 and permitted by P2
intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a

#ifdef OPTIMIZE_WQO
-- Optimization
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 c1 c2@ permits orderings of P1 and orderings of P2
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 o c@ strengthes @c@ to also contain every relation in @o@
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 = -- trace' ("Get constraints, size : " ++ (show $ dnfSize 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
   -- trace' = trace

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
   -- trace' = trace

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)

-- | See 'ConstraintsADT'
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