New Tactic Providers: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Nicolas
m Page bootstrap
 
imported>Nicolas
m Added explanations and example
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.  
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.  


=== Proposed Framework ===
== Proposed Framework ==
 
The current proposal consists in the following published interfaces:


  public interface ITacticProvider2 {
  public interface ITacticProvider2 {
Line 9: Line 11:
                                                     String globalInput);
                                                     String globalInput);
  }
  }


  public interface ITacticApplication {
  public interface ITacticApplication {
     void apply(String[] inputs, String globalInput, IProgressMonitor monitor);
     void apply(String[] inputs,
              String globalInput,
              IProgressMonitor monitor);
  }
  }


  public interface IPositionApplication  extends ITacticApplication {
  public interface IPositionApplication  extends ITacticApplication {
Line 23: Line 25:
  public interface IPredicateApplication extends ITacticApplication {
  public interface IPredicateApplication extends ITacticApplication {
     Image getIcon();
     Image getIcon();
     String getTip();
     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, tactic providers, instead of returning just one fixed tactic to apply, can return several possible 'autonomous' applications.
== Example ==
<pre>
// rewrites occurrences of literal 4 into either 2+2 or 2*2
public class ExampleTacticProvider2 implements ITacticProvider2 {
    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
            }
        }
    }
    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
    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;
    }
}
</pre>

Revision as of 16:09, 10 September 2009

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.

Proposed Framework

The current proposal consists in the following published interfaces:

public interface ITacticProvider2 {
   List<ITacticApplication> getPossibleApplications(IUserSupport userSupport,
                                                    IProofTreeNode node,
                                                    Predicate hyp,
                                                    String globalInput);
}
public interface ITacticApplication {
   void apply(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, tactic providers, instead of returning just one fixed tactic to apply, can return several possible 'autonomous' applications.

Example

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

    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
            }
        }
    }

    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
    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;
    }
}