Moved transfer documentation to doc/. Added sections and text to transfer tutorial and reference. Added script for generating html from txt2tags files.

1 files changed, 413 insertions, 0 deletions

diff --git a/doc/transfer-reference.txt b/doc/transfer-reference.txt
new file mode 100644
index 000000000..dd16e2d39
--- /dev/null
+++ b/doc/transfer-reference.txt
@@ -0,0 +1,413 @@
+Transfer language reference
+Author: Björn Bringert <bringert@cs.chalmers.se>
+Last update: %%date(%c)
+
+
+% NOTE: this is a txt2tags file.
+% Create an html file from this file using:
+% txt2tags transfer.txt
+
+%!target:html
+%!options(html): --toc
+
+
+
+
+
+
+This document describes the features of the Transfer language.
+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.
+
+== 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 #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 ===[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 ==
+