From c703a92136ce579282c63c6e31fff76cc84b37ce Mon Sep 17 00:00:00 2001 From: bringert Date: Tue, 6 Dec 2005 16:33:40 +0000 Subject: Transfer: Changed transfer program file extension from .tr to .tra to avoid collision with Troff file extension. --- transfer/examples/aggregation/aggregate.tr | 56 ----------------------------- transfer/examples/aggregation/aggregate.tra | 56 +++++++++++++++++++++++++++++ transfer/examples/aggregation/tree.tr | 23 ------------ transfer/examples/aggregation/tree.tra | 23 ++++++++++++ 4 files changed, 79 insertions(+), 79 deletions(-) delete mode 100644 transfer/examples/aggregation/aggregate.tr create mode 100644 transfer/examples/aggregation/aggregate.tra delete mode 100644 transfer/examples/aggregation/tree.tr create mode 100644 transfer/examples/aggregation/tree.tra (limited to 'transfer/examples/aggregation') diff --git a/transfer/examples/aggregation/aggregate.tr b/transfer/examples/aggregation/aggregate.tr deleted file mode 100644 index b71ccfef2..000000000 --- a/transfer/examples/aggregation/aggregate.tr +++ /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 --} diff --git a/transfer/examples/aggregation/aggregate.tra b/transfer/examples/aggregation/aggregate.tra new file mode 100644 index 000000000..b71ccfef2 --- /dev/null +++ b/transfer/examples/aggregation/aggregate.tra @@ -0,0 +1,56 @@ +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 +-} diff --git a/transfer/examples/aggregation/tree.tr b/transfer/examples/aggregation/tree.tr deleted file mode 100644 index 5515efa21..000000000 --- a/transfer/examples/aggregation/tree.tr +++ /dev/null @@ -1,23 +0,0 @@ -import prelude ; -data Cat : Type where { - Conj : Cat ; - NP : Cat ; - S : Cat ; - VP : Cat -} ; -data Tree : Cat -> Type where { - And : Tree Conj ; - Bill : Tree NP ; - ConjNP : Tree Conj -> Tree NP -> Tree NP -> Tree NP ; - ConjS : Tree Conj -> Tree S -> Tree S -> Tree S ; - ConjVP : Tree Conj -> Tree VP -> Tree VP -> Tree VP ; - John : Tree NP ; - Mary : Tree NP ; - Or : Tree Conj ; - Pred : Tree NP -> Tree VP -> Tree S ; - Run : Tree VP ; - Swim : Tree VP ; - Walk : Tree VP -} ; -derive Eq Tree ; -derive Compos Tree ; diff --git a/transfer/examples/aggregation/tree.tra b/transfer/examples/aggregation/tree.tra new file mode 100644 index 000000000..5515efa21 --- /dev/null +++ b/transfer/examples/aggregation/tree.tra @@ -0,0 +1,23 @@ +import prelude ; +data Cat : Type where { + Conj : Cat ; + NP : Cat ; + S : Cat ; + VP : Cat +} ; +data Tree : Cat -> Type where { + And : Tree Conj ; + Bill : Tree NP ; + ConjNP : Tree Conj -> Tree NP -> Tree NP -> Tree NP ; + ConjS : Tree Conj -> Tree S -> Tree S -> Tree S ; + ConjVP : Tree Conj -> Tree VP -> Tree VP -> Tree VP ; + John : Tree NP ; + Mary : Tree NP ; + Or : Tree Conj ; + Pred : Tree NP -> Tree VP -> Tree S ; + Run : Tree VP ; + Swim : Tree VP ; + Walk : Tree VP +} ; +derive Eq Tree ; +derive Compos Tree ; -- cgit v1.2.3