Donkey: Det and Conj added, as well as negative sentences

4 files changed, 92 insertions, 50 deletions

diff --git a/examples/typetheory/Donkey.gf b/examples/typetheory/Donkey.gf
index 6dd77ba97..6268a7846 100644
--- a/examples/typetheory/Donkey.gf
+++ b/examples/typetheory/Donkey.gf
@@ -4,58 +4,84 @@ flags startcat = S ;
 
 cat 
   S ; 
+  Cl ;
   CN ;
+  Det ;
+  Conj ;
   NP Set ;
   VP Set ;
   V2 Set Set ;
   V  Set ;
   AP Set ;
   PN Set ;
+  RC Set ;
 
 data
-  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 ;
+  IfS     : (A : S) -> (El (iS A) -> S) -> S ;              -- if A B
+  ConjS   : Conj -> S -> S -> S ;                           -- A and B ; A or B
+  PosCl   : Cl -> S ;                                       -- John walks
+  NegCl   : Cl -> S ;                                       -- John doesn't walk
+  PredVP  : ({A} : Set)   -> NP A -> VP A -> Cl ;           -- John (walks / doesn't walk)
+  ComplV2 : ({A,B} : Set) -> V2 A B -> NP B -> VP A ;       -- loves John
+  UseV    : ({A} : Set)   -> V A -> VP A ;                  -- walks
+  UseAP   : ({A} : Set)   -> AP A -> VP A ;                 -- is old
+  DetCN   : Det -> (A : CN) -> NP (iCN A) ;                 -- every man
+  ConjNP  : Conj -> ({A} : Set) -> NP A -> NP A -> NP A ;   -- John and every man
+  The     : (A : CN)   -> El (iCN A) -> NP (iCN A) ;        -- the donkey
+  Pron    : ({A} : CN) -> El (iCN A) -> NP (iCN A) ;        -- he/she/it
+  UsePN   : ({A} : Set) -> PN A -> NP A ;                   -- John
+  ModAP   : (A : CN) -> AP (iCN A) -> CN ;                  -- old man
+  ModRC   : (A : CN) -> RC (iCN A) -> CN ;                  -- man that walks
+  RelVP   : ({A} : CN) -> VP (iCN A) -> RC (iCN A) ;        -- that walks
+  An      : Det ;
+  Every   : Det ; 
+  And     : Conj ;
+  Or      : Conj ;
 
   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) ;
+  Love : ({A,B} : Set) -> V2 A B ; -- polymorphic verb
+  Walk, Talk : V (iCN Man) ;       -- monomorphic verbs
+  Old : ({A} : Set) -> AP A ;      -- polymorphic adjective
+  Pregnant : AP (iCN Woman) ;      -- monomorphic adjective
   John : PN (iCN Man) ;
 
 -- Montague semantics in type theory
 
 fun
-  iS  : S -> Set ;
-  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 ;
+  iS    : S -> Set ;
+  iCl   : Cl -> Set ;
+  iCN   : CN -> Set ;
+  iDet  : Det -> ({A} : Set) -> (El A -> Set) -> Set ;
+  iConj : Conj -> Set -> Set -> 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) ;
+  iRC   : ({A} : Set) -> RC 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)) ;
+  iS (PosCl A) = iCl A ;
+  iS (NegCl A) = Neg (iCl A) ;
+  iS  (IfS A B) = Pi (iS A) (\x -> iS (B x)) ;
+  iS (ConjS C A B) = iConj C (iS A) (iS B) ;
+  iCl (PredVP A Q F) = iNP A Q (\x -> iVP A F 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 _ (DetCN D A) F = iDet D (iCN A) F ;
+  iNP _ (ConjNP C A Q R) F = iConj C (iNP A Q F) (iNP A R 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) ;
+  iDet An A F = Sigma A F ;
+  iDet Every A F = Pi A F ;
+  iCN (ModAP A F) = Sigma (iCN A) (\x -> iAP (iCN A) F x) ;
+  iCN (ModRC A F) = Sigma (iCN A) (\x -> iRC (iCN A) F x) ;
+  iRC _ (RelVP A F) x = iVP (iCN A) F x ;
+  iConj And = Prod ;
+  iConj Or = Plus ;
 
 --- for the type-theoretical lexicon
 
diff --git a/examples/typetheory/DonkeyEng.gf b/examples/typetheory/DonkeyEng.gf
index 927f453ff..51f5c32ca 100644
--- a/examples/typetheory/DonkeyEng.gf
+++ b/examples/typetheory/DonkeyEng.gf
@@ -1,9 +1,12 @@
 --# -path=.:present
 
-concrete DonkeyEng of Donkey = TypesSymb ** open TryEng, IrregEng, Prelude in {
+concrete DonkeyEng of Donkey = TypesSymb ** open TryEng, IrregEng, (E = ExtraEng), Prelude in {
 
 lincat 
   S  = TryEng.S ; 
+  Cl = TryEng.Cl ;
+  Det = TryEng.Det ;
+  Conj = TryEng.Conj ;
   CN = {s : TryEng.CN ; p : TryEng.Pron} ; -- since English CN has no gender
   NP = TryEng.NP ;
   VP = TryEng.VP ;
@@ -11,19 +14,29 @@ lincat
   V2 = TryEng.V2 ;
   V  = TryEng.V ;
   PN = TryEng.PN ; 
+  RC = TryEng.RS ;
 
 lin
-  PredVP _ Q F = mkS (mkCl Q F) ;
+  IfS A B = mkS (mkAdv if_Subj A) (lin S (ss B.s)) ;
+  ConjS C A B = mkS C A B ;
+  PosCl A = mkS A ;
+  NegCl A = mkS negativePol A ;
+  PredVP _ Q F = 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 ;
-  Every A = mkNP every_Det A.s ;
+  An = mkDet a_Quant ;
+  Every = every_Det ;
+  DetCN D A = mkNP D 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} ;
+  ConjNP C _ Q R = mkNP C Q R ;
+  ModAP A F = {s = mkCN F A.s ; p = A.p} ;
+  ModRC A F = {s = mkCN A.s F ; p = A.p} ;
+  RelVP A F = mkRS (mkRCl (relPron A) F) ;
+  And = and_Conj ;
+  Or = or_Conj ;
 
   Man = {s = mkCN (mkN "man" "men") ; p = he_Pron} ;
   Woman = {s = mkCN (mkN "woman" "women") ; p = she_Pron} ;
@@ -37,6 +50,18 @@ lin
   Pregnant = mkAP (mkA "pregnant") ;
   John = mkPN "John" ;
 
+oper
+  relPron : {s : CN ; p : Pron} -> RP = \cn -> case isHuman cn.p of { 
+---    True  => who_RP ;
+---    False => which_RP
+    _ => E.that_RP
+    } ;
+  isHuman : Pron -> Bool = \p -> case p.a of {
+---    AgP3Sg Neutr => False ;
+    _ => True
+    } ;  
+
+
 -- for the lexicon in type theory
 
 lin
diff --git a/examples/typetheory/README b/examples/typetheory/README
index 75a3ee422..7d77e41b7 100644
--- a/examples/typetheory/README
+++ b/examples/typetheory/README
@@ -46,22 +46,13 @@ Example 2: parse and interpret a sentence, also showing the nice formula.
   (Σ v0 : man')(Σ v1 : donkey')own' (v0 , v1)
 
 
-Example 3: (to be revisited) parse of "the donkey sentence" fails, but should succeed
+Example 3: (to be revisited) parse of "the donkey sentence" returns some metavariables
 
-  Donkey> p -cat=S "if a man owns a donkey he beats it"
-
-  The sentence is not complete
- 
-  Donkey> p -cat=S "if a man owns a donkey the man beats the donkey"
-
-  The sentence is not complete
+  Donkey> dc interpret p ?0 | pt -transfer=iS | l -unlexcode
 
+  Donkey> %interpret "if a man owns a donkey he beats it"
 
-Example 4: problem that appears with CN's modified by polymorphic AP's (old), but not with monomorphic ones (pregnant)
+  (Π v0 : (Σ v0 : man')(Σ v1 : donkey')own' (v0 , v1))beat' (?16 , ?22)
+  
 
-  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')
+ 
diff --git a/examples/typetheory/TypesSymb.gf b/examples/typetheory/TypesSymb.gf
index 1c0cc5fae..3ace7e158 100644
--- a/examples/typetheory/TypesSymb.gf
+++ b/examples/typetheory/TypesSymb.gf
@@ -23,7 +23,7 @@ lin
   Plus A B = parenss (infixSS "+" A B) ;
   Pi A B = ss (paren (capPi ++ B.$0 ++ ":" ++ A.s) ++ B.s) ;
   Sigma A B = ss (paren (capSigma ++ B.$0 ++ ":" ++ A.s) ++ B.s) ;
-  Falsum = ss "_|_" ;
+  Falsum = ss "Ø" ;
   Nat = ss "N" ; 
   Id A a b = apply "I" A a b ;