{-# LANGUAGE FlexibleContexts, UndecidableInstances, RecordWildCards #-}
module Twee.Constraints where
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 =
Branch {
forall f. Branch f -> [Fun f]
funs :: [Fun f],
forall f. Branch f -> [(Atom f, Atom f)]
less :: [(Atom f, Atom f)],
forall f. Branch f -> [(Atom f, Atom f)]
equals :: [(Atom f, Atom f)] }
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)
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))
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
lessEq :: Term f -> Term f -> Bool
lessIn :: Model f -> Term f -> Term f -> Maybe Strictness
lessEqSkolem :: Term f -> Term f -> Bool
data Strictness =
Strict
| 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)
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)
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