/* Backward Chaining OAV Expert System Shell Modified for 1995 Final Probl. 3.
   Sample data and rule at end of file. Changes made in the quantifier
   clause (search for "Goal=") and the rule and data added at the end.

	Please report all bugs to koppel@gate.ee.lsu.edu.
	Technical support: 14:00 - 16:30 M,Th; 10:40-11:30 MWF
	(except during tests).

*/

:-reconsult('stdStuff.pro'). :-reconsult('ask.pro').  

:-op(950,xfx,:).	:-op(945,fx,if).	:-op(940,xfx,then).  
:-op(800,xfy,or).	:-op(750,xfy,and).	:-op(700,fy,not).
:-op(100,xfx,':=').	:-op(90,xfx,':.').	

% Remove old instance name counters and facts used for quantified expressions.
%
wipe:-abolish(nameList,2),abolish(doAllRec,2),fail.

% Remove old facts, except for initial facts.
%
wipe:-( D=data(_,_,X) ; D=data(_,_,_,X) ),D,
 	not(X=init),retract(D),
	fail ; true.

% Start expert system by finding value of root goal.
%
rootGoal(RG):-
	wipe,deduce(RG,TV),
	sOut<<"The root goal has value "<<<TV<<nl.

%
% The Parse Clauses
%
% deduce(Expr,Val) unifies Val with value of Expr.
%
% The following main cases are considered; some use several clauses.
%  Check for error conditions.		E.g., X
%  Check for logical operators,		E.g., a and b.
%  Check for a command.			E.g., sOut<<"Hello, world!"<<nl
%  Check for a quantifier.		
%    E.g., forAll(C:.isa=animal,C:.spec=dog,C:.personality=friendly)
%  Check for a new instance request.	E.g., new(human,X).
%  Check for unification.		E.g., Color=red.
%  Check for item's value in database.
%  Ask the user.
%  Try a rule.
%  If all else fails, an item's value is itself.
%

% Check for an unbound item, an error.
%
deduce(Item,_):-
	( var(Item) ; Item=Obj:._,var(Obj) ),!,
	sOut<<"Warning! Unbound item to parse."<<nl.

% Parse conjunction.
%
deduce(Goal1 and Goal2,TV):-!,
	deduce(Goal1,V1),isTV(V1),	% Get truth of goal 1.
	once (
	 V1=false,TV=false		% If goal 1 false, TV=false;...
	 ;
	 V1=true,deduce(Goal2,V2),	% ...otherwise, check goal 2.
	 isTV(V2),TV=V2			% Check for error and set TV.
	).

% Parse disjunction.
%
deduce(Goal1 or Goal2,TV):-!,
	deduce(Goal1,V1),isTV(V1),	% Get truth of goal 1.
	once (
	 V1=true,TV=true		% If true, TV=true;...
	 ;
	 V1=false,deduce(Goal2,V2),	% ..otherwise, check goal 2.
	 isTV(V2),TV=V2			% Check for error and set TV.
	).

% Parse negation.
%
deduce(not Goal,TV):-!,
	deduce(Goal,V),isTV(V),		% Get truth of goal.
	( V=true,TV=false 		% Negate.
	; V=false,TV=true).

% Perform a command.
%
deduce(Goal,Result):-
	member(Goal,			% Is goal in command list?
	[askAndCheck(_,_,_,_),_<_,_>_,_=<_,_>=_,_ is _
	,newName(_,_),_ << _,_ <<< _
	,conclude(_,_,_),conclude(_,_,_,_),call(_)]),!,
	once (				
	 Goal,!,Result=true 		% If so, execute and return
	 ; Result=false			%  appropriate result.
	).

% Handle quantified expressions.
%
% Parts of this clause:
%  1. Parse goal.
%  2. Get list of candidate objects, Os.
%     (An object, say x, is a candidate if M is true when O=x.)
%  3. For each candidate in Os, test if G is true.
%  4. Unify Val to true or false, depending on how many times G was true.
%
deduce(Goal,Val):-
	Goal=..[Amt,O:.isa=Class|R],	% Extract parts of quantifier cmd.
	var(O),atom(Class),
	member(Amt,[forAll,forEach	% Check for valid quantifier.
	,forSome,forNone,forCount]),
	!,				% (Below) Get list of objects.
	once ( 
	  Amt=forCount, R=[M,G,P] 
	  ;
	  R=[M,G]
	  ),
	setof(O,[M,From]^(data(O,isa,Class,From),deduce(M,true)),Os),
	newName(doAll,Name),		% Make a outcome name.
	asserta(doAllRec(Name,true,0)), % Initialize number of true outcomes.
	asserta(doAllRec(Name,fail,0)), % Initialize number of fail outcomes.
	(
	 member(O,Os),			% Get an object.
	 once (deduce(G,Outcome)),	% Test condition on object.
					% (Below) increment appropriate outcome.
	 retract(doAllRec(Name,Outcome,Num)),
	 NumI is Num +1,
	 asserta(doAllRec(Name,Outcome,NumI)),
	 fail				% Induce backtracking to get 
	 ; 				%   next object.
	 true
	),				
	retract(doAllRec(Name,true,NT)),% Retreive num. of true outcomes.
	once ( NT>0,S=t ; true ),	% Bind S=t if there is >=1 success.
	retract(doAllRec(Name,fail,NF)),% Retreive num. of fail outcomes.
	once ( NF>0,F=t ; true ),	% Bind F=t if there is >=1 fail.
	once ( 
	  ( Amt=forNone,var(S) ; Amt=forSome,not((var(S),nonvar(T))) ; 
	    Amt=forAll,var(F)  ; Amt=forEach ;
					% (Below) Compute fraction of succs.
	    Amt=forCount, length(Os,L), P is NT / L
	  ),!,Val=true
	  ;
	  Val=false
	).

% Existential Quantifier.
%
deduce(thereExist(O:.isa=Class,SuchThat),TV):-!,
	(data(O,isa,Class,Val),		% Find an object.
	 deduce(SuchThat,true),!,	% See if condition true.
	 TV=true			% Is true.
	 ;
	 TV=false			% Condition false.
	),!.

% Make a new instance of Class.
%
deduce(new(Class,Inst),Res):-
	var(Inst),			% Check for error condition.
	props(Class,_,_,_),		% Make sure class is a class.
 	newName(Class,Inst),		% Make a name for the instance.
					% (Below) Assert "isa" link.
	conclude(Inst,isa,Class,newClause),!,Res=true
	; Res=false.

% Unify two items.
%
deduce(X=Y,Val):-!,			% (Below) Get values.
	( nonvar(X),deduce(X,Vx) ; Vx=X ),
	( nonvar(Y),deduce(Y,Vy) ; Vy=Y ),
	(
	 Vx=Vy,!,Val=true		% Try to unify. Set result.
	 ;
	 Val=false		
	),!. 

% Retreive known data for OAV.
%
deduce(Obj:.Attr,Val):-
    	isOA(Obj,Attr),			% Check for error conditions.
	data(Obj,Attr,V,_),!,V=Val.	% Try to retreive value.

% Retreive known data for item.
%
deduce(Item,Val):-
        isItem(Item),
	data(Item,V,_),V=Val.

% Ask user about OAV.
%
deduce(O:.Attr,Res):-
        isOA(O,Attr),
	( 
	  data(O,isa,Class,_) 		% Either O is a class instance...
	  ; 
	  Class=O 			% ...or it's not.
	),
	props(Class,Attr,Q,Valid),	% Get question and validation rule.
 	askAndCheck(Q,O,Valid,Ans),	% Ask...
	conclude(O,Attr,Ans,user),	% ...and assert answer.
	!,Res=Ans.

% Ask user about item.
%
deduce(Item,Res):-
        isItem(Item),
	props(Item,Q,Valid),		% Retreive question,
 	askAndCheck(Q,Item,Valid,Ans),	% ask,
	conclude(Item,Ans,user),	% and assert answer.
	!,Res=Ans.

% Use a rule to prove a proposition true.
%
deduce(Prop,Res):-
	atom(Prop),			% Check for symbol.
	_:if _ then Prop,!,		% If >=one rule found then
	once (				%  this is the right clause.
	 Rule:if Ante then Prop,	% Find a rule.
	 deduce(Ante,true),		% If antecedent true...
	 TV=true			%  ...consequent true; otherwise
	 ;				%  try another rule.
	 TV=false			% If no rules work, assume false.
	),
	conclude(Prop,TV,byRule(Rule)), % Write result.
	!,Res=TV.			% Unify with result.

% Use a rule for an OA which can take on a truth value.
%
deduce(Obj:.Attr,Res):-
        isOA(Obj,Attr),			% Check that Obj and Attr are okay.
	_:if _ then Obj:.Attr,!,	% If >-one rule found then
	once (				%  this is the right clause.
	 Rule:if Ante then Obj:.Attr,	% Find a rule.
	 deduce(Ante,true),		% If antecedent true...
	 TV=true			% ...consequent is true.
	 ;
	 TV=false			% Assume false.
	),conclude(Obj,Attr,TV,byRule(Rule)),!,TV=Res.

% Use a rule to find an item's value.
%
deduce(Item,Res):-
	atom(Item),			% Make sure item is an item.
	R:if Ante then Item:=Val,	% Find rule.
	deduce(Ante,true),!,		% If antecdent true...
	conclude(Item,Val,byRule(R)),	% ...Val unified with value.
	Res=Val.

% Use a rule to find an OA's value.
%
deduce(Obj:.Attr,Res):-			
        isOA(Obj,Attr),			% Make sure Obj and Attr are.
					% (Below) Find rule.
	Rule:if Ante then Obj:.Attr:=Val,
	deduce(Ante,true),!,		% If antecedent true...
	conclude(Obj,Attr,Val,Rule),	% ...Val unified with value.
	Res=Val.			% Unify with parameter.

% Use matching rule. (Consequent cannot be an OAV, and its truth value is not
% asserted.  In other words, consequent is a command to fire a rule rather
% than a proposition to prove true.)
%
deduce(Command,true):-
	Rule:if Antecedent then Command,% Find command and
	deduce(Antecedent,true),!.	% execute. 
	
% If an Item's value cannot be found any other way, then value is item.
%
deduce(Item,Item).

% Print a message when selected items are found.
%
% Variable Say is item  or instance, variable It is class or item.
%
announce(Item,Val):-
	(
	 atom(Item),Say=Item,It=Item	% Simple case: Item.
	 ; 
	 Item=Obj:.Attr,		% Other case, OAV.
	 ( data(Obj,isa,Class,_) ; Class=Obj ),
	 It=Class:.Attr,		% (Above) Obj is instance or class.
	 Say=Obj:.Attr
	),
	aGoalList(Goals),		% Retrieve list of facts to announce.
	( 
	  announceAll ; 		% Announce all (for debugging) or
	  member(It,Goals) 		% use list.
	),				% (Below) Announcement.
	sOut<<"The item "<<<Say<<" has been shown to have value "<<Val<<"."<<nl.

announce(_,_).				% Succeed even if no announcement.

% Check for truth value. If none found, print error message.
%
isTV(true):-!.
isTV(false):-!.
isTV(X):-
	sOut<<"Warning, truth value expected, "<<<X<<" encountered."<<nl.

% Check if O is an object and A is an attribute of that object. The
% code below does not yet do that. It instead makes a much weaker test.
%
isOA(O,A):-atom(O),atom(A).

isItem(X):-atom(X).

% Assert new OAV value.
%
conclude(O,A,V,Source):-
	atom(O),atom(A),nonvar(V),	% Check for error conditions.
	nonvar(Source),
	announce(O:.A,V),		% Print message for user, if wanted.
	asserta(data(O,A,V,Source)).	% Put value into database.

% Assert new item value.
%
conclude(Item,V,Source):-
	atom(Item),nonvar(V),		% Check for error conditions.
	nonvar(Source),
	announce(Item,V),		% Print message for user, if wanted.
	asserta(data(Item,V,Source)).	% Put value in database.


% Create a new instance name.
%
newName(Name,NextName):-
					% (Below) Get or initialize old cound.
	( retract(nameList(Name,OldCount)) ; OldCount=0),
	NewCount is OldCount+1,		% Increment.
	NextNameL<<Name<<NewCount,	% Combine class name with count.
	name(NextName,NextNameL),	% Create atom. (Below) Put in db.
	asserta(nameList(Name,NewCount)),!.

r1:if forCount(O:.isa=thing,O:.speed=fast and O:.loose=true,O:.height=3,P)
    then n:=P.

props(thing,speed,"How fast is it?",isString).

data(thingU1,isa,thing,init).
data(thingU1,speed,fast,init).
data(thingU1,loose,true,init).
data(thingU1,height,3,init).

data(thingU2,isa,thing,init).
data(thingU2,speed,slow,init).
data(thingU2,loose,true,init).
data(thingU2,height,7,init).

data(thingU3,isa,thing,init).
data(thingU3,speed,fast,init).
data(thingU3,loose,false,init).
data(thingU3,height,3,init).

data(thingU4,isa,thing,init).
data(thingU4,speed,medium,init).
data(thingU4,loose,true,init).
data(thingU4,height,3,init).

data(thingU5,isa,thing,init).
data(thingU5,speed,fast,init).
data(thingU5,loose,true,init).
data(thingU5,height,3,init).

data(thingU6,isa,thing,init).
data(thingU6,speed,fast,init).
data(thingU6,loose,false,init).
data(thingU6,height,11,init).

data(thingU7,isa,thing,init).
data(thingU7,speed,stopped,init).
data(thingU7,loose,true,init).
data(thingU7,height,3,init).

data(thingU8,isa,thing,init).
data(thingU8,speed,fast,init).
data(thingU8,loose,true,init).
data(thingU8,height,1,init).

data(thingU9,isa,thing,init).
data(thingU9,speed,fast,init).
data(thingU9,loose,true,init).
data(thingU9,height,33,init).

data(thingU10,isa,thing,init).
data(thingU10,speed,fast,init).
data(thingU10,loose,false,init).
data(thingU10,height,3,init).

data(thingU11,isa,thing,init).
data(thingU11,speed,fast,init).
data(thingU11,loose,false,init).
data(thingU11,height,3,init).

data(thingU12,isa,thing,init).
data(thingU12,speed,fast,init).
data(thingU12,loose,true,init).
data(thingU12,height,2,init).