Add or-patterns support in pattern matching by zielinsky · Pull Request #287 · fram-lang/dbl

zielinsky · 2025-12-04T00:21:00Z

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.

src/TypeInference/Error.ml

ppolesiuk

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

parser
proper handling of existential types in patterns.

src/DblParser/YaccParser.mly

src/EffectInference/Pattern.ml

src/EffectInference/PatternMatch.ml

src/TypeInference/PartialEnv.ml

ppolesiuk · 2025-12-11T11:32:02Z

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.

Copilot

Pull request overview

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

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

src/TypeInference/PartialEnv.ml

Copilot

Pull request overview

Copilot reviewed 36 out of 36 changed files in this pull request and generated 2 comments.

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

ppolesiuk · 2026-03-23T10:14:12Z

src/TypeInference/PartialEnv.ml

+        merge_opts t1 t2
+          ~on_mismatch:(fun () -> Error.report (Error.or_pattern_type_vars_mismatch ~pos t_name))
+          ~on_both:(fun t1 t2 ->
+            if not (T.TVar.equal t1 t2) then
+              Error.report (Error.or_pattern_type_vars_mismatch ~pos t_name);
+            Some t1)


Currently, or-patterns cannot bind type variables. This piece of code could be removed, and replaced by raising an appropriate error.

ppolesiuk · 2026-03-23T10:16:14Z

src/TypeInference/PartialEnv.ml

+let intersect_val_info ~check_schemes ~pp ~pos name info1 info2 =
+  merge_opts info1 info2
+    ~on_mismatch:(fun () -> Error.report (Error.or_pattern_vars_mismatch ~pos ~pp name))
+    ~on_both:(fun info1 info2 ->
+      Option.iter (fun check -> check info1.vi_scheme info2.vi_scheme) check_schemes;
+      Some info1)


I agree that public/private attribute should be taken into account.

ppolesiuk · 2026-03-23T09:52:48Z

src/DblParser/YaccParser.mly

 : KW_RETURN  expr ARROW2 expr { make (HCReturn($2, $4))  }
 | KW_FINALLY expr ARROW2 expr { make (HCFinally($2, $4)) }


Is there any reason, why parentheses are required around or patterns in return an finally clauses?

Suggested change

: KW_RETURN pattern ARROW2 expr { make (HCReturn($2, $4)) }

| KW_FINALLY pattern ARROW2 expr { make (HCFinally($2, $4)) }

ppolesiuk · 2026-03-23T10:08:06Z

src/TypeInference/PartialEnv.ml

+  let ren =
+    Name.Map.fold (fun name info2 ren ->
+      match Name.Map.find_opt name penv1.val_map with
+      | Some info1 -> T.Ren.add_var ren info2.vi_var info1.vi_var
+      | None -> ren
+    ) penv2.val_map (T.Ren.empty ~scope)
+  in
+  let ren =
+    StrMap.fold (fun mname minfo2 ren ->
+      match StrMap.find_opt mname penv1.module_map with
+      | Some minfo1 ->
+        let vars1 =
+          List.fold_left
+            (fun m (name, var, _) -> Name.Map.add name var m)
+            Name.Map.empty minfo1.mi_vals
+        in
+        List.fold_left
+          (fun ren (name, var2, _) ->
+            match Name.Map.find_opt name vars1 with
+            | Some var1 -> T.Ren.add_var ren var2 var1
+            | None -> ren)
+          ren minfo2.mi_vals
+      | None -> ren
+    ) penv2.module_map ren
+  in


The code that builds the renaming became quite large, so it deserves to be a separate function. This would increase the code readability. Moreover, some pieces of the code seems to be repeated. I believe that it could be refactored.

ppolesiuk · 2026-03-23T10:14:12Z

src/TypeInference/PartialEnv.ml

+        merge_opts t1 t2
+          ~on_mismatch:(fun () -> Error.report (Error.or_pattern_type_vars_mismatch ~pos t_name))
+          ~on_both:(fun t1 t2 ->
+            if not (T.TVar.equal t1 t2) then
+              Error.report (Error.or_pattern_type_vars_mismatch ~pos t_name);
+            Some t1)


Currently, or-patterns cannot bind type variables. This piece of code could be removed, and replaced by raising an appropriate error.

ppolesiuk · 2026-03-23T10:16:14Z

src/TypeInference/PartialEnv.ml

+let intersect_val_info ~check_schemes ~pp ~pos name info1 info2 =
+  merge_opts info1 info2
+    ~on_mismatch:(fun () -> Error.report (Error.or_pattern_vars_mismatch ~pos ~pp name))
+    ~on_both:(fun info1 info2 ->
+      Option.iter (fun check -> check info1.vi_scheme info2.vi_scheme) check_schemes;
+      Some info1)


I agree that public/private attribute should be taken into account.

ppolesiuk

And of course, merge conflicts should be resolved.

zielinsky force-pushed the or-patterns branch from 70b2e46 to d8d60ac Compare December 4, 2025 00:26

zielinsky requested a review from Copilot December 4, 2025 00:27

Copilot started reviewing on behalf of zielinsky December 4, 2025 00:28 View session

Copilot finished reviewing on behalf of zielinsky December 4, 2025 00:33

Copilot AI reviewed Dec 4, 2025

View reviewed changes

src/TypeInference/Error.ml Outdated Show resolved Hide resolved

zielinsky force-pushed the or-patterns branch from d8d60ac to 2172c9f Compare December 4, 2025 01:05

zielinsky marked this pull request as ready for review December 4, 2025 11:28

add or-patterns

8aa64cd

zielinsky force-pushed the or-patterns branch from 2172c9f to 8aa64cd Compare December 5, 2025 13:03

zielinsky added 1. type inference Type inference and the Unif language 2. effect inference Effect inference and the ConE language 2.1. pattern-matching Compilation of deep pattern-matching labels Dec 5, 2025

ppolesiuk requested changes Dec 11, 2025

View reviewed changes

ppolesiuk mentioned this pull request Dec 14, 2025

Fram backend fram-lang/cpspg#4

Open

zielinsky marked this pull request as draft December 16, 2025 14:09

zielinsky force-pushed the or-patterns branch from 67946f4 to 1ea9a3d Compare January 29, 2026 11:05

zielinsky requested a review from Copilot January 29, 2026 11:07

Copilot started reviewing on behalf of zielinsky January 29, 2026 11:08 View session

zielinsky force-pushed the or-patterns branch from 1ea9a3d to 04b29a5 Compare January 29, 2026 11:11

Copilot AI reviewed Jan 29, 2026

View reviewed changes

zielinsky force-pushed the or-patterns branch from 04b29a5 to f6caa17 Compare January 29, 2026 11:37

address review

47a2d64

zielinsky force-pushed the or-patterns branch from f6caa17 to 47a2d64 Compare January 29, 2026 12:53

zielinsky requested a review from Copilot March 13, 2026 06:49

Copilot started reviewing on behalf of zielinsky March 13, 2026 06:49 View session

Copilot AI reviewed Mar 13, 2026

View reviewed changes

src/TypeInference/PartialEnv.ml Show resolved Hide resolved

zielinsky force-pushed the or-patterns branch from f12d7d9 to c7cd2c4 Compare March 15, 2026 22:09

zielinsky marked this pull request as ready for review March 15, 2026 22:21

clean tests and address review

20331f2

zielinsky force-pushed the or-patterns branch from c7cd2c4 to 20331f2 Compare March 15, 2026 22:27

zielinsky requested review from Copilot and ppolesiuk March 15, 2026 22:30

Copilot started reviewing on behalf of zielinsky March 16, 2026 11:34 View session

Copilot AI reviewed Mar 16, 2026

View reviewed changes

ppolesiuk requested changes Mar 23, 2026

View reviewed changes

ppolesiuk reviewed Mar 23, 2026

View reviewed changes

		: KW_RETURN expr ARROW2 expr { make (HCReturn($2, $4)) }
		\| KW_FINALLY expr ARROW2 expr { make (HCFinally($2, $4)) }


	: KW_RETURN pattern ARROW2 expr { make (HCReturn($2, $4)) }
	\| KW_FINALLY pattern ARROW2 expr { make (HCFinally($2, $4)) }

Conversation

zielinsky commented Dec 4, 2025

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

ppolesiuk left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ppolesiuk commented Dec 11, 2025

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

ppolesiuk Mar 23, 2026

Choose a reason for hiding this comment

Uh oh!

ppolesiuk Mar 23, 2026

Choose a reason for hiding this comment

Uh oh!

ppolesiuk Mar 23, 2026

Choose a reason for hiding this comment

Uh oh!

ppolesiuk Mar 23, 2026

Choose a reason for hiding this comment

Uh oh!

ppolesiuk Mar 23, 2026

Choose a reason for hiding this comment

Uh oh!

ppolesiuk Mar 23, 2026

Choose a reason for hiding this comment

Uh oh!

ppolesiuk left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants