diff options
Diffstat (limited to 'doc/gf-reference.html')
| -rw-r--r-- | doc/gf-reference.html | 112 |
1 files changed, 99 insertions, 13 deletions
diff --git a/doc/gf-reference.html b/doc/gf-reference.html index b05d25072..330e30c7f 100644 --- a/doc/gf-reference.html +++ b/doc/gf-reference.html @@ -1,19 +1,20 @@ <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"> <HTML> <HEAD> -<META NAME="generator" CONTENT="http://txt2tags.sf.net"> +<META NAME="generator" CONTENT="http://txt2tags.org"> <LINK REL="stylesheet" TYPE="text/css" HREF="../css/style.css"> -<TITLE>GF Quick Reference</TITLE> +<meta name = "viewport" content = "width = device-width"><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> -April 4, 2006 -</FONT></CENTER> +<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> @@ -41,8 +42,10 @@ 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 @@ -51,6 +54,7 @@ phrases <I>one pizza</I> and <I>two pizzas</I>. <P> File <CODE>Order.gf</CODE>: </P> + <PRE> abstract Order = { cat @@ -61,9 +65,11 @@ File <CODE>Order.gf</CODE>: Pizza : Item ; } </PRE> + <P> File <CODE>OrderEng.gf</CODE> (the top file): </P> + <PRE> --# -path=.:prelude concrete OrderEng of Order = @@ -78,9 +84,11 @@ File <CODE>OrderEng.gf</CODE> (the top file): Pizza = regNoun "pizza" ; } </PRE> + <P> File <CODE>Res.gf</CODE>: </P> + <PRE> resource Res = open Prelude in { param Num = Sg | Pl ; @@ -92,18 +100,21 @@ File <CODE>Res.gf</CODE>: } ; } </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 @@ -112,32 +123,39 @@ File named <CODE>Foo.gf</CODE> contains module named <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 @@ -154,6 +172,7 @@ Module types and judgements in them: CI with instantiates a functor by (I = J) instances of open interfaces </PRE> + <P> The forms <CODE>param</CODE>, <CODE>oper</CODE> @@ -164,15 +183,18 @@ not inherited to extensions. 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 : {}} @@ -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 = <>} </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 @@ -213,26 +238,32 @@ Any <CODE>concrete</CODE> of it then works as an <CODE>instance</CODE>. 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 @@ -244,9 +275,11 @@ Abstract syntax (in <CODE>fun</CODE>): 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 @@ -259,9 +292,11 @@ Concrete syntax (in <CODE>lincat</CODE>): {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 @@ -270,32 +305,40 @@ Resource (in <CODE>oper</CODE>): all those of concrete, plus 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 @@ -303,17 +346,21 @@ Tokens and token lists "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" ; @@ -334,9 +381,11 @@ Tables 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"} @@ -345,17 +394,21 @@ Records <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 @@ -365,42 +418,52 @@ Local definitions 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 @@ -416,9 +479,10 @@ which they appear in the grammar. 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 @@ -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 </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 @@ -463,6 +529,7 @@ Flags can appear, with growing priority, <P> Some common flags used in grammars: </P> + <PRE> 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 </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> @@ -507,8 +579,10 @@ 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, @@ -519,9 +593,11 @@ if it lacks a module header. <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. @@ -529,9 +605,11 @@ Rules must be one per line. The RHS can be empty. <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. @@ -541,9 +619,11 @@ Rule labels are generated automatically. <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. @@ -551,20 +631,26 @@ on command line. This file can be the grammar file itself. <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> @@ -573,6 +659,6 @@ 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.5 (http://txt2tags.sf.net) --> +<!-- html code generated by txt2tags 2.6 (http://txt2tags.org) --> <!-- cmdline: txt2tags -thtml ./doc/gf-reference.t2t --> </BODY></HTML> |