mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
578 lines
16 KiB
HTML
578 lines
16 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
|
|
<HTML>
|
|
<HEAD>
|
|
<META NAME="generator" CONTENT="http://txt2tags.sf.net">
|
|
<TITLE>GF Quick Reference</TITLE>
|
|
</HEAD><BODY BGCOLOR="white" TEXT="black">
|
|
<P ALIGN="center"><CENTER><H1>GF Quick Reference</H1>
|
|
<FONT SIZE="4">
|
|
<I>Aarne Ranta</I><BR>
|
|
Tue Apr 4 09:41:30 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.cs.chalmers.se/~aarne/GF/doc/tutorial/">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>
|
|
<P></P>
|
|
<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>
|
|
<P></P>
|
|
<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>
|
|
<P></P>
|
|
<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>
|
|
<P></P>
|
|
<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>
|
|
<P></P>
|
|
<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.cs.chalmers.se/~aarne/GF/">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.0 (http://txt2tags.sf.net) -->
|
|
<!-- cmdline: txt2tags -thtml -\-toc gf-reference.txt -->
|
|
</BODY></HTML>
|