forked from GitHub/gf-core
0dbe9a6d50
Most of the pages on the GF web site have an exemplary simple design, with just one column of text. This make them adapt exceptionally well to screens of different sizes. In particular, they should be easy to read even on smartphones. However, smartphone browsers like Mobile Safari and the default Android Browser assume that pages do *not* adapt well to small screens, so by default they emulate a big screen, forcing the user to zoom in to a part of the page to be able to read it. By adding the meta tag <meta name = "viewport" content = "width = device-width"> the big screen emulation can be turned off, allowing pages to be formatted to fit the actual screen size and text to be displayed at a readable size.
665 lines
16 KiB
HTML
665 lines
16 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
|
|
<HTML>
|
|
<HEAD>
|
|
<META NAME="generator" CONTENT="http://txt2tags.org">
|
|
<LINK REL="stylesheet" TYPE="text/css" HREF="../css/style.css">
|
|
<meta name = "viewport" content = "width = device-width"><TITLE>GF Quick Reference</TITLE>
|
|
</HEAD><BODY BGCOLOR="white" TEXT="black">
|
|
<CENTER>
|
|
<H1><a href="../"><IMG src="../doc/Logos/gf0.png"></a>GF Quick Reference</H1>
|
|
<FONT SIZE="4"><I>Aarne Ranta</I></FONT><BR>
|
|
<FONT SIZE="4">April 4, 2006</FONT>
|
|
</CENTER>
|
|
|
|
<P></P>
|
|
<HR NOSHADE SIZE=1>
|
|
<P></P>
|
|
|
|
<UL>
|
|
<LI><A HREF="#toc1">A complete example</A>
|
|
<LI><A HREF="#toc2">Modules and files</A>
|
|
<LI><A HREF="#toc3">Judgements</A>
|
|
<LI><A HREF="#toc4">Types</A>
|
|
<LI><A HREF="#toc5">Expressions</A>
|
|
<LI><A HREF="#toc6">Pattern matching</A>
|
|
<LI><A HREF="#toc7">Sample library functions</A>
|
|
<LI><A HREF="#toc8">Flags</A>
|
|
<LI><A HREF="#toc9">File paths</A>
|
|
<LI><A HREF="#toc10">Alternative grammar formats</A>
|
|
<LI><A HREF="#toc11">References</A>
|
|
</UL>
|
|
|
|
<P></P>
|
|
<HR NOSHADE SIZE=1>
|
|
<P></P>
|
|
<P>
|
|
This is a quick reference on GF grammars. It aims to
|
|
cover all forms of expression available when writing
|
|
grammars. It assumes basic knowledge of GF, which
|
|
can be acquired from the
|
|
<A HREF="http://www.grammaticalframework.org/doc/tutorial/gf-tutorial.html">GF Tutorial</A>.
|
|
Help on GF commands is obtained on line by the
|
|
help command (<CODE>help</CODE>), and help on invoking
|
|
GF with (<CODE>gf -help</CODE>).
|
|
</P>
|
|
|
|
<A NAME="toc1"></A>
|
|
<H3>A complete example</H3>
|
|
|
|
<P>
|
|
This is a complete example of a GF grammar divided
|
|
into three modules in files. The grammar recognizes the
|
|
phrases <I>one pizza</I> and <I>two pizzas</I>.
|
|
</P>
|
|
<P>
|
|
File <CODE>Order.gf</CODE>:
|
|
</P>
|
|
|
|
<PRE>
|
|
abstract Order = {
|
|
cat
|
|
Order ;
|
|
Item ;
|
|
fun
|
|
One, Two : Item -> Order ;
|
|
Pizza : Item ;
|
|
}
|
|
</PRE>
|
|
|
|
<P>
|
|
File <CODE>OrderEng.gf</CODE> (the top file):
|
|
</P>
|
|
|
|
<PRE>
|
|
--# -path=.:prelude
|
|
concrete OrderEng of Order =
|
|
open Res, Prelude in {
|
|
flags startcat=Order ;
|
|
lincat
|
|
Order = SS ;
|
|
Item = {s : Num => Str} ;
|
|
lin
|
|
One it = ss ("one" ++ it.s ! Sg) ;
|
|
Two it = ss ("two" ++ it.s ! Pl) ;
|
|
Pizza = regNoun "pizza" ;
|
|
}
|
|
</PRE>
|
|
|
|
<P>
|
|
File <CODE>Res.gf</CODE>:
|
|
</P>
|
|
|
|
<PRE>
|
|
resource Res = open Prelude in {
|
|
param Num = Sg | Pl ;
|
|
oper regNoun : Str -> {s : Num => Str} =
|
|
\dog -> {s = table {
|
|
Sg => dog ;
|
|
_ => dog + "s"
|
|
}
|
|
} ;
|
|
}
|
|
</PRE>
|
|
|
|
<P>
|
|
To use this example, do
|
|
</P>
|
|
|
|
<PRE>
|
|
% gf -- in shell: start GF
|
|
> i OrderEng.gf -- in GF: import grammar
|
|
> p "one pizza" -- parse string
|
|
> l Two Pizza -- linearize tree
|
|
</PRE>
|
|
|
|
<A NAME="toc2"></A>
|
|
<H3>Modules and files</H3>
|
|
|
|
<P>
|
|
One module per file.
|
|
File named <CODE>Foo.gf</CODE> contains module named
|
|
<CODE>Foo</CODE>.
|
|
</P>
|
|
<P>
|
|
Each module has the structure
|
|
</P>
|
|
|
|
<PRE>
|
|
moduletypename =
|
|
Inherits ** -- optional
|
|
open Opens in -- optional
|
|
{ Judgements }
|
|
</PRE>
|
|
|
|
<P>
|
|
Inherits are names of modules of the same type.
|
|
Inheritance can be restricted:
|
|
</P>
|
|
|
|
<PRE>
|
|
Mo[f,g], -- inherit only f,g from Mo
|
|
Lo-[f,g] -- inheris all but f,g from Lo
|
|
</PRE>
|
|
|
|
<P>
|
|
Opens are possible in <CODE>concrete</CODE> and <CODE>resource</CODE>.
|
|
They are names of modules of these two types, possibly
|
|
qualified:
|
|
</P>
|
|
|
|
<PRE>
|
|
(M = Mo), -- refer to f as M.f or Mo.f
|
|
(Lo = Lo) -- refer to f as Lo.f
|
|
</PRE>
|
|
|
|
<P>
|
|
Module types and judgements in them:
|
|
</P>
|
|
|
|
<PRE>
|
|
abstract A -- cat, fun, def, data
|
|
concrete C of A -- lincat, lin, lindef, printname
|
|
resource R -- param, oper
|
|
|
|
interface I -- like resource, but can have
|
|
oper f : T without definition
|
|
instance J of I -- like resource, defines opers
|
|
that I leaves undefined
|
|
incomplete -- functor: concrete that opens
|
|
concrete CI of A = one or more interfaces
|
|
open I in ...
|
|
concrete CJ of A = -- completion: concrete that
|
|
CI with instantiates a functor by
|
|
(I = J) instances of open interfaces
|
|
</PRE>
|
|
|
|
<P>
|
|
The forms
|
|
<CODE>param</CODE>, <CODE>oper</CODE>
|
|
may appear in <CODE>concrete</CODE> as well, but are then
|
|
not inherited to extensions.
|
|
</P>
|
|
<P>
|
|
All modules can moreover have <CODE>flags</CODE> and comments.
|
|
Comments have the forms
|
|
</P>
|
|
|
|
<PRE>
|
|
-- till the end of line
|
|
{- any number of lines between -}
|
|
--# used for compiler pragmas
|
|
</PRE>
|
|
|
|
<P>
|
|
A <CODE>concrete</CODE> can be opened like a <CODE>resource</CODE>.
|
|
It is translated as follows:
|
|
</P>
|
|
|
|
<PRE>
|
|
cat C ---> oper C : Type =
|
|
lincat C = T T ** {lock_C : {}}
|
|
|
|
fun f : G -> C ---> oper f : A* -> C* = \g ->
|
|
lin f = t t g ** {lock_C = <>}
|
|
</PRE>
|
|
|
|
<P>
|
|
An <CODE>abstract</CODE> can be opened like an <CODE>interface</CODE>.
|
|
Any <CODE>concrete</CODE> of it then works as an <CODE>instance</CODE>.
|
|
</P>
|
|
|
|
<A NAME="toc3"></A>
|
|
<H3>Judgements</H3>
|
|
|
|
<PRE>
|
|
cat C -- declare category C
|
|
cat C (x:A)(y:B x) -- dependent category C
|
|
cat C A B -- same as C (x : A)(y : B)
|
|
fun f : T -- declare function f of type T
|
|
def f = t -- define f as t
|
|
def f p q = t -- define f by pattern matching
|
|
data C = f | g -- set f,g as constructors of C
|
|
data f : A -> C -- same as
|
|
fun f : A -> C; data C=f
|
|
|
|
lincat C = T -- define lin.type of cat C
|
|
lin f = t -- define lin. of fun f
|
|
lin f x y = t -- same as lin f = \x y -> t
|
|
lindef C = \s -> t -- default lin. of cat C
|
|
printname fun f = s -- printname shown in menus
|
|
printname cat C = s -- printname shown in menus
|
|
printname f = s -- same as printname fun f = s
|
|
|
|
param P = C | D Q R -- define parameter type P
|
|
with constructors
|
|
C : P, D : Q -> R -> P
|
|
oper h : T = t -- define oper h of type T
|
|
oper h = t -- omit type, if inferrable
|
|
|
|
flags p=v -- set value of flag p
|
|
</PRE>
|
|
|
|
<P>
|
|
Judgements are terminated by semicolons (<CODE>;</CODE>).
|
|
Subsequent judgments of the same form may share the
|
|
keyword:
|
|
</P>
|
|
|
|
<PRE>
|
|
cat C ; D ; -- same as cat C ; cat D ;
|
|
</PRE>
|
|
|
|
<P>
|
|
Judgements can also share RHS:
|
|
</P>
|
|
|
|
<PRE>
|
|
fun f,g : A -- same as fun f : A ; g : A
|
|
</PRE>
|
|
|
|
<A NAME="toc4"></A>
|
|
<H3>Types</H3>
|
|
|
|
<P>
|
|
Abstract syntax (in <CODE>fun</CODE>):
|
|
</P>
|
|
|
|
<PRE>
|
|
C -- basic type, if cat C
|
|
C a b -- basic type for dep. category
|
|
(x : A) -> B -- dep. functions from A to B
|
|
(_ : A) -> B -- nondep. functions from A to B
|
|
(p,q : A) -> B -- same as (p : A)-> (q : A) -> B
|
|
A -> B -- same as (_ : A) -> B
|
|
Int -- predefined integer type
|
|
Float -- predefined float type
|
|
String -- predefined string type
|
|
</PRE>
|
|
|
|
<P>
|
|
Concrete syntax (in <CODE>lincat</CODE>):
|
|
</P>
|
|
|
|
<PRE>
|
|
Str -- token lists
|
|
P -- parameter type, if param P
|
|
P => B -- table type, if P param. type
|
|
{s : Str ; p : P}-- record type
|
|
{s,t : Str} -- same as {s : Str ; t : Str}
|
|
{a : A} **{b : B}-- record type extension, same as
|
|
{a : A ; b : B}
|
|
A * B * C -- tuple type, same as
|
|
{p1 : A ; p2 : B ; p3 : C}
|
|
Ints n -- type of n first integers
|
|
</PRE>
|
|
|
|
<P>
|
|
Resource (in <CODE>oper</CODE>): all those of concrete, plus
|
|
</P>
|
|
|
|
<PRE>
|
|
Tok -- tokens (subtype of Str)
|
|
A -> B -- functions from A to B
|
|
Int -- integers
|
|
Strs -- list of prefixes (for pre)
|
|
PType -- parameter type
|
|
Type -- any type
|
|
</PRE>
|
|
|
|
<P>
|
|
As parameter types, one can use any finite type:
|
|
<CODE>P</CODE> defined in <CODE>param P</CODE>,
|
|
<CODE>Ints n</CODE>, and record types of parameter types.
|
|
</P>
|
|
|
|
<A NAME="toc5"></A>
|
|
<H3>Expressions</H3>
|
|
|
|
<P>
|
|
Syntax trees = full function applications
|
|
</P>
|
|
|
|
<PRE>
|
|
f a b -- : C if fun f : A -> B -> C
|
|
1977 -- : Int
|
|
3.14 -- : Float
|
|
"foo" -- : String
|
|
</PRE>
|
|
|
|
<P>
|
|
Higher-Order Abstract syntax (HOAS): functions as arguments:
|
|
</P>
|
|
|
|
<PRE>
|
|
F a (\x -> c) -- : C if a : A, c : C (x : B),
|
|
fun F : A -> (B -> C) -> C
|
|
</PRE>
|
|
|
|
<P>
|
|
Tokens and token lists
|
|
</P>
|
|
|
|
<PRE>
|
|
"hello" -- : Tok, singleton Str
|
|
"hello" ++ "world" -- : Str
|
|
["hello world"] -- : Str, same as "hello" ++ "world"
|
|
"hello" + "world" -- : Tok, computes to "helloworld"
|
|
[] -- : Str, empty list
|
|
</PRE>
|
|
|
|
<P>
|
|
Parameters
|
|
</P>
|
|
|
|
<PRE>
|
|
Sg -- atomic constructor
|
|
VPres Sg P2 -- applied constructor
|
|
{n = Sg ; p = P3} -- record of parameters
|
|
</PRE>
|
|
|
|
<P>
|
|
Tables
|
|
</P>
|
|
|
|
<PRE>
|
|
table { -- by full branches
|
|
Sg => "mouse" ;
|
|
Pl => "mice"
|
|
}
|
|
table { -- by pattern matching
|
|
Pl => "mice" ;
|
|
_ => "mouse" -- wildcard pattern
|
|
}
|
|
table {
|
|
n => regn n "cat" -- variable pattern
|
|
}
|
|
table Num {...} -- table given with arg. type
|
|
table ["ox"; "oxen"] -- table as course of values
|
|
\\_ => "fish" -- same as table {_ => "fish"}
|
|
\\p,q => t -- same as \\p => \\q => t
|
|
|
|
t ! p -- select p from table t
|
|
case e of {...} -- same as table {...} ! e
|
|
</PRE>
|
|
|
|
<P>
|
|
Records
|
|
</P>
|
|
|
|
<PRE>
|
|
{s = "Liz"; g = Fem} -- record in full form
|
|
{s,t = "et"} -- same as {s = "et";t= "et"}
|
|
{s = "Liz"} ** -- record extension: same as
|
|
{g = Fem} {s = "Liz" ; g = Fem}
|
|
|
|
<a,b,c> -- tuple, same as {p1=a;p2=b;p3=c}
|
|
</PRE>
|
|
|
|
<P>
|
|
Functions
|
|
</P>
|
|
|
|
<PRE>
|
|
\x -> t -- lambda abstract
|
|
\x,y -> t -- same as \x -> \y -> t
|
|
\x,_ -> t -- binding not in t
|
|
</PRE>
|
|
|
|
<P>
|
|
Local definitions
|
|
</P>
|
|
|
|
<PRE>
|
|
let x : A = d in t -- let definition
|
|
let x = d in t -- let defin, type inferred
|
|
let x=d ; y=e in t -- same as
|
|
let x=d in let y=e in t
|
|
let {...} in t -- same as let ... in t
|
|
|
|
t where {...} -- same as let ... in t
|
|
</PRE>
|
|
|
|
<P>
|
|
Free variation
|
|
</P>
|
|
|
|
<PRE>
|
|
variants {x ; y} -- both x and y possible
|
|
variants {} -- nothing possible
|
|
</PRE>
|
|
|
|
<P>
|
|
Prefix-dependent choices
|
|
</P>
|
|
|
|
<PRE>
|
|
pre {"a" ; "an" / v} -- "an" before v, "a" otherw.
|
|
strs {"a" ; "i" ;"o"}-- list of condition prefixes
|
|
</PRE>
|
|
|
|
<P>
|
|
Typed expression
|
|
</P>
|
|
|
|
<PRE>
|
|
<t:T> -- same as t, to help type inference
|
|
</PRE>
|
|
|
|
<P>
|
|
Accessing bound variables in <CODE>lin</CODE>: use fields <CODE>$1, $2, $3,...</CODE>.
|
|
Example:
|
|
</P>
|
|
|
|
<PRE>
|
|
fun F : (A : Set) -> (El A -> Prop) -> Prop ;
|
|
lin F A B = {s = ["for all"] ++ A.s ++ B.$1 ++ B.s}
|
|
</PRE>
|
|
|
|
<A NAME="toc6"></A>
|
|
<H3>Pattern matching</H3>
|
|
|
|
<P>
|
|
These patterns can be used in branches of <CODE>table</CODE> and
|
|
<CODE>case</CODE> expressions. Patterns are matched in the order in
|
|
which they appear in the grammar.
|
|
</P>
|
|
|
|
<PRE>
|
|
C -- atomic param constructor
|
|
C p q -- param constr. applied to patterns
|
|
x -- variable, matches anything
|
|
_ -- wildcard, matches anything
|
|
"foo" -- string
|
|
56 -- integer
|
|
{s = p ; y = q} -- record, matches extensions too
|
|
<p,q> -- tuple, same as {p1=p ; p2=q}
|
|
p | q -- disjunction, binds to first match
|
|
x@p -- binds x to what p matches
|
|
- p -- negation
|
|
p + "s" -- sequence of two string patterns
|
|
p* -- repetition of a string pattern
|
|
</PRE>
|
|
|
|
<A NAME="toc7"></A>
|
|
<H3>Sample library functions</H3>
|
|
|
|
<PRE>
|
|
-- lib/prelude/Predef.gf
|
|
drop : Int -> Tok -> Tok -- drop prefix of length
|
|
take : Int -> Tok -> Tok -- take prefix of length
|
|
tk : Int -> Tok -> Tok -- drop suffix of length
|
|
dp : Int -> Tok -> Tok -- take suffix of length
|
|
occur : Tok -> Tok -> PBool -- test if substring
|
|
occurs : Tok -> Tok -> PBool -- test if any char occurs
|
|
show : (P:Type) -> P ->Tok -- param to string
|
|
read : (P:Type) -> Tok-> P -- string to param
|
|
toStr : (L:Type) -> L ->Str -- find "first" string
|
|
|
|
-- lib/prelude/Prelude.gf
|
|
param Bool = True | False
|
|
oper
|
|
SS : Type -- the type {s : Str}
|
|
ss : Str -> SS -- construct SS
|
|
cc2 : (_,_ : SS) -> SS -- concat SS's
|
|
optStr : Str -> Str -- string or empty
|
|
strOpt : Str -> Str -- empty or string
|
|
bothWays : Str -> Str -> Str -- X++Y or Y++X
|
|
init : Tok -> Tok -- all but last char
|
|
last : Tok -> Tok -- last char
|
|
prefixSS : Str -> SS -> SS
|
|
postfixSS : Str -> SS -> SS
|
|
infixSS : Str -> SS -> SS -> SS
|
|
if_then_else : (A : Type) -> Bool -> A -> A -> A
|
|
if_then_Str : Bool -> Str -> Str -> Str
|
|
</PRE>
|
|
|
|
<A NAME="toc8"></A>
|
|
<H3>Flags</H3>
|
|
|
|
<P>
|
|
Flags can appear, with growing priority,
|
|
</P>
|
|
|
|
<UL>
|
|
<LI>in files, judgement <CODE>flags</CODE> and without dash (<CODE>-</CODE>)
|
|
<LI>as flags to <CODE>gf</CODE> when invoked, with dash
|
|
<LI>as flags to various GF commands, with dash
|
|
</UL>
|
|
|
|
<P>
|
|
Some common flags used in grammars:
|
|
</P>
|
|
|
|
<PRE>
|
|
startcat=cat use this category as default
|
|
|
|
lexer=literals int and string literals recognized
|
|
lexer=code like program code
|
|
lexer=text like text: spacing, capitals
|
|
lexer=textlit text, unknowns as string lits
|
|
|
|
unlexer=code like program code
|
|
unlexer=codelit code, remove string lit quotes
|
|
unlexer=text like text: punctuation, capitals
|
|
unlexer=textlit text, remove string lit quotes
|
|
unlexer=concat remove all spaces
|
|
unlexer=bind remove spaces around "&+"
|
|
|
|
optimize=all_subs best for almost any concrete
|
|
optimize=values good for lexicon concrete
|
|
optimize=all usually good for resource
|
|
optimize=noexpand for resource, if =all too big
|
|
</PRE>
|
|
|
|
<P>
|
|
For the full set of values for <CODE>FLAG</CODE>,
|
|
use on-line <CODE>h -FLAG</CODE>.
|
|
</P>
|
|
|
|
<A NAME="toc9"></A>
|
|
<H3>File paths</H3>
|
|
|
|
<P>
|
|
Colon-separated lists of directories searched in the
|
|
given order:
|
|
</P>
|
|
|
|
<PRE>
|
|
--# -path=.:../abstract:../common:prelude
|
|
</PRE>
|
|
|
|
<P>
|
|
This can be (in order of growing preference), as
|
|
first line in the top file, as flag to <CODE>gf</CODE>
|
|
when invoked, or as flag to the <CODE>i</CODE> command.
|
|
The prefix <CODE>--#</CODE> is used only in files.
|
|
</P>
|
|
<P>
|
|
If the environment variabls <CODE>GF_LIB_PATH</CODE> is defined, its
|
|
value is automatically prefixed to each directory to
|
|
extend the original search path.
|
|
</P>
|
|
|
|
<A NAME="toc10"></A>
|
|
<H3>Alternative grammar formats</H3>
|
|
|
|
<P>
|
|
<B>Old GF</B> (before GF 2.0):
|
|
all judgements in any kinds of modules,
|
|
division into files uses <CODE>include</CODE>s.
|
|
A file <CODE>Foo.gf</CODE> is recognized as the old format
|
|
if it lacks a module header.
|
|
</P>
|
|
<P>
|
|
<B>Context-free</B> (file <CODE>foo.cf</CODE>). The form of rules is e.g.
|
|
</P>
|
|
|
|
<PRE>
|
|
Fun. S ::= NP "is" AP ;
|
|
</PRE>
|
|
|
|
<P>
|
|
If <CODE>Fun</CODE> is omitted, it is generated automatically.
|
|
Rules must be one per line. The RHS can be empty.
|
|
</P>
|
|
<P>
|
|
<B>Extended BNF</B> (file <CODE>foo.ebnf</CODE>). The form of rules is e.g.
|
|
</P>
|
|
|
|
<PRE>
|
|
S ::= (NP+ ("is" | "was") AP | V NP*) ;
|
|
</PRE>
|
|
|
|
<P>
|
|
where the RHS is a regular expression of categories
|
|
and quoted tokens: <CODE>"foo", CAT, T U, T|U, T*, T+, T?</CODE>, or empty.
|
|
Rule labels are generated automatically.
|
|
</P>
|
|
<P>
|
|
<B>Probabilistic grammars</B> (not a separate format).
|
|
You can set the probability of a function <CODE>f</CODE> (in its value category) by
|
|
</P>
|
|
|
|
<PRE>
|
|
--# prob f 0.009
|
|
</PRE>
|
|
|
|
<P>
|
|
These are put into a file given to GF using the <CODE>probs=File</CODE> flag
|
|
on command line. This file can be the grammar file itself.
|
|
</P>
|
|
<P>
|
|
<B>Example-based grammars</B> (file <CODE>foo.gfe</CODE>). Expressions of the form
|
|
</P>
|
|
|
|
<PRE>
|
|
in Cat "example string"
|
|
</PRE>
|
|
|
|
<P>
|
|
are preprocessed by using a parser given by the flag
|
|
</P>
|
|
|
|
<PRE>
|
|
--# -resource=File
|
|
</PRE>
|
|
|
|
<P>
|
|
and the result is written to <CODE>foo.gf</CODE>.
|
|
</P>
|
|
|
|
<A NAME="toc11"></A>
|
|
<H3>References</H3>
|
|
|
|
<P>
|
|
<A HREF="http://www.grammaticalframework.org/">GF Homepage</A>
|
|
</P>
|
|
<P>
|
|
A. Ranta, Grammatical Framework: A Type-Theoretical Grammar Formalism.
|
|
<I>The Journal of Functional Programming</I>, vol. 14:2. 2004, pp. 145-189.
|
|
</P>
|
|
|
|
<!-- html code generated by txt2tags 2.6 (http://txt2tags.org) -->
|
|
<!-- cmdline: txt2tags -thtml ./doc/gf-reference.t2t -->
|
|
</BODY></HTML>
|