sjkillen
/
wfs-operator-experiment
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

aaaaaaaa

This commit is contained in:
Spencer Killen 2023-01-12 15:32:51 -07:00
parent 10506e3898
commit a1f9acc6f9
Signed by: sjkillen
GPG Key ID: F307025B65C860BA
15 changed files with 141 additions and 142 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.vscode/settings.json vendored Normal file
View File

@ -0,0 +1,3 @@
{
"python.formatting.provider": "black"
}

18
AST.py
View File

@ -7,20 +7,24 @@ from operator import itemgetter
from functools import reduce, partial from functools import reduce, partial
from enum import Enum from enum import Enum
@dataclass @dataclass
class LRule: class LRule:
head: tuple[str, ...] head: tuple[str, ...]
pbody: tuple[str, ...] pbody: tuple[str, ...]
nbody: tuple[str, ...] nbody: tuple[str, ...]
@dataclass @dataclass
class OFormula: class OFormula:
pass pass
class OConst(Enum): class OConst(Enum):
TRUE = OFormula() TRUE = OFormula()
FALSE = OFormula() FALSE = OFormula()
@dataclass @dataclass
class OBinary(OFormula): class OBinary(OFormula):
operator: str operator: str
@ -40,6 +44,7 @@ class KB:
rules: list[LRule] rules: list[LRule]
atoms: set[str] atoms: set[str]
class HMKNFVisitor(ParseTreeVisitor): class HMKNFVisitor(ParseTreeVisitor):
def __init__(self) -> None: def __init__(self) -> None:
self.atoms = set() self.atoms = set()
@ -47,7 +52,9 @@ class HMKNFVisitor(ParseTreeVisitor):
def visitKb(self, ctx: HMKNFParser.KbContext): def visitKb(self, ctx: HMKNFParser.KbContext):
orules = (self.visit(orule) for orule in ctx.orule()) if ctx.orule() else () orules = (self.visit(orule) for orule in ctx.orule()) if ctx.orule() else ()
ont = reduce(partial(OBinary, "&"), orules, OConst.TRUE) ont = reduce(partial(OBinary, "&"), orules, OConst.TRUE)
lrules = tuple(self.visit(lrule) for lrule in ctx.lrule()) if ctx.lrule() else () lrules = (
tuple(self.visit(lrule) for lrule in ctx.lrule()) if ctx.lrule() else ()
)
return KB(ont, lrules, self.atoms) return KB(ont, lrules, self.atoms)
def visitLrule(self, ctx: HMKNFParser.LruleContext): def visitLrule(self, ctx: HMKNFParser.LruleContext):
@ -67,11 +74,10 @@ class HMKNFVisitor(ParseTreeVisitor):
def visitOrule(self, ctx: HMKNFParser.OruleContext): def visitOrule(self, ctx: HMKNFParser.OruleContext):
return self.visit(ctx.oformula()) return self.visit(ctx.oformula())
def visitDisj(self, ctx: HMKNFParser.DisjContext): def visitDisjOrConj(self, ctx: HMKNFParser.DisjOrConjContext):
return OBinary("|", self.visit(ctx.oformula(0)), self.visit(ctx.oformula(1))) return OBinary(
ctx.operator.text, self.visit(ctx.oformula(0)), self.visit(ctx.oformula(1))
def visitConj(self, ctx: HMKNFParser.ConjContext): )
return OBinary("&", self.visit(ctx.oformula(0)), self.visit(ctx.oformula(1)))
def visitParenth(self, ctx: HMKNFParser.ParenthContext): def visitParenth(self, ctx: HMKNFParser.ParenthContext):
return self.visit(ctx.oformula()) return self.visit(ctx.oformula())

11
HMKNF.g4
View File

@ -10,11 +10,10 @@ body: ':-' (katom (',' katom)*)?;
orule: oformula '.'; orule: oformula '.';
oformula: oformula:
'(' oformula ')' # parenth '(' oformula ')' # parenth
| oatom # literal | oatom # literal
| oformula '->' oformula # imp | oformula (operator = ('|' | '&')) oformula # disjOrConj
| oformula '|' oformula # disj | oformula '->' oformula # imp;
| oformula '&' oformula # conj;
katom: patom | natom; katom: patom | natom;
oatom: patom | fatom; oatom: patom | fatom;
@ -22,4 +21,4 @@ patom: IDENTIFIER;
natom: 'not' IDENTIFIER; natom: 'not' IDENTIFIER;
fatom: '-' IDENTIFIER; fatom: '-' IDENTIFIER;
IDENTIFIER: [a-z][A-Za-z0-9]*; IDENTIFIER: [a-z'][A-Za-z0-9']*;

2
Makefile
View File

@ -11,7 +11,7 @@ antlr4.jar:
wget https://www.antlr.org/download/antlr-4.10.1-complete.jar wget https://www.antlr.org/download/antlr-4.10.1-complete.jar
mv *.jar antlr4.jar mv *.jar antlr4.jar
.PHONY: cleaneB .PHONY: clean
clean: clean:
rm -rf grammars rm -rf grammars

4
grammars/HMKNF.interp
View File

@ -5,9 +5,9 @@ null
':-' ':-'
'(' '('
')' ')'
'->'
'|' '|'
'&' '&'
'->'
'not' 'not'
'-' '-'
null null
@ -43,4 +43,4 @@ fatom
atn: atn:
[4, 1, 12, 99, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 2, 10, 7, 10, 1, 0, 1, 0, 5, 0, 25, 8, 0, 10, 0, 12, 0, 28, 9, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 35, 8, 1, 1, 1, 1, 1, 1, 2, 1, 2, 1, 2, 5, 2, 42, 8, 2, 10, 2, 12, 2, 45, 9, 2, 1, 3, 1, 3, 1, 3, 1, 3, 5, 3, 51, 8, 3, 10, 3, 12, 3, 54, 9, 3, 3, 3, 56, 8, 3, 1, 4, 1, 4, 1, 4, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 3, 5, 67, 8, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 5, 5, 78, 8, 5, 10, 5, 12, 5, 81, 9, 5, 1, 6, 1, 6, 3, 6, 85, 8, 6, 1, 7, 1, 7, 3, 7, 89, 8, 7, 1, 8, 1, 8, 1, 9, 1, 9, 1, 9, 1, 10, 1, 10, 1, 10, 1, 10, 0, 1, 10, 11, 0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 0, 0, 100, 0, 26, 1, 0, 0, 0, 2, 34, 1, 0, 0, 0, 4, 38, 1, 0, 0, 0, 6, 46, 1, 0, 0, 0, 8, 57, 1, 0, 0, 0, 10, 66, 1, 0, 0, 0, 12, 84, 1, 0, 0, 0, 14, 88, 1, 0, 0, 0, 16, 90, 1, 0, 0, 0, 18, 92, 1, 0, 0, 0, 20, 95, 1, 0, 0, 0, 22, 25, 3, 2, 1, 0, 23, 25, 3, 8, 4, 0, 24, 22, 1, 0, 0, 0, 24, 23, 1, 0, 0, 0, 25, 28, 1, 0, 0, 0, 26, 24, 1, 0, 0, 0, 26, 27, 1, 0, 0, 0, 27, 1, 1, 0, 0, 0, 28, 26, 1, 0, 0, 0, 29, 30, 3, 4, 2, 0, 30, 31, 3, 6, 3, 0, 31, 35, 1, 0, 0, 0, 32, 35, 3, 4, 2, 0, 33, 35, 3, 6, 3, 0, 34, 29, 1, 0, 0, 0, 34, 32, 1, 0, 0, 0, 34, 33, 1, 0, 0, 0, 35, 36, 1, 0, 0, 0, 36, 37, 5, 1, 0, 0, 37, 3, 1, 0, 0, 0, 38, 43, 5, 12, 0, 0, 39, 40, 5, 2, 0, 0, 40, 42, 5, 12, 0, 0, 41, 39, 1, 0, 0, 0, 42, 45, 1, 0, 0, 0, 43, 41, 1, 0, 0, 0, 43, 44, 1, 0, 0, 0, 44, 5, 1, 0, 0, 0, 45, 43, 1, 0, 0, 0, 46, 55, 5, 3, 0, 0, 47, 52, 3, 12, 6, 0, 48, 49, 5, 2, 0, 0, 49, 51, 3, 12, 6, 0, 50, 48, 1, 0, 0, 0, 51, 54, 1, 0, 0, 0, 52, 50, 1, 0, 0, 0, 52, 53, 1, 0, 0, 0, 53, 56, 1, 0, 0, 0, 54, 52, 1, 0, 0, 0, 55, 47, 1, 0, 0, 0, 55, 56, 1, 0, 0, 0, 56, 7, 1, 0, 0, 0, 57, 58, 3, 10, 5, 0, 58, 59, 5, 1, 0, 0, 59, 9, 1, 0, 0, 0, 60, 61, 6, 5, -1, 0, 61, 62, 5, 4, 0, 0, 62, 63, 3, 10, 5, 0, 63, 64, 5, 5, 0, 0, 64, 67, 1, 0, 0, 0, 65, 67, 3, 14, 7, 0, 66, 60, 1, 0, 0, 0, 66, 65, 1, 0, 0, 0, 67, 79, 1, 0, 0, 0, 68, 69, 10, 3, 0, 0, 69, 70, 5, 6, 0, 0, 70, 78, 3, 10, 5, 4, 71, 72, 10, 2, 0, 0, 72, 73, 5, 7, 0, 0, 73, 78, 3, 10, 5, 3, 74, 75, 10, 1, 0, 0, 75, 76, 5, 8, 0, 0, 76, 78, 3, 10, 5, 2, 77, 68, 1, 0, 0, 0, 77, 71, 1, 0, 0, 0, 77, 74, 1, 0, 0, 0, 78, 81, 1, 0, 0, 0, 79, 77, 1, 0, 0, 0, 79, 80, 1, 0, 0, 0, 80, 11, 1, 0, 0, 0, 81, 79, 1, 0, 0, 0, 82, 85, 3, 16, 8, 0, 83, 85, 3, 18, 9, 0, 84, 82, 1, 0, 0, 0, 84, 83, 1, 0, 0, 0, 85, 13, 1, 0, 0, 0, 86, 89, 3, 16, 8, 0, 87, 89, 3, 20, 10, 0, 88, 86, 1, 0, 0, 0, 88, 87, 1, 0, 0, 0, 89, 15, 1, 0, 0, 0, 90, 91, 5, 12, 0, 0, 91, 17, 1, 0, 0, 0, 92, 93, 5, 9, 0, 0, 93, 94, 5, 12, 0, 0, 94, 19, 1, 0, 0, 0, 95, 96, 5, 10, 0, 0, 96, 97, 5, 12, 0, 0, 97, 21, 1, 0, 0, 0, 11, 24, 26, 34, 43, 52, 55, 66, 77, 79, 84, 88] [4, 1, 12, 96, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 2, 10, 7, 10, 1, 0, 1, 0, 5, 0, 25, 8, 0, 10, 0, 12, 0, 28, 9, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 35, 8, 1, 1, 1, 1, 1, 1, 2, 1, 2, 1, 2, 5, 2, 42, 8, 2, 10, 2, 12, 2, 45, 9, 2, 1, 3, 1, 3, 1, 3, 1, 3, 5, 3, 51, 8, 3, 10, 3, 12, 3, 54, 9, 3, 3, 3, 56, 8, 3, 1, 4, 1, 4, 1, 4, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 3, 5, 67, 8, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 5, 5, 75, 8, 5, 10, 5, 12, 5, 78, 9, 5, 1, 6, 1, 6, 3, 6, 82, 8, 6, 1, 7, 1, 7, 3, 7, 86, 8, 7, 1, 8, 1, 8, 1, 9, 1, 9, 1, 9, 1, 10, 1, 10, 1, 10, 1, 10, 0, 1, 10, 11, 0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 0, 1, 1, 0, 6, 7, 96, 0, 26, 1, 0, 0, 0, 2, 34, 1, 0, 0, 0, 4, 38, 1, 0, 0, 0, 6, 46, 1, 0, 0, 0, 8, 57, 1, 0, 0, 0, 10, 66, 1, 0, 0, 0, 12, 81, 1, 0, 0, 0, 14, 85, 1, 0, 0, 0, 16, 87, 1, 0, 0, 0, 18, 89, 1, 0, 0, 0, 20, 92, 1, 0, 0, 0, 22, 25, 3, 2, 1, 0, 23, 25, 3, 8, 4, 0, 24, 22, 1, 0, 0, 0, 24, 23, 1, 0, 0, 0, 25, 28, 1, 0, 0, 0, 26, 24, 1, 0, 0, 0, 26, 27, 1, 0, 0, 0, 27, 1, 1, 0, 0, 0, 28, 26, 1, 0, 0, 0, 29, 30, 3, 4, 2, 0, 30, 31, 3, 6, 3, 0, 31, 35, 1, 0, 0, 0, 32, 35, 3, 4, 2, 0, 33, 35, 3, 6, 3, 0, 34, 29, 1, 0, 0, 0, 34, 32, 1, 0, 0, 0, 34, 33, 1, 0, 0, 0, 35, 36, 1, 0, 0, 0, 36, 37, 5, 1, 0, 0, 37, 3, 1, 0, 0, 0, 38, 43, 5, 12, 0, 0, 39, 40, 5, 2, 0, 0, 40, 42, 5, 12, 0, 0, 41, 39, 1, 0, 0, 0, 42, 45, 1, 0, 0, 0, 43, 41, 1, 0, 0, 0, 43, 44, 1, 0, 0, 0, 44, 5, 1, 0, 0, 0, 45, 43, 1, 0, 0, 0, 46, 55, 5, 3, 0, 0, 47, 52, 3, 12, 6, 0, 48, 49, 5, 2, 0, 0, 49, 51, 3, 12, 6, 0, 50, 48, 1, 0, 0, 0, 51, 54, 1, 0, 0, 0, 52, 50, 1, 0, 0, 0, 52, 53, 1, 0, 0, 0, 53, 56, 1, 0, 0, 0, 54, 52, 1, 0, 0, 0, 55, 47, 1, 0, 0, 0, 55, 56, 1, 0, 0, 0, 56, 7, 1, 0, 0, 0, 57, 58, 3, 10, 5, 0, 58, 59, 5, 1, 0, 0, 59, 9, 1, 0, 0, 0, 60, 61, 6, 5, -1, 0, 61, 62, 5, 4, 0, 0, 62, 63, 3, 10, 5, 0, 63, 64, 5, 5, 0, 0, 64, 67, 1, 0, 0, 0, 65, 67, 3, 14, 7, 0, 66, 60, 1, 0, 0, 0, 66, 65, 1, 0, 0, 0, 67, 76, 1, 0, 0, 0, 68, 69, 10, 2, 0, 0, 69, 70, 7, 0, 0, 0, 70, 75, 3, 10, 5, 3, 71, 72, 10, 1, 0, 0, 72, 73, 5, 8, 0, 0, 73, 75, 3, 10, 5, 2, 74, 68, 1, 0, 0, 0, 74, 71, 1, 0, 0, 0, 75, 78, 1, 0, 0, 0, 76, 74, 1, 0, 0, 0, 76, 77, 1, 0, 0, 0, 77, 11, 1, 0, 0, 0, 78, 76, 1, 0, 0, 0, 79, 82, 3, 16, 8, 0, 80, 82, 3, 18, 9, 0, 81, 79, 1, 0, 0, 0, 81, 80, 1, 0, 0, 0, 82, 13, 1, 0, 0, 0, 83, 86, 3, 16, 8, 0, 84, 86, 3, 20, 10, 0, 85, 83, 1, 0, 0, 0, 85, 84, 1, 0, 0, 0, 86, 15, 1, 0, 0, 0, 87, 88, 5, 12, 0, 0, 88, 17, 1, 0, 0, 0, 89, 90, 5, 9, 0, 0, 90, 91, 5, 12, 0, 0, 91, 19, 1, 0, 0, 0, 92, 93, 5, 10, 0, 0, 93, 94, 5, 12, 0, 0, 94, 21, 1, 0, 0, 0, 11, 24, 26, 34, 43, 52, 55, 66, 74, 76, 81, 85]

6
grammars/HMKNF.tokens
View File

@ -15,8 +15,8 @@ IDENTIFIER=12
':-'=3 ':-'=3
'('=4 '('=4
')'=5 ')'=5
'->'=6 '|'=6
'|'=7 '&'=7
'&'=8 '->'=8
'not'=9 'not'=9
'-'=10 '-'=10

4
grammars/HMKNFLexer.interp
View File

@ -5,9 +5,9 @@ null
':-' ':-'
'(' '('
')' ')'
'->'
'|' '|'
'&' '&'
'->'
'not' 'not'
'-' '-'
null null
@ -50,4 +50,4 @@ mode names:
DEFAULT_MODE DEFAULT_MODE
atn: atn:
[4, 0, 12, 63, 6, -1, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 2, 10, 7, 10, 2, 11, 7, 11, 1, 0, 1, 0, 1, 1, 1, 1, 1, 2, 1, 2, 1, 2, 1, 3, 1, 3, 1, 4, 1, 4, 1, 5, 1, 5, 1, 5, 1, 6, 1, 6, 1, 7, 1, 7, 1, 8, 1, 8, 1, 8, 1, 8, 1, 9, 1, 9, 1, 10, 4, 10, 51, 8, 10, 11, 10, 12, 10, 52, 1, 10, 1, 10, 1, 11, 1, 11, 5, 11, 59, 8, 11, 10, 11, 12, 11, 62, 9, 11, 0, 0, 12, 1, 1, 3, 2, 5, 3, 7, 4, 9, 5, 11, 6, 13, 7, 15, 8, 17, 9, 19, 10, 21, 11, 23, 12, 1, 0, 3, 3, 0, 9, 10, 13, 13, 32, 32, 1, 0, 97, 122, 3, 0, 48, 57, 65, 90, 97, 122, 64, 0, 1, 1, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 5, 1, 0, 0, 0, 0, 7, 1, 0, 0, 0, 0, 9, 1, 0, 0, 0, 0, 11, 1, 0, 0, 0, 0, 13, 1, 0, 0, 0, 0, 15, 1, 0, 0, 0, 0, 17, 1, 0, 0, 0, 0, 19, 1, 0, 0, 0, 0, 21, 1, 0, 0, 0, 0, 23, 1, 0, 0, 0, 1, 25, 1, 0, 0, 0, 3, 27, 1, 0, 0, 0, 5, 29, 1, 0, 0, 0, 7, 32, 1, 0, 0, 0, 9, 34, 1, 0, 0, 0, 11, 36, 1, 0, 0, 0, 13, 39, 1, 0, 0, 0, 15, 41, 1, 0, 0, 0, 17, 43, 1, 0, 0, 0, 19, 47, 1, 0, 0, 0, 21, 50, 1, 0, 0, 0, 23, 56, 1, 0, 0, 0, 25, 26, 5, 46, 0, 0, 26, 2, 1, 0, 0, 0, 27, 28, 5, 44, 0, 0, 28, 4, 1, 0, 0, 0, 29, 30, 5, 58, 0, 0, 30, 31, 5, 45, 0, 0, 31, 6, 1, 0, 0, 0, 32, 33, 5, 40, 0, 0, 33, 8, 1, 0, 0, 0, 34, 35, 5, 41, 0, 0, 35, 10, 1, 0, 0, 0, 36, 37, 5, 45, 0, 0, 37, 38, 5, 62, 0, 0, 38, 12, 1, 0, 0, 0, 39, 40, 5, 124, 0, 0, 40, 14, 1, 0, 0, 0, 41, 42, 5, 38, 0, 0, 42, 16, 1, 0, 0, 0, 43, 44, 5, 110, 0, 0, 44, 45, 5, 111, 0, 0, 45, 46, 5, 116, 0, 0, 46, 18, 1, 0, 0, 0, 47, 48, 5, 45, 0, 0, 48, 20, 1, 0, 0, 0, 49, 51, 7, 0, 0, 0, 50, 49, 1, 0, 0, 0, 51, 52, 1, 0, 0, 0, 52, 50, 1, 0, 0, 0, 52, 53, 1, 0, 0, 0, 53, 54, 1, 0, 0, 0, 54, 55, 6, 10, 0, 0, 55, 22, 1, 0, 0, 0, 56, 60, 7, 1, 0, 0, 57, 59, 7, 2, 0, 0, 58, 57, 1, 0, 0, 0, 59, 62, 1, 0, 0, 0, 60, 58, 1, 0, 0, 0, 60, 61, 1, 0, 0, 0, 61, 24, 1, 0, 0, 0, 62, 60, 1, 0, 0, 0, 3, 0, 52, 60, 1, 6, 0, 0] [4, 0, 12, 63, 6, -1, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 2, 10, 7, 10, 2, 11, 7, 11, 1, 0, 1, 0, 1, 1, 1, 1, 1, 2, 1, 2, 1, 2, 1, 3, 1, 3, 1, 4, 1, 4, 1, 5, 1, 5, 1, 6, 1, 6, 1, 7, 1, 7, 1, 7, 1, 8, 1, 8, 1, 8, 1, 8, 1, 9, 1, 9, 1, 10, 4, 10, 51, 8, 10, 11, 10, 12, 10, 52, 1, 10, 1, 10, 1, 11, 1, 11, 5, 11, 59, 8, 11, 10, 11, 12, 11, 62, 9, 11, 0, 0, 12, 1, 1, 3, 2, 5, 3, 7, 4, 9, 5, 11, 6, 13, 7, 15, 8, 17, 9, 19, 10, 21, 11, 23, 12, 1, 0, 3, 3, 0, 9, 10, 13, 13, 32, 32, 2, 0, 39, 39, 97, 122, 4, 0, 39, 39, 48, 57, 65, 90, 97, 122, 64, 0, 1, 1, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 5, 1, 0, 0, 0, 0, 7, 1, 0, 0, 0, 0, 9, 1, 0, 0, 0, 0, 11, 1, 0, 0, 0, 0, 13, 1, 0, 0, 0, 0, 15, 1, 0, 0, 0, 0, 17, 1, 0, 0, 0, 0, 19, 1, 0, 0, 0, 0, 21, 1, 0, 0, 0, 0, 23, 1, 0, 0, 0, 1, 25, 1, 0, 0, 0, 3, 27, 1, 0, 0, 0, 5, 29, 1, 0, 0, 0, 7, 32, 1, 0, 0, 0, 9, 34, 1, 0, 0, 0, 11, 36, 1, 0, 0, 0, 13, 38, 1, 0, 0, 0, 15, 40, 1, 0, 0, 0, 17, 43, 1, 0, 0, 0, 19, 47, 1, 0, 0, 0, 21, 50, 1, 0, 0, 0, 23, 56, 1, 0, 0, 0, 25, 26, 5, 46, 0, 0, 26, 2, 1, 0, 0, 0, 27, 28, 5, 44, 0, 0, 28, 4, 1, 0, 0, 0, 29, 30, 5, 58, 0, 0, 30, 31, 5, 45, 0, 0, 31, 6, 1, 0, 0, 0, 32, 33, 5, 40, 0, 0, 33, 8, 1, 0, 0, 0, 34, 35, 5, 41, 0, 0, 35, 10, 1, 0, 0, 0, 36, 37, 5, 124, 0, 0, 37, 12, 1, 0, 0, 0, 38, 39, 5, 38, 0, 0, 39, 14, 1, 0, 0, 0, 40, 41, 5, 45, 0, 0, 41, 42, 5, 62, 0, 0, 42, 16, 1, 0, 0, 0, 43, 44, 5, 110, 0, 0, 44, 45, 5, 111, 0, 0, 45, 46, 5, 116, 0, 0, 46, 18, 1, 0, 0, 0, 47, 48, 5, 45, 0, 0, 48, 20, 1, 0, 0, 0, 49, 51, 7, 0, 0, 0, 50, 49, 1, 0, 0, 0, 51, 52, 1, 0, 0, 0, 52, 50, 1, 0, 0, 0, 52, 53, 1, 0, 0, 0, 53, 54, 1, 0, 0, 0, 54, 55, 6, 10, 0, 0, 55, 22, 1, 0, 0, 0, 56, 60, 7, 1, 0, 0, 57, 59, 7, 2, 0, 0, 58, 57, 1, 0, 0, 0, 59, 62, 1, 0, 0, 0, 60, 58, 1, 0, 0, 0, 60, 61, 1, 0, 0, 0, 61, 24, 1, 0, 0, 0, 62, 60, 1, 0, 0, 0, 3, 0, 52, 60, 1, 6, 0, 0]

34
grammars/HMKNFLexer.py
View File

@ -12,25 +12,25 @@ def serializedATN():
return [ return [
4,0,12,63,6,-1,2,0,7,0,2,1,7,1,2,2,7,2,2,3,7,3,2,4,7,4,2,5,7,5,2, 4,0,12,63,6,-1,2,0,7,0,2,1,7,1,2,2,7,2,2,3,7,3,2,4,7,4,2,5,7,5,2,
6,7,6,2,7,7,7,2,8,7,8,2,9,7,9,2,10,7,10,2,11,7,11,1,0,1,0,1,1,1, 6,7,6,2,7,7,7,2,8,7,8,2,9,7,9,2,10,7,10,2,11,7,11,1,0,1,0,1,1,1,
1,1,2,1,2,1,2,1,3,1,3,1,4,1,4,1,5,1,5,1,5,1,6,1,6,1,7,1,7,1,8,1, 1,1,2,1,2,1,2,1,3,1,3,1,4,1,4,1,5,1,5,1,6,1,6,1,7,1,7,1,7,1,8,1,
8,1,8,1,8,1,9,1,9,1,10,4,10,51,8,10,11,10,12,10,52,1,10,1,10,1,11, 8,1,8,1,8,1,9,1,9,1,10,4,10,51,8,10,11,10,12,10,52,1,10,1,10,1,11,
1,11,5,11,59,8,11,10,11,12,11,62,9,11,0,0,12,1,1,3,2,5,3,7,4,9,5, 1,11,5,11,59,8,11,10,11,12,11,62,9,11,0,0,12,1,1,3,2,5,3,7,4,9,5,
11,6,13,7,15,8,17,9,19,10,21,11,23,12,1,0,3,3,0,9,10,13,13,32,32, 11,6,13,7,15,8,17,9,19,10,21,11,23,12,1,0,3,3,0,9,10,13,13,32,32,
1,0,97,122,3,0,48,57,65,90,97,122,64,0,1,1,0,0,0,0,3,1,0,0,0,0,5, 2,0,39,39,97,122,4,0,39,39,48,57,65,90,97,122,64,0,1,1,0,0,0,0,3,
1,0,0,0,0,7,1,0,0,0,0,9,1,0,0,0,0,11,1,0,0,0,0,13,1,0,0,0,0,15,1, 1,0,0,0,0,5,1,0,0,0,0,7,1,0,0,0,0,9,1,0,0,0,0,11,1,0,0,0,0,13,1,
0,0,0,0,17,1,0,0,0,0,19,1,0,0,0,0,21,1,0,0,0,0,23,1,0,0,0,1,25,1, 0,0,0,0,15,1,0,0,0,0,17,1,0,0,0,0,19,1,0,0,0,0,21,1,0,0,0,0,23,1,
0,0,0,3,27,1,0,0,0,5,29,1,0,0,0,7,32,1,0,0,0,9,34,1,0,0,0,11,36, 0,0,0,1,25,1,0,0,0,3,27,1,0,0,0,5,29,1,0,0,0,7,32,1,0,0,0,9,34,1,
1,0,0,0,13,39,1,0,0,0,15,41,1,0,0,0,17,43,1,0,0,0,19,47,1,0,0,0, 0,0,0,11,36,1,0,0,0,13,38,1,0,0,0,15,40,1,0,0,0,17,43,1,0,0,0,19,
21,50,1,0,0,0,23,56,1,0,0,0,25,26,5,46,0,0,26,2,1,0,0,0,27,28,5, 47,1,0,0,0,21,50,1,0,0,0,23,56,1,0,0,0,25,26,5,46,0,0,26,2,1,0,0,
44,0,0,28,4,1,0,0,0,29,30,5,58,0,0,30,31,5,45,0,0,31,6,1,0,0,0,32, 0,27,28,5,44,0,0,28,4,1,0,0,0,29,30,5,58,0,0,30,31,5,45,0,0,31,6,
33,5,40,0,0,33,8,1,0,0,0,34,35,5,41,0,0,35,10,1,0,0,0,36,37,5,45, 1,0,0,0,32,33,5,40,0,0,33,8,1,0,0,0,34,35,5,41,0,0,35,10,1,0,0,0,
0,0,37,38,5,62,0,0,38,12,1,0,0,0,39,40,5,124,0,0,40,14,1,0,0,0,41, 36,37,5,124,0,0,37,12,1,0,0,0,38,39,5,38,0,0,39,14,1,0,0,0,40,41,
42,5,38,0,0,42,16,1,0,0,0,43,44,5,110,0,0,44,45,5,111,0,0,45,46, 5,45,0,0,41,42,5,62,0,0,42,16,1,0,0,0,43,44,5,110,0,0,44,45,5,111,
5,116,0,0,46,18,1,0,0,0,47,48,5,45,0,0,48,20,1,0,0,0,49,51,7,0,0, 0,0,45,46,5,116,0,0,46,18,1,0,0,0,47,48,5,45,0,0,48,20,1,0,0,0,49,
0,50,49,1,0,0,0,51,52,1,0,0,0,52,50,1,0,0,0,52,53,1,0,0,0,53,54, 51,7,0,0,0,50,49,1,0,0,0,51,52,1,0,0,0,52,50,1,0,0,0,52,53,1,0,0,
1,0,0,0,54,55,6,10,0,0,55,22,1,0,0,0,56,60,7,1,0,0,57,59,7,2,0,0, 0,53,54,1,0,0,0,54,55,6,10,0,0,55,22,1,0,0,0,56,60,7,1,0,0,57,59,
58,57,1,0,0,0,59,62,1,0,0,0,60,58,1,0,0,0,60,61,1,0,0,0,61,24,1, 7,2,0,0,58,57,1,0,0,0,59,62,1,0,0,0,60,58,1,0,0,0,60,61,1,0,0,0,
0,0,0,62,60,1,0,0,0,3,0,52,60,1,6,0,0 61,24,1,0,0,0,62,60,1,0,0,0,3,0,52,60,1,6,0,0
] ]
class HMKNFLexer(Lexer): class HMKNFLexer(Lexer):
@ -57,7 +57,7 @@ class HMKNFLexer(Lexer):
modeNames = [ "DEFAULT_MODE" ] modeNames = [ "DEFAULT_MODE" ]
literalNames = [ "<INVALID>", literalNames = [ "<INVALID>",
"'.'", "','", "':-'", "'('", "')'", "'->'", "'|'", "'&'", "'not'", "'.'", "','", "':-'", "'('", "')'", "'|'", "'&'", "'->'", "'not'",
"'-'" ] "'-'" ]
symbolicNames = [ "<INVALID>", symbolicNames = [ "<INVALID>",

6
grammars/HMKNFLexer.tokens
View File

@ -15,8 +15,8 @@ IDENTIFIER=12
':-'=3 ':-'=3
'('=4 '('=4
')'=5 ')'=5
'->'=6 '|'=6
'|'=7 '&'=7
'&'=8 '->'=8
'not'=9 'not'=9
'-'=10 '-'=10

157
grammars/HMKNFParser.py
View File

@ -10,37 +10,36 @@ else:
def serializedATN(): def serializedATN():
return [ return [
4,1,12,99,2,0,7,0,2,1,7,1,2,2,7,2,2,3,7,3,2,4,7,4,2,5,7,5,2,6,7, 4,1,12,96,2,0,7,0,2,1,7,1,2,2,7,2,2,3,7,3,2,4,7,4,2,5,7,5,2,6,7,
6,2,7,7,7,2,8,7,8,2,9,7,9,2,10,7,10,1,0,1,0,5,0,25,8,0,10,0,12,0, 6,2,7,7,7,2,8,7,8,2,9,7,9,2,10,7,10,1,0,1,0,5,0,25,8,0,10,0,12,0,
28,9,0,1,1,1,1,1,1,1,1,1,1,3,1,35,8,1,1,1,1,1,1,2,1,2,1,2,5,2,42, 28,9,0,1,1,1,1,1,1,1,1,1,1,3,1,35,8,1,1,1,1,1,1,2,1,2,1,2,5,2,42,
8,2,10,2,12,2,45,9,2,1,3,1,3,1,3,1,3,5,3,51,8,3,10,3,12,3,54,9,3, 8,2,10,2,12,2,45,9,2,1,3,1,3,1,3,1,3,5,3,51,8,3,10,3,12,3,54,9,3,
3,3,56,8,3,1,4,1,4,1,4,1,5,1,5,1,5,1,5,1,5,1,5,3,5,67,8,5,1,5,1, 3,3,56,8,3,1,4,1,4,1,4,1,5,1,5,1,5,1,5,1,5,1,5,3,5,67,8,5,1,5,1,
5,1,5,1,5,1,5,1,5,1,5,1,5,1,5,5,5,78,8,5,10,5,12,5,81,9,5,1,6,1, 5,1,5,1,5,1,5,1,5,5,5,75,8,5,10,5,12,5,78,9,5,1,6,1,6,3,6,82,8,6,
6,3,6,85,8,6,1,7,1,7,3,7,89,8,7,1,8,1,8,1,9,1,9,1,9,1,10,1,10,1, 1,7,1,7,3,7,86,8,7,1,8,1,8,1,9,1,9,1,9,1,10,1,10,1,10,1,10,0,1,10,
10,1,10,0,1,10,11,0,2,4,6,8,10,12,14,16,18,20,0,0,100,0,26,1,0,0, 11,0,2,4,6,8,10,12,14,16,18,20,0,1,1,0,6,7,96,0,26,1,0,0,0,2,34,
0,2,34,1,0,0,0,4,38,1,0,0,0,6,46,1,0,0,0,8,57,1,0,0,0,10,66,1,0, 1,0,0,0,4,38,1,0,0,0,6,46,1,0,0,0,8,57,1,0,0,0,10,66,1,0,0,0,12,
0,0,12,84,1,0,0,0,14,88,1,0,0,0,16,90,1,0,0,0,18,92,1,0,0,0,20,95, 81,1,0,0,0,14,85,1,0,0,0,16,87,1,0,0,0,18,89,1,0,0,0,20,92,1,0,0,
1,0,0,0,22,25,3,2,1,0,23,25,3,8,4,0,24,22,1,0,0,0,24,23,1,0,0,0, 0,22,25,3,2,1,0,23,25,3,8,4,0,24,22,1,0,0,0,24,23,1,0,0,0,25,28,
25,28,1,0,0,0,26,24,1,0,0,0,26,27,1,0,0,0,27,1,1,0,0,0,28,26,1,0, 1,0,0,0,26,24,1,0,0,0,26,27,1,0,0,0,27,1,1,0,0,0,28,26,1,0,0,0,29,
0,0,29,30,3,4,2,0,30,31,3,6,3,0,31,35,1,0,0,0,32,35,3,4,2,0,33,35, 30,3,4,2,0,30,31,3,6,3,0,31,35,1,0,0,0,32,35,3,4,2,0,33,35,3,6,3,
3,6,3,0,34,29,1,0,0,0,34,32,1,0,0,0,34,33,1,0,0,0,35,36,1,0,0,0, 0,34,29,1,0,0,0,34,32,1,0,0,0,34,33,1,0,0,0,35,36,1,0,0,0,36,37,
36,37,5,1,0,0,37,3,1,0,0,0,38,43,5,12,0,0,39,40,5,2,0,0,40,42,5, 5,1,0,0,37,3,1,0,0,0,38,43,5,12,0,0,39,40,5,2,0,0,40,42,5,12,0,0,
12,0,0,41,39,1,0,0,0,42,45,1,0,0,0,43,41,1,0,0,0,43,44,1,0,0,0,44, 41,39,1,0,0,0,42,45,1,0,0,0,43,41,1,0,0,0,43,44,1,0,0,0,44,5,1,0,
5,1,0,0,0,45,43,1,0,0,0,46,55,5,3,0,0,47,52,3,12,6,0,48,49,5,2,0, 0,0,45,43,1,0,0,0,46,55,5,3,0,0,47,52,3,12,6,0,48,49,5,2,0,0,49,
0,49,51,3,12,6,0,50,48,1,0,0,0,51,54,1,0,0,0,52,50,1,0,0,0,52,53, 51,3,12,6,0,50,48,1,0,0,0,51,54,1,0,0,0,52,50,1,0,0,0,52,53,1,0,
1,0,0,0,53,56,1,0,0,0,54,52,1,0,0,0,55,47,1,0,0,0,55,56,1,0,0,0, 0,0,53,56,1,0,0,0,54,52,1,0,0,0,55,47,1,0,0,0,55,56,1,0,0,0,56,7,
56,7,1,0,0,0,57,58,3,10,5,0,58,59,5,1,0,0,59,9,1,0,0,0,60,61,6,5, 1,0,0,0,57,58,3,10,5,0,58,59,5,1,0,0,59,9,1,0,0,0,60,61,6,5,-1,0,
-1,0,61,62,5,4,0,0,62,63,3,10,5,0,63,64,5,5,0,0,64,67,1,0,0,0,65, 61,62,5,4,0,0,62,63,3,10,5,0,63,64,5,5,0,0,64,67,1,0,0,0,65,67,3,
67,3,14,7,0,66,60,1,0,0,0,66,65,1,0,0,0,67,79,1,0,0,0,68,69,10,3, 14,7,0,66,60,1,0,0,0,66,65,1,0,0,0,67,76,1,0,0,0,68,69,10,2,0,0,
0,0,69,70,5,6,0,0,70,78,3,10,5,4,71,72,10,2,0,0,72,73,5,7,0,0,73, 69,70,7,0,0,0,70,75,3,10,5,3,71,72,10,1,0,0,72,73,5,8,0,0,73,75,
78,3,10,5,3,74,75,10,1,0,0,75,76,5,8,0,0,76,78,3,10,5,2,77,68,1, 3,10,5,2,74,68,1,0,0,0,74,71,1,0,0,0,75,78,1,0,0,0,76,74,1,0,0,0,
0,0,0,77,71,1,0,0,0,77,74,1,0,0,0,78,81,1,0,0,0,79,77,1,0,0,0,79, 76,77,1,0,0,0,77,11,1,0,0,0,78,76,1,0,0,0,79,82,3,16,8,0,80,82,3,
80,1,0,0,0,80,11,1,0,0,0,81,79,1,0,0,0,82,85,3,16,8,0,83,85,3,18, 18,9,0,81,79,1,0,0,0,81,80,1,0,0,0,82,13,1,0,0,0,83,86,3,16,8,0,
9,0,84,82,1,0,0,0,84,83,1,0,0,0,85,13,1,0,0,0,86,89,3,16,8,0,87, 84,86,3,20,10,0,85,83,1,0,0,0,85,84,1,0,0,0,86,15,1,0,0,0,87,88,
89,3,20,10,0,88,86,1,0,0,0,88,87,1,0,0,0,89,15,1,0,0,0,90,91,5,12, 5,12,0,0,88,17,1,0,0,0,89,90,5,9,0,0,90,91,5,12,0,0,91,19,1,0,0,
0,0,91,17,1,0,0,0,92,93,5,9,0,0,93,94,5,12,0,0,94,19,1,0,0,0,95, 0,92,93,5,10,0,0,93,94,5,12,0,0,94,21,1,0,0,0,11,24,26,34,43,52,
96,5,10,0,0,96,97,5,12,0,0,97,21,1,0,0,0,11,24,26,34,43,52,55,66, 55,66,74,76,81,85
77,79,84,88
] ]
class HMKNFParser ( Parser ): class HMKNFParser ( Parser ):
@ -53,8 +52,8 @@ class HMKNFParser ( Parser ):
sharedContextCache = PredictionContextCache() sharedContextCache = PredictionContextCache()
literalNames = [ "<INVALID>", "'.'", "','", "':-'", "'('", "')'", "'->'", literalNames = [ "<INVALID>", "'.'", "','", "':-'", "'('", "')'", "'|'",
"'|'", "'&'", "'not'", "'-'" ] "'&'", "'->'", "'not'", "'-'" ]
symbolicNames = [ "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", symbolicNames = [ "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>",
"<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>", "<INVALID>",
@ -411,10 +410,11 @@ class HMKNFParser ( Parser ):
super().copyFrom(ctx) super().copyFrom(ctx)
class DisjContext(OformulaContext): class DisjOrConjContext(OformulaContext):
def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext
super().__init__(parser) super().__init__(parser)
self.operator = None # Token
self.copyFrom(ctx) self.copyFrom(ctx)
def oformula(self, i:int=None): def oformula(self, i:int=None):
@ -425,28 +425,8 @@ class HMKNFParser ( Parser ):
def accept(self, visitor:ParseTreeVisitor): def accept(self, visitor:ParseTreeVisitor):
if hasattr( visitor, "visitDisj" ): if hasattr( visitor, "visitDisjOrConj" ):
return visitor.visitDisj(self) return visitor.visitDisjOrConj(self)
else:
return visitor.visitChildren(self)
class ConjContext(OformulaContext):
def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext
super().__init__(parser)
self.copyFrom(ctx)
def oformula(self, i:int=None):
if i is None:
return self.getTypedRuleContexts(HMKNFParser.OformulaContext)
else:
return self.getTypedRuleContext(HMKNFParser.OformulaContext,i)
def accept(self, visitor:ParseTreeVisitor):
if hasattr( visitor, "visitConj" ):
return visitor.visitConj(self)
else: else:
return visitor.visitChildren(self) return visitor.visitChildren(self)
@ -513,6 +493,7 @@ class HMKNFParser ( Parser ):
_prevctx = localctx _prevctx = localctx
_startState = 10 _startState = 10
self.enterRecursionRule(localctx, 10, self.RULE_oformula, _p) self.enterRecursionRule(localctx, 10, self.RULE_oformula, _p)
self._la = 0 # Token type
try: try:
self.enterOuterAlt(localctx, 1) self.enterOuterAlt(localctx, 1)
self.state = 66 self.state = 66
@ -541,7 +522,7 @@ class HMKNFParser ( Parser ):
raise NoViableAltException(self) raise NoViableAltException(self)
self._ctx.stop = self._input.LT(-1) self._ctx.stop = self._input.LT(-1)
self.state = 79 self.state = 76
self._errHandler.sync(self) self._errHandler.sync(self)
_alt = self._interp.adaptivePredict(self._input,8,self._ctx) _alt = self._interp.adaptivePredict(self._input,8,self._ctx)
while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER:
@ -549,50 +530,44 @@ class HMKNFParser ( Parser ):
if self._parseListeners is not None: if self._parseListeners is not None:
self.triggerExitRuleEvent() self.triggerExitRuleEvent()
_prevctx = localctx _prevctx = localctx
self.state = 77 self.state = 74
self._errHandler.sync(self) self._errHandler.sync(self)
la_ = self._interp.adaptivePredict(self._input,7,self._ctx) la_ = self._interp.adaptivePredict(self._input,7,self._ctx)
if la_ == 1: if la_ == 1:
localctx = HMKNFParser.ImpContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState)) localctx = HMKNFParser.DisjOrConjContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState))
self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula) self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula)
self.state = 68 self.state = 68
if not self.precpred(self._ctx, 3):
from antlr4.error.Errors import FailedPredicateException
raise FailedPredicateException(self, "self.precpred(self._ctx, 3)")
self.state = 69
self.match(HMKNFParser.T__5)
self.state = 70
self.oformula(4)
pass
elif la_ == 2:
localctx = HMKNFParser.DisjContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState))
self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula)
self.state = 71
if not self.precpred(self._ctx, 2): if not self.precpred(self._ctx, 2):
from antlr4.error.Errors import FailedPredicateException from antlr4.error.Errors import FailedPredicateException
raise FailedPredicateException(self, "self.precpred(self._ctx, 2)") raise FailedPredicateException(self, "self.precpred(self._ctx, 2)")
self.state = 72
self.match(HMKNFParser.T__6) self.state = 69
self.state = 73 localctx.operator = self._input.LT(1)
_la = self._input.LA(1)
if not(_la==HMKNFParser.T__5 or _la==HMKNFParser.T__6):
localctx.operator = self._errHandler.recoverInline(self)
else:
self._errHandler.reportMatch(self)
self.consume()
self.state = 70
self.oformula(3) self.oformula(3)
pass pass
elif la_ == 3: elif la_ == 2:
localctx = HMKNFParser.ConjContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState)) localctx = HMKNFParser.ImpContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState))
self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula) self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula)
self.state = 74 self.state = 71
if not self.precpred(self._ctx, 1): if not self.precpred(self._ctx, 1):
from antlr4.error.Errors import FailedPredicateException from antlr4.error.Errors import FailedPredicateException
raise FailedPredicateException(self, "self.precpred(self._ctx, 1)") raise FailedPredicateException(self, "self.precpred(self._ctx, 1)")
self.state = 75 self.state = 72
self.match(HMKNFParser.T__7) self.match(HMKNFParser.T__7)
self.state = 76 self.state = 73
self.oformula(2) self.oformula(2)
pass pass
self.state = 81 self.state = 78
self._errHandler.sync(self) self._errHandler.sync(self)
_alt = self._interp.adaptivePredict(self._input,8,self._ctx) _alt = self._interp.adaptivePredict(self._input,8,self._ctx)
@ -637,17 +612,17 @@ class HMKNFParser ( Parser ):
localctx = HMKNFParser.KatomContext(self, self._ctx, self.state) localctx = HMKNFParser.KatomContext(self, self._ctx, self.state)
self.enterRule(localctx, 12, self.RULE_katom) self.enterRule(localctx, 12, self.RULE_katom)
try: try:
self.state = 84 self.state = 81
self._errHandler.sync(self) self._errHandler.sync(self)
token = self._input.LA(1) token = self._input.LA(1)
if token in [HMKNFParser.IDENTIFIER]: if token in [HMKNFParser.IDENTIFIER]:
self.enterOuterAlt(localctx, 1) self.enterOuterAlt(localctx, 1)
self.state = 82 self.state = 79
self.patom() self.patom()
pass pass
elif token in [HMKNFParser.T__8]: elif token in [HMKNFParser.T__8]:
self.enterOuterAlt(localctx, 2) self.enterOuterAlt(localctx, 2)
self.state = 83 self.state = 80
self.natom() self.natom()
pass pass
else: else:
@ -694,17 +669,17 @@ class HMKNFParser ( Parser ):
localctx = HMKNFParser.OatomContext(self, self._ctx, self.state) localctx = HMKNFParser.OatomContext(self, self._ctx, self.state)
self.enterRule(localctx, 14, self.RULE_oatom) self.enterRule(localctx, 14, self.RULE_oatom)
try: try:
self.state = 88 self.state = 85
self._errHandler.sync(self) self._errHandler.sync(self)
token = self._input.LA(1) token = self._input.LA(1)
if token in [HMKNFParser.IDENTIFIER]: if token in [HMKNFParser.IDENTIFIER]:
self.enterOuterAlt(localctx, 1) self.enterOuterAlt(localctx, 1)
self.state = 86 self.state = 83
self.patom() self.patom()
pass pass
elif token in [HMKNFParser.T__9]: elif token in [HMKNFParser.T__9]:
self.enterOuterAlt(localctx, 2) self.enterOuterAlt(localctx, 2)
self.state = 87 self.state = 84
self.fatom() self.fatom()
pass pass
else: else:
@ -747,7 +722,7 @@ class HMKNFParser ( Parser ):
self.enterRule(localctx, 16, self.RULE_patom) self.enterRule(localctx, 16, self.RULE_patom)
try: try:
self.enterOuterAlt(localctx, 1) self.enterOuterAlt(localctx, 1)
self.state = 90 self.state = 87
self.match(HMKNFParser.IDENTIFIER) self.match(HMKNFParser.IDENTIFIER)
except RecognitionException as re: except RecognitionException as re:
localctx.exception = re localctx.exception = re
@ -786,9 +761,9 @@ class HMKNFParser ( Parser ):
self.enterRule(localctx, 18, self.RULE_natom) self.enterRule(localctx, 18, self.RULE_natom)
try: try:
self.enterOuterAlt(localctx, 1) self.enterOuterAlt(localctx, 1)
self.state = 92 self.state = 89
self.match(HMKNFParser.T__8) self.match(HMKNFParser.T__8)
self.state = 93 self.state = 90
self.match(HMKNFParser.IDENTIFIER) self.match(HMKNFParser.IDENTIFIER)
except RecognitionException as re: except RecognitionException as re:
localctx.exception = re localctx.exception = re
@ -827,9 +802,9 @@ class HMKNFParser ( Parser ):
self.enterRule(localctx, 20, self.RULE_fatom) self.enterRule(localctx, 20, self.RULE_fatom)
try: try:
self.enterOuterAlt(localctx, 1) self.enterOuterAlt(localctx, 1)
self.state = 95 self.state = 92
self.match(HMKNFParser.T__9) self.match(HMKNFParser.T__9)
self.state = 96 self.state = 93
self.match(HMKNFParser.IDENTIFIER) self.match(HMKNFParser.IDENTIFIER)
except RecognitionException as re: except RecognitionException as re:
localctx.exception = re localctx.exception = re
@ -853,14 +828,10 @@ class HMKNFParser ( Parser ):
def oformula_sempred(self, localctx:OformulaContext, predIndex:int): def oformula_sempred(self, localctx:OformulaContext, predIndex:int):
if predIndex == 0: if predIndex == 0:
return self.precpred(self._ctx, 3)
if predIndex == 1:
return self.precpred(self._ctx, 2) return self.precpred(self._ctx, 2)
if predIndex == 2: if predIndex == 1:
return self.precpred(self._ctx, 1) return self.precpred(self._ctx, 1)

9
grammars/HMKNFVisitor.py
View File

@ -34,13 +34,8 @@ class HMKNFVisitor(ParseTreeVisitor):
return self.visitChildren(ctx) return self.visitChildren(ctx)
# Visit a parse tree produced by HMKNFParser#disj. # Visit a parse tree produced by HMKNFParser#disjOrConj.
def visitDisj(self, ctx:HMKNFParser.DisjContext): def visitDisjOrConj(self, ctx:HMKNFParser.DisjOrConjContext):
return self.visitChildren(ctx)
# Visit a parse tree produced by HMKNFParser#conj.
def visitConj(self, ctx:HMKNFParser.ConjContext):
return self.visitChildren(ctx) return self.visitChildren(ctx)

10
hmknf.py
View File

@ -61,6 +61,7 @@ def block(kb: KB, T: set[str], P: set[str]):
continue continue
if h not in F: if h not in F:
continue continue
# Can't be P or T? TODO
if P.intersection(nbody): if P.intersection(nbody):
continue continue
for atom in pbody: for atom in pbody:
@ -149,5 +150,10 @@ def main():
fprint_partition(wfm) fprint_partition(wfm)
if __name__ == "__main__" and not flags.interactive: kb = loadProgram(open("tests/uh_oh2.in").read())
main()
least_ext_stable_fixedpoint(kb, ext_op)
# if __name__ == "__main__" and not flags.interactive:
# main()

5
tests/uh_oh.in Normal file
View File

@ -0,0 +1,5 @@
-b.
b :- a, not c.
c :- a.
a.

7
tests/uh_oh2.in Normal file
View File

@ -0,0 +1,7 @@
-b | -e -> -c.
c :- not c'.
c' :- not c.
d :- c, c'.

7
tests/whaaat.in Normal file
View File

@ -0,0 +1,7 @@
-b | -e -> -c.
c :- not c'.
c' :- not c.
d :- c, c'.