/* QD-Linear Janus implementation.
Authors: Vijay Saraswat, Clifford Tse
Bugs to: {saraswat,tse}@parc.xerox.com
Copyright: (C) Xerox Corporation, 1992.
File: lj3.pl 
Last Modified: Sat Feb 22 11:26:09 1992

Brief Description:
  Top-level loop. 

Files in this module:
   Files: {lj3,match,eval,new,ops,map}.pl, 

Exports:
   lj/{3,4}

Things to do:
1. Avoid the search for a message. That is, record the message on the 
   variable itself, as well as all the processes suspended on the variable.

2. LJ variables can be (and should be) Prolog constants. 

3. In fact, an explicit substitution operator is needed, which 
   makes sure to alpha-rename existential constructs to avoid spurious 
   capture. We cannot represent \-variables as Prolog variables, and 
   bind these to the actual values, since this can lead to spurious
   capture, e.g.
          x:\m -o n^b:(m,n),
          x:n
   To fix this, the top-level query should go through the agent input,
   and replace all LJ existential variables with brand-new Prolog variables.
   Also, copy should make sure that existenial variables are replaced with
   brand-new existential variables.

   In fact, ! agents are semantically equivalent to agents of the syntactic
   form:
        ! X:M -o X1^X2^...Xk^ AX
   where A is built up from the productions
       AX ::=  Y:t | Y:t -o AX | AX, AX | !Y:t -o A 
   (A is any arbitrary agent.)
   That is, the only existentials occurring in AX are protected under
   an !.  The AX-normal form of an agent A is obtained by basically identifying
   all the existential variables in A occurring in a sub-term not protected by
   !, and moving them to the ``top-level'', using the following semantic
   equivalences:
             B, X^A = X^(B,A)    provided that X is not free in B
             X^A = Y^(A[Y/X])    where Y is free for X in A

4. Fix the Prolog-reader (rdtok.pl) so that -o is parsed as a symbol 
   (this has been done). Use myread/{1,2} instead of read/{1,2} to get 
   terms from a Linear Janus source file so that -o is parsed as a symbol.

5. Adapt the top-level interface of QD-Janus to this implementation. 
   (See janus.pl.)

6. Develop a compilation algorithm, which inputs an LJ file and produces
   basically Prolog code. 

*/
:- ensure_loaded([ops,match,eval,map,new]).

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:T1, Store), Q-Q, nodeadlock) :-  eval(T, T1).
lj((A,B), Store, AnsStore, Ans-Tail, Flag) :-
   lj(A, Store,  Store1, Ans-Mid, Flag),
   lj(B, Store1, AnsStore, Mid-Tail, Flag).

lj(X^A, Store, AnsStore, Ans, nodeadlock) :-
   new(X, _NewX, A, A1), 
   lj(A1, Store, AnsStore, Ans, _Flag).

lj((C -> A), Store, AnsStore, Ans-Tail, nodeadlock) :-
   ask(C) 
    -> lj(A, Store, AnsStore, Ans-Tail, _Flag)
      ; (AnsStore=Store, Ans=Tail).

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

lj(! Clause, Store, AnsStore, (!Clause, Ans) - Tail,  Flag) :-
   copy(Clause, X:M '-o' A),
   (match(X, M, Store, Store1)
    -> (lj(A, Store1, AnsStore, Ans -Tail, _Flag), Flag=nodeadlock)
      ; (AnsStore=Store, Ans= Tail)).
	
ask(C):- call(C).

