Predicate Variables Extension - Revision history

imported>Pascal: /* The category has been added */

2010-02-18T15:14:19Z

The category has been added

← Older revision		Revision as of 15:14, 18 February 2010
Line 40:		Line 40:

	This verification will be done as follows: Check each occurrence of the <tt>typeCheck()</tt>, <tt>isTypeChecked()</tt> or even <tt>isWellFormed()</tt> methods applied to an AST node. If this call occurs just after a <tt>parsePredicate()</tt> or <tt>parseExpression()</tt> call, then there is no risk of introducing a predicate meta-variable (as it would be ruled out by the parser). In all other cases (especially when receiving an AST object coming from an external reasoner), a check must be added to ensure that the AST tree that is type-checked is also free of predicate meta-variable.		This verification will be done as follows: Check each occurrence of the <tt>typeCheck()</tt>, <tt>isTypeChecked()</tt> or even <tt>isWellFormed()</tt> methods applied to an AST node. If this call occurs just after a <tt>parsePredicate()</tt> or <tt>parseExpression()</tt> call, then there is no risk of introducing a predicate meta-variable (as it would be ruled out by the parser). In all other cases (especially when receiving an AST object coming from an external reasoner), a check must be added to ensure that the AST tree that is type-checked is also free of predicate meta-variable.

			[[Category:Developer documentation]]

imported>Tommy: /* Further verifications to carry out */

2009-12-08T17:56:27Z

Further verifications to carry out

← Older revision		Revision as of 17:56, 8 December 2009
Line 39:		Line 39:
	The typical unwanted side-effet is that a predicate meta-variable creep into code that was not designed to cope with it.		The typical unwanted side-effet is that a predicate meta-variable creep into code that was not designed to cope with it.

	This verification will be done as follows: Check each occurrence of the <tt>typeCheck()</tt> ~~method~~ applied to an AST node. If this call occurs just after a <tt>parsePredicate()</tt> or <tt>parseExpression()</tt> call, then there is no risk of introducing a predicate meta-variable (as it would be ruled out by the parser). In all other cases (especially when receiving an AST object coming from an external reasoner), a check must be added to ensure that the AST tree that is type-checked is also free of predicate meta-variable.		This verification will be done as follows: Check each occurrence of the <tt>typeCheck()</tt>, <tt>isTypeChecked()</tt> or even <tt>isWellFormed()</tt> methods applied to an AST node. If this call occurs just after a <tt>parsePredicate()</tt> or <tt>parseExpression()</tt> call, then there is no risk of introducing a predicate meta-variable (as it would be ruled out by the parser). In all other cases (especially when receiving an AST object coming from an external reasoner), a check must be added to ensure that the AST tree that is type-checked is also free of predicate meta-variable.

imported>Laurent: /* Further verifications to carry out */ Refactored text

2009-12-03T10:27:27Z

Further verifications to carry out: Refactored text

← Older revision		Revision as of 10:27, 3 December 2009
Line 36:		Line 36:
	== Further verifications to carry out ==		== Further verifications to carry out ==

	A verification will follow implementation, in order to check that no side-~~effects were~~ introduced by this extension. ~~We will trace and verify~~ that ~~no external processing on predicates returns predicates containing~~ predicate ~~variables~~.		A verification will follow implementation, in order to check that no side-effect is introduced by this extension.
	~~For example, one must ensure that there isn't no call to~~ the "typeCheck()" method ~~in the platform's code that doesn't follow~~ a ~~call to~~ parsePredicate()~~. The aim~~ is ~~to verify that~~ no predicate ~~variables remain at~~ the ~~time of the "typeCheck~~()~~" call~~.		The typical unwanted side-effet is that a predicate meta-variable creep into code that was not designed to cope with it.

			This verification will be done as follows: Check each occurrence of the <tt>typeCheck()</tt> method applied to an AST node. If this call occurs just after a <tt>parsePredicate()</tt> or <tt>parseExpression()</tt> call, then there is no risk of introducing a predicate meta-variable (as it would be ruled out by the parser). In all other cases (especially when receiving an AST object coming from an external reasoner), a check must be added to ensure that the AST tree that is type-checked is also free of predicate meta-variable.

imported>Laurent: /* Plan to implement this extension in the API */

2009-12-03T10:21:58Z

Plan to implement this extension in the API

← Older revision		Revision as of 10:21, 3 December 2009
Line 15:		Line 15:
	*D. modify visitors, rewriters, filters, etc. according to this extension		*D. modify visitors, rewriters, filters, etc. according to this extension
	*E. implement new AST tests		*E. implement new AST tests
	*F. ensure that this extension has no side-effect on existing code

	== Implementation details ==		== Implementation details ==

imported>Laurent: /* Implementation details */

2009-12-03T10:21:28Z

Implementation details

← Older revision		Revision as of 10:21, 3 December 2009
Line 31:		Line 31:

	For C, the class 'PredicateVariable' will be added as a new predicate class.		For C, the class 'PredicateVariable' will be added as a new predicate class.
	In ~~the~~ Formula ~~class will be~~ added PredicateVariable[] getPredicateVariables() ~~and~~ boolean hasPredicateVariables() ~~methods.~~		In class Formula, two methods are added
			public PredicateVariable[] getPredicateVariables()
			public boolean hasPredicateVariables()

	== Further verifications to carry out ==		== Further verifications to carry out ==

imported>Laurent at 10:19, 3 December 2009

2009-12-03T10:19:54Z

← Older revision		Revision as of 10:19, 3 December 2009
Line 1:		Line 1:
	~~This~~ extension ~~will~~ allow ~~people to define~~ proof rules for the Rule Based Prover using meta-variables as predicate placeholders.		The aim of this extension is to allow defining proof rules for the Rule Based Prover using meta-variables as predicate placeholders.

	For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters.		For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters.

	~~The~~ meta-variables ~~will be identified with the~~ symbol '$'.		For technical reasons (predicates and expressions are distinct syntactic categories), predicate meta-variables are distinguished by a leading symbol '$'.
	For one given predicate, one wanting to refer to this predicate as P, will write in ~~his~~ proof rules~~, the~~ meta-variable '$P'.		For one given predicate, one wanting to refer to this predicate as P, will write in one's proof rules meta-variable '$P'.
	The symbol '?' could be originally chosen to define meta-variables but this revealed to be confusing due to the use of the symbol '?' in ~~the~~ CSP ~~language~~.		The symbol '?' could be originally chosen to define meta-variables but this revealed to be confusing due to the use of the symbol '?' in CSP.
	The choice of the symbol '$' seems to solve such ~~type~~ of issue.		The choice of the symbol '$' seems to solve such kind of issue.

	== Plan to implement this extension in the API ==		== Plan to implement this extension in the API ==
Line 13:		Line 13:
	*B. extend the parser		*B. extend the parser
	*C. extend the AST		*C. extend the AST
	*D. modify visitors, rewriters, filters, etc. ~~accorded~~ to this extension		*D. modify visitors, rewriters, filters, etc. according to this extension
	*E. implement new AST tests		*E. implement new AST tests
			*F. ensure that this extension has no side-effect on existing code

	== Implementation details ==		== Implementation details ==

imported>Tommy at 10:12, 3 December 2009

2009-12-03T10:12:34Z

← Older revision		Revision as of 10:12, 3 December 2009
Line 1:		Line 1:
	This extension will allow people to define proof rules for the Rule Based Prover using meta-variables as predicate placeholders.		This extension will allow people to define proof rules for the Rule Based Prover using meta-variables as predicate placeholders.

	For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters ~~to refer to an existing predicate declaration~~.		For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters.

	The meta-variables will be identified with the symbol '$'.		The meta-variables will be identified with the symbol '$'.

imported>Tommy: Predicate variables Extension moved to Predicate Variables Extension

2009-12-03T10:10:08Z

Predicate variables Extension moved to Predicate Variables Extension

← Older revision	Revision as of 10:10, 3 December 2009
(No difference)

imported>Tommy: Predicate variables moved to Predicate variables Extension

2009-12-03T10:08:45Z

Predicate variables moved to Predicate variables Extension

← Older revision	Revision as of 10:08, 3 December 2009
(No difference)

imported>Tommy: Explanations about the predicate variables extension.

2009-12-03T10:07:14Z

Explanations about the predicate variables extension.

New page

This extension will allow people to define proof rules for the Rule Based Prover using meta-variables as predicate placeholders.

For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters to refer to an existing predicate declaration.

The meta-variables will be identified with the symbol '$'.
For one given predicate, one wanting to refer to this predicate as P, will write in his proof rules, the meta-variable '$P'.
The symbol '?' could be originally chosen to define meta-variables but this revealed to be confusing due to the use of the symbol '?' in the CSP language.
The choice of the symbol '$' seems to solve such type of issue.

== Plan to implement this extension in the API ==

*A. extend the lexer
*B. extend the parser
*C. extend the AST
*D. modify visitors, rewriters, filters, etc. accorded to this extension
*E. implement new AST tests

== Implementation details ==

For B, clients (plug-in contributers) will be allowed to select the mode they want to work with.
Thus, will coexist 2 parsing modes one taking into account predicate variables and the other, the current one, which parses predicates or expressions without predicate variables.

- the current one available in the current API (FormulaFactory),
public IParseResult parsePredicate(String formula, LanguageVersion version,Object origin)
public IParseResult parseExpression(String formula, LanguageVersion version,Object origin)

- a specific one providing the support for predicate variables.
public IParseResult parsePredicatePattern(String formula, LanguageVersion version,Object origin)
public IParseResult parseExpressionPattern(String formula, LanguageVersion version,Object origin)

For C, the class 'PredicateVariable' will be added as a new predicate class.
In the Formula class will be added PredicateVariable[] getPredicateVariables() and boolean hasPredicateVariables() methods.

== Further verifications to carry out ==

A verification will follow implementation, in order to check that no side-effects were introduced by this extension. We will trace and verify that no external processing on predicates returns predicates containing predicate variables.
For example, one must ensure that there isn't no call to the "typeCheck()" method in the platform's code that doesn't follow a call to parsePredicate(). The aim is to verify that no predicate variables remain at the time of the "typeCheck()" call.