diff --git a/doc/darcs.html b/doc/darcs.html
index b45dd38f3..7c74741e6 100644
--- a/doc/darcs.html
+++ b/doc/darcs.html
@@ -7,7 +7,7 @@
GF Darcs repository
Author: Björn Bringert <bringert@cs.chalmers.se>
-Last update: Tue Dec 6 13:23:38 2005
+Last update: Tue Dec 6 14:29:33 2005
@@ -492,5 +492,5 @@ For more info about what you can do with darcs, see
+
+
+
+Transfer language reference
+
+Transfer language reference
+
+Author: Björn Bringert <bringert@cs.chalmers.se>
+Last update: Tue Dec 6 14:26:07 2005
+
+
+
+
+
+
+
+
+
+
+
+This document describes the features of the Transfer language.
+See the Transfer tutorial
+for an example of a Transfer program, and how to compile and use
+Transfer programs.
+
+
+Transfer is a dependently typed functional programming language
+with eager evaluation.
+
+
+Layout syntax
+
+Transfer uses layout syntax, where the indentation of a piece of code
+determines which syntactic block it belongs to.
+
+
+To give the block structure of a piece of code without using layout
+syntax, you can enclose the block in curly braces ({ }) and
+separate the parts of the blocks with semicolons (;).
+
+
+For example, this case expression:
+
+
+ case x of
+ p1 -> e1
+ p2 -> e2
+
+
+
+is equivalent to this one:
+
+
+ case x of {
+ p1 -> e1 ;
+ p2 -> e2
+ }
+
+
+
+Here the layout is insignificant, as the structure is given with
+braces and semicolons. Thus the above is equivalent to:
+
+
+ case x of { p1 -> e1 ; p2 -> e2 }
+
+
+
+Imports
+
+A Transfer module start with some imports. Most modules will have to
+import the prelude, which contains definitons used by most programs:
+
+
+ import prelude
+
+
+
+Function declarations
+
+Functions need to be given a type and a definition. The type is given
+by a typing judgement on the form:
+
+
+ f : T
+
+
+
+where f is the function's name, and T its type. See
+Function types for a how the types of functions
+are written.
+
+
+The definition of the function is the given as a sequence of pattern
+equations. The first equation whose patterns match the function arguments
+is used when the function is called. Pattern equations are on the form:
+
+
+ f p1 ... p1n = exp
+ ...
+ f qn1 ... qnm = exp
+
+
+
+Data type declarations
+
+Transfer supports Generalized Algebraic Datatypes.
+They are declared thusly:
+
+
+ data D : T where
+ c1 : Tc1
+ ...
+ cn : Tcn
+
+
+
+Here D is the name of the data type, T is the type of the type
+constructor, c1 to cn are the data constructor names, and
+Tc1 to Tcn are their types.
+
+
+Lambda expressions
+
+Lambda expressions are terms which express functions, without
+giving names to them. For example:
+
+
+ \x -> x + 1
+
+
+
+is the function which takes an argument, and returns the value of the
+argument + 1.
+
+
+Local definitions
+
+To give local definition to some names, use:
+
+
+ let x1 : T1 = exp1
+ ...
+ xn : Tn = expn
+ in exp
+
+
+
+Types
+
+Function types
+
+Functions types are of the form:
+
+
+ A -> B
+
+
+
+This is the type of functions which take an argument of type
+A and returns a result of type B.
+
+
+To write functions which take more than one argument, we use currying.
+A function which takes n arguments is a function which takes 1
+argument and returns a function which takes n-1 arguments. Thus,
+
+
+ A -> (B -> C)
+
+
+
+or, equivalently, since -> associates to the right:
+
+
+ A -> B -> C
+
+
+
+is the type of functions which take 2 arguments, the first of type
+A and the second of type B. This arrangement lets us do
+partial application of function to fewer arguments than the function
+is declared to take, returning a new function which takes the rest
+of the arguments.
+
+Dependent function types
+
+In a function type, the value of an argument can be used later
+in the type. Such dependent function types are written:
+
+
+ (x1 : T1) -> ... -> (xn : Tn) -> T
+
+
+
+Here, x1 can be used in T2 to Tn, x1 can be used
+in T2 to Tn
+
+
+Basic types
+Integers
+
+The type of integers is called Integer.
+standard decmial integer literals are used to represent values of this type.
+
+Floating-point numbers
+
+The only currently supported floating-point type is Double, which supports
+IEEE-754 double-precision floating-point numbers. Double literals are written
+in decimal notation, e.g. 123.456.
+
+Strings
+
+There is a primitive String type. This might be replaced by a list of
+characters representation in the future. String literals are written
+with double quotes, e.g. "this is a string".
+
+Booleans
+
+Booleans are not a built-in type, though some features of the Transfer language
+depend on them.
+
+
+ data Bool : Type where
+ True : Bool
+ False : Bool
+
+
+
+In addition to normal pattern matching on booleans, you can use the built-in
+if-expression:
+
+
+ if exp1 then exp2 else exp3
+
+
+
+where exp1 must be an expression of type Bool.
+
+
+Records
+
+Record types are created by using a sig expression:
+
+
+ sig { p1 : T1; ... ; pn : Tn }
+
+
+
+Here, p1 to pn are the field labels and T1 to Tn are their types.
+
+
+Record values are constructed using rec expressions:
+
+
+ rec { p1 = exp1; ... ; pn = expn }
+
+
+
+The curly braces and semicolons are simply explicit layout syntax, so
+the record type and record expression above can also be written as:
+
+
+ sig p1 : T1
+ pn : Tn
+
+
+
+ rec p1 = exp1
+ pn = expn
+
+
+Record subtyping
+
+A record of some type R1 can be used as a record of any type R2
+such that for every field p1 : T1 in R2, p1 : T1 is also a
+field of T1.
+
+
+Tuples
+
+Tuples on the form:
+
+
+ (exp1, ..., expn)
+
+
+
+are syntactic sugar for records with fields p1 to pn. The expression
+above is equivalent to:
+
+
+ rec { p1 = exp1; ... ; pn = expn }
+
+
+
+Lists
+
+The List type is not built-in, though there is some special syntax for it.
+The list type is declared as:
+
+
+ data List : Type -> Type where
+ Nil : (A:Type) -> List A
+ Cons : (A:Type) -> A -> List A -> List A
+
+
+
+The empty lists can be written as []. There is a operator :: which can
+be used instead of Cons. These are just syntactic sugar for expressions
+using Nil and Cons, with the type arguments hidden.
+
+
+Pattern matching
+
+Pattern matching is done in pattern equations and by using the
+case construct:
+
+
+ case exp of
+ p1 | guard1 -> rhs1
+ ...
+ pn | guardn -> rhsn
+
+
+
+guard1 to guardn are boolean expressions. Case arms can also be written
+without guards, such as:
+
+
+ pk -> rhsk
+
+
+
+This is the same as writing:
+
+
+ pk | True -> rhsk
+
+
+
+The syntax of patterns are decribed below.
+
+
+Constructor patterns
+
+Constructor patterns are written as:
+
+
+ C p1 ... pn
+
+
+
+where C is a data constructor which takes n arguments.
+If the value to be matched is the constructor C applied to
+arguments v1 to vn, then v1 to vn will be matched
+against p1 to pn.
+
+
+Variable patterns
+
+A variable pattern is a single identifier:
+
+
+ x
+
+
+
+A variable pattern matches any value, and binds the variable name to the
+value. A variable may not occur more than once in a pattern.
+
+
+Wildcard patterns
+
+Wildcard patterns are written as with a single underscore:
+
+
+ _
+
+
+
+Wildcard patterns match all values and bind no variables.
+
+
+Record patterns
+
+Record patterns match record values:
+
+
+ rec { l1 = p1; ... ; ln = pn }
+
+
+
+A record value matches a record pattern, if the record value has all the
+fields l1 to ln, and their values match p1 to pn.
+
+
+Note that a record value may have more fields than the record pattern and
+they will still match.
+
+
+Disjunctive patterns
+
+It is possible to write a pattern on the form:
+
+
+ p1 || ... || pn
+
+
+
+A value will match this pattern if it matches any of the patterns p1 to pn.
+FIXME: talk about how this is expanded
+
+
+List patterns
+
+Tuple patterns
+
+Tuples patterns on the form:
+
+
+ (p1, ... , pn)
+
+
+
+are syntactic sugar for record patterns, in the same way as tuple expressions.
+
+
+String literal patterns
+
+String literals can be used as patterns.
+
+
+Integer literal patterns
+
+Integer literals can be used as patterns.
+
+
+Meta variables
+
+Type classes
+
+Operators
+
+Compositional functions
+
+do notation
+
+
+
+
diff --git a/transfer/examples/aggregation/transfer.txt b/doc/transfer-reference.txt
similarity index 71%
rename from transfer/examples/aggregation/transfer.txt
rename to doc/transfer-reference.txt
index fa1603005..dd16e2d39 100644
--- a/transfer/examples/aggregation/transfer.txt
+++ b/doc/transfer-reference.txt
@@ -1,4 +1,6 @@
Transfer language reference
+Author: Björn Bringert
+Last update: %%date(%c)
% NOTE: this is a txt2tags file.
@@ -14,7 +16,9 @@ Transfer language reference
This document describes the features of the Transfer language.
-See the Transfer tutorial for how to compile and use Transfer programs.
+See the [Transfer tutorial transfer-tutorial.html]
+for an example of a Transfer program, and how to compile and use
+Transfer programs.
Transfer is a dependently typed functional programming language
with eager evaluation.
@@ -28,10 +32,31 @@ To give the block structure of a piece of code without using layout
syntax, you can enclose the block in curly braces (``{ }``) and
separate the parts of the blocks with semicolons (``;``).
+For example, this case expression:
-== Top-level stuff ==
+```
+case x of
+ p1 -> e1
+ p2 -> e2
+```
-=== Imports ===
+is equivalent to this one:
+
+```
+case x of {
+ p1 -> e1 ;
+ p2 -> e2
+}
+```
+
+Here the layout is insignificant, as the structure is given with
+braces and semicolons. Thus the above is equivalent to:
+
+```
+case x of { p1 -> e1 ; p2 -> e2 }
+```
+
+== Imports ==
A Transfer module start with some imports. Most modules will have to
import the prelude, which contains definitons used by most programs:
@@ -41,7 +66,7 @@ import prelude
```
-=== Declaring functions ===
+== Function declarations ==
Functions need to be given a type and a definition. The type is given
by a typing judgement on the form:
@@ -50,7 +75,9 @@ by a typing judgement on the form:
f : T
```
-where ``f`` is the function's name, and ``T`` its type.
+where ``f`` is the function's name, and ``T`` its type. See
+[Function types #function_types] for a how the types of functions
+are written.
The definition of the function is the given as a sequence of pattern
equations. The first equation whose patterns match the function arguments
@@ -63,7 +90,7 @@ f qn1 ... qnm = exp
```
-=== Declaring new data types ===
+== Data type declarations ==
Transfer supports Generalized Algebraic Datatypes.
They are declared thusly:
@@ -80,6 +107,19 @@ constructor, ``c1`` to ``cn`` are the data constructor names, and
``Tc1`` to ``Tcn`` are their types.
+== Lambda expressions ==
+
+//Lambda expressions// are terms which express functions, without
+giving names to them. For example:
+
+```
+\x -> x + 1
+```
+
+is the function which takes an argument, and returns the value of the
+argument + 1.
+
+
== Local definitions ==
To give local definition to some names, use:
@@ -95,6 +135,50 @@ let x1 : T1 = exp1
== Types ==
+=== Function types ===[function_types]
+
+Functions types are of the form:
+
+```
+A -> B
+```
+
+This is the type of functions which take an argument of type
+``A`` and returns a result of type ``B``.
+
+To write functions which take more than one argument, we use //currying//.
+A function which takes n arguments is a function which takes 1
+argument and returns a function which takes n-1 arguments. Thus,
+
+```
+A -> (B -> C)
+```
+
+or, equivalently, since ``->`` associates to the right:
+
+```
+A -> B -> C
+```
+
+is the type of functions which take 2 arguments, the first of type
+``A`` and the second of type ``B``. This arrangement lets us do
+//partial application// of function to fewer arguments than the function
+is declared to take, returning a new function which takes the rest
+of the arguments.
+
+
+==== Dependent function types ====
+
+In a function type, the value of an argument can be used later
+in the type. Such dependent function types are written:
+
+```
+(x1 : T1) -> ... -> (xn : Tn) -> T
+```
+
+Here, ``x1`` can be used in ``T2`` to ``Tn``, ``x1`` can be used
+in ``T2`` to ``Tn``
+
=== Basic types ===
==== Integers ====
@@ -106,13 +190,13 @@ standard decmial integer literals are used to represent values of this type.
The only currently supported floating-point type is ``Double``, which supports
IEEE-754 double-precision floating-point numbers. Double literals are written
-in decimal notation, e.g. "123.456".
+in decimal notation, e.g. ``123.456``.
==== Strings ====
There is a primitive ``String`` type. This might be replaced by a list of
-characters representation in the future. String literals are written with double
-quotes, e.g. ``"this is a string"``.
+characters representation in the future. String literals are written
+with double quotes, e.g. ``"this is a string"``.
==== Booleans ====
@@ -168,8 +252,9 @@ rec p1 = exp1
==== Record subtyping ====
-
-
+A record of some type R1 can be used as a record of any type R2
+such that for every field ``p1 : T1`` in R2, ``p1 : T1`` is also a
+field of T1.
=== Tuples ===
@@ -324,3 +409,5 @@ Integer literals can be used as patterns.
== Compositional functions ==
+== do notation ==
+
diff --git a/doc/transfer-tutorial.html b/doc/transfer-tutorial.html
new file mode 100644
index 000000000..7ca1c2060
--- /dev/null
+++ b/doc/transfer-tutorial.html
@@ -0,0 +1,210 @@
+
+
+
+
+Transfer tutorial
+
+Transfer tutorial
+
+Author: Björn Bringert <bringert@cs.chalmers.se>
+Last update: Tue Dec 6 14:26:07 2005
+
+
+
+
+
+
+
+
+
+
+
+Objective
+
+We want to write a Transfer program which we can use to do aggregation
+in sentences which use conjugations on the sentence, noun phrase and
+verb phrase levels. For example, we want to be able to transform
+the sentence "John walks and Mary walks" to the sentence
+"John and Mary walk". We would also like to transform
+"John walks and John swims" to "John walks and swims".
+
+
+Thus that what we want to do is:
+
+
+- Transform sentence conjugation where the verb phrases in the sentences
+ are identical to noun phrase conjugation.
+
- Transform sentence conjugation where the noun phrases in the sentences
+ are identical to verb phrase conjugation.
+
+
+
+This needs to be done recursively and thoughout the sentence, to be
+able to handle cases like "John walks and Mary walks and Bill walks", and
+"John runs and Mary walks and Bill walks".
+
+
+FIXME: what about John walks and Mary runs and Bill walks"?
+
+
+Abstract syntax
+
+We will use the abstract syntax defined in
+Abstract.gf.
+
+
+Concrete syntax
+
+There is an English concrete syntax for this grammar in
+English.gf.
+
+
+Generate tree module
+
+To be able to write Transfer programs which sue the types defined in
+an abstract syntax, we first need to generate a Transfer file with
+a data type defintition corresponding to the abstract syntax.
+This is done with the transfer grammar printer:
+
+
+ $ gf
+ > i English.gf
+ > pg -printer=transfer | wf tree.tr
+
+
+
+Note that you need to load a concrete syntax which uses the abstract
+syntax that you want to create a Transfer data type for. Loading just the
+abstract syntax module is not enough. FIXME: why?
+
+
+The command sequence above writes a Transfer data type definition to the
+file tree.tr.
+
+
+Write transfer code
+
+We write the Transfer program
+aggregate.tr.
+
+
+FIXME: explain the code
+
+
+Compiling Transfer programs
+
+Transfer programs are written in the human-friendly Transfer language,
+but GF only understands the simpler Transfer Core language. Therefore,
+before using a Transfer program, you must first compile it to
+Transfer Core. This is done using the transferc command:
+
+
+ $ transferc -i<lib> <transfer program>
+
+
+
+Here, <lib> is the path to search for any modules which you import
+in your Transfer program. You can give several -i flags.
+
+
+So, to compile aggregate.tr which we created above, we use:
+
+
+ $ transferc aggregate.tr
+
+
+
+The creates the Transfer Core file aggregate.trc.
+
+
+Using Transfer programs in GF
+
+Loading the grammars
+
+To use a Transfer Core program to transform abstract syntax terms
+in GF, you must first load the grammars which you want to use the
+program with. For the example above, we need the grammar English.gf
+and its dependencies. We load this grammar with:
+
+
+ > i English.gf
+
+
+
+Loading the Transfer program
+
+There are two steps to using a Transfer Core program in GF. First you load
+the program into GF. This is done with the i command, which is also
+used when loading grammar modules. To load the aggregate.trc which
+we created above, we use:
+
+
+ > i aggregate.trc
+
+
+
+Calling Transfer functions
+
+To call a Transfer function on a term, we use the at command.
+The at command takes the name of a Transfer function and an abstract
+syntax term, and applies the function to the term:
+
+
+ > at aggregS ConjS And (Pred John Walk) (Pred Mary Walk)
+
+ Pred (ConjNP And John Mary) Walk
+
+
+
+Of course, the input and output terms of the at command can
+be read from and written to pipes:
+
+
+ > p "John walks and Mary walks" | at aggregS | l
+
+ John and Mary walk
+
+
+
+To see what is going on between the steps, we can use -tr flags
+to the commands:
+
+
+ > p -tr "John walks and Mary walks" | at -tr aggregS | l
+
+ ConjS And (Pred John Walk) (Pred Mary Walk)
+
+ Pred (ConjNP And John Mary) Walk
+
+ John and Mary walk
+
+
+
+Transfer between different abstract syntaxes
+
+If the transfer function which you wan to call takes as input a term in one
+abstract syntax, and returns a term in a different abstract syntax, you
+can use the -lang flag with the at command. This is needed since the
+at command type checks the result it produces, and it needs to
+know which abstract sytnax to type check it in.
+
+
+
+
+
diff --git a/doc/transfer-tutorial.txt b/doc/transfer-tutorial.txt
new file mode 100644
index 000000000..dba660871
--- /dev/null
+++ b/doc/transfer-tutorial.txt
@@ -0,0 +1,164 @@
+Transfer tutorial
+Author: Björn Bringert
+Last update: %%date(%c)
+
+% NOTE: this is a txt2tags file.
+% Create an html file from this file using:
+% txt2tags -t html --toc darcs.txt
+
+%!target:html
+%!options(html): --toc
+
+
+
+= Objective =
+
+We want to write a Transfer program which we can use to do aggregation
+in sentences which use conjugations on the sentence, noun phrase and
+verb phrase levels. For example, we want to be able to transform
+the sentence "John walks and Mary walks" to the sentence
+"John and Mary walk". We would also like to transform
+"John walks and John swims" to "John walks and swims".
+
+Thus that what we want to do is:
+
+- Transform sentence conjugation where the verb phrases in the sentences
+ are identical to noun phrase conjugation.
+- Transform sentence conjugation where the noun phrases in the sentences
+ are identical to verb phrase conjugation.
+
+
+This needs to be done recursively and thoughout the sentence, to be
+able to handle cases like "John walks and Mary walks and Bill walks", and
+"John runs and Mary walks and Bill walks".
+
+
+FIXME: what about John walks and Mary runs and Bill walks"?
+
+
+= Abstract syntax =
+
+We will use the abstract syntax defined in
+[Abstract.gf ../transfer/examples/aggregation/Abstract.gf].
+
+= Concrete syntax =
+
+There is an English concrete syntax for this grammar in
+[English.gf ../transfer/examples/aggregation/English.gf].
+
+= Generate tree module =
+
+To be able to write Transfer programs which use the types defined in
+an abstract syntax, we first need to generate a Transfer file with
+a data type defintition corresponding to the abstract syntax.
+This is done with the ``transfer`` grammar printer:
+
+```
+$ gf
+> i English.gf
+> pg -printer=transfer | wf tree.tr
+```
+
+Note that you need to load a concrete syntax which uses the abstract
+syntax that you want to create a Transfer data type for. Loading just the
+abstract syntax module is not enough. FIXME: why?
+
+The command sequence above writes a Transfer data type definition to the
+file ``tree.tr``.
+
+
+= Write transfer code =
+
+We write the Transfer program
+[aggregate.tr ../transfer/examples/aggregation/aggregate.tr].
+
+FIXME: explain the code
+
+= Compiling Transfer programs =
+
+Transfer programs are written in the human-friendly Transfer language,
+but GF only understands the simpler Transfer Core language. Therefore,
+before using a Transfer program, you must first compile it to
+Transfer Core. This is done using the ``transferc`` command:
+
+```
+$ transferc -i
+```
+
+Here, ```` is the path to search for any modules which you import
+in your Transfer program. You can give several ``-i`` flags.
+
+So, to compile ``aggregate.tr`` which we created above, we use:
+
+```
+$ transferc aggregate.tr
+```
+
+The creates the Transfer Core file ``aggregate.trc``.
+
+
+= Using Transfer programs in GF =
+
+== Loading the grammars ==
+
+To use a Transfer Core program to transform abstract syntax terms
+in GF, you must first load the grammars which you want to use the
+program with. For the example above, we need the grammar ``English.gf``
+and its dependencies. We load this grammar with:
+
+```
+> i English.gf
+```
+
+== Loading the Transfer program ==
+
+There are two steps to using a Transfer Core program in GF. First you load
+the program into GF. This is done with the ``i`` command, which is also
+used when loading grammar modules. To load the ``aggregate.trc`` which
+we created above, we use:
+
+```
+> i aggregate.trc
+```
+
+== Calling Transfer functions ==
+
+To call a Transfer function on a term, we use the ``at`` command.
+The ``at`` command takes the name of a Transfer function and an abstract
+syntax term, and applies the function to the term:
+
+```
+> at aggregS ConjS And (Pred John Walk) (Pred Mary Walk)
+
+Pred (ConjNP And John Mary) Walk
+```
+
+Of course, the input and output terms of the ``at`` command can
+be read from and written to pipes:
+
+```
+> p "John walks and Mary walks" | at aggregS | l
+
+John and Mary walk
+```
+
+To see what is going on between the steps, we can use ``-tr`` flags
+to the commands:
+
+```
+> p -tr "John walks and Mary walks" | at -tr aggregS | l
+
+ConjS And (Pred John Walk) (Pred Mary Walk)
+
+Pred (ConjNP And John Mary) Walk
+
+John and Mary walk
+```
+
+=== Transfer between different abstract syntaxes ===
+
+If the transfer function which you wan to call takes as input a term in one
+abstract syntax, and returns a term in a different abstract syntax, you
+can use the ``-lang`` flag with the ``at`` command. This is needed since the
+``at`` command type checks the result it produces, and it needs to
+know which abstract sytnax to type check it in.
\ No newline at end of file
diff --git a/doc/transfer.html b/doc/transfer.html
new file mode 100644
index 000000000..87c5bb05f
--- /dev/null
+++ b/doc/transfer.html
@@ -0,0 +1,30 @@
+
+
+
+
+The GF Transfer language
+
+The GF Transfer language
+
+Author: Björn Bringert <bringert@cs.chalmers.se>
+Last update: Tue Dec 6 14:26:07 2005
+
+
+
+The GF Transfer language is a programming language which can be
+used to write functions which work on abstract syntax terms.
+
+Transfer tutorial
+
+The Transfer tutorial shows an example of how to
+write and use a simple transfer function for a GF grammar.
+
+Transfer reference
+
+The Transfer reference aims to cover
+all constructs in the Transfer language.
+
+
+
+
+
diff --git a/doc/transfer.txt b/doc/transfer.txt
new file mode 100644
index 000000000..7952aae5f
--- /dev/null
+++ b/doc/transfer.txt
@@ -0,0 +1,24 @@
+The GF Transfer language
+Author: Björn Bringert
+Last update: %%date(%c)
+
+% NOTE: this is a txt2tags file.
+% Create an html file from this file using:
+% txt2tags transfer.txt
+
+%!target:html
+
+The GF Transfer language is a programming language which can be
+used to write functions which work on abstract syntax terms.
+
+= Transfer tutorial =
+
+The [Transfer tutorial transfer-tutorial.html] shows an example of how to
+write and use a simple transfer function for a GF grammar.
+
+
+= Transfer reference =
+
+The [Transfer reference transfer-reference.html] aims to cover
+all constructs in the Transfer language.
+
diff --git a/doc/txt2html.sh b/doc/txt2html.sh
new file mode 100644
index 000000000..801541e95
--- /dev/null
+++ b/doc/txt2html.sh
@@ -0,0 +1,13 @@
+#!/bin/sh
+
+FILES="darcs.txt transfer-reference.txt transfer-tutorial.txt \
+ transfer.txt"
+
+for f in $FILES; do
+ h=`basename "$f" ".txt"`.html
+ if [ "$f" -nt "$h" ]; then
+ txt2tags $f
+ else
+ echo "$h is newer than $f, skipping"
+ fi
+done
diff --git a/transfer/Makefile b/transfer/Makefile
index b4bee8ce8..1ef8da644 100644
--- a/transfer/Makefile
+++ b/transfer/Makefile
@@ -1,11 +1,13 @@
SRCDIR=../src
GHC=ghc
-GHCFLAGS=-i$(SRCDIR)
+GHCFLAGS=-i$(SRCDIR)
+GHCOPTFLAGS=-O2
.PHONY: all bnfc bnfctest doc docclean clean bnfcclean distclean
+all: GHCFLAGS += $(GHCOPTFLAGS)
all:
$(GHC) $(GHCFLAGS) --make -o trci trci.hs
$(GHC) $(GHCFLAGS) --make -o transferc transferc.hs
diff --git a/transfer/examples/aggregation/aggregate.tr b/transfer/examples/aggregation/aggregate.tr
index d7d955bb8..7cdfaddca 100644
--- a/transfer/examples/aggregation/aggregate.tr
+++ b/transfer/examples/aggregation/aggregate.tr
@@ -44,23 +44,14 @@ aggreg _ t =
case t of
ConjS c s1 s2 ->
case (aggreg ? s1, aggreg ? s2) of
- (Pred np1 vp1, Pred np2 vp2) | eq_NP np1 np2 ->
+ (Pred np1 vp1, Pred np2 vp2) | eq NP (eq_Tree NP) np1 np2 ->
Pred np1 (ConjVP c vp1 vp2)
- (Pred np1 vp1, Pred np2 vp2) | eq_VP vp1 vp2 ->
+ (Pred np1 vp1, Pred np2 vp2) | eq VP (eq_Tree VP) vp1 vp2 ->
Pred (ConjNP c np1 np2) vp1
- (s1',s2') -> ConjS c s1' s2'
+ (s1',s2') -> ConjS c s1' s2'
_ -> composOp ? ? compos_Tree ? aggreg t
-- aggreg specialized for Tree S
aggregS : Tree S -> Tree S
aggregS = aggreg S
-
--- equality specialized for Tree NP
-eq_NP : Tree NP -> Tree NP -> Bool
-eq_NP = eq NP (eq_Tree NP)
-
--- equality specialized for Tree VP
-eq_VP : Tree VP -> Tree VP -> Bool
-eq_VP = eq VP (eq_Tree VP)
-
diff --git a/transfer/examples/aggregation/transfer-tutorial.txt b/transfer/examples/aggregation/transfer-tutorial.txt
deleted file mode 100644
index cb8ca876d..000000000
--- a/transfer/examples/aggregation/transfer-tutorial.txt
+++ /dev/null
@@ -1,12 +0,0 @@
-- Problem
-
-- Abstract syntax
-
-- Concrete syntax
-
-- Generate tree module
-
-- Write transfer code
- - Derive Compos and Eq
-
-
diff --git a/transfer/examples/aggregation/tree.tr b/transfer/examples/aggregation/tree.tr
index 2e9ead648..5515efa21 100644
--- a/transfer/examples/aggregation/tree.tr
+++ b/transfer/examples/aggregation/tree.tr
@@ -1,20 +1,23 @@
+import prelude ;
data Cat : Type where {
Conj : Cat ;
NP : Cat ;
S : Cat ;
VP : Cat
} ;
-data Tree : (_ : Cat)-> Type where {
+data Tree : Cat -> Type where {
And : Tree Conj ;
Bill : Tree NP ;
- ConjNP : (_ : Tree Conj)-> (_ : Tree NP)-> (_ : Tree NP)-> Tree NP ;
- ConjS : (_ : Tree Conj)-> (_ : Tree S)-> (_ : Tree S)-> Tree S ;
- ConjVP : (_ : Tree Conj)-> (_ : Tree VP)-> (_ : Tree VP)-> Tree VP ;
+ ConjNP : Tree Conj -> Tree NP -> Tree NP -> Tree NP ;
+ ConjS : Tree Conj -> Tree S -> Tree S -> Tree S ;
+ ConjVP : Tree Conj -> Tree VP -> Tree VP -> Tree VP ;
John : Tree NP ;
Mary : Tree NP ;
Or : Tree Conj ;
- Pred : (_ : Tree NP)-> (_ : Tree VP)-> Tree S ;
+ Pred : Tree NP -> Tree VP -> Tree S ;
Run : Tree VP ;
Swim : Tree VP ;
Walk : Tree VP
-}
+} ;
+derive Eq Tree ;
+derive Compos Tree ;
diff --git a/transfer/examples/test.tr b/transfer/examples/test.tr
index 8f08f8431..0abb933ef 100644
--- a/transfer/examples/test.tr
+++ b/transfer/examples/test.tr
@@ -1,4 +1,4 @@
import nat
import fib
-main = natToInt (fibNat (intToNat 10))
\ No newline at end of file
+-- main = natToInt (fibNat (intToNat 10))
\ No newline at end of file