Difference between revisions of "Predicate Variables Extension"
imported>Tommy m |
imported>Laurent m |
||
| Line 1: | Line 1: | ||
| − | + | 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. | ||
| − | + | 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 | + | 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 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 | + | 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. | + | *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 == | ||
Revision as of 10:19, 3 December 2009
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 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 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 CSP. The choice of the symbol '$' seems to solve such kind 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. according to this extension
- E. implement new AST tests
- F. ensure that this extension has no side-effect on existing code
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.
