Thanks, indeed List.map snd ... is not right -- I'm not sure why I thought it would work.

Regarding the first commit, that it is the only one that I suggested that you could cherry-pick into #1550 -- not the second commit which indeed is independent.

This code is non-trivial to write because it is the only one where we have both a negative matrix and a positive matrix. In other functions (for example the satisfiable variables) we have only a positive row, and then they work by specializing the negative matrix in each case. Here we need to do a cross-product, splitting submatrices for both matrices -- or we could have done only a single split on the joint matrix, but this would require API changes and is hard with different row types.

The reason why the other functions get away with only a positive row (instead of the general case of a positive matrix) is that they have an easy operation to join the results of two "parallel" calls, the calls on the two sides of an or-pattern (for satisfiable the join is just ||). I don't know (it is not obvious) whether this function can be rewritten in this style.

I think I'll wait until #1550 is merged to make another iteration on this PR, taking your comments/suggestions into account.

@trefis: I just rebased this PR, and I changed the algorithm to split on all rows (positive and negative) at the same time -- kind of cool. Let me know what you think.

(I have left the handling of the default matrix in the non-empty-constrs case unchanged, while it is not completely clear to me that it is actually correct. But I think it is.)

OK, I think I know what the issue is:

In the case where constrs is not nil, you say:

If the first column contains some head constructors, there
is no need to look at stability for the default matrix: all
other submatrices contain the default matrix, so they have
less stable variables.

But that's actually wrong.
The default matrix might also contain fewer negative rows, and so it might contain more unstable variables!

On the example I have given, the problem appears as follow

neg | Val A1    Val A1 |
pos | Val x     _      |
pos | _         Val x  |

Which will be split into:

            neg | A1   Val A1 |
constrs = [ pos | _    _      | ]
            pos | _    Val x  |

default = pos | _   _     |
          pos | _   Val x |

And then you recurse only on constrs (note that recursing on this first default matrix would have given you a warning I believe).

Which is further split into:

            neg | Val A1 |
constrs = [ pos | _      | ]
            pos | Val x  |

default = pos | _     |
          pos | Val x |

And again:

            neg | A1 |
constrs = [ pos | _  | ]
            pos | _  |

default = pos | _ |
          pos | _ |

And one last time:

            neg | |
constrs = [ pos | | ]
            pos | |

default = pos | |
          pos | |

At which point when you recurse on the only constrs matrix you say "oh I have a negative row, all the variables must be stable!".

The thing that is a bit sad is that if we recurse on the default matrix as well as on the constrs matrices, we will get the warning even if A1 is alone in its signature.
But I don't see any easy way around that. Perhaps simplify_head_amb_pat_* could check if a constructor is alone in its signature and replace it by omega but that seems britle, and doesn't extend well ("signature" is too loosely defined in our untyped world)

Also, I meant to say: simplify_first_amb_col reads to me like "simplify the first ambiguous column" which is not what's going on.

How about introducing submodules which will contain a "row" type and the correspond simplification functions?

At which point when you recurse on the only constrs matrix you say "oh I have a negative row, all the variables must be stable!".

The thing that is a bit sad is that if we recurse on the default matrix as well as on the constrs matrices, we will get the warning even if A1 is alone in its signature.

Actually, that hints at the fact that we probably want to call full_match to decide whether we want to consider the default matrix or the specialized submatrices.
I'll let you check it out, I'm done for today!

Excellent observations and interesting feedback -- as I am getting used to. Thanks!

I made a first batch of easy changes that addresses some of your comment (and optimizes the special case where there is no positive row left in the matrix). In particular, I believe that the default issue is fixed in the most natural (and least clever) way, by defining submatrices as default :: List.map snd constrs. Feedback is welcome. I plan to use your suggestion of sub-modules and propose this change later in the day.

(I'm also interested in playing with full_match, we'll see.)

I just pushed a new commit that uses full_match in a surprisingly simple way (minor point, but it's a bit annoying that full_match [] raises an assert false instead of returning false) that I believe is correct. I use your testcase with type a = A1;; to check that the behavior you expect works.

I think I agree with you that the current implementation is correct.

I'll resume nitpicking then:

• some (comment) lines are over 80c

• in one of the base cases of the algorithm you say:

  if at least one row is negative, the matrix matches no value

  this is poorly formulated (the matrix does match some values, doesn't it?), I'd go with something along the line of "if the matrix still has a negative row, that row will match before any positive one", and I'd move the comment to the place where we catch the exception and return All.

in one of the base cases of the algorithm you say:

if at least one row is negative, the matrix matches no value

this is poorly formulated (the matrix does match some values, doesn't it?), I'd go with something along the line of "if the matrix still has a negative row, that row will match before any positive one", and I'd move the comment to the place where we catch the exception and return All.

I think we are misunderstanding each other here and we should dig in. The comment is there (only) in the case where the rows are empty (a non-empty matrix with several empty rows). One or several empty positive rows matches exactly one vector of values (the empty vector), but the presence of a negative row means that this empty vector is rejected, so the matrix matches nothing.

that row will match before any positive one

Note that, in matrix_stable_vars, I don't consider an order between the rows -- the result of the function does not depend on the row order. For the positive rows, stability is precisely about computing who doesn't depend on the matching order. For the negative rows, the idea is that the value space is the same no matter what the order is. In practice, I think that the order is preserved (negative rows start at the top, and I think they stay at the top), but the semantics of the function is that a negative row anywhere kills this sub-space of values before they reach any of the positive rows.

(Most other functions in Parmatch have this characteristic that they are insensitive to the row order. The order comes in in the choice of who is pss and who is rs.)

@trefis two points:

• The Module-using change is rather invasive, in part because it encourages me to indent larger blocks of code. I would prefer to do it as a separate PR, so that it does not trash the whole diff, either before we try to merge this PR or after it.

• I think that you are moving from the spot of "reviewer" to the spot of "co-author" in the (yet unwritten) Changes entry, which means that we need @maranget to review it when we both agree that we like the current state.

• Delaying the renaming / introduction of modules sounds fine.
• Having Luc review this is obviously a good idea, regardless of my "spot" :)

Going back to the discussion about ordering and such:
When you arrive on a matrix with no columns but at least one (and potentially more) row then they are all matching the same empty vector (if you ignore the polarity of the row), I think we both agree on that.

Now, I guess your interpretation of the polarity in some way leads you to saying that "if I have a negative row, then the matrix doesn't filter the empty vector": you are changing the definition of what it means for a matrix to filter a value in presence of polarity. That might be fine, but I wasn't reasoning about it in the same way and it is also never made explicit in your documentation/comments (but of course I might have missed the relevant comment).

The way I was thinking about it was more in line with the other comments you've placed in the code (on the definition of signed):

To track this information, the matrices we analyze contain both positive rows,
that describe the rows currently being analyzed (of type amb_row, so that their
varsets are tracked) and negative rows, that describe the cases already
matched against.

Indeed even though in the matrix the rows order is irrelevant (and not guaranteed) the guarantee you have is we consider the clauses of the pattern matching in order, and grow our set of negative rows as we go.

I see this as coherent with the last part of your message above, i.e.

For the negative rows, the idea is that the value space is the same no matter what the order is.
[...] the semantics of the function is that a negative row anywhere kills this sub-space of values before they reach any of the positive rows.

which is what I was roughly trying to express previously.

Does that make sense?

I made two small changes suggested by Luc during his review:

• the optimization of all-negative rows is implemented by an if instead of a when
• the construction of the initial matrix in pattern_stable_vars is written in a slightly
  different way that restores the expected row order (the row order is irrelevant in
  the algorithm, but we can still finesse about it)

Edit: the plan is to merge the PR if the CI passes. @trefis, if you wish to tell Github that the changes you requested have been performed, now is the time.

Sorry, I forgot to change that comment. I will do this soon, before merging -- currently I am rebasing #1560 and #1561 against this one.

@trefis thinking about this more, I think that it is correct to say explicitly that the semantics of a signed matrix is different from the semantics of a non-signed matrix: their set-of-values interpretation is not the same. To this end, I amended the comment introducing signed as follows:

    To track this information, the matrices we analyze contain both
    *positive* rows, that describe the rows currently being analyzed
-   (of type amb_row, so that their varsets are tracked) and *negative
-   rows*, that describe the cases already matched against. A variable
-   is stable if, for any value not matched by any of the negative
-   rows, the environment captured by any of the matching positive rows
-   is identical.
+   (of type Varsets.row, so that their varsets are tracked) and
+   *negative rows*, that describe the cases already matched against.
+
+   The values matched by a signed matrix are the values matched by
+   some of the positive rows but none of the negative rows. In
+   particular, a variable is stable if, for any value not matched by
+   any of the negative rows, the environment captured by any of the
+   matching positive rows is identical.
 *)
 type ('a, 'b) signed = Positive of 'a | Negative of 'b

I believe that the comment in the function itself is now correct with respect to that interpretation.

(Maybe it would be even clearer to explicitly distinguish the "semantics as a matrix" and the "semantics as a signed matrix" (the signed semantics), and say something like "the signed semantics of m is empty" or at least "the signed matrix m is empty".)

thinking about this more, I think that it is correct to say explicitly that the semantics of a signed matrix is different from the semantics of a non-signed matrix: their set-of-values interpretation is not the same.

Yep, that's the other way to fix "the issue".
I have no problem with that option: as long are the comments are all consistent, I'll be happy.

Your new comment on signed seems enough indeed. I'd be curious to see your "more explicit" version, but probably you can keep it for the paper you'll surely write about this.