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