Modularisation Plug-in

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.

API Proposal

The current proposal 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);
}

public interface IPositionApplication  extends ITacticApplication {
   Point getHyperlinkBounds();
   String getHyperlinkLabel();
}

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

The current extension point "proofTactics" remains unchanged.

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 proposed protocol using ITacticApplication is the following:

• an empty list of applications if not applicable
• a non empty list of applications 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 (or shall we assume IPredicateApplication with default values ?).

Example

The following example demonstrates (part of) the implementation of a tactic using the proposed API. For simplicity, a simple ITacticApplication is used, but a IPositionApplication could (should) be used instead. The underlying IReasoner (ExampleReasoner) is not shown here, as it is not impacted by the proposed 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 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));
        }
    }

    // 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, applications); 
        pred.accept(visitor);
        return visitor.getApplications();
    }
}