168 lines
4.1 KiB
Go
168 lines
4.1 KiB
Go
package schema
|
|
|
|
import (
|
|
"logik/aussagenlogik/formulae"
|
|
parser "logik/grammars/aussagenlogik"
|
|
"regexp"
|
|
|
|
"github.com/antlr/antlr4/runtime/Go/antlr"
|
|
)
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* EXPORTS
|
|
* ---------------------------------------------------------------- */
|
|
|
|
func ParseExpr(u string) formulae.Formula {
|
|
var lexer = createLexer(u)
|
|
var tokenStream = lexerToTokenStream(lexer)
|
|
var prs = parser.NewaussagenlogikParser(tokenStream)
|
|
var t = prs.Start()
|
|
tree := createFormula(t, prs)
|
|
return tree
|
|
}
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* PRIVATE
|
|
* ---------------------------------------------------------------- */
|
|
|
|
func exprToStream(u string) *antlr.InputStream {
|
|
return antlr.NewInputStream(u)
|
|
}
|
|
|
|
func lexerToTokenStream(lexer antlr.Lexer) antlr.TokenStream {
|
|
return antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
|
|
}
|
|
|
|
func createLexer(u string) antlr.Lexer {
|
|
stream := exprToStream(u)
|
|
return parser.NewaussagenlogikLexer(stream)
|
|
}
|
|
|
|
func createFormula(tree antlr.Tree, parser antlr.Parser) formulae.Formula {
|
|
var ant = antlrTree{tree: tree, parser: &parser}
|
|
return ant.toFormula()
|
|
}
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* Struct: antlrTree + Methods
|
|
* ---------------------------------------------------------------- */
|
|
|
|
type antlrTree struct {
|
|
tree antlr.Tree
|
|
parser *antlr.Parser
|
|
}
|
|
|
|
func (ant antlrTree) getChildren() []antlrTree {
|
|
var nodes = ant.tree.GetChildren()
|
|
var subants = make([]antlrTree, len(nodes))
|
|
for i, node := range nodes {
|
|
subants[i] = antlrTree{tree: node, parser: ant.parser}
|
|
}
|
|
return subants
|
|
}
|
|
|
|
func (ant antlrTree) getLabel() string {
|
|
return antlr.TreesGetNodeText(ant.tree, []string{}, *ant.parser)
|
|
}
|
|
|
|
func (ant antlrTree) getTextContent() string {
|
|
var expr string = ""
|
|
var subants = ant.getChildren()
|
|
if len(subants) == 0 {
|
|
return ant.getLabel()
|
|
}
|
|
for _, subant := range subants {
|
|
expr += subant.getTextContent()
|
|
}
|
|
return expr
|
|
}
|
|
|
|
func (ant antlrTree) toFormula() formulae.Formula {
|
|
var label string = ant.getLabel()
|
|
var subants = ant.getChildren()
|
|
var nChildren = len(subants)
|
|
|
|
switch label {
|
|
case "start":
|
|
if nChildren == 1 {
|
|
return subants[0].toFormula()
|
|
}
|
|
case "open":
|
|
if nChildren == 1 {
|
|
return subants[0].toFormula()
|
|
}
|
|
case "closed":
|
|
switch nChildren {
|
|
case 1:
|
|
return subants[0].toFormula()
|
|
// expr = ( expr )
|
|
case 3:
|
|
return subants[1].toFormula()
|
|
}
|
|
case "atomic":
|
|
if nChildren == 1 {
|
|
return subants[0].toFormula()
|
|
}
|
|
case "taut":
|
|
return formulae.Tautology
|
|
case "contradiction":
|
|
return formulae.Contradiction
|
|
case "atom":
|
|
name := ant.getTextContent()
|
|
return formulae.Atom(name)
|
|
case "generic":
|
|
re := regexp.MustCompile(`^{|}$`)
|
|
name := string(re.ReplaceAll([]byte(ant.getTextContent()), []byte("")))
|
|
return formulae.Generic(name)
|
|
case "not":
|
|
// NOTE: expr = ! expr
|
|
if nChildren == 2 {
|
|
return formulae.Negation(subants[1].toFormula())
|
|
}
|
|
case "and2":
|
|
// NOTE: expr = expr && expr
|
|
if nChildren == 3 {
|
|
return formulae.Conjunction2(subants[0].toFormula(), subants[2].toFormula())
|
|
}
|
|
case "or2":
|
|
// NOTE: expr = expr || expr
|
|
if nChildren == 3 {
|
|
return formulae.Disjunction2(subants[0].toFormula(), subants[2].toFormula())
|
|
}
|
|
case "implies":
|
|
// NOTE: expr = expr -> expr
|
|
if nChildren == 3 {
|
|
return formulae.Implies(subants[0].toFormula(), subants[2].toFormula())
|
|
}
|
|
case "iff":
|
|
// NOTE: expr = expr <=> expr
|
|
if nChildren == 3 {
|
|
return formulae.DoubleImplication(subants[0].toFormula(), subants[2].toFormula())
|
|
}
|
|
case "and", "or":
|
|
// NOTE: expr = expr op expr op ... op expr
|
|
var n int = int((len(subants) + 1) / 2)
|
|
if nChildren == 2*n-1 && n >= 2 {
|
|
var subtrees = make([]formulae.Formula, n)
|
|
var isSymb bool = true
|
|
var i int = 0
|
|
for _, subant := range subants {
|
|
if isSymb {
|
|
subtrees[i] = subant.toFormula()
|
|
i++
|
|
}
|
|
// NOTE: infix notation: alternatives between expression and symbol
|
|
isSymb = !isSymb
|
|
}
|
|
switch label {
|
|
case "and":
|
|
return formulae.Conjunction(subtrees)
|
|
case "or":
|
|
return formulae.Disjunction(subtrees)
|
|
}
|
|
}
|
|
}
|
|
|
|
panic("Could not parse expression")
|
|
}
|