Simple transfer tutorial touch-up.

doc/transfer-tutorial.html

@@ -7,7 +7,7 @@
 <P ALIGN="center"><CENTER><H1>Transfer tutorial</H1>
 <FONT SIZE="4">
 <I>Author: Björn Bringert &lt;bringert@cs.chalmers.se&gt;</I><BR>
-Last update: Tue Dec  6 14:26:07 2005
+Last update: Tue Dec  6 17:25:21 2005
 </FONT></CENTER>
 
 <P></P>
@@ -77,7 +77,7 @@ There is an English concrete syntax for this grammar in
 <A NAME="toc4"></A>
 <H1>Generate tree module</H1>
 <P>
-To be able to write Transfer programs which sue the types defined in
+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 <CODE>transfer</CODE> grammar printer:
@@ -95,7 +95,7 @@ abstract syntax module is not enough. FIXME: why?
 </P>
 <P>
 The command sequence above writes a Transfer data type definition to the
-file <CODE>tree.tr</CODE>.
+file <A HREF="../transfer/examples/aggregation/tree.tr">tree.tr</A>.
 </P>
 <A NAME="toc5"></A>
 <H1>Write transfer code</H1>
@@ -206,5 +206,5 @@ know which abstract sytnax to type check it in.
 </P>
 
 <!-- html code generated by txt2tags 2.0 (http://txt2tags.sf.net) -->
-<!-- cmdline: txt2tags darcs.txt transfer-reference.txt transfer-tutorial.txt transfer.txt -->
+<!-- cmdline: txt2tags transfer-tutorial.txt -->
 </BODY></HTML>

doc/transfer-tutorial.txt

@@ -64,7 +64,7 @@ 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``.
+file [tree.tr ../transfer/examples/aggregation/tree.tr].
 
 
 = Write transfer code =

transfer/examples/aggregation/aggregate.tr

@@ -1,44 +1,12 @@
 import prelude
 import tree
 
-derive Eq Tree
-derive Compos Tree
-
-
--- When the Transfer compiler gets meta variable inference,
--- we can write:
-{-
-aggreg : (A : Type) -> Tree A -> Tree A
-aggreg _ t = 
-  case t of
-      ConjS c s1 s2 -> 
-	case (aggreg ? s1, aggreg ? s2) of
-		(Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> 
-			Pred np1 (ConjVP c vp1 vp2)
-                (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> 
-	        	Pred (ConjNP c np1 np2) vp1
-		(s1',s2') -> ConjS c s1' s2'
-      _ -> composOp ? ? ? ? aggreg t
--}
-
--- Adding hidden arguments, we could write something like:
-{-
-aggreg : (A : Type) => Tree A -> Tree A
-aggreg t = 
-  case t of
-      ConjS c s1 s2 -> 
-	case (aggreg s1, aggreg s2) of
-		(Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> 
-			Pred np1 (ConjVP c vp1 vp2)
-                (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> 
-	        	Pred (ConjNP c np1 np2) vp1
-		(s1',s2') -> ConjS c s1' s2'
-      _ -> composOp aggreg t
--}
 
+-- aggreg specialized for Tree S
+aggregS : Tree S -> Tree S
+aggregS = aggreg S
 
 -- For now, here's what we have to do:
-
 aggreg : (A : Type) -> Tree A -> Tree A
 aggreg _ t = 
   case t of
@@ -52,6 +20,37 @@ aggreg _ t =
       _ -> composOp ? ? compos_Tree ? aggreg t
 
 
--- aggreg specialized for Tree S
+
-aggregS : Tree S -> Tree S
+
-aggregS = aggreg S
+
+{-
+-- When the Transfer compiler gets meta variable inference,
+-- we can write this:
+aggreg : (A : Type) -> Tree A -> Tree A
+aggreg _ t = 
+  case t of
+      ConjS c s1 s2 -> 
+	case (aggreg ? s1, aggreg ? s2) of
+		(Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> 
+			Pred np1 (ConjVP c vp1 vp2)
+                (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> 
+	        	Pred (ConjNP c np1 np2) vp1
+		(s1',s2') -> ConjS c s1' s2'
+      _ -> composOp ? ? ? ? aggreg t
+-}
+
+
+{-
+-- If we added idden arguments, we could write something like this:
+aggreg : (A : Type) => Tree A -> Tree A
+aggreg t = 
+  case t of
+      ConjS c s1 s2 -> 
+	case (aggreg s1, aggreg s2) of
+		(Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> 
+			Pred np1 (ConjVP c vp1 vp2)
+                (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> 
+	        	Pred (ConjNP c np1 np2) vp1
+		(s1',s2') -> ConjS c s1' s2'
+      _ -> composOp aggreg t
+-}