{-# 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
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
[Atom f] -> ShowS
Atom f -> String
(Int -> Atom f -> ShowS)
-> (Atom f -> String) -> ([Atom f] -> ShowS) -> Show (Atom f)
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
(Atom f -> Atom f -> Bool)
-> (Atom f -> Atom f -> Bool) -> Eq (Atom f)
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, Eq (Atom f)
Eq (Atom f)
-> (Atom f -> Atom f -> Ordering)
-> (Atom f -> Atom f -> Bool)
-> (Atom f -> Atom f -> Bool)
-> (Atom f -> Atom f -> Bool)
-> (Atom f -> Atom f -> Bool)
-> (Atom f -> Atom f -> Atom f)
-> (Atom f -> Atom f -> Atom f)
-> Ord (Atom f)
Atom f -> Atom f -> Bool
Atom f -> Atom f -> Ordering
Atom f -> Atom f -> Atom f
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
$cp1Ord :: forall f. Eq (Atom f)
Ord)

{-# INLINE atoms #-}
atoms :: Term f -> [Atom f]
atoms :: Term f -> [Atom f]
atoms Term f
t = TermList f -> [Atom f]
forall f. TermList f -> [Atom f]
aux (Term f -> TermList f
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) = Fun f -> Atom f
forall f. Fun f -> Atom f
Constant Fun f
fAtom f -> [Atom f] -> [Atom f]
forall a. a -> [a] -> [a]
:TermList f -> [Atom f]
aux TermList f
t
    aux (Cons (Var Var
x) TermList f
t) = Var -> Atom f
forall f. Var -> Atom f
Variable Var
xAtom f -> [Atom f] -> [Atom f]
forall 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 :: Atom f -> Term f
toTerm (Constant Fun f
f) = Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Fun f -> Builder f
forall f. Fun f -> Builder f
con Fun f
f)
toTerm (Variable Var
x) = Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Var -> Builder f
forall f. Var -> Builder f
var Var
x)

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

instance (Labelled f, PrettyTerm f) => Pretty (Atom f) where
  pPrint :: Atom f -> Doc
pPrint = Term f -> Doc
forall a. Pretty a => a -> Doc
pPrint (Term f -> Doc) -> (Atom f -> Term f) -> Atom f -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom f -> Term f
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
(Formula f -> Formula f -> Bool)
-> (Formula f -> Formula f -> Bool) -> Eq (Formula f)
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, Eq (Formula f)
Eq (Formula f)
-> (Formula f -> Formula f -> Ordering)
-> (Formula f -> Formula f -> Bool)
-> (Formula f -> Formula f -> Bool)
-> (Formula f -> Formula f -> Bool)
-> (Formula f -> Formula f -> Bool)
-> (Formula f -> Formula f -> Formula f)
-> (Formula f -> Formula f -> Formula f)
-> Ord (Formula f)
Formula f -> Formula f -> Bool
Formula f -> Formula f -> Ordering
Formula f -> Formula f -> Formula f
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
$cp1Ord :: forall f. Eq (Formula f)
Ord, Int -> Formula f -> ShowS
[Formula f] -> ShowS
Formula f -> String
(Int -> Formula f -> ShowS)
-> (Formula f -> String)
-> ([Formula f] -> ShowS)
-> Show (Formula f)
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 (Atom f -> Doc
forall a. Pretty a => a -> Doc
pPrint Atom f
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"<") Int
2 (Atom f -> Doc
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 (Atom f -> Doc
forall a. Pretty a => a -> Doc
pPrint Atom f
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"<=") Int
2 (Atom f -> Doc
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 Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
10)
      ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
" &") ([Doc] -> [Doc]
nest_ ((Formula f -> Doc) -> [Formula f] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (PrettyLevel -> Rational -> Formula f -> Doc
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
xDoc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:(Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2) [Doc]
xs
      nest_ [] = [Doc]
forall a. HasCallStack => a
undefined
  pPrintPrec PrettyLevel
l Rational
p (Or [Formula f]
xs) =
    Bool -> Doc -> Doc
maybeParens (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
10)
      ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
" |") ([Doc] -> [Doc]
nest_ ((Formula f -> Doc) -> [Formula f] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (PrettyLevel -> Rational -> Formula f -> Doc
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
xDoc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:(Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2) [Doc]
xs
      nest_ [] = [Doc]
forall a. HasCallStack => a
undefined

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

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

Formula f
x &&& :: Formula f -> Formula f -> Formula f
&&& Formula f
y = [Formula f] -> Formula f
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 = [Formula f] -> Formula f
forall (t :: * -> *) f. Foldable t => t (Formula f) -> Formula f
disj [Formula f
x, Formula f
y]
true :: Formula f
true  = [Formula f] -> Formula f
forall f. [Formula f] -> Formula f
And []
false :: Formula f
false = [Formula f] -> Formula f
forall f. [Formula f] -> Formula f
Or []

data Branch f =
  -- Branches are kept normalised wrt equals
  Branch {
    Branch f -> [Fun f]
funs        :: [Fun f],
    Branch f -> [(Atom f, Atom f)]
less        :: [(Atom f, Atom f)],  -- sorted
    Branch f -> [(Atom f, Atom f)]
equals      :: [(Atom f, Atom f)] } -- sorted, greatest atom first in each pair
  deriving (Branch f -> Branch f -> Bool
(Branch f -> Branch f -> Bool)
-> (Branch f -> Branch f -> Bool) -> Eq (Branch f)
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, Eq (Branch f)
Eq (Branch f)
-> (Branch f -> Branch f -> Ordering)
-> (Branch f -> Branch f -> Bool)
-> (Branch f -> Branch f -> Bool)
-> (Branch f -> Branch f -> Bool)
-> (Branch f -> Branch f -> Bool)
-> (Branch f -> Branch f -> Branch f)
-> (Branch f -> Branch f -> Branch f)
-> Ord (Branch f)
Branch f -> Branch f -> Bool
Branch f -> Branch f -> Ordering
Branch f -> Branch f -> Branch f
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
$cp1Ord :: forall f. Eq (Branch f)
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 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
",") ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
      [Atom f -> Doc
forall a. Pretty a => a -> Doc
pPrint Atom f
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"<" Doc -> Doc -> Doc
<+> Atom f -> Doc
forall a. Pretty a => a -> Doc
pPrint Atom f
y | (Atom f
x, Atom f
y) <- [(Atom f, Atom f)]
less ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
      [Atom f -> Doc
forall a. Pretty a => a -> Doc
pPrint Atom f
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> Atom f -> 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 :: Branch f
trueBranch = [Fun f] -> [(Atom f, Atom f)] -> [(Atom f, Atom f)] -> Branch f
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 :: 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 = Atom f -> Maybe (Atom f) -> Atom f
forall a. a -> Maybe a -> a
fromMaybe Atom f
x (Atom f -> [(Atom f, Atom f)] -> Maybe (Atom f)
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 :: 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]
..} =
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
forall f. Minimal f => Fun f
minimal | (Atom f
_, Constant Fun f
f) <- [(Atom f, Atom f)]
less] Bool -> Bool -> Bool
||
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Fun f
f Fun f -> Fun f -> Bool
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
||
  (SCC (Atom f) -> Bool) -> [SCC (Atom f)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SCC (Atom f) -> Bool
forall vertex. SCC vertex -> Bool
cyclic ([(Atom f, Atom f, [Atom f])] -> [SCC (Atom f)]
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 Atom f -> Atom f -> Bool
forall a. Eq a => a -> a -> Bool
== Atom f
x']) | Atom f
x <- [Atom f] -> [Atom f]
forall a. Ord a => [a] -> [a]
usort (((Atom f, Atom f) -> Atom f) -> [(Atom f, Atom f)] -> [Atom f]
forall a b. (a -> b) -> [a] -> [b]
map (Atom f, Atom f) -> Atom f
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 :: Formula f -> [Branch f] -> [Branch f]
formAnd Formula f
f [Branch f]
bs = [Branch f] -> [Branch f]
forall a. Ord a => [a] -> [a]
usort ([Branch f]
bs [Branch f] -> (Branch f -> [Branch f]) -> [Branch f]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Formula f -> Branch f -> [Branch f]
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 = Atom f -> Atom f -> Branch f -> [Branch f]
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 = Atom f -> Atom f -> Branch f -> [Branch f]
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 [Branch f] -> [Branch f] -> [Branch f]
forall a. [a] -> [a] -> [a]
++ Atom f -> Atom f -> Branch f -> [Branch f]
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 [Branch f] -> (Branch f -> [Branch f]) -> [Branch f]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Formula f -> Branch f -> [Branch f]
add ([Formula f] -> Formula f
forall f. [Formula f] -> Formula f
And [Formula f]
fs)
    add (Or [Formula f]
fs) Branch f
b = [Branch f] -> [Branch f]
forall a. Ord a => [a] -> [a]
usort ([[Branch f]] -> [Branch f]
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 :: Formula f -> [Branch f]
branches Formula f
x = [Formula f] -> [Branch f]
forall f.
(Minimal f, Ordered f, Labelled f) =>
[Formula f] -> [Branch f]
aux [Formula f
x]
  where
    aux :: [Formula f] -> [Branch f]
aux [] = [[Fun f] -> [(Atom f, Atom f)] -> [(Atom f, Atom f)] -> Branch f
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 [Formula f] -> [Formula f] -> [Formula f]
forall a. [a] -> [a] -> [a]
++ [Formula f]
ys)
    aux (Or [Formula f]
xs:[Formula f]
ys) = [Branch f] -> [Branch f]
forall a. Ord a => [a] -> [a]
usort ([Branch f] -> [Branch f]) -> [Branch f] -> [Branch f]
forall a b. (a -> b) -> a -> b
$ [[Branch f]] -> [Branch f]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Formula f] -> [Branch f]
aux (Formula f
xFormula f -> [Formula f] -> [Formula f]
forall a. a -> [a] -> [a]
:[Formula f]
ys) | Formula f
x <- [Formula f]
xs]
    aux (Less Atom f
t Atom f
u:[Formula f]
xs) = [Branch f] -> [Branch f]
forall a. Ord a => [a] -> [a]
usort ([Branch f] -> [Branch f]) -> [Branch f] -> [Branch f]
forall a b. (a -> b) -> a -> b
$ (Branch f -> [Branch f]) -> [Branch f] -> [Branch f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Atom f -> Atom f -> Branch f -> [Branch f]
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) =
      [Branch f] -> [Branch f]
forall a. Ord a => [a] -> [a]
usort ([Branch f] -> [Branch f]) -> [Branch f] -> [Branch f]
forall a b. (a -> b) -> a -> b
$
      (Branch f -> [Branch f]) -> [Branch f] -> [Branch f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Atom f -> Atom f -> Branch f -> [Branch f]
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) [Branch f] -> [Branch f] -> [Branch f]
forall a. [a] -> [a] -> [a]
++
      (Branch f -> [Branch f]) -> [Branch f] -> [Branch f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Atom f -> Atom f -> Branch f -> [Branch f]
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 :: Atom f -> Atom f -> Branch f -> [Branch f]
addLess Atom f
_ (Constant Fun f
min) Branch f
_ | Fun f
min Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
forall f. Minimal f => Fun f
minimal = []
addLess (Constant Fun f
min) Atom f
_ Branch f
b | Fun f
min Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
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]
..} =
  (Branch f -> Bool) -> [Branch f] -> [Branch f]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Branch f -> Bool) -> Branch f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Branch f -> Bool
forall f. (Minimal f, Ord f, Labelled f) => Branch f -> Bool
contradictory)
    [Atom f -> Branch f -> Branch f
forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Branch f -> Branch f
addTerm Atom f
t (Atom f -> Branch f -> Branch f
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 = [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a. Ord a => [a] -> [a]
usort ((Atom f
t, Atom f
u)(Atom f, Atom f) -> [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a. a -> [a] -> [a]
:[(Atom f, Atom f)]
less)})]
  where
    t :: Atom f
t = Branch f -> Atom f -> Atom f
forall f. Eq f => Branch f -> Atom f -> Atom f
norm Branch f
b Atom f
t0
    u :: Atom f
u = Branch f -> Atom f -> Atom f
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 :: 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 Atom f -> Atom f -> Bool
forall a. Eq a => a -> a -> Bool
== Atom f
u Bool -> Bool -> Bool
|| (Atom f
t, Atom f
u) (Atom f, Atom f) -> [(Atom f, Atom f)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Atom f, Atom f)]
equals = [Branch f
b]
  | Bool
otherwise =
    (Branch f -> Bool) -> [Branch f] -> [Branch f]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Branch f -> Bool) -> Branch f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Branch f -> Bool
forall f. (Minimal f, Ord f, Labelled f) => Branch f -> Bool
contradictory)
      [Atom f -> Branch f -> Branch f
forall f.
(Minimal f, Ordered f, Labelled f) =>
Atom f -> Branch f -> Branch f
addTerm Atom f
t (Atom f -> Branch f -> Branch f
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      = [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a. Ord a => [a] -> [a]
usort ([(Atom f, Atom f)] -> [(Atom f, Atom f)])
-> [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a b. (a -> b) -> a -> b
$ (Atom f
t, Atom f
u)(Atom f, Atom f) -> [(Atom f, Atom f)] -> [(Atom f, Atom f)]
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') = (Atom f, Atom f) -> (Atom f, Atom f)
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' Atom f -> Atom f -> Bool
forall a. Eq a => a -> a -> Bool
/= Atom f
y'],
         less :: [(Atom f, Atom f)]
less        = [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a. Ord a => [a] -> [a]
usort ([(Atom f, Atom f)] -> [(Atom f, Atom f)])
-> [(Atom f, Atom f)] -> [(Atom f, Atom f)]
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) = (b -> b -> b
forall a. Ord a => a -> a -> a
min b
x b
y, b -> b -> b
forall a. Ord a => a -> a -> a
max b
x b
y)
    (Atom f
u, Atom f
t) = (Atom f, Atom f) -> (Atom f, Atom f)
forall b. Ord b => (b, b) -> (b, b)
sort2 (Branch f -> Atom f -> Atom f
forall f. Eq f => Branch f -> Atom f -> Atom f
norm Branch f
b Atom f
t0, Branch f -> Atom f -> Atom f
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 Atom f -> Atom f -> Bool
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 :: Atom f -> Branch f -> Branch f
addTerm (Constant Fun f
f) Branch f
b
  | Fun f
f Fun f -> [Fun f] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Branch f -> [Fun f]
forall f. Branch f -> [Fun f]
funs Branch f
b =
    Branch f
b {
      funs :: [Fun f]
funs = Fun f
fFun f -> [Fun f] -> [Fun f]
forall a. a -> [a] -> [a]
:Branch f -> [Fun f]
forall f. Branch f -> [Fun f]
funs Branch f
b,
      less :: [(Atom f, Atom f)]
less =
        [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a. Ord a => [a] -> [a]
usort ([(Atom f, Atom f)] -> [(Atom f, Atom f)])
-> [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a b. (a -> b) -> a -> b
$
          [ (Fun f -> Atom f
forall f. Fun f -> Atom f
Constant Fun f
f, Fun f -> Atom f
forall f. Fun f -> Atom f
Constant Fun f
g) | Fun f
g <- Branch f -> [Fun f]
forall f. Branch f -> [Fun f]
funs Branch f
b, Fun f
f Fun f -> Fun f -> Bool
forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
g ] [(Atom f, Atom f)] -> [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a. [a] -> [a] -> [a]
++
          [ (Fun f -> Atom f
forall f. Fun f -> Atom f
Constant Fun f
g, Fun f -> Atom f
forall f. Fun f -> Atom f
Constant Fun f
f) | Fun f
g <- Branch f -> [Fun f]
forall f. Branch f -> [Fun f]
funs Branch f
b, Fun f
g Fun f -> Fun f -> Bool
forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
f ] [(Atom f, Atom f)] -> [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a. [a] -> [a] -> [a]
++ Branch f -> [(Atom f, Atom f)]
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
(Model f -> Model f -> Bool)
-> (Model f -> Model f -> Bool) -> Eq (Model f)
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
[Model f] -> ShowS
Model f -> String
(Int -> Model f -> ShowS)
-> (Model f -> String) -> ([Model f] -> ShowS) -> Show (Model f)
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)
    | Map (Atom f) (Int, Int) -> Int
forall k a. Map k a -> Int
Map.size Map (Atom f) (Int, Int)
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = String -> Doc
text String
"empty"
    | Bool
otherwise = [Doc] -> Doc
fsep ([(Atom f, (Int, Int))] -> [Doc]
forall a a b. (Pretty a, Eq a) => [(a, (a, b))] -> [Doc]
go (((Atom f, (Int, Int)) -> (Atom f, (Int, Int)) -> Ordering)
-> [(Atom f, (Int, Int))] -> [(Atom f, (Int, Int))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Atom f, (Int, Int)) -> (Int, Int))
-> (Atom f, (Int, Int)) -> (Atom f, (Int, Int)) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Atom f, (Int, Int)) -> (Int, Int)
forall a b. (a, b) -> b
snd) (Map (Atom f) (Int, Int) -> [(Atom f, (Int, Int))]
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)
_)] = [a -> Doc
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))]
_)) =
          (a -> Doc
forall a. Pretty a => a -> Doc
pPrint a
x Doc -> Doc -> Doc
<+> String -> Doc
text String
rel)Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:[(a, (a, b))] -> [Doc]
go [(a, (a, b))]
xs
          where
            rel :: String
rel = if a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j then String
"<=" else String
"<"

modelToLiterals :: Model f -> [Formula f]
modelToLiterals :: Model f -> [Formula f]
modelToLiterals (Model Map (Atom f) (Int, Int)
m) = [(Atom f, (Int, Int))] -> [Formula f]
forall a f b. Eq a => [(Atom f, (a, b))] -> [Formula f]
go (((Atom f, (Int, Int)) -> (Atom f, (Int, Int)) -> Ordering)
-> [(Atom f, (Int, Int))] -> [(Atom f, (Int, Int))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Atom f, (Int, Int)) -> (Int, Int))
-> (Atom f, (Int, Int)) -> (Atom f, (Int, Int)) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Atom f, (Int, Int)) -> (Int, Int)
forall a b. (a, b) -> b
snd) (Map (Atom f) (Int, Int) -> [(Atom f, (Int, Int))]
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))]
_)) =
      Atom f -> Atom f -> Formula f
forall f. Atom f -> Atom f -> Formula f
rel Atom f
x Atom f
yFormula f -> [Formula f] -> [Formula f]
forall 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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j then Atom f -> Atom f -> Formula f
forall f. Atom f -> Atom f -> Formula f
LessEq else Atom f -> Atom f -> Formula f
forall f. Atom f -> Atom f -> Formula f
Less

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

weakenModel :: Model f -> [Model f]
weakenModel :: Model f -> [Model f]
weakenModel (Model Map (Atom f) (Int, Int)
m) =
  [ Map (Atom f) (Int, Int) -> Model f
forall f. Map (Atom f) (Int, Int) -> Model f
Model (Atom f -> Map (Atom f) (Int, Int) -> Map (Atom f) (Int, Int)
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 <- Map (Atom f) (Int, Int) -> [Atom f]
forall k a. Map k a -> [k]
Map.keys Map (Atom f) (Int, Int)
m ] [Model f] -> [Model f] -> [Model f]
forall a. [a] -> [a] -> [a]
++
  [ Map (Atom f) (Int, Int) -> Model f
forall f. Map (Atom f) (Int, Int) -> Model f
Model ([(Atom f, (Int, Int))] -> Map (Atom f) (Int, Int)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Atom f, (Int, Int))]
xs)
  | [(Atom f, (Int, Int))]
xs <- [(Atom f, (Int, Int))] -> [[(Atom f, (Int, Int))]]
forall a b a. (Ord a, Num b) => [(a, (a, b))] -> [[(a, (a, b))]]
glue (((Atom f, (Int, Int)) -> (Atom f, (Int, Int)) -> Ordering)
-> [(Atom f, (Int, Int))] -> [(Atom f, (Int, Int))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Atom f, (Int, Int)) -> (Int, Int))
-> (Atom f, (Int, Int)) -> (Atom f, (Int, Int)) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Atom f, (Int, Int)) -> (Int, Int)
forall a b. (a, b) -> b
snd) (Map (Atom f) (Int, Int) -> [(Atom f, (Int, Int))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Atom f) (Int, Int)
m)),
    ([(Atom f, (Int, Int))] -> Bool)
-> [[(Atom f, (Int, Int))]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all [(Atom f, (Int, Int))] -> Bool
forall f b. [(Atom f, b)] -> Bool
ok (((Atom f, (Int, Int)) -> (Atom f, (Int, Int)) -> Bool)
-> [(Atom f, (Int, Int))] -> [[(Atom f, (Int, Int))]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Int -> Int -> Bool)
-> ((Atom f, (Int, Int)) -> Int)
-> (Atom f, (Int, Int))
-> (Atom f, (Int, Int))
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ((Int, Int) -> Int
forall a b. (a, b) -> a
fst ((Int, Int) -> Int)
-> ((Atom f, (Int, Int)) -> (Int, Int))
-> (Atom f, (Int, Int))
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Atom f, (Int, Int)) -> (Int, Int)
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))
a(a, (a, b)) -> [(a, (a, b))] -> [(a, (a, b))]
forall a. a -> [a] -> [a]
:(a
y, (a
i1, b
j1b -> b -> b
forall a. Num a => a -> a -> a
+b
1))(a, (a, b)) -> [(a, (a, b))] -> [(a, (a, b))]
forall a. a -> [a] -> [a]
:[(a, (a, b))]
xs) | a
i1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
i2 ] [[(a, (a, b))]] -> [[(a, (a, b))]] -> [[(a, (a, b))]]
forall a. [a] -> [a] -> [a]
++
      ([(a, (a, b))] -> [(a, (a, b))])
-> [[(a, (a, b))]] -> [[(a, (a, b))]]
forall a b. (a -> b) -> [a] -> [b]
map ((a, (a, b))
a(a, (a, b)) -> [(a, (a, b))] -> [(a, (a, b))]
forall a. a -> [a] -> [a]
:) ([(a, (a, b))] -> [[(a, (a, b))]]
glue ((a, (a, b))
b(a, (a, b)) -> [(a, (a, b))] -> [(a, (a, b))]
forall 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 = [Fun f] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Fun f
x | (Constant Fun f
x, b
_) <- [(Atom f, b)]
xs] Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1

varInModel :: (Minimal f, Ord f) => Model f -> Var -> Bool
varInModel :: Model f -> Var -> Bool
varInModel (Model Map (Atom f) (Int, Int)
m) Var
x = Var -> Atom f
forall f. Var -> Atom f
Variable Var
x Atom f -> Map (Atom f) (Int, Int) -> Bool
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 :: Model f -> [(Fun f, [Var], Maybe (Fun f))]
varGroups (Model Map (Atom f) (Int, Int)
m) = ((Fun f, [Var], Maybe (Fun f)) -> Bool)
-> [(Fun f, [Var], Maybe (Fun f))]
-> [(Fun f, [Var], Maybe (Fun f))]
forall a. (a -> Bool) -> [a] -> [a]
filter (Fun f, [Var], Maybe (Fun f)) -> Bool
forall a a c. (a, [a], c) -> Bool
nonempty (Fun f -> [Atom f] -> [(Fun f, [Var], Maybe (Fun f))]
forall f. Fun f -> [Atom f] -> [(Fun f, [Var], Maybe (Fun f))]
go Fun f
forall f. Minimal f => Fun f
minimal (((Atom f, (Int, Int)) -> Atom f)
-> [(Atom f, (Int, Int))] -> [Atom f]
forall a b. (a -> b) -> [a] -> [b]
map (Atom f, (Int, Int)) -> Atom f
forall a b. (a, b) -> a
fst (((Atom f, (Int, Int)) -> (Atom f, (Int, Int)) -> Ordering)
-> [(Atom f, (Int, Int))] -> [(Atom f, (Int, Int))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Atom f, (Int, Int)) -> (Int, Int))
-> (Atom f, (Int, Int)) -> (Atom f, (Int, Int)) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Atom f, (Int, Int)) -> (Int, Int)
forall a b. (a, b) -> b
snd) (Map (Atom f) (Int, Int) -> [(Atom f, (Int, Int))]
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 (Atom f -> Bool) -> [Atom f] -> ([Atom f], [Atom f])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Atom f -> Bool
forall f. Atom f -> Bool
isVariable [Atom f]
xs of
        ([Atom f]
_, []) -> [(Fun f
f, (Atom f -> Var) -> [Atom f] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Atom f -> Var
forall f. Atom f -> Var
unVariable [Atom f]
xs, Maybe (Fun f)
forall a. Maybe a
Nothing)]
        ([Atom f]
ys, Constant Fun f
g:[Atom f]
zs) ->
          (Fun f
f, (Atom f -> Var) -> [Atom f] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Atom f -> Var
forall f. Atom f -> Var
unVariable [Atom f]
ys, Fun f -> Maybe (Fun f)
forall a. a -> Maybe a
Just Fun f
g)(Fun f, [Var], Maybe (Fun f))
-> [(Fun f, [Var], Maybe (Fun f))]
-> [(Fun f, [Var], Maybe (Fun f))]
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 :: 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
_) <- Atom f -> Map (Atom f) (Int, Int) -> Maybe (Int, 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
_) <- Atom f -> Map (Atom f) (Int, Int) -> Maybe (Int, 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
b = Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Strict
  | Just (Int, Int)
a <- Atom f -> Map (Atom f) (Int, Int) -> Maybe (Int, 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, Int)
b <- Atom f -> Map (Atom f) (Int, Int) -> Maybe (Int, Int)
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 (Int, Int) -> (Int, Int) -> Bool
forall a. Ord a => a -> a -> Bool
< (Int, Int)
b = Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Nonstrict
  | Atom f
x Atom f -> Atom f -> Bool
forall a. Eq a => a -> a -> Bool
== Atom f
y = Strictness -> Maybe Strictness
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 Fun f -> Fun f -> Bool
forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
b = Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Strict
  | Constant Fun f
a <- Atom f
x, Fun f
a Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
forall f. Minimal f => Fun f
minimal = Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Nonstrict
  | Bool
otherwise = Maybe Strictness
forall a. Maybe a
Nothing

solve :: (Minimal f, Ordered f, PrettyTerm f, Labelled f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)
solve :: [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]
..}
  | [(Atom f, Atom f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Atom f, Atom f)]
equals Bool -> Bool -> Bool
&& Bool -> Bool
not (((Atom f, Atom f) -> Bool) -> [(Atom f, Atom f)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Atom f, Atom f) -> Bool
true [(Atom f, Atom f)]
less) =
    String -> Either (Model f) (Subst f)
forall a. HasCallStack => String -> a
error (String -> Either (Model f) (Subst f))
-> String -> Either (Model f) (Subst f)
forall a b. (a -> b) -> a -> b
$ String
"Model " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Model f -> String
forall a. Pretty a => a -> String
prettyShow Model f
model String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not a model of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Branch f -> String
forall a. Pretty a => a -> String
prettyShow Branch f
branch String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (edges = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Atom f, Atom f, [Atom f])] -> String
forall a. Pretty a => a -> String
prettyShow [(Atom f, Atom f, [Atom f])]
edges String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", vs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Atom f] -> String
forall a. Pretty a => a -> String
prettyShow [Atom f]
vs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  | [(Atom f, Atom f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Atom f, Atom f)]
equals = Model f -> Either (Model f) (Subst f)
forall a b. a -> Either a b
Left Model f
model
  | Bool
otherwise = Subst f -> Either (Model f) (Subst f)
forall a b. b -> Either a b
Right Subst f
sub
    where
      sub :: Subst f
sub = Subst f -> Maybe (Subst f) -> Subst f
forall a. a -> Maybe a -> a
fromMaybe Subst f
forall a. HasCallStack => a
undefined (Maybe (Subst f) -> Subst f)
-> ([(Var, Term f)] -> Maybe (Subst f))
-> [(Var, Term f)]
-> Subst f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Var, Term f)] -> Maybe (Subst f)
forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst ([(Var, Term f)] -> Subst f) -> [(Var, Term f)] -> Subst f
forall a b. (a -> b) -> a -> b
$
        [(Var
x, Atom f -> Term f
forall f. Atom f -> Term f
toTerm Atom f
y) | (Variable Var
x, Atom f
y) <- [(Atom f, Atom f)]
equals] [(Var, Term f)] -> [(Var, Term f)] -> [(Var, Term f)]
forall a. [a] -> [a] -> [a]
++
        [(Var
y, Atom f -> Term f
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 = Fun f -> Atom f
forall f. Fun f -> Atom f
Constant Fun f
forall f. Minimal f => Fun f
minimalAtom f -> [Atom f] -> [Atom f]
forall a. a -> [a] -> [a]
:[Atom f] -> [Atom f]
forall a. [a] -> [a]
reverse ([SCC (Atom f)] -> [Atom f]
forall a. [SCC a] -> [a]
flattenSCCs ([(Atom f, Atom f, [Atom f])] -> [SCC (Atom f)]
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 Atom f -> Atom f -> Bool
forall a. Eq a => a -> a -> Bool
== Atom f
x']) | Atom f
x <- [Atom f]
as, Atom f
x Atom f -> Atom f -> Bool
forall a. Eq a => a -> a -> Bool
/= Fun f -> Atom f
forall f. Fun f -> Atom f
Constant Fun f
forall f. Minimal f => Fun f
minimal]
      less' :: [(Atom f, Atom f)]
less' = [(Atom f, Atom f)]
less [(Atom f, Atom f)] -> [(Atom f, Atom f)] -> [(Atom f, Atom f)]
forall a. [a] -> [a] -> [a]
++ [(Fun f -> Atom f
forall f. Fun f -> Atom f
Constant Fun f
x, Fun f -> Atom f
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 Fun f -> Fun f -> Bool
forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
y]
      as :: [Atom f]
as = [Atom f] -> [Atom f]
forall a. Ord a => [a] -> [a]
usort ([Atom f] -> [Atom f]) -> [Atom f] -> [Atom f]
forall a b. (a -> b) -> a -> b
$ [Atom f]
xs [Atom f] -> [Atom f] -> [Atom f]
forall a. [a] -> [a] -> [a]
++ ((Atom f, Atom f) -> Atom f) -> [(Atom f, Atom f)] -> [Atom f]
forall a b. (a -> b) -> [a] -> [b]
map (Atom f, Atom f) -> Atom f
forall a b. (a, b) -> a
fst [(Atom f, Atom f)]
less [Atom f] -> [Atom f] -> [Atom f]
forall a. [a] -> [a] -> [a]
++ ((Atom f, Atom f) -> Atom f) -> [(Atom f, Atom f)] -> [Atom f]
forall a b. (a -> b) -> [a] -> [b]
map (Atom f, Atom f) -> Atom f
forall a b. (a, b) -> b
snd [(Atom f, Atom f)]
less
      model :: Model f
model = [Atom f] -> Model f
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) = Model f -> Atom f -> Atom f -> Maybe Strictness
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 Maybe Strictness -> Maybe Strictness -> Bool
forall a. Eq a => a -> a -> Bool
== Strictness -> Maybe Strictness
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
(Strictness -> Strictness -> Bool)
-> (Strictness -> Strictness -> Bool) -> Eq Strictness
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
(Int -> Strictness -> ShowS)
-> (Strictness -> String)
-> ([Strictness] -> ShowS)
-> Show Strictness
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 :: Term f -> Term f -> Bool
lessThan Term f
t Term f
u = Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
t Term f
u Bool -> Bool -> Bool
&& Maybe (Subst f) -> Bool
forall a. Maybe a -> Bool
isNothing (Term f -> Term f -> Maybe (Subst f)
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 :: Term f -> Term f -> Maybe Ordering
orientTerms Term f
t Term f
u
  | Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ
  | Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
t Term f
u = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
LT
  | Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
u Term f
t = Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT
  | Bool
otherwise = Maybe Ordering
forall a. Maybe a
Nothing