removed obsolete items from doc

1 files changed, 0 insertions, 649 deletions

diff --git a/doc/transfer-reference.txt b/doc/transfer-reference.txt
deleted file mode 100644
index 143780381..000000000
--- a/doc/transfer-reference.txt
+++ /dev/null
@@ -1,649 +0,0 @@
-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
-%!encoding:utf-8
-
-**WARNING: The Transfer language is still experimental. Its syntax, type system and semantics may change without notice. I will try to help you with any problems this might cause, but I will not refrain from changing the language solely for reasons of backwards compatibility.**
-
-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. The language supports generalized algebraic
-datatypes, pattern matching and function overloading.
-
-
-== Current implementation status ==
-
-**Not all features of the Transfer language have been implemented yet**. The most 
-important missing piece is the type checker. This means that there are almost
-no checks done on Transfer programs before they are run. It also means that
-the values of metavariables are not inferred. Thus metavariables cannot
-be used where their values matter. For example, dictionaries for overloaded 
-functions must be given explicitly, not as metavariables.
-
-
-== 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 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 it is equivalent to:
-
-```
-case x of { p1 -> e1 ; p2 -> e2 }
-```
-
-
-== Imports ==
-
-A Transfer module starts with some imports. Most modules will have to
-import the prelude, which contains definitons used by most programs:
-
-```
-import prelude
-```
-
-For more information about the standard prelude, see [Standard prelude #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 then 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 p11 ... p1m = exp1
-...
-f pn1 ... pnm = expn
-```
-
-where ``p11`` to ``pnm`` are patterns, see [Patterns #patterns].
-
-
-Pattern equations can also have guards, boolean expressions which determine
-whether to use the equation when the pattern has been matched. Pattern equations 
-with guards are written:
-
-```
-f p11 ... p1m | guard1 = exp1
-...
-f pn1 ... pnm | guardn = expn
-```
-
-Pattern equations with and without guards can be mixed in the definiton of 
-a function.
-
-Any variables bound in the patterns are in scope in the guards and 
-right hand sides of each pattern equation.
-
-
-
-== 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. 
-
-FIXME: explain the constraints on the types of type and data constructors.
-
-
-== 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 = exp1
-    ...
-    xn = expn
- in exp
-```
-
-Here, the variables ``x1`` to ``xn`` are in scope in all the expressions
-``exp1`` to ``expn``, and in ``exp``. Thus let-defined functions can be
-mutually recursive.
-
-
-== 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 one
-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 teo 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:
-
-```
-(x : A) -> B
-```
-
-Here, ``x`` is in scope in ``B``. 
-
-
-=== Basic types ===
-
-==== Integers ====
-
-The type of integers is called ``Integer``. 
-Standard decmial integer literals, such as ``0`` and ``1234`` 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. String literals are written 
-with double quotes, e.g. ``"this is a string"``.
-FIXME: This might be replaced by a list of 
-characters representation in the future. 
-
-
-==== Booleans ====
-
-Booleans are not a built-in type, though some features of the Transfer language
-depend on them. The ``Bool`` type is defined in the 
-[Standard prelude #prelude].
-
-```
-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 ====
-
-Record types are created by using a ``sig`` expression:
-
-```
-sig { l1 : T1; ... ; ln : Tn }
-```
-
-Here, ``l1`` to ``ln`` are the field labels and ``T1`` to ``Tn`` are field types.
-
-==== Record values ====
-
-Record values are constructed using ``rec`` expressions:
-
-```
-rec { l1 = exp1; ... ; ln = expn }
-```
-
-==== Record projection ====
-
-Fields are selected from records using the ``.`` operator. This expression selects
-the field ``l`` from the record value ``r``:
-
-```
-r.l
-```
-
-==== Records and layout syntax ====
-
-The curly braces and semicolons are simply explicit layout syntax, so 
-the record type and record expression above can also be written as:
-
-```
-sig l1 : T1
-    ...
-    ln : Tn
-```
-
-```
-rec l1 = exp1
-    ...
-    ln = expn
-```
-
-
-==== Record subtyping ====[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]
-
-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 list can be written as ``[]``. There is an operator ``::`` which can 
-be used instead of ``Cons``. These are just syntactic sugar for expressions
-using ``Nil`` and ``Cons``, with the type arguments hidden.
-
-
-== Case expressions ==
-
-Pattern matching is done in pattern equations and with the 
-``case`` construct:
-
-```
-case exp of
-     p1 | guard1 -> rhs1
-     ...
-     pn | guardn -> rhsn
-```
-
-where ``p1`` to ``pn`` are patterns, see [Patterns #patterns].
-``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
-```
-
-
-== Patterns ==[patterns]
-
-=== 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 ``C v1 ... 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.
-Note that variable patterns may not use the same identifier as data constructors
-which are in scope, since they will then be interpreted as constructor
-patterns.
-
-
-=== Wildcard patterns ===
-
-Wildcard patterns are written 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.
-The values of these fields do not influence the pattern matching.
-
-
-=== 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 ===
-
-When pattern matching on lists, there are two special constructs.
-A whole list can by matched be a list of patterns:
-
-```
-[p1, ... , pn]
-```
-
-This pattern will match lists of length n, such that each element
-in the list matches the corresponding pattern. The empty list pattern:
-
-```
-[]
-```
-
-is a special case of this. It matches the empty list, oddly enough.
-
-Non-empty lists can also be matched with ``::``-patterns:
-
-```
-p1::p2
-```
-
-This pattern matches non-empty lists such that the first element of
-the list matches ``p1`` and the rest of the list matches ``p2``.
-
-
-=== Tuple patterns ===
-
-Tuples patterns on the form:
-
-```
-(p1, ... , pn)
-```
-
-are syntactic sugar for record patterns, in the same way as 
-tuple expressions, see [Tuples #tuples].
-
-
-=== String literal patterns ===
-
-String literals can be used as patterns.
-
-
-=== Integer literal patterns ===
-
-Integer literals can be used as patterns.
-
-
-== Metavariables ==[metavariables]
-
-Metavariables are written as questions marks:
-
-```
-?
-```
-
-A metavariable is a way to tell the type checker that:
-"you should be able to figure out what this should be,
-I can't be bothered to tell you". 
-
-Metavariables can be used to avoid having to give type
-and dictionary arguments explicitly.
-
-
-== Overloaded functions ==
-
-In Transfer, functions can be overloaded by having them take a record
-of functions as an argument. For example, the functions for equality
-and inequality in the Transfer [Prelude #prelude] are defined as:
-
-```
-Eq : Type -> Type
-Eq A = sig eq : A -> A -> Bool
-
-eq : (A : Type) -> Eq A -> A -> A -> Bool
-eq _ d = d.eq
-
-neq : (A : Type) -> Eq A -> A -> A -> Bool
-neq A d x y = not (eq A d x y)
-```
-
-We call ``Eq`` a //type class//, though it's actually just a record type
-used to pass function implementations to overloaded functions.  We
-call a value of type ``Eq A`` an Eq //dictionary// for the type A.
-The dictionary is used to look up the version of some function for the
-particular type we want to use the function on. Thus, in order to use
-the ``eq`` function on two integers, we need a dictionary of type 
-``Eq Integer``:
-
-```
-eq_Integer : Eq Integer
-eq_Integer = rec eq = prim_eq_Integer
-```
-
-where ``prim_eq_Integer`` is the built-in equality function for
-integers. To check whether two numbers ``x`` and ``y`` are equal, we
-can then call the overloaded ``eq`` function with the dictionary:
-
-```
-eq Integer eq_Integer x y
-```
-
-Giving the type at which to use the overloaded function, and the appropriate
-dictionary can be cumbersome. [Metavariables #metavariables] come to the rescue:
-
-```
-eq ? ? x y
-```
-
-The type checker can in most cases figure out the values of the type and 
-dictionary arguments. **NOTE: this is not implemented yet.**
-
-
-=== Type class extension ===
-
-By using record subtyping, see [Record subtyping #record_subtyping], we can
-create type classes which extend other type classes. A dictionary for the
-new type class can also be used as a dictionary for old type class.
-
-For example, we can extend the ``Eq`` type class above to ``Ord``, a type 
-class for orderings:
-
-```
-Ord : Type -> Type
-Ord A = sig eq : A -> A -> Bool
-            compare : A -> A -> Ordering
-```
-
-To extend an existing class, we keep the fields of the class we want to
-extend, and add any new fields that we want. Because of record subtyping, 
-for any type ``A``, a value of type ``Ord A`` is also a value of type ``Eq A``.
-
-
-=== Extending multiple classes ===
-
-A type class can also extend several classes, by simply having all the fields
-from all the classes we want to extend. The ``Num`` class in the 
-[Standard prelude #prelude] is an example of this.
-
-
-== Standard prelude ==[prelude]
-
-The standard prelude, see [prelude.tra ../transfer/lib/prelude.tra],
-contains definitions of a number of standard types, functions and 
-type classes.
-
-
-== Operators == 
-
-Most built-in operators in the Transfer language are translated
-to calls to overloaded functions. This means that they can be
-used at any type for which there is a dictionary for the type class
-in question.
-
-=== Unary operators ===
-
-|| Operator | Precedence | Translation              |
-| ``-``     |    10      |  ``-x => negate ? ? x``  |
-
-
-=== Binary operators ===
-
-|| Operator | Precedence | Associativity | Translation of ``x op y``    |
-|  ``>>=``  |     3      |    left       |  ``bind ? ? x y``            |
-|  ``>>``   |     3      |    left       |  ``bind ? ? x (\_ -> y)``    |
-|  ``||``   |     4      |    right      |  ``if x then True else y``   |
-|  ``&&``   |     5      |    right      |  ``if x then y else False``  |
-|  ``==``   |     6      |    none       |  ``eq ? ? x y``              |
-|  ``/=``   |     6      |    none       |  ``neq ? ? x y``             |
-|  ``<``    |     6      |    none       |  ``lt ? ? x y``              |
-|  ``<=``   |     6      |    none       |  ``le ? ? x y``              |
-|  ``>``    |     6      |    none       |  ``gt ? ? x y``              |
-|  ``>=``   |     6      |    none       |  ``ge ? ? x y``              |
-|  ``::``   |     7      |    right      |  ``Cons ? ? x y``            |
-|  ``+``    |     8      |    left       |  ``plus ? ? x y``            |
-|  ``-``    |     8      |    left       |  ``minus ? ? x y``           |
-|  ``*``    |     9      |    left       |  ``times ? ? x y``           |
-|  ``/``    |     9      |    left       |  ``div ? ? x y``             |
-|  ``%``    |     9      |    left       |  ``mod ? ? x y``             |
-
-
-
-== Compositional functions ==
-
-
-
-== do notation ==
-
-Sequences of operations in the Monad type class can be written 
-using do-notation, like in Haskell:
-
-```
-do x <- f
-   y <- g x
-   h y
-```
-
-is equivalent to:
-
-```
-f >>= \x -> g x >>= \y -> h y
-```