gf-core/doc/gf-reference.t2t

GF Quick Reference
Aarne Ranta
April 4, 2006

% NOTE: this is a txt2tags file.
% Create an html file from this file using:
% txt2tags -thtml gf-reference.t2t

%!style:../css/style.css
%!target:html
%!options: --toc
%!postproc(html): <TITLE> <meta name = "viewport" content = "width = device-width"><TITLE>
%!postproc(html): <H1> <H1><a href="../"><IMG src="../doc/Logos/gf0.png"></a>

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 
[GF Tutorial http://www.grammaticalframework.org/doc/tutorial/gf-tutorial.html].
Help on GF commands is obtained on line by the
help command (``help``), and help on invoking
GF with (``gf -help``).


===A complete example===

This is a complete example of a GF grammar divided
into three modules in files. The grammar recognizes the
phrases //one pizza// and //two pizzas//.

File ``Order.gf``:
```
abstract Order = {
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 ;
    _  => dog + "s"
    }
  } ;
}
```
To use this example, do
```
  % gf             -- in shell: start GF
  > i OrderEng.gf  -- in GF: import grammar
  > p "one pizza"  --        parse string
  > l Two Pizza    --        linearize tree
```



===Modules and files===

One module per file.
File named ``Foo.gf`` contains module named
``Foo``.

Each module has the structure
```
moduletypename =   
  Inherits **        -- optional
  open Opens in      -- optional
  { Judgements }   
```
Inherits are names of modules of the same type.
Inheritance can be restricted:
```
  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), -- refer to f as M.f or Mo.f
  (Lo = Lo) -- refer to f as Lo.f
```
Module types and judgements in them:
```
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
``` 
The forms 
``param``, ``oper`` 
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 -}
--# used for compiler pragmas
```
A ``concrete`` can be opened like a ``resource``.
It is translated as follows:
```
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 = <>}          
```
An ``abstract`` can be opened like an ``interface``.
Any ``concrete`` of it then works as an ``instance``.



===Judgements===

```
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
```
Judgements are terminated by semicolons (``;``).
Subsequent judgments of the same form may share the
keyword:
```
cat C ; D ;         -- same as cat C ; cat D ;
```
Judgements can also share RHS:
```
fun f,g : A         -- same as fun f : A ; g : A
```


===Types===

Abstract syntax (in ``fun``):
```
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
```
Concrete syntax (in ``lincat``):
```
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
```
Resource (in ``oper``): all those of concrete, plus
``` 
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
```
As parameter types, one can use any finite type:
``P`` defined in ``param P``,
``Ints n``, and record types of parameter types.



===Expressions===

Syntax trees = full function applications
```
f a b              -- : C if fun f : A -> B -> C
1977               -- : Int
3.14               -- : Float
"foo"              -- : String
```
Higher-Order Abstract syntax (HOAS): functions as arguments:
```
F a (\x -> c)      -- : C if a : A, c : C (x : B), 
                      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"  -- : Tok, computes to "helloworld"
[]                 -- : Str, empty list
```
Parameters
```
Sg                   -- atomic constructor
VPres Sg P2          -- applied constructor
{n = Sg ; p = P3}    -- record of parameters
```
Tables
```
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 
```
Records
```
{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}
```
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=e in t
let {...} in t     -- same as let ... in t

t where {...}      -- same as let ... in t
```
Free variation
```
variants {x ; y}     -- both x and y possible
variants {}          -- nothing possible
```
Prefix-dependent choices
```
pre {"a" ; "an" / v} -- "an" before v, "a" otherw.
strs {"a" ; "i" ;"o"}-- list of condition prefixes
```
Typed expression
```
<t:T>                -- same as t, to help type inference
```
Accessing bound variables in ``lin``: use fields ``$1, $2, $3,...``. 
Example:
```
fun F : (A : Set) -> (El A -> Prop) -> Prop ; 
lin F A B = {s = ["for all"] ++ A.s ++ B.$1 ++ B.s}
```


===Pattern matching===

These patterns can be used in branches of ``table`` and
``case`` expressions. Patterns are matched in the order in
which they appear in the grammar.
```
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
```

===Sample library functions===

```
-- 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
```


===Flags===

Flags can appear, with growing priority,
- in files, judgement ``flags`` and without dash (``-``)
- as flags to ``gf`` when invoked, with dash
- as flags to various GF commands, with dash


Some common flags used in grammars:
```
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
```
For the full set of values for ``FLAG``, 
use on-line ``h -FLAG``.



===File paths===

Colon-separated lists of directories searched in the
given order: 
```
--# -path=.:../abstract:../common:prelude
```
This can be (in order of growing preference), as
first line in the top file, as flag to ``gf``
when invoked, or as flag to the ``i`` command.
The prefix ``--#`` is used only in files.

If the environment variabls ``GF_LIB_PATH`` is defined, its
value is automatically prefixed to each directory to
extend the original search path.


===Alternative grammar formats===

**Old GF** (before GF 2.0): 
all judgements in any kinds of modules,
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 e.g.
```
Fun. S ::= NP "is" AP ;
```
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 e.g.
```
S ::= (NP+ ("is" | "was") AP | V NP*) ;
```
where the RHS is a regular expression of categories
and quoted tokens: ``"foo", CAT, T U, T|U, T*, T+, T?``, or empty.
Rule labels are generated automatically.


**Probabilistic grammars** (not a separate format).
You can set the probability of a function ``f`` (in its value category) by
```
--# prob f 0.009
```
These are put into a file given to GF using the ``probs=File`` flag
on command line. This file can be the grammar file itself.

**Example-based grammars**  (file ``foo.gfe``). Expressions of the form
```
in Cat "example string"
```
are preprocessed by using a parser given by the flag 
```
--# -resource=File
```
and the result is written to ``foo.gf``.


===References===

[GF Homepage http://www.grammaticalframework.org/]

A. Ranta, Grammatical Framework: A Type-Theoretical Grammar Formalism.
//The Journal of Functional Programming//, vol. 14:2. 2004, pp. 145-189.