Ssreflect Users Discussion List

[Georges Gonthier <>]

  This topic is related to another recent discussion about features of the 
Ssreflect matching algorithm.
Recall that Ssreflect uses two passes to find a subterm matching a given 
pattern (unfortunately, this isn't documented in the reference manual).
Ssreflect first looks for a literal match of the pattern, with no conversion 
allowed beyond the initial head beta-iota simplification of the pattern.
keyed matching with full conversion in the arguments of the head constant is 
only used if this first pass fails. The rational for the two-pass approach is 
that it favours "obvious" matches  over ones that require expanding 
constants. For example, one can use rewrite addnA to remove the parentheses 
in a + (b + c) + d even if there is a definition d := e + 3 in the context.
   The current implementation of this first "literal" pass has never been 
entirely satisfactory, because it uses the Ltac routines to match hidden 
inferred implicit arguments and coercion chains exactly, and can thus  miss 
"obvious" matches. Its behaviour is not very robust because it depends tot 
much on type inference specifics; indeed this has been a small but constant 
source of minor regressions in the Ssreflect library.
   Enrico has been considering replacing the matching code for this first 
pass with a more liberal version, that ignores hidden information. If he does 
go through with this, then there would be a much greater chance that an 
"obvious" match fails the subsequent full unification check (this is already 
possible, because the current pass does not check type constraints). Such 
"near misses" could be logged, and subsequently analysed and used to diagnose 
match failures. In Yves' example, this would detect the intended match and 
then complain that bigQ does not unify with EqType.sort _.
   -- Georges
   
, even in the arguments 

-----Original Message-----
From:  
[] On Behalf Of Cyril Cohen
Sent: 06 November 2014 13:42
To: bertot; ssreflect
Subject: Re: [ssreflect] Matter for reflexion: error message

Hi Yves,

On 06/11/2014 14:08, bertot wrote:
> The error message should help users understand that size l == 0 does 
> not match because bigQ  is not an EqType.
> 
> How shall we do that?

Good question, I guess that keyed matching already identified (size l == 0)%B 
as a possible match. So, if the matching algorithm displayed its attempt and 
explained it failed because (size l == 0)%B and (size _ == 0)%B didn't match, 
it would a first good step?

Maybe this is enough for the user to realize he should print the implicit 
arguments in order to realize that the implicit argument of size required by 
size_eq0 is of the form (Equality.sort _). Leading him to (immediately? :)) 
understand that BigQ is not the Equality.sort of anything.

The problem with this kind of more explanatory error message is to avoid 
showing all the time the full trace of matching attempts. Maybe we could 
provide debug flags with some granularity and encourage the user to use it?

Another way to see it, is that this kind of match failure happens a lot in 
mathcomp, so maybe pattern matching could be tweek to add a remark to check 
for missing canonical structures in some particular cases. For
example: how easy would it be to see that unification failed where it could 
have succeeded if there were a canonical projection registered?

Best,
--
Cyril