The GF plug-in knows how to translate all Alfa built-in syntax (the various forms of definitions and expressions), and provides default translations of user-defined identifiers. However, to obtain nice text, the user is expected to provide sutiable translations along with any new definitions introduced in a proof. These translations are specified by adding grammatical annotations to definitons. The grammatical annotions are written in a simple language provided by GF.
As a simple example, let's see how to translate the definition of natural numbers and addition of natural numbers to English. We start by defining these things in the usual way in Alfa:
alfa - -plugins GF
We can already obtain an English translation of this. By selecting GF: Eng as the default declaration view from the View menu, we get the following:
It is also possible to select definition(s) and apply commands from the menu window to choose how to present them, e.g., GF: Show in Eng, GF: Show all translation, Show default declaration view. You can also select parts of expressions and apply similar commands to them.
The next step is to tell GF how to translate
+ to English.
We start by considering the translation of
Names of data types (sets) are usually
translated into nouns. In this case we want to use the phrase
natural number. Nouns may be used in both singular and plural
forms, so the translation have to indicate both forms. Fortunately,
the grammatical annotation language provides some auxiliary functions
to make this easy. In the case of regular nouns, for which the plural
form is obtained by adding an
s to the end of the word,
it is particularly easy.
To enter the translation of
Nat in Alfa, select the definition
Nat (or just the name in the LHS of the definition)
and choose the command GF: Change Eng translation of
Nat in the menu window. You should now see a text editor
window containing the default translation of
We can now replace the default translation with the desired one:
Note that strings enclosed in quotes (
") should contain
single words and that the operator
++ is used to form
phrases containg more than one word. The function
takes care of adding an
s to the last word of the
argument phrase, in the places where it is used in the plural form.
When we press OK, the translation of the definitions in the main window will be updated accordingly:
Nat is appropriately translated to a
natural number or natural numbers depending on the context.
We continue with the translation of the constructors
Succ. (To be able to select them and edit their
translations, you probably first have to switch back the declaration view to
While the names of sets behave like nouns, constructors and other
elements of sets behave more like proper names. For
Succ, we enter the following
Zero@_ = mkPN "zero"
Succ@_ n = likeSucc "successor" n
mkPNcreates simple proper names and
likeSuccconstructs phrases like the xxx of yyy, where xxx is a word and yyy is another proper name:
Finally, we add a translation for the operator
choose to translate
a+b to the phrase
the sum of a
and b, which can be used as a proper name.
We now have completed our example, and the final translation to English is:
+ a b = likeSum "sum" a b
+above is 2, so it must always be applied to two arguments. Something like
map (+2) xs, which could otherwise be perfectly reasonable, can at present not be translated correctly.
likeSumand many more). (Not written yet.)