Skip to content
Snippets Groups Projects
Commit ccd5990a authored by Katja Goltsova's avatar Katja Goltsova Committed by Viktor Kunčak
Browse files

Add a parser for LISA kernel

Implement a parser for first order logic with equality and schematic functions/predicates
using scallion.
parent 74fce621
No related branches found
No related tags found
4 merge requests!62Easy tactics,!58Easy tactics,!54Front integration,!53Front integration
package lisa.utils
import lisa.kernel.fol.FOL
import lisa.kernel.fol.FOL._
import lisa.kernel.fol.FOL.equality
import lisa.kernel.proof.SequentCalculus.*
import scallion.*
import silex.*
object Parser {
class ParserException(msg: String) extends Exception(msg)
object UnreachableException extends ParserException("Internal error: expected unreachable")
def parseSequent(s: String): Sequent = s.split("⊢") match {
case Array(fs) => Sequent(Set(), fs.split(";").map(parseFormula).toSet)
case Array(fsl, fsr) => Sequent(fsl.split(";").map(parseFormula).toSet, fsr.split(";").map(parseFormula).toSet)
case _ => throw ParserException("Invalid sequent")
}
private def extractParseResult[T](r: FormulaParser.ParseResult[T]): T = r match {
case FormulaParser.Parsed(value, _) => value
// TODO: at position
// TODO: leaking implementation? Should I sugar tokens?
case FormulaParser.UnexpectedToken(token, _) => throw ParserException(s"Unexpected input: $token")
case FormulaParser.UnexpectedEnd(_) => throw ParserException(s"Unexpected end of input")
}
def parseFormula(s: String): Formula =
extractParseResult(FormulaParser(FormulaLexer(s.iterator)))
def parseTerm(s: String): Term =
extractParseResult(FormulaParser.parseTerm(FormulaLexer(s.iterator)))
private[Parser] sealed abstract class FormulaToken
case object ForallToken extends FormulaToken
case object ExistsOneToken extends FormulaToken
case object ExistsToken extends FormulaToken
case object DotToken extends FormulaToken
case object AndToken extends FormulaToken
case object OrToken extends FormulaToken
case object ImpliesToken extends FormulaToken
case object IffToken extends FormulaToken
case object NegationToken extends FormulaToken
case object EqualityToken extends FormulaToken
// Constant functions and predicates
case class ConstantToken(id: String) extends FormulaToken
// Variables, schematic functions and predicates
case class SchematicToken(id: String) extends FormulaToken
case class ParenthesisToken(isOpen: Boolean) extends FormulaToken
case object CommaToken extends FormulaToken
case object SpaceToken extends FormulaToken
private[Parser] object FormulaLexer extends Lexers with CharLexers {
type Token = FormulaToken
// TODO: add positions ==> ranges to tokens
type Position = Unit
private val lexer = Lexer(
elem('∀') |> { _ => ForallToken },
word("∃!") |> { _ => ExistsOneToken },
elem('∃') |> { _ => ExistsToken },
elem('.') |> { _ => DotToken },
elem('=') |> { _ => EqualityToken },
elem('∧') | word("/\\") |> { _ => AndToken },
elem('∨') | word("\\/") |> { _ => OrToken },
elem('⇒') | word("=>") | word("==>") |> { _ => ImpliesToken },
elem('↔') | word("<=>") | word("<==>") |> { _ => IffToken },
elem('¬') | elem('!') |> { _ => NegationToken },
elem('(') |> ParenthesisToken(true),
elem(')') |> ParenthesisToken(false),
elem(',') |> CommaToken,
many1(whiteSpace) |> SpaceToken,
elem('?') ~ many1(elem(_.isLetter) | elem('_') | elem(_.isDigit) | elem('\'')) |> { cs =>
// drop the '?'
SchematicToken(cs.drop(1).mkString)
},
many1(elem(_.isLetter) | elem('_') | elem(_.isDigit)) |> { cs => ConstantToken(cs.mkString) }
) onError { (cs, _) =>
throw ParserException(s"Unexpected input: ${cs.mkString}")
}
def apply(it: Iterator[Char]): Iterator[Token] = {
val source = Source.fromIterator(it, NoPositioner)
lexer(source).filter(_ != SpaceToken)
}
}
private[Parser] object FormulaParser extends Parsers {
sealed abstract class TokenKind
// and, or are both (left) associative and bind tighter than implies, iff
case object AndKind extends TokenKind
case object OrKind extends TokenKind
// implies, iff are both non-associative and are of equal priority, lower than and, or
case object TopLevelConnectorKind extends TokenKind
case object NegationKind extends TokenKind
case object FunctionOrPredicateKind extends TokenKind
case object EqualityKind extends TokenKind
case object CommaKind extends TokenKind
case class ParenthesisKind(isOpen: Boolean) extends TokenKind
case object BinderKind extends TokenKind
case object DotKind extends TokenKind
case object OtherKind extends TokenKind
type Token = lisa.utils.Parser.FormulaToken
type Kind = TokenKind
// can safely skip tokens which were mapped to unit with elem(kind).unit(token)
import SafeImplicits._
def getKind(t: Token): Kind = t match {
case AndToken => AndKind
case OrToken => OrKind
case IffToken | ImpliesToken => TopLevelConnectorKind
case NegationToken => NegationKind
case _: ConstantToken | _: SchematicToken => FunctionOrPredicateKind
case EqualityToken => EqualityKind
case CommaToken => CommaKind
case ParenthesisToken(isOpen) => ParenthesisKind(isOpen)
case ExistsToken | ExistsOneToken | ForallToken => BinderKind
case DotToken => DotKind
case SpaceToken => OtherKind
}
/////////////////////// SEPARATORS ////////////////////////////////
def parens(isOpen: Boolean): Syntax[Unit] =
elem(ParenthesisKind(isOpen)).unit(ParenthesisToken(isOpen))
val open: Syntax[Unit] = parens(true)
val closed: Syntax[Unit] = parens(false)
val comma: Syntax[Unit] = elem(CommaKind).unit(CommaToken)
val eq: Syntax[Unit] = elem(EqualityKind).unit(EqualityToken)
///////////////////////////////////////////////////////////////////
//////////////////////// LABELS ///////////////////////////////////
val toplevelConnector: Syntax[Implies.type | Iff.type] = accept(TopLevelConnectorKind) {
case ImpliesToken => Implies
case IffToken => Iff
}
val negation: Syntax[Neg.type] = accept(NegationKind) { case NegationToken => Neg }
///////////////////////////////////////////////////////////////////
//////////////////////// TERMS ////////////////////////////////////
lazy val args: Syntax[Seq[Term]] = recursive(open.skip ~ repsep(term, comma) ~ closed.skip)
lazy val term: Syntax[Term] = recursive((elem(FunctionOrPredicateKind) ~ opt(args)).map {
case ConstantToken(id) ~ maybeArgs =>
val args = maybeArgs.getOrElse(Seq())
FunctionTerm(ConstantFunctionLabel(id, args.length), args)
case SchematicToken(id) ~ Some(args) => FunctionTerm(SchematicFunctionLabel(id, args.length), args)
case SchematicToken(id) ~ None => VariableTerm(VariableLabel(id))
case _ => throw UnreachableException
})
///////////////////////////////////////////////////////////////////
//////////////////////// FORMULAS /////////////////////////////////
// can appear without parentheses
lazy val simpleFormula: Syntax[Formula] = predicate.up[Formula] | negated.up[Formula]
lazy val subformula: Syntax[Formula] = simpleFormula | open.skip ~ formula ~ closed.skip
def createFunctionTerm(label: Token, args: Seq[Term]): Term = label match {
case ConstantToken(id) => FunctionTerm(ConstantFunctionLabel(id, args.size), args)
case SchematicToken(id) =>
args match {
case Seq() => VariableTerm(VariableLabel(id))
case _ => FunctionTerm(SchematicFunctionLabel(id, args.size), args)
}
case _ => throw UnreachableException
}
val predicate: Syntax[PredicateFormula] = (elem(FunctionOrPredicateKind) ~ opt(args) ~ opt(eq.skip ~ elem(FunctionOrPredicateKind) ~ opt(args))).map {
// predicate application
case ConstantToken(id) ~ maybeArgs ~ None =>
val args = maybeArgs.getOrElse(Seq())
PredicateFormula(ConstantPredicateLabel(id, args.size), args)
case SchematicToken(id) ~ Some(args) ~ None => PredicateFormula(SchematicNPredicateLabel(id, args.size), args)
case SchematicToken(id) ~ None ~ None => PredicateFormula(VariableFormulaLabel(id), Seq())
// equality of two function applications
case fun1 ~ args1 ~ Some(fun2 ~ args2) =>
PredicateFormula(FOL.equality, Seq(createFunctionTerm(fun1, args1.getOrElse(Seq())), createFunctionTerm(fun2, args2.getOrElse(Seq()))))
case _ => throw UnreachableException
}
val negated: Syntax[ConnectorFormula] = recursive {
(negation ~ subformula).map { case n ~ f =>
ConnectorFormula(n, Seq(f))
}
}
// 'and' has higher priority than 'or'
val connectorFormula: Syntax[Formula] = operators(subformula)(
elem(AndKind) map {
case AndToken => And
case _ => throw UnreachableException
} is LeftAssociative,
elem(OrKind) map {
case OrToken => Or
case _ => throw UnreachableException
} is LeftAssociative
)(
{ case (l, conn, r) =>
ConnectorFormula(conn, Seq(l, r))
},
{ case ConnectorFormula(conn, Seq(l, r)) =>
(l, conn, r)
}
)
def getBinderFormulaConstructor(binders: Seq[BinderLabel ~ VariableLabel]): Formula => Formula = binders match {
case Seq() => f => f
case (binder ~ boundVar) +: rest => f => BinderFormula(binder, boundVar, getBinderFormulaConstructor(rest)(f))
}
// consume binders and return a function that constructs a BinderFormula given the inner formula
val binders: Syntax[Formula => Formula] = many(accept(BinderKind) {
case ExistsToken => Exists
case ExistsOneToken => ExistsOne
case ForallToken => Forall
} ~ accept(FunctionOrPredicateKind) {
case ConstantToken(id) => VariableLabel(id)
case SchematicToken(id) => VariableLabel(id)
} ~ elem(DotKind).unit(DotToken).skip) map getBinderFormulaConstructor
lazy val formula: Syntax[Formula] = recursive {
(binders ~ connectorFormula ~ opt(toplevelConnector ~ connectorFormula)) map { case binderFormulaConstructor ~ f ~ rest =>
rest match {
case Some(conn ~ f2) => binderFormulaConstructor(ConnectorFormula(conn, Seq(f, f2)))
case None => binderFormulaConstructor(f)
}
}
}
///////////////////////////////////////////////////////////////////
val parser: FormulaParser.Parser[FOL.Formula] = Parser(formula)
val termParser: FormulaParser.Parser[FOL.Term] = Parser(term)
def apply(it: Iterator[Token]): ParseResult[Formula] = parseFormula(it)
def parseFormula(it: Iterator[Token]): ParseResult[Formula] = parser(it)
def parseTerm(it: Iterator[Token]): ParseResult[Term] = termParser(it)
}
}
package lisa.utils
import lisa.kernel.fol.FOL.*
import org.scalatest.funsuite.AnyFunSuite
class ParserTest extends AnyFunSuite {
val (a, b, c) = (ConstantPredicateLabel("a", 0), ConstantPredicateLabel("b", 0), ConstantPredicateLabel("c", 0))
val (x, y, z) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
val (cx, cy, cz) = (ConstantFunctionLabel("x", 0), ConstantFunctionLabel("y", 0), ConstantFunctionLabel("z", 0))
val (f0, f1, f2, f3) = (ConstantFunctionLabel("f", 0), ConstantFunctionLabel("f", 1), ConstantFunctionLabel("f", 2), ConstantFunctionLabel("f", 3))
val (sf1, sf2, sf3) = (SchematicFunctionLabel("f", 1), SchematicFunctionLabel("f", 2), SchematicFunctionLabel("f", 3))
given Conversion[PredicateLabel, PredicateFormula] = PredicateFormula(_, Seq.empty)
given Conversion[ConstantFunctionLabel, FunctionTerm] = FunctionTerm(_, Seq())
given Conversion[VariableLabel, VariableTerm] = VariableTerm.apply
test("constant") {
assert(Parser.parseTerm("x") == FunctionTerm(cx, Seq()))
}
test("variable") {
assert(Parser.parseTerm("?x") == VariableTerm(x))
}
test("constant function application") {
assert(Parser.parseTerm("f()") == FunctionTerm(f0, Seq()))
assert(Parser.parseTerm("f(x)") == FunctionTerm(f1, Seq(cx)))
assert(Parser.parseTerm("f(x, y)") == FunctionTerm(f2, Seq(cx, cy)))
assert(Parser.parseTerm("f(x, y, z)") == FunctionTerm(f3, Seq(cx, cy, cz)))
assert(Parser.parseTerm("f(?x)") == FunctionTerm(f1, Seq(x)))
assert(Parser.parseTerm("f(?x, ?y)") == FunctionTerm(f2, Seq(x, y)))
assert(Parser.parseTerm("f(?x, ?y, ?z)") == FunctionTerm(f3, Seq(x, y, z)))
}
test("schematic function application") {
// Parser.parseTerm("?f()") -- schematic functions of 0 arguments do not exist, those are variables
assert(Parser.parseTerm("?f(x)") == FunctionTerm(sf1, Seq(cx)))
assert(Parser.parseTerm("?f(x, y)") == FunctionTerm(sf2, Seq(cx, cy)))
assert(Parser.parseTerm("?f(x, y, z)") == FunctionTerm(sf3, Seq(cx, cy, cz)))
assert(Parser.parseTerm("?f(?x)") == FunctionTerm(sf1, Seq(x)))
assert(Parser.parseTerm("?f(?x, ?y)") == FunctionTerm(sf2, Seq(x, y)))
assert(Parser.parseTerm("?f(?x, ?y, ?z)") == FunctionTerm(sf3, Seq(x, y, z)))
}
test("nested function application") {
assert(Parser.parseTerm("?f(?f(?x), ?y)") == FunctionTerm(sf2, Seq(FunctionTerm(sf1, Seq(x)), y)))
}
test("0-ary predicate") {
assert(Parser.parseFormula("a") == PredicateFormula(ConstantPredicateLabel("a", 0), Seq()))
assert(Parser.parseFormula("a()") == PredicateFormula(ConstantPredicateLabel("a", 0), Seq()))
}
test("predicate application") {
assert(Parser.parseFormula("p(x, y, z)") == PredicateFormula(ConstantPredicateLabel("p", 3), Seq(cx, cy, cz)))
assert(Parser.parseFormula("p(?x, ?y, ?z)") == PredicateFormula(ConstantPredicateLabel("p", 3), Seq(x, y, z)))
}
test("equality") {
assert(Parser.parseFormula("(x = x)") == PredicateFormula(equality, Seq(cx, cx)))
assert(Parser.parseFormula("x = x") == PredicateFormula(equality, Seq(cx, cx)))
assert(Parser.parseFormula("a ∧ (?x = ?x)") == ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x)))))
}
test("unicode connectors") {
assert(Parser.parseFormula("¬a") == ConnectorFormula(Neg, Seq(a)))
assert(Parser.parseFormula("a ∧ b") == ConnectorFormula(And, Seq(a, b)))
assert(Parser.parseFormula("a ∨ b") == ConnectorFormula(Or, Seq(a, b)))
assert(Parser.parseFormula("a ⇒ b") == ConnectorFormula(Implies, Seq(a, b)))
assert(Parser.parseFormula("a ↔ b") == ConnectorFormula(Iff, Seq(a, b)))
}
test("ascii connectors") {
assert(Parser.parseFormula("!a") == ConnectorFormula(Neg, Seq(a)))
assert(Parser.parseFormula("a /\\ b") == ConnectorFormula(And, Seq(a, b)))
assert(Parser.parseFormula("a \\/ b") == ConnectorFormula(Or, Seq(a, b)))
assert(Parser.parseFormula("a => b") == ConnectorFormula(Implies, Seq(a, b)))
assert(Parser.parseFormula("a ==> b") == ConnectorFormula(Implies, Seq(a, b)))
assert(Parser.parseFormula("a <=> b") == ConnectorFormula(Iff, Seq(a, b)))
}
test("connector associativity") {
assert(Parser.parseFormula("a ∧ b ∧ c") == ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, b)), c)))
assert(Parser.parseFormula("a ∨ b ∨ c") == ConnectorFormula(Or, Seq(ConnectorFormula(Or, Seq(a, b)), c)))
}
test("connector priority") {
// a ∨ (b ∧ c)
assert(Parser.parseFormula("a ∨ b ∧ c") == ConnectorFormula(Or, Seq(a, ConnectorFormula(And, Seq(b, c)))))
// (a ∧ b) ∨ c
assert(Parser.parseFormula("a ∧ b ∨ c") == ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, b)), c)))
// (a ∧ b) => c
assert(Parser.parseFormula("a ∧ b => c") == ConnectorFormula(Implies, Seq(ConnectorFormula(And, Seq(a, b)), c)))
// a => (b ∧ c)
assert(Parser.parseFormula("a => b ∧ c") == ConnectorFormula(Implies, Seq(a, ConnectorFormula(And, Seq(b, c)))))
// (a ∨ b) => c
assert(Parser.parseFormula("a ∨ b => c") == ConnectorFormula(Implies, Seq(ConnectorFormula(Or, Seq(a, b)), c)))
// a => (b ∨ c)
assert(Parser.parseFormula("a => b ∨ c") == ConnectorFormula(Implies, Seq(a, ConnectorFormula(Or, Seq(b, c)))))
// (a ∧ b) <=> c
assert(Parser.parseFormula("a ∧ b <=> c") == ConnectorFormula(Iff, Seq(ConnectorFormula(And, Seq(a, b)), c)))
// a <=> (b ∧ c)
assert(Parser.parseFormula("a <=> b ∧ c") == ConnectorFormula(Iff, Seq(a, ConnectorFormula(And, Seq(b, c)))))
// (a ∨ b) <=> c
assert(Parser.parseFormula("a ∨ b <=> c") == ConnectorFormula(Iff, Seq(ConnectorFormula(Or, Seq(a, b)), c)))
// a <=> (b ∨ c)
assert(Parser.parseFormula("a <=> b ∨ c") == ConnectorFormula(Iff, Seq(a, ConnectorFormula(Or, Seq(b, c)))))
}
test("connector parentheses") {
assert(Parser.parseFormula("(a ∨ b) ∧ c") == ConnectorFormula(And, Seq(ConnectorFormula(Or, Seq(a, b)), c)))
assert(Parser.parseFormula("a ∧ (b ∨ c)") == ConnectorFormula(And, Seq(a, ConnectorFormula(Or, Seq(b, c)))))
}
test("quantifiers") {
assert(Parser.parseFormula("∀ ?x. (p)") == BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
assert(Parser.parseFormula("∃ ?x. (p)") == BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
assert(Parser.parseFormula("∃! ?x. (p)") == BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
assert(Parser.parseFormula("∀ ?x. p") == BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
assert(Parser.parseFormula("∃ ?x. p") == BinderFormula(Exists, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
assert(Parser.parseFormula("∃! ?x. p") == BinderFormula(ExistsOne, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 0), Seq())))
}
test("nested quantifiers") {
assert(Parser.parseFormula("∀x. ∃y. ∃!z. a") == BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a))))
}
test("quantifier parentheses") {
assert(Parser.parseFormula("∀x. b ∧ a") == BinderFormula(Forall, x, ConnectorFormula(And, Seq(b, a))))
assert(
Parser.parseFormula("∀ ?x. p(?x) ∧ q(?x)") == BinderFormula(
Forall,
x,
ConnectorFormula(And, Seq(PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x)), PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))))
)
)
assert(Parser.parseFormula("(∀x. b) ∧ a") == ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a)))
assert(
Parser.parseFormula("(∀ ?x. p(?x)) ∧ q(?x)") == ConnectorFormula(
And,
Seq(
BinderFormula(Forall, VariableLabel("x"), PredicateFormula(ConstantPredicateLabel("p", 1), Seq(x))),
PredicateFormula(ConstantPredicateLabel("q", 1), Seq(x))
)
)
)
assert(Parser.parseFormula("a ∧ (∀x. b) ∨ a") == ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a)))
assert(Parser.parseFormula("(a ∧ (∀x. b)) ∧ a") == ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a)))
}
test("complex formulas with connectors") {
assert(Parser.parseFormula("¬(a ∨ b)") == ConnectorFormula(Neg, Seq(ConnectorFormula(Or, Seq(a, b)))))
assert(Parser.parseFormula("¬(¬a)") == ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(a)))))
assert(Parser.parseFormula("¬¬a") == ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(a)))))
assert(Parser.parseFormula("¬¬(a ∧ b)") == ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(ConnectorFormula(And, Seq(a, b)))))))
assert(Parser.parseFormula("¬a ∧ ¬b ∧ ¬c") == ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(a)), ConnectorFormula(Neg, Seq(b)))), ConnectorFormula(Neg, Seq(c)))))
}
test("complex formulas") {
assert(Parser.parseFormula("∀x. ?x = ?x") == BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x))))
}
test("parser limitations") {
// TODO: more specific error reporting check
assertThrows[Parser.ParserException](Parser.parseFormula("(a ∧ ∀x. b) ∧ a"))
}
test("sequent") {
fail("not implemented")
}
test("sequents from Mapping proof") {
fail("not implemented")
}
test("sequents from Peano proof") {
fail("not implemented")
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment