diff options
| -rw-r--r-- | doc/gf-reference.html | 574 | ||||
| -rw-r--r-- | doc/gf-reference.pdf | bin | 0 -> 50694 bytes | |||
| -rw-r--r-- | doc/gf-reference.txt | 215 |
3 files changed, 686 insertions, 103 deletions
diff --git a/doc/gf-reference.html b/doc/gf-reference.html new file mode 100644 index 000000000..f019a383d --- /dev/null +++ b/doc/gf-reference.html @@ -0,0 +1,574 @@ +<!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> +Wed Mar 29 13:21:48 2006 +</FONT></CENTER> + +<P></P> +<HR NOSHADE SIZE=1> +<P></P> + <UL> + <LI><A HREF="#toc1">A Quick 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. +Help on GF commands is obtained on line by the +help command (<CODE>h</CODE>). +</P> +<A NAME="toc1"></A> +<H2>A Quick Example</H2> +<P> +This is a complete example, dividing a grammar +into three files. +</P> +<P> +<CODE>abstract</CODE>, <CODE>concrete</CODE>, and <CODE>resource</CODE>. +</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 ; + Pl => 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> +<H2>Modules and files</H2> +<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 -} + --# reserved 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> +<H2>Judgements</H2> +<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> +<H2>Types</H2> +<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 (subset 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>param</CODE> constants <CODE>P</CODE>, +<CODE>Ints n</CODE>, and record types of parameter types. +</P> +<A NAME="toc5"></A> +<H2>Expressions</H2> +<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 (\y -> b) -- : C if a : A, b : B (x : A), + 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> +<H2>Pattern matching</H2> +<P> +These patterns can be used in branches of <CODE>table</CODE> and +<CODE>case</CODE> expressions. +</P> +<PRE> + C -- atomic param constructor + C p q -- param constr. appl- 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> +<H2>Sample library functions</H2> +<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> +<H2>Flags</H2> +<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> +<H2>File paths</H2> +<P> +Colon-separated lists of directories tried 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 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> +<H2>Alternative grammar formats</H2> +<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", 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> +<H2>References</H2> +<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> diff --git a/doc/gf-reference.pdf b/doc/gf-reference.pdf Binary files differnew file mode 100644 index 000000000..4a43a8635 --- /dev/null +++ b/doc/gf-reference.pdf diff --git a/doc/gf-reference.txt b/doc/gf-reference.txt index edfe0fd49..16e7b2378 100644 --- a/doc/gf-reference.txt +++ b/doc/gf-reference.txt @@ -16,41 +16,48 @@ help command (``h``). ==A Quick Example== -This is a complete example using +This is a complete example, dividing a grammar +into three files. + ``abstract``, ``concrete``, and ``resource``. + +File ``Order.gf`` ``` --- in file Order.gf abstract Order = { - cat - Order ; - Item ; - fun - One, Two : Item -> Order ; - Pizza : Item ; - } - --- in file OrderEng.gf -concrete OrderEng of Order = open Res in { - flags startcat=Order ; - cat - Order = {s : Str} ; - Item = {s : Num => Str} ; - fun - One it = {s = "one" ++ it.s ! Sg} ; - Two it = {s = "two" ++ it.s ! Pl} ; - Pizza = regNoun "pizza" ; - } - --- in file Res.gf -resource Res = { - param Num = Sg | Pl ; - oper regNoun : Str -> {s : Num => Str} = - \dog -> {s = table { - Sg => dog ; - Pl => dog + "s" - } - } ; - } ; +cat + Order ; + Item ; +fun + One, Two : Item -> Order ; + Pizza : Item ; +} +``` +File ``OrderEng.gf`` (the top file): +``` +--# -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" ; +} +``` +File ``Res.gf``: +``` +resource Res = open Prelude in { +param Num = Sg | Pl ; +oper regNoun : Str -> {s : Num => Str} = + \dog -> {s = table { + Sg => dog ; + Pl => dog + "s" + } + } ; +} ``` To use this example, do ``` @@ -64,29 +71,29 @@ To use this example, do ==Modules and files== -In standard GF, there is one module per file. +One module per file. File named ``Foo.gf`` contains module named ``Foo``. Each module has the structure ``` moduletypename = - Extends ** -- optional - open Opens in -- optional + Inherits ** -- optional + open Opens in -- optional { Judgements } ``` -Extends are names of modules of the same type. -They can be restricted: +Inherits are names of modules of the same type. +Inheritance can be restricted: ``` - Mo[f,g], -- inherit only f,g - Lo-[f,g] -- inheris all but f,g + 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), -- references M.f or Mo.f - (Lo = Lo) -- references Lo.f + (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: ``` @@ -95,23 +102,28 @@ concrete C of A -- lincat, lin, lindef, printname resource R -- param, oper interface I -- like resource, but can have - -- oper f : T without definition + oper f : T without definition instance J of I -- like resource, defines opers - -- that I leaves undefined + that I leaves undefined incomplete -- functor: concrete that opens - concrete CI of A = -- one or more interfaces + concrete CI of A = one or more interfaces open I in ... concrete CJ of A = -- completion: concrete that - CI with -- instantiates a functor by giving - (I = J) -- instances of its open interfaces + CI with instantiates a functor by + (I = J) instances of open interfaces ``` The forms ``param``, ``oper`` -may appear in ``concrete`` as well, but are not inherited to -extensions. - -All modules can moreover have ``flag``s. +may appear in ``concrete`` as well, but are then +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 -} +--# reserved for compiler pragmas +``` A ``concrete`` can be opened like a ``resource``. It is translated as follows: ``` @@ -130,13 +142,14 @@ Any ``concrete`` of it then works as an ``instance``. ``` cat C -- declare category C -cat C (x : A) -- dependent category C -cat C A -- same as C (x : A) +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 -- set f as constructor of C -data f : A -> C -- same as fun f : A; data C=f +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 @@ -146,15 +159,16 @@ 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 ptype P with constrs - -- C : P, D : Q -> R -> P +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 -flag p=v -- define value of flag p +flags p=v -- set value of flag p ``` Judgements are terminated by semicolons (``;``). -Subsequent judgments of the same form may share their +Subsequent judgments of the same form may share the keyword: ``` cat C ; D ; -- same as cat C ; cat D ; @@ -187,9 +201,9 @@ 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 : A ; b : B} A * B * C -- tuple type, same as - -- {p1 : A ; p2 : B ; p3 : C} + {p1 : A ; p2 : B ; p3 : C} Ints n -- type of n first integers ``` Resource (in ``oper``): all those of concrete, plus @@ -197,7 +211,7 @@ Resource (in ``oper``): all those of concrete, plus Tok -- tokens (subset of Str) A -> B -- functions from A to B Int -- integers -Strs -- list of prefixes +Strs -- list of prefixes (for pre) PType -- parameter type Type -- any type ``` @@ -219,14 +233,14 @@ f a b -- : C if fun f : A -> B -> C Higher-Order Abstract syntax (HOAS): functions as arguments: ``` F a (\y -> b) -- : C if a : A, b : B (x : A), - -- fun F : A -> (B -> C) -> C + fun F : A -> (B -> C) -> C ``` Tokens and token lists ``` "hello" -- : Tok, singleton Str "hello" ++ "world" -- : Str ["hello world"] -- : Str, same as "hello" ++ "world" -"hello" + "world" -- : Str, computes to "helloworld" +"hello" + "world" -- : Tok, computes to "helloworld" [] -- : Str, empty list ``` Parameters @@ -248,24 +262,21 @@ table { -- by pattern matching table { n => regn n "cat" ;-- variable pattern } - -\\_ => "fish" -- same as table {n => "fish"} +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 -table Num [ -- table given with arg. type - "mouse" ; "mice" -- and course of values - ] - t ! p -- select p from table t case e of {...} -- same as table {...} ! e ``` Records ``` -{s = "Liz" ; g = Fem}-- record in full form +{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} + {g = Fem} {s = "Liz" ; g = Fem} <a,b,c> -- tuple, same as {p1=a;p2=b;p3=c} ``` @@ -273,13 +284,14 @@ 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 let x=d ; y=e in t -- same as - -- let x=d in let y=t in d + let x=d in let y=e in t let {...} in t -- same as let ... in t t where {...} -- same as let ... in t @@ -298,10 +310,11 @@ Typed expression ``` <t:T> -- same as t, to help type inference ``` -Accessing bound variables in HOAS: use fields ``$1, $2, $3,...``. +Accessing bound variables in ``lin``: use fields ``$1, $2, $3,...``. Example: ``` -lin F a b = {s = ["for all"] ++ a.s ++ b.$1 ++ b.s} +fun F : (A : Set) -> (El A -> Prop) -> Prop ; +lin F A B = {s = ["for all"] ++ A.s ++ B.$1 ++ B.s} ``` @@ -329,15 +342,15 @@ p* -- repetition of a string pattern ``` -- 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 +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 @@ -347,7 +360,7 @@ oper cc2 : (_,_ : SS) -> SS -- concat SS's optStr : Str -> Str -- string or empty strOpt : Str -> Str -- empty or string - bothWays : Str -> Str -> Str -- XY or YX + 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 @@ -361,8 +374,7 @@ oper ==Flags== Flags can appear, with growing priority, -- in files, with judgement keyword ``flags`` - and without dash (``-``) +- in files, judgement ``flags`` and without dash (``-``) - as flags to ``gf`` when invoked, with dash - as flags to various GF commands, with dash @@ -383,18 +395,19 @@ unlexer=textlit text, remove string lit quotes unlexer=concat remove all spaces unlexer=bind remove spaces around "&+" -optimize=values good for lexicon concrete 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 ``` -For the full set of flags, use on-line ``h -flag``. +For the full set of values for ``flag``, +use on-line ``h -flag``. ==File paths== -Colon-separated lists of search directories tried in the +Colon-separated lists of directories tried in the given order: ``` --# -path=.:../abstract:../common:prelude @@ -417,23 +430,19 @@ division into files uses ``include``s. A file ``Foo.gf`` is recognized as the old format if it lacks a module header. -**Context-free** (file ``foo.cf``). The form of rules is +**Context-free** (file ``foo.cf``). The form of rules is e.g. ``` - Fun. Cat ::= Cat "tok" Cat ; +Fun. S ::= NP "is" AP ; ``` -where ``Fun`` is optional. Rules must be one per line. -The RHS can be empty. +If ``Fun`` is omitted, it is generated automatically. +Rules must be one per line. The RHS can be empty. -**Extended BNF** (file ``foo.ebnf``). The form of rules is -``` - Cat ::= Reg ; +**Extended BNF** (file ``foo.ebnf``). The form of rules is e.g. ``` -where ``Reg`` is a regular expression of categories -and quoted tokens: +S ::= (NP+ ("is" | "was") AP | V NP*) ; ``` - T U, T|U, T*, T+, T? -``` -The RHS can also be empty. +where the RHS is a regular expression of categories +and quoted tokens: ``"foo", T U, T|U, T*, T+, T?``, or empty. Rule labels are generated automatically. @@ -447,11 +456,11 @@ on command line. This file can be the grammar file itself. **Example-based grammars** (file ``foo.gfe``). Expressions of the form ``` -in Mo.Cat "example string" +in Cat "example string" ``` are preprocessed by using a parser given by the flag ``` ---# resource=File +--# -resource=File ``` and the result is written to ``foo.gf``. |