+
+
+The Module System of GF
+ ++ +8/4/2005 + +
+ +Aarne Ranta + +
+
+
++ +8/4/2005 + +
+ +Aarne Ranta + +
+ +This document is meant as an appendix to the GF tutorial, and +presupposes knowledge of GF judgements and expressions. It aims +just to tell what module system adds to the old functionality; +some information is repeated to give understanding on how the +module system related to the already familiar uses of GF grammars. + + + +
+ abstract Logic = {
+ cat Prop ;
+ fun Conj : Prop -> Prop -> Prop ;
+ fun Disj : Prop -> Prop -> Prop ;
+ fun Impl : Prop -> Prop -> Prop ;
+ fun Falsum : Prop ;
+ }
+
+The name of this module is Logic.
+
++ +An abstract module defines an abstract syntax, which +is a language-independent representation of a fragment of language. +It consists of two kinds of judgements: +
+ concrete LogicEng of Logic = {
+ lincat Prop = {s : Str} ;
+ lin Conj a b = {s = a.s ++ "and" ++ b.s} ;
+ lin Disj a b = {s = a.s ++ "or" ++ b.s} ;
+ lin Impl a b = {s = "if" ++ a.s ++ "then" ++ b.s} ;
+ lin Falsum = {s = ["we have a contradiction"]} ;
+ }
+
+The module LogicEng is a concrete syntax of the
+abstract syntax Logic. The GF grammar compiler checks that
+the concrete is valid with respect to the abstract syntax of
+which it is claimed to be. The validity requires that there has to be
++ +There can also be lindef and printname judgements in a +concrete syntax. + + +
+ Impl (Disj Falsum Falsum) Falsum ++has the linearization +
+ if we have a contradiction or we have a contradiction then we have a contradiction ++which in turn can be parsed uniquely as that tree. + + +
+ i LogicEng.gf ++It is also possible to specify the imported grammar(s) on the command +line when invoking GF: +
+ gf LogicEng.gf ++Various compilation flags can be added to both ways of compiling a module: +
+ +Grammar modules can reside in different directories. They can then be found +by means of a search path, which is a flag such as +
+ -path=.:../prelude ++given to the import command or the shell command invoking GF. +(It can also be defined in the grammar file; see below.) The compiler +writes every gfc file in the same directory as the corresponding +gf file. + +
+ +Parsing and linearization can be performed with the parse +(p) and linearize (l) commands, respectively. +For instance, +
+ > l Impl (Disj Falsum Falsum) Falsum + if we have a contradiction or we have a contradiction then we have a contradiction + + > p -cat=Prop "we have a contradiction" + Falsum ++Notice that the parse command needs the parsing category +as a flag. This necessary since a grammar can have several +possible parsing categories ("entry points"). + + + +
+ concrete LogicFre of Logic = {
+ lincat Prop = {s : Str} ;
+ lin Conj a b = {s = a.s ++ "et" ++ b.s} ;
+ lin Disj a b = {s = a.s ++ "ou" ++ b.s} ;
+ lin Impl a b = {s = "si" ++ a.s ++ "alors" ++ b.s} ;
+ lin Falsum = {s = ["nous avons une contradiction"]} ;
+ }
+
+ concrete LogicSymb of Logic = {
+ lincat Prop = {s : Str} ;
+ lin Conj a b = {s = "(" ++ a.s ++ "&" ++ b.s ++ ")"} ;
+ lin Disj a b = {s = "(" ++ a.s ++ "v" ++ b.s ++ ")"} ;
+ lin Impl a b = {s = "(" ++ a.s ++ "->" ++ b.s ++ ")"} ;
+ lin Falsum = {s = "_|_"} ;
+ }
+
+The four modules Logic, LogicEng, LogicFre, and
+LogicSymb together form a multilingual grammar, in which
+it is possible to perform parsing and linearization with respect to any
+of the concrete syntaxes. As a combination of parsing and linearization,
+one can also perform translation from one language to another.
+(By language we mean the set of expressions generated by one
+concrete syntax.)
+
+
++ i LogicEng.gf + i LogicFre.gf + i LogicSymb.gf + pm | wf logic.gfcm ++The "end user" of the grammar only needs the file logic.gfcm to +access all the functionality of the multilingual grammar. It can be +imported in the GF system in the same way as .gf files. But +it can also be used in the Embedded Java Interpreter for GF to +build Java programs of which the multilingual grammar functionalities +(linearization, parsing, translation) form a part. + +
+ +In a multilingual grammar, the concrete syntax module names work as +names of languages that can be selected for linearization and parsing: +
+ > l -lang=LogicFre Impl Falsum Falsum + si nous avons une contradiction alors nous avons une contradiction + + > l -lang=LogicSymb Impl Falsum Falsum + ( _|_ -> _|_ ) + + > p -cat=Prop -lang=LogicSymb "( _|_ & _|_ )" + Conj Falsum Falsum ++The option -multi gives linearization to all languages: +
+ > l -multi Impl Falsum Falsum + if we have a contradiction then we have a contradiction + si nous avons une contradiction alors nous avons une contradiction + ( _|_ -> _|_ ) ++Translation can be obtained by using a pipe from a parser +to a linearizer: +
+ > p -cat=Prop -lang=LogicSymb "( _|_ & _|_ )" | l -lang=LogicEng + if we have a contradiction then we have a contradiction ++ + +
+ resource Util = {
+ oper SS : Type = {s : Str} ;
+ oper ss : Str -> SS = \s -> {s = s} ;
+ oper paren : Str -> Str = \s -> "(" ++ s ++ ")" ;
+ oper infix : Str -> SS -> SS -> SS = \h,x,y ->
+ ss (x.s ++ h ++ y.s) ;
+ oper infixp : Str -> SS -> SS -> SS = \h,x,y ->
+ ss (paren (infix h x y)) ;
+ }
+
+Modules of resource type have two forms of judgement:
+
+ concrete LogicSymb of Logic = open Util in {
+ lincat Prop = SS ;
+ lin Conj = infixp "&" ;
+ lin Disj = infixp "v" ;
+ lin Impl = infixp "->" ;
+ lin Falsum = ss "_|_" ;
+ }
+
+What happens when this variant of LogicSymb is
+compiled is that the oper-defined constants
+of Util are inlined in the
+right-hand-sides of the judgements of LogicSymb,
+and these expressions are partially evaluated, i.e.
+computed as far as possible. The generated gfc file
+will look just like the file generated for the first version
+of LogicSymb - at least, it will do the same job.
+
++ +Several resource modules can be opened +at the same time. If the modules contain same names, the +conflict can be resolved by qualified opening and +reference. For instance, +
+ concrete LogicSymb of Logic = open Util, Prelude in { ...
+ } ;
+
+(where Prelude is a standard library of GF) brings
+into scope two definitions of the constant SS.
+To specify which one is used, you can write
+Util.SS or Prelude.SS instead of just SS.
+You can also introduce abbreviations to avoid long qualifiers, e.g.
+
+ concrete LogicSymb of Logic = open (U=Util), (P=Prelude) in { ...
+ } ;
+
+which means that you can write U.SS and P.SS.
+
+
++ +If you look at any gfc or gfr file generated +by the GF compiler, you see that all names have been replaced by +their qualified variants. This is an important first step (after parsing) +the compiler does. As for the commands in the GF shell, some output +qualified names and some not. The difference does not always result +from firm principles. + + +
+ > i -retain Util.gf ++The command compute_concrete (cc) +can now be used for evaluating expressions that may concain +operations defined in Util: +
+ > cc ss (paren "foo")
+ {s = "(" ++ "foo" ++ ")"}
+
+To find out, what opers are available for a given type,
+the command show_operations (so) can be used:
++ > so SS + Util.ss : Str -> SS ; + Util.infix : Str -> SS -> SS -> SS ; + Util.infixp : Str -> SS -> SS -> SS ; ++ + +
+ +In addition to its special modularity, GF provides inheritance, +which is familiar from other programming languages (in particular, +object-oriented ones). Inheritance means that a module inherits all +judgements from another module; we also say that it extends +the other module. Inheritance is useful to divide big grammars into +smaller units, and also to reuse the same units in different bigger +grammars. + +
+ +The first example of inheritance is for abstract syntax. Let us +extend the module Logic to Arithmetic: +
+ abstract Arithmetic = Logic ** {
+ cat Nat ;
+ fun Even : Nat -> Prop ;
+ fun Odd : Nat -> Prop ;
+ fun Zero : Nat ;
+ fun Succ : Nat -> Nat ;
+ }
+
+In parallel with the extension of the abstract syntax
+Logic to Arithmetic, we can extend
+the concrete syntax LogicEng to ArithmeticEng:
+
+ concrete ArithmeticEng of Arithmetic = LogicEng ** open Util in {
+ lincat Nat = SS ;
+ lin Even x = ss (x.s ++ "is" ++ "even") ;
+ lin Odd x = ss (x.s ++ "is" ++ "odd") ;
+ lin Zero = ss "zero" ;
+ lin Succ x = ss ("the" ++ "successor" ++ "of" ++ x.s) ;
+ }
+
+Another extension of Logic is Geometry,
+
+ abstract Geometry = Logic ** {
+ cat Point ;
+ cat Line ;
+ fun Incident : Point -> Line -> Prop ;
+ }
+
+The corresponding concrete syntax is left as exercise.
+
++ +Inheritance can be multiple, which means that a module +may extend many modules at the same time. Suppose, for instance, +that we want to build a module for mathematics covering both +arithmetic and geometry, and the underlying logic. We then write +
+ abstract Mathematics = Arithmetic, Geometry ** {
+ } ;
+
+We could of course add some new judgements in this module, but
+it is not necessary to do so.
+
++ +The module Mathematics also shows that it is possibe +to extend a module already built by extension. The correctness +criterion for extensions is that the same name +(cat, fun, oper, or param) +may not be defined twice in the resulting union of names. +That the names defined in Logic are "inherited twice" +by Mathematics (via both Arithmetic and +Geometry) is no violation of this rule; the usual +problems of multiple inheritance do not arise, since +the definitions of inherited constants cannot be changed. + + +
+ Mathematics.Prop Arithmetic.Prop Logic.Prop + Geometry.Prop ++all refer to the same category, declared in the module +Logic. + + + +