formal language derivations

Logic/Language/L.hs

@@ -1,143 +0,0 @@
-module Logic.Language.L where
-
-import Logic.Language (Language(..), Seq(..))
-import Logic.Statement (Statement(..))
-import Logic.Parse
-  ( Parser(..)
-  , ParseError
-  , Input(..)
-  , eof
-  , expected
-  , mkInput
-  , parseToken
-  )
-
-import Control.Applicative (Alternative((<|>)))
-import Data.Either (isRight)
-import Data.Maybe (fromJust, maybeToList)
-import Text.Read (readMaybe)
-
--- The language L
-data AlphaL
-  = Arrow
-  | Tilde
-  | Open
-  | Close
-  | Variable Integer
-  deriving (Eq, Show)
-
-type StringL = [AlphaL]
-
-instance Language AlphaL where
-  isWellFormed string = isRight $ eof parseL $ mkInput string
-
-  axiom2 = [lAxiom1, lAxiom3]
-  axiom3 = [lAxiom2]
-  infer2 = [lRule1]
-
--- (A → (B → A))
-lAxiom1 :: StringL -> StringL -> StringL
-lAxiom1 wff1 wff2 =
-  [Open] ++
-    wff1 ++
-  [Arrow] ++
-    [Open] ++ wff2 ++ [Arrow] ++ wff1 ++ [Close] ++
-  [Close]
-
--- ((A → (B → C)) → ((A → B) → (A → C)))
-lAxiom2 :: StringL -> StringL -> StringL -> StringL
-lAxiom2 wff1 wff2 wff3 =
-  [Open] ++
-    [Open] ++
-      wff1 ++
-    [Arrow] ++
-      [Open] ++ wff2 ++ [Arrow] ++ wff3 ++ [Close] ++
-    [Close] ++
-  [Arrow] ++
-    [Open] ++
-      [Open] ++ wff1 ++ [Arrow] ++ wff2 ++ [Close] ++
-    [Arrow] ++
-      [Open] ++ wff1 ++ [Arrow] ++ wff3 ++ [Close] ++
-    [Close] ++
-  [Close]
-
--- ((¬A → ¬B) → ((¬A → B) → A))
-lAxiom3 :: StringL -> StringL -> StringL
-lAxiom3 wff1 wff2 =
-  [Open] ++
-    [Open, Tilde] ++ wff1 ++ [Arrow, Tilde] ++ wff2 ++ [Close] ++
-  [Arrow] ++
-    [Open] ++
-      [Open, Tilde] ++ wff1 ++ [Arrow] ++ wff2 ++ [Close] ++
-    [Arrow] ++
-      wff1 ++
-    [Close] ++
-  [Close]
-
-{-
-ghci> import Logic.Statement.Eval (bucket)
-ghci> import Data.Either (fromRight)
-ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom1 [Variable 0] [Variable 1]
-Tautology
-ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom2 [Variable 0] [Variable 1] [Variable 2]
-Tautology
-ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom3 [Variable 0] [Variable 1]
-Tautology
--}
-
--- Modus ponens: from (A → B) and A, conclude B.
-lRule1 :: StringL -> StringL -> [StringL]
-lRule1 theorem1 theorem2 = maybeToList $ do
-  s1 <- fromEither $ eof parseL $ mkInput theorem1
-  s2 <- fromEither $ eof parseL $ mkInput theorem2
-  case s1 of
-    Implies s1a s1b
-      | s2 == s1a -> Just $ fromJust $ serializeL s1b
-      | otherwise -> Nothing
-    _ -> Nothing
-  where
-    fromEither = either (const Nothing) Just
-
-{-
-ghci> f x = fromJust $ serializeL $ fromRight undefined $ eof stmt $ mkInput x
-ghci> lRule1 (f "(0->1)") (f "0")
-[[Variable 1]]
-ghci> lRule1 (f "((!0->2)->(!!!!!!!1->1))") (f "(!0->2)")
-[[Open,Tilde,Tilde,Tilde,Tilde,Tilde,Tilde,Tilde,Variable 1,Arrow,Variable 1,Close]]
-ghci> lRule1 (f "((!0->2)->(!!!!!!!1->1))") (f "(!0->3)")
-[]
--}
-
-parseL :: Parser AlphaL Statement
-parseL = Parser variable <|> Parser tilde <|> arrow <|> fail
-  where
-    variable :: Input AlphaL -> Either ParseError (Statement, Input AlphaL)
-    variable input@(Input pos ((Variable n):xs)) =
-      Right (Atom $ show n, Input (pos + 1) xs)
-    variable input = Left $ expected "statement variable" input
-
-    tilde :: Input AlphaL -> Either ParseError (Statement, Input AlphaL)
-    tilde input@(Input pos (Tilde:xs)) =
-      (\(statement, rest) -> (Not statement, rest)) <$>
-      runParser parseL (Input (pos + 1) xs)
-    tilde input = Left $ expected "negation" input
-
-    arrow :: Parser AlphaL Statement
-    arrow = do
-      parseToken [Open]
-      s1 <- parseL
-      parseToken [Arrow]
-      s2 <- parseL
-      parseToken [Close]
-      return $ Implies s1 s2
-
-    fail :: Parser AlphaL Statement
-    fail = Parser $ \input -> Left $ expected "well-formed formula" input
-
-serializeL :: Statement -> Maybe [AlphaL]
-serializeL (Atom label) = (\x -> [x]) <$> Variable <$> readMaybe label
-serializeL (Not s) = (Tilde:) <$> serializeL s
-serializeL (Implies s1 s2) = do
-  l1 <- serializeL s1
-  l2 <- serializeL s2
-  return $ [Open] ++ l1 ++ [Arrow] ++ l2 ++ [Close]