; Analysis by Chung-chieh (Ken) Shan and Chris Barker.
; Reference grammar for Shan and Barker, Explaining crossover and superiority 
; as left to right evaluation, to appear in Linguistics and Philosophy.
; 2002-2005.

; Type-shifters without quotes (e.g., L,U,D,S) are posited automatically.
; Type-shifters in quotes (e.g., "B", "_") need to be explicitly inserted. 
; Removing quotes works, but slows down the parser.

; Uncomment Z to get right-to-left parsing (see section 7).

(set! grammar
  `(
    ((L ((2 / (1 \ 2)) / 1)) (^ x (^ f (f x))))       
    ((U ((2 // (1 \\ 2)) / 1)) (^ x (^ f (f x))))
    ((D (1 / (1 // (t \\ t)))) (^ k (k (^ x x))))
    ((S (((4 // (2 \\ 5)) / (3 // (1 \\ 5))) / (4 // ((2 / 1) \\ 3))))
     (^ L (^ R (^ c (L (^ l (R (^ r (c (l r))))))))))
;    ((Z (((5 // (2 \\ 3)) / (5 // (1 \\ 4))) / (4 // ((2 / 1) \\ 3))))
;     (^ L (^ R (^ c (R (^ r (L (^ l (c (l r))))))))))

    (("B" ((1 // (e \\ (e > 2))) / (1 // (e \\ 2))))
     (^ c (^ d (c (^ x ((d x) x))))))

    (("_" ((e \\ 1) // (e \\ 1))) (^ k k))
    (("_r" ((((e > t) // (e \\ t)) \\ t) // (((e > t) // (e \\ t)) \\ t)))
     (^ k k))
;    (("_r" (((2 // (e \\ 1)) \\ 3) // ((2 // (e \\ 1)) \\ 3))) (^ k k))
    ((Q (((e ? 1) / 2) / ((e ? 1) // 2))) (^ k k))

    (("everyone" (t // (e \\ t))) (^ k (forall x (k x)))) 
    (("someone" (t // (e \\ t))) (^ k (exists x (k x)))) 

    (("he" ((e > 1) // (e \\ 1))) (^ k k))
    (("him" ((e > 1) // (e \\ 1))) (^ k k))
    (("his" ((e > 1) // (e \\ 1))) (^ k k))

    (("who" ((e ? 1) // (e \\ 1))) (^ k k))
    (("what" ((e ? 1) // (e \\ 1))) (^ k k))
    (("whose" ((e ? 1) // (e \\ 1))) (^ k k))

    (("which-students" ((e \\ (e ? 1)) // (e \\ (e \\ 1))))
     (^ c (^ trace (which-students (^ x ((c x) trace))))))

    (("john" e) j)
    (("mary" e) m)
    (("mother" (e \ e)) mother)
    (("friend" (e \ e)) friend)
    (("birthday" (e \ e)) birthday)
    (("left" (e \ t)) left)
    (("saw" ((e \ t) / e)) saw)
    (("bought" ((e \ t) / e)) bought)
    (("buy" ((e \ t) / e)) buy)
    (("resent" ((e \ t) / e)) resent)
    (("call" ((e \ t) / e)) call)
    (("phoned" ((e \ t) / e)) phoned)
    (("give" (((e \ t) / e) / e)) give)
    (("thought" ((e \ t) / t)) thought)
    (("did" (t / t)) (^ p p))
    (("on" (((e \ t) \ (e \ t)) / e)) on)
    (("criticism-of" ((e \ e) / e)) criticism-of)
))    

(set! filter-cats '(t))

;(set! display-derivation? #t)
(set! display-derivation? #f)

;(parse '(mary saw john))

;(parse '(john saw everyone))
;(parse '(john mother left))
;(parse '(everyone mother left))
(parse '(someone saw everyone))
;(check '(U "everyone"))
;(check '((S (U U)) "everyone"))

; "if the underlined (S (U U)) were replaced with just U..."
;(check '(D ((S (U D)) ((S (U (S ((S (U L)) "someone")))) ((S (U U)) ((S (U "saw")) "everyone"))))))
;(check '(D ((S (U D)) ((S (U (S ((S (U L)) "someone")))) (U ((S (U "saw")) "everyone"))))))
; "indeed, ..., we can get as far as applying Down once..."
;(check '((S (U D)) ((S(U(S((S(U L))((S((S(U L))"his"))(U "mother"))))))((S(U U))((S(U "saw"))("B" "everyone"))))))
; "we can apply Down once here, resulting in the category..."
;(check '((S (U D)) ((S (U (S (U "did")))) ((S (U (S (U (L "mary"))))) ((S (U (S ((S (U "give")) "who")))) ((S (U U)) "_"))))))

(set! filter-cats '(t (e > 1)))
;(parse '(he left))
;(parse '(john saw him))
;(parse '(everyone saw him))
;(parse '(john thought he left))

;(check '("B" "everyone"))

;(parse '(B everyone thought he left))
;(parse '(B everyone mother thought he left))
;(parse '(everyone thought he left))
;(parse '(he saw him))

(set! filter-cats '(t (e ? 2)))
;(parse '(who left))
;(parse '(who bought what))
;(parse '(whose mother left))

;(parse '(who _ left))
;(parse '(what did mary buy _))
;(parse '(who did mary give _ what))
;(parse '(what who did mary say _ bought _))

(set! max-edges 1000)
;(parse '(B everyone saw his mother))
;(parse '(his mother saw B everyone)) ; works with Z
;(parse '(mary phoned B everyone on his birthday))
;(parse '(mary phoned his mother on B everyone birthday)) ; works with Z

;(parse '(who did mary give _ what))
;(parse '(what did mary give who _))  ; works with Z
;(parse '(what did who buy _))

;(parse '(what did which-students buy _))

;(check '("B" "_"))
;(parse '(who B _ saw his mother))
;(parse '(B who _ saw his mother))

;(parse '(B whose friend _ saw his mother))
;(parse '(B who did mary call _ on his birthday))
;(parse '(who did mary call B _ on his birthday))

(set! max-depth 7)
(set! max-edges 1200)
(set! display-derivation? #t)
;(parse '(whose criticism-of his mother did B everyone resent _r))

; To see the reversal in order of evaluation, uncomment Z above