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 @@

Transfer tutorial

Author: Björn Bringert <bringert@cs.chalmers.se>
-Last update: Tue Dec 6 14:26:07 2005 +Last update: Tue Dec 6 17:25:21 2005

@@ -77,7 +77,7 @@ There is an English concrete syntax for this grammar in

Generate tree module

-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 transfer grammar printer: @@ -95,7 +95,7 @@ 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.

Write transfer code

@@ -206,5 +206,5 @@ know which abstract sytnax to type check it in.

- + 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,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 +-}