summaryrefslogtreecommitdiff
path: root/transfer/examples/aggregation/aggregate.tra
diff options
context:
space:
mode:
authoraarne <aarne@cs.chalmers.se>2008-06-26 21:05:01 +0000
committeraarne <aarne@cs.chalmers.se>2008-06-26 21:05:01 +0000
commitfb1d9b7d2c3c8261fc5a2ce3698e6749458b207a (patch)
tree466adc81f2c6ac803d20804863927c076e2b243a /transfer/examples/aggregation/aggregate.tra
parent33eb6d899fef48f2d38a92bc0fab66ff585be553 (diff)
removed transfer from gf3
Diffstat (limited to 'transfer/examples/aggregation/aggregate.tra')
-rw-r--r--transfer/examples/aggregation/aggregate.tra56
1 files changed, 0 insertions, 56 deletions
diff --git a/transfer/examples/aggregation/aggregate.tra b/transfer/examples/aggregation/aggregate.tra
deleted file mode 100644
index b71ccfef2..000000000
--- a/transfer/examples/aggregation/aggregate.tra
+++ /dev/null
@@ -1,56 +0,0 @@
-import prelude
-import 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 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
--}