formal language L

Logic/Language.hs

@@ -1,13 +1,30 @@
 module Logic.Language where
 
+type List a = [a]
+
 -- Formal language (/grammar/production system/whatever)
 class (Eq symbol, Show symbol) => Language symbol where
-  -- If Haskell had dependent types this could be generalized.
-  -- For now the languages I want to make use at most up to infer3.
-  infer0 :: [[symbol]]
-  infer1 :: [[symbol] -> [[symbol]]]
-  infer2 :: [[symbol] -> [symbol] -> [[symbol]]]
-  infer3 :: [[symbol] -> [symbol] -> [symbol] -> [[symbol]]]
+  isWellFormed :: [symbol] -> Bool
+
+  -- If Haskell had dependent types these could be generalized.
+
+  -- axiomN : N wffs -> theorem
+  axiom0 :: [[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

@@ -0,0 +1,142 @@
+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,15 +13,16 @@ data AlphaM
 type StringM = [AlphaM]
 
 instance Language AlphaM where
-  infer0 = [[M, I]]
+  isWellFormed (M:_) = True
+  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,53 +3,55 @@ module Logic.Parse where
 import Control.Applicative (Applicative, Alternative(..))
 import Data.Functor (Functor)
 
-newtype Parser output = Parser
-  { runParser :: Input -> Either ParseError (output, Input)
+newtype Parser symbol output = Parser
+  { runParser :: Input symbol -> Either ParseError (output, Input symbol)
   }
 
-data Input = Input
+data Input symbol = Input
   { inputPos :: Int
-  , inputSeq :: [Char]
+  , inputSeq :: [symbol]
   } deriving (Eq, Show)
 
-mkInput :: [Char] -> Input
+mkInput :: [symbol] -> Input symbol
 mkInput = Input 0
 
 data ParseError =
   ParseError Int String
-  deriving (Show)
+  deriving Show
 
-expected :: String -> Input -> ParseError
+expected :: Show s => String -> Input s -> ParseError
 expected thing input = ParseError (inputPos input) $
   "expected " <> thing <> ", found " <> show (take 20 $ inputSeq input)
 
-eof :: Parser a -> Input -> Either ParseError a
+eof :: Show symbol => Parser symbol a -> Input symbol -> 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 where
-  fmap :: (a -> b) -> Parser a -> Parser b
+instance Functor (Parser s) where
+  fmap :: (a -> b) -> Parser symbol a -> Parser symbol b
   fmap f (Parser p) = Parser $ \input -> do
     (result, rest) <- p input
     return (f result, rest)
 
-instance Applicative Parser where
-  pure :: a -> Parser a
+instance Applicative (Parser s) where
+  pure :: a -> Parser s 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 where
-  empty :: Parser a
+instance Alternative (Parser s) where
+  empty :: Parser s a
   empty = Parser $ const empty
 
+  (<|>) :: Parser s a -> Parser s a -> Parser s a
   (Parser p1) <|> (Parser p2) =
     Parser $ \input -> p1 input <|> p2 input
 
@@ -57,10 +59,18 @@ 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
 
-parseToken :: String -> Parser String
+instance Monad (Parser s) where
+  (>>=) :: 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
@@ -68,7 +78,7 @@ parseToken token = Parser parse
       | token == take n xs = Right $ (token,) $ Input (pos + n) (drop n xs)
       | otherwise = Left $ expected (show token) input
 
-parseIf :: String -> (Char -> Bool) -> Parser Char
+parseIf :: Show s => String -> (s -> Bool) -> Parser s s
 parseIf description check = Parser $ \input ->
   case inputSeq input of
     [] -> Left $ ParseError (inputPos input) "unexpected end of input"

Logic/Statement/Parse.hs

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