% Procedure		hole_antwort/3
% -- mit assert mod --
% Procedure		useranswer(Goal, Trace, Answer)
% (Bratko, Fig 15.7)
%
% generates, through backtracking, user-supplied solutions to Goal.
% Trace is a chain of ancestor goals and rules for 'why' explanation.
%
% 'askable' sollte gemaess Ihrer Modellierung definiert werden
% nach Bratko Vorlage  / -am-

% this part assumes
:- op(900, xfx, :).
:- op(800, xfx, was).
:- op(880, xfx, '-->').
:- op(300, fx, 'derived by').
:- op(600, xfx, from).
:- op(600, xfx, by).


% 
% Bratko

getreply(Reply) :- 
  read(Answer),
  ameans(Answer, Reply),!		% answer means s.th. ?
  ;
  nl, write('Answer unknown, try again please'),nl,
  getreply(Reply).

ameans( yes, yes).
ameans( y, yes).
ameans( no, no).
ameans( n, no).
ameans( why, why).
ameans( w, why).



% damits Deutsch mundet :-)
hole_antwort( Goal, Trace, Answer ) :-
  useranswer( Goal, Trace, Answer ). 

useranswerInit :-			% keep Quintus happy
  assert(wastold([],true,0)),		% this is a true hack, not
  assert(end_answers([])),		% as in Bratko :-)
  assert(lastindex(0)).			% first index for 'wastold'

useranswer( Goal, Trace, Answer ) :-
  askable( Goal, _),			% May be asked of the user
  freshcopy( Goal, Copy ),		% Variables in Goal renamed
  useranswer( Goal, Copy, Trace, Answer, 1).

% do not ask again about an uninstantiated goal

useranswer(Goal, _,_,_, N) :-
  N > 1,				% Repeated question ?
  instantiated(Goal),!,			% No variables in Goal
  fail.					% Donot ask again

% Is Goal implied true or false for all instantiations?

useranswer( Goal, Copy, _, Answer, _) :-
  wastold( Copy, Answer, _ ),
  instance_of( Copy, Goal ), !.		% Answer to Goal implied

% retrieve known solutions, indexed from N on, for Goal

useranswer( Goal, _,_, true, N) :-
  wastold(Goal,true,M),
  M>=N.

% has everything already been said about Goal?

useranswer(Goal, Copy, _, Answer, _) :-
  end_answers( Copy ),
  instance_of(Copy, Goal), !,		% Everything was already said about Goal
  fail.

% ask the user for (more) solutions

useranswer(Goal, _, Trace, Answer, N) :-
  askuser( Goal, Trace, Answer, N).

askuser( Goal, Trace, Answer, N) :-
  askable(Goal, ExternFormat),
  format(Goal, ExternFormat, Question, [], Variables),	% Get question format
  ask( Goal, Question, Variables, Trace, Answer, N).

ask(Goal, Question, Variables, Trace, Answer, N) :-
  nl,
  ( Variables = [], !,
    write('Is it true: ')				% Introduce question
    ;
    write('Any (more) solution to:')
  ),
  write( Question), write('? '),
  getreply(Reply),!,					% Reply = yes/no/why
  process( Reply, Goal, Question, Variables, Trace, Answer, N).

process( why, Goal, Question, Veriables, Trace, Answer, N) :-
  showtrace(Trace),
  ask(Goal, Question, Variables, Trace, Answer,N).

process( yes, Goal, _, Variables, Trace, true, N) :-
  nextindex(Next),					% Get new free index for 'wastold'
  Next1 is Next+1,
  (askvars(Variables),
   assertz( wastold(Goal,true,Next) )			% Record solution
   ;
   freshcopy(Goal,Copy)	,				% Copy of Goal
   useranswer(Goal,Copy,Trace, Answer,Next1)		% More answers?
  ).

process(no, Goal, _,_,_, false, N) :-
  freshcopy(Goal,Copy),
  wastold(Copy, true, _), !,				% 'no' means: no more solutions
  assertz( end_answers(Goal) ),				% Mark end of answers
  fail
  ;
  nextindex(Next),					% Next free index for 'wastold'
  assertz(wastold(Goal,false,Next)).			% 'no' means: no solution

format(Var, Name, Name, Vars, [Var/Name | Vars]) :-
  var(Var),!.

format(Atom,Name,Atom, Vars,Vars) :-
  atomic(Atom),!,
  atomic(Name).

format(Goal,Form,Question,Vars0,Vars) :-
  Goal =.. [Functor|Args1],
  Form =.. [Functor|Forms],
  formatall(Args1,Forms,Args2,Vars0,Vars),
  Question =.. [Functor|Args2].

formatall([],[],[],Vars,Vars).

formatall([X|XL],[F|FL],[Q|QL],Vars0,Vars) :-
  formatall( XL,FL,QL,Vars0,Vars1),
  format(X,F,Q,Vars1,Vars).

askvars([]).

askvars([Variable/Name|Variables]) :-
  nl, write(Name), write(' = '),
  read(Variable),
  askvars(Variables).

showtrace([]) :-
  nl,write('This was your question'),nl.

showtrace( [Goal by Rule | Trace] ) :-
  nl, write('To investigate, by '),
  write(Rule), write(', '),
  write(Goal),
  showtrace(Trace).

instantiated(Term) :-
  numbervars(Term,0,0).				% No variables in Term

% instance_of(T1,T2): instance of T1 is T2; that is,
% term T1 is more general than T2 or equally general as T2

instance_of(Term,Term1) :-			% Instance of Term is Term1
  freshcopy(Term1,Term2),			% Copy of Term1 with fresh set of variables
  numbervars(Term2,0,_),!,
  Term=Term2.					% This succeeds is Term1 is instance of Term

freshcopy(Term, FreshTerm) :-			% Make a copy of Term with variables renamed
  asserta(copy(Term)),
  retract(copy(FreshTerm)),!.


nextindex(Next) :-				% Next free index for 'wastold'
  retract(lastindex(Last)),!,
  Next is Last + 1,
  assert(lastindex(Next)).