163 lines
5.6 KiB
Haskell
163 lines
5.6 KiB
Haskell
module Logic.Statement.Laws where
|
|
|
|
import Logic.Parse (eof, mkInput)
|
|
import Logic.Statement (Statement(..))
|
|
import Logic.Statement.Parse (stmt)
|
|
|
|
import Data.Either (fromRight)
|
|
import Data.Maybe (fromJust, listToMaybe)
|
|
|
|
data Law = Law
|
|
{ lawName :: String
|
|
, lawLhs :: Statement
|
|
, lawRhs :: Statement
|
|
} deriving (Eq, Show)
|
|
|
|
mkLaw :: String -> String -> String -> Law
|
|
mkLaw name lhs rhs = Law name (fromString lhs) (fromString rhs)
|
|
where
|
|
fromString :: String -> Statement
|
|
fromString string = fromRight undefined (eof stmt $ mkInput string)
|
|
|
|
laws :: [Law]
|
|
laws =
|
|
[ mkLaw "dbl_neg" "A" "!!A"
|
|
, mkLaw "and_comm" "(A&B)" "(B&A)"
|
|
, mkLaw "or_comm" "(A|B)" "(B|A)"
|
|
, mkLaw "and_assoc" "(A&(B&C))" "((A&B)&C)"
|
|
, mkLaw "or_assoc" "(A|(B|C))" "((A|B)|C)"
|
|
, mkLaw "and_or_distrib" "(A&(B|C))" "((A&B)|(A&C))"
|
|
, mkLaw "or_and_distrib" "(A|(B&C))" "((A|B)&(A|C))"
|
|
, mkLaw "and_symm_eq" "A" "(A&A)"
|
|
, mkLaw "or_symm_eq" "A" "(A|A)"
|
|
, mkLaw "not_and_distrib" "!(A&B)" "(!A|!B)"
|
|
, mkLaw "not_or_distrib" "!(A|B)" "(!A&!B)"
|
|
, mkLaw "implies_or" "(A->B)" "(!A|B)"
|
|
, mkLaw "implies_and" "(A->B)" "!(A&!B)"
|
|
, mkLaw "or_contr_eq" "A" "(A|(B&!B))"
|
|
, mkLaw "and_or_cancel" "A" "(A&(A|B))"
|
|
, mkLaw "or_and_cancel" "A" "(A|(A&B))"
|
|
, mkLaw "iff_and" "(A<->B)" "((A->B)&(B->A))"
|
|
, mkLaw "iff_or" "(A<->B)" "((A&B)|(!A&!B))"
|
|
]
|
|
|
|
lookupLaw :: String -> Maybe Law
|
|
lookupLaw name = listToMaybe $ filter (\law -> lawName law == name) laws
|
|
|
|
match
|
|
:: Statement
|
|
-- ^ pattern
|
|
-> Statement
|
|
-- ^ statement to search
|
|
-> Maybe [(String, Statement)]
|
|
-- ^ mapping from pattern-statement atoms to search-statement parts
|
|
match = aux []
|
|
where
|
|
aux
|
|
:: [(String, Statement)]
|
|
-> Statement
|
|
-> Statement
|
|
-> Maybe [(String, Statement)]
|
|
aux mapping (Atom key) s = add mapping (key, s)
|
|
aux mapping (Not p) (Not s) = aux mapping p s
|
|
aux mapping (And p1 p2) (And s1 s2) = binary mapping (p1, s1) (p2, s2)
|
|
aux mapping (Or p1 p2) (Or s1 s2) = binary mapping (p1, s1) (p2, s2)
|
|
aux mapping (Implies p1 p2) (Implies s1 s2) = binary mapping (p1, s1) (p2, s2)
|
|
aux mapping (Iff p1 p2) (Iff s1 s2) = binary mapping (p1, s1) (p2, s2)
|
|
aux mapping pattern s = Nothing
|
|
|
|
add
|
|
:: [(String, Statement)]
|
|
-> (String, Statement)
|
|
-> Maybe [(String, Statement)]
|
|
add mapping entry@(key, s') =
|
|
case lookup key mapping of
|
|
Nothing -> Just (entry:mapping)
|
|
Just existing
|
|
| existing == s' -> Just mapping
|
|
| otherwise -> Nothing
|
|
|
|
binary
|
|
:: [(String, Statement)]
|
|
-> (Statement, Statement)
|
|
-> (Statement, Statement)
|
|
-> Maybe [(String, Statement)]
|
|
binary mapping (p1, s1) (p2, s2) = do
|
|
mapping' <- aux mapping p1 s1
|
|
aux mapping' p2 s2
|
|
|
|
{-
|
|
ghci> f x = fromRight undefined $ eof stmt $ mkInput x
|
|
ghci> match (f "(A&B)") (f "(p&(q|r))")
|
|
Just [("B",Or (Atom "q") (Atom "r")),("A",Atom "p")]
|
|
ghci> match (f "((A&B)|A)") (f "(p&(q|r))")
|
|
Nothing
|
|
ghci> match (f "((A&B)|A)") (f "((p&(q|r))|p)")
|
|
Just [("B",Or (Atom "q") (Atom "r")),("A",Atom "p")]
|
|
ghci> match (f "((A&B)|A)") (f "((p&(q|r))|q)")
|
|
Nothing
|
|
ghci> l = fromJust $ lookupLaw "and_or_distrib"
|
|
ghci> l
|
|
Law {lawName = "and_or_distrib", lawLhs = And (Atom "A") (Or (Atom "B") (Atom "C")), lawRhs = Or (And (Atom "A") (Atom "B")) (And (Atom "A") (Atom "C"))}
|
|
ghci> match (lawLhs l) (f "(p&(q|r))")
|
|
Just [("C",Atom "r"),("B",Atom "q"),("A",Atom "p")]
|
|
-}
|
|
|
|
data SwapError
|
|
= Indeterminate
|
|
-- ^ An atom in p2 doesn't exist in p1.
|
|
-- Strictly: an atom in p2 doesn't exist in the result from `match`
|
|
-- (matters only if `match` is implemented incorrectly).
|
|
-- If for atoms we used terms of a type instead of strings,
|
|
-- we could avoid needing this error.
|
|
| NonMatchingPattern
|
|
deriving Show
|
|
|
|
swap :: Statement -> Statement -> Statement -> Either SwapError Statement
|
|
swap p1 p2 s = do
|
|
mapping <- maybe (Left NonMatchingPattern) Right $ match p1 s
|
|
maybe (Left Indeterminate) Right $ aux mapping p2
|
|
where
|
|
aux :: [(String, Statement)] -> Statement -> Maybe Statement
|
|
aux mapping (Atom key) = lookup key mapping
|
|
aux mapping (Not p) = Not <$> aux mapping p
|
|
aux mapping (And p1 p2) = And <$> aux mapping p1 <*> aux mapping p2
|
|
aux mapping (Or p1 p2) = Or <$> aux mapping p1 <*> aux mapping p2
|
|
aux mapping (Implies p1 p2) = Implies <$> aux mapping p1 <*> aux mapping p2
|
|
aux mapping (Iff p1 p2) = Iff <$> aux mapping p1 <*> aux mapping p2
|
|
|
|
{-
|
|
ghci> f x = fromRight undefined $ eof stmt $ mkInput x
|
|
ghci> l = fromJust $ lookupLaw "and_or_distrib"
|
|
ghci> l
|
|
Law {lawName = "and_or_distrib", lawLhs = And (Atom "A") (Or (Atom "B") (Atom "C")), lawRhs = Or (And (Atom "A") (Atom "B")) (And (Atom "A") (Atom "C"))}
|
|
ghci>
|
|
ghci> match (f "(A&B)") (f "(p&(q|r))")
|
|
Just [("B",Or (Atom "q") (Atom "r")),("A",Atom "p")]
|
|
ghci> swap (f "(A&B)") (f "A") (f "(p&(q|r))")
|
|
Right (Atom "p")
|
|
ghci> swap (f "(A&B)") (f "B") (f "(p&(q|r))")
|
|
Right (Or (Atom "q") (Atom "r"))
|
|
ghci> swap (f "(A&B)") (f "C") (f "(p&(q|r))")
|
|
Left Indeterminate
|
|
ghci> swap (f "((A&B)->C)") (f "A") (f "(p&(q|r))")
|
|
Left NonMatchingPattern
|
|
ghci>
|
|
ghci> x = f "(p&(q|r))"
|
|
ghci> x
|
|
And (Atom "p") (Or (Atom "q") (Atom "r"))
|
|
ghci> serialize Plain x
|
|
"(p&(q|r))"
|
|
ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawLhs l) x
|
|
"(p&(q|r))"
|
|
ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawRhs l) x
|
|
"((p&q)|(p&r))"
|
|
ghci>
|
|
ghci> x = f "(p&(!q|r))"
|
|
ghci> serialize Plain x
|
|
"(p&(!q|r))"
|
|
ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawLhs l) x
|
|
"(p&(!q|r))"
|
|
ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawRhs l) x
|
|
"((p&!q)|(p&r))"
|
|
-}
|