/***************************************************************************
  file: closure/flreqltrailer.fli

  Author(s): Guizhen Yang

  Contact:   flora-users@lists.sourceforge.net

  Copyright (C) The Research Foundation of SUNY, 1999-2001

  This is a template file to generate the FLORA trailer with
  equality maintenance.

  The actual trailer, flreqltrailer.flh,
  is generated by the predicate flWrapAround/1 in
  flrwraparound.P. It is invoked by the makefile when Flora is built.
***************************************************************************/


#include "flora_wspredicates.flh"
#include "flora_porting.flh"

:- import flora_warning_line/1 from flrprint.
:- import flora_funct_arity/2 from flrwrapper.


/***************************************************************************
  closure rules for X::Y

  The following rules are removed from the new trailer:

  %% super_sub/2
  super_sub(X,Y) :-
	inferred_sub_eql(X,Z),
	inferred_sub_eql(Z,Y).

  super_sub(X,Y) :-
	super_sub(X,Z),
	inferred_sub_eql(Z,Y).

  %% immediate_sub/2
  immediate_sub(X,Y) :-
	inferred_sub_eql(X,Y),
	FLORA_TNOT(super_sub(X,Y)).
***************************************************************************/
%% inferred_sub_eql/2
inferred_sub_eql(X,Y) :-
	inferred_sub(X,Y).

inferred_sub_eql(X,Y) :-
	diffobjeql(X,OX),
	inferred_sub(OX,Y).

inferred_sub_eql(X,Y) :-
	diffobjeql(Y,OY),
	inferred_sub(X,OY).

inferred_sub_eql(X,Y) :-
	diffobjeql(X,OX),
	diffobjeql(Y,OY),
	inferred_sub(OX,OY).


%% sub/2
sub(X,Y) :-
	inferred_sub_eql(X,Y),
	(X=Y, flora_warning_line('cycle in class hierarchy'); true).

sub(X,Y) :-
	silent_sub(X,Z),
	inferred_sub_eql(Z,Y),
	(X=Y, flora_warning_line('cycle in class hierarchy'); true).


/***************************************************************************
  closure rules for O:C

  The following rules are removed from the new trailer:

  %% super_isa/2
  super_isa(O,C) :-
	inferred_isa_eql(O,S),
	sub(S,C).

  %% immediate_isa/2
  immediate_isa(O,C) :-
	inferred_isa_eql(O,C),
	FLORA_TNOT(super_isa(O,C)).
***************************************************************************/
%% inferred_isa_eql/2
inferred_isa_eql(O,C) :-
	inferred_isa(O,C).

inferred_isa_eql(O,C) :-
	diffobjeql(O,OX),
	inferred_isa(OX,C).

inferred_isa_eql(O,C) :-
	diffobjeql(C,CX),
	inferred_isa(O,CX).

inferred_isa_eql(O,C) :-
	diffobjeql(O,OX),
	diffobjeql(C,CX),
	inferred_isa(OX,CX).


%% isa/2
isa(O,C) :-
	inferred_isa_eql(O,C).

isa(O,C) :-
	inferred_isa_eql(O,S),
	sub(S,C).


/*****************************************************************************
  The following rules propogate the effects of equality.
*****************************************************************************/
%% inferred_ifd_eql/3
inferred_ifd_eql(C,M,V) :-
	inferred_ifd(C,M,V).

inferred_ifd_eql(C,M,V) :-
	diffobjeql(C,CX),
	inferred_ifd(CX,M,V).

inferred_ifd_eql(C,M,V) :-
	diffobjeql(V,VX),
	inferred_ifd(C,M,VX).

inferred_ifd_eql(C,M,V) :-
	diffobjeql(C,CX),
	diffobjeql(V,VX),
	inferred_ifd(CX,M,VX).


%% inferred_fd_eql/3
inferred_fd_eql(O,M,V) :-
	inferred_fd(O,M,V).

inferred_fd_eql(O,M,V) :-
	diffobjeql(O,OX),
	inferred_fd(OX,M,V).

inferred_fd_eql(O,M,V) :-
	diffobjeql(V,VX),
	inferred_fd(O,M,VX).

inferred_fd_eql(O,M,V) :-
	diffobjeql(O,OX),
	diffobjeql(V,VX),
	inferred_fd(OX,M,VX).


%% inferred_imvd_eql/3
inferred_imvd_eql(C,M,V) :-
	inferred_imvd(C,M,V).

inferred_imvd_eql(C,M,V) :-
	diffobjeql(C,CX),
	inferred_imvd(CX,M,V).

inferred_imvd_eql(C,M,V) :-
	diffobjeql(V,VX),
	inferred_imvd(C,M,VX).

inferred_imvd_eql(C,M,V) :-
	diffobjeql(C,CX),
	diffobjeql(V,VX),
	inferred_imvd(CX,M,VX).


%% inferred_imvddef_eql/2
inferred_imvddef_eql(C,M) :-
	inferred_imvddef(C,M).

inferred_imvddef_eql(C,M) :-
	diffobjeql(C,CX),
	inferred_imvddef(CX,M).


%% inferred_mvd_eql/3
inferred_mvd_eql(O,M,V) :-
	inferred_mvd(O,M,V).

inferred_mvd_eql(O,M,V) :-
	diffobjeql(O,OX),
	inferred_mvd(OX,M,V).

inferred_mvd_eql(O,M,V) :-
	diffobjeql(V,VX),
	inferred_mvd(O,M,VX).

inferred_mvd_eql(O,M,V) :-
	diffobjeql(O,OX),
	diffobjeql(V,VX),
	inferred_mvd(OX,M,VX).


%% inferred_mvddef_eql/2
inferred_mvddef_eql(O,M) :-
	inferred_mvddef(O,M).

inferred_mvddef_eql(O,M) :-
	diffobjeql(O,OX),
	inferred_mvddef(OX,M).


/*****************************************************************************
  inheritable methods that are locally defined

  The argument "MethSign" is in the form of Funct/Arity/Type.
*****************************************************************************/
%% local_ifd/2
local_ifd(S,MethSign) :-
	var(MethSign),
	!,
	inferred_ifd_eql(S,M,_V),
	%% Should have a cut here when XSB will allow
	flora_funct_arity(M,MethSign).

local_ifd(S,MethSign) :-
	flora_funct_arity(M,MethSign),
	inferred_ifd_eql(S,M,_V).
	%% Should have a cut here when XSB will allow


%% local_fd/2
local_fd(S,MethSign) :-
	var(MethSign),
	!,
	inferred_fd_eql(S,M,_V),
	%% Should have a cut here when XSB will allow
	flora_funct_arity(M,MethSign).

local_fd(S,MethSign) :-
	flora_funct_arity(M,MethSign),
	inferred_fd_eql(S,M,_V).
	%% Should have a cut here when XSB will allow


%% local_imvd/2
local_imvd(S,MethSign) :-
	var(MethSign),
	inferred_imvd_eql(S,M,_V),
	%% Should have a cut here when XSB will allow
	flora_funct_arity(M,MethSign).

local_imvd(S,MethSign) :-
	var(MethSign),
	!,
	inferred_imvddef_eql(S,M),
	flora_funct_arity(M,MethSign).

local_imvd(S,MethSign) :-
	flora_funct_arity(M,MethSign),
	inferred_imvd_eql(S,M,_V).
	%% Should have a cut here when XSB will allow

local_imvd(S,MethSign) :-
	flora_funct_arity(M,MethSign),
	inferred_imvddef_eql(S,M).


%% local_mvd/2
local_mvd(S,MethSign) :-
	var(MethSign),
	inferred_mvd_eql(S,M,_V),
	%% Should have a cut here when XSB will allow
	flora_funct_arity(M,MethSign).

local_mvd(S,MethSign) :-
	var(MethSign),
	!,
	inferred_mvddef_eql(S,M),
	flora_funct_arity(M,MethSign).

local_mvd(S,MethSign) :-
	flora_funct_arity(M,MethSign),
	inferred_mvd_eql(S,M,_V).
	%% Should have a cut here when XSB will allow

local_mvd(S,MethSign) :-
	flora_funct_arity(M,MethSign),
	inferred_mvddef_eql(S,M).


/*****************************************************************************
  nonmonotonic multiple inheritance of scalar attributes
  from superclasses to subclasses
*****************************************************************************/
ifd(C,M,V) :-
	inferred_ifd_eql(C,M,V).

ifd(C,M,V) :-
	var(M),
	!,
	inheritance_ifd_eql(Super,M,V),
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_ifd(C,MethSign)),
	candidate_class_ifd(Super,MethSign,C),
	FLORA_TNOT(multiple_class_ifd(Super,MethSign,C)).

ifd(C,M,V) :-
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_ifd(C,MethSign)),
	candidate_class_ifd(Super,MethSign,C),
	inheritance_ifd_eql(Super,M,V),
	FLORA_TNOT(multiple_class_ifd(Super,MethSign,C)).


/*****************************************************************************
  nonmonotonic multiple inheritance of scalar attributes
  from superclasses to instances/members
*****************************************************************************/
fd(O,M,V) :-
	inferred_fd_eql(O,M,V).

fd(O,M,V) :-
	var(M),
	!,
	inheritance_ifd_eql(Super,M,V),
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_fd(O,MethSign)),
	candidate_object_ifd(Super,MethSign,O),
	FLORA_TNOT(multiple_object_ifd(Super,MethSign,O)).

fd(O,M,V) :-
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_fd(O,MethSign)),
	candidate_object_ifd(Super,MethSign,O),
	inheritance_ifd_eql(Super,M,V),
	FLORA_TNOT(multiple_object_ifd(Super,MethSign,O)).


/*****************************************************************************
  nonmonotonic multiple inheritance of multivalued attributes
  from superclasses to subclasses
*****************************************************************************/
imvd(C,M,V) :-
	inferred_imvd_eql(C,M,V).

imvd(C,M,V) :-
	var(M),
	!,
	inheritance_imvd_eql(Super,M,V),
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_imvd(C,MethSign)),
	candidate_class_imvd(Super,MethSign,C),
	FLORA_TNOT(multiple_class_imvd(Super,MethSign,C)).

imvd(C,M,V) :-
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_imvd(C,MethSign)),
	candidate_class_imvd(Super,MethSign,C),
	inheritance_imvd_eql(Super,M,V),
	FLORA_TNOT(multiple_class_imvd(Super,MethSign,C)).


imvddef(C,M) :-
	inferred_imvddef_eql(C,M).

imvddef(C,M) :-
	var(M),
	!,
	inheritance_imvddef_eql(Super,M),
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_imvd(C,MethSign)),
	candidate_class_imvd(Super,MethSign,C),
	FLORA_TNOT(multiple_class_imvd(Super,MethSign,C)).

imvddef(C,M) :-
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_imvd(C,MethSign)),
	candidate_class_imvd(Super,MethSign,C),
	inheritance_imvddef_eql(Super,M),
	FLORA_TNOT(multiple_class_imvd(Super,MethSign,C)).

imvddef(C,M) :-
	imvd(C,M,_V).
	%% Should have a cut here when XSB will allow


/*****************************************************************************
  nonmonotonic multiple inheritance of multivalued attributes
  from superclasses to instances/members
*****************************************************************************/
mvd(O,M,V) :-
	inferred_mvd_eql(O,M,V).

mvd(O,M,V) :-
	var(M),
	!,
	inheritance_imvd_eql(Super,M,V),
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_mvd(O,MethSign)),
	candidate_object_imvd(Super,MethSign,O),
	FLORA_TNOT(multiple_object_imvd(Super,MethSign,O)).

mvd(O,M,V) :-
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_mvd(O,MethSign)),
	candidate_object_imvd(Super,MethSign,O),
	inheritance_imvd_eql(Super,M,V),
	FLORA_TNOT(multiple_object_imvd(Super,MethSign,O)).


mvddef(O,M) :-
	inferred_mvddef_eql(O,M).

mvddef(O,M) :-
	var(M),
	!,
	inheritance_imvddef_eql(Super,M),
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_mvd(O,MethSign)),
	candidate_object_imvd(Super,MethSign,O),
	FLORA_TNOT(multiple_object_imvd(Super,MethSign,O)).

mvddef(O,M) :-
	flora_funct_arity(M,MethSign),
	FLORA_TNOT(local_mvd(O,MethSign)),
	candidate_object_imvd(Super,MethSign,O),
	inheritance_imvddef_eql(Super,M),
	FLORA_TNOT(multiple_object_imvd(Super,MethSign,O)).

mvddef(O,M) :-
	mvd(O,M,_V).
	%% Should have a cut here when XSB will allow


/*****************************************************************************
  monotonic inheritance of binary attributes (tabled methods)
*****************************************************************************/
meth(O,M) :-
	inferred_meth(O,M).

meth(O,M) :-
	diffobjeql(O,OX),
	inferred_meth(OX,M).

meth(O,M) :-
	isa(O,C),
	imeth(C,M).


imeth(C,M) :-
	inferred_imeth(C,M).

imeth(C,M) :-
	diffobjeql(C,CX),
	inferred_imeth(CX,M).

imeth(C,M) :-
	inheritance_sub(C,S),
	imeth(S,M).


/*****************************************************************************
  nontabled methods (transactions)
*****************************************************************************/
tran(O,T) :-
	inferred_tran(O,T).

tran(O,T) :-
	diffobjeql(O,OX),
	inferred_tran(OX,T).


/*****************************************************************************
  monotonic inheritance of signatures
*****************************************************************************/
%% fdsig/3
fdsig(O,M,R) :-
	inferred_fdsig(O,M,R).

fdsig(O,M,R) :-
	diffobjeql(O,OX),
	inferred_fdsig(OX,M,R).

fdsig(O,M,R) :-
	diffobjeql(R,RX),
	inferred_fdsig(O,M,RX).

fdsig(O,M,R) :-
	diffobjeql(O,OX),
	diffobjeql(R,RX),
	inferred_fdsig(OX,M,RX).

fdsig(O,M,R) :-
	isa(O,C),
	ifdsig(C,M,R).


%% fdsigdef/2
fdsigdef(O,M) :-
	inferred_fdsigdef(O,M).

fdsigdef(O,M) :-
	diffobjeql(O,OX),
	inferred_fdsigdef(OX,M).

fdsigdef(O,M) :-
	isa(O,C),
	ifdsigdef(C,M).

fdsigdef(O,M) :-
	fdsig(O,M,_V).
	%% Should have a cut here when XSB will allow


%% ifdsig/3
ifdsig(C,M,R) :-
	inferred_ifdsig(C,M,R).

ifdsig(C,M,R) :-
	diffobjeql(C,CX),
	inferred_ifdsig(CX,M,R).

ifdsig(C,M,R) :-
	diffobjeql(R,RX),
	inferred_ifdsig(C,M,RX).

ifdsig(C,M,R) :-
	diffobjeql(C,CX),
	diffobjeql(R,RX),
	inferred_ifdsig(CX,M,RX).

ifdsig(C,M,R) :-
	inheritance_sub(C,S),
	ifdsig(S,M,R).


%% ifdsigdef/2
ifdsigdef(C,M) :-
	inferred_ifdsigdef(C,M).

ifdsigdef(C,M) :-
	diffobjeql(C,CX),
	inferred_ifdsigdef(CX,M).

ifdsigdef(C,M) :-
	inheritance_sub(C,S),
	ifdsigdef(S,M).

ifdsigdef(C,M) :-
	ifdsig(C,M,_V).
	%% Should have a cut here when XSB will allow


%% mvdsig/3
mvdsig(O,M,R) :-
	inferred_mvdsig(O,M,R).

mvdsig(O,M,R) :-
	diffobjeql(O,OX),
	inferred_mvdsig(OX,M,R).

mvdsig(O,M,R) :-
	diffobjeql(R,RX),
	inferred_mvdsig(O,M,RX).

mvdsig(O,M,R) :-
	diffobjeql(O,OX),
	diffobjeql(R,RX),
	inferred_mvdsig(OX,M,RX).

mvdsig(O,M,R) :-
	isa(O,C),
	imvdsig(C,M,R).


%% mvdsigdef/2
mvdsigdef(O,M) :-
	inferred_mvdsigdef(O,M).

mvdsigdef(O,M) :-
	diffobjeql(O,OX),
	inferred_mvdsigdef(OX,M).

mvdsigdef(O,M) :-
	isa(O,C),
	imvdsigdef(C,M).

mvdsigdef(O,M) :-
	mvdsig(O,M,_V).
	%% Should have a cut here when XSB will allow


%% imvdsig/3
imvdsig(C,M,R) :-
	inferred_imvdsig(C,M,R).

imvdsig(C,M,R) :-
	diffobjeql(C,CX),
	inferred_imvdsig(CX,M,R).

imvdsig(C,M,R) :-
	diffobjeql(R,RX),
	inferred_imvdsig(C,M,RX).

imvdsig(C,M,R) :-
	diffobjeql(C,CX),
	diffobjeql(R,RX),
	inferred_imvdsig(CX,M,RX).

imvdsig(C,M,R) :-
	inheritance_sub(C,S),
	imvdsig(S,M,R).


%% imvdsigdef/2
imvdsigdef(C,M) :-
	inferred_imvdsigdef(C,M).

imvdsigdef(C,M) :-
	diffobjeql(C,CX),
	inferred_imvdsigdef(CX,M).

imvdsigdef(C,M) :-
	inheritance_sub(C,S),
	imvdsigdef(S,M).

imvdsigdef(C,M) :-
	imvdsig(C,M,_V).
	%% Should have a cut here when XSB will allow


/*****************************************************************************
  object existence
*****************************************************************************/
exists(X) :-
	inferred_exists(X).

exists(X) :-
	diffobjeql(X,OX),
	inferred_exists(OX).


/*****************************************************************************
  basic equality maintenance
*****************************************************************************/
%% Means X,Y are equal, but not identical
diffobjeql(X,Y) :-
	inferred_objeql(X,Y),
	X \= Y.

diffobjeql(X,Y) :-
	inferred_objeql(Y,X),
	X \= Y.

diffobjeql(X,Y) :-
	diffobjeql(X,Z),
	diffobjeql(Z,Y),
	X \= Y.