{- |
Module      : Fitch.Unification
Copyright   : (c) Leon Vatthauer, 2026
License     : GPL-3
Maintainer  : Leon Vatthauer <leon.vatthauer@fau.de>
Stability   : experimental
Portability : non-portable (ghc-wasm-meta)

This module implements the ability to check a t'Term', t'Formula' or t'Assumption'
against its t'TermSpec', t'FormulaSpec' or t'AssumptionSpec'.

Furthermore, implements a variant of the Martelli Montanari unification algorithm. where
t'Formula'e or t'Term's are unified __on__ a specific variable, meaning the variable must
occur on the left-hand-side of the resulting unifier.
-}
module Fitch.Unification where

import Data.Set qualified as Set
import Fitch.Proof
import Relude.Extra (delete, member, notMember)
import Specification.Types

-- * Collecting Variables

-- ** All variables

-- | Type class for structures that have variables occuring in them.
class AllVars a where
  -- | Returns all variables occuring in the structure.
  allVars :: a -> Set Name

  {- | Takes a name and a structure and makes it fresh
  w.r.t. all the variables occuring in the structure.
  -}
  makeFresh :: Name -> a -> Name
  makeFresh Name
n a
t = if Bool -> Bool
not (Name -> a -> Bool
forall a. AllVars a => Name -> a -> Bool
isFresh Name
n a
t) then Name -> a -> Name
forall a. AllVars a => Name -> a -> Name
makeFresh (Name
n Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
"'") a
t else Name
n

  -- | Checks if a variable is fresh in a structure.
  isFresh :: Name -> a -> Bool
  isFresh Name
n a
t = Name
Key (Set Name)
n Key (Set Name) -> Set Name -> Bool
forall t. StaticMap t => Key t -> t -> Bool
`notMember` a -> Set Name
forall a. AllVars a => a -> Set Name
allVars a
t

instance AllVars Term where
  allVars :: Term -> Set Name
  allVars :: Term -> Set Name
allVars (Var Name
x) = OneItem (Set Name) -> Set Name
forall x. One x => OneItem x -> x
one Name
OneItem (Set Name)
x
  allVars (Fun Name
_ [Term]
ts) = (Term -> Set Name) -> [Term] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term -> Set Name
forall a. AllVars a => a -> Set Name
allVars [Term]
ts

instance AllVars RawFormula where
  allVars :: RawFormula -> Set Name
  allVars :: RawFormula -> Set Name
allVars (Pred Name
_ [Term]
args) = (Term -> Set Name) -> [Term] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term -> Set Name
forall a. AllVars a => a -> Set Name
allVars [Term]
args
  allVars (Opr Name
_ [RawFormula]
fs) = (RawFormula -> Set Name) -> [RawFormula] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap RawFormula -> Set Name
forall a. AllVars a => a -> Set Name
allVars [RawFormula]
fs
  allVars (Quantifier Name
_ Name
v RawFormula
f) = OneItem (Set Name) -> Set Name
forall x. One x => OneItem x -> x
one Name
OneItem (Set Name)
v Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Set Name
forall a. AllVars a => a -> Set Name
allVars RawFormula
f

instance AllVars RawAssumption where
  allVars :: RawAssumption -> Set Name
  allVars :: RawAssumption -> Set Name
allVars (RawAssumption RawFormula
f) = RawFormula -> Set Name
forall a. AllVars a => a -> Set Name
allVars RawFormula
f
  allVars (FreshVar Name
v) = OneItem (Set Name) -> Set Name
forall x. One x => OneItem x -> x
one Name
OneItem (Set Name)
v

-- ** Free variables

-- | Type class for structures that have variables occuring in them.
class FreeVars a where
  -- | Returns only the __free__ (i.e. unbound) variables occuring in the structure.
  freeVars :: a -> Set Name

instance FreeVars Term where
  freeVars :: Term -> Set Name
  freeVars :: Term -> Set Name
freeVars (Var Name
x) = OneItem (Set Name) -> Set Name
forall x. One x => OneItem x -> x
one Name
OneItem (Set Name)
x
  freeVars (Fun Name
_ [Term]
ts) = (Term -> Set Name) -> [Term] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term -> Set Name
forall a. FreeVars a => a -> Set Name
freeVars [Term]
ts

instance FreeVars RawFormula where
  freeVars :: RawFormula -> Set Name
  freeVars :: RawFormula -> Set Name
freeVars (Pred Name
_ [Term]
args) = (Term -> Set Name) -> [Term] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term -> Set Name
forall a. FreeVars a => a -> Set Name
freeVars [Term]
args
  freeVars (Opr Name
_ [RawFormula]
fs) = (RawFormula -> Set Name) -> [RawFormula] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap RawFormula -> Set Name
forall a. FreeVars a => a -> Set Name
freeVars [RawFormula]
fs
  freeVars (Quantifier Name
_ Name
v RawFormula
f) = Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.delete Name
v (Set Name -> Set Name) -> Set Name -> Set Name
forall a b. (a -> b) -> a -> b
$ RawFormula -> Set Name
forall a. FreeVars a => a -> Set Name
freeVars RawFormula
f

instance FreeVars RawAssumption where
  freeVars :: RawAssumption -> Set Name
  freeVars :: RawAssumption -> Set Name
freeVars (RawAssumption RawFormula
f) = RawFormula -> Set Name
forall a. FreeVars a => a -> Set Name
freeVars RawFormula
f
  freeVars (FreshVar Name
_) = Set Name
forall a. Monoid a => a
mempty

-- * Substitution

-- | Type class for substitution.
class Substitute a b where
  {- | Takes a substitution and replaces variables occuring
  in the structure of type @a@ with elements of type @b@.
  Of course this only makes sense if the type @a@ also contains the type @b@.
  -}
  subst :: Subst b -> a -> a

instance Substitute Term Term where
  subst :: Subst Term -> Term -> Term
  subst :: Subst Term -> Term -> Term
subst (Subst Name
y Term
s) t :: Term
t@(Var Name
x) = if Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y then Term
s else Term
t
  subst Subst Term
sub (Fun Name
f [Term]
ts) = Name -> [Term] -> Term
Fun Name
f ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Subst Term -> Term -> Term
forall a b. Substitute a b => Subst b -> a -> a
subst Subst Term
sub) [Term]
ts

instance Substitute RawFormula Term where
  subst :: Subst Term -> RawFormula -> RawFormula
  subst :: Subst Term -> RawFormula -> RawFormula
subst Subst Term
sub (Pred Name
name [Term]
args) = Name -> [Term] -> RawFormula
Pred Name
name ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Subst Term -> Term -> Term
forall a b. Substitute a b => Subst b -> a -> a
subst Subst Term
sub) [Term]
args)
  subst Subst Term
sub (Opr Name
op [RawFormula]
fs) = Name -> [RawFormula] -> RawFormula
Opr Name
op ((RawFormula -> RawFormula) -> [RawFormula] -> [RawFormula]
forall a b. (a -> b) -> [a] -> [b]
map (Subst Term -> RawFormula -> RawFormula
forall a b. Substitute a b => Subst b -> a -> a
subst Subst Term
sub) [RawFormula]
fs)
  subst s :: Subst Term
s@(Subst Name
x Term
t) (Quantifier Name
q Name
v RawFormula
f)
    | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
v = Name -> Name -> RawFormula -> RawFormula
Quantifier Name
q Name
v RawFormula
f
    | Name
Key (Set Name)
v Key (Set Name) -> Set Name -> Bool
forall t. StaticMap t => Key t -> t -> Bool
`member` Term -> Set Name
forall a. FreeVars a => a -> Set Name
freeVars Term
t = Subst Term -> RawFormula -> RawFormula
forall a b. Substitute a b => Subst b -> a -> a
subst (Name -> Term -> Subst Term
forall a. Name -> a -> Subst a
Subst Name
x Term
t) (Name -> Name -> RawFormula -> RawFormula
Quantifier Name
q Name
v' RawFormula
f')
    | Bool
otherwise = Name -> Name -> RawFormula -> RawFormula
Quantifier Name
q Name
v (Subst Term -> RawFormula -> RawFormula
forall a b. Substitute a b => Subst b -> a -> a
subst Subst Term
s RawFormula
f)
   where
    v' :: Name
v' = Name -> RawFormula -> Name
forall a. AllVars a => Name -> a -> Name
makeFresh (Name -> Term -> Name
forall a. AllVars a => Name -> a -> Name
makeFresh Name
v Term
t) RawFormula
f
    f' :: RawFormula
f' = Subst Term -> RawFormula -> RawFormula
forall a b. Substitute a b => Subst b -> a -> a
subst (Name -> Term -> Subst Term
forall a. Name -> a -> Subst a
Subst Name
v (Name -> Term
Var Name
v')) RawFormula
f
  subst Subst Term
_ RawFormula
f = RawFormula
f

-- * Unification

{- | Unification on terms, this is the Martelli-Montanari unification algorithm
with a twist:
the unification happens __on__ a variable @x@.
Meaning the resulting unificator must have the variable @x@ on the left hand side.

This is guaranteed by adding a new orient rule,
which orients assignments of the form @x := y@, where @y@ is also a variable.
-}
unifyTermsOnVariable :: Name -> [(Term, Term)] -> Maybe [(Name, Term)]
unifyTermsOnVariable :: Name -> [(Term, Term)] -> Maybe [(Name, Term)]
unifyTermsOnVariable Name
n [(Term, Term)]
ts = do
  -- apply the rules until none of them match anymore.
  dc <- [(Term, Term)] -> Maybe (Bool, [(Term, Term)])
decompConflict [(Term, Term)]
ts
  case dc of
    (Bool
True, [(Term, Term)]
ts') -> Name -> [(Term, Term)] -> Maybe [(Name, Term)]
unifyTermsOnVariable Name
n [(Term, Term)]
ts'
    (Bool
False, [(Term, Term)]
ts') -> do
      edoo <- [(Term, Term)] -> Maybe (Bool, [(Term, Term)])
elimDeleteOccursOrient [(Term, Term)]
ts'
      case edoo of
        (Bool
True, [(Term, Term)]
ts'') -> Name -> [(Term, Term)] -> Maybe [(Name, Term)]
unifyTermsOnVariable Name
n [(Term, Term)]
ts''
        (Bool
False, [(Term, Term)]
ts'') -> [(Term, Term)] -> Maybe [(Name, Term)]
makeUnificator [(Term, Term)]
ts''
 where
  {- Tries to apply the (decomp) or (conflict) rule,
  returns `Nothing` on failure (i.e. on conflict).
  Also returns whether the rule was applied, or no match was found. -}
  decompConflict :: [(Term, Term)] -> Maybe (Bool, [(Term, Term)])
  decompConflict :: [(Term, Term)] -> Maybe (Bool, [(Term, Term)])
decompConflict [(Term, Term)]
ts = ((Bool, [(Term, Term)])
 -> (Term, Term) -> Maybe (Bool, [(Term, Term)]))
-> (Bool, [(Term, Term)])
-> [(Term, Term)]
-> Maybe (Bool, [(Term, Term)])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (Bool, [(Term, Term)])
-> (Term, Term) -> Maybe (Bool, [(Term, Term)])
once (Bool
False, [(Term, Term)]
ts) [(Term, Term)]
ts
   where
    once :: (Bool, [(Term, Term)]) -> (Term, Term) -> Maybe (Bool, [(Term, Term)])
    once :: (Bool, [(Term, Term)])
-> (Term, Term) -> Maybe (Bool, [(Term, Term)])
once (Bool
_, [(Term, Term)]
list) tup :: (Term, Term)
tup@(Fun Name
f [Term]
args1, Fun Name
g [Term]
args2)
      -- (decomp)
      | Name
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
g = (Bool, [(Term, Term)]) -> Maybe (Bool, [(Term, Term)])
forall a. a -> Maybe a
Just (Bool
True, [Term] -> [Term] -> [(Term, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
args1 [Term]
args2 [(Term, Term)] -> [(Term, Term)] -> [(Term, Term)]
forall a. Semigroup a => a -> a -> a
<> ((Term, Term) -> Bool) -> [(Term, Term)] -> [(Term, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Term, Term) -> (Term, Term) -> Bool
forall a. Eq a => a -> a -> Bool
/= (Term, Term)
tup) [(Term, Term)]
list)
      -- (conflict)
      | Bool
otherwise = Maybe (Bool, [(Term, Term)])
forall a. Maybe a
Nothing
    once (Bool, [(Term, Term)])
ret (Term, Term)
_ = (Bool, [(Term, Term)]) -> Maybe (Bool, [(Term, Term)])
forall a. a -> Maybe a
Just (Bool, [(Term, Term)])
ret

  {- Tries to apply the (elim), (occurs), (delete) and (orient) rules,
  returns `Nothing` on failure (i.e. on occurs).
  Also returns whether the rule was applied, or no match was found. -}
  elimDeleteOccursOrient :: [(Term, Term)] -> Maybe (Bool, [(Term, Term)])
  elimDeleteOccursOrient :: [(Term, Term)] -> Maybe (Bool, [(Term, Term)])
elimDeleteOccursOrient [(Term, Term)]
ts = ((Bool, [(Term, Term)])
 -> (Term, Term) -> Maybe (Bool, [(Term, Term)]))
-> (Bool, [(Term, Term)])
-> [(Term, Term)]
-> Maybe (Bool, [(Term, Term)])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (Bool, [(Term, Term)])
-> (Term, Term) -> Maybe (Bool, [(Term, Term)])
once (Bool
False, [(Term, Term)]
ts) [(Term, Term)]
ts
   where
    once :: (Bool, [(Term, Term)]) -> (Term, Term) -> Maybe (Bool, [(Term, Term)])
    -- (delete)
    once :: (Bool, [(Term, Term)])
-> (Term, Term) -> Maybe (Bool, [(Term, Term)])
once (Bool
_, [(Term, Term)]
list) tup :: (Term, Term)
tup@(Var Name
x, Var Name
y)
      | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y =
          (Bool, [(Term, Term)]) -> Maybe (Bool, [(Term, Term)])
forall a. a -> Maybe a
Just (Bool
True, ((Term, Term) -> Bool) -> [(Term, Term)] -> [(Term, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Term, Term) -> (Term, Term) -> Bool
forall a. Eq a => a -> a -> Bool
/= (Term, Term)
tup) [(Term, Term)]
list)
    -- (orient) [with special case to also orient `n`]
    once (Bool
_, [(Term, Term)]
list) tup :: (Term, Term)
tup@(Term
t, Var Name
x)
      | Term -> Bool
isFun Term
t Bool -> Bool -> Bool
|| Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n =
          (Bool, [(Term, Term)]) -> Maybe (Bool, [(Term, Term)])
forall a. a -> Maybe a
Just (Bool
True, (Name -> Term
Var Name
x, Term
t) (Term, Term) -> [(Term, Term)] -> [(Term, Term)]
forall a. a -> [a] -> [a]
: ((Term, Term) -> Bool) -> [(Term, Term)] -> [(Term, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Term, Term) -> (Term, Term) -> Bool
forall a. Eq a => a -> a -> Bool
/= (Term, Term)
tup) [(Term, Term)]
list)
    once (Bool
b, [(Term, Term)]
list) tup :: (Term, Term)
tup@(Var Name
x, Term
t)
      -- (occurs)
      | Name
Key (Set Name)
x Key (Set Name) -> Set Name -> Bool
forall t. StaticMap t => Key t -> t -> Bool
`member` Term -> Set Name
forall a. FreeVars a => a -> Set Name
freeVars Term
t = Maybe (Bool, [(Term, Term)])
forall a. Maybe a
Nothing
      -- (elim)
      | Name
Key (Set Name)
x
          Key (Set Name) -> Set Name -> Bool
forall t. StaticMap t => Key t -> t -> Bool
`member` ((Term, Term) -> Set Name) -> [(Term, Term)] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
            (\(Term
t1, Term
t2) -> Term -> Set Name
forall a. FreeVars a => a -> Set Name
freeVars Term
t1 Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Term -> Set Name
forall a. FreeVars a => a -> Set Name
freeVars Term
t2)
            (((Term, Term) -> Bool) -> [(Term, Term)] -> [(Term, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Term, Term) -> (Term, Term) -> Bool
forall a. Eq a => a -> a -> Bool
/= (Term, Term)
tup) [(Term, Term)]
list) =
          (Bool, [(Term, Term)]) -> Maybe (Bool, [(Term, Term)])
forall a. a -> Maybe a
Just
            ( Bool
True
            , (Name -> Term
Var Name
x, Term
t)
                (Term, Term) -> [(Term, Term)] -> [(Term, Term)]
forall a. a -> [a] -> [a]
: ((Term, Term) -> (Term, Term)) -> [(Term, Term)] -> [(Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map
                  ( (Term -> Term) -> (Term -> Term) -> (Term, Term) -> (Term, Term)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
                      (Subst Term -> Term -> Term
forall a b. Substitute a b => Subst b -> a -> a
subst (Name -> Term -> Subst Term
forall a. Name -> a -> Subst a
Subst Name
x Term
t))
                      (Subst Term -> Term -> Term
forall a b. Substitute a b => Subst b -> a -> a
subst (Name -> Term -> Subst Term
forall a. Name -> a -> Subst a
Subst Name
x Term
t))
                  )
                  (((Term, Term) -> Bool) -> [(Term, Term)] -> [(Term, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Term, Term) -> (Term, Term) -> Bool
forall a. Eq a => a -> a -> Bool
/= (Name -> Term
Var Name
x, Term
t)) [(Term, Term)]
list)
            )
    once (Bool, [(Term, Term)])
ret (Term, Term)
_ = (Bool, [(Term, Term)]) -> Maybe (Bool, [(Term, Term)])
forall a. a -> Maybe a
Just (Bool, [(Term, Term)])
ret

  -- Turns a list of term tuples to a unificator.
  makeUnificator :: [(Term, Term)] -> Maybe [(Name, Term)]
  makeUnificator :: [(Term, Term)] -> Maybe [(Name, Term)]
makeUnificator [] = [(Name, Term)] -> Maybe [(Name, Term)]
forall a. a -> Maybe a
Just []
  makeUnificator ((Var Name
x, Term
t) : [(Term, Term)]
rest) = ((Name
x, Term
t) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
:) ([(Name, Term)] -> [(Name, Term)])
-> Maybe [(Name, Term)] -> Maybe [(Name, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term, Term)] -> Maybe [(Name, Term)]
makeUnificator [(Term, Term)]
rest
  makeUnificator [(Term, Term)]
_ = Maybe [(Name, Term)]
forall a. Maybe a
Nothing

-- | Lifts `unifyTermsOnVariable` to formulae.
unifyFormulaeOnVariable :: Name -> [(RawFormula, RawFormula)] -> Maybe (Map Name Term)
unifyFormulaeOnVariable :: Name -> [(RawFormula, RawFormula)] -> Maybe (Map Name Term)
unifyFormulaeOnVariable Name
n = ([(Name, Term)] -> Map Name Term)
-> Maybe [(Name, Term)] -> Maybe (Map Name Term)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Name, Term)] -> Map Name Term
[Item (Map Name Term)] -> Map Name Term
forall l. IsList l => [Item l] -> l
fromList (Maybe [(Name, Term)] -> Maybe (Map Name Term))
-> ([(RawFormula, RawFormula)] -> Maybe [(Name, Term)])
-> [(RawFormula, RawFormula)]
-> Maybe (Map Name Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RawFormula, RawFormula)] -> Maybe [(Name, Term)]
go
 where
  go :: [(RawFormula, RawFormula)] -> Maybe [(Name, Term)]
  go :: [(RawFormula, RawFormula)] -> Maybe [(Name, Term)]
go [] = [(Name, Term)] -> Maybe [(Name, Term)]
forall a. a -> Maybe a
Just []
  go ((Pred Name
p [Term]
ts, Pred Name
q [Term]
ss) : [(RawFormula, RawFormula)]
rest) | Name
p Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
q Bool -> Bool -> Bool
&& [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ss = do
    mapping <- [(RawFormula, RawFormula)] -> Maybe [(Name, Term)]
go [(RawFormula, RawFormula)]
rest
    unifyTermsOnVariable n $ zip ts ss <> map (first Var) mapping
  go ((Opr Name
o1 [RawFormula]
fs1, Opr Name
o2 [RawFormula]
fs2) : [(RawFormula, RawFormula)]
rest)
    | Name
o1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
o2 Bool -> Bool -> Bool
&& [RawFormula] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RawFormula]
fs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [RawFormula] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RawFormula]
fs2 =
        [(RawFormula, RawFormula)] -> Maybe [(Name, Term)]
go ([RawFormula] -> [RawFormula] -> [(RawFormula, RawFormula)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RawFormula]
fs1 [RawFormula]
fs2 [(RawFormula, RawFormula)]
-> [(RawFormula, RawFormula)] -> [(RawFormula, RawFormula)]
forall a. Semigroup a => a -> a -> a
<> [(RawFormula, RawFormula)]
rest)
  go ((Quantifier Name
q1 Name
v1 RawFormula
f1, Quantifier Name
q2 Name
v2 RawFormula
f2) : [(RawFormula, RawFormula)]
rest)
    | Name
q1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
q2 Bool -> Bool -> Bool
&& Name
v1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
v2 =
        [(RawFormula, RawFormula)] -> Maybe [(Name, Term)]
go ((RawFormula
f1, RawFormula
f2) (RawFormula, RawFormula)
-> [(RawFormula, RawFormula)] -> [(RawFormula, RawFormula)]
forall a. a -> [a] -> [a]
: [(RawFormula, RawFormula)]
rest)
  go [(RawFormula, RawFormula)]
_ = Maybe [(Name, Term)]
forall a. Maybe a
Nothing

-- | Unify t'Term' with t'TermSpec'.
termMatchesSpec :: [(Term, TermSpec)] -> Bool
termMatchesSpec :: [(Term, TermSpec)] -> Bool
termMatchesSpec ((Fun Name
t [Term]
ts, TFun Name
s [TermSpec]
ss) : [(Term, TermSpec)]
rest)
  | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
s Bool -> Bool -> Bool
&& [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TermSpec] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TermSpec]
ss =
      [(Term, TermSpec)] -> Bool
termMatchesSpec ([Term] -> [TermSpec] -> [(Term, TermSpec)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
ts [TermSpec]
ss [(Term, TermSpec)] -> [(Term, TermSpec)] -> [(Term, TermSpec)]
forall a. [a] -> [a] -> [a]
++ [(Term, TermSpec)]
rest)
termMatchesSpec ((Var Name
x, TVar Name
y) : [(Term, TermSpec)]
rest) = [(Term, TermSpec)] -> Bool
termMatchesSpec [(Term, TermSpec)]
rest
termMatchesSpec ((Term
t, TPlaceholder Name
n) : [(Term, TermSpec)]
rest) = [(Term, TermSpec)] -> Bool
termMatchesSpec [(Term, TermSpec)]
rest
termMatchesSpec [] = Bool
True
termMatchesSpec [(Term, TermSpec)]
_ = Bool
False

-- | Unify t'RawFormula' with t'FormulaSpec'.
formulaMatchesSpec :: RawFormula -> FormulaSpec -> Bool
formulaMatchesSpec :: RawFormula -> FormulaSpec -> Bool
formulaMatchesSpec f :: RawFormula
f@(Pred Name
p [Term]
ts) fs :: FormulaSpec
fs@(FPred Name
p' [TermSpec]
ts')
  | Name
p Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
p' Bool -> Bool -> Bool
&& [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TermSpec] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TermSpec]
ts' = [(Term, TermSpec)] -> Bool
termMatchesSpec ([Term] -> [TermSpec] -> [(Term, TermSpec)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
ts [TermSpec]
ts')
formulaMatchesSpec f :: RawFormula
f@(InfixPred Name
p Term
t1 Term
t2) fs :: FormulaSpec
fs@(FInfixPred Name
p' TermSpec
t1' TermSpec
t2')
  | Name
p Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
p' = [(Term, TermSpec)] -> Bool
termMatchesSpec [(Term
t1, TermSpec
t1')] Bool -> Bool -> Bool
&& [(Term, TermSpec)] -> Bool
termMatchesSpec [(Term
t2, TermSpec
t2')]
formulaMatchesSpec (Opr Name
op [RawFormula]
fs) (FOpr Name
op' [FormulaSpec]
fs')
  | Name
op Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
op' = ((RawFormula, FormulaSpec) -> Bool)
-> [(RawFormula, FormulaSpec)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((RawFormula -> FormulaSpec -> Bool)
-> (RawFormula, FormulaSpec) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry RawFormula -> FormulaSpec -> Bool
formulaMatchesSpec) ([RawFormula] -> [FormulaSpec] -> [(RawFormula, FormulaSpec)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RawFormula]
fs [FormulaSpec]
fs')
formulaMatchesSpec f :: RawFormula
f@(Quantifier Name
q Name
v RawFormula
form) fs :: FormulaSpec
fs@(FQuantifier Name
q' Name
v' FormulaSpec
form')
  | Name
q Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
q' = RawFormula -> FormulaSpec -> Bool
formulaMatchesSpec RawFormula
form FormulaSpec
form'
formulaMatchesSpec RawFormula
f fs :: FormulaSpec
fs@(FPlaceholder Name
n) = Bool
True
formulaMatchesSpec RawFormula
f fs :: FormulaSpec
fs@(FSubst Name
n Subst Name
sub) = Bool
True
formulaMatchesSpec RawFormula
_ FormulaSpec
_ = Bool
False

-- | Unify t'RawAssumption' with t'AssumptionSpec'.
assumptionMatchesSpec :: RawAssumption -> AssumptionSpec -> Bool
assumptionMatchesSpec :: RawAssumption -> AssumptionSpec -> Bool
assumptionMatchesSpec (FreshVar{}) (FFreshVar{}) = Bool
True
assumptionMatchesSpec (RawAssumption RawFormula
rf) (AssumptionSpec FormulaSpec
fSpec) =
  RawFormula -> FormulaSpec -> Bool
formulaMatchesSpec RawFormula
rf FormulaSpec
fSpec
assumptionMatchesSpec RawAssumption
_ AssumptionSpec
_ = Bool
False