Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
c04bd2d
feat(and-patterns): parser + AST + frontend plumbing
ggreif Apr 23, 2026
763dd68
test(and-patterns): run + fail coverage for frontend behaviour
ggreif Apr 23, 2026
7b4d8ae
refactor(and-patterns): express AST-interpreter match_pat in monadic …
ggreif Apr 23, 2026
ac6d7ba
feat(and-patterns): plumb through IR, middle-end passes, and codegen
ggreif Apr 23, 2026
b351b22
docs(changelog): add Next entry for and-patterns (#6049)
ggreif Apr 23, 2026
e7f728d
docs(and-patterns): language-manual section + fundamentals-table row
ggreif Apr 23, 2026
bfe6a06
test(and-patterns): cover codegen CanFail paths and disjoint-bindings…
ggreif Apr 23, 2026
6aac4f7
Merge branch 'master' into gabor/and-patterns
ggreif Apr 23, 2026
39cc51a
test: accept parser-error listing now including `and <pat_bin>`
ggreif Apr 23, 2026
91722b3
tweak
ggreif Apr 23, 2026
c4b1066
and-patterns: dedicated M0260 error code + style polish
ggreif Apr 23, 2026
6d25f82
test: fix stale M0189 reference in and-pattern-overlap-case comment
ggreif Apr 23, 2026
7a75752
coverage(and-patterns): proper InAnd1 context + dedicated test
ggreif Apr 23, 2026
1b332d7
and-patterns: dedicated M0261 for 'cannot infer', stop reusing M0184
ggreif Apr 23, 2026
1355414
test: exercise M0261 'cannot infer and-pattern' via func-arg AndP
ggreif Apr 23, 2026
4633157
Merge branch 'master' into gabor/and-patterns
ggreif Apr 24, 2026
753404c
refactor(and-patterns): rigour in check_ir and M0260 parity in let-co…
ggreif Apr 24, 2026
3e730ff
test(and-patterns): cover type-mismatched legs
ggreif Apr 24, 2026
844603e
docs(and-patterns): fix stale M0184 comment and clarify check-mode
ggreif Apr 24, 2026
28229fd
refactor(check_ir): use verify_pair in check_pats sibling-disjointness
ggreif Apr 24, 2026
5c8380c
feat(and-patterns): propagate one-leg inference into the other leg
ggreif Apr 24, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Changelog.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

* motoko (`moc`)

* feat: and-patterns — `(p1 and p2)` matches when both legs match, binding from both (#6049).
* feat: Add null-coalescing operator `??` (#5722).
`e1 ?? e2` evaluates to the unwrapped contents of `e1` when `e1` is `?v`,
otherwise to `e2`. The right-hand side is evaluated lazily (short-circuit).
Expand Down
12 changes: 11 additions & 1 deletion doc/md/16-language-manual.md
Original file line number Diff line number Diff line change
Expand Up @@ -1618,7 +1618,17 @@ The or pattern `<pat1> or <pat2>` is a disjunctive pattern.

The result of matching `<pat1> or <pat2>` against a value is the result of matching `<pat1>`, if it succeeds, or the result of matching `<pat2>`, if the first match fails.

An `or`-pattern may contain identifier (`<id>`) patterns with the restriction that both alternatives must bind the same set of identifiers. Each identifier's type is the least upper bound of its type in `<pat1>` and `<pat2>`.
An `or`-pattern may contain identifier (`<id>`) patterns with the restriction that both alternatives must bind the same set of identifiers. Each identifier's type is the least upper bound of the types assigned to it by `<pat1>` and `<pat2>`.

### And pattern

The and pattern `<pat1> and <pat2>` is a conjunctive pattern.

The result of matching `<pat1> and <pat2>` against a value is the union of the bindings produced by matching `<pat1>` and then `<pat2>`, both against the same value. The match fails if either sub-match fails.

Unlike an `or`-pattern, the two sides of an `and`-pattern must bind *disjoint* sets of identifiers; a name bound in both sides is a type error.

`and` binds tighter than `or`, so `<pat1> or <pat2> and <pat3>` parses as `<pat1> or (<pat2> and <pat3>)`.

### Expression declaration

Expand Down
1 change: 1 addition & 0 deletions doc/md/examples/grammar.txt
Original file line number Diff line number Diff line change
Expand Up @@ -320,6 +320,7 @@
<pat_bin> ::=
<pat_un>
<pat_bin> 'or' <pat_bin>
<pat_bin> 'and' <pat_bin>
<pat_bin> ':' <typ>

<pat> ::=
Expand Down
3 changes: 2 additions & 1 deletion doc/md/fundamentals/8-pattern-matching.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ Motoko supports several types of patterns:
| Named | Introduces identifiers into a new scope. | `age`, `x` |
| Tuple | Must have at least two components. | `( component0, component1, …​ )` |
| Alternative (`or`-pattern) | Match multiple patterns. | `0 or 1` |
| Conjunctive (`and`-pattern) | Match both patterns; bindings combine. | `?x and s` |

## Concepts

Expand All @@ -29,7 +30,7 @@ Unlike traditional `enum` types in other languages, which define fixed sets of v

### Irrefutable and refutable patterns

Patterns are either refutable** or irrefutable. A refutable pattern can fail to match (like literal patterns or specific variant tags). An irrefutable pattern always matches any value of its type. Examples include the wildcard `_`, simple variable names, or structured patterns (like records or tuples) made only from irrefutable parts.
Patterns are either **refutable** or **irrefutable**. A refutable pattern can fail to match (like literal patterns or specific variant tags). An irrefutable pattern always matches any value of its type. Examples include the wildcard `_`, simple variable names, or structured patterns (like records or tuples) made only from irrefutable parts.

### Singleton types

Expand Down
9 changes: 9 additions & 0 deletions src/codegen/compile_classical.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13166,6 +13166,12 @@ and fill_pat env ae pat : patternCode =
CannotFail set_i ^^^
orElse (CannotFail get_i ^^^ code1)
(CannotFail get_i ^^^ code2)
| AndP (p1, p2) ->
let code1, code2 = fill_pat env ae p1, fill_pat env ae p2 in
let set_i, get_i = new_local env "and_scrut" in
CannotFail set_i ^^^
(CannotFail get_i ^^^ code1) ^^^
(CannotFail get_i ^^^ code2)

and alloc_pat_local env ae pat =
let d = Freevars.pat pat in
Expand Down Expand Up @@ -13441,6 +13447,9 @@ and destruct_const_pat ae pat const : VarEnv.t option = match pat.it with
let l = destruct_const_pat ae p1 const in
if l = None then destruct_const_pat ae p2 const
else l
| AndP (p1, p2) ->
Option.bind (destruct_const_pat ae p1 const) (fun ae' ->
destruct_const_pat ae' p2 const)
| TupP ps ->
let cs = match const with (_, Const.Tuple cs) -> cs | (_, Const.Unit) -> [] | _ -> assert false in
let go ae p c = match ae with
Expand Down
14 changes: 14 additions & 0 deletions src/codegen/compile_enhanced.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13492,6 +13492,16 @@ and fill_pat env ae pat : patternCode =
CannotFail set_i ^^^
orElse (CannotFail get_i ^^^ code1)
(CannotFail get_i ^^^ code2)
| AndP (p1, p2) ->
(* Both legs must match the same scrutinee; bindings from both
are available. Stash the scrutinee once, feed it to each leg
in sequence. `(^^^)` threads failure through — either leg's
failure cancels the whole match. *)
let code1, code2 = fill_pat env ae p1, fill_pat env ae p2 in
let set_i, get_i = new_local env "and_scrut" in
CannotFail set_i ^^^
(CannotFail get_i ^^^ code1) ^^^
(CannotFail get_i ^^^ code2)

and alloc_pat_local env ae pat =
let d = Freevars.pat pat in
Expand Down Expand Up @@ -13767,6 +13777,10 @@ and destruct_const_pat ae pat const : VarEnv.t option = match pat.it with
let l = destruct_const_pat ae p1 const in
if l = None then destruct_const_pat ae p2 const
else l
| AndP (p1, p2) ->
(* Both legs must accept; fold bindings left-to-right. *)
Option.bind (destruct_const_pat ae p1 const) (fun ae' ->
destruct_const_pat ae' p2 const)
| TupP ps ->
let cs = match const with Const.Tuple cs -> cs | Const.Unit -> [] | _ -> assert false in
let go ae p c = match ae with
Expand Down
5 changes: 5 additions & 0 deletions src/docs/namespace.ml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,11 @@ let rec idents_in_pattern : Syntax.pat -> string list =
| Syntax.AnnotP (p, _)
| Syntax.ParP p ->
idents_in_pattern p
| Syntax.AndP (p1, p2) ->
(* typechecker rejects overlapping bindings across legs, but
this helper may run on not-yet-checked code (mo-doc), so
dedupe defensively *)
List.sort_uniq compare (idents_in_pattern p1 @ idents_in_pattern p2)
| Syntax.WildP | Syntax.SignP (_, _) | Syntax.LitP _ -> []

let from_module =
Expand Down
1 change: 1 addition & 0 deletions src/ir_def/arrange_ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,7 @@ and pat p = match p.it with
| OptP p -> "OptP" $$ [ pat p ]
| TagP (i, p) -> "TagP" $$ [ id i; pat p ]
| AltP (p1,p2) -> "AltP" $$ [ pat p1; pat p2 ]
| AndP (p1,p2) -> "AndP" $$ [ pat p1; pat p2 ]

and lit = function
| NullLit -> Atom "NullLit"
Expand Down
26 changes: 24 additions & 2 deletions src/ir_def/check_ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -149,6 +149,12 @@ let disjoint_union env at fmt env1 env2 =
try T.Env.disjoint_union env1 env2
with T.Env.Clash k -> error env at fmt k

(* Error on the first key of env1 that falsifies `ok k env2`, naming
that key via `fmt`. A cheap iter + predicate test, without the
raise/catch machinery of `disjoint_union`. *)
let verify_pair env at fmt ok env1 env2 =
T.Env.iter (fun k _ -> if not (ok k env2) then error env at fmt k) env1

(* Types *)

(* FIX ME: these error reporting functions are eager and will construct unnecessary type strings !*)
Expand Down Expand Up @@ -1037,6 +1043,11 @@ and gather_pat env const ve0 pat : val_env =
let ve1, ve2 = go ve pat1, go ve pat2 in
let common i1 i2 = { typ = lub env i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in
T.Env.merge (fun _ -> Lib.Option.map2 common) ve1 ve2
| AndP (pat1, pat2) ->
(* pre-population only; check_pat below rejects overlapping
bindings via verify_pair, so IR loaded from disk is
validated without trusting the frontend *)
go (go ve pat1) pat2
| OptP pat1
| TagP (_, pat1) ->
go ve pat1
Expand Down Expand Up @@ -1087,14 +1098,25 @@ and check_pat env pat : val_env =
error env pat.at "set of bindings differ for alternative pattern";
let common i1 i2 = { typ = lub env i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in
T.Env.merge (fun _ -> Lib.Option.map2 common) ve1 ve2
| AndP (pat1, pat2) ->
(* both legs must accept the scrutinee; verify_pair enforces
disjoint bindings without trusting the frontend *)
let ve1 = check_pat env pat1 in
let ve2 = check_pat env pat2 in
t <: pat1.note;
t <: pat2.note;
verify_pair env pat.at "duplicate binding for %s in and-pattern"
(fun k ve2 -> not (T.Env.mem k ve2)) ve1 ve2;
T.Env.adjoin ve1 ve2

and check_pats at env pats ve : val_env =
match pats with
| [] -> ve
| pat::pats' ->
let ve1 = check_pat env pat in
let ve' = disjoint_union env at "duplicate binding for %s in pattern" ve ve1 in
check_pats at env pats' ve'
verify_pair env at "duplicate binding for %s in pattern"
(fun k ve -> not (T.Env.mem k ve)) ve1 ve;
check_pats at env pats' (T.Env.adjoin ve ve1)

and check_pat_fields env t = List.iter (check_pat_field env t)

Expand Down
1 change: 1 addition & 0 deletions src/ir_def/freevars.ml
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,7 @@ let rec pat p : td = match p.it with
| OptP p
| TagP (_, p) -> pat p
| AltP (p1, p2) -> pat p1 +- pat p2
| AndP (p1, p2) -> pat p1 +- pat p2

and pats ps : td = List.(fold_left (+-) M.empty (map pat ps))

Expand Down
1 change: 1 addition & 0 deletions src/ir_def/ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ and pat' =
| OptP of pat (* option *)
| TagP of Type.lab * pat (* variant *)
| AltP of pat * pat (* disjunctive *)
| AndP of pat * pat (* conjunctive *)

and pat_field = pat_field' Source.phrase
and pat_field' = {name : Type.lab; pat : pat}
Expand Down
1 change: 1 addition & 0 deletions src/ir_def/ir_utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ let rec is_irrefutable p = match p.it with
| TupP pats -> List.for_all is_irrefutable pats
| ObjP pfs -> List.for_all (fun (pf : pat_field) -> is_irrefutable pf.it.pat) pfs
| AltP (pat1, _) -> is_irrefutable pat1
| AndP (pat1, pat2) -> is_irrefutable pat1 && is_irrefutable pat2
| WildP | VarP _ -> true
| TagP _ | LitP _ | OptP _ -> false

Expand Down
6 changes: 6 additions & 0 deletions src/ir_def/rename.ml
Original file line number Diff line number Diff line change
Expand Up @@ -144,6 +144,10 @@ and pat' rho = function
end;
let rho' = ids_bind rho is1 in
(AltP (pat_subst rho' p1, pat_subst rho' p2), rho')
| AndP (p1, p2) ->
let (p1', rho') = pat rho p1 in
let (p2', rho'') = pat rho' p2 in
(AndP (p1', p2'), rho'')

and pats rho ps =
match ps with
Expand Down Expand Up @@ -173,6 +177,8 @@ and pat_subst' rho = function
TagP (i, pat_subst rho p)
| AltP (p1, p2) ->
AltP (pat_subst rho p1, pat_subst rho p2)
| AndP (p1, p2) ->
AndP (pat_subst rho p1, pat_subst rho p2)

and pats_subst rho ps =
List.map (pat_subst rho) ps
Expand Down
1 change: 1 addition & 0 deletions src/ir_def/subst_var.ml
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,7 @@ and pat' rho = function
List.compare String.compare is1 is2 = 0
end;
ids_bind rho is1
| AndP (p1, p2) -> pat (pat rho p1) p2

and pats rho ps = List.fold_left pat rho ps

Expand Down
4 changes: 4 additions & 0 deletions src/ir_interpreter/interpret_ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -690,6 +690,7 @@ and declare_pat pat : val_env =
| OptP pat1
| TagP (_, pat1) -> declare_pat pat1
| AltP (pat1, _pat2) -> declare_pat pat1 (* pat2 has the same bindings *)
| AndP (pat1, pat2) -> V.Env.adjoin (declare_pat pat1) (declare_pat pat2)

and declare_pats pats ve : val_env =
match pats with
Expand Down Expand Up @@ -761,6 +762,9 @@ and match_pat pat v : val_env option =
| None -> match_pat pat2 v
| some -> some
)
| AndP (pat1, pat2) ->
Option.(bind (match_pat pat1 v) (fun ve1 ->
map (V.Env.adjoin ve1) (match_pat pat2 v)))

and match_pats pats vs ve : val_env option =
match pats, vs with
Expand Down
2 changes: 2 additions & 0 deletions src/ir_passes/async.ml
Original file line number Diff line number Diff line change
Expand Up @@ -518,6 +518,8 @@ let transform prog =
TagP (i, t_pat pat1)
| AltP (pat1, pat2) ->
AltP (t_pat pat1, t_pat pat2)
| AndP (pat1, pat2) ->
AndP (t_pat pat1, t_pat pat2)

and t_typ_bind' tb =
{ tb with con = t_con tb.con; bound = t_typ tb.bound }
Expand Down
7 changes: 7 additions & 0 deletions src/ir_passes/await.ml
Original file line number Diff line number Diff line change
Expand Up @@ -562,6 +562,7 @@ and declare_pat pat exp : exp =
| OptP pat1
| TagP (_, pat1) -> declare_pat pat1 exp
| AltP (pat1, pat2) -> declare_pat pat1 exp
| AndP (pat1, pat2) -> declare_pat pat1 (declare_pat pat2 exp)

and declare_pats pats exp : exp =
match pats with
Expand Down Expand Up @@ -597,6 +598,10 @@ and rename_pat' pat =
assert(Freevars.(M.is_empty (pat pat1)));
assert(Freevars.(M.is_empty (pat pat2)));
(PatEnv.empty,pat.it)
| AndP (pat1, pat2) ->
let (patenv1, pat1') = rename_pat pat1 in
let (patenv2, pat2') = rename_pat pat2 in
(PatEnv.disjoint_union patenv1 patenv2, AndP (pat1', pat2'))

and rename_pats pats =
match pats with
Expand All @@ -621,6 +626,8 @@ and define_pat patenv pat : dec list =
assert(Freevars.(M.is_empty (pat pat1)));
assert(Freevars.(M.is_empty (pat pat2)));
[]
| AndP (pat1, pat2) ->
define_pat patenv pat1 @ define_pat patenv pat2

and define_pats patenv (pats : pat list) : dec list =
List.concat_map (define_pat patenv) pats
Expand Down
1 change: 1 addition & 0 deletions src/ir_passes/const.ml
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,7 @@ let rec pat env p = match p.it with
| TupP pats -> List.fold_left pat env pats
| ObjP pfs -> List.fold_left pat env (pats_of_obj_pat pfs)
| AltP (pat1, _) | OptP pat1 | TagP (_, pat1) -> pat env pat1
| AndP (pat1, pat2) -> pat (pat env pat1) pat2

let find v env = match M.find_opt v env with
| None -> raise (Invalid_argument (Printf.sprintf "Unbound var: %s\n" v))
Expand Down
2 changes: 2 additions & 0 deletions src/ir_passes/erase_typ_field.ml
Original file line number Diff line number Diff line change
Expand Up @@ -201,6 +201,8 @@ let transform prog =
TagP (i, t_pat pat1)
| AltP (pat1, pat2) ->
AltP (t_pat pat1, t_pat pat2)
| AndP (pat1, pat2) ->
AndP (t_pat pat1, t_pat pat2)

and t_typ_bind' tb =
{ tb with con = t_con tb.con; bound = t_typ tb.bound }
Expand Down
1 change: 1 addition & 0 deletions src/ir_passes/tailcall.ml
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,7 @@ and pat' env = function
| OptP p
| TagP (_, p) -> pat env p
| AltP (p1, _p2) -> pat env p1 (* both bind the same vars, ensured in check_pat *)
| AndP (p1, p2) -> pat (pat env p1) p2

and pats env ps =
match ps with
Expand Down
1 change: 1 addition & 0 deletions src/js/astjs.ml
Original file line number Diff line number Diff line change
Expand Up @@ -587,6 +587,7 @@ module Make (Cfg : Config) = struct
| OptP p -> to_js_object "OptP" [| pat_js p |]
| TagP (i, p) -> to_js_object "TagP" [| js_string ("#" ^ i.it); pat_js p |]
| AltP (p1, p2) -> to_js_object "AltP" [| pat_js p1; pat_js p2 |]
| AndP (p1, p2) -> to_js_object "AndP" [| pat_js p1; pat_js p2 |]
| ParP p -> to_js_object "ParP" [| pat_js p |]

and pat_field_js pf =
Expand Down
2 changes: 2 additions & 0 deletions src/lang_utils/error_codes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -217,6 +217,8 @@ let error_codes : (string * string option) list =
"M0257", None; (* Misplaced uninitialized dec *)
"M0258", None; (* Uninitialized `let` with non <id> : <typ> pattern *)
"M0259", None; (* Uninitialized dec requires type annotation *)
"M0260", None; (* `and`-pattern binds the same variable in both legs *)
"M0261", None; (* Cannot infer and-pattern, please use an annotation *)
]

(** Message codes that can be both used as warnings and errors *)
Expand Down
1 change: 1 addition & 0 deletions src/lowering/desugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1324,6 +1324,7 @@ and pat' = function
| S.OptP p -> I.OptP (pat p)
| S.TagP (i, p) -> I.TagP (i.it, pat p)
| S.AltP (p1, p2) -> I.AltP (pat p1, pat p2)
| S.AndP (p1, p2) -> I.AndP (pat p1, pat p2)
| S.AnnotP (p, _)
| S.ParP p -> pat' p.it

Expand Down
1 change: 1 addition & 0 deletions src/mo_def/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,7 @@ module Make (Cfg : Config) = struct
| OptP p -> "OptP" $$ [pat p]
| TagP (i, p) -> "TagP" $$ [tag i; pat p]
| AltP (p1, p2) -> "AltP" $$ [pat p1; pat p2]
| AndP (p1, p2) -> "AndP" $$ [pat p1; pat p2]
| ParP p -> "ParP" $$ [pat p]))

and lit = function
Expand Down
4 changes: 1 addition & 3 deletions src/mo_def/syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -120,11 +120,9 @@ and pat' =
| OptP of pat (* option *)
| TagP of id * pat (* tagged variant *)
| AltP of pat * pat (* disjunctive *)
| AndP of pat * pat (* conjunctive *)
| AnnotP of pat * typ (* type annotation *)
| ParP of pat (* parenthesis *)
(*
| AsP of pat * pat (* conjunctive *)
*)

and pat_field = pat_field' phrase
and pat_field' =
Expand Down
16 changes: 16 additions & 0 deletions src/mo_frontend/coverage.ml
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ type ctxt =
| InObj of ctxt * desc LabMap.t * string * pat_field list * T.field list
| InAlt1 of ctxt * region * pat * T.typ
| InAlt2 of ctxt * region
| InAnd1 of ctxt * pat * T.typ
| InCase of region * case list * T.typ

type sets =
Expand Down Expand Up @@ -268,6 +269,15 @@ let rec match_pat ctxt desc pat t sets =
| AltP (pat1, pat2) ->
sets.alts <- AtSet.add pat1.at (AtSet.add pat2.at sets.alts);
match_pat (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets
| AndP (pat1, pat2) ->
(* AndP accepts v iff both pat1 and pat2 accept v.
Match pat1 first under an InAnd1 context; on success, continue
with pat2 on the narrowed `desc` under the outer context; on
failure, the whole AndP fails for that desc-slice. Non-covering
content in pat2 (e.g. a variant tag incompatible with what pat1
already admitted) surfaces as uncovered via the normal ctxt
flow — no special casing needed. *)
match_pat (InAnd1 (ctxt, pat2, t)) desc pat1 t sets
| AnnotP (pat1, _)
| ParP pat1 ->
match_pat ctxt desc pat1 t sets
Expand Down Expand Up @@ -332,6 +342,9 @@ and succeed ctxt desc sets : bool =
| InAlt2 (ctxt', at2) ->
sets.reached_alts <- AtSet.add at2 sets.reached_alts;
succeed ctxt' desc sets
| InAnd1 (ctxt', pat2, t) ->
(* pat1 accepted `desc`; now pat2 must also accept it *)
match_pat ctxt' desc pat2 t sets
| InCase (at, cases, _t) ->
sets.reached_cases <- AtSet.add at sets.reached_cases;
skip cases sets
Expand All @@ -358,6 +371,9 @@ and fail ctxt desc sets : bool =
match_pat (InAlt2 (ctxt', pat2.at)) desc pat2 t sets
| InAlt2 (ctxt', at2) ->
fail ctxt' desc sets
| InAnd1 (ctxt', _pat2, _t) ->
(* pat1 rejected `desc`; AndP rejects too *)
fail ctxt' desc sets
| InCase (at, [], t) ->
T.span t = Some 0 || not (T.inhabited t) ||
(sets.missing <- desc::sets.missing; false)
Expand Down
Loading
Loading