-- |
-- Module      : AutoProof.Internal.Formula.Operations
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Defines miscellaneous operations on formulas.
module AutoProof.Internal.Formula.Operations
  ( subformulas,
    substitute,
    getAnyVariable,
  )
where

import AutoProof.Internal.Formula.Types
  ( Formula (And, Iff, Imp, Lit, Not, Or, Var),
  )
import AutoProof.Internal.AST (children)
import Data.Set (Set)
import qualified Data.Set as Set
import Control.Applicative ((<|>))

-- | Get the set of subformulas of a propositional formula.
--
-- ==== __Examples__
--
-- >>> subformulas $ Or (Var 'x') (And (Var 'y') (Var 'z'))
-- fromList [Var 'x',Var 'y',Var 'z',And (Var 'y') (Var 'z'),Or (Var 'x') (And (Var 'y') (Var 'z'))]
subformulas :: Ord a => Formula a -> Set (Formula a)
subformulas :: Formula a -> Set (Formula a)
subformulas = Set (Formula a) -> Formula a -> Set (Formula a)
forall a. Ord a => Set (Formula a) -> Formula a -> Set (Formula a)
go Set (Formula a)
forall a. Set a
Set.empty
  where
    go :: Set (Formula a) -> Formula a -> Set (Formula a)
go s :: Set (Formula a)
s p :: Formula a
p@(Lit _) = Formula a -> Set (Formula a) -> Set (Formula a)
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
p Set (Formula a)
s
    go s :: Set (Formula a)
s p :: Formula a
p@(Var _) = Formula a -> Set (Formula a) -> Set (Formula a)
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
p Set (Formula a)
s
    go s :: Set (Formula a)
s p :: Formula a
p@(Not a :: Formula a
a) = Set (Formula a) -> Formula a -> Set (Formula a)
go (Formula a -> Set (Formula a) -> Set (Formula a)
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
p Set (Formula a)
s) Formula a
a
    go s :: Set (Formula a)
s p :: Formula a
p@(Imp a :: Formula a
a b :: Formula a
b) = Set (Formula a) -> Formula a -> Set (Formula a)
go (Set (Formula a) -> Formula a -> Set (Formula a)
go (Formula a -> Set (Formula a) -> Set (Formula a)
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
p Set (Formula a)
s) Formula a
a) Formula a
b
    go s :: Set (Formula a)
s p :: Formula a
p@(Or a :: Formula a
a b :: Formula a
b) = Set (Formula a) -> Formula a -> Set (Formula a)
go (Set (Formula a) -> Formula a -> Set (Formula a)
go (Formula a -> Set (Formula a) -> Set (Formula a)
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
p Set (Formula a)
s) Formula a
a) Formula a
b
    go s :: Set (Formula a)
s p :: Formula a
p@(And a :: Formula a
a b :: Formula a
b) = Set (Formula a) -> Formula a -> Set (Formula a)
go (Set (Formula a) -> Formula a -> Set (Formula a)
go (Formula a -> Set (Formula a) -> Set (Formula a)
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
p Set (Formula a)
s) Formula a
a) Formula a
b
    go s :: Set (Formula a)
s p :: Formula a
p@(Iff a :: Formula a
a b :: Formula a
b) = Set (Formula a) -> Formula a -> Set (Formula a)
go (Set (Formula a) -> Formula a -> Set (Formula a)
go (Formula a -> Set (Formula a) -> Set (Formula a)
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
p Set (Formula a)
s) Formula a
a) Formula a
b

-- | @('substitute' a x p)@ represents \(a[p/x]\), the substitution of each
-- occurence of the variable \(x\) in the formula \(a\) by the formula \(p\).
--
-- ==== __Examples__
--
-- >>> substitute (Imp (Var 'e') (Var 'e')) 'e' (And (Var 'a') (Var 'a'))
-- Imp (And (Var 'a') (Var 'a')) (And (Var 'a') (Var 'a'))
substitute :: Eq a => Formula a -> a -> Formula a -> Formula a
substitute :: Formula a -> a -> Formula a -> Formula a
substitute a :: Formula a
a@(Lit _) _ _ = Formula a
a
substitute v :: Formula a
v@(Var y :: a
y) x :: a
x p :: Formula a
p = if a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y then Formula a
p else Formula a
v
substitute (Not a :: Formula a
a) x :: a
x p :: Formula a
p = Formula a -> Formula a
forall a. Formula a -> Formula a
Not (Formula a -> Formula a) -> Formula a -> Formula a
forall a b. (a -> b) -> a -> b
$ Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
a a
x Formula a
p
substitute (Imp a :: Formula a
a b :: Formula a
b) x :: a
x p :: Formula a
p = Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
a a
x Formula a
p) (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
b a
x Formula a
p)
substitute (Or a :: Formula a
a b :: Formula a
b) x :: a
x p :: Formula a
p = Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
a a
x Formula a
p) (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
b a
x Formula a
p)
substitute (And a :: Formula a
a b :: Formula a
b) x :: a
x p :: Formula a
p = Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
a a
x Formula a
p) (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
b a
x Formula a
p)
substitute (Iff a :: Formula a
a b :: Formula a
b) x :: a
x p :: Formula a
p = Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Iff (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
a a
x Formula a
p) (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
b a
x Formula a
p)

-- | Obtain a propositional variable from a formula, if there is one.
--
-- ==== __Examples__
--
-- >>> getAnyVariable (Or (Var "a") (Var "b"))
-- Just "a"
--
-- >>> getAnyVariable (Lit False :: Formula String)
-- Nothing
getAnyVariable :: Formula a -> Maybe a
getAnyVariable :: Formula a -> Maybe a
getAnyVariable (Var x :: a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
getAnyVariable a :: Formula a
a = (Formula a -> Maybe a -> Maybe a)
-> Maybe a -> [Formula a] -> Maybe a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Maybe a -> Maybe a -> Maybe a)
-> (Formula a -> Maybe a) -> Formula a -> Maybe a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> Maybe a
forall a. Formula a -> Maybe a
getAnyVariable) Maybe a
forall a. Maybe a
Nothing (Formula a -> [Formula a]
forall t. AST t => t -> [t]
children Formula a
a)