/* QD-Linear Janus implementation.

Authors: Vijay Saraswat
Bugs to: saraswat@parc.xerox.com
Copyright: (C) Xerox Corporation, 1992, 1993.
File: lj9.pl 
Last Modified: Thu May 13 10:20:31 1993


Tue May 11 07:30:09 1993

Introduced tracking of existential quantifiers. Implicitly, the
following rule is used (X^A) ox B ---> X^(A ox B). This is valid
if X does not occur free in B. This is not checked for explicitly
right now, but ensuring that all bound variables (universal or existential) 
are distinct will ensure this (Caveat 3). 

Caveats
(1) Use logical variables in the object-language
  (beginning with an upper-case letter) to represent universally
  bound variables, and constants (begining in a lower-case letter)
  to represent existentially quantified variables.
(2) Ensure that an object-variable is bound exactly once; rename your 
  variables to make this be the case. e.g. (x^A) ox (x^B) should be renamed to
  (x^A) ox (y^B'), where B' is B with y replacing x, for some new variable y.

A lambda-term (lambda x.A) is represented by x\A (as in
Lambda-Prolog).  Application is expressed using the binary infix
@. Thus (x\A)@x beta-reduces to A.

Examples:
?- lj((y^(x:y, x: \Z '-o' Z:Z)), P).

P = y^(y:y,1),
Z = y ? 

yes
| ?-

*/

:- op(975, fx, [ ! ]).         /* Re-use operation. */
:- op(950, xfy, [ -*, @ ]).     /* Linear Asks. */
:- op(150, fx, [ \ ]).	       /* Universal quantifier */
:- op(950, xfy, [ \ ]).	       /* Lambda variable */

:- use_module(library(ordsets)).

lj(Agent) :- lj(Agent, 1).
lj(Agent, Result) :- 
  simplify_agent(Agent, Binders, NormAgent),
  annotate(NormAgent, p(Methods-[], Store-[],  _Ins, _Outs)), 
  lj(Methods, Store,  AnsStore),
  canonicalize_ll(Binders, AnsStore, Result).

lj([], Store, Store).
lj(Methods, Store, AnsStore) :-
  my_mem(X:M -* p(NewM-MTail, NewS-[], _InChans, _OutChans), Methods, MRest),
  match(X, M, Store, SRest), 
  determinate(X, MRest), !,
  normalize(NewS, SRest, NewS1),
  MTail=MRest, 
  lj(NewM, NewS1, AnsStore).

lj(Methods, Store, AnsStore) :-
   my_mem(X:M -* p(NewM-MRest, NewS-SRest, _InChans, _OutChans), Methods, MRest), 
   match(X, M, Store, SRest), 
   lj(NewM, NewS, AnsStore).

my_mem(M, [M | R], R).
my_mem(M, [N | R], [N | S]) :- my_mem(M, R, S).

determinate(_X, []).
determinate(X, [_Y:_M -* p(_, _, _, OutChans) | R]) :-
   ord_disjoint([X], OutChans),
   determinate(X, R).

/* ------------------  Static Analysis ------------------*/

simplify_agent(Agent, Binders, Norm) :-
  simplify(Agent, Binders-[], Norm).

simplify(1, X-X, p(Y-Y, Z-Z)).
simplify(A, X-X, p(Y-Y, [A |Z]-Z)) :- atomic_formula(A), !.
simplify(X^A, [X|Y]-Z, Norm) :- simplify(A, Y-Z, Norm).
simplify((X:M -* A), Binders, p([X:M -* NA | Y]-Y, Z-Z)) :- 
   simplify(A, Binders, NA).
simplify((A,B), H-T, p(Ah-At, Sh-St)) :-
   simplify(A, H-M, p(Ah-Am, Sh-Sm)),
   simplify(B, M-T, p(Am-At, Sm-St)).

atomic_formula(_X:_M).
atomic_formula(X) :- atomic(X).

annotate(p(Methods-[], Store-STail), p(Methods1, Store-STail, InChans, OutChans)) :-
  annotate_type(Methods, Methods1, [], InChans, [], Out),
  add_outs(Store, STail, Out, OutChans).

add_outs(Head, Tail, Out, Out) :- Head == Tail, !.
add_outs([X:_M | Rest], Tail, Out_in, Out) :-
  ord_add_element(Out_in, X, Out1),
  add_outs(Rest, Tail, Out1, Out).

annotate_type([], Tail-Tail, In, In, Out, Out).
annotate_type([X:M -* A | R],  [X:M -* AA | R1]-Tail, InChans_in, InChans, OutChans_in, OutChans) :-
   annotate(A, AA),  AA = p(_, _, In1, Out1),
   ord_union(In1, InChans_in, In2), ord_add_element(In2, X, In3),
   ord_union(Out1, OutChans_in, Out2),
   annotate_type(R, R1-Tail, In3, InChans, Out2, OutChans).

/* ------------- ``Run-time system'' -------------------
normalize(T, S) :-
   normalize T (through beta-reductions) to get S.
*/

normalize([], S, S).
normalize([T | R], U, [S | A]) :- normalize(T, S), normalize(R, U, A).

normalize(T, S) :- (var(T) ; atomic(T)), !, S=T.
normalize((L\Term)@Arg, Result) :- !,
      new(Term, Value, L, Arg),
      normalize(Value, Result).
normalize(Term, Result) :- map_tree(normalize, Term, Result).

/* canonicalize_ll(Binders, Form1, Form) :-
   Canonicalize the formula Binders^Form1, by removing any 
   variable in Binders that does not occur in Form1.
*/

canonicalize_ll([], Form, Form).
canonicalize_ll([X | Binders], Form1, Form) :-
    occurs_in(Form1, X) 
         -> canonicalize_ll(Binders, X^Form1, Form)
         ; canonicalize_ll(Binders, Form1, Form).

occurs_in(Form, X) :- occurs_in(Form, [X|_]-[], X). 
occurs_in(Form1, R-S, X) :- 
   (var(Form1); atomic(Form1)), !, 
    (X == Form1 -> R=[X | S] ; R=S).
occurs_in(Term, R-S, X) :- eval_tree(occurs_in, Term, R-S, [X]).

/*
Brief Description:
 Find a message in the store matching a given template. 
 Pattern variables are represented as logical variables.
 Generate and test is used to find a match. The first match found is
 returned.
*/

match_all(X:M, Store, Result) :- !, match(X, M, Store, Result).
match_all((A, B), Store, Result) :- !, 
  match_all(A, Store, Store1),
  match_all(B, Store1, Result).

match(X, M, Store, Store1) :- member(X:R, Store, Store1), match(M, R), !.

member(X:R, [Y:T | Store], Store1) :- X==Y, !, R=T, Store1=Store.
member(X:R, [Item | Store], [Item | Store1]) :- member(X:R, Store, Store1).

/* VJ Sun May  2 22:51:00 1993

  The second clause below cheats. What needs to be done is an enumeration
  of all the most general matchers. We cheat in that 
  (1) we generate only the mgu in which all occurrences of Var are 
      lambda-bound
  (2) we do not give the entry for match corresponding to the case in which
      the lambda-term is applied to something that is not a variables.

  Fernando, you should add some kind of higher-order matching routine here.

*/

match(\Term, Term):- !.
match((\Lambda @ Var), Term):- (var(Var) ; atomic(Var)), !, Lambda = (Var\Term).
match(Template, Term) :- map_tree(match, Template, Term).

/* map_tree(Transformer, Term, Value, Args) :-
    Value is the tree obtained from Term by 
    applying Transformer with the extra args Args
    on every sub-tree of Term.
*/

map_tree(Transformer, Term, Value) :- 
  map_tree(Transformer, Term, Value, []).

map_tree(Transformer, Term, Value, Arg) :-
   functor(Term, F, A),
   functor(Value, F, A),
   map_each(0, A, Transformer, Term, Value, Arg).

map_each(M, N, Trans, Term, Value, Args):- 
   M = N 
      -> true
      ; 
       ( M1 is M+1,
         arg(M1, Term, Term_M1),
         arg(M1, Value, Value_M1),  
         funcall(Trans, [Term_M1, Value_M1 | Args]),
         map_each(M1, N, Trans, Term, Value, Args)
       ).

funcall(Proc, Args) :- Agent =.. [Proc | Args],  call(Agent).

/* eval_tree(+Pred, +Tree, ?Result, +Args) :-
    Apply Pred to each sub-tree of Tree, passing a D-list and
    Args to each call; the concatentation of the D-lists is Result.

*/

eval_tree(Pred, Tree, Result, Args) :-
   functor(Tree, _F, A),
   eval_each(0, A, Pred, Tree, Result, Args).

eval_each(M, N, Pred, Term, X-Z, Args):- 
   M = N 
      -> Z=X
      ; ( M1 is M+1,
         arg(M1, Term, Term_M1),
         funcall(Pred, [Term_M1, X-Y | Args]),
         eval_each(M1, N, Pred, Term, Y-Z, Args)
       ).


/* new(Term, Term1, X, Y) :-
 Term1 is Term with all free occurrences of
 X replaced by Y. Note that Term may have the binders ^ and \. */

new(Z, R, X, Y):- (var(Z) ; atom(Z)), !, (Z==X -> R=Y ; R=Z).

new((Z : M -* A), (Z1 : M1 -*  A1), X, Y):- !,
    new(Z, Z1, X, Y),
    new(M, M1, X, Y, Bound),
    (Bound == bound 
        -> A1 = A ;
           new(A, A1, X, Y)).
new(Z^A, R, X, _Y):- X == Z, !, R=Z^A.
new(Z^A, Z^A1, X, Y):-  !, new(A, A1, X, Y).
new(Term, Term1, X, Y) :- map_tree(new, Term, Term1, [X, Y]).

