/* Backward Chaining OAV Expert System Shell

	Please report all bugs to koppel@ee.lsu.edu.
	Technical support: 14:00 - 16:30 T,Th; 14:00-16:30 TT
	(except during tests).

*/


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Load some needed procedures and define operators.
%

:-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,':.').	


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Procedures for initialization and starting.
%

% 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,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.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Classification and parsing routines.
%

% Check if value. (Or, make sure not an expression.)
%
isValue(Term):-number(Term).
isValue(Term):-atom(Term).
isValue(true).
isValue(false).
isValue([H|T],[H|T]):-H>0,H<128.  % Probably an ASCII string.

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

% Determine term type. If not a simple term, fail.
%
getTermType(Term,global):-atom(Term).
getTermType(global:.Term,global):-atom(Term).
getTermType(Obj:.Attr,oav):-atom(Obj),atom(Attr).
getTermType(Term,command):-Term=..[Func,_|_], not( Func=':.' ).

% Parse oav, inserting global object if necessary.
%
parseOAV(Term,Object,Attribute):-
    getTermType(Term,Type),
    (
      Type=oav,    Object:.Attribute=Term
      ;
      Type=global, Object:.Attribute=global:.Term
     ).

% Parse oav into "class," object, and attributes. 
%
% If Term is not a class instance then ClassOrObj bound to object name,
% which is global if no object specifed.
%
getClass(Term,ClassOrObj,Object,Attr):-
    getTermType(Term,Type),
    (
      Type=global, Object:.Attr=global:.Term
      ;
      Type=oav,    Object:.Attr=Term,
      once ( data(Object,isa,ClassOrObj,_) ; ClassOrObj=Object )
     ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% The Parse Clauses
%
% deduce(Expr,Val) unifies Val with value of Expr.
%
% The following main cases are considered; some use several clauses.
%  Check for some error conditions.	E.g., X  (unbound variable)
%  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.
%  Try a rule.
%  Ask the user.
%  If a proposition, assume false.
%  If all else fails, an item's value is itself.
%

% Check for an unbound expression or object, an error.
%
deduce(Expr,_):-
	( var(Expr) ; Expr=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(_,_,_),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,M,G],	% Extract parts of quantifier cmd.
	var(O),atom(Class),
	member(Amt,[forAll,forEach	% Check for valid quantifier.
	,forSome,forNone]),
	!,				% (Below) Get list of objects.
	setof(O,[M,From]^(data(O,isa,Class,From),deduce(M,true)),Os),
	newName(doAll,Name),		% Make a outcome str. name.
	T=doAllRec(Name,Outcome),	% Make an outcome structure.
	(
	 member(O,Os),			% Get an object.
	 once (deduce(G,Outcome)),	% Test condition on object.
	 once ( T ; asserta(T) ),fail	% Update outcome if new;
	 ; 				%  get next object.
	 true
	),				% (Below) Check outcomes.
	once ( retract(doAllRec(Name,true)),S=t ; true ),
	once ( retract(doAllRec(Name,false)),F=t ; true ),
	once ( 
	  ( Amt=forNone,var(S) ; Amt=forSome,not((var(S),nonvar(T))) ; 
	    Amt=forAll,var(F)  ; Amt=forEach
	  ),!,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(Term,Val):-
    parseOAV(Term,Obj,Attr),	        % Make sure term is OAV.
    data(Obj,Attr,V,_),!,Val=V.		% Retreive data, unify with return.

% Use a rule.
%
deduce(Term,V):-
   getTermType(Term,TermType),	        % Make sure term is OAV or command.
   (
     Rule:if Ante then Term,	        % Consequent a proposition by default.
     Value=true
    ;
     Rule:if Ante then Term:=Value      % Consequent value shown explicitly.
   ),
   deduce(Ante,TV),
   traceRule(Rule,Term,TV,Value),       % Print a trace (debug) message.
   isTV(TV),TV=true,!,			% Evaluate ante., backtrack if false.
   (
     TermType=global, conclude(global:.Term,Value,rule(Rule))
    ;
     TermType=oav,    conclude(Term,Value,rule(Rule))
    ;
     TermType=command                   % Data not saved for commands.
   ),
   V=Value.			

% Ask user about OAV.
%
deduce(Term,Val):-
    getClass(Term,ClassOrObj,Object,Attr),  % Get class.
    props(ClassOrObj,Attr,Question,Valid),  % Get question for attribute. 
    askAndCheck(Question,Object,Valid,Ans), % Ask user...
    conclude(Object:.Attr,Ans,user),	    % ...and assert answer.
    !,Val=Ans.

% If execution reaches this point and Term is a proposition which
% appears in the consequent of at least one rule, then Term is assumed false.
%
deduce(Term,false):-
    getTermType(Term,TermType),
    ( TermType=oav ; TermType=global ),
    _:if _ then Term,!,
    parseOAV(Term,Obj,Attr),
    conclude(Obj:.Attr,false,assumption).

% If a value, just return value.
%
deduce(Term,Term):-isValue(Term),!.

% Term is something that can't be handled.
%
deduce(Term,error):-
    sOut<<"Cannot handle expression "<<<Term<<nl.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Procedures for announcing and writing values, and creating instance names.
%

% Print a message when selected items are found.
%
% Variable Say is item  or instance, variable It is class or item.
%
announce(Term,Val,How):-
    getClass(Term,ClassOrObj,Object,Attr),
    aGoalList(List),
    ( member(ClassOrObj:.Attr,List) ; member(Attr,List) ),
    sOut<<"Item "<<<Term<<" has been shown to have value "<<Val<<" by "
     <<How<<"."<<nl.

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

% 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,Source),	% Print message for user, if wanted.
	asserta(data(O,A,V,Source)).	% Put value into database.

conclude(OA,V,S):-
	sOut<<"Warning, conclude called with inappropriate values:"<<nl
	<<"OA: "<<<OA<<" Value: "<<<V<<" How: "<<<Source<<nl.

% 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)),!.

traceRule(Rule,Cons,AV,CV):-
	traceRule(Rule),		% Okay to trace.
	sOut<<"Rule "<<Rule<<" antecedent is "<<AV<<" with cons. "
	<<Cons<<" value "<<CV<<nl.
traceRule(_,_,_,_).			% If not supposed to trace.

% Askable property for global objects.
%
props(global,Attr,Quest,Valid):-props(Attr,Quest,Valid).

%