Skip to content
This repository has been archived by the owner on Jul 10, 2024. It is now read-only.

Commit

Permalink
AST: added structure type.
Browse files Browse the repository at this point in the history
  • Loading branch information
@traeger
traeger committed Oct 21, 2019
1 parent f1ccad3 commit 74c1a67
Show file tree
Hide file tree
Showing 6 changed files with 224 additions and 227 deletions.
9 changes: 8 additions & 1 deletion bin/python3/README.md
View file
Original file line number Diff line number Diff line change
@@ -1,2 +1,9 @@
# A fast TPTP-parser for Python3
This TPTP-parser is created using flex/bison and swig.
This TPTP-parser is created using flex/bison and swig. The sources can be found at {https://github.com/leoprover/tptp-parser}.

## Testrun
### python3
```$ python3 PROBLEM_FILE```

## License
The TPTP-parser is licensed under the BSD 3-clause "New" or "Revised" License. See [LICENSE](LICENSE).
37 changes: 0 additions & 37 deletions bin/python3/setup.py
View file

This file was deleted.

27 changes: 18 additions & 9 deletions tptp-parser/tptp.ast.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,47 +50,54 @@ node::node(std::string&& _value) {
this->numChildren = 0;
}

node::node(nodetype _rule) {
node::node(nodetype _rule, structuretype _structure) {
this->type = _rule;
this->structure = _structure;
this->numChildren = 0;
}
node::node(nodetype _rule, node&& c1) {
node::node(nodetype _rule, structuretype _structure, node&& c1) {
this->type = _rule;
this->structure = _structure;
this->cright.push_back(c1);
this->numChildren = 1;
}
node::node(nodetype _rule, node&& c1, node&& c2) {
node::node(nodetype _rule, structuretype _structure, node&& c1, node&& c2) {
this->type = _rule;
this->structure = _structure;
this->cright.push_back(c1);
this->cright.push_back(c2);
this->numChildren = 2;
}
node::node(nodetype _rule, node&& c1, node&& c2, node&& c3) {
node::node(nodetype _rule, structuretype _structure, node&& c1, node&& c2, node&& c3) {
this->type = _rule;
this->structure = _structure;
this->cright.push_back(c1);
this->cright.push_back(c2);
this->cright.push_back(c3);
this->numChildren = 3;
}
node::node(nodetype _rule, node&& c1, node&& c2, node&& c3, node&& c4) {
node::node(nodetype _rule, structuretype _structure, node&& c1, node&& c2, node&& c3, node&& c4) {
this->type = _rule;
this->structure = _structure;
this->cright.push_back(c1);
this->cright.push_back(c2);
this->cright.push_back(c3);
this->cright.push_back(c4);
this->numChildren = 4;
}
node::node(nodetype _rule, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5) {
node::node(nodetype _rule, structuretype _structure, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5) {
this->type = _rule;
this->structure = _structure;
this->cright.push_back(c1);
this->cright.push_back(c2);
this->cright.push_back(c3);
this->cright.push_back(c4);
this->cright.push_back(c5);
this->numChildren = 5;
}
node::node(nodetype _rule, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5, node&& c6) {
node::node(nodetype _rule, structuretype _structure, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5, node&& c6) {
this->type = _rule;
this->structure = _structure;
this->cright.push_back(c1);
this->cright.push_back(c2);
this->cright.push_back(c3);
Expand All @@ -99,8 +106,9 @@ node::node(nodetype _rule, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5
this->cright.push_back(c6);
this->numChildren = 6;
}
node::node(nodetype _rule, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5, node&& c6, node&& c7) {
node::node(nodetype _rule, structuretype _structure, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5, node&& c6, node&& c7) {
this->type = _rule;
this->structure = _structure;
this->cright.push_back(c1);
this->cright.push_back(c2);
this->cright.push_back(c3);
Expand All @@ -110,8 +118,9 @@ node::node(nodetype _rule, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5
this->cright.push_back(c7);
this->numChildren = 7;
}
node::node(nodetype _rule, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5, node&& c6, node&& c7, node&& c8) {
node::node(nodetype _rule, structuretype _structure, node&& c1, node&& c2, node&& c3, node&& c4, node&& c5, node&& c6, node&& c7, node&& c8) {
this->type = _rule;
this->structure = _structure;
this->cright.push_back(c1);
this->cright.push_back(c2);
this->cright.push_back(c3);
Expand Down
45 changes: 30 additions & 15 deletions tptp-parser/tptp.ast.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,20 +36,17 @@ MAKE_ENUM(nodetype,
annotated_formula,
thf_annotated, tff_annotated, tcf_annotated, fof_annotated, cnf_annotated, tpi_annotated,
thf_formula, tff_formula, tcf_formula, fof_formula, cnf_formula, tpi_formula,
// thf
thf_logic_formula, thf_binary_formula, thf_unit_formula, thf_preunit_formula, thf_unitary_formula, thf_apply_formula,
thf_quantified_formula, thf_quantification, thf_variable_list, thf_typed_variable,
/*thf_unary_formula,*/ thf_prefix_unary, /*thf_infix_unary,*/ thf_atomic_formula, thf_plain_atomic,
thf_defined_atomic, /*thf_defined_infix,*/ thf_system_atomic,
thf_prefix_unary, thf_atomic_formula, thf_plain_atomic,
thf_defined_atomic, thf_system_atomic,
thf_conditional, thf_unitary_term, thf_let, thf_let_types, thf_let_types_list,
thf_let_defn, thf_let_defns, thf_let_defns_list, thf_tuple, thf_formula_list, thf_conn_term,
thf_top_level_type, thf_atom_typing, thf_binary_type, thf_mapping_type, thf_xprod_type, thf_union_type, thf_subtype, thf_sequent,
thf_unitary_type, thf_apply_type,
// quantifier
thf_quantifier, th1_quantifier, th0_quantifier, fof_quantifier,
thf_unary_connective, th1_unary_connective, unary_connective, nonassoc_connective, assoc_connective,
// general
atom, untyped_atom, /*defined_infix_pred,*/
atom, untyped_atom,
constant, functor, system_constant, system_functor, defined_constant, defined_functor, defined_term, variable,
source, optional_info, useful_info,
include, formula_selection, name_list,
Expand All @@ -59,6 +56,23 @@ MAKE_ENUM(nodetype,
atomic_word, single_quoted, distinct_object
);

enum class structuretype{
none,
OPERATOR, /* c1 IND c2 */
SEQUENCE, /* c1 c2 c3 .. */
SEPERATED_SEQUENCE, /* c1 PLC c2 PLC c3 .. */
LIST, /* PLC c1 PLC c2 PLC c3 .. PLC */
NAMED_LIST, /* IND PLC c1 PLC c2 PLC c3 .. PLC */
SINGLE, /* c1 */
ANNONTATED, /* IND c1 PLC c2 PLC c3 optional PLC */
ANNONTATED_OPTION, /* PLC c1 c2 */
PREFIX, /* IND c1 */
SUFFIX, /* c1 INC */
BINDER, /* IND PLC c1 PLC PLC */
BRACKET, /* PLC c1 c2 c3 .. PLC */
NAMED_BRACKET /* INC PLC c1 c2 c3 .. PLC */
};

class StopNodeIterator {};

class node
Expand All @@ -78,15 +92,15 @@ public:
// list initializer, to be able to write
// node n1 = node(name, {c1, c2, c3})
// node(nodetype, std::initializer_list<node>);
node(nodetype);
node(nodetype, node&&);
node(nodetype, node&&, node&&);
node(nodetype, node&&, node&&, node&&);
node(nodetype, node&&, node&&, node&&, node&&);
node(nodetype, node&&, node&&, node&&, node&&, node&&);
node(nodetype, node&&, node&&, node&&, node&&, node&&, node&&);
node(nodetype, node&&, node&&, node&&, node&&, node&&, node&&, node&&);
node(nodetype, node&&, node&&, node&&, node&&, node&&, node&&, node&&, node&&);
node(nodetype, structuretype);
node(nodetype, structuretype, node&&);
node(nodetype, structuretype, node&&, node&&);
node(nodetype, structuretype, node&&, node&&, node&&);
node(nodetype, structuretype, node&&, node&&, node&&, node&&);
node(nodetype, structuretype, node&&, node&&, node&&, node&&, node&&);
node(nodetype, structuretype, node&&, node&&, node&&, node&&, node&&, node&&);
node(nodetype, structuretype, node&&, node&&, node&&, node&&, node&&, node&&, node&&);
node(nodetype, structuretype, node&&, node&&, node&&, node&&, node&&, node&&, node&&, node&&);

// add a child as the leftmost child, return the node itself for method-chaining
node& add_left(node&&);
Expand All @@ -107,6 +121,7 @@ public:

bool isTerminal();

structuretype structure = structuretype::none;
nodetype type = nodetype::none;
std::string value;
int numChildren;
Expand Down
3 changes: 3 additions & 0 deletions tptp-parser/tptp.parser.i
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,9 @@
%ignore tptp::ast::node::out; // no ostream support
%ignore operator<<(std::ostream& o, const node& n); // no ostream support

%ignore tptp::ast::structuretype;
%ignore tptp::ast::node::structure;

%rename(__str__) tptp::ast::node::toString;
%rename(__getitem__) tptp::ast::node::child;

Expand Down
Loading

0 comments on commit 74c1a67

Please sign in to comment.