New Tactic Providers

The purpose is to give more flexibility to tactic providers by allowing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position.

A new API

The new API consists in the following published interfaces:

public interface ITacticProvider2 {
   List<ITacticApplication> getPossibleApplications(IProofTreeNode node,
                                                    Predicate hyp,
                                                    String globalInput);
}

public interface ITacticApplication {
   ITactic getTactic(String[] inputs,
              String globalInput);
   String getTacticID();
}

public interface IPositionApplication  extends ITacticApplication {
   Point getHyperlinkBounds(String parsedString, Predicate parsedPredicate);
   String getHyperlinkLabel();
}

public interface IPredicateApplication extends ITacticApplication {
   Image getIcon();
   String getTooltip();
}

The existing extension point "proofTactics" is added an optional attribute to allow skipping post tactic application (default is false).

All those interfaces are intended to be implemented by clients.

Explanations

The idea is to encapsulate in ITacticApplication all data needed by the UI to display and apply tactics. Thus, an ITacticProvider2, instead of returning just one fixed tactic to apply, can return several possible 'autonomous' tactic applications.

Interfaces IPositionApplication and IPredicateApplication are particular application types:

• IPositionApplication is for tactics applied at a given position in a formula (red hyperlinks in interactive prover UI). The getHyperlinkLabel() method allows to override extension point behaviour (using the fixed 'tooltip' attribute), in order to have a different text for each application in the hyperlink list. If null is returned, then default 'tooltip' from extension point is taken.

• IPredicateApplication is for tactics applied to a whole predicate, like 'Contradict Goal' or 'Contradict Hyp' (icons on the left of a predicate in interactive prover UI). The methods allow to override extension point behaviour (using the 'icon' and 'tooltip' attributes), in order to have a different icon and tooltip for each application in the left icon list. If null is returned, then default data from extension point is taken.

A different Protocol

The current protocol concerning the return value of tactic providers is the following:

• null if not applicable
• empty list of positions if applicable to predicate
• non empty list of positions if applicable to a position in predicate

The new protocol using ITacticApplication is the following:

• an empty list of applications if not applicable
• a non empty list of applications if applicable and, for each application:
  • an instanceof IPredicateApplication if applicable to predicate, even if default icon and tooltip from extension point should be used (methods returning null)
  • an instanceof IPositionApplication if applicable to a position in predicate

Thus, the distinction between application to predicate or position is based on objects's actual type. Hence, one of IPredicateApplication or IPositionApplication interface should be implemented. Only implementing ITacticApplication would make the UI ignore the extension.

Example

The following example demonstrates (part of) the implementation of a tactic using the new API. For simplicity, a simple ITacticApplication is used, but a IPositionApplication should be used instead. The underlying IReasoner (ExampleReasoner) is not shown here, as it is not impacted by the new API.

//rewrites occurrences of literal 4 into either 2+2 or 2*2 
public class ExampleTacticProvider2 implements ITacticProvider2 {

    // our own implementation of a tactic application
    private static class ExampleApplication implements ITacticApplication {

        private static final String TACTIC_ID = "fr.systerel.example";
    	
        private final Predicate hyp;
        private final IPosition position;
        // 2 Kinds: PLUS (2+2) and MULT (2*2)
        private final ExampleReasoner.Kind kind;

        public ExampleApplication(Predicate hyp, IPosition position, Kind kind) {
            this.hyp = hyp;
            this.position = position;
            this.kind = kind;
        }

        public ITactic getTactic(String[] inputs, String globalInput) {
            // ExampleReasoner implements IReasoner and rewrites literal 4
            // at given position into:
            // . 2+2 if input.kind is PLUS
            // . 2*2 if input.kind is MULT
            return BasicTactics.reasonerTac(
                    new ExampleReasoner(),
                    new ExampleReasoner.Input(hyp, position, kind));
        }

        public String getTacticID() {
            return TACTIC_ID;
        }
    }

    // visits a formula and adds applications on occurrences of literal 4
    private static class ExampleApplicationVisitor extends DefaultVisitor {

        private final Predicate hyp;
        private final Predicate predicate;
        // a list to put applications into
        private final List<ITacticApplication> applications =
                new ArrayList<ITacticApplication>();

        public ExampleApplicationVisitor(Predicate predicate, Predicate hyp) {
            this.predicate = predicate;
            this.hyp = hyp;
        }

        public List<ITacticApplication> getApplications() {
            return applications;
        }

        @Override
        public boolean visitINTLIT(IntegerLiteral lit) {
            if (lit.getValue().intValue() == 4) {
                final IPosition position = predicate.getPosition(lit.getSourceLocation());
                applications.add(new ExampleApplication(hyp, position, Kind.MULT));
                applications.add(new ExampleApplication(hyp, position, Kind.PLUS));
            }
            return true;
        }
    }

    // the ITacticProvider2 interface method: calls the visitor on the predicate
    public List<ITacticApplication> getPossibleApplications(IProofTreeNode node,
                                                            Predicate hyp,
                                                            String globalInput) {

        final Predicate pred = (hyp == null) ? node.getSequent().goal() : hyp;

        ExampleApplicationVisitor visitor =
                new ExampleApplicationVisitor(pred, hyp); 
        pred.accept(visitor);
        return visitor.getApplications();
    }
}