From 186cb1e651dfb29020b42055a5dcbf9a17d8739d Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Fri, 20 Oct 2023 14:02:55 -0400 Subject: [PATCH 01/12] Init --- src/haz3lcore/statics/Info.re | 1 + 1 file changed, 1 insertion(+) diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index a68171bc52..869a7f7a22 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -70,6 +70,7 @@ type error_exp = [@deriving (show({with_path: false}), sexp, yojson)] type error_pat = | ExpectedConstructor /* Only construtors can be applied */ + // TODO | Common(error_common); [@deriving (show({with_path: false}), sexp, yojson)] From 33c484eeea9369191910fb56c8f5ca831d9eef59 Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Fri, 20 Oct 2023 20:19:53 -0400 Subject: [PATCH 02/12] Added error_pat.Redundant --- src/haz3lcore/statics/Info.re | 5 +++-- src/haz3lweb/view/CursorInspector.re | 11 ++++++++++- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 869a7f7a22..6708f39ffb 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -70,7 +70,7 @@ type error_exp = [@deriving (show({with_path: false}), sexp, yojson)] type error_pat = | ExpectedConstructor /* Only construtors can be applied */ - // TODO + | Redundant(option(error_pat)) | Common(error_common); [@deriving (show({with_path: false}), sexp, yojson)] @@ -301,8 +301,9 @@ let rec status_common = InHole(Inconsistent(Internal(Typ.of_source(tys)))) }; -let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => +let rec status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => switch (mode, self) { + // TODO: | | (Syn | Ana(_), Common(self_pat)) | (SynFun, Common(IsConstructor(_) as self_pat)) => /* Little bit of a hack. Anything other than a bound ctr will, in diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 6cc2adf8f6..86db8d7aa9 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -174,9 +174,18 @@ let rec exp_view = (cls: Term.Cls.t, status: Info.status_exp) => | NotInHole(ok) => div_ok(common_ok_view(cls, ok)) }; -let pat_view = (cls: Term.Cls.t, status: Info.status_pat) => +let rec pat_view = (cls: Term.Cls.t, status: Info.status_pat) => switch (status) { | InHole(ExpectedConstructor) => div_err([text("Expected a constructor")]) + | InHole(Redundant(additional_err)) => + switch (additional_err) { + | None => div_err([text("Pattern is necessarily redundant")]) + | Some(err) => + div_err([ + pat_view(cls, InHole(err)), + text("; pattern is necessarily redundant"), + ]) + } | InHole(Common(error)) => div_err(common_err_view(cls, error)) | NotInHole(ok) => div_ok(common_ok_view(cls, ok)) }; From 7276a41aa5e0b5811793f35090e06075b75cc7c2 Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Fri, 20 Oct 2023 20:52:44 -0400 Subject: [PATCH 03/12] Added Self.pat --- src/haz3lcore/statics/Info.re | 13 ++++++++++++- src/haz3lcore/statics/Self.re | 2 ++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 6708f39ffb..8674eec840 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -303,7 +303,18 @@ let rec status_common = let rec status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => switch (mode, self) { - // TODO: | + | (_, Redundant(self)) => + let additional_err = + switch (status_pat(ctx, mode, self)) { + | InHole(Common(Inconsistent(Internal(_) | Expectation(_))) as err) + | InHole(Common(NoType(_)) as err) => Some(err) + | NotInHole(_) => None + | InHole(Common(Inconsistent(WithArrow(_)))) + | InHole(ExpectedConstructor | Redundant(_)) => + // ExpectedConstructor cannot be a reason to hole-wrap the entire pattern + failwith("InHole(Redundant(impossible_err))") + }; + InHole(Redundant(additional_err)); | (Syn | Ana(_), Common(self_pat)) | (SynFun, Common(IsConstructor(_) as self_pat)) => /* Little bit of a hack. Anything other than a bound ctr will, in diff --git a/src/haz3lcore/statics/Self.re b/src/haz3lcore/statics/Self.re index 684b19b01b..9f4f7d48ed 100644 --- a/src/haz3lcore/statics/Self.re +++ b/src/haz3lcore/statics/Self.re @@ -40,6 +40,7 @@ type exp = [@deriving (show({with_path: false}), sexp, yojson)] type pat = + | Redundant(pat) | Common(t); /* What the type would be if the position had been @@ -64,6 +65,7 @@ let typ_of_exp: (Ctx.t, exp) => option(Typ.t) = let typ_of_pat: (Ctx.t, pat) => option(Typ.t) = ctx => fun + | Redundant(_) => None | Common(self) => typ_of(ctx, self); /* The self of a var depends on the ctx; if the From b3d8cce65376c4046e1ec6a1c7257f6b73f11af3 Mon Sep 17 00:00:00 2001 From: Karan Anand Date: Sat, 21 Oct 2023 14:31:06 -0400 Subject: [PATCH 04/12] Generating pattern constraints sequentially --- src/haz3lcore/statics/Statics.re | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 547e8a8913..ed8438a730 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -44,6 +44,21 @@ let map_m = (f, xs, m: Map.t) => xs, ); +let map_m_constraint = (f, xs, m: Map.t) => + List.fold_left( + ((xs, m, acc_cons), x) => + f(x, m) + |> ( + ((x, m)) => ( + xs @ [x], + m, + Constraint.or_constraints([acc_cons, Info.pat_constraint(x)]), + ) + ), + ([], m, Constraint.Falsity), + xs, + ); + let add_info = (ids: list(Id.t), info: Info.t, m: Map.t): Map.t => ids |> List.fold_left((m, id) => Id.Map.add(id, info, m), m); @@ -273,8 +288,14 @@ and uexp_to_info_map = let rules_to_info_map = (rules: list((UPat.t, UExp.t)), m) => { let (ps, es) = List.split(rules); let branch_ids = List.map(UExp.rep_id, es); - let (ps, m) = - map_m(go_pat(~is_synswitch=false, ~mode=Mode.Ana(scrut.ty)), ps, m); + [@warning "-27"] + //final_cons is the final constraint generated during the mapping process + let (ps, m, final_cons) = + map_m_constraint( + go_pat(~is_synswitch=false, ~mode=Mode.Ana(scrut.ty)), + ps, + m, + ); let p_constraints = List.map(Info.pat_constraint, ps); let p_ctxs = List.map(Info.pat_ctx, ps); let (es, m) = From 0d5f5b55774b2ba692aa794ff12f0a268a9eb801 Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Sun, 22 Oct 2023 02:34:14 -0400 Subject: [PATCH 05/12] Inlined map_m_constraint Co-Authored-By: Karan Anand <58492510+karananand01@users.noreply.github.com> --- src/haz3lcore/statics/Statics.re | 29 +++++++++++------------------ 1 file changed, 11 insertions(+), 18 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index ed8438a730..cc917e42e5 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -44,21 +44,6 @@ let map_m = (f, xs, m: Map.t) => xs, ); -let map_m_constraint = (f, xs, m: Map.t) => - List.fold_left( - ((xs, m, acc_cons), x) => - f(x, m) - |> ( - ((x, m)) => ( - xs @ [x], - m, - Constraint.or_constraints([acc_cons, Info.pat_constraint(x)]), - ) - ), - ([], m, Constraint.Falsity), - xs, - ); - let add_info = (ids: list(Id.t), info: Info.t, m: Map.t): Map.t => ids |> List.fold_left((m, id) => Id.Map.add(id, info, m), m); @@ -291,10 +276,18 @@ and uexp_to_info_map = [@warning "-27"] //final_cons is the final constraint generated during the mapping process let (ps, m, final_cons) = - map_m_constraint( - go_pat(~is_synswitch=false, ~mode=Mode.Ana(scrut.ty)), + List.fold_left( + ((xs, m, acc_cons), x) => + go_pat(~is_synswitch=false, ~mode=Mode.Ana(scrut.ty), x, m) + |> ( + ((x, m)) => ( + xs @ [x], + m, + Constraint.Or(acc_cons, Info.pat_constraint(x)), + ) + ), + ([], m, Constraint.Falsity), ps, - m, ); let p_constraints = List.map(Info.pat_constraint, ps); let p_ctxs = List.map(Info.pat_ctx, ps); From 5361ce690aeb044eddee6fbe3f65c0731921e6a0 Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Sun, 22 Oct 2023 03:59:29 -0400 Subject: [PATCH 06/12] Adjusted info for redundant patterns --- src/haz3lcore/statics/Info.re | 3 ++- src/haz3lcore/statics/Statics.re | 42 +++++++++++++++++++++----------- 2 files changed, 30 insertions(+), 15 deletions(-) diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 8674eec840..cf692f8f71 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -460,8 +460,9 @@ let fixed_constraint_pat = (ctx, mode: Mode.t, self: Self.pat, constraint_: Constraint.t) : Constraint.t => switch (status_pat(ctx, mode, self)) { - | InHole(_) => Constraint.Hole + | InHole(Redundant(None)) | NotInHole(_) => constraint_ + | InHole(_) => Constraint.Hole }; let fixed_typ_exp = (ctx, mode: Mode.t, self: Self.exp): Typ.t => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index cc917e42e5..840f2a5292 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -273,23 +273,37 @@ and uexp_to_info_map = let rules_to_info_map = (rules: list((UPat.t, UExp.t)), m) => { let (ps, es) = List.split(rules); let branch_ids = List.map(UExp.rep_id, es); - [@warning "-27"] - //final_cons is the final constraint generated during the mapping process - let (ps, m, final_cons) = + let (ps, m, final_constraint) = List.fold_left( - ((xs, m, acc_cons), x) => - go_pat(~is_synswitch=false, ~mode=Mode.Ana(scrut.ty), x, m) - |> ( - ((x, m)) => ( - xs @ [x], - m, - Constraint.Or(acc_cons, Info.pat_constraint(x)), - ) - ), + ((ps, m, acc_constraint), p) => { + let (p, m) = + go_pat(~is_synswitch=false, ~mode=Mode.Ana(scrut.ty), p, m); + let p_constraint = Info.pat_constraint(p); + if (!Incon.is_redundant(p_constraint, acc_constraint)) { + (ps @ [p], m, Constraint.Or(p_constraint, acc_constraint)); + } else { + let info = + Info.derived_pat( + ~upat=p.term, + ~ctx=p.ctx, + ~mode=p.mode, + ~ancestors=p.ancestors, + ~self=Redundant(p.self), + // Mark patterns as redundant at the top level + // because redundancy doesn't make sense in a smaller context + ~constraint_=p_constraint, + ); + ( + ps @ [info], + // Override the info for the single upat + add_info(p.term.ids, InfoPat(info), m), + acc_constraint // Redundant patterns are ignored + ); + }; + }, ([], m, Constraint.Falsity), ps, ); - let p_constraints = List.map(Info.pat_constraint, ps); let p_ctxs = List.map(Info.pat_ctx, ps); let (es, m) = List.fold_left2( @@ -303,7 +317,7 @@ and uexp_to_info_map = es, List.map2(CoCtx.mk(ctx), p_ctxs, List.map(Info.exp_co_ctx, es)), branch_ids, - Constraint.or_constraints(p_constraints), + final_constraint, m, ); }; From 3c4e58db465c8038b9385a9ded0d37b90957044f Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Mon, 23 Oct 2023 00:11:02 -0400 Subject: [PATCH 07/12] Made redundancy not a runtime error --- src/haz3lcore/dynamics/Elaborator.re | 7 +++++++ src/haz3lcore/statics/Info.re | 9 ++++++++- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index 126dee2e21..28d271688a 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -284,6 +284,13 @@ let rec dhexp_of_uexp = and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => { switch (Id.Map.find_opt(Term.UPat.rep_id(upat), m)) { | Some(InfoPat({mode, self, ctx, _})) => + // NOTE: for the current implementation, redundancy is considered a static error + // but not a runtime error. + let self = + switch (self) { + | Redundant(self) => self + | _ => self + }; let err_status = Info.status_pat(ctx, mode, self); let maybe_reason: option(ErrStatus.HoleReason.t) = switch (err_status) { diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index cf692f8f71..69bbb1c6db 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -450,11 +450,18 @@ let fixed_typ_ok: ok_pat => Typ.t = | Ana(Consistent({join, _})) => join | Ana(InternallyInconsistent({ana, _})) => ana; -let fixed_typ_pat = (ctx, mode: Mode.t, self: Self.pat): Typ.t => +let fixed_typ_pat = (ctx, mode: Mode.t, self: Self.pat): Typ.t => { + // TODO: get rid of unwrapping (probably by changing the implementation of error_exp.Redundant) + let self = + switch (self) { + | Redundant(self) => self + | _ => self + }; switch (status_pat(ctx, mode, self)) { | InHole(_) => Unknown(Internal) | NotInHole(ok) => fixed_typ_ok(ok) }; +}; let fixed_constraint_pat = (ctx, mode: Mode.t, self: Self.pat, constraint_: Constraint.t) From cd03276cb320285b358f2e6fbbb2a6457708f3c4 Mon Sep 17 00:00:00 2001 From: Jiezhong Yang <108375845+pigumar1@users.noreply.github.com> Date: Mon, 23 Oct 2023 12:58:26 -0400 Subject: [PATCH 08/12] Allowed redundant patterns to have types in Self.typ_of_pat --- src/haz3lcore/statics/Self.re | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/haz3lcore/statics/Self.re b/src/haz3lcore/statics/Self.re index 9f4f7d48ed..3b4e1b7cc8 100644 --- a/src/haz3lcore/statics/Self.re +++ b/src/haz3lcore/statics/Self.re @@ -62,10 +62,10 @@ let typ_of_exp: (Ctx.t, exp) => option(Typ.t) = | InexhaustiveMatch(_) => None | Common(self) => typ_of(ctx, self); -let typ_of_pat: (Ctx.t, pat) => option(Typ.t) = +let rec typ_of_pat: (Ctx.t, pat) => option(Typ.t) = ctx => fun - | Redundant(_) => None + | Redundant(pat) => typ_of_pat(ctx, pat) | Common(self) => typ_of(ctx, self); /* The self of a var depends on the ctx; if the From df04be9cdde305c4a498d1cbfcd9b68f884b7e6b Mon Sep 17 00:00:00 2001 From: Jiezhong Yang <108375845+pigumar1@users.noreply.github.com> Date: Thu, 26 Oct 2023 12:25:38 -0400 Subject: [PATCH 09/12] =?UTF-8?q?=20Removed=20=E2=80=9Cnecessarily?= =?UTF-8?q?=E2=80=9D=20in=20the=20user-facing=20message?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/haz3lweb/view/CursorInspector.re | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 78fd8b9922..b586e6dfe2 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -179,11 +179,11 @@ let rec pat_view = (cls: Term.Cls.t, status: Info.status_pat) => | InHole(ExpectedConstructor) => div_err([text("Expected a constructor")]) | InHole(Redundant(additional_err)) => switch (additional_err) { - | None => div_err([text("Pattern is necessarily redundant")]) + | None => div_err([text("Pattern is redundant")]) | Some(err) => div_err([ pat_view(cls, InHole(err)), - text("; pattern is necessarily redundant"), + text("; pattern is redundant"), ]) } | InHole(Common(error)) => div_err(common_err_view(cls, error)) From ed3138ebdb66a5ae61042f5b9eb680fbcd5e071b Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Thu, 26 Oct 2023 12:31:31 -0400 Subject: [PATCH 10/12] Reformatted --- src/haz3lweb/view/CursorInspector.re | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index b586e6dfe2..027b0320c4 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -181,10 +181,7 @@ let rec pat_view = (cls: Term.Cls.t, status: Info.status_pat) => switch (additional_err) { | None => div_err([text("Pattern is redundant")]) | Some(err) => - div_err([ - pat_view(cls, InHole(err)), - text("; pattern is redundant"), - ]) + div_err([pat_view(cls, InHole(err)), text("; pattern is redundant")]) } | InHole(Common(error)) => div_err(common_err_view(cls, error)) | NotInHole(ok) => div_ok(common_ok_view(cls, ok)) From c81ee313fc8190086aa6058124e26eb5666b8247 Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Mon, 25 Dec 2023 09:20:34 -0500 Subject: [PATCH 11/12] Update Statics.re --- src/haz3lcore/statics/Statics.re | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 0febe2ceaf..3a92c49722 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -308,7 +308,13 @@ and uexp_to_info_map = List.fold_left( ((ps', m, acc_constraint), p) => { let (p, m) = - go_pat(~is_synswitch=false, ~co_ctx=CoCtx.empty, ~mode=Mode.Ana(scrut.ty), p, m); + go_pat( + ~is_synswitch=false, + ~co_ctx=CoCtx.empty, + ~mode=Mode.Ana(scrut.ty), + p, + m, + ); let p_constraint = Info.pat_constraint(p); if (!Incon.is_redundant(p_constraint, acc_constraint)) { (ps' @ [p], m, Constraint.Or(p_constraint, acc_constraint)); @@ -317,6 +323,7 @@ and uexp_to_info_map = Info.derived_pat( ~upat=p.term, ~ctx=p.ctx, + ~co_ctx=p.co_ctx, ~mode=p.mode, ~ancestors=p.ancestors, ~self=Redundant(p.self), @@ -359,13 +366,7 @@ and uexp_to_info_map = List.combine(ps, e_co_ctxs), m, ); - ( - es, - e_co_ctxs, - branch_ids, - final_constraint, - m, - ); + (es, e_co_ctxs, branch_ids, final_constraint, m); }; let (es, e_co_ctxs, branch_ids, final_constraint, m) = rules_to_info_map(rules, m); From 42266ceb1e4d6959fafbb5da72d160cc6294dc3b Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Thu, 18 Jan 2024 18:22:17 -0500 Subject: [PATCH 12/12] Fixed overwritten-map bug --- src/haz3lcore/statics/Statics.re | 57 +++++++++++++++----------------- 1 file changed, 27 insertions(+), 30 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 3a92c49722..d9be5dc2ff 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -304,20 +304,42 @@ and uexp_to_info_map = let rules_to_info_map = (rules: list((UPat.t, UExp.t)), m) => { let (ps, es) = List.split(rules); let branch_ids = List.map(UExp.rep_id, es); - let (ps', m, final_constraint) = + let (ps', m) = + map_m( + go_pat( + ~is_synswitch=false, + ~co_ctx=CoCtx.empty, + ~mode=Mode.Ana(scrut.ty), + ), + ps, + m, + ); + let p_ctxs = List.map(Info.pat_ctx, ps'); + let (es, m) = + List.fold_left2( + ((es, m), e, ctx) => + go'(~ctx, ~mode, e, m) |> (((e, m)) => (es @ [e], m)), + ([], m), + es, + p_ctxs, + ); + let e_co_ctxs = + List.map2(CoCtx.mk(ctx), p_ctxs, List.map(Info.exp_co_ctx, es)); + /* Add co-ctxs to patterns */ + let (m, final_constraint) = List.fold_left( - ((ps', m, acc_constraint), p) => { + ((m, acc_constraint), (p, co_ctx)) => { let (p, m) = go_pat( ~is_synswitch=false, - ~co_ctx=CoCtx.empty, + ~co_ctx, ~mode=Mode.Ana(scrut.ty), p, m, ); let p_constraint = Info.pat_constraint(p); if (!Incon.is_redundant(p_constraint, acc_constraint)) { - (ps' @ [p], m, Constraint.Or(p_constraint, acc_constraint)); + (m, Constraint.Or(p_constraint, acc_constraint)); } else { let info = Info.derived_pat( @@ -332,39 +354,14 @@ and uexp_to_info_map = ~constraint_=p_constraint, ); ( - ps' @ [info], // Override the info for the single upat add_info(p.term.ids, InfoPat(info), m), acc_constraint // Redundant patterns are ignored ); }; }, - ([], m, Constraint.Falsity), - ps, - ); - let p_ctxs = List.map(Info.pat_ctx, ps'); - let (es, m) = - List.fold_left2( - ((es, m), e, ctx) => - go'(~ctx, ~mode, e, m) |> (((e, m)) => (es @ [e], m)), - ([], m), - es, - p_ctxs, - ); - let e_co_ctxs = - List.map2(CoCtx.mk(ctx), p_ctxs, List.map(Info.exp_co_ctx, es)); - /* Add co-ctxs to patterns */ - let (_, m) = - map_m( - ((p, co_ctx)) => - go_pat( - ~is_synswitch=false, - ~co_ctx, - ~mode=Mode.Ana(scrut.ty), - p, - ), + (m, Constraint.Falsity), List.combine(ps, e_co_ctxs), - m, ); (es, e_co_ctxs, branch_ids, final_constraint, m); };