Part 2: Model definition

From textX we can generate an AST (textX calls it a model). Using rule attributes, we will add to the grammar an explicit description to decide what to include in the generated AST. The resulting AST will consist of a tree structure made up of Python objects, with each object corresponding to a specific grammar rule. By judiciously selecting rule attributes and customizing class behavior, information from the rules can be passed to the objects. The following sections will delve into the intricacies of attributes and classes in more detail.

Attributes

Attributes are specified by the grammar rules, and the matched values are passed to the python objects that makes up the model constructed from the input. To specify a basic attribute, you must designate an identifier for the attribute, followed by an equals sign and then a rule. This rule can either be a built-in rule like ID or a custom rule like WFF. This process results in an instance of an object from the specified class being connected to that attribute, facilitating the creation of a hierarchy of Python objects in a tree structure.

The Atom rule will include an attribute called id of type ID. This attribute will store the unique identifier of the atom, allowing us to access it easily using the id attribute. Here’s the result:

Model: wff=WFF;
WFF: Atom | Negation | Conjunction | Disjunction | Implication | Equivalence;
Atom: id=ID;

To track sub-formulas within the input, we must add attributes to the rules representing the connectives. Therefore, we assign a WFF object to an attribute labeled wff for the unary connective Negation. Binary connectives will instead have lhs (left-hand side) and rhs (right-hand side) attributes.

When we add attributes to the relevant rules, the grammar looks like this:

Model: wff=WFF;
WFF: Atom | Negation | Conjunction | Disjunction | Implication | Equivalence;
Atom: id=ID;
Negation: '~' wff=WFF;
Equivalence: '(' lhs=WFF '<=>' rhs=WFF ')';
Implication: '(' lhs=WFF '=>' rhs=WFF ')';
Disjunction: '(' lhs=WFF '|' rhs=WFF ')';
Conjunction: '(' lhs=WFF '&' rhs=WFF ')';

A metamodel, as called by textX, is the parser built from the grammar. More precisely, textX metamodel is a Python object that knows about all classes that can be instantiated while parsing the input. Due to its recursive nature, the metamodel has several loops as can be seen in the following diagram.

This metamodel can be used to generate the models, i.e., the ASTs. The black arrow with a diamond represents composition (has a) and the white arrow represents extension (is a). The atoms will be the leaf nodes of the AST, notice that there is only one (white) arrow from Atom to WFF. The model represents a well-formed formula, which can be composed of nested logical connectives, so logical connectives have arrows with a diamond. — **Figure 1. Visualization of the metamodel generated from our grammar.** This metamodel can be used to generate the models, i.e., the ASTs. The black arrow with a diamond represents composition (has a) and the white arrow represents extension (is a). The atoms will be the leaf nodes of the AST, notice that there is only one (white) arrow from `Atom` to `WFF`. The model represents a well-formed formula, which can be composed of nested logical connectives, so logical connectives have arrows with a diamond.

Classes

The classes corresponding to the rules are created automatically from the grammar rules. So, by defining the class attributes, we can generate an AST. However, to control the behavior of the classes, we need to create them explicitly and modify them as needed.

Unless the class is abstract, it needs to receive initial parameters. The parameters include the parent which is mandatory and the user-defined attributes. The Atom and Negation classes only take one parameter id and wff respectively. The binary connective classes will need a left-hand side (lhs) and a right-hand side (rhs) parameter which represent the operands. We present below a possible implementation for the custom classes.

from abc import ABC
from typing import Any, List

type Variable = str


class WFF(ABC):
    pass


class Atom(WFF):
    def __init__(self, parent: Any, id: Variable):
        self.parent = parent
        self.id = id


class Negation(WFF):
    def __init__(self, parent: Any, wff: WFF):
        self.parent = parent
        self.wff = wff
        

class Conjunction(WFF):
    def __init__(self, parent: Any, lhs: WFF, rhs: WFF):
        self.parent = parent
        self.lhs = lhs
        self.rhs = rhs


class Disjunction(WFF):
    def __init__(self, parent: Any, lhs: WFF, rhs: WFF):
        self.parent = parent
        self.lhs = lhs
        self.rhs = rhs


class Implication(WFF):
    def __init__(self, parent: Any, lhs: WFF, rhs: WFF):
        self.parent = parent
        self.lhs = lhs
        self.rhs = rhs


class Equivalence(WFF):
    def __init__(self, parent: Any, lhs: WFF, rhs: WFF):
        self.parent = parent
        self.lhs = lhs
        self.rhs = rhs

In part 3 we will instantiate a model from the input WFF and the grammar.