Rules: Allow type annotations in higher-order patterns

[francoisthire]

To make Dedukti compliant with the standard.

[GuillaumeGen]

What is the semantic of adding a type annotation in a pattern? If I understand the code, what you are suggesting is that the type annotation must be always valid. So annotation are used at type-checking of the rule phase, not at matching phase. This is maybe an acceptable choice (I think) but clearly not the only one, it has to be documented.

[GuillaumeGen]

Furthermore, I had a look at the standard and it simply states pattern := term https://github.com/Deducteam/Dedukti-standard#rewrite-rules . I do not think that this is what we want. This means that one can write rules like

[f, x] f x --> x.
[f] (\x => f) --> (\x => x).
[h] F (\x => h 0) --> h.

and all those rules would be valid syntax. Of course, the first 2 break type preservation and they all break confluence, but those are other (later) steps in the processing of files. (And for subject reduction, it is possible to come with a signature such that they are type-preserving).

[GuillaumeGen]

So I would greatly prefer to write a closer to what we do in the various tools implementing the standard grammar for patterns in the standard than modifying this tool to be closer (but still miles away, the examples I gave are refused at parse time currently by Dedukti, and I think (hope) by lambdapi, kontroli, dedukti-js and whichever other implementation I am not (yet) aware of) of the current one. I expect this grammar not to allow type annotations in lambda-abstraction in patterns, but if it does, and if the semantic choice associated to it is that this type annotation must be "universal" (in the sense that whenever a term matches the pattern with the type-annotation erased, then the type of the abstracted variable is convertible to the one written in the pattern), then your PR will be great.

[francoisthire]

It is buggy, and this won't be part of the standard. The semantics implemented was the same one as the brackets one. So a weird semantics which we do not want to specify either.

This MR was wrote after a discussion with Michael and I opened the MR before realising the consequences, and then we realised it was buggy. The standard will be modified accordingly to prevent any type in lambda abstractions for patterns.

[francoisthire]

Concerning

Furthermore, I had a look at the standard and it simply states pattern := term https://github.com/Deducteam/Dedukti-standard#rewrite-rules . I do not think that this is not what we want.

Yeah I was contesting that, but @01mf02insisted a bit and I gave it a try to add types into patterns. The new version of the standard makes something a bit different which is:

• Syntax-wise: Have an optional type annotation for the abstraction constructor for the grammar rules
• Semantics-wise: Say the type is mandatory for terms and absent for patterns

This can be implemented by the grammar rules. The only difference is whether a file that contains:

[H] f (\x: A. H x) --> H

should be refuted by the parser or not (like the scoper).