Mathematical Extensions

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,
              IProgressMonitor monitor);
}

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 methods allow to override extension point data, in order to have a different text for each application in the hyperlink list. If null is returned, then default data from extension point is taken.

• IPredicateApplication is for tactics applied at 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 data, 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.

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 IUserSupport userSupport;
        private final Predicate hyp;
        private final IPosition position;
        // 2 Kinds: PLUS (2+2) and MULT (2*2)
        private final ExampleReasoner.Kind kind;

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

        public void apply(String[] inputs, String globalInput, IProgressMonitor monitor) {
            try {
                // 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
                userSupport.applyTactic(BasicTactics.reasonerTac(
                        new ExampleReasoner(),
                        new ExampleReasoner.Input(hyp, position, kind)),
                        true, monitor);
            } catch (RodinDBException e) {
                // log the problem
            }
        }
    }

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

        private final IUserSupport userSupport;
        private final Predicate hyp;
        private final Predicate predicate;
        // a list to put applications into
        private final List<ITacticApplication> applications;

        public ExampleApplicationVisitor(IUserSupport userSupport,
                Predicate predicate, Predicate hyp,
                List<ITacticApplication> applications) {
            this.userSupport = userSupport;
            this.predicate = predicate;
            this.hyp = hyp;
            this.applications = applications;
        }

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

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

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

        final List<ITacticApplication> applications = new ArrayList<ITacticApplication>();
        
        pred.accept(new ExampleApplicationVisitor(userSupport, pred, hyp, applications));
        
        return applications;
    }
}