-
-
-The Module System of GF
- -- -8/4/2005 - 10/4 - -
- -Aarne Ranta - -
-
-
-- -8/4/2005 - 10/4 - -
- -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 relates 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 contain -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 this special kind of 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 Geometry.Prop Logic.Prop --all refer to the same category, declared in the module -Logic. - - - -
- cat C ; ===> oper C : Type = T ; - lincat C = T ; - - fun f : A ; ===> oper f : A = t ; - lin f = t ; --Due to this translation, a concrete module -can be opened in the same way as a -resource module; the translation is done -on the fly (it is computationally very cheap). - -
- -Modular grammar engineering often means that some grammarians -focus on the semantics of the domain whereas others take care -of linguistic details. Thus a typical reuse opens a -linguistically oriented resource grammar, -
- abstract Resource = {
- cat S ; NP ; A ;
- fun PredA : NP -> A -> S ;
- }
- concrete ResourceEng of Resource = {
- lincat S = ... ;
- lin PredA = ... ;
- }
-
-The application grammar, instead of giving linearizations
-explicitly, just reduces them to categories and functions in the
-resource grammar:
-
- concrete ArithmeticEng of Arithmetic = LogicEng ** open ResourceEng in {
- lincat Nat = NP ;
- lin Even x = PredA x (regA "even") ;
- }
-
-If the resource grammar is only capable of generating grammatically
-correct expressions, then the grammaticality of the application
-grammar is also guaranteed: the type checker of GF is used as
-grammar checker.
-To guarantee distinctions between categories that have
-the same linearization type, the actual translation used
-in GF adds to every linearization type and linearization
-a lock field,
-
- cat C ; ===> oper C : Type = T ** {lock_C : {}} ;
- lincat C = T ;
-
- fun f : C_1 ... C_n -> C ; ===> oper f : C_1 ... C_n -> C = \x_1,...,x_n ->
- lin f = t ; t x_1 ... x_n ** {lock_C = <>};
-
-(Notice that the latter translation is type-correct because of
-record subtyping, which means that t can ignore the
-lock fields of its arguments.) An application grammarian who
-only uses resource grammar categories and functions never
-needs to write these lock fields herself. Having to do so
-serves as a warning that the grammaticality guarantee given
-by the resource grammar no longer holds.
-
-
-- -However, the separation of declarations and definitions is so -useful a notion that GF also has specific modules types that -resource modules into two parts. In this splitting, -an interface module corresponds to an abstract syntax, -in giving the declarations of operations (and parameter types). -For instance, a generic markup interface would look as follows: -
- interface Markup = open Util in {
- oper Boldface : Str -> Str ;
- oper Heading : Str -> Str ;
- oper markupSS : (Str -> Str) -> SS -> SS = \f,r ->
- ss (f r.s) ;
- }
-
-The definitions of the constants declared in an interface
-are given in an instance module (which is always of
-an interface, in the same way as a concrete is always
-of an abstract). The following instances
-define markup in HTML and latex.
-
- instance MarkupHTML of Markup = open Util in {
- oper Boldface s = "<b>" ++ s ++ "</b>" ;
- oper Heading s = "<h2>" ++ s ++ "</h2>" ;
- }
-
- instance MarkupLatex of Markup = open Util in {
- oper Boldface s = "\\textbf{" ++ s ++ "}" ;
- oper Heading s = "\\section{" ++ s ++ "}" ;
- }
-
-Notice that both interfaces and instances may
-open resources (and also reused top-level grammars).
-An interface may moreover define some of the operations it
-declares; these definitions are inherited by all instances and cannot
-be changed in them. Inheritance by module extension
-is possible, as always, between modules of the same type.
-
-
-- -A module that opens an interface is therefore -incomplete, and has to be completed with an -instance of the interface to become complete. To make -this situation clear, GF requires any module that opens an -interface to be marked as incomplete. Thus -the module -
- incomplete concrete DocMarkup of Doc = open Markup in {
- ...
- }
-
-uses the interface Markup to place markup in
-chosen places in its linearization rules, but the
-implementation of markup - whether in HTML or in LaTeX - is
-left unspecified. This is a powerful way of sharing
-the code of a whole module with just differences in
-the definitions of some constants.
-
-- -Another terminology for incomplete modules is -parametrized modules or functors. -The interface gives the list of parameters -that the functor depends on. - - -
- concrete DocHTML of Doc = DocMarkup with (Markup = MarkupHTML) ; --Instantiation of Markup with MarkupLatex is -another one-liner. - -
- -If more interfaces than one are instantiated, a comma-separated -list of equations in parentheses is used, e.g. -
- concrete RulesIta = CategoriesIta ** RulesRomance with - (TypesRomance = TypesIta), (SyntaxRomance = SyntaxIta) ; --(an example from the GF resource grammar library, where languages for -Romance languages share two interfaces). -All interfaces that are opened in the completed model -must be completed. - -
- -Notice that the completion of an incomplete module -may at the same time extend modules of the same type (which need -not be completions). But it cannot add new judgements. - - -
-abstract A = (A1,...,An **)? -{J1 ; ... ; Jm ; } - -
- -where -
-incomplete? concrete C of A = -(C1,...,Cn **)? -(open O1,...,Ok in)? -{J1 ; ... ; Jm ; } - -
- -where -
- -If the modifier incomplete appears, then any R in -an open specification may also be an interface. - -
- -Semantic conditions: -
-resource R = -(R1,...,Rn **)? -(open O1,...,Ok in)? -{J1 ; ... ; Jm ; } - -
-where -
- -Semantic conditions: -
-interface R = -(R1,...,Rn **)? -(open O1,...,Ok in)? -{J1 ; ... ; Jm ; } - -
-where -
- -Semantic conditions: -
-instance R of I = -(R1,...,Rn **)? -(open O1,...,Ok in)? -{J1 ; ... ; Jm ; } - -
-where -
- -Semantic conditions: -
-concrete C of A = -(C1,...,Cn **)? -B -with -(I1 =J1), ... -, (Im =Jm) ; - -
- -where -
- -August 31, 2007. GF Graduate Course -organized by GSLT: first module -September 13-14 in Gothenburg. - -
- -July 8, 2007. GF 2.8 released. Some highlights: -
- -June 27, 2007. GF 2.8 forthcoming next week. Some highlights: -
- - -December 22, 2006. GF 2.7 released. Some highlights: -
- -October 13, 2006. -PhD defence by Janna Khegai at Chalmers. Thesis - - Language engineering in Grammatical Framework (GF). - -
- -June 22, 2006. -Release of GF version 2.6. Highlights: -
- -March 29, 2006. -GF Quick Reference. Also available in -pdf. - -
- -June 21, 2006. GF 2.5 released. Some highlights: -
- -December 22, 2005. GF 2.4 released. Some highlights: -
-
-
-December 9, 2005.
-
-MCFG/GF library for Prolog, by
-Peter Ljunglöf.
-This means that you can use GF grammars as parts of
-Prolog programs (in the same way as in Java and Haskell
-before).
-
-
-
-December 8, 2005.
-A structured Documentation page on GF.
-
-
-
-December 1, 2005.
-Publicly accessible
-
-Darcs repository
-for latest sources and documents. The snapshots are no longer updated.
-
-
-
-September 22, 2005.
-
-Snapshots: latest source and linux binary packages, for testers
-and developers. See
-GF history for the latest changes.
-
-Notice (1/12):
-Use the
-
-Darcs repository instead!
-
-
-
-July 1, 2005. GF 2.3 released.
-Download from
-SourceForge.
-The GF history lists changes.
-The source package on SourceForge also contains a new GUI and some new grammars.
-
-
-
-June 3, 2005. Started a page on
-history of changes.
-These changes will appear soon in releases.
-
-
-
-May 17, 2005. Version 2.2 released. See
-highlights.
-Download from
-SourceForge.
-
-
-
-May 12, 2005. GF now has a mailing list, to which you can register
-here.
-GF also has a project page on SourceForge,
-
-https://sourceforge.net/projects/gf-tools,
-but this page does not yet have much content.
-
-
-
-May 9, 2005.
-PhD Thesis by
-Kristofer Johannisson:
-
-Formal and Informal Software Specifications.
-
-
-
-
-March 15, 2005.
-Master's thesis by
-Björn Bringert on
-
-Embedded grammars:
-GF grammars that can be used as parts of Java programs. And a
-demo film
-of a multimodal dialogue system built with embedded grammars.
-
-
-
-
-November 9, 2004.
-PhD Thesis by
-Peter Ljunglöf:
-
-Expressivity and Complexity of the Grammatical Framework.
-
-
-
-November 8, 2004. GF 2.1 released.
-Here are the highlights.
-Software available on the GF 2.1 Download
-Page.
-Main novelties in 2.1:
-multiple inheritance of grammar modules,
-speech recognition grammar generation,
-lots of bug fixes.
-Version 2.0 still available
-on the GF 2.0 Download Page.
-If you need something from the previous version of the web page, it is
-still available:
-
-GF 1.2.
-
-
-<7html>
\ No newline at end of file
diff --git a/doc/quick-editor.gif b/doc/quick-editor.gif
deleted file mode 100644
index 0cbe42073..000000000
Binary files a/doc/quick-editor.gif and /dev/null differ
diff --git a/doc/quick-editor.png b/doc/quick-editor.png
deleted file mode 100644
index c840a8108..000000000
Binary files a/doc/quick-editor.png and /dev/null differ