% CATEGORIAL GRAMMAR
% =============================================================================

% Signature
% =============================================================================

bot sub [cat,synsem,syn,sem_obj,list_quant].
  cat sub [] 
      intro [synsem:synsem,
             qstore:list_quant].
  synsem sub [functional, basic].
    functional sub [forward,backward]
               intro [arg:synsem,
                      res:synsem].
      forward sub [].
      backward sub [].
    basic sub [] 
          intro [syn:syn, sem:sem_obj].
  syn sub [np,s,n].
    np sub [].
    s sub [].
    n sub [].
  sem_obj sub [individual, proposition, property].
    individual sub [j,m].
      j sub [].
      m sub [].
    property sub []
             intro [ind:individual,
                    body:proposition].
    proposition sub [logical,quant,run,hit,nominal].
      logical sub [and,or].
        and sub []
            intro [conj1:proposition,
                   conj2:proposition].
        or sub []
           intro [disj1:proposition,
                  disj2:proposition].
      quant sub [every,some]
            intro [var:individual,
                   restr:proposition,
                   scope:proposition].
        every sub [].
        some sub [].
      run sub [] 
          intro [runner:individual].
      hit sub []
          intro [hitter:individual, 
                 hittee:individual].
      nominal sub [kid,toy,big,red] 
              intro [arg1:individual].
        kid sub [].
        toy sub [].
        big sub [].
        red sub [].
  list_quant sub [e_list, ne_list_quant].
    e_list sub [].
    ne_list_quant sub []
                  intro [hd:quant,
                         tl:list_quant].



% Lexicon
% =============================================================================

kid --->
  @ cn(kid).

toy --->
  @ cn(toy).

big --->
  @ adj(big).

red --->
  @ adj(red).

every --->
  @ gdet(every).

some --->
  @ gdet(some).

john --->
  @ pn(j).

runs --->
  @ iv((run,runner:Ind),Ind).

hits --->
  @ tv(hit).


% Empty Categories
% =============================================================================

% empty @ gdet(some).


% Grammar
% =============================================================================

forward_application rule
(synsem:Z,
 qstore:Qs) 
===> 
cat> (synsem:(forward,
              arg:Y,
              res:Z),
      qstore:Qs1),
cat> (synsem:Y,
      qstore:Qs2),
goal> append(Qs1,Qs2,Qs).


backward_application rule
(synsem:Z,
 qstore:Qs)
===> 
cat> (synsem:Y,
      qstore:Qs1),
cat> (synsem:(backward,
              arg:Y,
              res:Z),
      qstore:Qs2),
goal> append(Qs1,Qs2,Qs).


s_quantifier rule
(synsem:(syn:s,
         sem:(Q,
              scope:Phi)),
 qstore:QsRest)
===> 
cat> (synsem:(syn:s,
              sem:Phi),
      qstore:Qs),
goal> select(Qs,Q,QsRest).


% Macros
% ==============================================================================

cn(Pred) macro
  synsem:(syn:n,
          sem:(body:(Pred,
                     arg1:X),
               ind:X)),
  @ quantifier_free.

gdet(Quant) macro
  synsem:(forward,
          arg: @ n(Restr,Ind),
          res: @ np(Ind)),
  qstore:[@ quant(Quant,Ind,Restr)].

quant(Quant,Ind,Restr) macro
  (Quant,
   var:Ind,
   restr:Restr).

adj(Rel) macro
  synsem:(forward,
          arg: @ n(Restr,Ind),
          res: @ n((and,
                    conj1:Restr,
                    conj2:(Rel,
                           arg1:Ind)),
                    Ind)),
  @ quantifier_free.

n(Restr,Ind) macro
  syn:n,
  sem:(body:Restr,
       ind:Ind).

np(Ind) macro
  syn:np,
  sem:Ind.

pn(Name) macro
  synsem: @ np(Name),
  @ quantifier_free.

iv(Sem,Arg) macro
  synsem:(backward,
          arg: @ np(Arg),
          res:(syn:s,
               sem:Sem)),
  @ quantifier_free.

tv(Rel) macro
  synsem:(forward,
          arg:(syn:np,
               sem:Y),
          res:(backward,
               arg:(syn:np,
                    sem:X),
               res:(syn:s,
                    sem:(Rel,
                         hitter:X,
                         hittee:Y)))),
  @ quantifier_free.

quantifier_free macro
  qstore:[].



% Definite Clauses
% ==============================================================================

append([],Xs,Xs) if
  true.
append([X|Xs],Ys,[X|Zs]) if
  append(Xs,Ys,Zs).


select([Q|Qs],Q,Qs) if
  true.
select([Q1|Qs1],Q,[Q1|Qs2]) if
  select(Qs1,Q,Qs2).


