% place_in_oven(Dish,Rack) <--
% Dish should be placed in the correct Rack

place_in_oven(Dish,top) :-
    pastry(Dish), size(Dish,small).
place_in_oven(Dish,middle) :-
    pastry(Dish), size(Dish,big).
place_in_oven(Dish,middle) :-
    main_meal(Dish).
place_in_oven(Dish,low) :-
    slow_cooker(Dish).

pastry(Dish) :- type(Dish,cake).
pastry(Dish) :- type(Dish,bread).

main_meal(Dish) :- type(Dish,meat).

slow_cooker(Dish) :- type(Dish,milk_pudding).

% interact/1 <-- naive interaction of expert system with user
%
interact(Goal) :-
	reset,
	solve1(Goal).

reset :-
	retractall(type(_Dish,_Type)),
	retractall(size(_Sish,_Size)),
	retractall(untrue(_Fact)).

solve1(true).
solve1((A,B)) :-
	solve1(A), solve1(B).
solve1(A) :-
	A \= (_A1,_A2),
	clause(A,B), solve1(B).
solve1(A) :-
	askable(A),
	\+ known(A),
	ask(A,Answer),
	respond(Answer,A).

askable(type(_Dish,_Type)).
askable(size(_Dish,_Size)).

ask(A,Answer) :-
	display_query(A),
	read(Answer).

:- dynamic(type/2).
:- dynamic(size/2).
:- dynamic(untrue/1).

respond(yes,A) :-
	assert(A).
respond(no,A) :-
	assert(untrue(A)),
	fail.

known(A) :- A.
known(A) :- untrue(A).

display_query(A) :-
	write(A), write('? ').


% interact_why/1 <- extends interact/1 by allowing the user
% to ask 'why'
%
interact_why(Goal) :-
	reset,
	solve2(Goal).

solve2(Goal) :-
	solve2(Goal,[]).

solve2(true,_Rules) :-
	!.
solve2((A,B),Rules) :-
	solve2(A,Rules),
	solve2(B,Rules).
solve2(A,Rules) :-
	A \= (_A1,_A2),
	clause(A,B),
	solve2(B,[rule(A,B)|Rules]).
solve2(A,Rules) :-
	askable(A),
	\+ known(A),
	ask(A,Answer),
	respond(Answer,A,Rules).

respond(yes,A,_Rules) :-
	assert(A).
respond(no,A,_Rules) :-
	assert(untrue(A)),
	fail.
respond(why,A,[Rule|Rules]) :-
	display_rule(Rule),
	ask(A,Answer),
	respond(Answer,A,Rules).

display_rule(rule(A,B)) :-
	write('if '), write_conjunction(B), write('then '),
	writeln(A).

write_conjunction((A,B)) :-
	!,
	write(A), write(' and '), write_conjunction(B).
write_conjunction(A) :-
	write(A), nl.

% solve(Goal,Proof) <-- a simple meta-interpreter
% where Proof is the proof of Goal

:- op(900,xfx,<--).

solve(true, true) :-
	!.	
solve((A,B), (ProofA,ProofB)) :-
	!,
	solve(A, ProofA),
	solve(B, ProofB).
solve(A, (A <-- Proof)) :-
	clause(A,B),
	solve(B, Proof).


% how(Goal) <-- explains how Goal was proved
%
how(Goal) :-
	solve(Goal,Proof),
	interpret(Proof).

interpret((Proof1,Proof2)) :-
	interpret(Proof1),
	interpret(Proof2).
interpret(Proof) :-
	fact(Proof,Fact),
	nl, write(Fact), writeln(' is a fact in the database').
interpret(Proof) :-
	rule(Proof,Head,Body,Proof1),
	nl, write(Head), writeln(' is proved using the rule'),
	display_rule(rule(Head,Body)),
	interpret(Proof1).

fact((Fact <-- true),Fact).

rule((Goal <-- Proof),Goal,Body,Proof) :-
	Proof \== true,
	extract_body(Proof,Body).

extract_body((Proof1,Proof2),(Body1,Body2)) :-
	!,
	extract_body(Proof1,Body1),
	extract_body(Proof2,Body2).
extract_body((Goal <-- _Proof),Goal).

% clause_cf <-- clauses with certainty factor
%
clause_cf(place_in_oven(Dish,top),(pastry(Dish), size(Dish,small)),0.7).
clause_cf(place_in_oven(Dish,middle),(pastry(Dish), size(Dish,big)),1).
clause_cf(place_in_oven(Dish,middle),main_meal(Dish),1).
clause_cf(place_in_oven(Dish,low),slow_cooker(Dish),0.5).
clause_cf(Head,Body,1) :-
	clause(Head,Body).

%solve(Goal,Certainty) <-- Certainty is confidence in Goal

solve3(true,1).
solve3((A,B),C) :-
	solve3(A,C1),
	solve3(B,C2),
	minimum(C1,C2,C).
solve3(A,C) :-
	clause_cf(A,B,C1),
	solve3(B,C2),
	C is C1 * C2.

minimum(X,Y,Z) :-
	X =< Y,
	!,
	Z = X.
minimum(X,Y,Y).

:- minimum(2,5,5).