New Tactic Providers - Revision history

imported>Nicolas: /* Example */ Added category Developer documentation

2009-10-12T13:00:12Z

Example: Added category Developer documentation

← Older revision		Revision as of 13:00, 12 October 2009
Line 144:		Line 144:
	}		}
	}</pre>		}</pre>


			[[Category:Developer documentation]]

imported>Nicolas: /* Explanations */

2009-10-07T07:55:52Z

Explanations

← Older revision		Revision as of 07:55, 7 October 2009
Line 31:		Line 31:
	All those interfaces are intended to be implemented by clients.		All those interfaces are intended to be implemented by clients.

	== Explanations ==		=== Explanations ===

	The idea is to encapsulate in {{class\|ITacticApplication}} all data needed by the UI to display and apply tactics.		The idea is to encapsulate in {{class\|ITacticApplication}} all data needed by the UI to display and apply tactics.
Line 44:		Line 44:


	=== A different Protocol ===		== A different Protocol ==

	The current protocol concerning the return value of tactic providers is the following:		The current protocol concerning the return value of tactic providers is the following:

imported>Nicolas: /* Example */

2009-10-06T16:44:26Z

Example

← Older revision		Revision as of 16:44, 6 October 2009
Line 63:		Line 63:
	== Example ==		== Example ==

	The following example demonstrates (part of) the implementation of a tactic using the ~~proposed~~ API.		The following example demonstrates (part of) the implementation of a tactic using the new API.
	For simplicity, a simple {{class\|ITacticApplication}} is used, but a {{class\|IPositionApplication}} should be used instead.		For simplicity, a simple {{class\|ITacticApplication}} is used, but a {{class\|IPositionApplication}} should be used instead.
	The underlying {{class\|IReasoner}} ({{class\|ExampleReasoner}}) is not shown here, as it is not impacted by the ~~proposed~~ API.		The underlying {{class\|IReasoner}} ({{class\|ExampleReasoner}}) is not shown here, as it is not impacted by the new API.

	<pre>		<pre>

imported>Nicolas: /* A different Protocol */

2009-10-06T16:43:14Z

A different Protocol

← Older revision		Revision as of 16:43, 6 October 2009
Line 52:		Line 52:


	The ~~proposed~~ protocol using {{class\|ITacticApplication}} is the following:		The new protocol using {{class\|ITacticApplication}} is the following:
	* an empty list of applications if not applicable		* an empty list of applications if not applicable
	* a non empty list of applications if applicable and, for each application:		* a non empty list of applications if applicable and, for each application:

imported>Nicolas: /* API Proposal */

2009-10-06T16:42:07Z

API Proposal

← Older revision		Revision as of 16:42, 6 October 2009
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.

	== API ~~Proposal~~ ==		== A new API ==

	The ~~current proposal~~ consists in the following published interfaces:		The new API consists in the following published interfaces:

	public interface ITacticProvider2 {		public interface ITacticProvider2 {
Line 27:		Line 27:
	}		}

	The ~~current~~ extension point "proofTactics" is added an optional attribute to allow skipping post tactic application (default is false).		The existing extension point "proofTactics" is added an optional attribute to allow skipping post tactic application (default is false).

	All those interfaces are intended to be implemented by clients.		All those interfaces are intended to be implemented by clients.

imported>Nicolas: /* Example */

2009-09-18T16:40:26Z

Example

← Older revision		Revision as of 16:40, 18 September 2009
Line 64:		Line 64:

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

Line 74:		Line 74:
	private static class ExampleApplication implements ITacticApplication {		private static class ExampleApplication implements ITacticApplication {

			private static final String TACTIC_ID = "fr.systerel.example";

	private final Predicate hyp;		private final Predicate hyp;
	private final IPosition position;		private final IPosition position;
Line 93:		Line 95:
	new ExampleReasoner(),		new ExampleReasoner(),
	new ExampleReasoner.Input(hyp, position, kind));		new ExampleReasoner.Input(hyp, position, kind));
			}

			public String getTacticID() {
			return TACTIC_ID;
	}		}
	}		}

imported>Nicolas: /* A different Protocol */

2009-09-18T16:29:13Z

A different Protocol

← Older revision		Revision as of 16:29, 18 September 2009
Line 54:		Line 54:
	The proposed protocol using {{class\|ITacticApplication}} is the following:		The proposed protocol using {{class\|ITacticApplication}} is the following:
	* an empty list of applications if not applicable		* an empty list of applications if not applicable
	* a non empty list of applications and, for each application:		* a non empty list of applications if applicable 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\|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		** 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 ?)~~.		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.

	== Example ==		== Example ==

imported>Nicolas: /* API Proposal */

2009-09-18T16:25:48Z

API Proposal

← Older revision		Revision as of 16:25, 18 September 2009
Line 14:		Line 14:
	ITactic getTactic(String[] inputs,		ITactic getTactic(String[] inputs,
	String globalInput);		String globalInput);
			String getTacticID();
	}		}

	public interface IPositionApplication extends ITacticApplication {		public interface IPositionApplication extends ITacticApplication {
	Point getHyperlinkBounds();		Point getHyperlinkBounds(String parsedString, Predicate parsedPredicate);
	String getHyperlinkLabel();		String getHyperlinkLabel();
	}		}
Line 26:		Line 27:
	}		}

	The current extension point "proofTactics" ~~remains unchanged~~.		The current extension point "proofTactics" is added an optional attribute to allow skipping post tactic application (default is false).

	All those interfaces are intended to be implemented by clients.		All those interfaces are intended to be implemented by clients.

imported>Nicolas: /* Example */ Corrected code to make it compile

2009-09-11T09:54:37Z

Example: Corrected code to make it compile

← Older revision		Revision as of 09:54, 11 September 2009
Line 67:		Line 67:

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

Line 132:		Line 132:

	ExampleApplicationVisitor visitor =		ExampleApplicationVisitor visitor =
	new ExampleApplicationVisitor(pred, hyp~~, applications~~);		new ExampleApplicationVisitor(pred, hyp);
	pred.accept(visitor);		pred.accept(visitor);
	return visitor.getApplications();		return visitor.getApplications();
	}		}
	}		}</pre>
	</pre>

imported>Nicolas: /* Explanations */

2009-09-11T09:47:17Z

Explanations

@@ Line 38: / Line 38: @@
 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 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.
+* {{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 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.
+* {{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.
 == Example ==