/* The following five lines are necessary for Sicstus, but not for LPA prolog*/
retractone(X) :- retract(X), !.
member(X,[X|_]).
member(X,[_|Y]) :- member(X,Y).
\=(X,Y) :- \==(X,Y).
?- op(700,xfx,\=).

?- op(600, xfx, ::).    /*Class qualifier*/ 
?- op(100,yfx,$).       /*Eval sequence of functions*/
?- op(100,yfx,#).       /*Dot symbol*/
?- op(110,xfy,mod).     /*Modifier classes*/
?- op(100,yfx,sub).     /*For subscript expressions */
?- op(100,yfx,key).     /*Followed by a primitive or list of primitives*/
?- op(90, fx, @).       /*Quote operator*/
?- op(110, fx, ^).      /*Pointer operator*/
?- op(710, xfx, withProto). /*For declaring prototype of set or class*/
?- op(720, xfx, inClass). /*x inClass classexpr withProto (assignments) */
?- op(710, xfx, inverse). /*name inverse id inClass class_expr (Bin Reln Decl)*/
?- op(700, xfx, :=).    /*Static assignment; right-side is primitive-valued*/
?- op(700, xfx, +=).    /*Insertion into set (primitive-valued)*/
?- op(700, xfx, =@).    /*Method assignment and subclass defn*/
?- op(700, xfx, +=@).   /*Method rule insertion */
?- op(720, xfx, <@).    /*b<@c  Redefine b as a subclass of c. */
?- op(720, xfx, +<@).   /* Add a subclass edge into ISA graph*/
?- op(690, xfx, where). /* For selection and subset defn*/
?- op(900, xfy, while). /* For while statements */
?- op(600, xfy, &).
?- op(750, xfy, ;).
?- op(740, xfy, ->).
?- op(500, fy, ~).
?- op(800, fx, for).    /* For "for PrologVar in ListExpr do Statement" */
?- op(790, xfx, in).
?- op(780, xfx, do).
?- op(900, fx, cd).     /* change directory */
?- op(1000,fx,print).
:-dynamic ':='/2 , modPass/1 .

:=(world#classes key X#invariant, @ (@true)) :- member(X,
   [any,objects,primitives,numbers,classes]).
X#sdn :=  @[[world#classes key numbers]] :- number(X), !.
_#X#sdn := @[[world#classes key numbers]] :- number(X), !.
:=( (@_) #sdn, @[[world#classes key primitives]]).

world#classes key set#sdn:= @[[world#classes key objects]].
world#sdn := @[[world#classes key objects]].
world#classes#prototype#sdn := @[[world#classes key objects]].
world#classes key any#sdn := @[ ].
world#classes key objects#sdn:= @[[world#classes key any]].
world#classes key classes#sdn:= @[[world#classes key objects]].
world#classes key primitives#sdn := @[[world#classes key objects]].
world#classes key numbers#sdn := @[[world#classes key primitives]].

world#classes key any#subsets:=world#classes key objects.
world#classes key objects#subsets:= world#classes key primitives.
world#classes key objects#subsets:= world#classes key classes.
world#classes key primitives#subsets:=world#classes key numbers.
world#subsets:= world#classes.   

/*Default assignment statements and insertion statements*/
world#classes key objects# @prologDefn(replace,
     replace(ref(X),Y)=@ @true) := @true :-
      nonvar(X), !, deleteDep(X), deleteRef(Y,R),
      condAssert(:=(X,R)), assertParts(X,R).
world#classes key objects# @prologDefn(insert,
   insert(ref(X),Y)=@ @true)  := @true :- 
      nonvar(X), !, deleteRef(Y,R), 
      condAssert(:=(X,R)), assertParts(X,R).
/*Assignments involve 1-level copy of structures, 
  not including values contained in prototype of set.*/
assertParts(X,Y) :- :=(Y#A,V), checkNotBoundAlready(X,A,V),
    A\=sdn, condAssert(:=(X#A,V)), fail.
assertParts(X,Y key Z) :- :=(Y#prototype#A,V), A\=sdn,
    checkNotBoundAlready(X,A,V), condAssert(:=(X#A,V)), fail.
assertParts(X,Y) :- :=(Y key Z, V), 
    condAssert(:=(X key Z,V)), fail.
assertParts(_,_).
checkNotBoundAlready(X key _,A,V) :- :=(X#prototype#A,V), !, fail.
checkNotBoundAlready(X,A,V) :- :=(X#A,V), !, fail.
checkNotBoundAlready(_,_,_).


deleteDep(X) :- retract((:=(X,Y):- true)), fail. /*deletes all*/
deleteDep(X) :-  retract((:=(X#Y ,Z):- true)),
	reAssertSdns(X,Y,Z), deleteDep(X#Y),fail. 
deleteDep(_).
reAssertSdns(X,Y,Z):- nonvar(Y), Y==sdn, assert(:=(X#sdn,Z)).

eval(_,X,X) :- var(X), !.  /*Prolog variables evaluate to themselves*/ 
eval(_,@X,@X) :- !.  /*Quotation mark*/
eval(Env,^X,ref(Z)) :- !, evalDot(Env,X,Z).
eval(_,ref(X),ref(X)) :- !.
eval(_,X,X) :- number(X), !.
eval(_,world,world) :- !.
eval(Env,this,Env) :- !.
eval(Env,props,ListProps) :- !,findset(P,V^(Env#P:=V),ListProps).
eval(Env,methods,L) :- !, findset(M,V^(Env#
     @prologDefn(M,V):= @true),L). 
eval(Env,(X,Y),V) :- !, eval(Env,X,_), eval(Env,Y,V).
eval(Env,(X->Y;Z),V) :- !, (eval(Env,X,@true)->eval(Env,Y,V));
      eval(Env,Z,V).
eval(Env,(X;Y),V) :- !, (eval(Env,X,V); eval(Env,Y,V)).
eval(Env,(X->Y),V) :- !, eval(Env,X,@true),eval(Env,Y,V).
eval(Env,(X while Y),@true) :-  eval(Env,X,@true), eval(Env,Y,_),
	!, eval(Env,(X while Y),@true).
eval(_,(_ while _), @true) :- !.
eval(Env,for X in ListExpr do Statement,Val) :- !,
	eval(Env, ListExpr, @List),
	member(X,List), 
	eval(Env,Statement,Val).
eval(Env,member(ref(X)),Y key K):- checkSetSubscripted(X,K,Y).
eval(Env,member(X),Y) :- !, eval(Env,X,@[H|T]), member(Y,[H|T]).
eval(_,[],[]) :- !. 
eval(Env,[X|Y],@Z) :- !, evalList(Env,[X|Y],Z).
eval(Env,X where Y,Z) :- !,
	eval(Env,X,Z), eval(Z,Y,V),
	V\= @false, V\=error(_). 
eval(Env,ClassExpr$asSet,V) :- !, 
	eval(Env,asSet(ref(ClassExpr)),V).
eval(Env,asSet(ClassExpr),M) :- 
	deleteRef(ClassExpr,R),
	checkClassExpr(R),!, 
	add2ClassExpr(R,C),
	eval(Env,C,M). 
eval(Env,asSet(Class),M) :-
	deleteRef(Class,C),
	evalDot(Env,C,D),
	checkSetSubscripted(D,M).
/*Set intersection using & */
eval(Env,X&Y,Z) :- !, eval(Env,X,Z), eval(Env,Y,Z).
eval(Env,X & ~Y,Z) :- !, eval(Env,X,Z), myNot(eval(Env,Y,Z)).
eval(Env, ~(X&Y),Z) :- !, eval(Env,(~X; ~Y),Z).
eval(Env, ~(X;Y),Z) :- !, eval(Env,(~X & ~Y),Z).
eval(Env,~(~X),Z) :- !, eval(Env,X,Z).
eval(Env,~X,Z) :- !, eval(Env,world#classes key any$asSet,Z),
	myNot(eval(Env,X,Z)).
eval(Env,empty(SetExpr),@true) :- 
	!, myNot(eval(Env,SetExpr,_)).
eval(Env,nonEmpty(ClassExpr),@true) :- !,
	myNot(eval(Env,empty(ClassExpr),@true)), !.
eval(Env,X+<@ClassExpr,XDot) :- !, /*add ClassExpr as superclass of X*/ 
	evalDot(Env,X,XDot), 
	(:=(XDot#sdn,@Old); Old=[]), !,
	mkeBool(Old,OldExpr),
	addEnv2ClassExpr(Env,ClassExpr,C),
	normalize(C,YNormal),
	addSdn(XDot,C),
	addSubsets(XDot,YNormal). 
eval(Env,X<@Y,Z) :- var(Y), !, eval(Env,X<@ (Y where true),Z).
eval(Env,(X<@(Y where Z)), @true):- !, /*adding X as subclass of Y */
	addEnv2ClassExpr(Env,Y,C), /*fails if Y not a classExpr*/
	evalDot(Env,X,XDot),  /*defaults superclass to objects*/
	deleteDep(XDot),
	addInvar(XDot,Z),
	normalize(C,YNormal),
	addSdn(XDot,C),
	addSubsets(XDot,YNormal). 
eval(Env,X<@Y,V) :- !, eval(Env,X<@Y where true, V).
eval(Env,X+=Y, V) :- !, /* subset addition to X */
	evalDot(Env,X,XDot), 
	eval(Env,Y,YVal),
	checkInvar(XDot,YVal),
	eval(Env,insert(ref(XDot),YVal),V).
eval(Env,(X:=Y),V) :- !, evalDot(Env,X,XDot),
	eval(Env,Y,YVal), 
	checkInvar(XDot,YVal),
	eval(Env,replace(ref(XDot),YVal),V). 
eval(Env, X inClass Y withProto A,@true) :- !, 
     addEnv2ClassExpr(Env,Y,W), normalize(W,N),
     evalDot(Env, X, XDot), 
     addAssX(A,XDot,AMod),
     eval(Env,AMod,_),  /*Execute assignments A */
     condAssert(:=(XDot#sdn,@N)).
eval(Env,X inClass Y,V) :- !, eval(Env,X inClass Y withProto @true,V).
/* Unlike :=, function defn and insertion cannot be overridden*/
eval(Env,(X=@Y),@true) :- !, evalDot(Env,X,Oid#Expr),
     functor(Expr,F,_),
     retractall(:=(Oid# @prologDefn(F,_=@_),@true)),
     assert(:=(Oid# @prologDefn(F,Expr=@Y), @true)).
eval(Env,(X+=@Y),@true) :- !, evalDot(Env,X,Oid#Expr),
     functor(Expr,F,_),
     assert(Oid# @prologDefn(F,Expr=@Y):= @true).
eval(Env,(X$hide),@true) :- !, 
     deleteRef(X,XDot),deleteDep(XDot).
eval(Parent key _, parent,Parent) :- !.
eval(Parent#_, parent, Parent) :- !.
/* Permits calls like pnt$move(1,2)$move(3,4)*/
eval(Env,(X$inv(Y)),Val) :- !, evalDot(Env,X$inv(Y),Val).
eval(Env,(X$of(Y)),Val) :- !, evalDot(Env,X$of(Y),Val).
eval(Env,(X$of(Y,Z)),Val) :- !, evalDot(Env,X$of(Y,Z),Val).
eval(Env,(X$Y), Val) :- !, Y=.. [F|Args], 
     evalDot(Env,X,Name),
     Z=.. [F,ref(Name)|Args],   /* change into a function call. */
     eval(Env,Z,Val). 
eval(Env,(X#Y), Val) :-  evalDot(Env,X#Y,A#B), !,
      eval(A,B,Val).   /* a#b#(work) changes dir to a#b and evals work */
eval(Env,(X#Y),Val) :- !, evalDot(Env,(X#Y),Val).  /*Return keyed name*/
eval(Env,(X sub Y), Val) :- !, evalDot(Env,(X sub Y), Name),
     getVal(Name,Val). 
eval(Env,(X key Y), Val) :- !, evalDot(Env,(X key Y), Name),
     getVal(Name,Val).
eval(Env,mod(X,Y),mod(X,YDot)) :- !, 
     evalDot(Env,Y,YDot).
eval(Env,print(X),@true) :- !, eval(Env,X,V),
     deleteRef(V,U),print(U), nl.
eval(Env,X::Y,X::Y) :- !.
eval(Oid,Call,Val) :-  !, evalArgs(Oid,Call,Ecall),
     evalCall(Oid,Ecall,Val).

checkInvar(XDot,YVal) :- 
	makeDefined(XDot),
	:=(XDot#invariant,Invar),!,
	eval(YVal,Invar,V),
	V\= @false,
	V\= @error(_).
checkInvar(_,_).
makeDefined(X key _) :- :=(X#sdn,_), !.
makeDefined(XDot) :- :=(XDot#sdn,_), !.
makeDefined(X key _) :- :=(X#prototype#sdn,_), !.
makeDefined(X key _ #Z) :- :=(X#prototype#Z#sdn,_), !. 
makeDefined(XDot) :- 
	assert(:=(XDot#sdn,@[[world#classes key objects]])).

addAssX(A:=B,XDot,XDot#A:=B):- !.
addAssX(A inClass B,XDot,XDot#A inClass B) :- !.
addAssX((A:=B,T),XDot,(XDot#A:=B,U)) :- addAssX(T,XDot,U), !.
addAssX((A inClass B,T), XDot,(XDot#A inClass B,U)) :- 
     addAssX(T,XDot,U), !.
addAssX(@A,X,@A):- !.
addAssX(A,XDot,_) :- print('Invalid withProto assignment'), 
     print(A),nl,fail.

getVal(Name,Val) :- Name:=ref(Val), atomic(Val), !.  
/*Simple value*/ 
getVal(Name,Val) :- :=(Name,_), !, :=(Name,Val).
getVal(Name,Name).
 
/*Compute all values, including both data and method calls*/

evalCall(Oid,Ecall,Val) :- getF(Ecall,Oid,F,Env,Ncall), !,
     getAncestors(Env,F,Ans), 
     evalAns(Env,Ncall,Ans,Val).
 
getF(Ecall,_,F,Cls,Ncall) :- Ecall=..[F,Cls::A | B], !,
	Ncall=..[F,A|B].
getF(Ecall,_,F,Env,Ecall) :- Ecall=..[F,Env|_], !.
getF(F,Oid,F,Oid,F).

/* Return simple-valued attributes and set elements*/
evalAns(_,_,A#F,Val) :-  :=(A#F,_), !, :=(A#F,Val).
evalAns(_,_,A key F, Val) :- :=(A key F,_), !, :=(A key F,Val).
evalAns(Oid,Ecall,A # @F, Val) :- !,
     :=(A# @prologDefn(F,(Ecall=@Expr)), @true), 
     eval(Oid,Expr,Val).
/* Return name of complex object */
evalAns(_,_,Name,Name).  /*complex object; just return name*/
 
getAncestors(X,replace,world#classes key objects# @replace) :- var(X), !.
getAncestors(X,insert,world#classes key objects# @insert) :- var(X), !.
getAncestors(X,_,_) :- var(X), !, 
     print([' ***error: unbound environment: ',X]),nl,fail.
getAncestors(_,X,_) :- var(X), !, 
     print([' ****error: unbound attribute or functor symbol: ',X]), nl, fail.
getAncestors(ref(X),F,Y) :- !, getAncestors(X,F,Y).
getAncestors(X,F,Y#F) :- checkBound(X,F,Y).  /*Dont cut*/
getAncestors(X,F,Y# @F) :- checkMethodDefn(X,F,Y).
getAncestors(X,F,Y key F) :-  checkSubscripted(X,F,Y).
getAncestors(X key W #Z,F,Y) :- checkOverRiding(X key W#Z,F),
	getAncestors(X#prototype#Z,F,Y), !. /*Get only 1 prototype*/

checkOverRiding(W,F) :- checkBound(W,F,_), !, fail.
checkOverRiding(_,_).
/*subclasses override superclasses' definitions, so cut*/
checkBound(X,F,X) :-     
      ( :=(X#F,_); :=(X#F#_,_); :=(X#F key _,_)), !. 
checkBound(X,F,Y) :- F\=sdn, F\=subsets,
	isaParent(X,Z), checkBound(Z,F,Y). 

checkMethodDefn(X,F,X) :- clause(:=(X#  @prologDefn(F,_),_),_), !.
checkMethodDefn(X,F,Y) :- F\=sdn,F\=subsets,
	isaParent(X,Z), checkMethodDefn(Z,F,Y).

checkSetSubscripted(X,Y) :- 
    findset(U key G,checkAllSubscripted(X,G,U),Z), 
    member(Y,Z).
checkSubscripted(X,F,Y) :- checkAllSubscripted(X,F,Y),  !.
checkAllSubscripted(X,F,X) :- checkKey(X,F).
checkAllSubscripted(X,F,Y) :- isaSon(X,Z), checkAllSubscripted(Z,F,Y).
checkKey(X,F) :-
      (:=(X key F, _); :=(X,@F); :=(X key F # _,_); :=(X key F key _,_)).

isaParent(X,_) :- var(X), !,fail.
isaParent(X,Y) :- (X#sdn:= @[H|T]), !, intersectSorted(H,T,D), 
         member(Y,D). /*Y must be in all conjunctions*/
isaParent(X key K,X):- !.  /* Elements are subclasses of their array*/

isaAncestor(X,Y) :- isaParent(X,Y). 
isaAncestor(X,Y) :- isaParent(X,Z), isaAncestor(Z,Y). 

existAnc(X,Y) :- isaAncestor(X,Y), !.

getDescendantClasses(X,Z) :- isaSon(X,Y), 
	getDescendantClasses2(Y,Z).
getDescendantClasses2(Y,Y) :- isClass(Y). 
getDescendantClasses2(X,Z) :- isaSon(X,Y), 
	getDescendantClasses2(Y,Z).

isClass(X) :- :=(X#invariant,_),!.

isaSon(X,Y) :- :=(X#subsets,Y).

addSubsets(XDot,Y) :- var(Y), !.
addSubsets(XDot,[SuperClasses]) :- /*Only match conjunctions*/
	member(Y,SuperClasses),
	deleteRef(XDot,X),
	condAssert(:=(Y#subsets,X)), /*Add X into subsets of Y*/
	addMods(Y),
	fail.
addSubsets(_,_).

deleteRef(ref(X),X):- !.
deleteRef(X,X). 
addMods(mod(A,B)) :- modPass(A), 
 	condAssert(:=(B#subsets,mod(A,B))),!, addMods(B).
addMods(Y key mod(A,B)) :- modPass(Y key A),
	condAssert(:=(B#subsets,Y key mod(A,B))), !,
	addMods(Y key B).
addMods(Y#mod(A,B)) :- modPass(Y#A),
	condAssert(:=(B#subsets,Y#mod(A,B))), !, 
	addMods(Y#B).
addMods(_).
allSubsumed(X,[]).
allSubsumed(X,[H|T]) :- subSortedList(X,H), allSubsumed(X,T).
 
intersectSorted([],_,[]) :- !.
intersectSorted(X,[],X) :- !.
intersectSorted(H,[A|B],V) :- intersect2(H,A,C), intersectSorted(C,B,V).
intersect2(X,[],[]) :- !.
intersect2([],X,[]) :- !.
intersect2([A|B],[A|C],[A|D]) :- !, intersect2(B,C,D).
intersect2([A|B],[C|D],E) :- compare(<,A,C), !, intersect2(B,[C|D],E).
intersect2(X,[C|D],E) :- !, intersect2(X,D,E).

evalDot(_,X,Y):- var(X), !, X=Y.
evalDot(_,ref(X),ref(X)) :- !.
evalDot(_,world,world) :- !.
evalDot(X#Y,parent,X) :- !.
evalDot(X,this,X) :- !.
evalDot(_,X,X) :- number(X), !.  /* X#sdn is world#classes key numbers. */
evalDot(Env,ref(X)#Y,ref(X#Y)) :- !.
evalDot(Env,X$inv(A),Z) :- !, evalDot(Env,X,V),
     :=(Z#A,V).
evalDot(Env,X$of(Y),Z) :- !, evalDot(Env,X$of(Y,_),Z). 
evalDot(Env,X$of(Y,A),U#A) :- 
      !, evalDot(Env,X,V),  /*A inherited from Y*/
       :=(U#A,V), existAnc(U#A,world#classes key Y). 
                /*Y,A are not quoted*/
evalDot(Env,X$Y,Z) :- !, eval(Env,X$Y,Z). /*Use ref(X)*/
evalDot(Env,X sub Y,U key V) :- !, 
      evalDot(Env,X,U), eval(Env,Y,@V).
evalDot(Env,X key Y, U key Y) :- !, evalDot(Env,X,U).
evalDot(Env,mod(X,Y), W) :-  
	evalDot(Env,Y,YDot), getAncestors(Env,mod(X,YDot),W),!.
evalDot(Env,X#Y,B#Y) :- !, evalDot(Env,X,A),checkForKey(Env,A,B).
/* subscripts refer directly to (lowest sorted-order) ancestor array */
evalDot(Env,X,Y key V):- atomic(X), getAncestors(Env,X,Y key V),!.
evalDot(Env,X,Env#X). 

checkForKey(Env,A,B key V) :- getAncestors(Env,A,B key V),!.
checkForKey(Env,A,A).

evalArgs(_,X,X) :- atomic(X), !.
evalArgs(Env,X,U) :-  X=..[F|Args], evalList(Env,Args,Eargs),
     U=..[F|Eargs].

evalList(_,[],[]).  
evalList(Env,[A|B],[C|D]) :- eval(Env,A,C), evalList(Env,B,D).

:=(A key mod(X,Y)#sdn,@N) :- nonvar(Y), 
	modPass(A key X), !, normalize(Y,N).
:=(A#mod(X,Y)#sdn,@N) :- nonvar(Y), 
        modPass(A#X), !, normalize(Y,N).
:=(mod(X,Y)#sdn,@N) :- nonvar(Y), 
        modPass(X), !, normalize(Y,N).

addSdn(A key mod(X,Y),Y) :- 
	var(Y), !, condAssert(modPass(A key X)).
addSdn(A#mod(X,Y),Y) :- var(Y), !, condAssert(modPass(A#X)).
addSdn(mod(X,Y),Y) :- var(Y), !, condAssert(modPass(X)).
addSdn(XDot,Y) :-
        retract(:=(XDot#sdn,@S)), !,
        mkeBool(S,T), 
        normalize( &(Y,T), N),!,
        assert(:=(XDot#sdn,@N)).
addSdn(XDot,Y) :-
        normalize(Y,N),
        assert(:=(XDot#sdn,@N)).

addInvar(XDot,Z) :- takeOutAmpersand(Z,W),
        retract(:=(XDot#invariant,@ Xinvar)),!,
        assert(:=(XDot#invariant, @  &(W,Xinvar))).
addInvar(XDot,Z) :- takeOutAmpersand(Z,W),
        assert(:=(XDot#invariant,@ W)).
takeOutAmpersand(@X,X) :- !.
takeOutAmpersand(X,X).

checkOid(_ # _) :- !.
checkOid(X) :- print('***error: Not an object identifier: '),
         print(X), nl.

addEnv2ClassExpr(Env,X,X) :- var(X), !.
addEnv2ClassExpr(_,world,world) :- !.
addEnv2ClassExpr(Env,X;Y,A;B) :- !, addEnv2ClassExpr(Env,X,A),
     addEnv2ClassExpr(Env,Y,B).
addEnv2ClassExpr(Env,X&Y,A&B) :- !, addEnv2ClassExpr(Env,X,A),
     addEnv2ClassExpr(Env,Y,B).
addEnv2ClassExpr(Env,~X,~A) :- !, addEnv2ClassExpr(Env,X,A).
addEnv2ClassExpr(Env, X mod Y, W) :-  
    var(Y), !, (getAncestors(Env,X mod Y,W) ; W=(X mod Y)), !.
addEnv2ClassExpr(Env, X mod Y, W) :- !, 
    addEnv2ClassExpr(Env,Y,Z), 
    (getAncestors(Env,X mod Z,W) ; W=(X mod Z)), !.
addEnv2ClassExpr(Env,X,X) :- isClass(X), !.
addEnv2ClassExpr(Env,X,V) :- getAncestors(Env,X,V).

add2ClassExpr(X,X) :- var(X),!.
add2ClassExpr(X&Y,A&B) :- !, add2ClassExpr(X,A),add2ClassExpr(Y,B).
add2ClassExpr(X;Y,A;B) :- !, add2ClassExpr(X,A),add2ClassExpr(Y,B).
add2ClassExpr(~X,~A) :- !, add2ClassExpr(X,A).
add2ClassExpr(X,X$asSet).


normalize(X,X) :- var(X), !.
normalize(X,W) :- normalize2(X,Z), sortDisj(Z,Y), 
    addresolvents(Y,W).

normalize2(~(X&Y), Z) :- !, normalize2(~X; ~Y,Z).
normalize2(~(X;Y), Z) :- !, normalize2(~X& ~Y, Z).
normalize2(~ ~X, Z) :- !, normalize2(X,Z).
normalize2((X;Y);Z, W) :- 
   !, normalize2(Y;Z,U), normalize2(X;U, W).
normalize2(X;Y, Z) :- normalize2(X,A), X\=A, 
   !, normalize2(A;Y,Z).
normalize2(X;Y,X;Z) :- normalize2(Y,Z). 
normalize2(X&(Y;Z), A) :- !, normalize2(X&Y;X&Z,A).
normalize2((Y;Z)&X, A) :- !, normalize2(Y&X;Z&X,A).
normalize2((X&Y)&Z, W) :- !, normalize2(X&(Y&Z), W).
normalize2(X&Y, W) :- nonBool(X), !, normalize2(Y,Z), dist(X,Z,W).
normalize2(~X&Y, W) :- nonBool(X), !, normalize2(Y,Z), dist(~X,Z,W).
normalize2(~X&Y, Z) :- !, normalize2(~X,U), normalize2(U&Y,Z).
normalize2(~X,~X) :- nonBool(X), !.
normalize2(X,X) :- nonBool(X).

nonBool(X) :- functor(X,F,N), \=(F/N,; /2), \=(F/N,& /2), \=(F,~ ).
sortDisj(X,Y) :- disj2List(X,L), sortConjs(L,M), 
	removeSubs(M,N), sort(N,Y).

sortConjs([],[]).
sortConjs([H|T],[A|B]) :- sortConj(H,A), sortConjs(T,B).

sortConj(X,Z) :- conj2List(X,L), sort(L,M), removeDup(M,Y),
    removeAncestors(Y,Z,Y).

removeAncestors([],[],_).
removeAncestors([H|T],M,N):- getDescendantClasses(H,A),
   member(A,N),!,
   removeAncestors(T,M,N).
removeAncestors([H|T],[H|M],N) :- removeAncestors(T,M,N).
dist(X,Y;Z,A;B) :- !, dist(X,Y,A), dist(X,Z,B).
dist(X,Y,X&Y).

conj2List((X&Y),[X|Z]) :- !, conj2List(Y,Z). 
conj2List(X,[X]).

list2Conj([X],X) :- !.
list2Conj([X|Y], X&Z) :- list2Conj(Y,Z).

disj2List((X;Y),L) :- !, disj2List(X,L1), disj2List(Y,L2), 
    append(L1,L2,L).
disj2List(X,[X]).

list2Disj([X],X) :- !.
list2Disj([X|Y], X;Z) :- list2Disj(Y,Z).

mkeBool([],world#classes key any).
mkeBool([X],A):- !, list2Conj(X,A).
mkeBool([X|Y],A;B) :- list2Conj(X,A), mkeBool(Y,B).

removeDup([X],[X]) :- !.
removeDup([X|Y],Z) :- member(X,Y), !, removeDup(Y,Z).
removeDup([X|Y],[X|Z]) :- removeDup(Y,Z).

removeSubs(X,Z) :- removeTauts(X,Y), removeSubs(Y,Z,[]).

removeSubs([],[],_) :- !.
removeSubs([X|Y],Z,L) :- (member(M,Y);member(M,L)),
	subSortedList(M,X), !, 
	removeSubs(Y,Z,L).  /* X is subsumed */
removeSubs([X|Y], [X|Z],L) :- removeSubs(Y,Z,[X|L]).

removeTauts([],[]).
removeTauts([X|Y],Z) :- member(M,X), member(~M,X), !, 
	removeTauts(Y,Z).
removeTauts([X|Y],[X|Z]) :- removeTauts(Y,Z).
subSortedList([],_).
subSortedList([X|Y],[X|Z]) :- !, subSortedList(Y,Z).
subSortedList(X,[_|Z]) :- subSortedList(X,Z).

addresolvents(InitialList, Ans) :-
	findall(X, resolvent(InitialList,X),L),
	append(InitialList,L,NewList),
	removeSubs(NewList,A),
	sort(A,SortedList),
	myNot(InitialList=SortedList), 
	!,
	addresolvents(SortedList,Ans).
addresolvents(X,X).
resolvent(X,T) :- member(A,X), member(B,X), delete1(L,A,AP),
      delete1(~L,B,BP), append(AP,BP,R), sort(R,S), removeDup(S,T).	

/* Every conj of X must be a sublist of some conj of Y. */
subClass(X,Y) :- member(M,X),  /*M is a list representing a conj*/
	myNot(subListof(M,Y)), !, fail.
subClass(_,_). 
subListof(M,Y):- member(N,Y), subSortedList(M,N).

delete1(X,[X|W],W) :- !. 
delete1(X,[Y|Z],[Y|W]) :- delete1(X,Z,W).

getvals([],[]).
getvals([X|Y],[A|B]) :- getval(X,A), getvals(Y,B).

getval(X,XV) :- number(X), !, X=XV.
getval(ref(X),XV) :- nonvar(X), :=(X,XV).

findSdnValue(Env,[],_):- !. 
findSdnValue(Env,Sdn,Value) :-  
	findMost(Sdn,[],Most) ,
	deleteMost(Most,Sdn,Deleted,Others) ,
	sdnCases(Env,Most,Deleted,Others,Value) .
sdnCases(Env,Most,Deleted,Others,Value) :- 
	findRest(Env,Most,Deleted,Value).
sdnCases(Env,_,_,Others,Value) :- 
	Others\= [], findSdnValue(Env,Others,Value).

findRest(Env,~Most,Deleted,Value) :- !, /* Negated class */
	evalDot(Env,Most,C),
	myNot(checkSetSubscripted(C,Value)),
	findSdnValue(Env,Deleted,Value).
findRest(Env,Most,Deleted,Value) :-
	evalDot(Env,Most,C),
	checkSetSubscripted(C,Value),
	findSdnValue(Env,Deleted,Value).

findMost([],Counts,X) :- findLargest(X:Most,Counts), !.
findMost([H|T],OldCounts,Most):- 
	updateCounts(H,OldCounts,NewCounts),
	findMost(T,NewCounts,Most).
findLargest([]:0,[]).
findLargest(X:N,[_:M | T]) :- findLargest(X:N,T), N>=M, !.
findLargest(X:N,[X:N | _]).
deleteMost(_,[],[],[]).
deleteMost(Most,[H|T],L,NT) :- delete1(Most,H,NH), !,
	deleteMost(Most,T,Y,NT), checkAppend(NH,NT,L).
deleteMost(Most,[H|T],NH,[H|NT]) :- deleteMost(Most,T,NH,NT).
checkAppend([],L,L):- !.
checkAppend(X,Y,Z) :- append(X,Y,Z).
updateCounts([],Counts,Counts).
updateCounts([H|T],Counts, NewCounts) :- 
	updateCounts(T,Counts,NT),
	add1Count(H,NT,NewCounts).

add1Count(X,[],[X:1]).
add1Count(H,[H:C|T],[H:C1|T]) :- !, C1 is C+1.
add1Count(X,[H|T],[H|R]) :- add1Count(X,T,R).

checkClassExpr(X;Y):- !.
checkClassExpr(X&Y):- !.
checkClassExpr(~X) :- !.

condAssert(X) :- call(X),!.
condAssert(X) :- assert(X).

findset(X,Y,Z) :- findall(X,Y,W), removeDup(W,Z).

myNot(X) :- call(X), !, fail.
myNot(X).

:-assert((modPass(dummy) :- fail)).  /*Some prologs must define all preds*/
/********Basic User Interface*************/
:-dynamic curDir/1.
main:- retractall(curDir(_)), assert(curDir(world)),
        repeat, read(X), mainEval(X,Y), print(Y), nl,
        X=end, !.
 /* To change directory to Dir inside of the program, the
notation Dir.( , , ...) should be used to execute the statements*/
mainEval(end,bye) :- !.
mainEval(cd(parent),yes) :- !, mainEval(popd,yes).
mainEval(cd(X),yes) :- !,getCurDir(C),
     evalDot(C,X,W),  asserta(curDir(W)).
mainEval(popd,yes) :- !, retractone(curDir(_)).
mainEval(pwd,X) :- !, getCurDir(X).
mainEval(X,Y) :- getCurDir(CurDir), eval(CurDir,X,Y).
mainEval(_,'no more'). getCurDir(X) :- curDir(X), !.

?-member([F,N],[[+,2],[-,2],[*,2],[/,2],[mod,2],[div,2],
    [~ ,1],[sin,1],[cos,1],[tan,1],[asin,1],[acos,1],[atan,1]]),
  functor(Y,F,N),
  assert((:=(world#classes key numbers# @prologDefn(F,Y=@ V),@true)
       :-  
      Y=..[F|Args], 
      getvals(Args,Eargs), Z=..[F|Eargs],
      V is Z)), 
  fail.
?-member([F,N],[[<,2],[>,2],[=,2],[\=,2],[==,2],[=\=,2],[>=,2],[=<,2]]),
  functor(Y,F,N),
  assert((:=(world#classes key numbers# @prologDefn(F,Y=@ V),@true)
       :-  
      Y=..[F|Args], 
      getvals(Args,Eargs), Z=..[F|Eargs],
      (call(Z)-> (V= @true);(V= @false)))), 
  fail.

/* A Sample execution */ 
?- main.
world#classes key mod(lockable,X) <@ any. 
	/*Don't inherit object's assignment*/
world#classes key mod(lockable,X)# 
       insert(ref(U),W) =@  (U$locked ->
	    @error('attempt to assign locked var', @U);
	  (insert(X::ref(U),W), 
           U#locked:= @true)).
world#classes key mod(lockable,X)#lock(ref(This)) =@ 
       (This#locked:= @true).
world#classes key mod(lockable,X)#unlock(ref(This)) =@ 
       (This#locked:= @false).
b<@mod(lockable,primitives).
b$lock.
b+=5.
b$unlock.
b+=7.
b.
numbers#factorial(This) =@
    (This>1 -> This*factorial(This-1); 1).
print factorial(10).

world#classes key courses<@ objects,
world#classes key people<@ objects,
world#classes key profs<@ people,
world#classes key students<@ people.
world#classes key gradStudents<@
           students where ((level=phd);(level=masters)).
print 1.
mod(our,This)<@This where (university := @'Chung Cheng').
print 2.
ourCourses <@ mod(our,courses), ourProfs <@ mod(our,profs),
  ourStudents <@ mod(our,students).
print 3.
ourCourses+= member([@cs100,@cs105,@cs120,@cs200]).
print 4.
ourProfs+= member([@'John Doe', @'Henry James', @'Superman']).
print 5.
for X in @[tim,john,mary] do ourStudents key X inClass
    mod(our,gradStudents) withProto (level:= @phd).
print 6.
newenvir<@world.
print 7.
for X in [^ourCourses,^ourProfs,^ourStudents,^world#classes] 
 do   newenvir#subsets += X.
cd newenvir.
print 8.
print tim$level. 
print 9.
world#classes key mod(singleton,X) <@ X.
print 10.
world#classes key mod(singleton,X)#insert(ref(U),W) =@ 
           (nonEmpty(U) ->
               @error('inserting in singleton set';X::U:=W);
               insert(X::ref(U),W)). 
print 11.
world#ourStudents#prototype#advisor<@ 
	world#classes key mod(singleton,world#classes key profs).
print 12.
mary#taking+=member([cs100,cs200]).
mary#advisor:= 'John Doe'.
tim#taking+= member([cs100,cs105]).
tim#advisor+= 'John Doe'.
print 13.
john#advisor+=member(['Henry James', 'John Doe']).
print 14.
john#taking+= member([cs100,cs120]).
print 15.
'John Doe'#teaching += member([cs100,cs200]).
print 16.
'Henry James'#teaching:= cs120.
print 17.
profs#teachingOwnStudents(ref(This))=@ 
    (nonEmpty(This$teaching$inv(taking) & This$inv(advisor))
	-> This). 
print mod(our,profs)$asSet$teachingOwnStudents.
end.