/*  INDUCTION

  copyright 1993-2001,  P. H. Roosen-Runge

Uses simplification and Wang's algorithm to attempt to verify
simple recursive programs expressed as
         F(Arg) = if(Arg, Initial, Result)
with respect to a Goal.

Here
         F = function name,
        Arg = name of the integer argument,
        Initial = F(0),
        Expression = F(Arg) if Arg <> 0.

The input to induction is a term  in one of the following forms:

  (1)  F(Integer) = if(Integer=0, Initial, Result) : Goal.
where Goal = desired mathematical value of F(Integer) for Integer >=
0.

Example: f(n) = if(n=0, 0, f(n-1) + m) : n*m.

  (2a)   F(Stack) = if(Stack = nil, Initial, Result) : Goal
  (2b)   F(List) = if(List = [], Initial, Result) : Goal

  (3)    tail(if(V=0, Result, F(Reduce(V), C(V, Result))):Goal,
              Identity).

Example: tail(if(n=0,s,sum(n-1,s+n)):n* (n+1)/2,0)

A special form which 'counts up' is also acceptable:

         tail(if(Index = V, Result, F(Index+1, C(Index, Result))):
              Goal, Identity).

  (4)  F(Tree) = if(Tree = nilTree, Initial, Result) : Goal.

Only meaningful example I can find:

       leaves(t) = if(t = nilTree, 1, leaves(left(t))+leaves(right(t))) :
           1 + nodes(t).
*/
% Version 1.1, Dec. 29, 1993: induction over stacks
%         2.1  Dec. 20, 1998: transform tail-recursion into simple recursion
%         2.2  Jan. 10, 1999: added error-checking for tail-recursion
%         2.4  Feb. 22: supports gen. induction; allows any "assert(Rule)"
%         2.4.3 January 2, 2000: recompiled with getTheories, v. 2.0
%         2.4.4 February 7: asserts that the induction variable is a nat.
%         2.5  Feb. 13: special form for counting-up for-loops
%         2.5.1 March 21: recompiled with simp, v. 2.1
%         2.6 April 15: identity test repaired
%         2.6.1 September 1: recompiled with condtrans.prolog
%         2.6.2 September 14: test for identity rather than left-identity
%                 (Is Kubiak wrong?)
%         2.7   October 31: goal substitution (finally, really) fixed
%         2.7.1 November 10: recompiled with simp v 3.1.1 to catch
%               circular recursive simplification rules.
%         2.8  Jan. 25, 2002: added induction over binary trees
%         2.9SWI Feb. 12, 2007: SWI version
%====================================================================
 
:- multifile '->>'/2. :- dynamic '->>'/2.

% uses paths from .plrc
:-ensure_loaded([qlib(arg), qlib(change_arg), qlib(occurs)]).
:-ensure_loaded([lib('simp.pl'), lib('equtaut.pl'), lib('getTheories.pl')]).

error(Message) :- nl, write('!! '), write(Message), nl, halt.

activate :-
        write('Version 2.9SWI, February 12, 2007'), nl,
        op(400, yfx, mod),  %  960 in SWI ??
	fileerrors(OldFlag, off),
        getTheories,
	proveTerms,
        fileerrors(_, OldFlag)
     ;
        nl, error('Something wrong.'), nl, halt.

proveTerms :- read(T),
       ( T==end_of_file -> halt
        ;
         T=theory(File), theory(File)
        ;
         T=assert(Rule), addRule(Rule)
        ;
         nl, write(T), nl, verify(T), nl
        ),
        proveTerms.

verify(LHS = if(Arg=0, Initial, Expression) : Goal) :-
	functor(LHS, F, Arity),
	(
	 arg(1, LHS, Arg), nonvar(Arg)
        ;
	 error('Error in recursion argument.')
	),
	assert(nat(Arg)),
	substitutex(0, Arg, Goal, Goal0),
	nl, write('Base case: '),
	try(Goal0 = Initial), !, % base case for the induction.
	instep(LHS, Expression, Arg, Goal, Step),
        nl, write('Inductive step: '),
        try(Goal = Step).
      
verify(LHS = if(Arg=nil, Initial, Expression) : Goal) :-
	LHS =.. [F, Arg | Rest],
        substitutex(nil, Arg, Goal, Goal0),
	nl, write('Base case: '),
        try(Goal0 = Initial), !, % base case for the induction.
        substitutex(pop(Arg), Arg, Goal, Goal1),
        FA1 =.. [F, pop(Arg) | Rest],
        substitutex(Goal1, FA1, Expression, Exp1), % inductive hypothesis.
        nl, write('Inductive step: '),  
        try(Goal = Exp1). 

verify(LHS = if(leaf(Arg), Initial, Expression) : Goal) :-
        LHS =.. [F, Arg | Rest],
        nl, write('Base case: '),
        try(leaf(Arg) implies Goal = Initial), !, 
              % base case for the induction.
        substitutex(left(Arg), Arg, Goal, Goal1),
        FA1 =.. [F,left(Arg) | Rest],
        substitutex(Goal1, FA1, Expression, Exp1), % inductive hypothesis.
        nl, write('Inductive step: '),
	substitutex(right(Arg), Arg, Goal, Goal2),
        FA2 =.. [F, right(Arg) | Rest],
        substitutex(Goal2, FA2, Exp1, Exp2), % inductive hypothesis.
	try(Goal = Exp2).

verify(LHS = if(Arg=[], Initial, Expression) : Goal) :-
        LHS =.. [F, Arg | Rest],
        substitutex([], Arg, Goal, Goal0),
        nl, write('Base case: '),
        try(Goal0 = Initial), !, % base case for the induction.
        substitutex(rest(Arg), Arg, Goal, Goal1),
        FA1 =.. [F, rest(Arg) | Rest],
        substitutex(Goal1, FA1, Expression, Exp1), % inductive hypothesis.
        nl, write('Inductive step: '),
        try(Goal = Exp1). 

verify(tail(Definition: Goal, Identity)) :-
        tail(Definition, Identity, Left = Naive) ->
	Def = (Left = Naive : Goal),
	nl, write('Verifying: '), write(Def),
        verify(Def).

verify(_) :-	nl, write('!! Cannot recognize input format.').

% call this (Args, LHS, Arity, 1, Goal, Result).	
subArgsInGoal(Args, LHS, Arity, N, Goal, Result) :-
	N =< Arity,
	arg(N, LHS, A), 
	item(N, Args, Arg), 
	substitutex(Arg, A, Goal, Modified),
	N1 is N+1,
	subArgsInGoal(Args, LHS, Arity, N1, Modified, Result).
subArgsInGoal(_, _, _, _, Result, Result).

subGoalForF(LHS, Path,Goal,  Expression, Result) :-
	functor(LHS, F, Arity),
	path_arg(Path, Expression, Call),
	Call =.. [F|Args],
	subArgsInGoal(Args, LHS, Arity, 1, Goal, ModGoal),
	change_path_arg(Path, Expression, _, Result, ModGoal).
	
subGoalForCalls(LHS, Goal, Expression, Result) :-
	functor(LHS, F, Arity),
	setof(Path, Match^(path_arg(Path, Expression, Match), 
		     functor(Match, F, Arity)), Calls),
% any better way to find these paths than to try them all?
        subGoalForFs(LHS, Goal, Expression, Calls, Result).

subGoalForFs(_, _, Expression, [], Expression).
subGoalForFs(LHS, Goal, Expression, [Call | Rest], Result) :-
	subGoalForF(LHS, Call, Goal, Expression, Modified),
	subGoalForFs(LHS, Goal, Modified, Rest, Result).

item(1, [X|_], X) :- !.
item(N, [_| Rest], X) :- N>1, N1 is N-1, item(N1, Rest, X).

/*
subInGoal(N, LHS,  Lists, Goal, Expression, Result) :-
	functor(LHS, _, Arity), N =< Arity,
	subInGoalforArg(N, LHS, Lists, Goal, Expression, Modified),
	N1 is N+1, 
	subInGoal(N1, LHS, Lists, Goal, Modified, Result).
subInGoal(_, _, _, _, Expression, Expression).

subInGoalforArg(N, LHS, [List | Rest], Goal, Expression, Result) :-
	arg(N, LHS, A),
	functor(LHS, F, _),
	path_arg(Path, Expression, Term),
	functor(Term, F, _), arg(N, Term, X),
	changeAll(List, X, Goal, ModifiedGoal),
	change_path_arg(Path, Expression, NewExpression, ModifiedGoal),
	!,
	subInGoalforArg(N, LHS, Rest, Goal, NewExpression, Result).
subInGoalforArg(_, _, _, _, Expression, Expression).
*/


instep(LHS, Expression, Arg, Goal, Result) :-
	functor(LHS, F, Arity),
	varList(Arity, VarList),
	Template =..  [F | VarList],
	arg(1, Template, V),
	findall(V, sub_term(Template, Expression), Vs),
	sort(Vs, Exps),
        (
	 checkBounds(Exps, F, Expression, Arg) 
        ; 
	 error('Error in function argument.')
	),
	(
	 Arity = 1 -> substituteArgs(Exps, Goal, Arg, Goals),
	 substituteGoals1(Goals, Exps, F, Expression, Result)
	   % substitute function args for induction variable in Goal
	   % substitute Goal for F(Exp)
	;
	 subGoalForCalls(LHS, Goal, Expression, Result)
        ).

varList(0, []).
varList(Arity, [_ | Rest]) :- A1 is Arity - 1, varList(A1, Rest).

firstArg(V, Template, Expression) :-
	arg(1, Template, V), sub_term(Template, Expression).

checkBounds([], _, _, _).
checkBounds([Arg - 1 | Rest], F, Expression, Arg) :-
	checkBounds(Rest, F, Expression, Arg).
checkBounds([Term | Rest], F, Expression, Arg) :- 
	(
	 sub_term(if(B, If, Else), Expression),
	 (
	  sub_term(Term, If),
	  try(0 < Arg and B implies 0 <= Term and Term < Arg)
	 ;
	  sub_term(Term, Else),
	  try(0 < Arg and not B implies 0 <= Term and Term < Arg)  
	 )
	;
         try(0 <= Term and Term < Arg)
	),
	checkBounds(Rest, F, Expression, Arg).  


	
substituteArgs([], _, _, []).
substituteArgs([Exp | Rest], Goal, Arg, [G | Goals]) :-
       substitutex(Exp, Arg, Goal, G),
       substituteArgs(Rest, Goal, Arg, Goals).
/*
% for F(Args) in the recursive expression, subArgs creates an
% equivalent goal (assuming the premises of the induction step.)

subArgs(_, [], Goal, Goal).
subArgs([P |RestP], [A | RestA], Goal, NewGoal) :-
       substitutex(A, P, Goal, Modified),
       subArgs(RestP, RestA, Modified, NewGoal).
*/

subGoals([], _, _, _, _, Expression, Expression).
subGoals([Exp | Rest], F, V, Arity, Goal, Expression, Result) :-
	substitutex(Exp, V, Goal, EGoal),
	substituteGoal(EGoal, F, Arity, Exp, Expression, New),
	subGoals(Rest, F, V, Arity, Goal, New, Result).

substituteGoal(EGoal, F, Arity, Exp, Expression, Result) :-
	path_arg(Path, Expression, Term),
	functor(Term, F, Arity),
	arg(1, Term, Exp),
	change_path_arg(Path, Expression, Modified, EGoal),
	!,
	substituteGoal(EGoal, F, Arity, Exp, Modified, Result).
substituteGoal(_, _, _, _, Expression, Expression).

substituteGoals1([], _,  _, Exp, Exp).
substituteGoals1([G | Goals], [Ex | Rest], F, Expression, Exp)  :-
	Fex =.. [F, Ex],
	substitutex(G, Fex, Expression, Exp1),
	substituteGoals1(Goals, Rest, F, Exp1, Exp).

% once again, based on the waterfall predicate, QP Library manual.
% but far from optimal?
substituteFunctor(F, G, Arity, Expression, Result) :-
	path_arg(Path, Expression, Term),
	change_functor(Term, F, New, G, Arity), 
	change_path_arg(Path,  Expression, _, Modified, New),
	!,
	substituteFunctor(F, G, Arity, Modified, Result).
substituteFunctor(_, _, _, Expression, Expression).

tail(if(A1 = A2, Terminal, G), Identity, Naive) :-
	G =.. [F, Index + 1, C, V],!,
	(A1 = V, A2 = Index ; A2 = V, A1 = Index),
	substitutex(V, Index, C, C1),
	G1 =..[F, V - 1, C1],
	tail(if(V = 0, Terminal, G1), Identity, Naive).

tail(if(A, Terminal, G), Identity, Naive) :-
       (
        \+atom(Terminal), error('The result argument must be a variable.'),
        !, fail
       ;
       Final = Identity,
       findvar(A, X),
       G =.. [F, E, C],functor(C, CFun, Arity),
       (Arity = 2 ->
        nl, write('Assume '), write(CFun), write(' is associative. '), nl,
        Arg =.. [F, E],
           % E =.. should involve X, but we don't check
        Left =.. [F, X],
       (
	findTerm(X, Terminal, C, D), contains_term(X, D), Path=[]
       ;
        findTerm(X, Terminal, C, D), path_arg(Path, C, D)
       ), !,
        substitutex(Identity, Terminal, C, IT),
	subForD(X, Path, 'X', D, IT, Ident),
	substitutex('X', Terminal, C, IT2),
	subForD(X, Path, Identity, D, IT2, Ident2),
        try(Ident = 'X'), try(Ident2 = 'X'),
        swapArgs(D, Terminal, C, CR),
	substitutex(Arg, Terminal, CR, Recurse),
        Naive = (Left = if(A, Final, Recurse))
       ;
        nl, write('Error! '), 
	write(C), 
	write(' doesn''t have the right structure for transformation.'),
	halt
       )).

tail(_, _, _) :-
        error('Something wrong in tail-recursion definition.').

subForD(N, Path, New, D, Old, Result) :-
	contains_term(N, D),
	substitutex(New, D, Old, Result)
       ; 
	path_arg(Path, Old, D),
	change_path_arg(Path, Old, Result, New).
 
findvar(X=_, X) :- functor(X, _, 0), \+number(X).
findvar(_=X, X) :- functor(X, _, 0), \+number(X).
findvar(A, X) :-
        A =.. [_, Y],
           (functor(X, _, 0) -> X=Y
            ;
            findvar(Y, X)
           ).          

findTerm(X, Result, Term, Sub) :-
	sub_term(Sub, Term ), 
	free_of_term(Result, Sub).

        
try(T) :- simplify(T, SimpT),
        ( tautology(SimpT), write(T), write(' is valid.'), nl
         ;
          nl, write('Cannot prove '), write(SimpT), write('.'), nl
        ).

swapArgs(A, B, C, Result) :-
	substitutex('DUMMY'(A), A, C, CA),
        substitutex('DUMMY'(B), B, CA,CAB),
        substitutex(B, 'DUMMY'(A), CAB, CB),
        substitutex(A, 'DUMMY'(B), CB, Result).
 
substitutex(V, R, G, W) :-
        setof(Path,path_arg(Path, G, R), Paths),
        changeAllx(Paths, V, G, W), !.
substitutex(_, _, G, G).

changeAllx([Path | Rest], V, G, W) :-
        change_path_arg(Path, G, Modified, V),
        changeAll( Rest, V, Modified, W).
changeAllx(_, _, G, G).    


                                     

