Ocaml syntax extension

I have a question concerning Ocaml pattern matching extension. More clearly, my task is to extend the existing syntactic pattern matching algorithm the Ocaml language use with other more general matching (equational matching).
For example, if we have an ocaml program:
let foo x = match x with p1 → exp1’ | p2 → exp2’ …

I want to have a matching algorithm integrated in the language which solves exp1 << x not only syntactically also with modulo some theory.

Could you tell me please what library would be best to look? Any suggestions will be helpful. Thank you

I guess you need to type if x = p1 then exp1 else if x = p2 then exp2 else exp0. Or something like this.

The variable names in a match syntax is already used to deconstruct structures: match tuple with (p1,p2) -> exp. Then they can’t be used to mean something that must be compared to x in your example. The when token can be used to express conditions, but it can be clumsy if all you need can be written with if/then/else.

match x with
  x when x = p1 -> exp1
…

Perhaps you would like a new token that can be used to make an expression seen as a constant:

match x with
   (const p1, p2) -> …

Would be a syntactic sugar for:


match x with
   (p1', p2) when p1=p1' -> …

I guess the introduction of your modulo equality can be written with a let open M in … where the M module has a (=) operator redefined.

I don’t think a library can solve a syntax need. At best, you have a function which can be used to compare your x with a set of expression and evaluate the first corresponding expression. But I don’t think it will be more handy than a set of if/then/else. ppx rewriters are more powerful. I guess a:

match%extended x with Const(p1) -> exp1

Can be rewritten in what you want. You may search GitHub - ocaml-ppx/ppx_view: A ppx rewriter that provides pattern matching on abstract types by transforming patterns into views/expressions. but an old compiler seems to be required.

Many thanks for your valuable feedback.

I need to have several constructors like matchTheory … with. For example, if I want to use commutative matching, I should be able to write the following program

let foo pair =
matchC pair with
| (x, a) → x

where ‘matchC’ stands for commutative matching.

in this case, let result = foo (a, b) as well result = foo (b, a) should result b.

Best regards,
Tornike

Therefore, I probably need to change/modify existing pattern matching (existing library). Any feedback would be welcome for this matter.