From 35b92c51097059f6e76dd258eaeb4697a71b53ae Mon Sep 17 00:00:00 2001
From: aarne <aarne@chalmers.se>
Date: Wed, 14 Sep 2011 09:29:56 +0000
Subject: [PATCH] Donkey: added AP, reported problem with ModCN and polymorphic
 AP's

---
 examples/typetheory/Donkey.gf    | 33 +++++++++++++++++++++++++++-----
 examples/typetheory/DonkeyEng.gf | 20 +++++++++++++++++--
 examples/typetheory/README       |  9 +++++++++
 3 files changed, 55 insertions(+), 7 deletions(-)

diff --git a/examples/typetheory/Donkey.gf b/examples/typetheory/Donkey.gf
index 5be8b526c..6dd77ba97 100644
--- a/examples/typetheory/Donkey.gf
+++ b/examples/typetheory/Donkey.gf
@@ -9,19 +9,29 @@ cat
   VP Set ;
   V2 Set Set ;
   V  Set ;
+  AP Set ;
+  PN Set ;
 
 data
-  PredVP  : ({A} : Set) -> NP A -> VP A -> S ;
+  PredVP  : ({A} : Set)   -> NP A -> VP A -> S ;
   ComplV2 : ({A,B} : Set) -> V2 A B -> NP B -> VP A ;
   UseV    : ({A} : Set)   -> V A -> VP A ;
+  UseAP   : ({A} : Set)   -> AP A -> VP A ;
   If      : (A : S) -> (El (iS A) -> S) -> S ;
   An      : (A : CN) -> NP (iCN A) ;
+  Every   : (A : CN) -> NP (iCN A) ;
   The     : (A : CN)   -> El (iCN A) -> NP (iCN A) ;
   Pron    : ({A} : CN) -> El (iCN A) -> NP (iCN A) ;
+  UsePN   : ({A} : Set) -> PN A -> NP A ;
+  ModCN   : (A : CN) -> AP (iCN A) -> CN ;
 
-  Man, Donkey : CN ;
+  Man, Donkey, Woman : CN ;
   Own, Beat : V2 (iCN Man) (iCN Donkey) ;
+  Love : ({A,B} : Set) -> V2 A B ;
   Walk, Talk : V (iCN Man) ;
+  Old : ({A} : Set) -> AP A ;
+  Pregnant : AP (iCN Woman) ;
+  John : PN (iCN Man) ;
 
 -- Montague semantics in type theory
 
@@ -30,31 +40,44 @@ fun
   iCN : CN -> Set ;
   iNP : ({A} : Set) -> NP A -> (El A -> Set) -> Set ;
   iVP : ({A} : Set) -> VP A -> (El A -> Set) ;
+  iAP : ({A} : Set) -> AP A -> (El A -> Set) ;
   iV  : ({A} : Set) -> V A -> (El A -> Set) ;
   iV2 : ({A,B} : Set) -> V2 A B -> (El A -> El B -> Set) ;
+  iPN : ({A} : Set) -> PN A -> El A ;
 def
   iS  (PredVP A Q F) = iNP A Q (\x -> iVP A F x) ;
   iS  (If A B) = Pi (iS A) (\x -> iS (B x)) ;
   iVP _ (ComplV2 A B F R) x = iNP B R (\y -> iV2 A B F x y) ;
   iVP _ (UseV A F) x = iV A F x ;
+  iVP _ (UseAP A F) x = iAP A F x ;
   iNP _ (An A) F = Sigma (iCN A) F ;
+  iNP _ (Every A) F = Pi (iCN A) F ;
   iNP _ (Pron _ x) F = F x ;
   iNP _ (The _ x) F = F x ;
-
+  iNP _ (UsePN A a) F = F (iPN A a) ;
+  iCN (ModCN A F) = Sigma (iCN A) (\x -> iAP (iCN A) F x) ;
 
 --- for the type-theoretical lexicon
 
 data
-  Man', Donkey' : Set ;
+  Man', Donkey', Woman' : Set ;
   Own', Beat' : El Man' -> El Donkey' -> Set ;
+  Love' : ({A,B} : Set) -> El A -> El B -> Set ;
+  Old' : ({A} : Set) -> El A -> Set ;
   Walk', Talk' : El Man' -> Set ;
-
+  Pregnant' : El Woman' -> Set ;
+  John' : El Man' ;
 def
   iCN Man = Man' ;
+  iCN Woman = Woman' ;
   iCN Donkey = Donkey' ;
   iV2 _ _ Beat = Beat' ;
   iV2 _ _ Own = Own' ;
+  iV2 _ _ (Love A B) = Love' A B ;
   iV _ Walk = Walk' ;
   iV _ Talk = Talk' ;
+  iAP _ (Old A) = Old' A ;
+  iAP _ Pregnant = Pregnant' ;
+  iPN _ John = John' ;
 
 }
\ No newline at end of file
diff --git a/examples/typetheory/DonkeyEng.gf b/examples/typetheory/DonkeyEng.gf
index 524f8e880..927f453ff 100644
--- a/examples/typetheory/DonkeyEng.gf
+++ b/examples/typetheory/DonkeyEng.gf
@@ -7,33 +7,49 @@ lincat
   CN = {s : TryEng.CN ; p : TryEng.Pron} ; -- since English CN has no gender
   NP = TryEng.NP ;
   VP = TryEng.VP ;
+  AP = TryEng.AP ;
   V2 = TryEng.V2 ;
   V  = TryEng.V ;
+  PN = TryEng.PN ; 
 
 lin
   PredVP _ Q F = mkS (mkCl Q F) ;
   ComplV2 _ _ F y = mkVP F y ;
   UseV _ F = mkVP F ;
+  UseAP _ F = mkVP F ;
   If A B = mkS (mkAdv if_Subj A) (lin S (ss B.s)) ;
   An A = mkNP a_Det A.s ;
-  The A _ = mkNP the_Det A.s ;
-  Pron A _ = mkNP A.p ;
+  Every A = mkNP every_Det A.s ;
+  The A r = mkNP the_Det A.s | mkNP (mkNP the_Det A.s) (lin Adv (parenss r)) ; -- variant showing referent: he ( john' )
+  Pron A r = mkNP A.p | mkNP (mkNP A.p) (lin Adv (parenss r)) ;
+  UsePN _ a = mkNP a ;
+  ModCN A F = {s = mkCN F A.s ; p = A.p} ;
 
   Man = {s = mkCN (mkN "man" "men") ; p = he_Pron} ;
+  Woman = {s = mkCN (mkN "woman" "women") ; p = she_Pron} ;
   Donkey = {s = mkCN (mkN "donkey") ; p = it_Pron} ;
   Own = mkV2 "own" ;
   Beat = mkV2 beat_V ;
+  Love _ _ = mkV2 "love" ;
   Walk = mkV "walk" ;
   Talk = mkV "talk" ;
+  Old _ = mkAP (mkA "old") ;
+  Pregnant = mkAP (mkA "pregnant") ;
+  John = mkPN "John" ;
 
 -- for the lexicon in type theory
 
 lin
   Man' = ss "man'" ;
+  Woman' = ss "woman'" ;
   Donkey' = ss "donkey'" ;
   Own' = apply "own'" ;
   Beat' = apply "beat'" ;
+  Love' _ _ = apply "love'" ;
   Walk' = apply "walk'" ;
   Talk' = apply "talk'" ;
+  Old' _ = apply "old'" ; 
+  Pregnant' = apply "pregnant'" ; 
+  John' = ss "john'" ;
 
 }
\ No newline at end of file
diff --git a/examples/typetheory/README b/examples/typetheory/README
index 61ac296ed..75a3ee422 100644
--- a/examples/typetheory/README
+++ b/examples/typetheory/README
@@ -56,3 +56,12 @@ Example 3: (to be revisited) parse of "the donkey sentence" fails, but should su
 
   The sentence is not complete
 
+
+Example 4: problem that appears with CN's modified by polymorphic AP's (old), but not with monomorphic ones (pregnant)
+
+  Donkey> p "an old man walks"
+  src/runtime/haskell/PGF/TypeCheck.hs:(528,4)-(550,67): Non-exhaustive patterns in function occurCheck
+  -- this should build (ModCN Man (Old Man'))
+
+  Donkey> p "a pregnant woman loves John " | pt -transfer=iS | l -unlexcode
+  (Σ v0 : (Σ v0 : woman')pregnant' (v0))love' (v0 , john')