Abstract syntax of PFCSes.
We define an abstract syntax straightforwardly derived from the concrete syntax.
Besides the abstract syntax trees (ASTs), we define some operations on ASTs, and some constructors to conveniently build ASTs. We also define a notion of indexed names, useful for building ``parameterized'' PFCSes.
We also formalize the mapping from the concrete syntax trees (CSTs) defined by the grammar to the corresponding ASTs.