Add or-patterns support in pattern matching

[zielinsky]

Closes #208

[Copilot]

Pull request overview

This PR adds support for or-patterns in pattern matching, allowing multiple patterns to be combined with the | operator (e.g., First a | Second a => a). This enables more concise pattern matching when multiple constructors should be handled identically. The implementation follows OCaml's or-pattern semantics, requiring that all branches of an or-pattern bind the same variables with compatible types.

Key changes:

• Added POr pattern constructor to the AST across all language levels (Surface, UnifPriv, Unif)
• Implemented type checking for or-patterns with variable binding validation using environment intersection
• Extended pattern compilation to expand or-patterns into multiple clauses during effect inference

Reviewed changes

Copilot reviewed 31 out of 31 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
src/Lang/Surface.ml	Added POr constructor to Surface language AST
src/Lang/UnifPriv/Syntax.ml	Added POr constructor to UnifPriv AST
src/Lang/UnifPriv/Ren.ml	Added renaming support for POr patterns
src/Lang/Unif.mli	Added POr constructor documentation to Unif interface
src/DblParser/YaccParser.mly	Added grammar rules for parsing or-patterns using | separator
src/DblParser/Desugar.ml	Added desugaring of | binary operator in patterns to POr
src/TypeInference/Pattern.ml	Implemented type checking for or-patterns with environment intersection
src/TypeInference/PartialEnv.ml	Added intersect function to validate variable consistency across or-pattern branches
src/TypeInference/PartialEnv.mli	Added interface for environment intersection
src/TypeInference/Unification.ml	Added equal_scheme function for checking scheme equality
src/TypeInference/Unification.mli	Added equal_scheme interface
src/TypeInference/Error.ml	Added error messages for or-pattern variable/type mismatches
src/TypeInference/Error.mli	Added error function interfaces for or-pattern validation
src/TypeInference/RecDefs.ml	Added POr to invalid recursive definition patterns
src/EffectInference/Pattern.ml	Added POr handling and simple environment intersection for effect inference
src/EffectInference/Pattern.mli	Added POr to pattern type definition
src/EffectInference/PatternMatch.ml	Implemented or-pattern expansion during pattern compilation
test/ok/ok0147_or_pattern_basic.fram	Basic or-pattern tests with simple constructors
test/ok/ok0148_or_pattern_basic_2.fram	Extended basic tests with multiple constructors
test/ok/ok0149_or_pattern_exhaustiveness.fram	Tests exhaustiveness checking with or-patterns
test/ok/ok0150_or_pattern_named_fields.fram	Tests or-patterns with named record fields
test/ok/ok0151_or_pattern_nested.fram	Tests nested and chained or-patterns
test/ok/ok0152_or_pattern_pub.fram	Tests or-patterns with public visibility modifiers
test/ok/ok0153_or_pattern_vars_pair.fram	Tests variable binding consistency with pairs
test/ok/ok0154_or_pattern_vars.fram	Basic variable binding tests
test/err/tc_0019_or_pattern_mismatch.fram	Tests error for variables not bound in all branches
test/err/tc_0020_or_pattern_var_mismatch_1.fram	Tests error for inconsistent variable binding (wildcard vs binding)
test/err/tc_0021_or_pattern_var_mismatch_2.fram	Tests error for different variable names across branches
test/err/tc_0022_or_pattern_var_mismatch_3.fram	Tests error for variables in some but not all branches
test/err/tc_0023_or_pattern_scheme_mismatch.fram	Tests error for variables with incompatible types
test/err/tc_0024_or_pattern_module_mismatch.fram	Tests error for inconsistent module bindings

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[ppolesiuk]

I like this direction, but some things should be fixed. The most important ones are:

• parser
• proper handling of existential types in patterns.

[ppolesiuk]

So, or-patterns can be used only at the level of match-clauses. Nested or patterns, like Some(p1 | p2) are not recognized by the parser. There is no reason for such a restriction.

[ppolesiuk]

The implementation forgets variables bound by penv2. This looks correct, because we are already after the type-checking phase, but maybe some additional comment (and assertion?) would be helpful.

[ppolesiuk]

I'm afraid that it would not work, when as-patterns are interleaved with or-patterns. In such a case, the algorithm would return non simplified or-pattern, which will result in assertion fail in line 146. However, I cannot test it, because the parser doesn't allow to use or-patterns under as-patterns.

[ppolesiuk]

This assertion (see comment above).

[ppolesiuk]

Or this (see comments above).

[ppolesiuk]

This condition would never be true, because type variables bound by patterns are bound variables, always refreshed by the algorithm (in a different way in different branches). Proper handling of type variables bound by patterns is not a trivial task (in OCaml, they decided to not handle them at all, and raise an error, when user tries to write an or-pattern with existential types). In Fram we can do betters, since types can be named. But at the beginning, I would follow the simpler OCaml's path, and raise an error, when tvar_tab is non-empty. If you are interested in a better solution, we could talk more on this topic.

[ppolesiuk]

I get "assertion failed" for this code.

data T = C of {type X} | D of {type X}

let foo x =
  match x with
  | C | D => ()
  end

[Copilot]

Pull request overview

Copilot reviewed 35 out of 35 changed files in this pull request and generated no new comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.