module inter_tacs.
accumulate tacticals.

type  report_fail, quit, backup
      goal -> goal -> o.
type  inter_repeat
      (goal -> goal -> o) -> goal -> goal -> o.
type  query, inter
      (goal -> (goal -> goal -> o) -> o) -> goal -> goal -> o.
type  basic_io
      (goal -> o) -> 
      ((goal -> goal -> o) -> o) -> 
      goal -> 
      (goal -> goal -> o) -> o.

%  The inter_repeat tactical allows the user to stop the proof by
%  invoking the quit tactic (resulting in Mid = ff).

inter_repeat Tac In Out :-
   Tac In Mid,
   ((Mid = ff), !, (Out = In);
    maptac (inter_repeat Tac) Mid Outx, goalreduce Outx Out).

% The query tactic asks the user for a tactic to apply. It allows the user
% to back up one step at a time.

query IO In Out :-
   IO In Tac,
   ((Tac = backup), !, fail;
    orelseC Tac report_fail In Out;
    query IO In Out).

inter IO In Out :- inter_repeat (query IO) In Out.

report_fail Goal Goal :- print "Tactic failed.\n".

quit In ff.

basic_io PrintGoal ReadTac Goal Tac :- PrintGoal Goal, ReadTac Tac.