From 186cb1e651dfb29020b42055a5dcbf9a17d8739d Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Fri, 20 Oct 2023 14:02:55 -0400 Subject: [PATCH 1/7] 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 2/7] 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 3/7] 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 4/7] 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 5/7] 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 6/7] 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 074546396100f5ace111d456e3ee2c76440bc662 Mon Sep 17 00:00:00 2001 From: Jiezhong Yang Date: Sun, 22 Oct 2023 12:18:11 -0400 Subject: [PATCH 7/7] Init --- src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 1 + 1 file changed, 1 insertion(+) diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index 2dc53757b5..ac241cd6f0 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -93,6 +93,7 @@ let mk_bin_float_op = (op: TermBase.UExp.op_bin_float): DHDoc.t => let mk_bin_string_op = (op: TermBase.UExp.op_bin_string): DHDoc.t => Doc.text(TermBase.UExp.string_op_to_string(op)); +// DHExp is annotated here let rec mk = ( ~settings: Settings.Evaluation.t,