/* QD-Linear Janus implementation.
Authors: Vijay Saraswat
Bugs to: saraswat@parc.xerox.com
Copyright: (C) Xerox Corporation, 1992.
File: lj5.pl 
Last Modified: Sun Apr 11 21:10:56 1993

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

lj(Agent) :- lj(Agent, 1).
lj(Agent, Result) :- lj(Agent, Result, 1).
lj(Agent, AnsStore, Ans) :- lj(Agent, 1, AnsStore, Ans).

lj(Agent, Store, AnsStore, Ans) :- 
  lj(Agent, Store, AnsStore1, Ans1-1, Flag),
  (Flag == nodeadlock 
       -> lj(Ans1, AnsStore1, AnsStore, Ans)
         ; (AnsStore=AnsStore1, Ans=Ans1)).

lj(1, Store, Store, Q-Q, _Flag).
lj(X:T, Store, (X:T, Store), Q-Q, nodeadlock).
lj((A,B), Store, AnsStore, Ans-Tail, Flag) :-
   lj(A, Store,  Store1, Ans-Mid, Flag),
   lj(B, Store1, AnsStore, Mid-Tail, Flag).

lj((X:M '-o' A), Store, AnsStore, Ans-Tail, nodeadlock) :-
   match(X, M, Store, Store1),
   lj(A, Store1,  AnsStore, Ans-Tail, _Flag).

lj((X:M '-o' A), Store, Store, ((X:M '-o' A), Tail)-Tail, _Flag).


lj(! Clause, Store, AnsStore, (!Clause, Ans) - Tail,  nodeadlock) :-
   copy(Clause, X:M '-o' A),
   match(X, M, Store, Store1),
   lj(A, Store1, AnsStore, Ans -Tail, _Flag).

lj(! Clause, Store, Store, (!Clause, Ans) - Ans,  _Flag).

/*
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.

Things to do:

*/
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).

match(\Term, 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)
       ).

/*
Brief Description:
  Provides procedures for making copies of agents,
  with new variables substituted in.

Exports:
   copy/2
   new/{3,4}

*/

/* copy(Clause, NewClause) :-
   NewClause is a copy of Clause in which all \-bound variables in Clause 
   appearing outside a ! are replaced with brand-new variables.
*/

copy(X:M '-o' A, X:M1 '-o' A2):- !,
   lambda_vars(M, Vars),
   special_new(Vars, M, M1),
   new(Vars,  A, A1),
   copy(A1, A2).

copy(1, 1).
copy((X:T), (X:T)).
copy((A1,A2), (B1, B2)):- copy(A1, B1), copy(A2, B2).
copy(!A, !A).

/* 
lambda_vars(T, Z) :-
   Z is a d-list of X=_NewX pairs of all the  lambda-variables
   X in T.
*/

lambda_vars(X, Y-Y):- (var(X) ; atom(X)), !.
lambda_vars(\X, [X=_NewX |Y]-Y):- !.
lambda_vars(Term, List) :- eval_tree(lambda_vars, Term, List, []).

/* new(Subst, Term, Result) :-
   Apply each of the renamings in Subst to Term to get Result. */

new([], A, A).
new([X=Y | Rest], A, Res) :-
   new(A, A1, X, Y), 
   new(Rest, A1, Res).


/* 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 '-o' A), (Z1 : M1 '-o' 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]).

/* new(Term, NewTerm, X, Y, Bound) :-
   Replace free occurrences of X in Term with Y to give NewTerm, 
   and equate Bound to bound if \X occurs in Term.
*/

new(Z, R, X, Y, _Bound):- (var(Z) ; atom(Z)), !, (Z==X -> R=Y ; R=Z).
new(\Z, \Z, X, _Y, Bound) :-  !, (X == Z -> Bound=bound ; true).
new(Term, Term1, X, Y, Bound) :- map_tree(new, Term, Term1, [X, Y, Bound]).


/* special_new/4 is just like new/5 without the Bound argument (see below), 
   except that it replaces \X with \Y, if X is to be replaced by Y. */

special_new([], M, M).
special_new([X=Y | Rest], M, Res) :-
   special_new(M, M1, X, Y),
   special_new(Rest, M1, Res).

special_new(Z, R, X, Y):- (var(Z) ; atom(Z)), !, (Z==X -> R=Y ; R=Z).
special_new(Z, R, X, Y) :- map_tree(special_new, Z, R, [X, Y]).

/* translate_pat(Subst, M, M1) :-
     Replace all occurrences of \X in M with Y to get M1 
     if Subst says that X should be mapped to Y. 
*/
translate_pat(Subst, M, M1) :- translate_pat_2(Subst, M, M1).
translate_pat(Subst, M, M1, M2) :- 
   translate_pat_1(Subst, M, M1),
   translate_pat_2(Subst, M, M2).

translate_pat_1([], M, M).
translate_pat_1([X=Y | Rest], M, Res) :-
   translate_pat_1(M, M1, X, Y),
   translate_pat_1(Rest, M1, Res).

translate_pat_1(Z, R, X, Y):- (var(Z) ; atom(Z)), !, (Z==X -> R=Y ; R=Z).
translate_pat_1(\Z, R, X, Y) :-  !, (X == Z -> R=Y ; R= (\Z)).
translate_pat_1(Z, R, X, Y) :- map_tree(translate_pat_1, Z, R, [X, Y]).


translate_pat_2([], M, M).
translate_pat_2([X=Y | Rest], M, Res) :-
   translate_pat_2(M, M1, X, Y),
   translate_pat_2(Rest, M1, Res).

translate_pat_2(Z, R, X, Y):- (var(Z) ; atom(Z)), !, (Z==X -> R=Y ; R=Z).
translate_pat_2(\Z, \R, X, Y) :-  !, (X == Z -> R=Y ; R= Z).
translate_pat_2(Z, R, X, Y) :- map_tree(translate_pat_2, Z, R, [X, Y]).


