152 lines
3.6 KiB
Python
152 lines
3.6 KiB
Python
"""
|
|
A grammar for parsing CNF files
|
|
|
|
If this module is run directly in python, it will spit out valid python which produces an
|
|
oracle table for the grammar it defines. It's recommended that this be done using
|
|
`build_oracle.sh` instead, however, which will build a whole python module containing the
|
|
oracle table, complete with imports.
|
|
"""
|
|
from enum import auto, IntEnum
|
|
from re import compile, Pattern
|
|
|
|
from typing import Collection, Mapping, Sequence, Tuple
|
|
|
|
class Tok(IntEnum):
|
|
"""
|
|
All possible tokens used in the grammar
|
|
"""
|
|
Newline = auto()
|
|
Whitespace = auto()
|
|
PredicateSection = auto()
|
|
VariablesSection = auto()
|
|
ConstantsSection = auto()
|
|
FunctionsSection = auto()
|
|
ClausesSection = auto()
|
|
Negate = auto()
|
|
OpenP = auto()
|
|
CloseP = auto()
|
|
Comma = auto()
|
|
Identifier = auto()
|
|
Eof = auto()
|
|
|
|
def __repr__(self):
|
|
return self._name_
|
|
|
|
LEX_TABLE: Collection[Tuple[Pattern[str], Tok]] = [
|
|
(compile(r"\n"), Tok.Newline),
|
|
(compile(r"[ \t]+"), Tok.Whitespace),
|
|
(compile("Predicates:"), Tok.PredicateSection),
|
|
(compile("Variables:"), Tok.VariablesSection),
|
|
(compile("Constants:"), Tok.ConstantsSection),
|
|
(compile("Functions:"), Tok.FunctionsSection),
|
|
(compile("Clauses:"), Tok.ClausesSection),
|
|
(compile("!"), Tok.Negate),
|
|
(compile(r"\("), Tok.OpenP),
|
|
(compile(r"\)"), Tok.CloseP),
|
|
(compile(","), Tok.Comma),
|
|
(compile(r"\w+"), Tok.Identifier),
|
|
]
|
|
"""
|
|
A mapping of regexs to the tokens the identify
|
|
|
|
Tokens earlier on in the list should be regarded as higher priority, even if a match lower
|
|
on the list also matches. All unicode strings should be matched by at least one token.
|
|
"""
|
|
|
|
class Variable(IntEnum):
|
|
Start = auto()
|
|
Idents = auto()
|
|
Clauses = auto()
|
|
Clauses_ = auto()
|
|
Clause = auto()
|
|
Clause_ = auto()
|
|
Term = auto()
|
|
Func = auto()
|
|
CSTerms = auto()
|
|
|
|
def __repr__(self) -> str:
|
|
return f'<{self._name_}>'
|
|
|
|
GRAMMAR: Sequence[Tuple[Variable, Sequence[Variable | Tok]]] = [
|
|
(Variable.Start,
|
|
[ Tok.PredicateSection, Variable.Idents, Tok.Newline
|
|
, Tok.VariablesSection, Variable.Idents, Tok.Newline
|
|
, Tok.ConstantsSection, Variable.Idents, Tok.Newline
|
|
, Tok.FunctionsSection, Variable.Idents, Tok.Newline
|
|
, Tok.ClausesSection, Variable.Clauses, Tok.Eof ] ),
|
|
|
|
(Variable.Idents,
|
|
[ Tok.Identifier, Variable.Idents ]),
|
|
(Variable.Idents,
|
|
[ ]),
|
|
|
|
(Variable.Clauses,
|
|
[ Tok.Newline, Variable.Clauses_ ]),
|
|
(Variable.Clauses,
|
|
[ ]),
|
|
|
|
(Variable.Clauses_,
|
|
[ Variable.Clause, Variable.Clauses ]),
|
|
(Variable.Clauses_,
|
|
[ ]),
|
|
|
|
(Variable.Clause,
|
|
[ Variable.Term, Variable.Clause_ ]),
|
|
|
|
(Variable.Clause_,
|
|
[ Variable.Clause ]),
|
|
(Variable.Clause_,
|
|
[ ]),
|
|
|
|
(Variable.Term,
|
|
[ Tok.Negate, Variable.Term ]),
|
|
(Variable.Term,
|
|
[ Tok.Identifier, Variable.Func ]),
|
|
|
|
(Variable.Func,
|
|
[ Tok.OpenP, Variable.CSTerms, Tok.CloseP ]),
|
|
(Variable.Func,
|
|
[ ]),
|
|
|
|
(Variable.CSTerms,
|
|
[ Tok.Comma, Variable.Term, Variable.CSTerms ]),
|
|
(Variable.CSTerms,
|
|
[ ]),
|
|
]
|
|
"""
|
|
Implements the following grammar:
|
|
|
|
Start := PredicateSection <Idents> Newline
|
|
VariablesSection <Idents> Newline
|
|
ConstantsSection <Idents> Newline
|
|
FunctionsSection <Idents> Newline
|
|
ClausesSection <Clauses> Eof
|
|
|
|
Idents := Identifier <Idents>
|
|
:= ε
|
|
|
|
Clauses := Newline <Clauses'>
|
|
:= ε
|
|
|
|
Clauses' := <Clause> <Clauses>
|
|
:= ε
|
|
|
|
Clause := <Term> <Clause'>
|
|
|
|
Clause' := <Clause>
|
|
:= ε
|
|
|
|
Term := Negate <Term>
|
|
:= Identifier <Func?>
|
|
|
|
Func? := OpenP <Term> <CSTerms> CloseP
|
|
:= ε
|
|
|
|
CSTerms := Comma <Term> <CSTerms>
|
|
:= ε
|
|
"""
|
|
|
|
if __name__ == '__main__':
|
|
from emis_funky_funktions import cur2, flip
|
|
from build_oracle import print_oracle_table_enum, oracle_table
|
|
print(print_oracle_table_enum(oracle_table(flip(cur2(isinstance))(Tok), GRAMMAR))) #type: ignore |