% -----------------------------------------------------------------------------
%  (C) Altran Praxis Limited
% -----------------------------------------------------------------------------
% 
%  The SPARK toolset is free software; you can redistribute it and/or modify it
%  under terms of the GNU General Public License as published by the Free
%  Software Foundation; either version 3, or (at your option) any later
%  version. The SPARK toolset is distributed in the hope that it will be
%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
%  Public License for more details. You should have received a copy of the GNU
%  General Public License distributed with the SPARK toolset; see file
%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
%  the license.
% 
% =============================================================================


/******** CASES: top-level checker command ********/
cases :-
        (
           command_arg(on, Formula)
        ;
           prompt_user('Type hypothesis no. or cases formula...','CASES> '),
           rread(F),
           parse_expression(F, Formula)
        ),
        !,
        cases(Formula), !.

cases(F) :-
        (
           F=h#N,
           integer(N)
        ;
           valid(F),
           no_qvars_in(F),
           free_hyp_no(N),
           add_new_hyp(F,N)
        ),
        !,
        do_cases(N),
        !.

/*** FREE_HYP_NO(N) - returns smallest N for which no hypothesis exists ***/
free_hyp_no(N) :-
        find_first_free_starting_at(1, N).


/*** find_first_free_starting_at(Start, Num) -- return the number of the
     smallest vacant hypothesis number Num counting from Start upwards. ***/

find_first_free_starting_at(S, S) :-
        \+ hyp(S, _),
        !.

find_first_free_starting_at(S, N) :-
        NewS is S+1,
        !,
        find_first_free_starting_at(NewS, N).




/*** DO_CASES(N) - use hypothesis N as case-generator & invoke case-proof ***/
do_cases(N) :-
   hyp(N,F),
   no_qvars_in(F),
   command_arg(expression, EXPRN),
   nonvar(EXPRN),
   (
      EXPRN = c#CONCNO,
      conc(CONCNO, FORMULA)
   ;
      novars(EXPRN),                                            /* CFR009 */
      checktype(EXPRN, boolean),                                /* CFR009 */
      FORMULA = EXPRN,
      CONCNO = []
   ),
   case_pointer(CP),
   C is CP+1,
   retractall(case(C,_,_)),
   save_cases(C,F),
   retractall(case_pointer(_)),
   retractall(on_case(C,_,_)),
   assertz(logfact(enterframe, C)),
   assertz(case_pointer(C)),
   retractall(proved_for_case(C,_)),
   free_hyp_no(HN),
   assertz(on_case(C,1,HN)),
   case_save(C),
   retractall(subgoal_formula(C,_,_,_)),
   assertz(subgoal_formula(C, FORMULA, CONCNO, 'CASES')),
   case(1).


/*** VALID(F) - checks if F covers all integers for some subexpression
                or if F is basically "X or not X" for some formula X   ***/
valid(A or (not A)) :- !.
valid((not A) or A) :- !.
valid(A or B) :-
   norm_typed_expr((not A)<->B,boolean,true),
   !.
valid(F) :-
   covers_interval(F,E,L,U),
   (
      L=[]
   ;
      infer(E>=L)
   ),
   (
      U=[]
   ;
      infer(E<=U)
   ), !.


/*** COVERS_INTERVAL(F,E,L,U) - expression E ranges over L..U in F ***/
covers_interval(F1 and F2,E,L,U) :- find_range(F1 and F2,E,L,U).

covers_interval(E=N,E,N,N).

covers_interval(N=E,E,N,N).

covers_interval(E<N,E,[],N-1).

covers_interval(N>E,E,[],N-1).

covers_interval(E<=N,E,[],N).

covers_interval(N>=E,E,[],N).

covers_interval(E>N,E,N+1,[]).

covers_interval(N<E,E,N+1,[]).

covers_interval(E>=N,E,N,[]).

covers_interval(N<=E,E,N,[]).

covers_interval(A or B,E,L,U) :-
   covers_interval(A,E,L1,U1),
   covers_interval(B,E,L2,U2),
   combine_intervals(L1,U1,L2,U2,L,U).


/*** FIND_RANGE(CONJ,E,L,U) - find E in CONJ covering L..U in CONJ ***/
find_range(F1 and F2,E,L,U) :-
   covers_interval(F1,E,L1,U1),
   covers_interval(F2,E,L2,U2),
   find_max(L1,L2,L),
   find_min(U1,U2,U),
   infer(L<=U).


/*** FIND_MAX(N1,N2,N) - find N in {N1,N2} s.t. N>=N1 and N>=N2 ***/
find_max(N1,N2,N) :-
   (
    intexp(N1),
    (
       intexp(N2),
       (
          N1>=N2,
          N is N1
       ;
          N2>N1,
          N is N2
       )
    ;
       V is N1,
       (
          infer(V>=N2),
          N=V
       ;
          infer(N2>=V),
          N=N2
       )
    )
   ;
    intexp(N2),
    V is N2,
    (
       infer(N1>=V),
       N=N1
    ;
       infer(V>=N1),
       N=V
    )
   ;
    infer(N1>=N2),
    N=N1
   ;
    infer(N2>=N1),
    N=N2
   ), !.


/*** FIND_MIN(N1,N2,N) - find N in {N1,N2} s.t. N<=N1 and N<=N2 ***/
find_min(N1,N2,N) :-
   (
    intexp(N1),
    (
       intexp(N2),
       (
          N1>=N2,
          N is N2
       ;
          N2>N1,
          N is N1
       )
    ;
       V is N1,
       (
          infer(V>=N2),
          N=N2
       ;
          infer(N2>=V),
          N=V
       )
    )
   ;
    intexp(N2),
    V is N2,
    (
       infer(N1>=V),
       N=V
    ;
       infer(V>=N1),
       N=N1
    )
   ;
    infer(N1>=N2),
    N=N2
   ;
    infer(N2>=N1),
    N=N1
   ), !.


/*** COMBINE_INTERVALS(L1,L2,U1,U2,LRes,URes) - combine L1..L2 & L2..U2 ***/
combine_intervals(L1,U1,U1,U2,L1,U2) :- U1\=[].

combine_intervals(U1,U2,L1,U1,L1,U2) :- U1\=[].

combine_intervals(L1,L2-1,L2,U2,L1,U2).

combine_intervals(L2,U2,L1,L2-1,L1,U2).

combine_intervals(L1,L2,L2+1,U2,L1,U2).

combine_intervals(L2+1,U2,L1,L2,L1,U2).

combine_intervals(L1,U1,L2,U2,L2,U1) :-
   U2\=[],
   L1\=[],
   (
      norm_typed_expr(U2+1>=L1,boolean,true)
   ;
      infer(U2+1>=L1)
   ;
      infer(U2>=L1-1)
   ;
      infer(L1<=U2)
   ).

combine_intervals(L1,U1,L2,U2,L1,U2) :-
   U1\=[],
   L2\=[],
   (
      norm_typed_expr(U1+1>=L2,boolean,true)
   ;
      infer(U1+1>=L2)
   ;
      infer(U1>=L2-1)
   ;
      infer(L2<=U1)
   ).

combine_intervals(L1,_U1,L2,U2,L2,U2) :-
   L1\=[],
   L2\=[],
   (
      norm_typed_expr(L2<=L1,boolean,true)
   ;
      infer(L2<=L1)
   ).


/******** STATUS: top-level checker command ********/
status :-
   nl,
   case_pointer(CP),
   CP>0,
   write('[DEPTH: '),
   print(CP),
   write(']'),
   nl,
   subgoal_formula(CP,F,_N,METHOD),
   print(METHOD),
   write(': '),
   print(F),
   nl,
   list_case_status(CP),
   !.
status :-
   case_pointer(0),
   write('[TOP-LEVEL]'),
   nl,
   !.
status :- !.


list_case_status(CP) :-
      case(CP,N,_F),
      (
         proved_for_case(CP,N),
         write('*** PROVED FOR CASE '),
         print(N),
         nl
      ;
         (\+ proved_for_case(CP,N)),
         write('<Case '),
         print(N),
         write(' pending>'),
         nl
      ),
      fail.
list_case_status(_) :- !.


/******** ABORT_CASE: top-level checker command ********/
abort_case :-
   case_pointer(CP),
   CP>0,
   on_case(CP,_,HN),
   retractall(on_case(CP,_,_)),
   retract(hyp(HN,_)),
   retractall(case(CP,_,_)),
   retractall(proved_for_case(CP,_)),
   retractall(case_pointer(_)),
   C is CP-1,
   NC is C-1,
   assertz(case_pointer(NC)),
   case_restore(C),
   !.


/******** CASE: top-level checker command ********/
case :-
        (
           command_arg(case_number, N)
        ;
           prompt_user('Which case? '),
           rread(N),
           integer(N)
        ),
        !,
        case(N),
        !.

case(N) :-
   case_pointer(CP),
   case(CP,N,F),
   nl,
   write('CASE '),
   print(N),
   write(': '),
   print(F),
   nl,
   on_case(CP,_,HN),
   case_restore(CP),
   assertz(hyp(HN,F)),
   new_hyp_message(HN, F),                                      /* CFR018 */
   retractall(conc(_,_)),
   subgoal_formula(CP, FORMULA, _, _),
   assertz(logfact((case), N)),
   assertz(logfact(newhyp, hyp(HN, F))),
   clear_up_could_facts,
   format_formula(logmessage, true -> FORMULA),                     /* CFR054 */
   retractall(on_case(CP,_,HN)),
   assertz(on_case(CP,N,HN)), !.


/*** SAVE_CASES(CP,CG) - save cases in formula CG as cases at depth CP ***/
save_cases(CP,X or Y) :-
   save_cases(CP,X),
   save_cases(CP,Y), !.

save_cases(CP,F) :- add_new_case(CP,1,F), !.


/*** ADD_NEW_CASE(CP,N,F) - add formula F as case N at depth CP ***/
add_new_case(CP,N,F) :-
   case(CP,N,_),
   M is N+1,
   add_new_case(CP,M,F), !.

add_new_case(CP,N,F) :- assertz(case(CP,N,F)), !.


/*** SAVE(LABEL) - save current VC as LABEL for future recall ***/
case_save(CP) :-
   retractall(saved_vc(CP,_)),
   case_save(CP,hyp(_,_)),
   case_save(CP,conc(_,_)),
   case_save(CP,forgotten(_)),
   case_save(CP,deleted(_)),
   case_save(CP,deleted_hyp(_,_)),
   case_save(CP,qvar(_)), !.

case_save(CP,X) :-
   call(X),
   assertz(saved_vc(CP,X)),
   fail.

case_save(_,_).


/*** case_restore(LABEL) - recall a previously-saved VC state ***/
case_restore(CP) :-
   retractall(hyp(_,_)),
   retractall(conc(_,_)),
   retractall(forgotten(_)),
   retractall(deleted(_)),
   retractall(deleted_hyp(_,_)),
   retractall(qvar(_)),
   restore_vc(CP), !.

restore_vc(CP) :-
   saved_vc(CP,Fact),
   assertz(Fact),
   fail.

restore_vc(_).
%###############################################################################
%END-OF-FILE