{-# LANGUAGE FlexibleContexts, UndecidableInstances, RecordWildCards #-}
-- | Solving constraints on variable ordering.
module Twee.Constraints where

--import Twee.Base hiding (equals, Term, pattern Fun, pattern Var, lookup, funs)
import qualified Twee.Term as Flat
import qualified Data.Map.Strict as Map
import Twee.Pretty hiding (equals)
import Twee.Utils
import Data.Maybe
import Data.List hiding (singleton)
import Data.Function
import Data.Graph
import Data.Map.Strict(Map)
import Data.Ord
import Twee.Term hiding (lookup)

data Atom f = Constant (Fun f) | Variable Var deriving (Int -> Atom f -> ShowS
forall f. (Labelled f, Show f) => Int -> Atom f -> ShowS
forall f. (Labelled f, Show f) => [Atom f] -> ShowS
forall f. (Labelled f, Show f) => Atom f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Atom f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Atom f] -> ShowS
show :: Atom f -> String
$cshow :: forall f. (Labelled f, Show f) => Atom f -> String
showsPrec :: Int -> Atom f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Atom f -> ShowS
Show, Atom f -> Atom f -> Bool
forall f. Atom f -> Atom f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Atom f -> Atom f -> Bool
$c/= :: forall f. Atom f -> Atom f -> Bool
== :: Atom f -> Atom f -> Bool
$c== :: forall f. Atom f -> Atom f -> Bool
Eq, Atom f -> Atom f -> Bool
Atom f -> Atom f -> Ordering
forall f. Eq (Atom f)
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 f. Atom f -> Atom f -> Bool
forall f. Atom f -> Atom f -> Ordering
forall f. Atom f -> Atom f -> Atom f
min :: Atom f -> Atom f -> Atom f
$cmin :: forall f. Atom f -> Atom f -> Atom f
max :: Atom f -> Atom f -> Atom f
$cmax :: forall f. Atom f -> Atom f -> Atom f
>= :: Atom f -> Atom f -> Bool
$c>= :: forall f. Atom f -> Atom f -> Bool
> :: Atom f -> Atom f -> Bool
$c> :: forall f. Atom f -> Atom f -> Bool
<= :: Atom f -> Atom f -> Bool
$c<= :: forall f. Atom f -> Atom f -> Bool
< :: Atom f -> Atom f -> Bool
$c< :: forall f. Atom f -> Atom f -> Bool
compare :: Atom f -> Atom f -> Ordering
$ccompare :: forall f. Atom f -> Atom f -> Ordering
Ord)

{-# INLINE atoms #-}
atoms :: Term f -> [Atom f]
atoms :: forall f. Term f -> [Atom f]
atoms Term f
t = forall {f}. TermList f -> [Atom f]
aux (forall f. Term f -> TermList f
singleton Term f
t)
  where
    aux :: TermList f -> [Atom f]
aux TermList f
Empty = []
    aux (Cons (App Fun f
f TermList f
Empty) TermList f
t) = forall f. Fun f -> Atom f
Constant Fun f
fforall a. a -> [a] -> [a]
:TermList f -> [Atom f]
aux TermList f
t
    aux (Cons (Var Var
x) TermList f
t) = forall f. Var -> Atom f
Variable Var
xforall a. a -> [a] -> [a]
:TermList f -> [Atom f]
aux TermList f
t
    aux ConsSym{rest :: forall f. TermList f -> TermList f
rest = TermList f
t} = TermList f -> [Atom f]
aux TermList f
t

toTerm :: Atom f -> Term f
toTerm :: forall f. Atom f -> Term f
toTerm (Constant Fun f
f) = forall a. Build a => a -> Term (BuildFun a)
build (forall f. Fun f -> Builder f
con Fun f
f)
toTerm (Variable Var
x) = forall a. Build a => a -> Term (BuildFun a)
build (forall f. Var -> Builder f
var Var
x)

fromTerm :: Flat.Term f -> Maybe (Atom f)
fromTerm :: forall f. Term f -> Maybe (Atom f)
fromTerm (App Fun f
f TermList f
Empty) = forall a. a -> Maybe a
Just (forall f. Fun f -> Atom f
Constant Fun f
f)
fromTerm (Var Var
x) = forall a. a -> Maybe a
Just (forall f. Var -> Atom f
Variable Var
x)
fromTerm Term f
_ = forall a. Maybe a
Nothing

instance (Labelled f, PrettyTerm f) => Pretty (Atom f) where
  pPrint :: Atom f -> Doc
pPrint = forall a. Pretty a => a -> Doc
pPrint forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Atom f -> Term f
toTerm

data Formula f =
    Less   (Atom f) (Atom f)
  | LessEq (Atom f) (Atom f)
  | And [Formula f]
  | Or  [Formula f]
  deriving (Formula f -> Formula f -> Bool
forall f. Formula f -> Formula f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Formula f -> Formula f -> Bool
$c/= :: forall f. Formula f -> Formula f -> Bool
== :: Formula f -> Formula f -> Bool
$c== :: forall f. Formula f -> Formula f -> Bool
Eq, Formula f -> Formula f -> Ordering
forall f. Eq (Formula f)
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 f. Formula f -> Formula f -> Bool
forall f. Formula f -> Formula f -> Ordering
forall f. Formula f -> Formula f -> Formula f
min :: Formula f -> Formula f -> Formula f
$cmin :: forall f. Formula f -> Formula f -> Formula f
max :: Formula f -> Formula f -> Formula f
$cmax :: forall f. Formula f -> Formula f -> Formula f
>= :: Formula f -> Formula f -> Bool
$c>= :: forall f. Formula f -> Formula f -> Bool
> :: Formula f -> Formula f -> Bool
$c> :: forall f. Formula f -> Formula f -> Bool
<= :: Formula f -> Formula f -> Bool
$c<= :: forall f. Formula f -> Formula f -> Bool
< :: Formula f -> Formula f -> Bool
$c< :: forall f. Formula f -> Formula f -> Bool
compare :: Formula f -> Formula f -> Ordering
$ccompare :: forall f. Formula f -> Formula f -> Ordering
Ord, Int -> Formula f -> ShowS
forall f. (Labelled f, Show f) => Int -> Formula f -> ShowS
forall f. (Labelled f, Show f) => [Formula f] -> ShowS
forall f. (Labelled f, Show f) => Formula f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Formula f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Formula f] -> ShowS
show :: Formula f -> String
$cshow :: forall f. (Labelled f, Show f) => Formula f -> String
showsPrec :: Int -> Formula f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Formula f -> ShowS
Show)

instance (Labelled f, PrettyTerm f) => Pretty (Formula f) where
  pPrintPrec :: PrettyLevel -> Rational -> Formula f -> Doc
pPrintPrec PrettyLevel
_ Rational
_ (Less Atom f
t Atom f
u) = Doc -> Int -> Doc -> Doc
hang (forall a. Pretty a => a -> Doc
pPrint Atom f
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"<") Int
2 (forall a. Pretty a => a -> Doc
pPrint Atom f
u)
  pPrintPrec PrettyLevel
_ Rational
_ (LessEq Atom f
t Atom f
u) = Doc -> Int -> Doc -> Doc
hang (forall a. Pretty a => a -> Doc
pPrint Atom f
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"<=") Int
2 (forall a. Pretty a => a -> Doc
pPrint Atom f
u)
  pPrintPrec PrettyLevel
_ Rational
_ (And []) = String -> Doc
text String
"true"
  pPrintPrec PrettyLevel
_ Rational
_ (Or []) = String -> Doc
text String
"false"
  pPrintPrec PrettyLevel
l Rational
p (And [Formula f]
xs) =
    Bool -> Doc -> Doc
maybeParens (Rational
p forall a. Ord a => a -> a -> Bool
> Rational
10)
      ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
" &") ([Doc] -> [Doc]
nest_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
11) [Formula f]
xs))))
    where
      nest_ :: [Doc] -> [Doc]
nest_ (Doc
x:[Doc]
xs) = Doc
xforall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2) [Doc]
xs
      nest_ [] = forall a. HasCallStack => a
undefined
  pPrintPrec PrettyLevel
l Rational
p (Or [Formula f]
xs) =
    Bool -> Doc -> Doc
maybeParens (Rational
p forall a. Ord a => a -> a -> Bool
> Rational
10)
      ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
" |") ([Doc] -> [Doc]
nest_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
11) [Formula f]
xs))))
    where
      nest_ :: [Doc] -> [Doc]
nest_ (Doc
x:[Doc]
xs) = Doc
xforall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2) [Doc]
xs
      nest_ [] = forall a. HasCallStack => a
undefined

negateFormula :: Formula f -> Formula f
negateFormula :: forall f. Formula f -> Formula f
negateFormula (Less Atom f
t Atom f
u) = forall f. Atom f -> Atom f -> Formula f
LessEq Atom f
u Atom f
t
negateFormula (LessEq Atom f
t Atom f
u) = forall f. Atom f -> Atom f -> Formula f
Less Atom f
u Atom f
t
negateFormula (And [Formula f]
ts) = forall f. [Formula f] -> Formula f
Or (forall a b. (a -> b) -> [a] -> [b]
map forall f. Formula f -> Formula f
negateFormula [Formula f]
ts)
negateFormula (Or [Formula f]
ts) = forall f. [Formula f] -> Formula f
And (forall a b. (a -> b) -> [a] -> [b]
map forall f. Formula f -> Formula f
negateFormula [Formula f]
ts)

conj :: t (Formula f) -> Formula f
conj t (Formula f)
forms
  | forall {f}. Formula f
false forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Formula f]
forms' = forall {f}. Formula f
false
  | Bool
otherwise =
    case [Formula f]
forms' of
      [Formula f
x] -> Formula f
x
      [Formula f]
xs  -> forall f. [Formula f] -> Formula f
And [Formula f]
xs
  where
    flatten :: Formula f -> [Formula f]
flatten (And [Formula f]
xs) = [Formula f]
xs
    flatten Formula f
x = [Formula f
x]
    forms' :: [Formula f]
forms' = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= forall {f}. Formula f
true) (forall a. Ord a => [a] -> [a]
usort (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {f}. Formula f -> [Formula f]
flatten t (Formula f)
forms))
disj :: t (Formula f) -> Formula f
disj t (Formula f)
forms
  | forall {f}. Formula f
true forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Formula f]
forms' = forall {f}. Formula f
true
  | Bool
otherwise =
    case [Formula f]
forms' of
      [Formula f
x] -> Formula f
x
      [Formula f]
xs  -> forall f. [Formula f] -> Formula f
Or [Formula f]
xs
  where
    flatten :: Formula f -> [Formula f]
flatten (Or [Formula f]
xs) = [Formula f]
xs
    flatten Formula f
x = [Formula f
x]
    forms' :: [Formula f]
forms' = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= forall {f}. Formula f
false) (forall a. Ord a => [a] -> [a]
usort (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {f}. Formula f -> [Formula f]
flatten t (Formula f)
forms))

Formula f
x &&& :: Formula f -> Formula f -> Formula f
&&& Formula f
y = forall {t :: * -> *} {f}. Foldable t => t (Formula f) -> Formula f
conj [Formula f
x, Formula f
y]
Formula f
x ||| :: Formula f -> Formula f -> Formula f
||| Formula f
y = forall {t :: * -> *} {f}. Foldable t => t (Formula f) -> Formula f
disj [Formula f
x, Formula f
y]
true :: Formula f
true  = forall f. [Formula f] -> Formula f
And []
false :: Formula f
false = forall f. [Formula f] -> Formula f
Or []

data Branch f =
  -- Branches are kept normalised wrt equals
  Branch {
    forall f. Branch f -> [Fun f]
funs        :: [Fun f],
    forall f. Branch f -> [(Atom f, Atom f)]
less        :: [(Atom f, Atom f)],  -- sorted
    forall f. Branch f -> [(Atom f, Atom f)]
equals      :: [(Atom f, Atom f)] } -- sorted, greatest atom first in each pair
  deriving (Branch f -> Branch f -> Bool
forall f. Branch f -> Branch f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Branch f -> Branch f -> Bool
$c/= :: forall f. Branch f -> Branch f -> Bool
== :: Branch f -> Branch f -> Bool
$c== :: forall f. Branch f -> Branch f -> Bool
Eq, Branch f -> Branch f -> Bool
Branch f -> Branch f -> Ordering
forall f. Eq (Branch f)
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 f. Branch f -> Branch f -> Bool
forall f. Branch f -> Branch f -> Ordering
forall f. Branch f -> Branch f -> Branch f
min :: Branch f -> Branch f -> Branch f
$cmin :: forall f. Branch f -> Branch f -> Branch f
max :: Branch f -> Branch f -> Branch f
$cmax :: forall f. Branch f -> Branch f -> Branch f
>= :: Branch f -> Branch f -> Bool
$c>= :: forall f. Branch f -> Branch f -> Bool
> :: Branch f -> Branch f -> Bool
$c> :: forall f. Branch f -> Branch f -> Bool
<= :: Branch f -> Branch f -> Bool
$c<= :: forall f. Branch f -> Branch f -> Bool
< :: Branch f -> Branch f -> Bool
$c< :: forall f. Branch f -> Branch f -> Bool
compare :: Branch f -> Branch f -> Ordering
$ccompare :: forall f. Branch f -> Branch f -> Ordering
Ord)

instance (Labelled f, PrettyTerm f) => Pretty (Branch f) where
  pPrint :: Branch f -> Doc
pPrint Branch{[(Atom f, Atom f)]
[Fun f]
equals :: [(Atom f, Atom f)]
less :: [(Atom f, Atom f)]
funs :: [Fun f]
equals :: forall f. Branch f -> [(Atom f, Atom f)]
less :: forall f. Branch f -> [(Atom f, Atom f)]
funs :: forall f. Branch f -> [Fun f]
..} =
    Doc -> Doc
braces forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
",") forall a b. (a -> b) -> a -> b
$
      [forall a. Pretty a => a -> Doc
pPrint Atom f
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"<" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint Atom f
y | (Atom f
x, Atom f
y) <- [(Atom f, Atom f)]
less ] forall a. [a] -> [a] -> [a]
++
      [forall a. Pretty a => a -> Doc
pPrint Atom f
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint Atom f
y | (Atom f
x, Atom f
y) <- [(Atom f, Atom f)]
equals ]

trueBranch :: Branch f
trueBranch :: forall f. Branch f
trueBranch = forall f.
[Fun f] -> [(Atom f, Atom f)] -> [(Atom f, Atom f)] -> Branch f
Branch [] [] []

norm :: Eq f => Branch f -> Atom f -> Atom f
norm :: forall f. Eq f => Branch f -> Atom f -> Atom f
norm Branch{[(Atom f, Atom f)]
[Fun f]
equals :: [(Atom f, Atom f)]
less :: [(Atom f, Atom f)]
funs :: [Fun f]
equals :: forall f. Branch f -> [(Atom f, Atom f)]
less :: forall f. Branch f -> [(Atom f, Atom f)]
funs :: forall f. Branch f -> [Fun f]
..} Atom f
x = forall a. a -> Maybe a -> a
fromMaybe Atom f
x (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Atom f
x [(Atom f, Atom f)]
equals)

contradictory :: (Minimal f, Ord f, Labelled f) => Branch f -> Bool
contradictory :: forall f. (Minimal f, Ord f, Labelled f) => Branch f -> Bool
contradictory Branch{[(Atom f, Atom f)]
[Fun f]
equals :: [(Atom f, Atom f)]
less :: [(Atom f, Atom f)]
funs :: [Fun f]
equals :: forall f. Branch f -> [(Atom f, Atom f)]
less :: forall f. Branch f -> [(Atom f, Atom f)]
funs :: forall f. Branch f -> [Fun f]
..} =
  forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Fun f
f forall a. Eq a => a -> a -> Bool
== forall f. Minimal f => Fun f
minimal | (Atom f
_, Constant Fun f
f) <- [(Atom f, Atom f)]
less] Bool -> Bool -> Bool
||
  forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Fun f
f forall a. Eq a => a -> a -> Bool
/= Fun f
g | (Constant Fun f
f, Constant Fun f
g) <- [(Atom f, Atom f)]
equals] Bool -> Bool -> Bool
||
  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall {vertex}. SCC vertex -> Bool
cyclic (forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp
    [(Atom f
x, Atom f
x, [Atom f
y | (Atom f
x', Atom f
y) <- [(Atom f, Atom f)]
less, Atom f
x forall a. Eq a => a -> a -> Bool
== Atom f
x']) | Atom f
x <- forall a. Ord a => [a] -> [a]
usort (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Atom f, Atom f)]
less)])
  where
    cyclic :: SCC vertex -> Bool
cyclic (AcyclicSCC vertex
_) = Bool
False
    cyclic (CyclicSCC [vertex]
_) = Bool
True

formAnd :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f] -> [Branch f]
formAnd :: forall f.
(Minimal f, Ordered f, Labelled f) =>
Formula f -> [Branch f] -> [Branch f]
formAnd Formula f
f [Branch f]
bs = forall a. Ord a => [a] -> [a]
usort ([Branch f]
bs forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {f}.
(Minimal f, Ordered f, Labelled f) =>
Formula f -> Branch f -> [Branch f]
add Formula f
f)
  where
    add :: Formula f -> Branch f -> [Branch f]
add (Less Atom f
t Atom f
u) Branch f
b = forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Atom f -> Branch f -> [Branch f]
addLess Atom f
t Atom f
u Branch f
b
    add (LessEq Atom f
t Atom f
u) Branch f
b = forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Atom f -> Branch f -> [Branch f]
addLess Atom f
t Atom f
u Branch f
b forall a. [a] -> [a] -> [a]
++ forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Atom f -> Branch f -> [Branch f]
addEquals Atom f
t Atom f
u Branch f
b
    add (And []) Branch f
b = [Branch f
b]
    add (And (Formula f
f:[Formula f]
fs)) Branch f
b = Formula f -> Branch f -> [Branch f]
add Formula f
f Branch f
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Formula f -> Branch f -> [Branch f]
add (forall f. [Formula f] -> Formula f
And [Formula f]
fs)
    add (Or [Formula f]
fs) Branch f
b = forall a. Ord a => [a] -> [a]
usort (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Formula f -> Branch f -> [Branch f]
add Formula f
f Branch f
b | Formula f
f <- [Formula f]
fs ])

branches :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f]
branches :: forall f.
(Minimal f, Ordered f, Labelled f) =>
Formula f -> [Branch f]
branches Formula f
x = forall {f}.
(Minimal f, Ordered f, Labelled f) =>
[Formula f] -> [Branch f]
aux [Formula f
x]
  where
    aux :: [Formula f] -> [Branch f]
aux [] = [forall f.
[Fun f] -> [(Atom f, Atom f)] -> [(Atom f, Atom f)] -> Branch f
Branch [] [] []]
    aux (And [Formula f]
xs:[Formula f]
ys) = [Formula f] -> [Branch f]
aux ([Formula f]
xs forall a. [a] -> [a] -> [a]
++ [Formula f]
ys)
    aux (Or [Formula f]
xs:[Formula f]
ys) = forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Formula f] -> [Branch f]
aux (Formula f
xforall a. a -> [a] -> [a]
:[Formula f]
ys) | Formula f
x <- [Formula f]
xs]
    aux (Less Atom f
t Atom f
u:[Formula f]
xs) = forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Atom f -> Branch f -> [Branch f]
addLess Atom f
t Atom f
u) ([Formula f] -> [Branch f]
aux [Formula f]
xs)
    aux (LessEq Atom f
t Atom f
u:[Formula f]
xs) =
      forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$
      forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Atom f -> Branch f -> [Branch f]
addLess Atom f
t Atom f
u) ([Formula f] -> [Branch f]
aux [Formula f]
xs) forall a. [a] -> [a] -> [a]
++
      forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Atom f -> Branch f -> [Branch f]
addEquals Atom f
u Atom f
t) ([Formula f] -> [Branch f]
aux [Formula f]
xs)

addLess :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]
addLess :: forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Atom f -> Branch f -> [Branch f]
addLess Atom f
_ (Constant Fun f
min) Branch f
_ | Fun f
min forall a. Eq a => a -> a -> Bool
== forall f. Minimal f => Fun f
minimal = []
addLess (Constant Fun f
min) Atom f
_ Branch f
b | Fun f
min forall a. Eq a => a -> a -> Bool
== forall f. Minimal f => Fun f
minimal = [Branch f
b]
addLess Atom f
t0 Atom f
u0 b :: Branch f
b@Branch{[(Atom f, Atom f)]
[Fun f]
equals :: [(Atom f, Atom f)]
less :: [(Atom f, Atom f)]
funs :: [Fun f]
equals :: forall f. Branch f -> [(Atom f, Atom f)]
less :: forall f. Branch f -> [(Atom f, Atom f)]
funs :: forall f. Branch f -> [Fun f]
..} =
  forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. (Minimal f, Ord f, Labelled f) => Branch f -> Bool
contradictory)
    [forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Branch f -> Branch f
addTerm Atom f
t (forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Branch f -> Branch f
addTerm Atom f
u Branch f
b{less :: [(Atom f, Atom f)]
less = forall a. Ord a => [a] -> [a]
usort ((Atom f
t, Atom f
u)forall a. a -> [a] -> [a]
:[(Atom f, Atom f)]
less)})]
  where
    t :: Atom f
t = forall f. Eq f => Branch f -> Atom f -> Atom f
norm Branch f
b Atom f
t0
    u :: Atom f
u = forall f. Eq f => Branch f -> Atom f -> Atom f
norm Branch f
b Atom f
u0

addEquals :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]
addEquals :: forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Atom f -> Branch f -> [Branch f]
addEquals Atom f
t0 Atom f
u0 b :: Branch f
b@Branch{[(Atom f, Atom f)]
[Fun f]
equals :: [(Atom f, Atom f)]
less :: [(Atom f, Atom f)]
funs :: [Fun f]
equals :: forall f. Branch f -> [(Atom f, Atom f)]
less :: forall f. Branch f -> [(Atom f, Atom f)]
funs :: forall f. Branch f -> [Fun f]
..}
  | Atom f
t forall a. Eq a => a -> a -> Bool
== Atom f
u Bool -> Bool -> Bool
|| (Atom f
t, Atom f
u) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Atom f, Atom f)]
equals = [Branch f
b]
  | Bool
otherwise =
    forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. (Minimal f, Ord f, Labelled f) => Branch f -> Bool
contradictory)
      [forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Branch f -> Branch f
addTerm Atom f
t (forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Branch f -> Branch f
addTerm Atom f
u Branch f
b {
         equals :: [(Atom f, Atom f)]
equals      = forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$ (Atom f
t, Atom f
u)forall a. a -> [a] -> [a]
:[(Atom f
x', Atom f
y') | (Atom f
x, Atom f
y) <- [(Atom f, Atom f)]
equals, let (Atom f
y', Atom f
x') = forall {b}. Ord b => (b, b) -> (b, b)
sort2 (Atom f -> Atom f
sub Atom f
x, Atom f -> Atom f
sub Atom f
y), Atom f
x' forall a. Eq a => a -> a -> Bool
/= Atom f
y'],
         less :: [(Atom f, Atom f)]
less        = forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$ [(Atom f -> Atom f
sub Atom f
x, Atom f -> Atom f
sub Atom f
y) | (Atom f
x, Atom f
y) <- [(Atom f, Atom f)]
less] })]
  where
    sort2 :: (b, b) -> (b, b)
sort2 (b
x, b
y) = (forall a. Ord a => a -> a -> a
min b
x b
y, forall a. Ord a => a -> a -> a
max b
x b
y)
    (Atom f
u, Atom f
t) = forall {b}. Ord b => (b, b) -> (b, b)
sort2 (forall f. Eq f => Branch f -> Atom f -> Atom f
norm Branch f
b Atom f
t0, forall f. Eq f => Branch f -> Atom f -> Atom f
norm Branch f
b Atom f
u0)

    sub :: Atom f -> Atom f
sub Atom f
x
      | Atom f
x forall a. Eq a => a -> a -> Bool
== Atom f
t = Atom f
u
      | Bool
otherwise = Atom f
x

addTerm :: (Minimal f, Ordered f, Labelled f) => Atom f -> Branch f -> Branch f
addTerm :: forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Branch f -> Branch f
addTerm (Constant Fun f
f) Branch f
b
  | Fun f
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall f. Branch f -> [Fun f]
funs Branch f
b =
    Branch f
b {
      funs :: [Fun f]
funs = Fun f
fforall a. a -> [a] -> [a]
:forall f. Branch f -> [Fun f]
funs Branch f
b,
      less :: [(Atom f, Atom f)]
less =
        forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$
          [ (forall f. Fun f -> Atom f
Constant Fun f
f, forall f. Fun f -> Atom f
Constant Fun f
g) | Fun f
g <- forall f. Branch f -> [Fun f]
funs Branch f
b, Fun f
f forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
g ] forall a. [a] -> [a] -> [a]
++
          [ (forall f. Fun f -> Atom f
Constant Fun f
g, forall f. Fun f -> Atom f
Constant Fun f
f) | Fun f
g <- forall f. Branch f -> [Fun f]
funs Branch f
b, Fun f
g forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
f ] forall a. [a] -> [a] -> [a]
++ forall f. Branch f -> [(Atom f, Atom f)]
less Branch f
b }
addTerm Atom f
_ Branch f
b = Branch f
b

newtype Model f = Model (Map (Atom f) (Int, Int))
  deriving (Model f -> Model f -> Bool
forall f. Model f -> Model f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Model f -> Model f -> Bool
$c/= :: forall f. Model f -> Model f -> Bool
== :: Model f -> Model f -> Bool
$c== :: forall f. Model f -> Model f -> Bool
Eq, Int -> Model f -> ShowS
forall f. (Labelled f, Show f) => Int -> Model f -> ShowS
forall f. (Labelled f, Show f) => [Model f] -> ShowS
forall f. (Labelled f, Show f) => Model f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Model f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Model f] -> ShowS
show :: Model f -> String
$cshow :: forall f. (Labelled f, Show f) => Model f -> String
showsPrec :: Int -> Model f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Model f -> ShowS
Show)
-- Representation: map from atom to (major, minor)
-- x <  y if major x < major y
-- x <= y if major x = major y and minor x < minor y

instance (Labelled f, PrettyTerm f) => Pretty (Model f) where
  pPrint :: Model f -> Doc
pPrint (Model Map (Atom f) (Int, Int)
m)
    | forall k a. Map k a -> Int
Map.size Map (Atom f) (Int, Int)
m forall a. Ord a => a -> a -> Bool
<= Int
1 = String -> Doc
text String
"empty"
    | Bool
otherwise = [Doc] -> Doc
fsep (forall {a} {a} {b}. (Pretty a, Eq a) => [(a, (a, b))] -> [Doc]
go (forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> b
snd) (forall k a. Map k a -> [(k, a)]
Map.toList Map (Atom f) (Int, Int)
m)))
      where
        go :: [(a, (a, b))] -> [Doc]
go [(a
x, (a, b)
_)] = [forall a. Pretty a => a -> Doc
pPrint a
x]
        go ((a
x, (a
i, b
_)):xs :: [(a, (a, b))]
xs@((a
_, (a
j, b
_)):[(a, (a, b))]
_)) =
          (forall a. Pretty a => a -> Doc
pPrint a
x Doc -> Doc -> Doc
<+> String -> Doc
text String
rel)forall a. a -> [a] -> [a]
:[(a, (a, b))] -> [Doc]
go [(a, (a, b))]
xs
          where
            rel :: String
rel = if a
i forall a. Eq a => a -> a -> Bool
== a
j then String
"<=" else String
"<"

modelToLiterals :: Model f -> [Formula f]
modelToLiterals :: forall f. Model f -> [Formula f]
modelToLiterals (Model Map (Atom f) (Int, Int)
m) = forall {a} {f} {b}. Eq a => [(Atom f, (a, b))] -> [Formula f]
go (forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> b
snd) (forall k a. Map k a -> [(k, a)]
Map.toList Map (Atom f) (Int, Int)
m))
  where
    go :: [(Atom f, (a, b))] -> [Formula f]
go []  = []
    go [(Atom f, (a, b))
_] = []
    go ((Atom f
x, (a
i, b
_)):xs :: [(Atom f, (a, b))]
xs@((Atom f
y, (a
j, b
_)):[(Atom f, (a, b))]
_)) =
      forall f. Atom f -> Atom f -> Formula f
rel Atom f
x Atom f
yforall a. a -> [a] -> [a]
:[(Atom f, (a, b))] -> [Formula f]
go [(Atom f, (a, b))]
xs
      where
        rel :: Atom f -> Atom f -> Formula f
rel = if a
i forall a. Eq a => a -> a -> Bool
== a
j then forall f. Atom f -> Atom f -> Formula f
LessEq else forall f. Atom f -> Atom f -> Formula f
Less

modelFromOrder :: (Minimal f, Ord f) => [Atom f] -> Model f
modelFromOrder :: forall f. (Minimal f, Ord f) => [Atom f] -> Model f
modelFromOrder [Atom f]
xs =
  forall f. Map (Atom f) (Int, Int) -> Model f
Model (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Atom f
x, (Int
i, Int
i)) | (Atom f
x, Int
i) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Atom f]
xs [Int
0..]])

weakenModel :: Model f -> [Model f]
weakenModel :: forall f. Model f -> [Model f]
weakenModel (Model Map (Atom f) (Int, Int)
m) =
  [ forall f. Map (Atom f) (Int, Int) -> Model f
Model (forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Atom f
x Map (Atom f) (Int, Int)
m) | Atom f
x <- forall k a. Map k a -> [k]
Map.keys Map (Atom f) (Int, Int)
m ] forall a. [a] -> [a] -> [a]
++
  [ forall f. Map (Atom f) (Int, Int) -> Model f
Model (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Atom f, (Int, Int))]
xs)
  | [(Atom f, (Int, Int))]
xs <- forall {a} {b} {a}.
(Ord a, Num b) =>
[(a, (a, b))] -> [[(a, (a, b))]]
glue (forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> b
snd) (forall k a. Map k a -> [(k, a)]
Map.toList Map (Atom f) (Int, Int)
m)),
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {f} {b}. [(Atom f, b)] -> Bool
ok (forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)) [(Atom f, (Int, Int))]
xs) ]
  where
    glue :: [(a, (a, b))] -> [[(a, (a, b))]]
glue [] = []
    glue [(a, (a, b))
_] = []
    glue (a :: (a, (a, b))
a@(a
_x, (a
i1, b
j1)):b :: (a, (a, b))
b@(a
y, (a
i2, b
_)):[(a, (a, b))]
xs) =
      [ ((a, (a, b))
aforall a. a -> [a] -> [a]
:(a
y, (a
i1, b
j1forall a. Num a => a -> a -> a
+b
1))forall a. a -> [a] -> [a]
:[(a, (a, b))]
xs) | a
i1 forall a. Ord a => a -> a -> Bool
< a
i2 ] forall a. [a] -> [a] -> [a]
++
      forall a b. (a -> b) -> [a] -> [b]
map ((a, (a, b))
aforall a. a -> [a] -> [a]
:) ([(a, (a, b))] -> [[(a, (a, b))]]
glue ((a, (a, b))
bforall a. a -> [a] -> [a]
:[(a, (a, b))]
xs))

    -- We must never make two constants equal
    ok :: [(Atom f, b)] -> Bool
ok [(Atom f, b)]
xs = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fun f
x | (Constant Fun f
x, b
_) <- [(Atom f, b)]
xs] forall a. Ord a => a -> a -> Bool
<= Int
1

varInModel :: (Minimal f, Ord f) => Model f -> Var -> Bool
varInModel :: forall f. (Minimal f, Ord f) => Model f -> Var -> Bool
varInModel (Model Map (Atom f) (Int, Int)
m) Var
x = forall f. Var -> Atom f
Variable Var
x forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map (Atom f) (Int, Int)
m

varGroups :: (Minimal f, Ord f) => Model f -> [(Fun f, [Var], Maybe (Fun f))]
varGroups :: forall f.
(Minimal f, Ord f) =>
Model f -> [(Fun f, [Var], Maybe (Fun f))]
varGroups (Model Map (Atom f) (Int, Int)
m) = forall a. (a -> Bool) -> [a] -> [a]
filter forall {a} {a} {c}. (a, [a], c) -> Bool
nonempty (forall {f}. Fun f -> [Atom f] -> [(Fun f, [Var], Maybe (Fun f))]
go forall f. Minimal f => Fun f
minimal (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> b
snd) (forall k a. Map k a -> [(k, a)]
Map.toList Map (Atom f) (Int, Int)
m))))
  where
    go :: Fun f -> [Atom f] -> [(Fun f, [Var], Maybe (Fun f))]
go Fun f
f [Atom f]
xs =
      case forall a. (a -> Bool) -> [a] -> ([a], [a])
span forall {f}. Atom f -> Bool
isVariable [Atom f]
xs of
        ([Atom f]
_, []) -> [(Fun f
f, forall a b. (a -> b) -> [a] -> [b]
map forall {f}. Atom f -> Var
unVariable [Atom f]
xs, forall a. Maybe a
Nothing)]
        ([Atom f]
ys, Constant Fun f
g:[Atom f]
zs) ->
          (Fun f
f, forall a b. (a -> b) -> [a] -> [b]
map forall {f}. Atom f -> Var
unVariable [Atom f]
ys, forall a. a -> Maybe a
Just Fun f
g)forall a. a -> [a] -> [a]
:Fun f -> [Atom f] -> [(Fun f, [Var], Maybe (Fun f))]
go Fun f
g [Atom f]
zs
    isVariable :: Atom f -> Bool
isVariable (Constant Fun f
_) = Bool
False
    isVariable (Variable Var
_) = Bool
True
    unVariable :: Atom f -> Var
unVariable (Variable Var
x) = Var
x
    nonempty :: (a, [a], c) -> Bool
nonempty (a
_, [], c
_) = Bool
False
    nonempty (a, [a], c)
_ = Bool
True

class Minimal f where
  minimal :: Fun f

{-# INLINE lessEqInModel #-}
lessEqInModel :: (Minimal f, Ordered f, Labelled f) => Model f -> Atom f -> Atom f -> Maybe Strictness
lessEqInModel :: forall f.
(Minimal f, Ordered f, Labelled f) =>
Model f -> Atom f -> Atom f -> Maybe Strictness
lessEqInModel (Model Map (Atom f) (Int, Int)
m) Atom f
x Atom f
y
  | Just (Int
a, Int
_) <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Atom f
x Map (Atom f) (Int, Int)
m,
    Just (Int
b, Int
_) <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Atom f
y Map (Atom f) (Int, Int)
m,
    Int
a forall a. Ord a => a -> a -> Bool
< Int
b = forall a. a -> Maybe a
Just Strictness
Strict
  | Just (Int, Int)
a <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Atom f
x Map (Atom f) (Int, Int)
m,
    Just (Int, Int)
b <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Atom f
y Map (Atom f) (Int, Int)
m,
    (Int, Int)
a forall a. Ord a => a -> a -> Bool
< (Int, Int)
b = forall a. a -> Maybe a
Just Strictness
Nonstrict
  | Atom f
x forall a. Eq a => a -> a -> Bool
== Atom f
y = forall a. a -> Maybe a
Just Strictness
Nonstrict
  | Constant Fun f
a <- Atom f
x, Constant Fun f
b <- Atom f
y, Fun f
a forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
b = forall a. a -> Maybe a
Just Strictness
Strict
  | Constant Fun f
a <- Atom f
x, Fun f
a forall a. Eq a => a -> a -> Bool
== forall f. Minimal f => Fun f
minimal = forall a. a -> Maybe a
Just Strictness
Nonstrict
  | Bool
otherwise = forall a. Maybe a
Nothing

solve :: (Minimal f, Ordered f, PrettyTerm f, Labelled f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)
solve :: forall f.
(Minimal f, Ordered f, PrettyTerm f, Labelled f) =>
[Atom f] -> Branch f -> Either (Model f) (Subst f)
solve [Atom f]
xs branch :: Branch f
branch@Branch{[(Atom f, Atom f)]
[Fun f]
equals :: [(Atom f, Atom f)]
less :: [(Atom f, Atom f)]
funs :: [Fun f]
equals :: forall f. Branch f -> [(Atom f, Atom f)]
less :: forall f. Branch f -> [(Atom f, Atom f)]
funs :: forall f. Branch f -> [Fun f]
..}
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Atom f, Atom f)]
equals Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Atom f, Atom f) -> Bool
true [(Atom f, Atom f)]
less) =
    forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Model " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Model f
model forall a. [a] -> [a] -> [a]
++ String
" is not a model of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Branch f
branch forall a. [a] -> [a] -> [a]
++ String
" (edges = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [(Atom f, Atom f, [Atom f])]
edges forall a. [a] -> [a] -> [a]
++ String
", vs = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Atom f]
vs forall a. [a] -> [a] -> [a]
++ String
")"
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Atom f, Atom f)]
equals = forall a b. a -> Either a b
Left Model f
model
  | Bool
otherwise = forall a b. b -> Either a b
Right Subst f
sub
    where
      sub :: Subst f
sub = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
undefined forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst forall a b. (a -> b) -> a -> b
$
        [(Var
x, forall f. Atom f -> Term f
toTerm Atom f
y) | (Variable Var
x, Atom f
y) <- [(Atom f, Atom f)]
equals] forall a. [a] -> [a] -> [a]
++
        [(Var
y, forall f. Atom f -> Term f
toTerm Atom f
x) | (x :: Atom f
x@Constant{}, Variable Var
y) <- [(Atom f, Atom f)]
equals]
      vs :: [Atom f]
vs = forall f. Fun f -> Atom f
Constant forall f. Minimal f => Fun f
minimalforall a. a -> [a] -> [a]
:forall a. [a] -> [a]
reverse (forall a. [SCC a] -> [a]
flattenSCCs (forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp [(Atom f, Atom f, [Atom f])]
edges))
      edges :: [(Atom f, Atom f, [Atom f])]
edges = [(Atom f
x, Atom f
x, [Atom f
y | (Atom f
x', Atom f
y) <- [(Atom f, Atom f)]
less', Atom f
x forall a. Eq a => a -> a -> Bool
== Atom f
x']) | Atom f
x <- [Atom f]
as, Atom f
x forall a. Eq a => a -> a -> Bool
/= forall f. Fun f -> Atom f
Constant forall f. Minimal f => Fun f
minimal]
      less' :: [(Atom f, Atom f)]
less' = [(Atom f, Atom f)]
less forall a. [a] -> [a] -> [a]
++ [(forall f. Fun f -> Atom f
Constant Fun f
x, forall f. Fun f -> Atom f
Constant Fun f
y) | Constant Fun f
x <- [Atom f]
as, Constant Fun f
y <- [Atom f]
as, Fun f
x forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
y]
      as :: [Atom f]
as = forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$ [Atom f]
xs forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Atom f, Atom f)]
less forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Atom f, Atom f)]
less
      model :: Model f
model = forall f. (Minimal f, Ord f) => [Atom f] -> Model f
modelFromOrder [Atom f]
vs
      true :: (Atom f, Atom f) -> Bool
true (Atom f
t, Atom f
u) = forall f.
(Minimal f, Ordered f, Labelled f) =>
Model f -> Atom f -> Atom f -> Maybe Strictness
lessEqInModel Model f
model Atom f
t Atom f
u forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Strictness
Strict

class Ord f => Ordered f where
  -- | Return 'True' if the first term is less than or equal to the second,
  -- in the term ordering.
  lessEq :: Term f -> Term f -> Bool
  -- | Check if the first term is less than or equal to the second in the given model,
  -- and decide whether the inequality is strict or nonstrict.
  lessIn :: Model f -> Term f -> Term f -> Maybe Strictness
  lessEqSkolem :: Term f -> Term f -> Bool

-- | Describes whether an inequality is strict or nonstrict.
data Strictness =
    -- | The first term is strictly less than the second.
    Strict
    -- | The first term is less than or equal to the second.
  | Nonstrict deriving (Strictness -> Strictness -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Strictness -> Strictness -> Bool
$c/= :: Strictness -> Strictness -> Bool
== :: Strictness -> Strictness -> Bool
$c== :: Strictness -> Strictness -> Bool
Eq, Int -> Strictness -> ShowS
[Strictness] -> ShowS
Strictness -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Strictness] -> ShowS
$cshowList :: [Strictness] -> ShowS
show :: Strictness -> String
$cshow :: Strictness -> String
showsPrec :: Int -> Strictness -> ShowS
$cshowsPrec :: Int -> Strictness -> ShowS
Show)

-- | Return 'True' if the first argument is strictly less than the second,
-- in the term ordering.
lessThan :: Ordered f => Term f -> Term f -> Bool
lessThan :: forall f. Ordered f => Term f -> Term f -> Bool
lessThan Term f
t Term f
u = forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
t Term f
u Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (forall f. Term f -> Term f -> Maybe (Subst f)
unify Term f
t Term f
u)

-- | Return the direction in which the terms are oriented according to the term
-- ordering, or 'Nothing' if they cannot be oriented. A result of @'Just' 'LT'@
-- means that the first term is less than /or equal to/ the second.
orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering
orientTerms :: forall f. Ordered f => Term f -> Term f -> Maybe Ordering
orientTerms Term f
t Term f
u
  | Term f
t forall a. Eq a => a -> a -> Bool
== Term f
u = forall a. a -> Maybe a
Just Ordering
EQ
  | forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
t Term f
u = forall a. a -> Maybe a
Just Ordering
LT
  | forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
u Term f
t = forall a. a -> Maybe a
Just Ordering
GT
  | Bool
otherwise = forall a. Maybe a
Nothing