{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}

{-|
Module       : ATP.FirstOrder.Occurrence
Description  : Occurrences of variables in first-order expressions.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
License      : GPL-3
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental
-}

module ATP.FirstOrder.Occurrence (
  -- * Occurrence
  FirstOrder(..),
  closed,
  close,
  unprefix
) where

import Prelude hiding (lookup)
import Control.Monad (liftM2, zipWithM, when)
import Data.Function (on)
#if !MIN_VERSION_base(4, 11, 0)
import Data.Semigroup (Semigroup(..))
#endif
import qualified Data.Set as S (insert, delete, member, null, singleton)
import Data.Set (Set)

import ATP.FirstOrder.Core
import ATP.FirstOrder.Alpha

-- $setup
-- >>> :load Property.Generators


-- * Occurrence

infix 5 ~=

-- | A class of first-order expressions, i.e. expressions that might contain
-- variables. @t'Formula'@s, @'Literal'@s and @'Term'@s are first-order expressions.
--
-- A variable can occur both as free and bound, therefore
-- @'free' e@ and @'bound' e@ are not necessarily disjoint and
-- @v `freeIn` e@ and @v `boundIn` e@ are not necessarily musually exclusive.
--
-- @'vars'@, @'free'@ and @'bound'@ are connected by the following property.
--
-- > free e <> bound e == vars e
--
-- @'occursIn'@, @'freeIn'@ and @'boundIn'@ are connected by the following property.
--
-- > v `freeIn` e || v `boundIn` e == v `occursIn` e
--
class FirstOrder e where
  -- | The set of all variables that occur anywhere in the given expression.
  vars :: e -> Set Var

  -- | The set of variables that occur freely in the given expression,
  -- i.e. are not bound by any quantifier inside the expression.
  free :: e -> Set Var

  -- | The set of variables that occur bound in the given expression,
  -- i.e. are bound by a quantifier inside the expression.
  bound :: e -> Set Var

  -- | Check whether the given variable occurs anywhere in the given expression.
  occursIn :: Var -> e -> Bool
  Var
v `occursIn` e
e = Var
v Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` e -> Set Var
forall e. FirstOrder e => e -> Set Var
vars e
e

  -- | Check whether the given variable occurs freely anywhere in the given expression.
  freeIn :: Var -> e -> Bool
  Var
v `freeIn` e
e = Var
v Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` e -> Set Var
forall e. FirstOrder e => e -> Set Var
free e
e

  -- | Check whether the given variable occurs bound anywhere in the given expression.
  boundIn :: Var -> e -> Bool
  Var
v `boundIn` e
e = Var
v Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` e -> Set Var
forall e. FirstOrder e => e -> Set Var
bound e
e

  -- | Check whether the given expression is ground, i.e. does not contain
  -- any variables.
  --
  -- Note that /ground formula/ is sometimes understood as /formula that does/
  -- /not contain any free variables/. In this library such formulas are called
  -- @'closed'@.
  ground :: e -> Bool
  ground = Set Var -> Bool
forall a. Set a -> Bool
S.null (Set Var -> Bool) -> (e -> Set Var) -> e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Set Var
forall e. FirstOrder e => e -> Set Var
vars

  -- | Check whether two given expressions are alpha-equivalent, that is
  -- equivalent up to renaming of variables.
  --
  -- '(~=)' is an equivalence relation.
  --
  -- __Symmetry__
  --
  -- > e ~= e
  --
  -- __Reflexivity__
  --
  -- > a ~= b == b ~= a
  --
  -- __Transitivity__
  --
  -- > a ~= b && b ~= c ==> a ~= c
  --
  (~=) :: e -> e -> Bool
  e
a ~= e
b = Alpha Bool -> Bool
forall a. Alpha a -> a
evalAlpha (e
a e -> e -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= e
b)

  -- | A helper function calculating alpha-equivalence using the 'Alpha' monad stack.
  (?=) :: e -> e -> Alpha Bool

  alpha :: MonadAlpha m => e -> AlphaT m e

instance FirstOrder LogicalExpression where
  vars :: LogicalExpression -> Set Var
vars = \case
    Clause  Clause
c -> Clause -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Clause
c
    Formula Formula
f -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Formula
f

  free :: LogicalExpression -> Set Var
free = \case
    Clause  Clause
c -> Clause -> Set Var
forall e. FirstOrder e => e -> Set Var
free Clause
c
    Formula Formula
f -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
free Formula
f

  bound :: LogicalExpression -> Set Var
bound = \case
    Clause  Clause
c -> Clause -> Set Var
forall e. FirstOrder e => e -> Set Var
bound Clause
c
    Formula Formula
f -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
bound Formula
f

  occursIn :: Var -> LogicalExpression -> Bool
occursIn Var
v = \case
    Clause  Clause
c -> Var -> Clause -> Bool
forall e. FirstOrder e => Var -> e -> Bool
occursIn Var
v Clause
c
    Formula Formula
f -> Var -> Formula -> Bool
forall e. FirstOrder e => Var -> e -> Bool
occursIn Var
v Formula
f

  freeIn :: Var -> LogicalExpression -> Bool
freeIn Var
v = \case
    Clause  Clause
c -> Var -> Clause -> Bool
forall e. FirstOrder e => Var -> e -> Bool
freeIn Var
v Clause
c
    Formula Formula
f -> Var -> Formula -> Bool
forall e. FirstOrder e => Var -> e -> Bool
freeIn Var
v Formula
f

  boundIn :: Var -> LogicalExpression -> Bool
boundIn Var
v = \case
    Clause  Clause
c -> Var -> Clause -> Bool
forall e. FirstOrder e => Var -> e -> Bool
boundIn Var
v Clause
c
    Formula Formula
f -> Var -> Formula -> Bool
forall e. FirstOrder e => Var -> e -> Bool
boundIn Var
v Formula
f

  ground :: LogicalExpression -> Bool
ground = \case
    Clause  Clause
c -> Clause -> Bool
forall e. FirstOrder e => e -> Bool
ground Clause
c
    Formula Formula
f -> Formula -> Bool
forall e. FirstOrder e => e -> Bool
ground Formula
f

  Clause  Clause
c ?= :: LogicalExpression -> LogicalExpression -> Alpha Bool
?= Clause  Clause
c' = Clause
c Clause -> Clause -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Clause
c'
  Formula Formula
f ?= Formula Formula
f' = Formula
f Formula -> Formula -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Formula
f'
  LogicalExpression
_         ?= LogicalExpression
_          = Bool -> Alpha Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  alpha :: LogicalExpression -> AlphaT m LogicalExpression
alpha = \case
    Clause  Clause
c -> Clause -> LogicalExpression
Clause  (Clause -> LogicalExpression)
-> AlphaT m Clause -> AlphaT m LogicalExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Clause -> AlphaT m Clause
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Clause
c
    Formula Formula
f -> Formula -> LogicalExpression
Formula (Formula -> LogicalExpression)
-> AlphaT m Formula -> AlphaT m LogicalExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> AlphaT m Formula
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Formula
f

instance FirstOrder Formula where
  vars :: Formula -> Set Var
vars = \case
    Atomic Literal
l         -> Literal -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Literal
l
    Negate Formula
f         -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Formula
f
    Connected  Connective
_ Formula
f Formula
g -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Formula
f Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Formula
g
    Quantified Quantifier
_ Var
_ Formula
f -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Formula
f

  free :: Formula -> Set Var
free = \case
    Atomic Literal
l         -> Literal -> Set Var
forall e. FirstOrder e => e -> Set Var
free Literal
l
    Negate Formula
f         -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
free Formula
f
    Connected  Connective
_ Formula
f Formula
g -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
free Formula
f Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
free Formula
g
    Quantified Quantifier
_ Var
v Formula
f -> Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
S.delete Var
v (Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
free Formula
f)

  bound :: Formula -> Set Var
bound = \case
    Atomic{}         -> Set Var
forall a. Monoid a => a
mempty
    Negate Formula
f         -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
bound Formula
f
    Connected  Connective
_ Formula
f Formula
g -> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
bound Formula
f Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
bound Formula
g
    Quantified Quantifier
_ Var
v Formula
f -> if Var
v Var -> Formula -> Bool
forall e. FirstOrder e => Var -> e -> Bool
`freeIn` Formula
f then Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
S.insert Var
v (Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
bound Formula
f) else Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
bound Formula
f

  Atomic Literal
l ?= :: Formula -> Formula -> Alpha Bool
?= Atomic Literal
l' = Literal
l Literal -> Literal -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Literal
l'
  Negate Formula
f ?= Negate Formula
f' = Formula
f Formula -> Formula -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Formula
f'
  Connected  Connective
c Formula
f Formula
g ?= Connected  Connective
c' Formula
f' Formula
g' | Connective
c Connective -> Connective -> Bool
forall a. Eq a => a -> a -> Bool
== Connective
c' = (Bool -> Bool -> Bool) -> Alpha Bool -> Alpha Bool -> Alpha Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) (Formula
f Formula -> Formula -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Formula
f') (Formula
g Formula -> Formula -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Formula
g')
  Quantified Quantifier
q Var
v Formula
f ?= Quantified Quantifier
q' Var
v' Formula
f' | Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
q' = Var -> Var -> Alpha Bool -> Alpha Bool
forall (m :: * -> *) a.
Monad m =>
Var -> Var -> AlphaT m a -> AlphaT m a
enter Var
v Var
v' (Formula
f Formula -> Formula -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Formula
f')
  Formula
_ ?= Formula
_ = Bool -> Alpha Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  alpha :: Formula -> AlphaT m Formula
alpha = \case
    Atomic Literal
l -> Literal -> Formula
Atomic (Literal -> Formula) -> AlphaT m Literal -> AlphaT m Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Literal -> AlphaT m Literal
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Literal
l
    Negate Formula
f -> Formula -> Formula
Negate (Formula -> Formula) -> AlphaT m Formula -> AlphaT m Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> AlphaT m Formula
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Formula
f
    Connected  Connective
c Formula
f Formula
g -> Connective -> Formula -> Formula -> Formula
Connected Connective
c (Formula -> Formula -> Formula)
-> AlphaT m Formula -> AlphaT m (Formula -> Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> AlphaT m Formula
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Formula
f AlphaT m (Formula -> Formula)
-> AlphaT m Formula -> AlphaT m Formula
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> AlphaT m Formula
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Formula
g
    Quantified Quantifier
q Var
v Formula
f -> do
      Var
v' <- Var -> AlphaT m Var
forall (m :: * -> *). MonadAlpha m => Var -> AlphaT m Var
binding Var
v
      Formula
f' <- Var -> Var -> AlphaT m Formula -> AlphaT m Formula
forall (m :: * -> *) a.
Monad m =>
Var -> Var -> AlphaT m a -> AlphaT m a
enter Var
v Var
v' (Formula -> AlphaT m Formula
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Formula
f)
      Formula -> AlphaT m Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantifier -> Var -> Formula -> Formula
Quantified Quantifier
q Var
v' Formula
f')

instance FirstOrder Clause where
  vars :: Clause -> Set Var
vars = [Signed Literal] -> Set Var
forall e. FirstOrder e => e -> Set Var
vars ([Signed Literal] -> Set Var)
-> (Clause -> [Signed Literal]) -> Clause -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Signed Literal]
getLiterals
  free :: Clause -> Set Var
free = Clause -> Set Var
forall e. FirstOrder e => e -> Set Var
vars
  bound :: Clause -> Set Var
bound Clause
_ = Set Var
forall a. Monoid a => a
mempty
  ~= :: Clause -> Clause -> Bool
(~=) = [Signed Literal] -> [Signed Literal] -> Bool
forall e. FirstOrder e => e -> e -> Bool
(~=) ([Signed Literal] -> [Signed Literal] -> Bool)
-> (Clause -> [Signed Literal]) -> Clause -> Clause -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Clause -> [Signed Literal]
getLiterals
  ?= :: Clause -> Clause -> Alpha Bool
(?=) = [Signed Literal] -> [Signed Literal] -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
(?=) ([Signed Literal] -> [Signed Literal] -> Alpha Bool)
-> (Clause -> [Signed Literal]) -> Clause -> Clause -> Alpha Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Clause -> [Signed Literal]
getLiterals
  alpha :: Clause -> AlphaT m Clause
alpha = ([Signed Literal] -> Clause)
-> AlphaT m [Signed Literal] -> AlphaT m Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Signed Literal] -> Clause
Literals (AlphaT m [Signed Literal] -> AlphaT m Clause)
-> (Clause -> AlphaT m [Signed Literal])
-> Clause
-> AlphaT m Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signed Literal -> AlphaT m (Signed Literal))
-> [Signed Literal] -> AlphaT m [Signed Literal]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Signed Literal -> AlphaT m (Signed Literal)
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha ([Signed Literal] -> AlphaT m [Signed Literal])
-> (Clause -> [Signed Literal])
-> Clause
-> AlphaT m [Signed Literal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Signed Literal]
getLiterals

instance FirstOrder e => FirstOrder (Signed e) where
  vars :: Signed e -> Set Var
vars  = e -> Set Var
forall e. FirstOrder e => e -> Set Var
vars  (e -> Set Var) -> (Signed e -> e) -> Signed e -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signed e -> e
forall e. Signed e -> e
unsign
  free :: Signed e -> Set Var
free  = e -> Set Var
forall e. FirstOrder e => e -> Set Var
free  (e -> Set Var) -> (Signed e -> e) -> Signed e -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signed e -> e
forall e. Signed e -> e
unsign
  bound :: Signed e -> Set Var
bound = e -> Set Var
forall e. FirstOrder e => e -> Set Var
bound (e -> Set Var) -> (Signed e -> e) -> Signed e -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signed e -> e
forall e. Signed e -> e
unsign

  occursIn :: Var -> Signed e -> Bool
occursIn Var
v = Var -> e -> Bool
forall e. FirstOrder e => Var -> e -> Bool
occursIn Var
v (e -> Bool) -> (Signed e -> e) -> Signed e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signed e -> e
forall e. Signed e -> e
unsign
  freeIn :: Var -> Signed e -> Bool
freeIn   Var
v = Var -> e -> Bool
forall e. FirstOrder e => Var -> e -> Bool
freeIn   Var
v (e -> Bool) -> (Signed e -> e) -> Signed e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signed e -> e
forall e. Signed e -> e
unsign
  boundIn :: Var -> Signed e -> Bool
boundIn  Var
v = Var -> e -> Bool
forall e. FirstOrder e => Var -> e -> Bool
boundIn  Var
v (e -> Bool) -> (Signed e -> e) -> Signed e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signed e -> e
forall e. Signed e -> e
unsign

  ground :: Signed e -> Bool
ground = e -> Bool
forall e. FirstOrder e => e -> Bool
ground (e -> Bool) -> (Signed e -> e) -> Signed e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signed e -> e
forall e. Signed e -> e
unsign

  ~= :: Signed e -> Signed e -> Bool
(~=) = e -> e -> Bool
forall e. FirstOrder e => e -> e -> Bool
(~=) (e -> e -> Bool) -> (Signed e -> e) -> Signed e -> Signed e -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Signed e -> e
forall e. Signed e -> e
unsign
  ?= :: Signed e -> Signed e -> Alpha Bool
(?=) = e -> e -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
(?=) (e -> e -> Alpha Bool)
-> (Signed e -> e) -> Signed e -> Signed e -> Alpha Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Signed e -> e
forall e. Signed e -> e
unsign

  alpha :: Signed e -> AlphaT m (Signed e)
alpha = (e -> AlphaT m e) -> Signed e -> AlphaT m (Signed e)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse e -> AlphaT m e
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha

instance FirstOrder Literal where
  vars :: Literal -> Set Var
vars = \case
    Propositional{} -> Set Var
forall a. Monoid a => a
mempty
    Predicate PredicateSymbol
_ [Term]
ts  -> [Term] -> Set Var
forall e. FirstOrder e => e -> Set Var
vars [Term]
ts
    Equality Term
a Term
b    -> Term -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Term
a Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Term
b

  free :: Literal -> Set Var
free = Literal -> Set Var
forall e. FirstOrder e => e -> Set Var
vars
  bound :: Literal -> Set Var
bound Literal
_ = Set Var
forall a. Monoid a => a
mempty

  Propositional Bool
b ?= :: Literal -> Literal -> Alpha Bool
?= Propositional Bool
b' = Bool -> Alpha Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
b Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b')
  Predicate PredicateSymbol
p [Term]
ts  ?= Predicate PredicateSymbol
p' [Term]
ts' | PredicateSymbol
p PredicateSymbol -> PredicateSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== PredicateSymbol
p' = [Term]
ts [Term] -> [Term] -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= [Term]
ts'
  Equality  Term
a Term
b   ?= Equality  Term
a' Term
b'  = (Bool -> Bool -> Bool) -> Alpha Bool -> Alpha Bool -> Alpha Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) (Term
a Term -> Term -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Term
a') (Term
b Term -> Term -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Term
b')
  Literal
_ ?= Literal
_ = Bool -> Alpha Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  alpha :: Literal -> AlphaT m Literal
alpha = \case
    Propositional Bool
b -> Literal -> AlphaT m Literal
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Literal
Propositional Bool
b)
    Predicate PredicateSymbol
p [Term]
ts  -> PredicateSymbol -> [Term] -> Literal
Predicate PredicateSymbol
p ([Term] -> Literal) -> AlphaT m [Term] -> AlphaT m Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> AlphaT m Term) -> [Term] -> AlphaT m [Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> AlphaT m Term
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha [Term]
ts
    Equality Term
a Term
b    -> Term -> Term -> Literal
Equality (Term -> Term -> Literal)
-> AlphaT m Term -> AlphaT m (Term -> Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> AlphaT m Term
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Term
a AlphaT m (Term -> Literal) -> AlphaT m Term -> AlphaT m Literal
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> AlphaT m Term
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Term
b

instance FirstOrder Term where
  vars :: Term -> Set Var
vars = \case
    Variable Var
v    -> Var -> Set Var
forall e. FirstOrder e => e -> Set Var
vars Var
v
    Function FunctionSymbol
_ [Term]
ts -> [Term] -> Set Var
forall e. FirstOrder e => e -> Set Var
vars [Term]
ts

  free :: Term -> Set Var
free = Term -> Set Var
forall e. FirstOrder e => e -> Set Var
vars
  bound :: Term -> Set Var
bound Term
_ = Set Var
forall a. Monoid a => a
mempty

  Variable Var
v    ?= :: Term -> Term -> Alpha Bool
?= Variable Var
v'     = Var
v Var -> Var -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= Var
v'
  Function FunctionSymbol
f [Term]
ts ?= Function FunctionSymbol
f' [Term]
ts' | FunctionSymbol
f FunctionSymbol -> FunctionSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== FunctionSymbol
f' = [Term]
ts [Term] -> [Term] -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
?= [Term]
ts'
  Term
_ ?= Term
_ = Bool -> Alpha Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  alpha :: Term -> AlphaT m Term
alpha = \case
    Function FunctionSymbol
f [Term]
ts -> FunctionSymbol -> [Term] -> Term
Function FunctionSymbol
f ([Term] -> Term) -> AlphaT m [Term] -> AlphaT m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> AlphaT m Term) -> [Term] -> AlphaT m [Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> AlphaT m Term
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha [Term]
ts
    Variable Var
v    -> Var -> Term
Variable   (Var -> Term) -> AlphaT m Var -> AlphaT m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> AlphaT m Var
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha Var
v

instance FirstOrder Var where
  vars :: Var -> Set Var
vars = Var -> Set Var
forall a. a -> Set a
S.singleton
  free :: Var -> Set Var
free = Var -> Set Var
forall e. FirstOrder e => e -> Set Var
vars
  bound :: Var -> Set Var
bound Var
_ = Set Var
forall a. Monoid a => a
mempty

  Var
v ?= :: Var -> Var -> Alpha Bool
?= Var
v' = Var -> AlphaT Identity (Maybe Var)
forall (m :: * -> *). Monad m => Var -> AlphaT m (Maybe Var)
lookup Var
v AlphaT Identity (Maybe Var)
-> (Maybe Var -> Alpha Bool) -> Alpha Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Var
w' -> Bool -> Alpha Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
w' Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v')
    Maybe Var
Nothing -> do
      [Var]
vs <- AlphaT Identity [Var]
forall (m :: * -> *). Monad m => AlphaT m [Var]
scope
      let f :: Bool
f = Var
v' Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Var]
vs
      Bool -> AlphaT Identity () -> AlphaT Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
f (Var -> Var -> AlphaT Identity ()
forall (m :: * -> *). Monad m => Var -> Var -> AlphaT m ()
share Var
v Var
v')
      Bool -> Alpha Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
f

  alpha :: Var -> AlphaT m Var
alpha Var
v = Var -> AlphaT m (Maybe Var)
forall (m :: * -> *). Monad m => Var -> AlphaT m (Maybe Var)
lookup Var
v AlphaT m (Maybe Var) -> (Maybe Var -> AlphaT m Var) -> AlphaT m Var
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Var
v' -> Var -> AlphaT m Var
forall (m :: * -> *). MonadAlpha m => Var -> AlphaT m Var
occurrence Var
v'
    Maybe Var
Nothing -> do { Var
v' <- Var -> AlphaT m Var
forall (m :: * -> *). MonadAlpha m => Var -> AlphaT m Var
binding Var
v; Var -> Var -> AlphaT m ()
forall (m :: * -> *). Monad m => Var -> Var -> AlphaT m ()
share Var
v Var
v'; Var -> AlphaT m Var
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v' }

instance FirstOrder e => FirstOrder [e] where
  vars :: [e] -> Set Var
vars = [Set Var] -> Set Var
forall a. Monoid a => [a] -> a
mconcat ([Set Var] -> Set Var) -> ([e] -> [Set Var]) -> [e] -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> Set Var) -> [e] -> [Set Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap e -> Set Var
forall e. FirstOrder e => e -> Set Var
vars
  free :: [e] -> Set Var
free = [e] -> Set Var
forall e. FirstOrder e => e -> Set Var
vars
  bound :: [e] -> Set Var
bound = [e] -> Set Var
forall a. Monoid a => a
mempty

  [e]
es ?= :: [e] -> [e] -> Alpha Bool
?= [e]
es' | [e] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [e]
es Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [e] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [e]
es' = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> AlphaT Identity [Bool] -> Alpha Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (e -> e -> Alpha Bool) -> [e] -> [e] -> AlphaT Identity [Bool]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM e -> e -> Alpha Bool
forall e. FirstOrder e => e -> e -> Alpha Bool
(?=) [e]
es [e]
es'
  [e]
_  ?= [e]
_   = Bool -> Alpha Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  alpha :: [e] -> AlphaT m [e]
alpha = (e -> AlphaT m e) -> [e] -> AlphaT m [e]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse e -> AlphaT m e
forall e (m :: * -> *).
(FirstOrder e, MonadAlpha m) =>
e -> AlphaT m e
alpha

-- | Check whether the given formula is closed, i.e. does not contain any free
-- variables.
closed :: Formula -> Bool
closed :: Formula -> Bool
closed = Set Var -> Bool
forall a. Set a -> Bool
S.null (Set Var -> Bool) -> (Formula -> Set Var) -> Formula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
free

-- | Make any given formula closed by adding a top-level universal quantifier
-- for each of its free variables.
--
-- @'close'@ and @'unprefix'@ are connected by the following property.
--
-- prop> unprefix (close f) === f
--
close :: Formula -> Formula
close :: Formula -> Formula
close Formula
f = (Formula -> Var -> Formula) -> Formula -> Set Var -> Formula
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Var -> Formula -> Formula) -> Formula -> Var -> Formula
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Var -> Formula -> Formula) -> Formula -> Var -> Formula)
-> (Var -> Formula -> Formula) -> Formula -> Var -> Formula
forall a b. (a -> b) -> a -> b
$ Quantifier -> Var -> Formula -> Formula
Quantified Quantifier
Forall) Formula
f (Formula -> Set Var
forall e. FirstOrder e => e -> Set Var
free Formula
f)

-- | Remove the top-level quantifiers.
--
-- >>> unprefix (Quantified Forall 1 (Quantified Exists 2 (Atomic (Equality (Variable 1) (Variable 2)))))
-- Atomic (Equality (Variable 1) (Variable 2))
--
unprefix :: Formula -> Formula
unprefix :: Formula -> Formula
unprefix = \case
  Quantified Quantifier
_ Var
_ Formula
f -> Formula -> Formula
unprefix Formula
f
  Formula
f -> Formula
f