Grammatical Framework Bibliography
-
-Aarne Ranta-Wed Dec 14 18:13:03 2011 -
Grammatical Framework BibliographyGrammatical Framework BibliographyIn reverse temporal order:
@@ -773,8 +776,10 @@ The type theory and type checker of GF.In alphabetical order:
@@ -864,6 +869,6 @@ A. Ranta. Interprets Lambek Calculus in type theory and defines some extensions. - + diff --git a/doc/gf-bibliography.t2t b/doc/gf-bibliography.t2t index 76324bdf9..33297de41 100644 --- a/doc/gf-bibliography.t2t +++ b/doc/gf-bibliography.t2t @@ -9,6 +9,7 @@ Aarne Ranta %!style:../css/style.css %!target:html %!options(html): --toc +%!postproc(html):GF Quick Referencehelp), and help on invoking
GF with (gf -help).
+
This is a complete example of a GF grammar divided into three modules in files. The grammar recognizes the @@ -51,6 +54,7 @@ phrases one pizza and two pizzas.
File Order.gf:
abstract Order = {
cat
@@ -61,9 +65,11 @@ File Order.gf:
Pizza : Item ;
}
+
File OrderEng.gf (the top file):
--# -path=.:prelude
concrete OrderEng of Order =
@@ -78,9 +84,11 @@ File OrderEng.gf (the top file):
Pizza = regNoun "pizza" ;
}
+
File Res.gf:
resource Res = open Prelude in {
param Num = Sg | Pl ;
@@ -92,18 +100,21 @@ File Res.gf:
} ;
}
+
To use this example, do
+
% gf -- in shell: start GF
> i OrderEng.gf -- in GF: import grammar
> p "one pizza" -- parse string
> l Two Pizza -- linearize tree
-
+
One module per file.
File named Foo.gf contains module named
@@ -112,32 +123,39 @@ File named Foo.gf contains module named
Each module has the structure
+
moduletypename =
Inherits ** -- optional
open Opens in -- optional
{ Judgements }
+
Inherits are names of modules of the same type. Inheritance can be restricted:
+
Mo[f,g], -- inherit only f,g from Mo
Lo-[f,g] -- inheris all but f,g from Lo
+
Opens are possible in concrete and resource.
They are names of modules of these two types, possibly
qualified:
(M = Mo), -- refer to f as M.f or Mo.f
(Lo = Lo) -- refer to f as Lo.f
+
Module types and judgements in them:
+
abstract A -- cat, fun, def, data
concrete C of A -- lincat, lin, lindef, printname
@@ -154,6 +172,7 @@ Module types and judgements in them:
CI with instantiates a functor by
(I = J) instances of open interfaces
+
The forms
param, oper
@@ -164,15 +183,18 @@ not inherited to extensions.
All modules can moreover have flags and comments.
Comments have the forms
-- till the end of line
{- any number of lines between -}
--# used for compiler pragmas
+
A concrete can be opened like a resource.
It is translated as follows:
cat C ---> oper C : Type =
lincat C = T T ** {lock_C : {}}
@@ -180,12 +202,15 @@ It is translated as follows:
fun f : G -> C ---> oper f : A* -> C* = \g ->
lin f = t t g ** {lock_C = <>}
+
An abstract can be opened like an interface.
Any concrete of it then works as an instance.
cat C -- declare category C cat C (x:A)(y:B x) -- dependent category C @@ -213,26 +238,32 @@ Any+concreteof it then works as aninstance. flags p=v -- set value of flag p
Judgements are terminated by semicolons (;).
Subsequent judgments of the same form may share the
keyword:
cat C ; D ; -- same as cat C ; cat D ;+
Judgements can also share RHS:
+fun f,g : A -- same as fun f : A ; g : A- +
Abstract syntax (in fun):
C -- basic type, if cat C
C a b -- basic type for dep. category
@@ -244,9 +275,11 @@ Abstract syntax (in fun):
Float -- predefined float type
String -- predefined string type
+
Concrete syntax (in lincat):
Str -- token lists
P -- parameter type, if param P
@@ -259,9 +292,11 @@ Concrete syntax (in lincat):
{p1 : A ; p2 : B ; p3 : C}
Ints n -- type of n first integers
+
Resource (in oper): all those of concrete, plus
Tok -- tokens (subtype of Str)
A -> B -- functions from A to B
@@ -270,32 +305,40 @@ Resource (in oper): all those of concrete, plus
PType -- parameter type
Type -- any type
+
As parameter types, one can use any finite type:
P defined in param P,
Ints n, and record types of parameter types.
Syntax trees = full function applications
+f a b -- : C if fun f : A -> B -> C 1977 -- : Int 3.14 -- : Float "foo" -- : String+
Higher-Order Abstract syntax (HOAS): functions as arguments:
+
F a (\x -> c) -- : C if a : A, c : C (x : B),
fun F : A -> (B -> C) -> C
+
Tokens and token lists
+"hello" -- : Tok, singleton Str "hello" ++ "world" -- : Str @@ -303,17 +346,21 @@ Tokens and token lists "hello" + "world" -- : Tok, computes to "helloworld" [] -- : Str, empty list+
Parameters
+
Sg -- atomic constructor
VPres Sg P2 -- applied constructor
{n = Sg ; p = P3} -- record of parameters
+
Tables
+
table { -- by full branches
Sg => "mouse" ;
@@ -334,9 +381,11 @@ Tables
t ! p -- select p from table t
case e of {...} -- same as table {...} ! e
+
Records
+
{s = "Liz"; g = Fem} -- record in full form
{s,t = "et"} -- same as {s = "et";t= "et"}
@@ -345,17 +394,21 @@ Records
<a,b,c> -- tuple, same as {p1=a;p2=b;p3=c}
+
Functions
+\x -> t -- lambda abstract \x,y -> t -- same as \x -> \y -> t \x,_ -> t -- binding not in t+
Local definitions
+
let x : A = d in t -- let definition
let x = d in t -- let defin, type inferred
@@ -365,42 +418,52 @@ Local definitions
t where {...} -- same as let ... in t
+
Free variation
+
variants {x ; y} -- both x and y possible
variants {} -- nothing possible
+
Prefix-dependent choices
+
pre {"a" ; "an" / v} -- "an" before v, "a" otherw.
strs {"a" ; "i" ;"o"}-- list of condition prefixes
+
Typed expression
+<t:T> -- same as t, to help type inference+
Accessing bound variables in lin: use fields $1, $2, $3,....
Example:
fun F : (A : Set) -> (El A -> Prop) -> Prop ;
lin F A B = {s = ["for all"] ++ A.s ++ B.$1 ++ B.s}
-
+
These patterns can be used in branches of table and
case expressions. Patterns are matched in the order in
which they appear in the grammar.
C -- atomic param constructor C p q -- param constr. applied to patterns @@ -416,9 +479,10 @@ which they appear in the grammar. p + "s" -- sequence of two string patterns p* -- repetition of a string pattern- +
-- lib/prelude/Predef.gf
drop : Int -> Tok -> Tok -- drop prefix of length
@@ -448,12 +512,14 @@ which they appear in the grammar.
if_then_else : (A : Type) -> Bool -> A -> A -> A
if_then_Str : Bool -> Str -> Str -> Str
-
+
Flags can appear, with growing priority,
+flags and without dash (-)
gf when invoked, with dash
@@ -463,6 +529,7 @@ Flags can appear, with growing priority,
Some common flags used in grammars:
+startcat=cat use this category as default @@ -483,19 +550,24 @@ Some common flags used in grammars: optimize=all usually good for resource optimize=noexpand for resource, if =all too big+
For the full set of values for FLAG,
use on-line h -FLAG.
Colon-separated lists of directories searched in the given order:
+--# -path=.:../abstract:../common:prelude+
This can be (in order of growing preference), as
first line in the top file, as flag to gf
@@ -507,8 +579,10 @@ If the environment variabls GF_LIB_PATH is defined, its
value is automatically prefixed to each directory to
extend the original search path.
Old GF (before GF 2.0): all judgements in any kinds of modules, @@ -519,9 +593,11 @@ if it lacks a module header.
Context-free (file foo.cf). The form of rules is e.g.
Fun. S ::= NP "is" AP ;+
If Fun is omitted, it is generated automatically.
Rules must be one per line. The RHS can be empty.
@@ -529,9 +605,11 @@ Rules must be one per line. The RHS can be empty.
Extended BNF (file foo.ebnf). The form of rules is e.g.
S ::= (NP+ ("is" | "was") AP | V NP*) ;
+
where the RHS is a regular expression of categories
and quoted tokens: "foo", CAT, T U, T|U, T*, T+, T?, or empty.
@@ -541,9 +619,11 @@ Rule labels are generated automatically.
Probabilistic grammars (not a separate format).
You can set the probability of a function f (in its value category) by
--# prob f 0.009+
These are put into a file given to GF using the probs=File flag
on command line. This file can be the grammar file itself.
@@ -551,20 +631,26 @@ on command line. This file can be the grammar file itself.
Example-based grammars (file foo.gfe). Expressions of the form
in Cat "example string"+
are preprocessed by using a parser given by the flag
+--# -resource=File+
and the result is written to foo.gf.