/* QD-Linear Janus implementation.

Authors: Vijay Saraswat
Bugs to: saraswat@parc.xerox.com
Copyright: (C) Xerox Corporation, 1992, 1993.
File: lj6.pl 
Last Modified: Sun May  2 21:52:26 1993

Gurantees that the final configuration is stable, that is, no method can 
fire in it.

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) I don't have !-formulas working correctly right now. (I
  need to make sure that existential and universal bound variables
  are renamed.)
(2) 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.
(3) 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, [ '-o', @ ]).     /* Linear Asks. */
:- op(150, fx, [ \ ]).	       /* Universal quantifier */
:- op(950, xfy, [ \ ]).	       /* Lambda variable */

lj(Agent) :- lj(Agent, 1).
lj(Agent, Result) :- lj(Agent, Result, 1).
lj(Agent, AnsStore, Ans) :- 
  lj(Agent, 1, AnsStore1, [], Binders, Ans1),
  canonicalize_ll(Binders, AnsStore1, AnsStore),
  canonicalize_ll(Binders, Ans1, Ans).

lj(Agent, Store, AnsStore, BindersIn, BindersOut, Ans) :- 
  lj(Agent, Store, AnsStore1, Ans1-1, BindersIn, Binders, Flag),
  (Flag == continue 
       -> lj(Ans1, AnsStore1, AnsStore, Binders, BindersOut, Ans)
         ; (stable(Ans1, AnsStore1)
             -> (AnsStore=AnsStore1, Ans=Ans1, Binders=BindersOut))).

lj(1, Store, Store, Q-Q, Binders, Binders, _Flag).
lj(X:T, Store, (X:T1, Store), H-H, Binders, Binders, continue) :- normalize(T, T1).

lj(Y^(Agent), Store, AnsStore, Agents, BindersIn, BindersOut, continue) :-
  lj(Agent, Store, AnsStore, Agents, [Y | BindersIn], BindersOut, _Flag).

lj((X:M '-o' A), Store, AnsStore, Agents, BindersIn, BindersOut, continue) :-
   match(X, M, Store, Store1),
   lj(A, Store1,  AnsStore, Agents, BindersIn, BindersOut, _Flag).

lj(((A '-o' B) '-o' C), Store, AnsStore, Agents, BindersIn, BindersOut, continue) :-
  lj((A, Agents),  Store, AnsStore1, BindersIn, BindersTemp, Ans),
  match_all(B, AnsStore1, RemStore),
  lj((C, Ans), RemStore,  AnsStore, Agents, BindersTemp, BindersOut, _Flag).

lj((A '-o' B), Store, Store, ((A '-o' B), Tail)-Tail, Binders, Binders, _Flag).
lj((A,B), Store, AnsStore, AgentsH-AgentsT, BindersIn, BindersOut, Flag) :- !,
  lj(A, Store, Store1, AgentsH-AgentsM, BindersIn, Binders1, Flag),
  lj(B, Store1, AnsStore, AgentsM-AgentsT, Binders1, BindersOut, Flag).

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

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

%  lj(((A,B),C), Store, AnsStore, Agents, Flag) :- !,
%    lj((A, (B,C)), Store, AnsStore, Agents, Flag).


/* stable(Methods, Messages) :-
   No Method can fire for the  given Messages.
*/

stable(1, _).
stable((M, A), Store) :- stable_method(M, Store), stable(A, Store).

stable_method(!(X:M '-o' _A), Store) :-  match(X, M, Store, _Store1), !, fail.
stable_method( (X:M '-o' _A), Store) :-  match(X, M, Store, _Store1), !, fail.
stable_method(_A, _B).

/* normalize(T, S) :-
   normalize T (through beta-reductions) to get S.
*/

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


/* 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.
Tue May 11 06:01:09 1993
  [Actually, I need to replace all universally quantified and existentially
   quantified variables as well.]
*/

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]).


