Added aggregation example.

5 files changed, 140 insertions, 0 deletions

diff --git a/transfer/examples/aggregation/Abstract.gf b/transfer/examples/aggregation/Abstract.gf
new file mode 100644
index 000000000..9d8b31d0d
--- /dev/null
+++ b/transfer/examples/aggregation/Abstract.gf
@@ -0,0 +1,24 @@
+-- testing transfer: aggregation by def definitions. AR 12/4/2003 -- 9/10
+
+--   p "Mary runs or John runs and John walks" | l -transfer=Aggregation
+--   Mary runs or John runs and walks
+--   Mary or John runs and John walks
+
+-- The two results are due to ambiguity in parsing. Thus it is not spurious!
+
+abstract Abstract = {
+
+cat 
+  S ; NP ; VP ; Conj ;
+
+fun
+  Pred : NP -> VP -> S ;
+  ConjS : Conj -> S -> S -> S ;
+  ConjVP : Conj -> VP -> VP -> VP ;
+  ConjNP : Conj -> NP -> NP -> NP ;
+
+  John, Mary, Bill : NP ;
+  Walk, Run, Swim : VP ;
+  And, Or : Conj ;
+
+}
diff --git a/transfer/examples/aggregation/English.gf b/transfer/examples/aggregation/English.gf
new file mode 100644
index 000000000..21da16b23
--- /dev/null
+++ b/transfer/examples/aggregation/English.gf
@@ -0,0 +1,18 @@
+concrete English of Abstract = {
+
+pattern
+  Pred np vp = np ++ vp ;
+  ConjS c A  B = A ++ c ++ B ;
+  ConjVP c A  B = A ++ c ++ B ;
+  ConjNP c A  B = A ++ c ++ B ;
+  
+  John = "John" ;
+  Mary = "Mary" ;
+  Bill = "Bill" ;
+  Walk = "walks" ;
+  Run = "runs" ;
+  Swim = "swims" ;
+
+  And = "and" ;
+  Or = "or" ;
+}
diff --git a/transfer/examples/aggregation/aggregate.tr b/transfer/examples/aggregation/aggregate.tr
new file mode 100644
index 000000000..d7d955bb8
--- /dev/null
+++ b/transfer/examples/aggregation/aggregate.tr
@@ -0,0 +1,66 @@
+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
+-}
+
+
+-- 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 np1 np2 -> 
+			Pred np1 (ConjVP c vp1 vp2)
+                (Pred np1 vp1, Pred np2 vp2) | eq_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
+
+-- equality specialized for Tree NP
+eq_NP : Tree NP -> Tree NP -> Bool
+eq_NP = eq NP (eq_Tree NP)
+
+-- equality specialized for Tree VP
+eq_VP : Tree VP -> Tree VP -> Bool
+eq_VP = eq VP (eq_Tree VP)
+
diff --git a/transfer/examples/aggregation/transfer.txt b/transfer/examples/aggregation/transfer.txt
new file mode 100644
index 000000000..cb8ca876d
--- /dev/null
+++ b/transfer/examples/aggregation/transfer.txt
@@ -0,0 +1,12 @@
+- Problem
+
+- Abstract syntax
+
+- Concrete syntax
+
+- Generate tree module
+
+- Write transfer code
+ - Derive Compos and Eq
+
+
diff --git a/transfer/examples/aggregation/tree.tr b/transfer/examples/aggregation/tree.tr
new file mode 100644
index 000000000..2e9ead648
--- /dev/null
+++ b/transfer/examples/aggregation/tree.tr
@@ -0,0 +1,20 @@
+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 
+}