Logic/Language.hs

@@ -1,30 +1,13 @@
 module Logic.Language where
 
-type List a = [a]
-
 -- Formal language (/grammar/production system/whatever)
 class (Eq symbol, Show symbol) => Language symbol where
-  isWellFormed :: [symbol] -> Bool
+  -- If Haskell had dependent types this could be generalized.
-
+  -- For now the languages I want to make use at most up to infer3.
-  -- If Haskell had dependent types these could be generalized.
+  infer0 :: [[symbol]]
-
+  infer1 :: [[symbol] -> [[symbol]]]
-  -- axiomN : N wffs -> theorem
+  infer2 :: [[symbol] -> [symbol] -> [[symbol]]]
-  axiom0 :: [[symbol]]
+  infer3 :: [[symbol] -> [symbol] -> [symbol] -> [[symbol]]]
-  axiom1 :: [[symbol] -> [symbol]]
-  axiom2 :: [[symbol] -> [symbol] -> [symbol]]
-  axiom3 :: [[symbol] -> [symbol] -> [symbol] -> [symbol]]
-
-  -- inferN : N theorems -> theorem
-  -- (axiom0 and infer0 would mean the same thing.)
-  infer1 :: [[symbol] -> List [symbol]]
-  infer2 :: [[symbol] -> [symbol] -> List [symbol]]
-
-  axiom0 = []
-  axiom1 = []
-  axiom2 = []
-  axiom3 = []
-  infer1 = []
-  infer2 = []
 
 -- Convenience newtype so strings are less ugly
 newtype Seq symbol = Seq [symbol]

Logic/Language/L.hs

@@ -1,142 +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
--}
-
-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]

Logic/Language/M.hs

@@ -13,16 +13,15 @@ data AlphaM
 type StringM = [AlphaM]
 
 instance Language AlphaM where
-  isWellFormed (M:_) = True
+  infer0 = [[M, I]]
-  isWellFormed _ = False
-
-  axiom0 = [[M, I]]
   infer1 =
     [ mRule1
     , mRule2
     , mRule3
     , mRule4
     ]
+  infer2 = []
+  infer3 = []
 
 -- RULE I: If you possess a string whose last letter is I, you can add on a U at the end.
 mRule1 :: StringM -> [StringM]

Logic/Parse.hs

@@ -3,55 +3,53 @@ module Logic.Parse where
 import Control.Applicative (Applicative, Alternative(..))
 import Data.Functor (Functor)
 
-newtype Parser symbol output = Parser
+newtype Parser output = Parser
-  { runParser :: Input symbol -> Either ParseError (output, Input symbol)
+  { runParser :: Input -> Either ParseError (output, Input)
   }
 
-data Input symbol = Input
+data Input = Input
   { inputPos :: Int
-  , inputSeq :: [symbol]
+  , inputSeq :: [Char]
   } deriving (Eq, Show)
 
-mkInput :: [symbol] -> Input symbol
+mkInput :: [Char] -> Input
 mkInput = Input 0
 
 data ParseError =
   ParseError Int String
-  deriving Show
+  deriving (Show)
 
-expected :: Show s => String -> Input s -> ParseError
+expected :: String -> Input -> ParseError
 expected thing input = ParseError (inputPos input) $
   "expected " <> thing <> ", found " <> show (take 20 $ inputSeq input)
 
-eof :: Show symbol => Parser symbol a -> Input symbol -> Either ParseError a
+eof :: Parser a -> Input -> Either ParseError a
 eof p input = do
   (result, rest) <- runParser p input
   case inputSeq rest of
     [] -> Right result
     _ -> Left $ expected "end of input" rest
 
-instance Functor (Parser s) where
+instance Functor Parser where
-  fmap :: (a -> b) -> Parser symbol a -> Parser symbol b
+  fmap :: (a -> b) -> Parser a -> Parser b
   fmap f (Parser p) = Parser $ \input -> do
     (result, rest) <- p input
     return (f result, rest)
 
-instance Applicative (Parser s) where
+instance Applicative Parser where
-  pure :: a -> Parser s a
+  pure :: a -> Parser a
   pure result = Parser $ \input -> Right (result, input)
 
-  (<*>) :: Parser s (a -> b) -> Parser s a -> Parser s b
   (Parser p1) <*> (Parser p2) =
     Parser $ \input -> do
       (f, rest) <- p1 input
       (result, rest') <- p2 rest
       return (f result, rest')
 
-instance Alternative (Parser s) where
+instance Alternative Parser where
-  empty :: Parser s a
+  empty :: Parser a
   empty = Parser $ const empty
 
-  (<|>) :: Parser s a -> Parser s a -> Parser s a
   (Parser p1) <|> (Parser p2) =
     Parser $ \input -> p1 input <|> p2 input
 
@@ -59,18 +57,10 @@ instance Alternative (Either ParseError) where
   empty :: Either ParseError a
   empty = Left $ ParseError 0 "this parser always fails"
 
-  (<|>) :: Either ParseError a -> Either ParseError a -> Either ParseError a
   (Right x) <|> _ = Right x
   (Left _) <|> e = e
 
-instance Monad (Parser s) where
+parseToken :: String -> Parser String
-  (>>=) :: Parser s a -> (a -> Parser s b) -> Parser s b
-  p1 >>= next = Parser $ \input ->
-    case runParser p1 input of
-      Right (result, rest) -> runParser (next result) rest
-      Left err -> Left err
-
-parseToken :: (Eq s, Show s) => [s] -> Parser s [s]
 parseToken token = Parser parse
   where
     n = length token
@@ -78,7 +68,7 @@ parseToken token = Parser parse
       | token == take n xs = Right $ (token,) $ Input (pos + n) (drop n xs)
       | otherwise = Left $ expected (show token) input
 
-parseIf :: Show s => String -> (s -> Bool) -> Parser s s
+parseIf :: String -> (Char -> Bool) -> Parser Char
 parseIf description check = Parser $ \input ->
   case inputSeq input of
     [] -> Left $ ParseError (inputPos input) "unexpected end of input"

Logic/Statement/Parse.hs

@@ -13,23 +13,19 @@ import Logic.Statement (Statement(..))
 import Control.Applicative (Alternative((<|>), some))
 import Data.Char (isAlphaNum)
 
-stmtAtom :: Parser Char Statement
+stmtAtom :: Parser Statement
 stmtAtom = Atom <$> parse
   where
-    parse = some $ parseIf "variable name" $ \char -> isAlphaNum char || char == '_'
+    parse = some $ parseIf "statement variable" $ \char -> isAlphaNum char || char == '_'
 
-stmtNot :: Parser Char Statement
+stmtNot :: Parser Statement
 stmtNot = Not <$> (parseToken "!" *> stmt)
 
-stmtBinary :: Parser Char Statement
+stmtBinary :: Parser Statement
-stmtBinary = do
+stmtBinary = parseToken "(" *> body <* parseToken ")"
-  parseToken "("
-  s1 <- stmt
-  constructor <- parseConnective
-  s2 <- stmt
-  parseToken ")"
-  return $ constructor s1 s2
   where
+    body = (\s1 f s2 -> f s1 s2) <$> stmt <*> parseConnective <*> stmt
+
     parseConnective =
       fmap (const And) (parseToken "&")
       <|> fmap (const Or) (parseToken "|")
@@ -39,7 +35,7 @@ stmtBinary = do
 
     fail = Parser $ \input -> Left $ expected "connective" input
 
-stmt :: Parser Char Statement
+stmt :: Parser Statement
 stmt = Parser $ \input ->
   let
     parser =