% Instant Glue
% Version 1.4
% Author: Miltiadis Kokkonidis
% Date: 9 June 2009
%
% (c) 2009 Miltiadis Kokkonidis
%
% Supported by Social Sciences and Humanities Research Council of Canada, 
% Standard Research Grant #410-2006-1650 to Ash Asudeh.
%
% Licence Agreement:
%
% Permission is granted to use and distribute this code as is.  Any code derived
% from the code herein must be publically available in source code form, be
% available free of charge, and carry the same licence and disclaimer.  It
% should both clearly acknowledge the current work, as well as provide a
% reasonably clear statement of the ways in which the derived work differs from
% the original work.  While the acknowledgements section may differ, mention
% should be made to both the AHRC (UK) and the SSHRC (Canada) grants that
% made the development of this software possible.  Licence to use this software
% is conditional upon acceptance of the disclaimer below.
%
% Disclaimer:
%
% This software comes as-is with no warranties of any kind, express or implied.
% The user assumes full responsibility for its use and is solely liable for
% resulting damages, if any.
%
% Versions and acknowledgesments:
%
% Versions 1.0, 1.1 and 1.2 were developed during the course of the author's
% DPhil studies at the University of Oxford supported by AHRC grant 2005/118667.
% The author wishes to thank his thesis advisor, Mary Dalrymple, for her
% support, as well as Maya Bangerter and Simon Clematide, for developing tools
% for Instant Glue.
%
%
% Version 1.4 is the first publically available version of Instant Glue.  Unlike
% earlier versions it supports not only linear implication, but also the
% tensor.  As a result, it is the first version of Instant Glue that directly
% supports analyses involving products such as the basic Glue analysis of
% anaphora and the Glue analysis of resumption. Work towards versions 1.3 and
% 1.4 was supported by  the Social Sciences and Humanities Research Council of
% Canada, Grant #410-2006-1650.  The author wishes to thank Ash Asudeh, the
% grant's Principal Investigator, for encouraging and funding this project.


:- op(598, yfx, user:( @ )).
:- op(599, xfy, user:( -> )).
:- op(649, xfx, user:( =- )).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

identmember(X, [Y|YS]) :- X == Y ; identmember(X, YS).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

appl(F,[], F).
appl(F,[X|XS], FE ) :- appl(F@X, XS, FE).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

endsIn(T,       T, [],     SG - SG).
endsIn(T, S -> TT, [E|ES], SG - EG) :- endsIn(T, TT, ES, SG - IG),
                                      g(IG - EG =-  E: S).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

g( SG-EG =- E:T ) :-
   select(P:(T1*T2), SG, IG),
   g( [fst(P):T1, snd(P):T2 | IG] - EG =- E:T ), !.

g( SG-EG =- lambda(var(X),E) : T->S ) :-  %!,
   g( [var(X):T|SG]-EG =- E: S ),
   not(identmember(var(X):T, EG)).

g( SG-EG =- E: T ) :-
   T \= _ -> _,    T \= _*_,
   select(A:S, SG, IG),
   endsIn(T, S, Args, IG - EG),
   appl(A, Args, E).

g( SG-EG =- let([ (var(X1), var(X2)) = EP ], E):T ) :-
   T \= _ -> _,
   select(A:S, SG, IG1),
   endsIn(T1*T2, S, Args, IG1 - IG2),
   appl(A, Args, EP),
   g([var(X1):T1,var(X2):T2 | IG2]-EG =- E:T).

g( SG-EG =- (A1,A2) : T1 * T2 ) :-
   g( SG-IG =- A1:T1),
   g( IG-EG =- A2:T2).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

glue( G =- M:T ) :-  g( G - [] =- M:T ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

readings(M,J) :-
   writeln('Judgement'),writeln(J),
   writeln('Readings:'), J, writeln(M), fail; true.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

example :-
   readings(M,
     glue([every:(e(s)->t(s))->(e(s)->t(A))->t(A),
           rep:e(r) -> (e(s)->t(s)),
           a1:(e(r)->t(r))->(e(r)->t(B))->t(B),
           firm: e(r)->t(r),
           take: e(s)->e(o)->t(f),
           a2:(e(o)->t(o))->(e(o)->t(C))->t(C),
           sample:e(o)->t(o)] =- M:t(f))).