{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}




module Language.REST.LPO (lpo, lpoStrict) where

import Prelude hiding (EQ, GT, lex)

import Control.Monad.Identity
import Data.Hashable

import           Language.REST.Op
import           Language.REST.Internal.OpOrdering as OpOrdering
import           Language.REST.WQOConstraints as OC
import           Language.REST.Types
import           Language.REST.RuntimeTerm

lex
  :: (Eq a, Ord b, Hashable b)
  => WQOConstraints impl m
  -> Bool
  -> impl b
  -> (WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b)
  -> [a]
  -> [a]
  -> impl b
lex :: forall a b (impl :: * -> *) (m :: * -> *).
(Eq a, Ord b, Hashable b) =>
WQOConstraints impl m
-> Bool
-> impl b
-> (WQOConstraints impl m
    -> Relation -> impl b -> a -> a -> impl b)
-> [a]
-> [a]
-> impl b
lex WQOConstraints impl m
oc Bool
strict impl b
cs WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b
f (a
t:[a]
ts) (a
u:[a]
us) | a
t a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
u = WQOConstraints impl m
-> Bool
-> impl b
-> (WQOConstraints impl m
    -> Relation -> impl b -> a -> a -> impl b)
-> [a]
-> [a]
-> impl b
forall a b (impl :: * -> *) (m :: * -> *).
(Eq a, Ord b, Hashable b) =>
WQOConstraints impl m
-> Bool
-> impl b
-> (WQOConstraints impl m
    -> Relation -> impl b -> a -> a -> impl b)
-> [a]
-> [a]
-> impl b
lex WQOConstraints impl m
oc Bool
strict impl b
cs WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b
f [a]
ts [a]
us
lex WQOConstraints impl m
oc Bool
strict impl b
cs WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b
f (a
t:[a]
ts) (a
u:[a]
us) = WQOConstraints impl m
-> forall a.
   (Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> impl a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
   (Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> impl a
union WQOConstraints impl m
oc impl b
case1 impl b
case2
  where
    -- t > u
    case1 :: impl b
case1 = WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b
f WQOConstraints impl m
oc Relation
GT impl b
cs a
t a
u
    -- t = u
    case2 :: impl b
case2 =
      let
        cs' :: impl b
cs' = WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b
f WQOConstraints impl m
oc Relation
EQ impl b
cs a
t a
u
      in
        WQOConstraints impl m
-> Bool
-> impl b
-> (WQOConstraints impl m
    -> Relation -> impl b -> a -> a -> impl b)
-> [a]
-> [a]
-> impl b
forall a b (impl :: * -> *) (m :: * -> *).
(Eq a, Ord b, Hashable b) =>
WQOConstraints impl m
-> Bool
-> impl b
-> (WQOConstraints impl m
    -> Relation -> impl b -> a -> a -> impl b)
-> [a]
-> [a]
-> impl b
lex WQOConstraints impl m
oc Bool
strict impl b
cs' WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b
f [a]
ts [a]
us
lex WQOConstraints impl m
oc Bool
_      impl b
_  WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b
_ []    (a
_:[a]
_) = WQOConstraints impl m -> forall a. impl a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints impl m
oc
lex WQOConstraints impl m
_  Bool
_      impl b
cs WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b
_ (a
_:[a]
_) []    = impl b
cs
lex WQOConstraints impl m
oc Bool
strict impl b
cs WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b
_ []    []    = if Bool
strict then WQOConstraints impl m -> forall a. impl a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints impl m
oc else impl b
cs

lpo' :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
  Bool -> WQOConstraints oc m -> Relation -> oc Op -> RuntimeTerm -> RuntimeTerm -> oc Op
-- lpo' False oc EQ cs t u = intersect oc (lpo' False oc GTE cs t u) (lpo' False oc GTE cs u t)
lpo' :: forall (oc :: * -> *) (m :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
lpo' Bool
False WQOConstraints oc m
oc Relation
EQ oc Op
_cs (App Op
_f [RuntimeTerm]
ts) (App Op
_g [RuntimeTerm]
us) | [RuntimeTerm] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RuntimeTerm]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [RuntimeTerm] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RuntimeTerm]
us = WQOConstraints oc m -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m
oc
lpo' Bool
False WQOConstraints oc m
oc Relation
EQ oc Op
cs (App Op
f [RuntimeTerm]
ts) (App Op
g [RuntimeTerm]
us) =
  let
    cs' :: oc Op
cs'  = WQOConstraints oc m
-> forall a.
   (Show a, Eq a, Ord a, Hashable a) =>
   oc a -> oc a -> oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
   (Show a, Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> impl a
intersect WQOConstraints oc m
oc oc Op
cs (WQOConstraints oc m -> WQO Op -> oc Op
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc (WQO Op -> oc Op) -> WQO Op -> oc Op
forall a b. (a -> b) -> a -> b
$ Op
f Op -> Op -> WQO Op
=. Op
g)
    subs :: [oc Op]
subs = (RuntimeTerm -> RuntimeTerm -> oc Op)
-> [RuntimeTerm] -> [RuntimeTerm] -> [oc Op]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
forall (oc :: * -> *) (m :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
lpo' Bool
False WQOConstraints oc m
oc Relation
EQ oc Op
cs') [RuntimeTerm]
ts [RuntimeTerm]
us
  in
    WQOConstraints oc m -> [oc Op] -> oc Op
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
intersectAll WQOConstraints oc m
oc (oc Op
cs' oc Op -> [oc Op] -> [oc Op]
forall a. a -> [a] -> [a]
: [oc Op]
subs)

lpo' Bool
True  WQOConstraints oc m
oc Relation
EQ oc Op
cs RuntimeTerm
t RuntimeTerm
u = if RuntimeTerm
t RuntimeTerm -> RuntimeTerm -> Bool
forall a. Eq a => a -> a -> Bool
== RuntimeTerm
u then oc Op
cs else WQOConstraints oc m -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m
oc
lpo' Bool
strict WQOConstraints oc m
oc Relation
r oc Op
cs t :: RuntimeTerm
t@(App Op
f [RuntimeTerm]
ts) u :: RuntimeTerm
u@(App Op
g [RuntimeTerm]
us) = oc Op
result
  where
    result :: oc Op
result  = WQOConstraints oc m
-> forall a.
   (Show a, Eq a, Ord a, Hashable a) =>
   oc a -> oc a -> oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
   (Show a, Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> impl a
intersect WQOConstraints oc m
oc oc Op
cs oc Op
result'
    result' :: oc Op
result' = WQOConstraints oc m -> [oc Op] -> oc Op
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
unionAll WQOConstraints oc m
oc [oc Op
case1, oc Op
case2, oc Op
case3]

    -- tᵢ ≥ u for some i
    case1 :: oc Op
case1 = WQOConstraints oc m -> [oc Op] -> oc Op
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
unionAll WQOConstraints oc m
oc ((RuntimeTerm -> oc Op) -> [RuntimeTerm] -> [oc Op]
forall a b. (a -> b) -> [a] -> [b]
map RuntimeTerm -> oc Op
go [RuntimeTerm]
ts) where
      go :: RuntimeTerm -> oc Op
go RuntimeTerm
ti = Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
forall (oc :: * -> *) (m :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
lpo' Bool
strict WQOConstraints oc m
oc Relation
GTE oc Op
cs RuntimeTerm
ti RuntimeTerm
u

    -- f > g ∧ t > uⱼ for all j
    case2 :: oc Op
case2 =
      if Op
f Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
g
      then WQOConstraints oc m -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m
oc
      else WQOConstraints oc m
-> forall a.
   (Show a, Eq a, Ord a, Hashable a) =>
   oc a -> oc a -> oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
   (Show a, Eq a, Ord a, Hashable a) =>
   impl a -> impl a -> impl a
intersect WQOConstraints oc m
oc oc Op
tDominatesUs (WQOConstraints oc m -> WQO Op -> oc Op
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc (WQO Op -> oc Op) -> WQO Op -> oc Op
forall a b. (a -> b) -> a -> b
$ Op
f Op -> Op -> WQO Op
>. Op
g)

    -- f = g ∧ t > uⱼ for all j ts >lex us
    case3 :: oc Op
case3 =
      if Bool
strict Bool -> Bool -> Bool
&& Op
f Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
/= Op
g
      then WQOConstraints oc m -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m
oc
      else WQOConstraints oc m -> [oc Op] -> oc Op
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
intersectAll WQOConstraints oc m
oc ([oc Op
tDominatesUs, WQOConstraints oc m
-> Bool
-> oc Op
-> (WQOConstraints oc m
    -> Relation -> oc Op -> RuntimeTerm -> RuntimeTerm -> oc Op)
-> [RuntimeTerm]
-> [RuntimeTerm]
-> oc Op
forall a b (impl :: * -> *) (m :: * -> *).
(Eq a, Ord b, Hashable b) =>
WQOConstraints impl m
-> Bool
-> impl b
-> (WQOConstraints impl m
    -> Relation -> impl b -> a -> a -> impl b)
-> [a]
-> [a]
-> impl b
lex WQOConstraints oc m
oc (Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
GT) oc Op
cs (Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
forall (oc :: * -> *) (m :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
lpo' Bool
strict) [RuntimeTerm]
ts [RuntimeTerm]
us] [oc Op] -> [oc Op] -> [oc Op]
forall a. [a] -> [a] -> [a]
++ [oc Op]
symEQ) where
        symEQ :: [oc Op]
symEQ = [WQOConstraints oc m -> WQO Op -> oc Op
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc (Op
f Op -> Op -> WQO Op
=. Op
g) | Op
f Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
/= Op
g]


    tDominatesUs :: oc Op
tDominatesUs = WQOConstraints oc m -> [oc Op] -> oc Op
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
intersectAll WQOConstraints oc m
oc ((RuntimeTerm -> oc Op) -> [RuntimeTerm] -> [oc Op]
forall a b. (a -> b) -> [a] -> [b]
map RuntimeTerm -> oc Op
go [RuntimeTerm]
us) where
      go :: RuntimeTerm -> oc Op
go = Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
forall (oc :: * -> *) (m :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
lpo' Bool
strict WQOConstraints oc m
oc Relation
GT oc Op
cs RuntimeTerm
t


-- | Constraint generator for a quasi-order extension to the Lexicographic path ordering
lpo :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity
lpo :: forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm Identity
lpo WQOConstraints oc m'
oc Relation
r oc Op
cs RuntimeTerm
t RuntimeTerm
u = oc Op -> Identity (oc Op)
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (oc Op -> Identity (oc Op)) -> oc Op -> Identity (oc Op)
forall a b. (a -> b) -> a -> b
$ Bool
-> WQOConstraints oc m'
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
forall (oc :: * -> *) (m :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
lpo' Bool
False WQOConstraints oc m'
oc Relation
r oc Op
cs RuntimeTerm
t RuntimeTerm
u

-- | Constraint generator for a strict version of the quasi-order extension to
--   the Lexicographic path ordering.
lpoStrict :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity
lpoStrict :: forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm Identity
lpoStrict WQOConstraints oc m'
oc Relation
r oc Op
cs RuntimeTerm
t RuntimeTerm
u = oc Op -> Identity (oc Op)
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (oc Op -> Identity (oc Op)) -> oc Op -> Identity (oc Op)
forall a b. (a -> b) -> a -> b
$ Bool
-> WQOConstraints oc m'
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
forall (oc :: * -> *) (m :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
Bool
-> WQOConstraints oc m
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> oc Op
lpo' Bool
True WQOConstraints oc m'
oc Relation
r oc Op
cs RuntimeTerm
t RuntimeTerm
u