{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | This module defines "Lazy" constraints on a WQO; the intention is that
--   computations on this type do only the necessary amount of work to determine
--   satisfiability (deferring further computations in a thunk).
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

-- Partially lazy ordering constraints:
-- thunks computation after showing satisfiability

type Thunk a = ADT.ConstraintsADT a

-- | Implementation of "Lazy" ordering constraints.
data LazyOC a =
    Unsat
    -- @Sat wqo thunk@ represent satisfiable constraints; @wqo@ is a candidate.
    -- @Thunk@ represents the other satisfiable constraints, if any.
  | 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
$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
/= :: 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
$ccompare :: forall a. Ord a => LazyOC a -> LazyOC a -> Ordering
compare :: LazyOC a -> LazyOC a -> Ordering
$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
>= :: LazyOC a -> LazyOC a -> Bool
$cmax :: forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
max :: LazyOC a -> LazyOC a -> LazyOC a
$cmin :: forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
min :: LazyOC a -> LazyOC a -> 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
$cfrom :: forall a x. LazyOC a -> Rep (LazyOC a) x
from :: forall x. LazyOC a -> Rep (LazyOC a) x
$cto :: forall a x. Rep (LazyOC a) x -> LazyOC a
to :: forall x. Rep (LazyOC a) x -> LazyOC a
Generic, Eq (LazyOC a)
Eq (LazyOC a) =>
(Int -> LazyOC a -> Int)
-> (LazyOC a -> Int) -> Hashable (LazyOC a)
Int -> LazyOC a -> Int
LazyOC a -> Int
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
$chashWithSalt :: forall a. Hashable a => Int -> LazyOC a -> Int
hashWithSalt :: Int -> LazyOC a -> Int
$chash :: forall a. Hashable a => LazyOC a -> Int
hash :: 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
_) = 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 :: forall a. (Eq a, Ord a, Hashable a) => 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
lhs 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
rhs)
    LazyOC a
Unsat     -> ConstraintsADT a -> LazyOC a
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 (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 :: forall a. Eq a => 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)

-- | Returns a new instance of 'LazyOC' permitting all WQOs
noConstraints :: LazyOC a
noConstraints :: forall a. 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 :: forall a. LazyOC a
unsatisfiable = LazyOC a
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 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 :: forall a. (Ord a, Hashable a) => 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)

-- | Returns @true@ if any orderings are permitted
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 = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
notStrongerThan LazyOC a
t1    LazyOC a
t2    = Bool -> m Bool
forall a. a -> m a
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 o c@ strengthes @c@ to also contain every relation in @o@
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 = 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 :: 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 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

-- | See 'LazyOC'
lazyOC :: Monad m => OC.WQOConstraints LazyOC m
lazyOC :: forall (m :: * -> *). Monad m => 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 -> LazyOC a -> LazyOC a)
-> (forall a. LazyOC a)
-> (forall a. LazyOC a -> Maybe (WQO 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 -> impl a -> impl a)
-> (forall a. impl a)
-> (forall a. impl a -> Maybe (WQO a))
-> WQOConstraints impl m
OC.OC
  WQO a -> LazyOC a -> LazyOC a
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
  LazyOC a -> LazyOC a -> LazyOC a
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 a. a -> m a
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)
  LazyOC a -> LazyOC a -> m Bool
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
  LazyOC a
forall a. LazyOC a
forall a. (Eq a, Ord a, Hashable a) => LazyOC a
noConstraints
  LazyOC a -> WQO a -> Bool
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
  LazyOC a -> LazyOC a -> LazyOC a
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
  LazyOC a
forall a. LazyOC a
unsatisfiable
  LazyOC a -> Maybe (WQO a)
forall a. LazyOC a -> Maybe (WQO a)
getOrdering