// $Id: Filter.java,v 1.2 1999/11/05 19:23:16 leavens Exp $

package lib;

public class Filter implements Iterator {

    protected Predicate saved_pred;
    protected Iterator saved_seq;

    /*@ public invariant: saved_pred != null && saved_seq != null
                       && (!saved_seq.hasMore()
                           || saved_pred.value(saved_seq.getElement()));
      @*/

    public Filter(Predicate pred, Iterator seq)
    //@ requires: pred != null && seq != null;
    {
        saved_pred = pred;
        saved_seq = seq;
        toNextSat();
    }

    protected void toNextSat()
    //@ requires: saved_pred != null && saved_seq != null;
    {
        while (saved_seq.hasMore()
               && !saved_pred.value(saved_seq.getElement())) {
            saved_seq.advance();
        }
        /*@ assert: !saved_seq.hasMore()
                   || saved_pred.value(saved_seq.getElement());
          @*/
    }

    public boolean hasMore() {
        return saved_seq.hasMore();
    }

    public void advance() {
        saved_seq.advance();
        // re-establish the invariant
        toNextSat();
    }

    public Object getElement() {
        return saved_seq.getElement();
    }
}