Разбор формальной логики в Haskell

Question

У меня есть следующий язык, который я пытаюсь проанализировать.

formula ::=  true  
         |  false  
         |  var  
         |  formula & formula  
         |  ∀ var . formula
         |  (formula)

    var ::=  letter { letter | digit }*

Я следил за этой статьей на вики Haskell и использовал комбинаторы Parsec для создания следующего парсера.

module LogicParser where

import System.IO
import Control.Monad
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
import Text.ParserCombinators.Parsec.Language
import qualified Text.ParserCombinators.Parsec.Token as Token

-- Data Structures
data Formula = Var String
             | TT
             | FF
             | Con Formula Formula
             | Forall String Formula
               deriving (Show)

-- Language Definition
lang :: LanguageDef st
lang =
    emptyDef{ Token.identStart      = letter
            , Token.identLetter     = alphaNum
            , Token.opStart         = oneOf "&."
            , Token.opLetter        = oneOf "&."
            , Token.reservedOpNames = ["&", "."]
            , Token.reservedNames   = ["tt", "ff", "forall"]
            }


-- Lexer for langauge
lexer = 
    Token.makeTokenParser lang


-- Trivial Parsers
identifier     = Token.identifier lexer
keyword        = Token.reserved lexer
op             = Token.reservedOp lexer
roundBrackets  = Token.parens lexer
whiteSpace     = Token.whiteSpace lexer

-- Main Parser, takes care of trailing whitespaces
formulaParser :: Parser Formula
formulaParser = whiteSpace >> formula

-- Parsing Formulas
formula :: Parser Formula
formula = conFormula
        <|> formulaTerm
        <|> forallFormula

-- Term in a Formula
formulaTerm :: Parser Formula
formulaTerm = roundBrackets formula
            <|> ttFormula
            <|> ffFormula
            <|> varFormula

-- Conjunction
conFormula :: Parser Formula
conFormula = 
    buildExpressionParser [[Infix (op "&" >> return Con) AssocLeft]] formula

-- Truth
ttFormula :: Parser Formula
ttFormula = keyword "tt" >> return TT

-- Falsehood
ffFormula :: Parser Formula
ffFormula = keyword "ff" >> return FF

-- Variable
varFormula :: Parser Formula
varFormula =
    do  var <- identifier
        return $ Var var

-- Universal Statement 
forallFormula :: Parser Formula
forallFormula = 
    do  keyword "forall"
        x <- identifier
        op "."
        phi <- formulaTerm
        return $ Forall x phi

-- For running runghc
calculate :: String -> String
calculate s = 
    case ret of
        Left e ->  "Error: " ++ (show e)
        Right n -> "Interpreted as: " ++ (show n)
    where 
        ret = parse formulaParser "" s

main :: IO ()
main = interact (unlines . (map calculate) . lines)

Проблема в операторе &, я пытаюсь смоделировать его на , как статья разбирает выражения , используя функцию Infix и передавая ей список операторови парсер для разбора терминов.Тем не менее, синтаксический анализатор ведет себя не так, как хотелось бы, и я не могу понять, почему.Вот несколько примеров желаемого поведения:

true                         -- parsing -->      TT
true & false                 -- parsing -->      Con TT FF
true & (true & false)        -- parsing -->      Con TT (Con TT FF)
forall x . false & true      -- parsing -->      Con (Forall "x" FF) TT

Однако в настоящее время анализатор не производит вывод.Я ценю любую помощь.

Answer 1

Я думаю, что мне удалось решить проблему, перефразировав грамматику, и соединение все еще остается ассоциативно левым:

formula :: Parser Formula
formula = conFormula
        <|> formulaTerm

formulaTerm :: Parser Formula
formulaTerm = roundBrackets formula
            <|> ttFormula
            <|> ffFormula
            <|> varFormula
            <|> forallFormula

conFormula :: Parser Formula
conFormula = 
    buildExpressionParser [[Infix (op "&" >> return Con) AssocLeft]] formulaTerm

Это успешно проанализировало следующее.

Answer 2

Проблема в вашем коде состоит в том, что вы пытаетесь проанализировать formula, для которого первая попытка состоит в анализе formulaCon.Затем он сначала пытается проанализировать formula, т. Е. Вы создаете бесконечную рекурсию без использования какого-либо ввода .

Чтобы решить эту проблему, вы должны структурировать свою грамматику.Определите ваши термины, как это (обратите внимание, что все эти термины потребляют некоторый ввод перед выполнением рекурсии обратно к formula):

formulaTerm = ttFormula
          <|> ffFormula
          <|> varFormula
          <|> forallFormula
          <|> roundBrackets formula

forallFormula = do
  keyword "forall"
  x <- identifier
  op "."
  phi <- formula
  return $ Forall x phi

В этом случае формула представляет собой либо отдельный термин, либо соединение, состоящее из термина,оператор и другая формула.Чтобы убедиться, что все входные данные проанализированы, сначала попытайтесь проанализировать конъюнкцию и - если это не удастся - проанализировать один термин:

formula = (try formulaCon) <|> formulaTerm

Наконец, formulaCon может быть проанализирован следующим образом:

formulaCon = do
  f1 <- formulaTerm
  op "&"
  f2 <- formula
  return $ Con f1 f2

Недостаток этого решения в том, что соединения теперь прямо ассоциативны.