![[Def of Nat and +]](P/gf0.gif)
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.
alfa - -plugins 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:
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:
![[GF: Eng view before adding grammatical annotations]](P/gf1.gif)
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 Nat and
+ to English.
We start by considering the translation of Nat.
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
of 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 Nat:
![[Editor with default grammatical annotation for Nat]](P/gf2.gif)
We can now replace the default translation with the desired one:
![[Editor with user provided grammatical annotation for Nat]](P/gf3.gif)
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 regCN
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:
![[Main window with improved translation of Nat]](P/gf4.gif)
Note that Nat is appropriately translated to a
natural number or natural numbers depending on the context.
We continue with the translation of the constructors Zero
and Succ. (To be able to select them and edit their
translations, you probably first have to switch back the declaration view to
Complete definitions.)
While the names of sets behave like nouns, constructors and other
elements of sets behave more like proper names. For
Zero and Succ, we enter the following
translations:
Zero@_ = mkPN "zero"Succ@_ n = likeSucc "successor" nmkPN creates simple proper names and
likeSucc constructs 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 +. We
choose to translate a+b to the phrase the sum of a
and b, which can be used as a proper name.
+ a b = likeSum "sum" a b
![[Final English translation of Nat and +]](P/gf5.gif)
+
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.
regCN, mkPN, likeSucc,
mkPN, likeSum and many more). (Not written yet.)