/*  CONTROL.PL  */

/*
:- module control.


:- public non_binding_call/1,
          call_without_failure/1,
          once/1,
          forall/2,
          while/2,
          for/5,
          for/3,
          for/2,
          for_in_list/3,
          for_in_list/4,
          for_reverse_in_list/3.
*/


/*
SPECIFICATION
-------------

The Tutor frequently needs to perform some action for each solution
of a goal, or for each element of a list, or as long as a
particular condition holds. There is an advantage to building predicates
to encapsulate such loops, hiding the (often messy) details of how they
are implemented. It saves programmer time; and it makes for more legible
programs, for the same reason that
    FOR I = 1 TO 20 BY 2 DO PRINT(I)
is easier to read then
        I = 1
    1:
        IF I > 20 THEN GOTO 2
        PRINT(I)
        I = I + 1
        GOTO 1
    2:
The function of the code is made explicit instead of being distributed
amongst smaller components. This is one of the themes of ``Software
Tools'', the authors of which present a pre-processor that translates
loops and other control constructs written in Ratfor, a ``rational
version of Fortran'' into Fortran. (There is much to be said for
treating Fortran as fit only for automatic generation; it is certainly
not a suitable tool for human use.)

This module does the same job for Prolog, but encapsulates the gory
details of cuts and other low-level control inside predicates, rather
than using a pre-processor.


In more detail, 'once', 'call_without_failure' and 'non_binding_call'
alter the way goals are called. For example, 'once' (you may already
have it on your system) makes a goal non-resatisfiable.

Finally, there is a selection of looping predicates, for packaging up
'repeat'...'fail' loops and others. Some of these are similar to some
described in Tony Dodd's book "Prolog: A Logical Approach". Note that,
unlike him, I don't define any of the predicate names as operators. This
is to avoid interfering with names that the user of the Tutor might pick
on.


All these predicates have a goal as one of their arguments. If you are
using a cross-referencer, you may have to tell it that they do. For
example, if you call
    once( all_solns(G,S) )
the cross-referencer will have no more reason to think that 'all_solns'
is a predicate than it does in seeing
    write( all_solns(G,S) ).
And if all_solns/2 is undefined, the cross-referencer will not detect
that fact. However, you will probably have some way of telling it that
'once' actually takes something to be called. The same caution applies
to other program-analysis programs.


PUBLIC non_binding_call( Goal+ ):
Calls Goal and succeeds or fails accordingly. But does not make any variable
bindings, so even if Goal succeeds, its variables are in the same state
after the call as before.

Example:
    non_binding_call( (I=2,J=3,I=J) )  --  fails.
    non_binding_call( (I=2,J=2,I=J) )  --  succeeds, leaving I and J
                                           unbound.



PUBLIC once( Goal+ ):
Calls Goal and succeeds or fails accordingly, but is not resatisfiable.

Example:
Given the facts a(1), a(2), a(3), then
    once(( a(X), write(X) )), fail
writes 1 and then fails.


PUBLIC call_without_failure( Goal+ ):
Calls Goal and always succeeds. Not resatisfiable.


PUBLIC forall( Cond+, Goal+ ):
'forall' calls Goal for each resatisfaction of Cond, and then succeeds.
If Goal fails, the action is undefined ('forall' will call 'bug'). Not
resatisfiable. All variables in Cond and Goal are unbound on exit.

Example:
    forall( a(X), (write(X),write(' ')) )
writes 1 2 3 using the above clauses for a/1.


PUBLIC while( Cond+, Goal+ ):
'while' evaluates Cond, and if it succeeds, calls Goal. It repeats this
for as long as Cond continues to succeed. 'while' is different from
'forall' in that it evaluates Cond afresh on each cycle rather than
backtracking into it. If Goal fails, the action is undefined (a call to
'bug'). Not resatisfiable. All variables in Cond and Goal are unbound
on exit.

Example:
    while( a(X), (write(X),write(' ')) )
writes 1 indefinitely.


PUBLIC for( I-, Start+, End+, Step+, Goal+ ):
'for' calls Goal for values of I from Start to End, increasing by Step
each time, and then succeeds. If Goal fails, the action is undefined
(a call to 'bug'). Not resatisfiable. I, and all variables in Goal,
are unbound on exit.

If I > End on call, for succeeds and does nothing.

Example:
    for( I, 1, 20, 2, (write(I),write(' ')) )
writes
    1 3 5 7 9 11 13 15 17 19


PUBLIC for( I-, End+, Goal+ ):
Equivalent to for(I, 1, End, 1, Goal ).


PUBLIC for( N+, Goal+ ):
Calls Goal N times. Equivalent to for(_,N,Goal).


PUBLIC for_in_list( Elt-, List+, Goal+ ):
'for_in_list' calls Goal for Elt bound to each element of List, in
order, and then succeeds. If Goal fails, the action is undefined (a call
to 'bug'). Not resatisfiable. Elt, and all variables in Goal, are
unbound on exit.

Example:
    for_in_list( Elt, [a,b,c,d], (write(Elt),write(' ')) )
writes
    a b c d


PUBLIC for_reverse_in_list( Elt-, List+, Goal+ ):
As 'for_in_list', but the elements are visited in reverse order.
Example:
    for_reverse_in_list( Elt, [a,b,c,d], (write(Elt),write(' ')) )
writes
    d c b a


PUBLIC for_in_list( Elt-, List+, Goal+, SepGoal+ ):
This is like for_in_list/3. However, it also calls SepGoal _between_ each
pair of elements (i.e. at each "comma" in the list).

Example:
    for_in_list( Elt, [a,b,c,d], write(Elt), write(', ') )
writes
    a, b, c, d
*/


/*
IMPLEMENTATION
--------------

'once' and 'call_without_failure' are trivial. 'non_binding_call' uses
'not'. not(not(G)) must, to be logically correct, have the same
success/fail status as G, but it can't bind any variables - but see
below for a horrid bug in Poplog.


The looping predicates use (_->_;_) where necessary to cut out unwanted
alternatives. They all call 'bug' if their Goal fails. I've assumed goal
failure probably indicates an error - if the user really wants to pass a
goal that sometimes fails, she can make it always succeed by calling
call_without_failure.

There are several predicates - for, for_in_list, for_reverse_in_list,
while - that call Goal once and then call themselves recursively if they
need to call Goal again. For example:
    for( I, Start, End, Step, Goal ) :-
        Start =< End,
        !,
        non_binding_call(( I=Start,
                           (Goal->true;bug('for: goal failed',Goal)) )),
        NewStart is Start+Step,
        for( I, NewStart, End, Step, Goal ).
'for' calls Goal once with the index variable I bound to Start, and then
again with it bound to Start+Step. In doing this, we must beware of the
possibility that Goal may bind some variables in itself. If it does,
then we have to unbind them before the next call. We do this by using
'non_binding_call'. This also serves to unbind the index variable (I in
'for'; Elt in 'for_in_list').


Having said this, the implementation of 'while' is now more long-winded
than necessary. My original code was
    while( Cond, Goal ) :-
        non_binding_call(
                          (
                              Cond
                          ->
                              (Goal->true;bug('while:goal failed'))
                          ;
                              fail
                          )
                      ),
        while( Cond, Goal ).
    while( _, _ ).
which I prefer. But this malfunctions in a horrible way on Poplog
(versions 11 _and_ 13). The bug is most simply seen in the question
    ?- not( not( X=1 -> true ; true ) ).
which binds X to 1! 'not' should _never_ bind variables: something
pretty bad is going on here. Anyway, it's necessary to program around
it. Robert Duncan says this bug is fixed in Poplog V14.1.

I have had to fix some of the other predicates for the same reason.
They use 'assertion' instead of saying
    ( Goal -> true ; bug('while:goal failed') )
. This was something that could have done for 'while', but forgot about.
*/


:- needs assertion.


once(G) :- call(G), !.


call_without_failure( G ) :-
    ( call( G ) -> true ; true ).


non_binding_call( G ) :-
    not(not(G)).


forall( Cond, Goal ) :-
    Cond,
    assertion( Goal,
               'forall: goal failed',
               [Goal]
             ),
    fail.

forall( _, _ ).


while( Cond, Goal ) :-
    once((
            repeat,
            while_1( Cond ,Goal )
        )).


while_1( Cond, Goal ) :-
    Cond, !,
    assertion( Goal,
               'while: goal failed',
               [Goal]
             ),
    fail.

while_1( _, _ ).


for( I, Start, End, Step, Goal ) :-
    Start =< End,
    !,
    non_binding_call(( I=Start,
                       assertion( Goal,
                                  'for: goal failed',
                                  [Goal]
                                )
                    )),
    NewStart is Start+Step,
    for( I, NewStart, End, Step, Goal ).

for( _, _, _, _, _ ).


for( I, End, Goal ) :-
    for( I, 1, End, 1, Goal ).


for( N, Goal ) :-
    for( _, N, Goal ).


for_in_list( Elt, [Head|Tail], Goal ) :-
    !,
    non_binding_call(( Elt=Head,
                       assertion( Goal,
                                  'for_in_list: goal failed',
                                  [Goal]
                                )
                    )),
    for_in_list( Elt, Tail, Goal ).

for_in_list( Elt, [], _ ).


for_in_list( Elt, [Head], EltGoal, _ ) :-
    !,
    non_binding_call(( Elt=Head,
                       assertion( EltGoal,
                                  'for_in_list: goal failed',[EltGoal]
                                )
                    )).

for_in_list( Elt, [Head|Tail], EltGoal, SepGoal ) :-
    !,
    non_binding_call(( Elt=Head,
                       assertion( EltGoal,
                                  'for_in_list: goal failed',
                                  [EltGoal]
                                )
                    )),
    for_in_list_1( Elt, Tail, EltGoal, SepGoal ).

for_in_list( _, [], _, _ ).


for_in_list_1( Elt, [Head|Tail], EltGoal, SepGoal ) :-
    !,
    non_binding_call((
                       assertion( SepGoal,
                                  'for_in_list: sep goal failed',
                                  [SepGoal]
                                )
                    )),
    non_binding_call(( Elt=Head,
                       assertion( EltGoal,
                                  'for_in_list: goal failed',
                                  [EltGoal]
                                )
                    )),
    for_in_list_1( Elt, Tail, EltGoal, SepGoal ).

for_in_list_1( _, [], _, _ ).


for_reverse_in_list( Elt, [Head|Tail], Goal ) :-
    for_reverse_in_list( Elt, Tail, Goal ),
    non_binding_call(( Elt=Head,
                       assertion( Goal,
                                  'for_reverse_in_list: goal failed',
                                  [Goal]
                                )
                    )).

for_reverse_in_list( Elt, [], _ ).


/*
:- endmodule.
*/
