Preface: This is the official PGF Specification, Version 1.0, but please make sure to refer to the Grammatical Framework main projects page for the offficial release.
So far, we talked about the Portable Grammar Format (PGF) as an abstract concept, but in the actual implementation, we store the compiled grammars in a concrete file format.
This appendix is the reference for the exact format, and it includes details which were intentionally skipped in the previous chapters because they were irrelevant to the main algorithms.
The format described here is a version 1.0 and is produced by GF 3.2. In case, if the format have to be changed in the future, the implementations should maintain backward compatibility.
The GF compiler will dump any PGF file into textual representation with a syntax close to what we used in the different chapters, if it is requested to produce the format pgf_pretty:
gf -make -output-format=pgf_pretty MyGrammar. pgf
Basic Types
The Portable Grammar Format is a binary format where the structures of the grammar are serialized as a sequence of bytes. Every structure is a list of sequentially serialized fields, where every field is either another structure or has a basic type. The allowed basic types are:
- Int8 - 8 bits integer, with sign, represented as a single byte.
- Int16 - 16 bits integer, with sign, represented as a sequence of two bytes where the most significant byte is stored first.
- Int - a 32 bits integer with sign encoded as a sequence of bytes with variable length. The last bit of every byte is an indication for whether there are more bytes left. If the bit is 1, then there is at least one more byte to be read, otherwise this is the last byte in the sequence. The other 7 bits are parts of the stored integer. We store the bits from the least significant to the most significant.
- String - a string in UTF-8 encoding. We first store as Int (a variable length integer) the length of the string in number of Unicode characters and after that we add the UTF-8 encoding of the string itself.
- Float - A double precision floating point number serialized in a big-endian format following the IEEE754 standard.
- List - Many of the object fields are lists of other objects. We say that the field is of type [Object] if it contains a list of objects of type Object. The list is serialized as a variable length integer indicating the length of the list in number of objects, followed by the serialization of the elements of the list.
PGF
The whole PGF file contains only one structure which corresponds to the abstract structure $G$ from Definition 1 in Section 2.1. The structure has the following fields:
| type |
description |
| Int16 |
major PGF version, should be 1. |
| Int16 |
minor PGF version, should be 0. |
| [Flag] |
global flags |
| Abstract |
abstract syntax |
| Concrete |
list of concrete syntaxes |
| If PGF is changed in the future, the version in the first two fields should be updated. |
|
| The implementations can use the version number to maintain backward compatibility. |
|
Flag
The flags are pairs of a name and a literal and store different configuration parameters. They are generated by the compiler and are accessible only internally from the interpreter. By using flags we can add new settings without changing the format.
| type |
description |
| String |
flag name |
| Literal |
flag value |
Abstract
This is the object that represents the abstract syntax A (Definition 2, Section 2.1) of a grammar. The name of the abstract syntax is the name of the top-level abstract module in the grammar. The start category is specified with the flag startcat.
| type |
description |
| String |
the name of the abstract syntax |
| [Flag] |
a list of flags |
| [AbsFun] |
a list of abstract functions |
| [AbsCat] |
a list of abstract categories |
| Note: all lists are sorted by name which makes it easy to do binary search. |
|
AbsFun
Every abstract function is represented with one AbsFun object.
| type |
description |
| String |
the name of the function |
| Type |
function’s type signature |
| Int |
function’s arity |
| Int8 |
a constructor tag: 0 - constructor; 1 - function |
| [Equation] |
definitional equations for this function if it is not a constructor |
| Float |
the probability of the function |
| The constructor tag distinguishes between constructors and computable functions, i.e. we can distinguish between this two judgements: |
|
- constructor: data $f: T$
- function: fun $f: T$
If this is a function, then we also include a list of definitional equations. The list can be empty which means that the function is an axiom. In the cases, when we have at least one equation then the arity is the number of arguments that have to be known in order to do pattern matching. For constructors or axioms the arity is zero.
AbsCat
Every abstract category is represented with one AbsCat object. The object includes the name and the type information for the category plus a list of all functions whose return type is this category. The functions are listed in the order in which they appear in the source code.
| type |
description |
| String |
the name of the category |
| [Hypo] |
a list of hypotheses |
| [CatFun] |
a list of functions in source-code order |
CatFun
This object is used internally to keep a list of abstract functions with their probabilities.
| type |
description |
| String |
the name of the function |
| Float |
the probability of the function |
Type
This is the description of an abstract syntax type. Since the types are monomorphic and in normal form, they have the general form:
$$(X_1 : T_1) → (x_2 : T_2) → … → (x_n: T_n) → C e_1… e_n$$
The list of hypotheses $(x_i: T_i)$ is stored as a list of Hypo objects and the indices $e_1 … e_n$ are stored as a list of expressions.
| type |
description |
| [Hypo] |
a list of hypotheses |
| String |
the name fo the categoary in the return type |
| [Expression] |
indices in the return type |
Hypo
Every Hypo object represents an argument in some function type. Since we support implicit and explicit arguments, the first field tells us whether we have explicit argument i.e. $(x: T)$ or implicit i.e. $({x} : T)$. The next two fields are the name of the bound variable and its type. If no variable is bound then the name is $’_’$.
| type |
description |
| BindType |
the binding type i.e. implicit/explicit argument |
| String |
a variable name or $’_’$ if no variable is bound |
| Type |
the type of the variable |
Equation
Every computable function is represented with a list of equations where the equation is a pair of list of patterns and an expression. All equations must have the same number of patterns which is equal to the arity of the function.
| type |
description |
| [Pattern] |
a sequence of patterns |
| Expression |
an expression |
Pattern
This is the representation of a single pattern in a definitional equation for computable function. The first field is a tag which encodes the kind of pattern.
| type |
description |
| Int8 |
a tag |
- tag=0 - pattern matching on constructor application (i.e. $c; p_1 ; p_2 … p_n$)
| type |
description |
| String |
the name of the constructor |
| [Pattern] |
a list of nested patterns for the arguments |
- tag=1 - a variable type
| type |
description |
| String |
the variable name |
- tag=2 - a pattern which binds a variable but also does nested pattern matching (i.e. $x@p$)
| type |
description |
| String |
the variable name |
| Pattern |
a nested pattern |
-
tag=3 - a wildcard (i.e. $_$).
-
tag=4 - matching a literal i.e. string, integer or float
| type |
description |
| Literal |
the value of the literal |
- tag=5 - pattern matching on an implicit argument (i.e. ${{P}}$)
| type |
description |
| [Pattern] |
the nested pattern |
- tag=6 - an inaccessible pattern $(\sim p)$
| type |
description |
| Expr |
the nested pattern |
Expression
This is the encoding of an abstract syntax expression (tree).
| type |
description |
| Int8 |
a tag |
- tag=0 - a lambda abstraction (i.e. $\\x → …$)
| type |
description |
| BindType |
a tag for implicit/explicit argument |
| String |
the variable name |
| Expression |
the body of the lambda abstraction |
- tag=1 - application (i.e. $f x$)
| type |
description |
| Expression |
the left-hand expression |
| Expression |
the right-hand expression |
| 3. tag=2 - a literal value i.e. string, integer or float type description |
|
| type |
description |
| Literal |
the value of the literal |
| 4. tag=3 - a metavariable (i.e. $?0, ?1,…$) |
|
| type |
description |
| Int |
the id of the metavariable |
- tag=4 - an abstract syntax function
| type |
description |
| String |
the function name |
- tag=5 - a variable
| type |
description |
| Int |
the de Bruijn index of the variable |
- tag=6 - an expression with a type annotation (i.e. $(e: t)$)
| type |
description |
| Expression |
the annotated expression |
| Type |
the type of the expression |
- tag=7 - an implicit argument (i.e. ${e}$)
| type |
description |
| Expression |
the expression for the argument |
Literal
The Literal object represents the built-in kinds of literal constants. It starts with a tag which encodes the type of the constant:
| type |
description |
| Int8 |
literal type |
Currently we support only three types of literals:
- tag=0 - string type
| type |
description |
| String |
the value |
- tag=1 - integer
| type |
description |
| Int |
the value |
- tag=2 - float type
| type |
description |
| Float |
the value |
BindType
The bind type is a tag which encodes whether we have an explicit or an implicit argument.
| type |
description |
| Int8 |
tag |
Concrete
Every concrete syntax C (Definition 3, Section 2.1), in the grammar, is represented with an object. The name of the concrete syntax is the name of the top-level concrete module in the grammar.
| type |
description |
| String |
the name of the concrete syntax |
| [Flag] |
a list of flags |
| [PrintName] |
a list of print names |
| [Sequence] |
a table with sequences (Section 2.8.1) |
| [CncFun] |
a list of concrete functions |
| [LinDef] |
a list of functions for default linearization |
| [ProductionSet] |
a list of production sets |
| [CncCat] |
a list of concrete categories |
| Int |
total number of concrete categories allocated for the grammar |
| Note: The lists Flag, PrintName and CncCat are sorted by name which makes it easy to do binary search. |
|
| Note: The total number of concrete categories is used by the parser to determine whether a given category is part of the grammar, i.e. member of $N^C$, or it was created during the parsing. This is the way to decide when to put metavariables during the tree extraction (Section 2.3.7). |
|
PrintName
Every function or category can have a print name which is a user friendly name that can be displayed in the user interface instead of the real one. The print names are defined in the concrete syntax which makes it easier to localize the user interface to different languages.
| type |
description |
| String |
the name of the function or the category |
| String |
the printable name |
Sequence
This is the representation of a single sequence in PMCFG, produced during the common subexpression optimization (Section 2.8.1).
| type |
description |
| [Symbol] |
a list of symbols |
Symbol
The Symbol (Definition 4, Section 2.1) represents either a terminal or a function argument in some sequence. The representation starts with a tag encoding the type of the symbol:
| type |
description |
| Int8 |
expression tag |
The supported symbols are:
- tag=0. This is the representation of an argument, i.e. a pair $\langle k; l \rangle$ ) where $k$ is the argument index and $l$ is the constituent index.
| type |
description |
| Int |
argument index |
| Int |
constituent index |
- tag=1 This is again an argument but we use different tag to indicate that the target can be a literal category (see Section 2.6). If the target category is not a new fresh category, generated by the parser, then it is treated as a literal category. In the pgf_pretty format, we print this kind of symbols as ${d; r}$ instead of $\langle d; r \rangle$ .
| type |
description |
| Int |
argument index |
| Int |
constituent index |
- tag=2 A high-order argument i.e. $\langle d; $r)$ (Section 2.7).
| type |
description |
| Int |
argument index |
| Int |
variable number |
- tag=3 This is a terminal symbol and represents a list of tokens.
| type |
description |
| [String] |
sequence of tokens |
- tag=4 An alternative terminal symbol representing phrase, whose form depends on the prefix of the next token. It corresponds to the pre construction in GF and encodes variations like a/an in English.
| type |
description |
| [String] |
the default form |
| [Alternative] |
a sequence of alternatives |
Alternative
Every Alternative represents one possible form of a phrase which is dependent on the prefix of the next token. For example when the construction:
$$pre {\text{“beau”}; \text{“bel”/"‘ami"}}$$
is compiled then the alternative bel / ami will be represented by the pair ([“bel”],[" ami"]).
| type |
description |
| [String] |
The tokens to use if the prefix matches |
| [String] |
The prefix matched with the following tokens |
CncFun
This is the definition of a single concrete function (Definition 4, Section 2.1). The first field is the name of the corresponding abstract function which gives us the direct definition of the $\psi_F$ mapping. The second field is the function definition given as a list of indices pointing to the sequences table (see the Concrete object).
| type |
description |
| String |
the name of the corresponding abstract function |
| [Int] |
list of indices into the sequences array |
LinDef
The LinDef object stores the list of all concrete functions that can be used for the default linearization of some concrete category (Section 2.5).
| type |
description |
| Int |
the concrete category |
| [Int] |
a list of concrete functions |
ProductionSet
A group of productions with the same result category. The productions are grouped because this makes it easier for the parser to find the relevant productions in the prediction step:
| type |
description |
| Int |
the result category |
| [Production] |
a list of productions |
Production
The production can be either an application of some function or a coercion.
| type |
description |
| Int8 |
tag |
- tag=0 the production is an application (Definition 4, Section 2.1):
| type |
description |
| Int |
the concrete function |
| [PArg] |
a list of arguments |
- tag=1 the production is a coercion (Section 2.8.1):
| type |
description |
| Int8 |
a concrete category |
PArg
An argument in a production.
| type |
description |
| [Int] |
the categories of the high-order arguments (Section 2.7) |
| Int |
a concrete category |
CncCat
This is the representation of a set of concrete categories which map to the same abstract category. Since all concrete categories generated from the same abstract category are always represented as consequtive integers, here we store only the first and the last cate-gory. The compiler also generates a name for every constituent so here we have the list of names. The length of the list is equal to the dimension of the category.
| type |
description |
| String |
the name of the corresponding (by $\psi_N$) abstract category |
| Int |
the first concrete category |
| Int |
the last concrete category |
| [String] |
a list of constituent names |