/* 

This is a theory for checking subtype constraints
for record types a la Abadi/Cardelli.

acc(S,L)  <=> type S accepts label L, i.e., S has a field
	  labelled L.
	  In that case sel(S,L) is the type of the L-field of S

sty(S,T)  <=> S is a subtype of T

input(_) is not compatible with equality, 
but restricts the kind of queries one can write.
We assume that acc(S,L) is a fact in the query
if, and only if, sel(S,L) is an input term,
that is, input(sel(S,L)) is a fact in the query.

Without transitivity of stt(_,_) the theory is not local.
But for queries without stt facts,
transitivity is admissible, that is, true in the least
model of the theory plus the query facts.

Also sty need not be compatible with equality
if we are interested in stt consequences only,
that is, if we do not ask about derivable
sty facts.


Except for the transitivity clause for stt,
every clause is covered by at most 2 terms.
Therefore entailment for queries of the kind described
can be done in time O(n^2).


*/



:-option(special_relations(off)).  

% equality
eq(X,X).
eq(X,Y) -> eq(Y,X).
eq(X,Y), eq(Y,Z) -> eq(X,Z).

eq(X,Y), eq(U,V), eq(sel(X,U),S) -> eq(sel(Y,V),S).        
eq(X,Y), eq(U,V), acc(X,U) -> acc(Y,V).      
%eq(X,Y), eq(U,V) -> eq(sty(X,U),sty(Y,V)).      
eq(X,Y), eq(U,V), sty(X,U) -> sty(Y,V).
eq(X,Y), eq(U,V), stt(X,U) -> stt(Y,V).      
  

% theory 
stt(X,X).
%eq(sty(X,Y),tt),stt(Y,Z) -> stt(X,Z).  % preferable, but does not work
sty(X,Y),stt(Y,Z) -> stt(X,Z).

%sty(X,Y) -> stt(X,Y).
stt(X,Y),stt(Y,Z) -> stt(X,Z).



acc(S,L),
acc(T,L),
stt(S,T),
input(sel(S,L)),
input(sel(T,L))
-> eq(sel(S,L),sel(T,L)).



% rejection of contraint sets if 
% saturated data base contains more facts
% about acc (and, hence, about sel)
% than initial database;
% this can be checked easily during congruence closure



precedence( [acc,sty,stt,sel,input,eq] ).

:-option([crw_depth(2),memo_constraints(on)]).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.

:-ordering(sto).  % subterm ordering


/*


Saturation terminated.

Persisting Clauses:

    1(1) : eq(B,B)
    2(1) : eq(B,C) -> eq(C,B)
    3(1) : eq(B,C),eq(C,D) -> eq(B,D)
    4(1) : eq(B,C),eq(D,E),eq(sel(B,D),F) -> eq(sel(C,E),F)
    5(1) : eq(B,C),eq(D,E),acc(B,D) -> acc(C,E)
    6(1) : eq(B,C),eq(D,E),sty(B,D) -> sty(C,E)
    7(1) : eq(B,C),eq(D,E),stt(B,D) -> stt(C,E)
    8(1) : stt(B,B)
    9(1) : sty(B,C),stt(C,D) -> stt(B,D)
   10(1) : stt(B,C),stt(C,D) -> stt(B,D)
   11(1) : input(sel(B,C)),input(sel(D,C)),acc(B,C),acc(D,C),stt(B,D) -> eq(sel(B,C),sel(D,C))
   29(2) : eq(B,C),eq(B,D) -> stt(C,D)



Total time: 99080 milliseconds

Number of forward inferences: 29
Number of tableau inferences: 0
Number of kept clauses: 12


*/