% File: lpe.pl
% Authors: Peter Clark and Rob Holte
% Date: updated 24th Feb 1992
% Purpose: Full machinery for lazy partial evaluation (LPE)
%	See README for more information on using LPE
%	See lpe.doc for more documentation on this particular implementation

/*
	========================================
		DEFINED PREDICATES:
		-------------------
	lpe_setup(Functor/Arity)       % set up for LPE for Goal with F/A
        lpe_call(+Goal)		       % evaluate Goal, doing LPE at same time
	lpe_listing(Functor/Arity)     % list current defn of concept with F/A

	set_tracing_mode(+Mode)	       % Mode = {on, off}
	set_learning_mode(+Mode)       % Mode = {lpe, pe, ebg, none}
	========================================

(That's all you need for LPE!)
*/

:- ensure_loaded([utils,kassert]).

:- dynamic learning_mode/1, tracing/1.
learning_mode(lpe).
tracing(off).

% ======================================================================
%		INITIAL SETTING UP FOR LPE
% ======================================================================

% lpe_setup(Functor/Arity).
% Simply copy clauses from the assert to the kassert database. Clauses are
% asserted in the kassert db ordered according to their `quality' (best first).
lpe_setup(F/A) :-
	kabolish(F/A),
	functor(Head, F, A),
	clause(Head, Body),
	tidy_and_split(Body, Op, Nonop),
	ordered_kassert( (Head:-call(Op),Nonop) ),
	fail.
lpe_setup(_).

% ======================================================================
%		I: THE LPE INTERPRETER
% ======================================================================
% Generates a revised concept definition of GenGoal from the (leaves of a) 
% (successful or failed) proof of Goal. It is used by the concept definition
% ordering/execution algorithm (which implements lpe_call/1) below.

lpe(Goal, GenGoal, GenProof) :-
	lpe(Goal, GenGoal, _, GenProof, _).

% lpe(+Goal, +GenGoal, -Proof, -GenProof, -TFFlag).
% Returns (the leaves of) a Proof and a generalised proof (GenProof) of Goal.
% If the proof was successful for Goal, TFFlag = true, if not TFFlag = false.
% The proof process of repeatedly replacing goals with subgoals ([1]) halts 
% immediately it is known that the proof does not apply to Goal ([2]).

lpe((A,B), (GenA,GenB), (ProofA,ProofB), (GenProofA,GenProofB), TF) :-   % [5]
	!,
	lpe(A, GenA, ProofA, GenProofA, TFA),				 % [6]
	(TFA = true -> 	lpe(B, GenB, ProofB, GenProofB, TF)		 % [7]
		    ;   ProofB = B, GenProofB = GenB, TF = false ).	 % [8]
lpe((A;B), (GenA;GenB), Proof, GenProof, TF) :- 
	!,
	( lpe(A, GenA, Proof, GenProof, TF)
	; lpe(B, GenB, Proof, GenProof, TF) ).
lpe(true, true, true, true, true) :-
	!.
lpe(A, GenA, false, GenA, false) :-
	learning_mode(lpe),					% [4]
	operational(GenA),
	\+ call(A),						% [2]
	!.
lpe(A, GenA, A, GenA, true) :-
	operational(GenA),
	!,
	( learning_mode(pe) -> may_succeed(GenA) ; call(A) ).   % [3]
lpe(Goal, GenGoal, Proof, GenProof, TF) :-
	clause(GenGoal, GenBody),				% [1]
	copy((GenGoal:-GenBody), (SpecGoal:-GoalBody)),
	UnificationGoal = (Goal=SpecGoal),
	lpe((UnificationGoal,GoalBody), (true,GenBody), Proof, GenProof, TF).

operational(F) :- \+ predicate_property(F, (dynamic)), !.

% ======================================================================
%	II: THE CONCEPT DEFINITION EXECUTION/ORDERING ALGORITHM
% ======================================================================

% lpe_call(+Goal).
% Like Prolog's call/1 except it also revises clauses for Goal using the LPE.
% lpe_call/1 uses the LPE interpreter above (lpe/3) to generate revised 
% concept definitions as required.
% The data structure for clauses is    Head :- call(OpGoals), NonopGoals.
% See lpe.doc for more information.

lpe_call(Goal) :- 
	learning_mode(none), !, call(Goal).
lpe_call(Goal) :- 
	kclause(Goal, Body, K),				     		 % [1]
	evaluate_body((Goal:-Body), K).

evaluate_body( (_:-call(true), true), _) :- !.
evaluate_body( (_:-call(  Op), true), _) :- !, call(Op).     % operational [2]
evaluate_body(Clause, K) :-
	learning_mode(ebg), !,
	kclause(GenHead, GenBody, K),		        % get copy of clause K
	Clause = ( _ :- call(Op), Nonop ),
	call(Op),
	\+ \+ call(Nonop),				% check is >= 1 proof 
	GenClause = (GenHead:-GenBody),
	expand(Clause, GenClause, NewClause),		% Find a proof & EBG it
	ordered_kassert(NewClause).			% Store learned op defn
evaluate_body(Clause, K) :-
	Clause = ( _ :- call(Op), _ ),
	call(Op), !,				        % Op bit passes    [3]
	kclause(GenHead, GenBody, K),		        % get copy of clause K
	GenClause = (GenHead:-GenBody),
	all_expands_and_kasserts(Clause, GenClause, K), % find all proofs  [4]
	kretract(_, K),				        % del orig. defn,  [5]
	fail.		    	          % bcktrck to [1] continue search [6]

%     -------------------------------------------------------------
%     | EXPANSION: Generate a revised concept definition based on |
%     | replacing non-operational goals in Body with subgoals.    |
%     -------------------------------------------------------------

% find and store all expansions of Clause (has key K)
all_expands_and_kasserts(Clause, GenClause, K) :- 
	expand(Clause, GenClause, NewClause), 
	ordered_kassert(NewClause, K),
	fail.
all_expands_and_kasserts(_, _, _).

% expand(+SpecClause, +GenClause, -NewClause)
% 	SpecClause (`specialised clause') is a Clause for Goal, evaluated as 
%	far as the first non-operational subgoal in its body. 
% expand/3 finds an LPE proof for the remaining subgoals in SpecClause ([1]), 
%       and returns a revised clause (NewClause) for Goal based on this proof.
% See lpe.doc for more information.

expand(SpeClause, GenClause, NewClause) :-
		( tracing(off) -> true 
		; pretty_write(GenClause), write(' expands to...'), nl ),
	SpeClause = (       _ :- call(    _),    Nonop),
	GenClause = ( GenHead :- call(GenOp), GenNonop),
	lpe(Nonop, GenNonop, GenProof),					% [1]
	tidy_and_split(GenProof, ExtraGenOp, NewGenNonop),	        % [2]
	join(GenOp, ExtraGenOp, NewGenOp),                              % [3]
	NewClause = (GenHead :- call(NewGenOp),NewGenNonop),
		write('*'), ttyflush,				% Tracing...
		( tracing(off) -> true 
		; write('	'), pretty_write(NewClause), write('.'), nl ).

%	   --------------------------------------------------------------
%	   | ordered_kassert/{1,2} : Assert a new clause in the kassert |
%   	   | db in the right place, so that the clauses are ordered by  |
%   	   | (upper bound on) quality (best first).                     |
%   	   --------------------------------------------------------------

% ordered_kassert/{1,2}
% Search for the right place to insert NewClause in kassert db, and kassert it.
% [1] search from clause FromK downwards to find the last clause KInsert 
% which is better than NewClause, [2] insert NewClause immediately after 
% (kassertn0/2 and kassertn/2). See lpe.doc for more info.

ordered_kassert((Head:-Body)) :-
	kstartkey(Head, K0),     % get K0 = key of start flag for clauses with
	ordered_kassert((Head:-Body), K0).	  % same functor/arity as Head

ordered_kassert(NewClause, FromK) :-
	place_to_insert(NewClause, FromK, KInsert), !,		% [1]
	kassertn(NewClause, KInsert).				% [2]
ordered_kassert(_, _).				     % already know NewClause

% place_to_insert(+NewClause, +Key, -KeyToInsert)
% Given a NewClause (constructed by LPEing the clause with Key), find where
% to insert it in the domain theory so that clauses are ordered by quality.
place_to_insert(NewClause, K, KInsert) :-
	next_kclause(K, NextK),
	kclause(Head, Body, NextK),
	\+ lpe_better_than(NewClause, (Head:-Body)),   % ie. worse or equal to
	!,
	not_equivalent((Head:-Body), NewClause),
	place_to_insert(NewClause, NextK, KInsert).
place_to_insert(_, K, K).

% ----------
% not_equivalent(+Clause1, +Clause2).
% This allows LPE to ignore definitions it already knows. See not_equivalent/2
% in lpe.doc for more details.
not_equivalent(A, B) :- A \= B, !.
not_equivalent(A, B) :- \+ ( numbervars(A,0,N), numbervars(B,0,N), A=B ). %[1]

% ----------
lpe_better_than(Defn1, Defn2) :-		   % EBG mode only:
	Defn1 = (_:-call(_), true), 		   % = operational defn
	Defn2 = (_:-call(_),Nonop), Nonop \= true, % = non-operational defn
	learning_mode(ebg),			   % EBG: operational defns
	!.            				   % necc. better than nonop 
lpe_better_than(Defn1, Defn2) :-
	quality(Defn1, Q1),
	quality(Defn2, Q2),
	Q1 @< Q2.	% must define Q s.t. Q1 better than Q2 iff Q1 @< Q2

% ======================================================================
% Default (upper bound on) quality of a concept definition = length of the
% operational part (shorter the better). If there's a tie, prefer fully
% operational definitions to non-operational definitions.

quality(Defn, Q-Q2) :-
	Defn = (_ :- call(Op),Nonop),
	clause_length(Op, Q),
	( Nonop = true -> Q2 = 0 ; Q2 = 1 ).  % 2nd order term in case of tie

clause_length((A,B), L) :- !,
	clause_length(A, LA), 
	clause_length(B, LB),
	L is LA + LB.
clause_length(_, 1).

% ======================================================================
%			UTILITIES
% ======================================================================

% may_succeed(+Goal). 
% It is called in PE mode only, to see if there might be a solution to Goal.
% If not then this line of proof is abandoned.
% See lpe.doc for more comments.

may_succeed(Goal) :- \+ \+ pe_evaluate(Goal).

pe_evaluate(\+ Goal) :- \+ is_ground(Goal), !.
pe_evaluate(A \= B) :- \+ is_ground(A \= B), !.
pe_evaluate(nonvar(_)) :- !.
pe_evaluate(_ is B) :- \+ is_ground(B), !.
pe_evaluate(Goal) :- call(Goal).

% --------------------
% tidy_and_split(+Goals, -OpPart, -NonopPart).
% Splits Goals (eg. (a,b,c,d,e)) into its operational part (eg. (a,b)) and
% its `non-operational' part (eg. (c,d,e)), where the `non-operational' part
% is defined as the first non-operational subgoal (eg. c) and all subsequent
% subgoals.
% See lpe.doc for more comments.

tidy_and_split(Proof, Op, Nonop) :-
	tidy_and_split(Proof, Op, Nonop, _).

tidy_and_split((A,B), Op, Nonop, Flag) :-
	!,
	tidy_and_split(A, OpA, NonopA, FlagA),
	( FlagA = true ->		% (NonopA necessarily = true)    % [2]
		tidy_and_split(B, OpB, NonopB, FlagB),
		join(OpA,OpB,Op),  Nonop =  NonopB,       Flag = FlagB
	; 	Op =  OpA, 	   join(NonopA,B,Nonop),  Flag = FlagA ). %[3]
tidy_and_split(A, true, true, true) :- single_soln(A), !, call(A).	 % [4]
tidy_and_split(A, true, true, true) :- can_filter_out(A), !.		 % [6]
tidy_and_split(A,    A, true, true) :- operational(A), !.
tidy_and_split(A, true,   A, false).					 % [1]

single_soln(A) :- is_ground(A), !.					 % [5]
single_soln(_=_).

can_filter_out(_) :- fail.           % (in general, don't filter anything) [7]

% --------------------
% join(+Goal1, +Goals2, -Goals). 
% concatenates Goals1 and Goals2 together.
join(A, true, A) :- !.
join((A,B), C, (A,D)) :- !, join(B, C, D).
join(true, B, B) :- !.
join(A, B, (A,B)).

% ======================================================================
%		LIST THE LPE CLAUSES IN THE KASSERT DATABASE:
% ======================================================================

% lpe_listing(Functor/Arity).
% List the clauses with Head of functor/arity, stored in the kassert db.
% This is a minor variation of klisting/1 in kassert.pl, and filters out
% LPE's `syntactic sugar' of storing clauses `Head:-call(Op),NonOp', instead
% displaying them as Head:-Op,NonOp.

lpe_listing(F/A) :-
	functor(Head, F, A),
	kclause(Head, (call(Op),NonOp)),
	join(Op, NonOp, Body),
	( Body = true -> pretty_write(Head) ; pretty_write((Head:-Body)) ),
	write('.'), nl,
	fail.
lpe_listing(_).

% ======================================================================
%		ADDITIONAL UTILITIES
% ======================================================================

set_tracing_mode(Mode) :-
	member(Mode, [on,off]), !,
	retractall( tracing(_) ),
	assertz( tracing(Mode) ),
	write('Tracing is now '), write(Mode), write('.'), nl.
set_tracing_mode(_) :-
	write('Hey! You can only switch the tracing mode on or off!'),
	nl, fail.

set_learning_mode(Mode) :-
	member(Mode, [lpe,pe,ebg,none]), !,
	retractall( learning_mode(_) ),
	assertz( learning_mode(Mode) ),
	write('Learning mode is now '), write(Mode), write('.'), nl.
set_learning_mode(_) :-
	write('Invalid learning mode! Must be one of lpe, pe, ebg or none.'),
	nl, fail.