{-# 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 forall a. Eq a => a -> a -> Bool
== a
u = 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) = 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
        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]
_) = 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 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) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [RuntimeTerm]
ts forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [RuntimeTerm]
us = 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'  = 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 (forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc forall a b. (a -> b) -> a -> b
$ Op
f Op -> Op -> OpOrdering
=. Op
g)
    subs :: [oc Op]
subs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (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
    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' 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 forall a. Eq a => a -> a -> Bool
== RuntimeTerm
u then oc Op
cs else 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  = 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' = 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 = 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 (forall a b. (a -> b) -> [a] -> [b]
map RuntimeTerm -> oc Op
go [RuntimeTerm]
ts) where
      go :: RuntimeTerm -> oc Op
go RuntimeTerm
ti = 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 forall a. Eq a => a -> a -> Bool
== Op
g
      then forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m
oc
      else 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 (forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc forall a b. (a -> b) -> a -> b
$ Op
f Op -> Op -> OpOrdering
>. Op
g)

    -- f = g ∧ t > uⱼ for all j ts >lex us
    case3 :: oc Op
case3 =
      if Bool
strict Bool -> Bool -> Bool
&& Op
f forall a. Eq a => a -> a -> Bool
/= Op
g
      then forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m
oc
      else 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, 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 forall a. Eq a => a -> a -> Bool
== Relation
GT) oc Op
cs (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] forall a. [a] -> [a] -> [a]
++ [oc Op]
symEQ) where
        symEQ :: [oc Op]
symEQ = [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 -> OpOrdering
=. Op
g) | Op
f forall a. Eq a => a -> a -> Bool
/= Op
g]


    tDominatesUs :: oc Op
tDominatesUs = 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 (forall a b. (a -> b) -> [a] -> [b]
map RuntimeTerm -> oc Op
go [RuntimeTerm]
us) where
      go :: RuntimeTerm -> oc Op
go = 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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