{-# LANGUAGE FlexibleContexts #-}

-- |
-- Module      : AutoProof.Internal.Parser
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Parser for propositional logic formulas
module AutoProof.Internal.Parser
  ( -- * Safe parsing
    parseFormula,
    parseJudgement,

    -- * Unsafe parsing
    unsafeParseFormula,
    unsafeParseJudgement,
  )
where

import AutoProof.Internal.Formula (Formula (And, Iff, Imp, Lit, Not, Or, Var))
import AutoProof.Internal.Judgement
  ( Judgement,
    (|-),
  )
import AutoProof.Internal.Utils.Parser
  ( Parser,
    between,
    chainl1,
    chainr1,
    char,
    eof,
    notFollowedBy,
    oneOf,
    parse,
    sepBy,
    spaces,
    string,
  )
import Control.Applicative (Alternative (empty, many, (<|>)))
import Data.Maybe (fromMaybe)

-- | @('parseFormula' s)@ parses a string @s@ as a propositional formula,
-- returning a @'Just' a@ on success, where @a@ is the parsed formula.
--
-- For a version of 'parseFormula' that does not return a wrapped formula but
-- also throws an error when it cannot parse, see 'unsafeParseFormula'.
--
-- ==== __Conventions__
--
-- * Supported connective symbols:
--
--     * Negation: @"~"@, @"¬"@.
--     * Implication: @"->"@, @"=>"@, @"→"@, @"⇾"@, @"⇒"@ @"⊃"@.
--     * Disjunction: @"|"@, @"\\/"@, @"∨"@, @"+"@
--     * Conjunction: @"&"@, @"/\\"@, @"∧"@, @"^"@, @"*"@
--     * Equivalence: @"\<-\>"@, @"↔"@, @"⇿"@, @"⇔"@
--
-- * Implication is right-associative and has lower precedence than the other
--   connectives.
-- * Equivalence is left-associative and has higher precedence than implication
--   but lower precedence than conjunction and disjunction.
-- * Disjunction is left-associative and has higher precedence than equivalence
--   but lower precedence than conjunction.
-- * Conjunction is left-associative and has highest precedence out of the
--   binary connectives.
-- * Negation binds most tightly, and must immediately precede its argument
--   (i.e., there should not be a space between a negation symbol and the
--   proposition that follows).
-- * Valid variable names begin with a letter (uppercase or lowercase) or an
--   underscore, and may be followed by a letter, underscore, digit, or single
--   quote (a "prime" symbol). The exceptions are the strings @"false"@ and
--   @"true"@, which are parsed as the propositional literals \(\bot\) and
--   \(\top\), respectively.
--
-- ==== __Examples__
--
-- >>> parseFormula "a -> b -> c"
-- Just (Imp (Var "a") (Imp (Var "b") (Var "c")))
--
-- >>> parseFormula "~a | b -> c"
-- Just (Imp (Or (Not (Var "a")) (Var "b")) (Var "c"))
--
-- >>> parseFormula "(a -> b) & ~c"
-- Just (And (Imp (Var "a") (Var "b")) (Not (Var "c")))
parseFormula :: String -> Maybe (Formula String)
parseFormula :: String -> Maybe (Formula String)
parseFormula = Parser (Formula String) -> String -> Maybe (Formula String)
forall a. Parser a -> String -> Maybe a
parse (Parser (Formula String)
formula Parser (Formula String) -> Parser () -> Parser (Formula String)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
eof)

-- | @(parseJudgement s)@ parses a string @s@ as a propositional judgement.
--
-- A valid judgement is made up of an antecedent, a turnstile symbol, and a
-- consequent (in that order). The antecedents are a (potentially empty)
-- comma-separated list of formulas, the turnstile symbol is either @"|-"@ or
-- @"⊢"@, and the consequent is another formula.
--
-- See 'parseFormula' for the specification of valid formulas.
--
-- ==== __Examples__
--
-- >>> parseJudgement "a, a -> b |- b"
-- Just ([Var "a",Imp (Var "a") (Var "b")] |- Var "b")
--
-- >>> parseJudgement "a |- a | b"
-- Just ([Var "a"] |- Or (Var "a") (Var "b"))
parseJudgement :: String -> Maybe (Judgement String)
parseJudgement :: String -> Maybe (Judgement String)
parseJudgement = Parser (Judgement String) -> String -> Maybe (Judgement String)
forall a. Parser a -> String -> Maybe a
parse (Parser (Judgement String)
judgement Parser (Judgement String) -> Parser () -> Parser (Judgement String)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
eof)

-- | @(unsafeParseFormula s)@ parses a string @s@ as a propositional formula,
-- returning the parsed formula on success, and throwing an error on failure.
--
-- See 'parseFormula' for grammar spcecifications.
--
-- ==== __Examples__
--
-- >>> unsafeParseFormula "(a => b) => c"
-- Imp (Imp (Var "a") (Var "b")) (Var "c")
unsafeParseFormula :: String -> Formula String
unsafeParseFormula :: String -> Formula String
unsafeParseFormula = Formula String -> Maybe (Formula String) -> Formula String
forall a. a -> Maybe a -> a
fromMaybe (String -> Formula String
forall a. HasCallStack => String -> a
error "Parse error") (Maybe (Formula String) -> Formula String)
-> (String -> Maybe (Formula String)) -> String -> Formula String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe (Formula String)
parseFormula

-- | @(unsafeParseJudgement s)@ parses a string @s@ as a propositional
-- judgement, returning the parsed judgement on success, and throwing an error
-- on failure.
--
-- See 'parseJudgement' for the specification of valid judgements.
--
-- ==== __Examples__
--
-- >>> unsafeParseJudgement "a, b |- a -> b"
-- [Var "a",Var "b"] |- Imp (Var "a") (Var "b")
--
-- >>> unsafeParseJudgement "a & b |- a"
-- [And (Var "a") (Var "b")] |- Var "a"
unsafeParseJudgement :: String -> Judgement String
unsafeParseJudgement :: String -> Judgement String
unsafeParseJudgement = Judgement String -> Maybe (Judgement String) -> Judgement String
forall a. a -> Maybe a -> a
fromMaybe (String -> Judgement String
forall a. HasCallStack => String -> a
error "Parse error") (Maybe (Judgement String) -> Judgement String)
-> (String -> Maybe (Judgement String))
-> String
-> Judgement String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe (Judgement String)
parseJudgement

-- Top-level parsers

formula :: Parser (Formula String)
formula :: Parser (Formula String)
formula = Parser (Formula String) -> Parser (Formula String)
forall a. Parser a -> Parser a
padded Parser (Formula String)
implication

context :: Parser [Formula String]
context :: Parser [Formula String]
context = Parser (Formula String)
formula Parser (Formula String) -> Parser Char -> Parser [Formula String]
forall a b. Parser a -> Parser b -> Parser [a]
`sepBy` Char -> Parser Char
char ','

judgement :: Parser (Judgement String)
judgement :: Parser (Judgement String)
judgement = [Formula String] -> Formula String -> Judgement String
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
(|-) ([Formula String] -> Formula String -> Judgement String)
-> Parser [Formula String]
-> Parser (Formula String -> Judgement String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Formula String]
context Parser (Formula String -> Judgement String)
-> Parser (Formula String) -> Parser (Judgement String)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
spaces Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser String
turnstileS Parser String -> Parser (Formula String) -> Parser (Formula String)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser (Formula String)
formula)

-- Special symbols

-- Generate a parser out of a collection of strings. The parser will parse any
-- one of the given strings.
symbol :: [String] -> Parser String
symbol :: [String] -> Parser String
symbol [] = Parser String
forall (f :: * -> *) a. Alternative f => f a
empty
symbol (c :: String
c : cs :: [String]
cs)
  -- Special case needed to handle the turnstile symbol "|-" separately from the
  -- disjunction symbol "|".
  | String
c String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "|" = (String -> Parser String
string "|" Parser String -> Parser () -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall a. Parser a -> Parser ()
notFollowedBy (Char -> Parser Char
char '-')) Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [String] -> Parser String
symbol [String]
cs
  | Bool
otherwise = String -> Parser String
string String
c Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [String] -> Parser String
symbol [String]
cs

impS :: Parser String
impS :: Parser String
impS = [String] -> Parser String
symbol ["->", "=>", "→", "⇾", "⇒", "⊃"]

iffS :: Parser String
iffS :: Parser String
iffS = [String] -> Parser String
symbol ["<->", "↔", "⇿", "⇔"]

andS :: Parser String
andS :: Parser String
andS = [String] -> Parser String
symbol ["&", "^", "∧", "/\\", "*"]

orS :: Parser String
orS :: Parser String
orS = [String] -> Parser String
symbol ["|", "∨", "\\/", "+"]

notS :: Parser String
notS :: Parser String
notS = [String] -> Parser String
symbol ["~", "¬"]

falseS :: Parser String
falseS :: Parser String
falseS = [String] -> Parser String
symbol ["⊥", "false"]

trueS :: Parser String
trueS :: Parser String
trueS = [String] -> Parser String
symbol ["⊤", "true"]

turnstileS :: Parser String
turnstileS :: Parser String
turnstileS = [String] -> Parser String
symbol ["|-", "⊢"]

-- Propositional formula components

-- Right-associative nested implications
implication :: Parser (Formula String)
implication :: Parser (Formula String)
implication = Parser (Formula String)
-> Parser (Formula String -> Formula String -> Formula String)
-> Parser (Formula String)
forall a. Parser a -> Parser (a -> a -> a) -> Parser a
chainr1 Parser (Formula String)
equivalence (Parser (Formula String -> Formula String -> Formula String)
-> Parser (Formula String -> Formula String -> Formula String)
forall a. Parser a -> Parser a
padded (Formula String -> Formula String -> Formula String
forall a. Formula a -> Formula a -> Formula a
Imp (Formula String -> Formula String -> Formula String)
-> Parser String
-> Parser (Formula String -> Formula String -> Formula String)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String
impS))

-- Left-associative nested equivalences
equivalence :: Parser (Formula String)
equivalence :: Parser (Formula String)
equivalence = Parser (Formula String)
-> Parser (Formula String -> Formula String -> Formula String)
-> Parser (Formula String)
forall a. Parser a -> Parser (a -> a -> a) -> Parser a
chainl1 Parser (Formula String)
disjunction (Parser (Formula String -> Formula String -> Formula String)
-> Parser (Formula String -> Formula String -> Formula String)
forall a. Parser a -> Parser a
padded (Formula String -> Formula String -> Formula String
forall a. Formula a -> Formula a -> Formula a
Iff (Formula String -> Formula String -> Formula String)
-> Parser String
-> Parser (Formula String -> Formula String -> Formula String)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String
iffS))

-- Left-associative nested disjunctions
disjunction :: Parser (Formula String)
disjunction :: Parser (Formula String)
disjunction = Parser (Formula String)
-> Parser (Formula String -> Formula String -> Formula String)
-> Parser (Formula String)
forall a. Parser a -> Parser (a -> a -> a) -> Parser a
chainl1 Parser (Formula String)
conjunction (Parser (Formula String -> Formula String -> Formula String)
-> Parser (Formula String -> Formula String -> Formula String)
forall a. Parser a -> Parser a
padded (Formula String -> Formula String -> Formula String
forall a. Formula a -> Formula a -> Formula a
Or (Formula String -> Formula String -> Formula String)
-> Parser String
-> Parser (Formula String -> Formula String -> Formula String)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String
orS))

-- Left-associative nested conjunctions
conjunction :: Parser (Formula String)
conjunction :: Parser (Formula String)
conjunction = Parser (Formula String)
-> Parser (Formula String -> Formula String -> Formula String)
-> Parser (Formula String)
forall a. Parser a -> Parser (a -> a -> a) -> Parser a
chainl1 Parser (Formula String)
negation (Parser (Formula String -> Formula String -> Formula String)
-> Parser (Formula String -> Formula String -> Formula String)
forall a. Parser a -> Parser a
padded (Formula String -> Formula String -> Formula String
forall a. Formula a -> Formula a -> Formula a
And (Formula String -> Formula String -> Formula String)
-> Parser String
-> Parser (Formula String -> Formula String -> Formula String)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String
andS))

-- Zero or more consecutive negations
negation :: Parser (Formula String)
negation :: Parser (Formula String)
negation = Parser String
spaces Parser String -> Parser (Formula String) -> Parser (Formula String)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (((Formula String -> Formula String)
 -> (Formula String -> Formula String)
 -> Formula String
 -> Formula String)
-> (Formula String -> Formula String)
-> [Formula String -> Formula String]
-> Formula String
-> Formula String
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Formula String -> Formula String)
-> (Formula String -> Formula String)
-> Formula String
-> Formula String
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Formula String -> Formula String
forall a. a -> a
id ([Formula String -> Formula String]
 -> Formula String -> Formula String)
-> Parser [Formula String -> Formula String]
-> Parser (Formula String -> Formula String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Formula String -> Formula String)
-> Parser [Formula String -> Formula String]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Formula String -> Formula String
forall a. Formula a -> Formula a
Not (Formula String -> Formula String)
-> Parser String -> Parser (Formula String -> Formula String)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String
notS) Parser (Formula String -> Formula String)
-> Parser (Formula String) -> Parser (Formula String)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Formula String)
atom)

atom :: Parser (Formula String)
atom :: Parser (Formula String)
atom = Parser (Formula String) -> Parser (Formula String)
forall a. Parser a -> Parser a
enclosed Parser (Formula String)
formula Parser (Formula String)
-> Parser (Formula String) -> Parser (Formula String)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Formula String)
false Parser (Formula String)
-> Parser (Formula String) -> Parser (Formula String)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Formula String)
true Parser (Formula String)
-> Parser (Formula String) -> Parser (Formula String)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Formula String)
variable

false :: Parser (Formula String)
false :: Parser (Formula String)
false = Bool -> Formula String
forall a. Bool -> Formula a
Lit Bool
False Formula String -> Parser String -> Parser (Formula String)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String
falseS

true :: Parser (Formula String)
true :: Parser (Formula String)
true = Bool -> Formula String
forall a. Bool -> Formula a
Lit Bool
True Formula String -> Parser String -> Parser (Formula String)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String
trueS

variable :: Parser (Formula String)
variable :: Parser (Formula String)
variable = String -> Formula String
forall a. a -> Formula a
Var (String -> Formula String)
-> Parser String -> Parser (Formula String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
name
  where
    name :: Parser String
name = (:) (Char -> String -> String)
-> Parser Char -> Parser (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char
nameStart Parser (String -> String) -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Char -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser Char
nameChar
    nameStart :: Parser Char
nameStart = String -> Parser Char
oneOf (String -> Parser Char) -> String -> Parser Char
forall a b. (a -> b) -> a -> b
$ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: ['a' .. 'z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ ['A' .. 'Z']
    nameChar :: Parser Char
nameChar = Parser Char
nameStart Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Parser Char
oneOf ('\'' Char -> String -> String
forall a. a -> [a] -> [a]
: ['0' .. '9'])

-- Helper functions

padded :: Parser a -> Parser a
padded :: Parser a -> Parser a
padded = Parser String -> Parser String -> Parser a -> Parser a
forall b c a. Parser b -> Parser c -> Parser a -> Parser a
between Parser String
spaces Parser String
spaces

enclosed :: Parser a -> Parser a
enclosed :: Parser a -> Parser a
enclosed = Parser Char -> Parser Char -> Parser a -> Parser a
forall b c a. Parser b -> Parser c -> Parser a -> Parser a
between (Char -> Parser Char
char '(') (Char -> Parser Char
char ')')