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

module Language.REST.WQOConstraints.Lazy (
      lazyOC
    , addConstraint
    , intersect
    , isSatisfiable
    , noConstraints
    , singleton
    , union
    , unsatisfiable
    , LazyOC
    ) where

import Text.Printf
import GHC.Generics (Generic)
import Data.Hashable
import qualified Data.Set as S

import qualified Language.REST.Internal.WQO as WQO
import qualified Language.REST.WQOConstraints as OC
import qualified Language.REST.WQOConstraints.ADT as ADT

type WQO = WQO.WQO

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

type Thunk a = ADT.ConstraintsADT a

data LazyOC a =
    Unsat
  | Sat (WQO a) (Thunk a)
  deriving (LazyOC a -> LazyOC a -> Bool
(LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> Bool) -> Eq (LazyOC a)
forall a. Eq a => LazyOC a -> LazyOC a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LazyOC a -> LazyOC a -> Bool
$c/= :: forall a. Eq a => LazyOC a -> LazyOC a -> Bool
== :: LazyOC a -> LazyOC a -> Bool
$c== :: forall a. Eq a => LazyOC a -> LazyOC a -> Bool
Eq, Eq (LazyOC a)
Eq (LazyOC a)
-> (LazyOC a -> LazyOC a -> Ordering)
-> (LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> Bool)
-> (LazyOC a -> LazyOC a -> LazyOC a)
-> (LazyOC a -> LazyOC a -> LazyOC a)
-> Ord (LazyOC a)
LazyOC a -> LazyOC a -> Bool
LazyOC a -> LazyOC a -> Ordering
LazyOC a -> LazyOC a -> LazyOC a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (LazyOC a)
forall a. Ord a => LazyOC a -> LazyOC a -> Bool
forall a. Ord a => LazyOC a -> LazyOC a -> Ordering
forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
min :: LazyOC a -> LazyOC a -> LazyOC a
$cmin :: forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
max :: LazyOC a -> LazyOC a -> LazyOC a
$cmax :: forall a. Ord a => LazyOC a -> LazyOC a -> LazyOC a
>= :: LazyOC a -> LazyOC a -> Bool
$c>= :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
> :: LazyOC a -> LazyOC a -> Bool
$c> :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
<= :: LazyOC a -> LazyOC a -> Bool
$c<= :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
< :: LazyOC a -> LazyOC a -> Bool
$c< :: forall a. Ord a => LazyOC a -> LazyOC a -> Bool
compare :: LazyOC a -> LazyOC a -> Ordering
$ccompare :: forall a. Ord a => LazyOC a -> LazyOC a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (LazyOC a)
Ord, (forall x. LazyOC a -> Rep (LazyOC a) x)
-> (forall x. Rep (LazyOC a) x -> LazyOC a) -> Generic (LazyOC a)
forall x. Rep (LazyOC a) x -> LazyOC a
forall x. LazyOC a -> Rep (LazyOC a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (LazyOC a) x -> LazyOC a
forall a x. LazyOC a -> Rep (LazyOC a) x
$cto :: forall a x. Rep (LazyOC a) x -> LazyOC a
$cfrom :: forall a x. LazyOC a -> Rep (LazyOC a) x
Generic, Int -> LazyOC a -> Int
LazyOC a -> Int
(Int -> LazyOC a -> Int)
-> (LazyOC a -> Int) -> Hashable (LazyOC a)
forall a. Hashable a => Int -> LazyOC a -> Int
forall a. Hashable a => LazyOC a -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: LazyOC a -> Int
$chash :: forall a. Hashable a => LazyOC a -> Int
hashWithSalt :: Int -> LazyOC a -> Int
$chashWithSalt :: forall a. Hashable a => Int -> LazyOC a -> Int
Hashable)

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

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

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


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

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

noConstraints :: LazyOC a
noConstraints :: LazyOC a
noConstraints = WQO a -> Thunk a -> LazyOC a
forall a. WQO a -> Thunk a -> LazyOC a
Sat (WQO a
forall a. WQO a
WQO.empty) Thunk a
forall a. ConstraintsADT a
ADT.Unsat

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

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

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

isSatisfiable :: LazyOC a -> Bool
isSatisfiable :: LazyOC a -> Bool
isSatisfiable (Sat WQO a
_ Thunk a
_) = Bool
True
isSatisfiable LazyOC a
Unsat     = Bool
False

singleton :: WQO a -> LazyOC a
singleton :: WQO a -> LazyOC a
singleton WQO a
c = WQO a -> Thunk a -> LazyOC a
forall a. WQO a -> Thunk a -> LazyOC a
Sat WQO a
c Thunk a
forall a. ConstraintsADT a
ADT.Unsat

relevantConstraints
  :: (Eq a, Ord a, Hashable a) => LazyOC a -> S.Set a -> S.Set a -> LazyOC a
relevantConstraints :: LazyOC a -> Set a -> Set a -> LazyOC a
relevantConstraints LazyOC a
c Set a
_ Set a
_ = LazyOC a
c

notStrongerThan :: (Monad m, Eq a) => LazyOC a -> LazyOC a -> m Bool
notStrongerThan :: LazyOC a -> LazyOC a -> m Bool
notStrongerThan LazyOC a
_     LazyOC a
Unsat = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
notStrongerThan LazyOC a
t1    LazyOC a
t2    = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ LazyOC a
t1 LazyOC a -> LazyOC a -> Bool
forall a. Eq a => a -> a -> Bool
== LazyOC a
t2

addConstraint :: (Ord a, Hashable a) => ADT.WQO a -> LazyOC a -> LazyOC a
addConstraint :: WQO a -> LazyOC a -> LazyOC a
addConstraint WQO a
o LazyOC a
c = ConstraintsADT a -> LazyOC a
forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> LazyOC a
eval (ConstraintsADT a -> LazyOC a) -> ConstraintsADT a -> LazyOC a
forall a b. (a -> b) -> a -> b
$ WQO a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
ADT.addConstraint WQO a
o (LazyOC a -> ConstraintsADT a
forall a. Eq a => LazyOC a -> ConstraintsADT a
toADT LazyOC a
c)

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

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