/* QD-Linear Janus implementation.
Authors: Vijay Saraswat
Bugs to: saraswat@parc.xerox.com
Copyright: (C) Xerox Corporation, 1992, 1993.
File: lj10.pl 
Last Modified: Sat May 15 22:05:13 1993

Nested implications of the form ((A -* B) -* C) are now handled correctly. 

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. (If you use logical variables to 
  represent exisntially quantified variables, you may get strange errors.)

(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.
   This, just for simplicity of implementation.

(3) The alternation of existential and universal quantifier is not handled completely
    correctly. For instance, in 
      \forall R.  (f:RY -* 1,
                   exists Z. (h:Z, \forall S. g:SZ -* g:every(a, Ra, Sa)))
      R cannot be instantiated with a term containing Z. This is not checked now ---
    for the examples of interest to us, this does not cause any spurious derivations. 

   For the basic Linear Janus language, this possibility is not allowed. Universal
   quantifiers can only appear before an implication, not before a tensor, and
   the u.q. variable must occur in the antecedent. So we are guaranteed that the
   discharge of the u.q.v will happen correctly, without having to track at run-time
   dependencies between existentially and universally quantified variables.

(4) Messages are normalized at the end of the computation, rather than when they are 
   placed in the store. Because of the simple nature of matching, this is believed to 
   be ok.

(5) ! needs to be re-added.

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, Z$(x: Z -* Z:Z)), P).

P = y^[y:y],
Z = y ? 

yes

lj(Agent, Result) :-
   Result is a (possibly existentially quantified) store (tensors of messages) 
    linearly entailed by Agent. All such stores are enumerated on backtracking. 

A store is a conjunction of messages (atomic formulas of the form Chan:Term).

SYNTAX OF AGENTS
   Agent ::= 1 | Message | Method | Var^Agent | Agent, Agent
   Method ::= X$Method | Chan: Pat -* Agent 
              | X$(Chan:Term -* Chan:Pat) -* Agent
   Message ::= Chan : Term
   Pat   ::= Var | Constant | Var @ Var  | f(Pat, ..., Pat)  
   Term  ::= Var | Constant | X\Term | Term @ Term | f(Term, ..., Term)

*/
:- prolog_flag(compiling, _, fastcode).

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

:- use_module(library(ordsets)).

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

lj_1(s([], Store, Query), []) :- !, equate(Store, Query).
lj_1(s([], Store, Query), 
   [p(NewM-MTail, NewS-SRest, _InChans, _OutChans), s(MTail, SRest, OQuery) | Rest ]) :-
   equate(Store, Query), 
   lj_1(s(NewM, NewS, OQuery), Rest).

lj_1(s(Methods, Store, Query), Stack) :-
  member(X:M -* p(NewM-MTail, NewS-SRest, _InChans, _OutChans), Methods, MRest),
  matches(X, M, Store), 
  determinate(X, MRest, Stack), !,
  match(X, M, Store, SRest), 
  MTail = MRest,
  lj_1(s(NewM, NewS, Query), Stack).

lj_1(s(Methods, Store, Query), Stack) :- Stack = [_ | _],
   inherit_method(X:M -* p(NewM-Methods, NewS-SRest, _InChans, _OutChans), 
                  Stack, NewStack),
   match(X, M, Store, SRest),
   determinate(X, Methods, NewStack), !,
   lj_1(s(NewM, NewS, Query), NewStack).

lj_1(s(Methods, Store, Query), Stack) :-
   member(X:M -* p(NewM-MRest, NewS-SRest, _InChans, _OutChans), Methods, MRest), 
   match(X, M, Store, SRest), 
   lj_1(s(NewM, NewS, Query), Stack).

lj_1(s(Methods, Store, Query), Stack) :-
   member((X:M -* Y:N) -* Body, Methods, MRest), 
   lj_1(s([], [X:M], [Y:N]), [Body, s(MRest, Store, Query) | Stack]).

lj_1(s(Methods, Store, Query), Stack) :- Stack = [_ | _],
   inherit_method(X:M -* p(NewM-Methods, NewS-SRest, _InChans, _OutChans), 
                  Stack, NewStack),
   match(X, M, Store, SRest),
   lj_1(s(NewM, NewS, Query), NewStack).

lj_1(s(Methods, Store, Query), Stack) :-  Stack = [_ | _],
   inherit_message(Y:P, Stack, NewStack),
   member(X:M -* p(NewM-MRest, NewS-Store, _InChans, _OutChans), Methods, MRest),    
   match(X, M, [Y:P], []),
   lj_1(s(NewM, NewS, Query), NewStack).

lj_1(s(Methods, Store, Query), Stack) :-  Stack = [_ | _],
   inherit_method((X:M -* Y:N) -* Body, Stack, NewStack),
   lj_1(s([], [X:M], [Y:N]), [Body, s(Methods, Store, Query) | NewStack]).

inherit_method(M, [P, s(Methods, Store, Res) | Stack], 
                  [P, s(RemMethods, Store, Res) | Stack]) :- 
   member(M, Methods, RemMethods).
inherit_method(M, [P, S | Stack], [P, S | NewStack]) :-  
   inherit_method(M, Stack, NewStack).

inherit_message(M, [P, s(Methods, Store, Res) | Stack], 
                   [P, s(Methods, RemStore, Res) | Stack]) :- 
   member(M, Store, RemStore).
inherit_message(M, [P, S | Stack], [P, S | NewStack]) :-
   inherit_message(M, Stack, NewStack).

equate(Store, Query) :-
  (Query = Store ;
   (Store = [X:Term], Query = [Y:(L @T)], X == Y, L = (T\Term))), !.

/* determinate(X, Methods, Stack) :-
    This is true precisely when X is a channel and none of the methods in Methods 
    or Stack demand or produce a message on X.
*/ 

determinate(X, Methods, Stack) :-
  determinate_m(X, Methods),
  determinate_s(X, Stack).

determinate_m(_X, []).
determinate_m(X, [Y:_M -* p(_, _, InChans, OutChans) | R]) :-
   X \== Y, 
   ord_disjoint([X], OutChans),  
   ord_disjoint([X], InChans),
   determinate_m(X, R).
determinate_m(X, [(Z:_N -* Y:_M) -* p(_, _, InChans, OutChans) | R]) :-
   X \== Y, X \== Z,
   ord_disjoint([X], OutChans),  
   ord_disjoint([X], InChans),
   determinate_m(X, R).

determinate_s(_X, []).
determinate_s(X, [_P, s(Methods, _Store, _Query) | Stack]) :-
  determinate_m(X, Methods),
  determinate_s(X, Stack).

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

/* ------------------  Static Analysis ------------------*/
/* 
Here is the grammar for the canonical form of agents.

Canonical_agent ::= Binders^Can_agent_1
Binders ::= [] | [Variable | Binders]
Can_agent_1 ::= p(MethodsH-MethodsT, StoreH-StoreT)
MethodsH ::= Variable | [Method | MethodsH]
StoreH  ::= Variable | [Atomic_formula | StoreH]
MethodsT, StoreT ::= Variable
Atomic_formula ::= 1 | Chan:Term
Chan ::= Variable

Annotated_Canonical_agent ::= p(MethodsH-MethodsT, StoreH-StoreT, InChans, OutChans)
InChans, OutChans ::= [] | [Chan | InChans]

simplify_agent(Agent, Binders, Norm) :-
  Norm is the normalized version of Agent, with binders Binders. 
  Essentially, the methods and atoms at each -* level are collected together, 
  per the grammar above. 

annotate(Canonical_agent, Annotated_Canonical_agent) :-
   Annotated_Canonical_agent is Canonical_agent with each p-structure being associated 
   with the list of channels on which Canonical_agent makes demands (inputs), and 
   produces messages (Outputs).

*/

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) :- 
   ((atom(X) ; var(X)) -> simplify(A, Y-Z, Norm) 
     ; error("~n Illegal term: ~p should be a variable or constant.", [X, X^A])).
simplify(X$A, Binders, Norm) :- 
   ((var(X); atom(X)) -> simplify(A, Binders, Norm)
     ; error("~n Illegal term: ~p should be a variable or constant.", [X, X^A])).     
simplify((X:M -* A), Binders, p([X:M -* NA | Y]-Y, Z-Z)) :-  simplify(A, Binders, NA).
simplify(((_$(X:M -* Y:N)) -* A), Binders, p([(X:M -* Y:N) -* NA | R]-R, Z-Z)) :-simplify(A, Binders, NA).
simplify((((X:M -* Y:N)) -* A), Binders, p([(X:M -* Y:N) -* NA | R]-R, 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).

annotate_type([(X:M -* Y:N) -* A | R],  [(X:M -* Y:N) -* 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, Y, In3),
   ord_union(Out1, OutChans_in, Out2), ord_add_element(Out2, X, Out3),
   annotate_type(R, R1-Tail, In3, InChans, Out3, OutChans).



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

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@Arg, Result) :- var(L), !, Result = (L@Arg).
normalize((L\Term)@Arg, Result) :- !,
      new(Term, Value, L, Arg),
      normalize(Value, Result).
normalize(Term, Result) :- map_tree(normalize, Term, Result), !.

/*
 match(X, M, Store, Store1) :- 
 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.

 VJ Sun May  2 22:51:00 1993
  The second clause  for match/2 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.

Want to backtrack through to allow all possible matches.

*/
matches(X, M, Store) :- \+(\+ match(X, M, Store, _)). 
match(X, M, Store, Store1) :- key_member(X, R, Store, Store1), match(M, R).

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

/* ------------------------- AUXILIARY PREDICATES ------------------------- */
member(M, [M | R], R).
member(M, [N | R], [N | S]) :- member(M, R, S).

key_member(Key, Item, [Y:Value | Store], Rem) :- Key==Y, Item=Value, Store=Rem.
key_member(Key, Item, [Entry | Store], [Entry | Rem]) :- key_member(Key, Item, Store, Rem).

/* 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 binder  \. 
 Recall:
   Term  ::= Var | Constant | X\Term | Term @ Term | f(Term, ..., Term)
*/

new(Z, R, X, Y):- (var(Z) ; atom(Z)), !, (Z==X -> R=Y ; R=Z).
new(Y1\R, S, X, Y):-  Y1 == Y, !,  new(R, S1, Y1, Z1), new(S1, S2, X, Y), S=(Z1\S2).
new(Y1\R, S, X, Y):-  new(R, S1, X, Y), S = (Y1\S1).
new(Term, Term1, X, Y) :- map_tree(new, Term, Term1, [X, Y]).


