{-# 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
forall a. Eq a => LazyOC a -> LazyOC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LazyOC a -> LazyOC a -> Bool
$c/= :: forall a. Eq a => LazyOC a -> LazyOC a -> Bool
== :: LazyOC a -> LazyOC a -> Bool
$c== :: forall a. Eq a => LazyOC a -> LazyOC a -> Bool
Eq, LazyOC a -> LazyOC a -> Bool
LazyOC a -> LazyOC a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (LazyOC a)
forall a. Ord a => LazyOC a -> LazyOC a -> Bool
forall a. Ord a => LazyOC a -> LazyOC a -> Ordering
forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
min :: LazyOC a -> LazyOC a -> LazyOC a
$cmin :: forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
max :: LazyOC a -> LazyOC a -> LazyOC a
$cmax :: forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
>= :: LazyOC a -> LazyOC a -> Bool
$c>= :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
> :: LazyOC a -> LazyOC a -> Bool
$c> :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
<= :: LazyOC a -> LazyOC a -> Bool
$c<= :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
< :: LazyOC a -> LazyOC a -> Bool
$c< :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
compare :: LazyOC a -> LazyOC a -> Ordering
$ccompare :: forall a. Ord a => LazyOC a -> LazyOC a -> Ordering
Ord, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (LazyOC a) x -> LazyOC a
forall a x. LazyOC a -> Rep (LazyOC a) x
$cto :: forall a x. Rep (LazyOC a) x -> LazyOC a
$cfrom :: forall a x. LazyOC a -> Rep (LazyOC a) x
Generic, forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall {a}. Hashable a => Eq (LazyOC a)
forall a. Hashable a => Int -> LazyOC a -> Int
forall a. Hashable a => LazyOC a -> Int
hash :: LazyOC a -> Int
$chash :: forall a. Hashable a => LazyOC a -> Int
hashWithSalt :: Int -> LazyOC a -> Int
$chashWithSalt :: forall a. Hashable a => Int -> LazyOC a -> Int
Hashable)

getOrdering :: LazyOC a -> Maybe (WQO a)
getOrdering :: forall a. LazyOC a -> Maybe (WQO a)
getOrdering (Sat WQO a
wqo Thunk a
_) = forall a. a -> Maybe a
Just WQO a
wqo
getOrdering LazyOC a
_           = forall a. Maybe a
Nothing

eval :: (Eq a, Ord a, Hashable a) => ADT.ConstraintsADT a -> LazyOC a
eval :: forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval (ADT.Sat WQO a
w)   = forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
w forall a. ConstraintsADT a
ADT.Unsat
eval ConstraintsADT a
ADT.Unsat     = forall a. LazyOC a
Unsat
eval (ADT.Union ConstraintsADT a
lhs ConstraintsADT a
rhs) =
  case forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
lhs of
    Sat WQO a
w ConstraintsADT a
t1' -> forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
w (forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union ConstraintsADT a
t1' ConstraintsADT a
rhs)
    LazyOC a
Unsat     -> forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
rhs

eval (ADT.Intersect ConstraintsADT a
t1 ConstraintsADT a
t2)       =
  case (forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
t1, forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
t2) of
    (Sat WQO a
c1 ConstraintsADT a
t1', Sat WQO a
c2 ConstraintsADT a
t2') ->
      let
        rest :: ConstraintsADT a
rest =
          forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect (forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
c1) ConstraintsADT a
t2' forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`ADT.union`
          forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect (forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
c2) ConstraintsADT a
t1' forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`ADT.union`
          forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect ConstraintsADT a
t1' ConstraintsADT a
t2'
      in
        case forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
c1 WQO a
c2 of
          Just WQO a
c' -> forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
c' ConstraintsADT a
rest
          Maybe (WQO a)
Nothing -> forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval ConstraintsADT a
rest
    (LazyOC a, LazyOC a)
_ -> forall a. LazyOC a
Unsat


toADT :: Eq a => LazyOC a -> ADT.ConstraintsADT a
toADT :: forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
Unsat     = forall a. ConstraintsADT a
ADT.Unsat
toADT (Sat WQO a
w Thunk a
r) = forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union (forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
w) Thunk a
r

instance (Show a, Eq a, Ord a, Hashable a) => Show (LazyOC a) where
  show :: LazyOC a -> String
show LazyOC a
Unsat     = String
"⊥"
  show (Sat WQO a
s Thunk a
r) = forall r. PrintfType r => String -> r
printf String
"%s ∨ lazy(%s)" (forall a. Show a => a -> String
show WQO a
s) (forall a. Show a => a -> String
show Thunk a
r)

-- | Returns a new instance of 'LazyOC' permitting all WQOs
noConstraints :: LazyOC a
noConstraints :: forall a. LazyOC a
noConstraints = forall a. WQO a -> Thunk a -> LazyOC a
Sat forall a. WQO a
WQO.empty forall a. ConstraintsADT a
ADT.Unsat

unsatisfiable :: LazyOC a
unsatisfiable :: forall a. LazyOC a
unsatisfiable = forall a. LazyOC a
Unsat

union :: Eq a => LazyOC a -> LazyOC a -> LazyOC a
union :: forall a. Eq a => LazyOC a -> LazyOC a -> LazyOC a
union LazyOC a
Unsat LazyOC a
s                 = LazyOC a
s
union LazyOC a
s LazyOC a
Unsat                 = LazyOC a
s
union (Sat WQO a
s Thunk a
_)    LazyOC a
_          | WQO a
s forall a. Eq a => a -> a -> Bool
== forall a. WQO a
WQO.empty = forall a. LazyOC a
noConstraints
union LazyOC a
_           (Sat WQO a
s Thunk a
_)   | WQO a
s forall a. Eq a => a -> a -> Bool
== forall a. WQO a
WQO.empty = forall a. LazyOC a
noConstraints
union (Sat WQO a
s1 Thunk a
r1) (Sat WQO a
s2 Thunk a
r2) = forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
s1 (forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union (forall a. WQO a -> ConstraintsADT a
ADT.Sat WQO a
s2) (forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.union Thunk a
r1 Thunk a
r2))

intersect :: (Ord a, Hashable a) => LazyOC a -> LazyOC a -> LazyOC a
intersect :: forall a. (Ord a, Hashable a) => LazyOC a -> LazyOC a -> LazyOC a
intersect LazyOC a
t1 LazyOC a
t2 = forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval forall a b. (a -> b) -> a -> b
$ forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
ADT.intersect (forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
t1) (forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
t2)

-- | 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 = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
notStrongerThan LazyOC a
t1    LazyOC a
t2    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LazyOC a
t1 forall a. Eq a => a -> a -> Bool
== LazyOC a
t2

-- | @addConstraint 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 = forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
ADT.addConstraint WQO a
o (forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
c)

permits :: (Ord a, Hashable a) => LazyOC a -> WQO.WQO a -> Bool
permits :: forall a. (Ord a, Hashable a) => LazyOC a -> WQO a -> Bool
permits LazyOC a
Unsat WQO a
_            = Bool
False
permits (Sat WQO a
s1 Thunk a
thunk) WQO a
wqo = WQO a
s1 forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
wqo Bool -> Bool -> Bool
|| forall a. (Ord a, Hashable a) => LazyOC a -> WQO a -> Bool
permits (forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval Thunk a
thunk) WQO a
wqo

-- | See 'LazyOC'
lazyOC :: Monad m => OC.WQOConstraints LazyOC m
lazyOC :: forall (m :: * -> *). Monad m => WQOConstraints LazyOC m
lazyOC = forall (impl :: * -> *) (m :: * -> *).
(forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a)
-> (forall a.
    (Show a, Eq a, Ord a, Hashable a) =>
    impl a -> impl a -> impl a)
-> (forall a.
    (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
    impl a -> m Bool)
-> (forall a.
    (ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
    impl a -> impl a -> m Bool)
-> (forall a. (Eq a, Ord a, Hashable a) => impl a)
-> (forall a.
    (Show a, Eq a, Ord a, Hashable a) =>
    impl a -> WQO a -> Bool)
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    impl a -> impl a -> impl a)
-> (forall a. impl a)
-> (forall a. impl a -> Maybe (WQO a))
-> WQOConstraints impl m
OC.OC
  forall a. (Ord a, Hashable a) => WQO a -> LazyOC a -> LazyOC a
addConstraint
  forall a. (Ord a, Hashable a) => LazyOC a -> LazyOC a -> LazyOC a
intersect
  (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LazyOC a -> Bool
isSatisfiable)
  forall (m :: * -> *) a.
(Monad m, Eq a) =>
LazyOC a -> LazyOC a -> m Bool
notStrongerThan
  forall a. LazyOC a
noConstraints
  forall a. (Ord a, Hashable a) => LazyOC a -> WQO a -> Bool
permits
  forall a. Eq a => LazyOC a -> LazyOC a -> LazyOC a
union
  forall a. LazyOC a
unsatisfiable
  forall a. LazyOC a -> Maybe (WQO a)
getOrdering