diff options
Diffstat (limited to 'doc/gf-reference.html')
| -rw-r--r-- | doc/gf-reference.html | 664 |
1 files changed, 0 insertions, 664 deletions
diff --git a/doc/gf-reference.html b/doc/gf-reference.html deleted file mode 100644 index 330e30c7f..000000000 --- a/doc/gf-reference.html +++ /dev/null @@ -1,664 +0,0 @@ -<!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> |