From 0e7bca0baa60ea63e350c082b6f1be1aca3a97fa Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Tue, 12 Aug 2025 03:59:40 +0000
Subject: [PATCH] apply logical laws

---
 Logic/Statement/Laws.hs | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/Logic/Statement/Laws.hs b/Logic/Statement/Laws.hs
index b38b1ed..0209a51 100644
--- a/Logic/Statement/Laws.hs
+++ b/Logic/Statement/Laws.hs
@@ -168,3 +168,37 @@ ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawLhs l) x
 ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawRhs l) x
 "((p&!q)|(p&r))"
 -}
+
+data ReplaceError
+  = IndeterminateReplace
+  deriving Show
+
+replace :: Statement -> Statement -> Statement -> Either ReplaceError [Statement]
+replace p1 p2 = firstLeft . aux
+  where
+    aux :: Statement -> [Either ReplaceError Statement]
+    aux s =
+      case swap p1 p2 s of
+        Left IndeterminateSwap -> [Left IndeterminateReplace]
+        -- ^ terminate here because in `replace` we stop at the first Left
+        Left NonMatchingPattern -> deeper s
+        Right s' -> (Right s'):(deeper s)
+
+    deeper :: Statement -> [Either ReplaceError Statement]
+    deeper (Atom key) = []
+    deeper (Not s) = do
+      e <- aux s
+      return $ Not <$> e
+    deeper (And     s1 s2) = binary And     s1 s2
+    deeper (Or      s1 s2) = binary Or      s1 s2
+    deeper (Implies s1 s2) = binary Implies s1 s2
+    deeper (Iff     s1 s2) = binary Iff     s1 s2
+
+    binary constructor s1 s2 =
+      [constructor <$> e1 <*> (Right s2) | e1 <- aux s1] ++
+      [constructor <$> (Right s1) <*> e2 | e2 <- aux s2]
+
+firstLeft :: [Either a b] -> Either a [b]
+firstLeft [] = Right []
+firstLeft ((Left a):_) = Left a
+firstLeft ((Right b):xs) = (b:) <$> firstLeft xs