imported>Nicolas |
|
Line 1: |
Line 1: |
− | 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 {{class|ITacticApplication}} all data needed by the UI to display and apply tactics.
| |
− | Thus, an {{class|ITacticProvider2}}, instead of returning just one fixed tactic to apply, can return several possible 'autonomous' tactic applications.
| |
− |
| |
− |
| |
− | Interfaces {{class|IPositionApplication}} and {{class|IPredicateApplication}} are particular application types:
| |
− |
| |
− | * {{class|IPositionApplication}} is for tactics applied at a given position in a formula (red hyperlinks in interactive prover UI). The {{method|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.
| |
− |
| |
− | * {{class|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 {{class|ITacticApplication}} is the following:
| |
− | * an empty list of applications if not applicable
| |
− | * a non empty list of applications and, for each application:
| |
− | ** an instanceof {{class|IPredicateApplication}} if applicable to predicate, even if default icon and tooltip from extension point should be used (methods returning '''null''')
| |
− | ** an instanceof {{class|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 {{class|IPredicateApplication}} or {{class|IPositionApplication}} interface should be implemented. Only implementing {{class|ITacticApplication}} would make the UI ignore the extension (or shall we assume {{class|IPredicateApplication}} with default values ?).
| |
− |
| |
− | == Example ==
| |
− |
| |
− | The following example demonstrates (part of) the implementation of a tactic using the proposed API.
| |
− | For simplicity, a simple {{class|ITacticApplication}} is used, but a {{class|IPositionApplication}} could (should) be used instead.
| |
− | The underlying {{class|IReasoner}} ({{class|ExampleReasoner}}) is not shown here, as it is not impacted by the proposed API.
| |
− |
| |
− | <pre>
| |
− | // 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();
| |
− | }
| |
− | }
| |
− | </pre>
| |