{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module Logical.OrdConstraints where
import Control.Exception
import Data.Foldable (Foldable, any)
import GHC.Base hiding (O)
import GHC.List hiding (any)
import Text.Show
import Text.Read
import GHC.Real (rem)
import Data.Maybe (fromMaybe)
data OrdConstraints a = O [a] | C [a] deriving (OrdConstraints a -> OrdConstraints a -> Bool
forall a. Eq a => OrdConstraints a -> OrdConstraints a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OrdConstraints a -> OrdConstraints a -> Bool
$c/= :: forall a. Eq a => OrdConstraints a -> OrdConstraints a -> Bool
== :: OrdConstraints a -> OrdConstraints a -> Bool
$c== :: forall a. Eq a => OrdConstraints a -> OrdConstraints a -> Bool
Eq, OrdConstraints a -> OrdConstraints a -> Bool
OrdConstraints a -> OrdConstraints 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 (OrdConstraints a)
forall a. Ord a => OrdConstraints a -> OrdConstraints a -> Bool
forall a. Ord a => OrdConstraints a -> OrdConstraints a -> Ordering
forall a.
Ord a =>
OrdConstraints a -> OrdConstraints a -> OrdConstraints a
min :: OrdConstraints a -> OrdConstraints a -> OrdConstraints a
$cmin :: forall a.
Ord a =>
OrdConstraints a -> OrdConstraints a -> OrdConstraints a
max :: OrdConstraints a -> OrdConstraints a -> OrdConstraints a
$cmax :: forall a.
Ord a =>
OrdConstraints a -> OrdConstraints a -> OrdConstraints a
>= :: OrdConstraints a -> OrdConstraints a -> Bool
$c>= :: forall a. Ord a => OrdConstraints a -> OrdConstraints a -> Bool
> :: OrdConstraints a -> OrdConstraints a -> Bool
$c> :: forall a. Ord a => OrdConstraints a -> OrdConstraints a -> Bool
<= :: OrdConstraints a -> OrdConstraints a -> Bool
$c<= :: forall a. Ord a => OrdConstraints a -> OrdConstraints a -> Bool
< :: OrdConstraints a -> OrdConstraints a -> Bool
$c< :: forall a. Ord a => OrdConstraints a -> OrdConstraints a -> Bool
compare :: OrdConstraints a -> OrdConstraints a -> Ordering
$ccompare :: forall a. Ord a => OrdConstraints a -> OrdConstraints a -> Ordering
Ord, Int -> OrdConstraints a -> ShowS
forall a. Show a => Int -> OrdConstraints a -> ShowS
forall a. Show a => [OrdConstraints a] -> ShowS
forall a. Show a => OrdConstraints a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OrdConstraints a] -> ShowS
$cshowList :: forall a. Show a => [OrdConstraints a] -> ShowS
show :: OrdConstraints a -> String
$cshow :: forall a. Show a => OrdConstraints a -> String
showsPrec :: Int -> OrdConstraints a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> OrdConstraints a -> ShowS
Show, ReadPrec [OrdConstraints a]
ReadPrec (OrdConstraints a)
ReadS [OrdConstraints a]
forall a. Read a => ReadPrec [OrdConstraints a]
forall a. Read a => ReadPrec (OrdConstraints a)
forall a. Read a => Int -> ReadS (OrdConstraints a)
forall a. Read a => ReadS [OrdConstraints a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [OrdConstraints a]
$creadListPrec :: forall a. Read a => ReadPrec [OrdConstraints a]
readPrec :: ReadPrec (OrdConstraints a)
$creadPrec :: forall a. Read a => ReadPrec (OrdConstraints a)
readList :: ReadS [OrdConstraints a]
$creadList :: forall a. Read a => ReadS [OrdConstraints a]
readsPrec :: Int -> ReadS (OrdConstraints a)
$creadsPrec :: forall a. Read a => Int -> ReadS (OrdConstraints a)
Read)
type OrdCs t a = t (OrdConstraints a)
validOrdCs :: Ord a => OrdConstraints a -> Bool
validOrdCs :: forall a. Ord a => OrdConstraints a -> Bool
validOrdCs (O (a
_:[a]
_)) = Bool
True
validOrdCs (C xs :: [a]
xs@(a
_:a
_:[a]
_)) = (forall a. [a] -> Int
length [a]
xs forall a. Integral a => a -> a -> a
`rem` Int
2) forall a. Eq a => a -> a -> Bool
== Int
0
validOrdCs OrdConstraints a
_ = Bool
False
ordCs2Predicate1 :: Ord a => OrdConstraints a -> a -> Bool
ordCs2Predicate1 :: forall a. Ord a => OrdConstraints a -> a -> Bool
ordCs2Predicate1 x :: OrdConstraints a
x@(O [a]
xs) a
y
| forall a. Ord a => OrdConstraints a -> Bool
validOrdCs OrdConstraints a
x = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Eq a => a -> a -> Bool
== a
y) [a]
xs
| Bool
otherwise = forall a. HasCallStack => String -> a
error String
"Logical.OrdConstraints.ordCs2Predicate1: Not valid logical constraint by constrution semantics."
ordCs2Predicate1 x :: OrdConstraints a
x@(C [a]
xs) a
y
| forall a. Ord a => OrdConstraints a -> Bool
validOrdCs OrdConstraints a
x = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(a
t:a
u:[a]
_) -> a
y forall a. Ord a => a -> a -> Bool
>= a
t Bool -> Bool -> Bool
&& a
y forall a. Ord a => a -> a -> Bool
<= a
u) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. [a] -> [[a]]
f forall a b. (a -> b) -> a -> b
$ [a]
xs
| Bool
otherwise = forall a. HasCallStack => String -> a
error String
"Logical.OrdConstraints.ordCs2Predicate1: Not valid logical constraint by constrution semantics."
where f :: [a] -> [[a]]
f (a
x:a
y:[a]
xs) = [a
x,a
y]forall a. a -> [a] -> [a]
:[a] -> [[a]]
f [a]
xs
f [] = []
ordCs2HPred1 :: (Ord a, Foldable t1) => OrdCs t1 a -> a -> Bool
ordCs2HPred1 :: forall a (t1 :: * -> *).
(Ord a, Foldable t1) =>
OrdCs t1 a -> a -> Bool
ordCs2HPred1 OrdCs t1 a
cs a
y = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\OrdConstraints a
c -> forall a. Ord a => OrdConstraints a -> a -> Bool
ordCs2Predicate1 OrdConstraints a
c a
y) forall a b. (a -> b) -> a -> b
$ OrdCs t1 a
cs
ordCs2Predicate :: Ord a => OrdConstraints a -> [a] -> Bool
ordCs2Predicate :: forall a. Ord a => OrdConstraints a -> [a] -> Bool
ordCs2Predicate OrdConstraints a
x [a]
ys
| forall a. [a] -> Bool
null [a]
ys = Bool
False
| Bool
otherwise = forall a. Ord a => OrdConstraints a -> a -> Bool
ordCs2Predicate1 OrdConstraints a
x (forall a. [a] -> a
head [a]
ys)
{-# INLINE ordCs2Predicate #-}
ordCs2HPred :: (Ord a, Foldable t1) => OrdCs t1 a -> [a] -> Bool
ordCs2HPred :: forall a (t1 :: * -> *).
(Ord a, Foldable t1) =>
OrdCs t1 a -> [a] -> Bool
ordCs2HPred OrdCs t1 a
cs [a]
ys
| forall a. [a] -> Bool
null [a]
ys = Bool
False
| Bool
otherwise = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\OrdConstraints a
c -> forall a. Ord a => OrdConstraints a -> a -> Bool
ordCs2Predicate1 OrdConstraints a
c (forall a. [a] -> a
head [a]
ys)) forall a b. (a -> b) -> a -> b
$ OrdCs t1 a
cs
ordCs2PredicateG :: (Ord a, Foldable t) => OrdConstraints a -> (t a -> Maybe a) -> t a -> Bool
ordCs2PredicateG :: forall a (t :: * -> *).
(Ord a, Foldable t) =>
OrdConstraints a -> (t a -> Maybe a) -> t a -> Bool
ordCs2PredicateG x :: OrdConstraints a
x@(O [a]
xs) t a -> Maybe a
p t a
ys
| forall a. Ord a => OrdConstraints a -> Bool
validOrdCs OrdConstraints a
x = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\a
k -> (forall a. a -> Maybe a -> a
fromMaybe Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Eq a => a -> a -> Bool
== a
k) forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Maybe a
p forall a b. (a -> b) -> a -> b
$ t a
ys)) [a]
xs
| Bool
otherwise = forall a. HasCallStack => String -> a
error String
"Logical.OrdConstraints.ordCs2PredicateG: Not valid logical constraint by constrution semantics."
ordCs2PredicateG x :: OrdConstraints a
x@(C [a]
xs) t a -> Maybe a
p t a
ys
| forall a. Ord a => OrdConstraints a -> Bool
validOrdCs OrdConstraints a
x = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(a
t:a
u:[a]
_) -> forall a. a -> Maybe a -> a
fromMaybe Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
k -> a
k forall a. Ord a => a -> a -> Bool
>= a
t Bool -> Bool -> Bool
&& a
k forall a. Ord a => a -> a -> Bool
<= a
u) forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Maybe a
p forall a b. (a -> b) -> a -> b
$ t a
ys) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. [a] -> [[a]]
f forall a b. (a -> b) -> a -> b
$ [a]
xs
| Bool
otherwise = forall a. HasCallStack => String -> a
error String
"Logical.OrdConstraints.ordCs2PredicateG: Not valid logical constraint by constrution semantics."
where f :: [a] -> [[a]]
f (a
x:a
y:[a]
xs) = [a
x,a
y]forall a. a -> [a] -> [a]
:[a] -> [[a]]
f [a]
xs
f [] = []
ordCs2HPredG :: (Ord a, Foldable t, Foldable t1) => OrdCs t1 a -> (t a -> Maybe a) -> t a -> Bool
ordCs2HPredG :: forall a (t :: * -> *) (t1 :: * -> *).
(Ord a, Foldable t, Foldable t1) =>
OrdCs t1 a -> (t a -> Maybe a) -> t a -> Bool
ordCs2HPredG OrdCs t1 a
cs t a -> Maybe a
p t a
ys = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\OrdConstraints a
c -> forall a (t :: * -> *).
(Ord a, Foldable t) =>
OrdConstraints a -> (t a -> Maybe a) -> t a -> Bool
ordCs2PredicateG OrdConstraints a
c t a -> Maybe a
p t a
ys) forall a b. (a -> b) -> a -> b
$ OrdCs t1 a
cs