From 7c24fcb38faeaada097d2797e9cb0f305dbc637e Mon Sep 17 00:00:00 2001
From: bringert <bringert@cs.chalmers.se>
Date: Mon, 5 Dec 2005 16:45:11 +0000
Subject: [PATCH] Added aggregation example.

---
 transfer/examples/aggregation/Abstract.gf  | 24 ++++++++
 transfer/examples/aggregation/English.gf   | 18 ++++++
 transfer/examples/aggregation/aggregate.tr | 66 ++++++++++++++++++++++
 transfer/examples/aggregation/transfer.txt | 12 ++++
 transfer/examples/aggregation/tree.tr      | 20 +++++++
 transfer/lib/pair.tr                       | 10 ++++
 6 files changed, 150 insertions(+)
 create mode 100644 transfer/examples/aggregation/Abstract.gf
 create mode 100644 transfer/examples/aggregation/English.gf
 create mode 100644 transfer/examples/aggregation/aggregate.tr
 create mode 100644 transfer/examples/aggregation/transfer.txt
 create mode 100644 transfer/examples/aggregation/tree.tr

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 
+}
diff --git a/transfer/lib/pair.tr b/transfer/lib/pair.tr
index 1b70411e8..a4956abdd 100644
--- a/transfer/lib/pair.tr
+++ b/transfer/lib/pair.tr
@@ -9,3 +9,13 @@ fst _ _ p = case p of Pair _ _ x _ -> x
 
 snd : (A:Type) -> (B:Type) -> Pair A B -> B
 snd _ _ p = case p of Pair _ _ x _ -> x
+
+{-
+
+ syntax:
+
+ (x1,...,xn) => { p1 = e1; ... ; pn = en }
+
+ where n >= 2 and x1,...,xn are expressions or patterns
+
+-}
\ No newline at end of file