Logic/Graph.hs

@@ -1,27 +0,0 @@
-module Logic.Graph where
-
-bfs :: Eq a => a -> a -> (a -> [(edge, a)]) -> Maybe [edge]
-bfs goal start getEdges = reverse <$> aux [([], start)] []
-  where
-    aux [] _ = Nothing
-    aux ((path, vertex):queue) visited
-      | vertex == goal = Just path
-      | otherwise =
-        let new = getUnvisitedAdjacent vertex visited
-        in
-          case filter (\(_, v) -> v == goal) new of
-            [] ->
-              let queue' = queue ++ map (\(edge, next) -> (edge:path, next)) new
-              in aux queue' (vertex:visited)
-            ((edge, _):_) -> Just (edge:path)
-
-    getUnvisitedAdjacent vertex visited =
-      filter (\(edge, next) -> not $ next `elem` visited) $
-      getEdges vertex
-
-{-
-ghci> bfs 10 0 (\x -> [("pred", x-1), ("succ", x+1)])
-Just ["succ","succ","succ","succ","succ","succ","succ","succ","succ","succ"]
-ghci> bfs 13 0 (\x -> [("double", x+x), ("add", x+1)])
-Just ["add","double","add","double","double","add"]
--}

Logic/Language/Impl/L.hs

@@ -151,12 +151,3 @@ deriveLExample1 = step5
     step3 = Infer2 0 0 step2 step1
     step4 = Axiom3 0 [Variable 0] [Variable 1] [Variable 2]
     step5 = Infer2 0 0 step4 step3
-
-deriveLExample2 :: Derivation AlphaL
-deriveLExample2 = step5
-  where
-    step1 = Axiom2 0 [Variable 0] [Open, Variable 0, Arrow, Variable 0, Close]
-    step2 = Axiom3 0 [Variable 0] [Open, Variable 0, Arrow, Variable 0, Close] [Variable 0]
-    step3 = Infer2 0 0 step2 step1
-    step4 = Axiom2 0 [Variable 0] [Variable 0]
-    step5 = Infer2 0 0 step3 step4

Logic/Statement.hs

@@ -20,11 +20,3 @@ atoms = toAscList . mkSet
     mkSet (Or s1 s2)      = union (mkSet s1) (mkSet s2)
     mkSet (Implies s1 s2) = union (mkSet s1) (mkSet s2)
     mkSet (Iff s1 s2)     = union (mkSet s1) (mkSet s2)
-
-substatements :: Statement -> [Statement]
-substatements s@(Atom _) = [s]
-substatements s@(Not s1) = s:(substatements s1)
-substatements s@(And s1 s2)     = (s:) $ substatements s1 ++ substatements s2
-substatements s@(Or s1 s2)      = (s:) $ substatements s1 ++ substatements s2
-substatements s@(Implies s1 s2) = (s:) $ substatements s1 ++ substatements s2
-substatements s@(Iff s1 s2)     = (s:) $ substatements s1 ++ substatements s2

Logic/Statement/Laws.hs

@@ -3,9 +3,8 @@ module Logic.Statement.Laws where
 import Logic.Parse (eof, mkInput)
 import Logic.Statement (Statement(..))
 import Logic.Statement.Parse (stmt)
-import Logic.Graph (bfs)
 
-import Data.Either (fromRight, rights)
+import Data.Either (fromRight)
 import Data.Maybe (fromJust, listToMaybe)
 
 data Law = Law
@@ -42,12 +41,6 @@ laws =
   , mkLaw "iff_or"  "(A<->B)" "((A&B)|(!A&!B))"
   ]
 
-{-
-ghci> import Logic.Statement.Eval (bucket, Bucket(Tautology))
-ghci> all (== Tautology) $ map (\law -> bucket $ Iff (lawLhs law) (lawRhs law)) laws
-True
--}
-
 lookupLaw :: String -> Maybe Law
 lookupLaw name = listToMaybe $ filter (\law -> lawName law == name) laws
 
@@ -55,7 +48,7 @@ match
   :: Statement
   -- ^ pattern
   -> Statement
-  -- ^ statement to search within
+  -- ^ statement to search
   -> Maybe [(String, Statement)]
   -- ^ mapping from pattern-statement atoms to search-statement parts
 match = aux []
@@ -111,20 +104,19 @@ Just [("C",Atom "r"),("B",Atom "q"),("A",Atom "p")]
 -}
 
 data SwapError
-  = IndeterminateSwap
+  = 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).
-  -- Theoretically if for atoms we used terms of a type instead of strings, we
-  -- could avoid needing this error, but I think we still wouldn't be able
-  -- to return a mapping from atom-type-1 to atom-type-2 in a type safe way.
+  -- 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 IndeterminateSwap) Right $ aux mapping p2
+  maybe (Left Indeterminate) Right $ aux mapping p2
   where
     aux :: [(String, Statement)] -> Statement -> Maybe Statement
     aux mapping (Atom key) = lookup key mapping
@@ -169,121 +161,3 @@ 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
-
-data LawsGraphEdge = LawsGraphEdge
-  { lgeLaw :: Law
-  , lgeReverse :: Bool
-  , lgeIndex :: Integer
-  } deriving (Eq, Show)
-
-bfsLaws :: Statement -> Statement -> Maybe [LawsGraphEdge]
-bfsLaws goal start = bfs goal start getLawsGraphEdges
-
-getLawsGraphEdges :: Statement -> [(LawsGraphEdge, Statement)]
-getLawsGraphEdges s = concat $ rights $ map aux laws
-  -- ^ `rights` here because we can't apply
-  -- e.g. or_contr_eq forwards without inventing B
-  where
-    aux :: Law -> Either ReplaceError [(LawsGraphEdge, Statement)]
-    aux law = do
-      forward <- direction law lawLhs lawRhs False
-      reverse <- direction law lawRhs lawLhs True
-      return $ forward ++ reverse
-
-    direction
-      :: Law
-      -> (Law -> Statement)
-      -> (Law -> Statement)
-      -> Bool
-      -> Either ReplaceError [(LawsGraphEdge, Statement)]
-    direction law mkPattern1 mkPattern2 isReverse = do
-      replaceds <- replace (mkPattern1 law) (mkPattern2 law) s
-      return $
-        (flip map) (zip [0..] replaceds) $ \(index, s') ->
-          let
-            edge = LawsGraphEdge
-              { lgeLaw = law
-              , lgeReverse = isReverse
-              , lgeIndex = index
-              }
-          in (edge, s')
-
-{-
-ghci> fromString x = fromRight undefined $ eof stmt $ mkInput x
-ghci> niceEdges = map (\edge -> (if lgeReverse edge then "< " else "> ") <> lawName (lgeLaw edge) <> " " <> show (lgeIndex edge))
-ghci> 
-ghci> niceEdges <$> bfsLaws (fromString "(p|!q)") (fromString "(p|!q)")
-Just []
-ghci> niceEdges <$> bfsLaws (fromString "!!(p|!q)") (fromString "(p|!q)")
-Just ["> dbl_neg 0"]
-ghci> niceEdges <$> bfsLaws (fromString "(!!p|!q)") (fromString "(p|!q)")
-Just ["> dbl_neg 1"]
-ghci> niceEdges <$> bfsLaws (fromString "(p|!!!q)") (fromString "(p|!q)")
-Just ["> dbl_neg 2"]
-ghci> niceEdges <$> bfsLaws (fromString "(p|p)") (fromString "p")
-Just ["> or_symm_eq 0"]
-ghci> niceEdges <$> bfsLaws (fromString "p") (fromString "(p|p)")
-Just ["< or_symm_eq 0"]
-ghci> 
-ghci> niceEdges <$> bfsLaws (fromString "!(!p&(q|q))") (fromString "(p|!q)")
-Just ["> dbl_neg 1","> or_symm_eq 5","< not_and_distrib 0"]
-ghci> niceEdges <$> bfsLaws (fromString "!(!(p&p)&(q|q))") (fromString "(p|!q)")
-Just ["> dbl_neg 1","> and_symm_eq 3","> or_symm_eq 7","< not_and_distrib 0"]
-ghci> 
-ghci> import Data.Time.POSIX (getPOSIXTime)
-ghci> time f = getPOSIXTime >>= \t0 -> f >> getPOSIXTime >>= \t1 -> return $ t1 - t0
-ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "p") (fromString "p")
-Just []
-0.000087114s
-ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!p") (fromString "p")
-Just ["> dbl_neg 0"]
-0.000201159s
-ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!p") (fromString "p")
-Just ["> dbl_neg 0","> dbl_neg 0"]
-0.000444047s
-ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!p") (fromString "p")
-Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
-0.001260947s
-ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!p") (fromString "p")
-Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
-0.021864298s
-ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!!!p") (fromString "p")
-Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
-3.244101767s
-Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
-3066.211460539s
--}