Adding Manual Inference Reasoners - Revision history

imported>Nicolas at 17:31, 24 November 2010

2010-11-24T17:31:57Z

← Older revision		Revision as of 17:31, 24 November 2010
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
			''Please also have a look at'' [[How_To_Evolve_Reasoners\| How To Evolve Reasoners]].


	Beside the input sequent, reasoners of this type have two extra inputs specify the hypothesis or the goal and the position inside the predicate when apply an inference rule to the input sequent. As an example, consider the following inference rule (called IMP_R).		Beside the input sequent, reasoners of this type have two extra inputs specify the hypothesis or the goal and the position inside the predicate when apply an inference rule to the input sequent. As an example, consider the following inference rule (called IMP_R).
	{{InfRule \| IMP_R \| <math>\frac{H, P \vdash Q}{H \vdash P \limp Q}</math>}}		{{InfRule \| IMP_R \| <math>\frac{H, P \vdash Q}{H \vdash P \limp Q}</math>}}

imported>Nicolas: /* Implement the Reasoner */ Added link to Versioned Reasoners

2009-10-06T18:02:52Z

Implement the Reasoner: Added link to Versioned Reasoners

← Older revision		Revision as of 18:02, 6 October 2009
Line 151:		Line 151:
	** Tom is used here to do pattern matching. In our case, match the goal with <math>P \limp Q</math>.		** Tom is used here to do pattern matching. In our case, match the goal with <math>P \limp Q</math>.
	** Methods for construct hypothesis actions, antecedent, etc. can be found in class ''org.eventb.core.seqprover.ProverFactory''.		** Methods for construct hypothesis actions, antecedent, etc. can be found in class ''org.eventb.core.seqprover.ProverFactory''.

			Note: in order to avoid problems with subsequent reasoner implementation evolutions, it would be wise to implement a [[Versioned Reasoners\|versioned reasoner]] (one more simple method).

	== Setting up Tom ==		== Setting up Tom ==

imported>Mathieu: cat + tocright

2008-09-17T16:55:24Z

cat + tocright

← Older revision		Revision as of 16:55, 17 September 2008
Line 1:		Line 1:
			{{TOCright}}
	Beside the input sequent, reasoners of this type have two extra inputs specify the hypothesis or the goal and the position inside the predicate when apply an inference rule to the input sequent. As an example, consider the following inference rule (called IMP_R).		Beside the input sequent, reasoners of this type have two extra inputs specify the hypothesis or the goal and the position inside the predicate when apply an inference rule to the input sequent. As an example, consider the following inference rule (called IMP_R).
	{{InfRule \| IMP_R \| <math>\frac{H, P \vdash Q}{H \vdash P \limp Q}</math>}}		{{InfRule \| IMP_R \| <math>\frac{H, P \vdash Q}{H \vdash P \limp Q}</math>}}
Line 222:		Line 223:

	* The content of the test class is as follows		* The content of the test class is as follows


			[[Category:Developer documentation]]
			[[Category:Rodin Platform]]

imported>Son at 15:06, 16 September 2008

2008-09-16T15:06:15Z

← Older revision		Revision as of 15:06, 16 September 2008
Line 100:		Line 100:
	if (pred != null)		if (pred != null)
	return null; // This must be applied to goal		return null; // This must be applied to goal
	if (position != IPosition.ROOT)		if (!position.equals(IPosition.ROOT))
	return null; // The applicable position must be ROOT (the implication).		return null; // The applicable position must be ROOT (the implication).

imported>Son: /* Test the Reasoner */

2008-09-16T15:05:48Z

Test the Reasoner

← Older revision		Revision as of 15:05, 16 September 2008
Line 211:		Line 211:

	== Test the Reasoner ==		== Test the Reasoner ==
			Follow the steps below to create a test for declaration of the newly created reasoner.

			* Create a test plug-in project, e.g. ''org.eventb.contributors.seqprover.implinference.tests''

			* Create dependencies on ''org.eventb.core.seqprover.tests'' and the project under test (in our example, it is ''org.eventb.contributors.seqprover.implinference''.

			* Create a package for the tests, e.g. ''org.eventb.internal.contributors.seqprover.implinference.tests''

			* Create a new class within the newly created package. This class will extend this abstract test class ''org.eventb.core.seqprover.eventbExtentionTests.AbstractManualInferenceTests''.

			* The content of the test class is as follows

imported>Son: /* Implement the Reasoner */

2008-09-16T13:21:23Z

Implement the Reasoner

← Older revision		Revision as of 13:21, 16 September 2008
Line 150:		Line 150:
	** Tom is used here to do pattern matching. In our case, match the goal with <math>P \limp Q</math>.		** Tom is used here to do pattern matching. In our case, match the goal with <math>P \limp Q</math>.
	** Methods for construct hypothesis actions, antecedent, etc. can be found in class ''org.eventb.core.seqprover.ProverFactory''.		** Methods for construct hypothesis actions, antecedent, etc. can be found in class ''org.eventb.core.seqprover.ProverFactory''.

			== Setting up Tom ==
			* Create a file named build-tom.xml within your project. The content of the file looks like this.

			<project name="org.eventb.contributors.seqprover.implrewrites" default="tom" basedir=".">
			<description>
			Generates derived files in the Sequent Prover.
			</description>

			<!-- set global properties for this build -->
			<property name="src" location="src" />

			<property name="org.eventb.core.ast.home" location="../org.eventb.core.ast" />
			<import file="${org.eventb.core.ast.home}/tom/tom-task.xml"/>

			<property name="inference.src"
			location="${src}/org/eventb/internal/contributors/seqprover/implinference" />

			<target name="init" description="Create the initial time stamp">
			<tstamp />
			</target>

			<target name="tom" depends="init"
			description="Launch tom for all files">
			<tom config="${tom.home}/Tom.xml"
			srcdir="${src}"
			destdir="${src}"
			options="-I ${org.eventb.core.ast.home}/tom --static"
			pretty="true"
			optimize="true">
			<include name="*/.t" />
			</tom>
			</target>

			<target name="clean" description="clean up">
			<delete file="${inference.src}/ManualInference.java" />
			</target>

			</project>

			The best way to create this file is to copy from org.eventb.core.seqprover project, and modify this accordingly.

			* Right click on the name of your project and choose Properties.
			* Choose "Builders", then click on "New" and choose "Ant Build" and click OK. A dialog will open for new builder wizard.
			* At the ''Main'' tab:
			** Enter the name of the builder, e.g. ''Tom Builder''.
			** Buildfile: ''Browse Workspace'' to your ''build-tom.xml''.
			** Base Directory: ''Variables'' and choose ''build_project''.
			* At the ''Targets'' tab:
			** Auto Build: Click ''Set Targets'' and choose "tom" from the list.
			** During a "clean": Click "Set Targets" and choose ''clean'' (unchecked ''tom'').

			* At the ''Refresh'' tab: Choose "Refresh resource upon completion", and "Specific resources". Click "Specify Resources" and browse to the location of the folder contains the Tom file. In our example, it will be ''src/org/eventb/internal/contributors/seqprover/implinference''

			* At the ''Build Options'' tab: Click "Specify working set of relevant resources". Click "Specify Resources" and browse to the Tom file, i.e. "ManualInference.t".

			* Click Apply and OK to close the dialog.

			* The Tom Builder should run and generate the Java implementation for ManualInference.java in the specified folder.

			== Test the Reasoner ==

imported>Son at 13:19, 16 September 2008

2008-09-16T13:19:01Z

← Older revision		Revision as of 13:19, 16 September 2008
Line 144:		Line 144:
	* Clients need to implement first the two methods to return the reasoner id, ''getReasonerID()'', and return the display name, ''getDisplayName()''.		* Clients need to implement first the two methods to return the reasoner id, ''getReasonerID()'', and return the display name, ''getDisplayName()''.

	* Moreover, clients need to implement the method for getting the actual antecedents ''getAntecedents(IProverSequent seq)''		* Moreover, clients need to implement the method for getting the actual antecedents ''getAntecedents(IProverSequent seq, Predicate pred, IPosition position)''
	** The input of the method is the sequent, a hypothesis predicate (''null'' if the apply to goal), and a position within the predicate		** The input of the method is the sequent, a hypothesis predicate (''null'' if the apply to goal), and a position within the predicate
	** The method return the list of antecedents to implement the inference rule.		** The method return the list of antecedents to implement the inference rule.

imported>Son: /* Implement the Reasoner */

2008-09-16T13:18:21Z

Implement the Reasoner

← Older revision		Revision as of 13:18, 16 September 2008
Line 139:		Line 139:

	}		}

			* The implementation is based on ''org.eventb.internal.core.seqprover.eventbExtensions.AbstractManualInference''. (For the moment, the class is internal within the project and subjected to be changed. Clients can make a copy of this class to develop their own implementation).

			* Clients need to implement first the two methods to return the reasoner id, ''getReasonerID()'', and return the display name, ''getDisplayName()''.

			* Moreover, clients need to implement the method for getting the actual antecedents ''getAntecedents(IProverSequent seq)''
			** The input of the method is the sequent, a hypothesis predicate (''null'' if the apply to goal), and a position within the predicate
			** The method return the list of antecedents to implement the inference rule.
			** Here the extra input, i.e. hypothesis predicate and position is used to check the applicability of the reasoner. In more complicated reasoners, these input can also influence the outcome of the reasoner.
			** Tom is used here to do pattern matching. In our case, match the goal with <math>P \limp Q</math>.
			** Methods for construct hypothesis actions, antecedent, etc. can be found in class ''org.eventb.core.seqprover.ProverFactory''.

imported>Son: /* Declare the Reasoner */

2008-09-16T13:00:14Z

Declare the Reasoner

← Older revision		Revision as of 13:00, 16 September 2008
Line 21:		Line 21:

	* We will use Tom to implement the reasoner class itself.		* We will use Tom to implement the reasoner class itself.

			== Implement the Reasoner ==
			The following steps is for implementing the reasoner using Tom.

			* Create a package within the ''src'' folder of the project with the name ''org.eventb.internal.contributors.seqprover.implinference''.

			* Create a Tom file within the newly created package with the name ''AutoInference.t''.

			* The content of the Tom file looks like this.

			package org.eventb.internal.contributors.seqprover.implinference;

			import java.math.BigInteger;
			import java.util.ArrayList;
			import java.util.Collection;
			import java.util.List;
			import java.util.Set;
			import java.util.HashSet;

			import org.eventb.core.ast.AssociativeExpression;
			import org.eventb.core.ast.AssociativePredicate;
			import org.eventb.core.ast.AtomicExpression;
			import org.eventb.core.ast.BinaryExpression;
			import org.eventb.core.ast.BinaryPredicate;
			import org.eventb.core.ast.BoolExpression;
			import org.eventb.core.ast.BoundIdentDecl;
			import org.eventb.core.ast.BoundIdentifier;
			import org.eventb.core.ast.DefaultFilter;
			import org.eventb.core.ast.Expression;
			import org.eventb.core.ast.Formula;
			import org.eventb.core.ast.FormulaFactory;
			import org.eventb.core.ast.FreeIdentifier;
			import org.eventb.core.ast.Identifier;
			import org.eventb.core.ast.IntegerLiteral;
			import org.eventb.core.ast.IPosition;
			import org.eventb.core.ast.LiteralPredicate;
			import org.eventb.core.ast.PowerSetType;
			import org.eventb.core.ast.Predicate;
			import org.eventb.core.ast.ProductType;
			import org.eventb.core.ast.QuantifiedExpression;
			import org.eventb.core.ast.QuantifiedPredicate;
			import org.eventb.core.ast.RelationalPredicate;
			import org.eventb.core.ast.SetExtension;
			import org.eventb.core.ast.SimplePredicate;
			import org.eventb.core.ast.Type;
			import org.eventb.core.ast.UnaryExpression;
			import org.eventb.core.ast.UnaryPredicate;
			import org.eventb.core.seqprover.eventbExtensions.Tactics;
			import org.eventb.core.seqprover.IProverSequent;
			import org.eventb.core.seqprover.IHypAction;
			import org.eventb.core.seqprover.ProverFactory;
			import org.eventb.core.seqprover.SequentProver;
			import org.eventb.core.seqprover.IProofRule.IAntecedent;
			import org.eventb.core.seqprover.eventbExtensions.Lib;
			import org.eventb.core.seqprover.eventbExtensions.Tactics;
			import org.eventb.internal.core.seqprover.eventbExtensions.AbstractManualInference;

			/**
			* Basic implementation for "manual implication inference"
			*/
			@SuppressWarnings("unused")
			public class ManualInference extends AbstractManualInference {

			%include {Formula.tom}

			public String getReasonerID() {
			return "org.eventb.contributors.seqprover.implinference.manualInference";
			}

			@Override
			protected String getDisplayName() {
			return "Manual deduction";
			}

			@Override
			protected IAntecedent[] getAntecedents(IProverSequent seq, Predicate pred,
			IPosition position) {
			if (pred != null)
			return null; // This must be applied to goal
			if (position != IPosition.ROOT)
			return null; // The applicable position must be ROOT (the implication).

			Predicate goal = seq.goal();

			Predicate P = null;
			Predicate Q = null;
			%match (Predicate goal) {

			/**
			* Deduction:
			* H, P \|- Q
			* -----------
			* H \|- P => Q
			*/
			Limp(PP, QQ) -> {
			P = `PP;
			Q = `QQ;
			}

			}

			if (P == null)
			return null;

			// There will be 1 antecidents
			IAntecedent[] antecidents = new IAntecedent[1];

			// Added hypothesis P
			Set<Predicate> addedHyps = new HashSet<Predicate>(1);
			addedHyps.add(P);
			// Select the new hypothesis P
			IHypAction hypAction = ProverFactory.makeSelectHypAction(addedHyps);
			antecidents[0] = ProverFactory.makeAntecedent(Q, addedHyps, hypAction);

			return antecidents;
			}

			}

imported>Son: New page: Beside the input sequent, reasoners of this type have two extra inputs specify the hypothesis or the goal and the position inside the predicate when apply an inference rule to the input s...

2008-09-16T12:46:09Z

New page: Beside the input sequent, reasoners of this type have two extra inputs specify the hypothesis or the goal and the position inside the predicate when apply an inference rule to the input s...

New page

Beside the input sequent, reasoners of this type have two extra inputs specify the hypothesis or the goal and the position inside the predicate when apply an inference rule to the input sequent. As an example, consider the following inference rule (called IMP_R).
{{InfRule | IMP_R | <math>\frac{H, P \vdash Q}{H \vdash P \limp Q}</math>}}

In this simple case the location is the location of the implication symbol in the goal.

== Declare the Reasoner ==
* Create a new plug-in project, e.g. ''org.eventb.contributors.seqprover.implinference''. Deselect the plug-in options for "Generating an activator" and "Contribution to the UI".

* Add dependency on the project ''org.eventb.core.seqprover''

* Add an extension for ''org.eventb.core.seqprover.reasoners'' for our implication rewrite reasoner, e.g.

<extension point="org.eventb.core.seqprover.reasoners">
<reasoner
class="org.eventb.internal.contributors.seqprover.implinference.ManualInference"
id="manualInference"
name="%manualInferenceName"/>
</extension>

(add the key manualInferenceName to the plugin.properties accordingly).

* We will use Tom to implement the reasoner class itself.