summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorbringert <bringert@cs.chalmers.se>2005-12-06 16:26:55 +0000
committerbringert <bringert@cs.chalmers.se>2005-12-06 16:26:55 +0000
commitee4adf5ba8ff50b4580a18d197f9e05d36195ede (patch)
treef12c7b7cc839a35735313c584b96c9e5febc5f2b
parent41aaed58d4734b7cec5a4d2567283cb818f77cbb (diff)
Simple transfer tutorial touch-up.
-rw-r--r--doc/transfer-tutorial.html8
-rw-r--r--doc/transfer-tutorial.txt2
-rw-r--r--transfer/examples/aggregation/aggregate.tr49
3 files changed, 29 insertions, 30 deletions
diff --git a/doc/transfer-tutorial.html b/doc/transfer-tutorial.html
index 7ca1c2060..038ba1aca 100644
--- a/doc/transfer-tutorial.html
+++ b/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>
diff --git a/doc/transfer-tutorial.txt b/doc/transfer-tutorial.txt
index dba660871..8f5c5179d 100644
--- a/doc/transfer-tutorial.txt
+++ b/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 =
diff --git a/transfer/examples/aggregation/aggregate.tr b/transfer/examples/aggregation/aggregate.tr
index 7cdfaddca..b71ccfef2 100644
--- a/transfer/examples/aggregation/aggregate.tr
+++ b/transfer/examples/aggregation/aggregate.tr
@@ -1,13 +1,31 @@
import prelude
import tree
-derive Eq Tree
-derive Compos Tree
+
+-- 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
+ ConjS c s1 s2 ->
+ case (aggreg ? s1, aggreg ? s2) of
+ (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 (eq_Tree VP) vp1 vp2 ->
+ Pred (ConjNP c np1 np2) vp1
+ (s1',s2') -> ConjS c s1' s2'
+ _ -> composOp ? ? compos_Tree ? aggreg t
+
+
+
--- When the Transfer compiler gets meta variable inference,
--- we can write:
{-
+-- When the Transfer compiler gets meta variable inference,
+-- we can write this:
aggreg : (A : Type) -> Tree A -> Tree A
aggreg _ t =
case t of
@@ -21,8 +39,9 @@ aggreg _ t =
_ -> composOp ? ? ? ? aggreg t
-}
--- Adding hidden arguments, we could write something like:
+
{-
+-- If we added idden arguments, we could write something like this:
aggreg : (A : Type) => Tree A -> Tree A
aggreg t =
case t of
@@ -35,23 +54,3 @@ aggreg t =
(s1',s2') -> ConjS c s1' s2'
_ -> composOp aggreg t
-}
-
-
--- For now, here's what we have to do:
-
-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) | eq NP (eq_Tree NP) np1 np2 ->
- Pred np1 (ConjVP c 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'
- _ -> composOp ? ? compos_Tree ? aggreg t
-
-
--- aggreg specialized for Tree S
-aggregS : Tree S -> Tree S
-aggregS = aggreg S