diff --git a/src/haz3lcore/dynamics/Constraint.re b/src/haz3lcore/dynamics/Constraint.re new file mode 100644 index 0000000000..a56f435e55 --- /dev/null +++ b/src/haz3lcore/dynamics/Constraint.re @@ -0,0 +1,153 @@ +open Sexplib.Std; + +[@deriving (show({with_path: false}), sexp, yojson)] +type t = + | Truth + | Falsity + | Hole + | Int(int) + | NotInt(int) + | Float(float) + | NotFloat(float) + | String(string) + | NotString(string) + | And(t, t) + | Or(t, t) + | InjL(t) + | InjR(t) + | Pair(t, t); + +let rec dual = (c: t): t => + switch (c) { + | Truth => Falsity + | Falsity => Truth + | Hole => Hole + | Int(n) => NotInt(n) + | NotInt(n) => Int(n) + | Float(n) => NotFloat(n) + | NotFloat(n) => Float(n) + | String(s) => NotString(s) + | NotString(s) => String(s) + | And(c1, c2) => Or(dual(c1), dual(c2)) + | Or(c1, c2) => And(dual(c1), dual(c2)) + | InjL(c1) => Or(InjL(dual(c1)), InjR(Truth)) + | InjR(c2) => Or(InjR(dual(c2)), InjL(Truth)) + | Pair(c1, c2) => + Or( + Pair(c1, dual(c2)), + Or(Pair(dual(c1), c2), Pair(dual(c1), dual(c2))), + ) + }; + +/** substitute Truth for Hole */ +let rec truify = (c: t): t => + switch (c) { + | Hole => Truth + | Truth + | Falsity + | Int(_) + | NotInt(_) + | Float(_) + | NotFloat(_) + | String(_) + | NotString(_) => c + | And(c1, c2) => And(truify(c1), truify(c2)) + | Or(c1, c2) => Or(truify(c1), truify(c2)) + | InjL(c) => InjL(truify(c)) + | InjR(c) => InjR(truify(c)) + | Pair(c1, c2) => Pair(truify(c1), truify(c2)) + }; + +/** substitute Falsity for Hole */ +let rec falsify = (c: t): t => + switch (c) { + | Hole => Falsity + | Truth + | Falsity + | Int(_) + | NotInt(_) + | Float(_) + | NotFloat(_) + | String(_) + | NotString(_) => c + | And(c1, c2) => And(falsify(c1), falsify(c2)) + | Or(c1, c2) => Or(falsify(c1), falsify(c2)) + | InjL(c) => InjL(falsify(c)) + | InjR(c) => InjR(falsify(c)) + | Pair(c1, c2) => Pair(falsify(c1), falsify(c2)) + }; + +let is_injL = + fun + | InjL(_) => true + | _ => false; + +let is_injR = + fun + | InjR(_) => true + | _ => false; + +let unwrapL = + fun + | InjL(c) => c + | _ => failwith("input can only be InjL(_)"); + +let unwrapR = + fun + | InjR(c) => c + | _ => failwith("input can only be InjR(_)"); + +let unwrap_pair = + fun + | Pair(c1, c2) => (c1, c2) + | _ => failwith("input can only be pair(_, _)"); + +let rec or_constraints = (lst: list(t)): t => + switch (lst) { + | [] => Falsity + | [xi] => xi + | [xi, ...xis] => Or(xi, or_constraints(xis)) + }; + +let rec ctr_of_nth_variant = (num_variants, nth): (t => t) => + if (num_variants == 1) { + Fun.id; + } else if (nth == 0) { + xi => InjL(xi); + } else { + xi => InjR(xi |> ctr_of_nth_variant(num_variants - 1, nth - 1)); + }; + +let of_ap = (ctx, mode, ctr: option(Constructor.t), arg: t, syn_ty): t => + switch (ctr) { + | Some(name) => + let ty = + switch (mode) { + | Mode.Ana(ty) => Some(ty) + | Syn => syn_ty + | _ => None + }; + switch (ty) { + | Some(ty) => + switch (Typ.weak_head_normalize(ctx, ty)) { + | Sum(map) => + let num_variants = ConstructorMap.cardinal(map); + switch (ConstructorMap.nth(map, name)) { + | Some(nth) => arg |> ctr_of_nth_variant(num_variants, nth) + | None => Falsity + }; + | _ => Falsity + } + | None => Falsity + }; + | None => Falsity + }; + +let of_ctr = (ctx, mode, name, self) => { + let syn_ty = + switch (self) { + | Self.IsConstructor({syn_ty, _}) => syn_ty + | _ => assert(false) // impossible + }; + of_ap(ctx, mode, Some(name), Truth, syn_ty); +}; diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index 764f40a644..b960dae875 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -376,7 +376,8 @@ let rec dhexp_of_uexp = |> OptUtil.sequence; let d = DHExp.Case(d_scrut, d_rules, 0); switch (err_status) { - | InHole(Common(Inconsistent(Internal(_)))) => + | InHole(Common(Inconsistent(Internal(_)))) + | InHole(InexhaustiveMatch(Some(Inconsistent(Internal(_))))) => DHExp.InconsistentBranches(id, 0, d) | _ => ConsistentCase(d) }; @@ -393,6 +394,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/dynamics/Incon.re b/src/haz3lcore/dynamics/Incon.re new file mode 100644 index 0000000000..6f5c6af13f --- /dev/null +++ b/src/haz3lcore/dynamics/Incon.re @@ -0,0 +1,145 @@ +open Sets; + +let is_inconsistent_int = (xis: list(Constraint.t)): bool => { + let (int_set, not_int_list) = + List.fold_left( + ((int_set, not_int_list), xi: Constraint.t) => + switch (xi) { + | Int(n) => (IntSet.add(n, int_set), not_int_list) + | NotInt(n) => (int_set, [n, ...not_int_list]) + | _ => failwith("input can only be Int | NotInt") + }, + (IntSet.empty, []), + xis, + ); + IntSet.cardinal(int_set) > 1 + || List.exists(IntSet.mem(_, int_set), not_int_list); +}; + +let is_inconsistent_float = (xis: list(Constraint.t)): bool => { + let (float_set, not_float_list) = + List.fold_left( + ((float_set, not_float_list), xi: Constraint.t) => + switch (xi) { + | Float(n) => (FloatSet.add(n, float_set), not_float_list) + | NotFloat(n) => (float_set, [n, ...not_float_list]) + | _ => failwith("input can only be Float | NotFloat") + }, + (FloatSet.empty, []), + xis, + ); + FloatSet.cardinal(float_set) > 1 + || List.exists(FloatSet.mem(_, float_set), not_float_list); +}; + +let is_inconsistent_string = (xis: list(Constraint.t)): bool => { + let (string_set, not_string_list) = + List.fold_left( + ((string_set, not_string_list), xi: Constraint.t) => + switch (xi) { + | String(s) => (StringSet.add(s, string_set), not_string_list) + | NotString(s) => (string_set, [s, ...not_string_list]) + | _ => failwith("input can only be String | NotString") + }, + (StringSet.empty, []), + xis, + ); + StringSet.cardinal(string_set) > 1 + || List.exists(StringSet.mem(_, string_set), not_string_list); +}; + +let rec is_inconsistent = (xis: list(Constraint.t)): bool => + switch (xis) { + | [] => false + | _ + when + List.exists(Constraint.is_injL, xis) + && List.exists(Constraint.is_injR, xis) => + true + | [xi, ...xis'] => + switch (xi) { + | Truth => is_inconsistent(xis') + | Falsity => true + | Hole => assert(false) // Impossible + | And(xi1, xi2) => is_inconsistent([xi1, xi2, ...xis']) + | Or(xi1, xi2) => + is_inconsistent([xi1, ...xis']) && is_inconsistent([xi2, ...xis']) + | InjL(_) => + switch (List.partition(Constraint.is_injL, xis)) { + | (injLs, []) => + injLs |> List.map(Constraint.unwrapL) |> is_inconsistent + | (injLs, others) => is_inconsistent(others @ injLs) + } + | InjR(_) => + switch (List.partition(Constraint.is_injR, xis)) { + | (injRs, []) => + injRs |> List.map(Constraint.unwrapR) |> is_inconsistent + | (injRs, others) => is_inconsistent(others @ injRs) + } + | Int(_) + | NotInt(_) => + switch ( + List.partition( + fun + | Constraint.Int(_) + | NotInt(_) => true + | _ => false, + xis, + ) + ) { + | (ns, []) => is_inconsistent_int(ns) + | (ns, others) => is_inconsistent(others @ ns) + } + | Float(_) + | NotFloat(_) => + switch ( + List.partition( + fun + | Constraint.Float(_) + | NotFloat(_) => true + | _ => false, + xis, + ) + ) { + | (fs, []) => is_inconsistent_float(fs) + | (fs, others) => is_inconsistent(others @ fs) + } + | String(_) + | NotString(_) => + switch ( + List.partition( + fun + | Constraint.String(_) + | NotString(_) => true + | _ => false, + xis, + ) + ) { + | (ss, []) => is_inconsistent_string(ss) + | (ss, others) => is_inconsistent(others @ ss) + } + | Pair(_, _) => + switch ( + List.partition( + fun + | Constraint.Pair(_) => true + | _ => false, + xis, + ) + ) { + | (pairs, []) => + let (xisL, xisR) = + pairs |> List.map(Constraint.unwrap_pair) |> List.split; + is_inconsistent(xisL) || is_inconsistent(xisR); + | (pairs, others) => is_inconsistent(others @ pairs) + } + } + }; + +let is_redundant = (xi_cur: Constraint.t, xi_pre: Constraint.t): bool => + is_inconsistent( + Constraint.[And(truify(xi_cur), dual(falsify(xi_pre)))], + ); + +let is_exhaustive = (xi: Constraint.t): bool => + is_inconsistent(Constraint.[dual(truify(xi))]); diff --git a/src/haz3lcore/dynamics/Sets.re b/src/haz3lcore/dynamics/Sets.re new file mode 100644 index 0000000000..5c2179da68 --- /dev/null +++ b/src/haz3lcore/dynamics/Sets.re @@ -0,0 +1,23 @@ +module IntSet = + Set.Make({ + type t = int; + let compare = compare; + }); + +module BoolSet = + Set.Make({ + type t = bool; + let compare = compare; + }); + +module FloatSet = + Set.Make({ + type t = float; + let compare = compare; + }); + +module StringSet = + Set.Make({ + type t = string; + let compare = compare; + }); diff --git a/src/haz3lcore/statics/ConstructorMap.re b/src/haz3lcore/statics/ConstructorMap.re index c9ff0667dc..a350d16d92 100644 --- a/src/haz3lcore/statics/ConstructorMap.re +++ b/src/haz3lcore/statics/ConstructorMap.re @@ -99,3 +99,12 @@ let rec is_ground = (is_ground_value: 'a => bool, map: t('a)): bool => | [(_, head), ...tail] => is_ground_value(head) && tail |> is_ground(is_ground_value) }; + +let nth = (map: t('a), ctr: Constructor.t): option(int) => { + // TODO: use List.find_index instead, which is available for OCaml 5.1 + let ctrs_sorted = map |> sort |> ctrs_of; + List.find_opt( + nth => List.nth(ctrs_sorted, nth) == ctr, + List.init(List.length(ctrs_sorted), Fun.id), + ); +}; diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 83f6ee86a0..11c44b1120 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -66,6 +66,7 @@ type error_common = [@deriving (show({with_path: false}), sexp, yojson)] type error_exp = | FreeVariable(Var.t) /* Unbound variable (not in typing context) */ + | InexhaustiveMatch(option(error_common)) | UnusedDeferral | BadPartialAp(Self.error_partial_ap) | Common(error_common); @@ -73,6 +74,7 @@ type error_exp = [@deriving (show({with_path: false}), sexp, yojson)] type error_pat = | ExpectedConstructor /* Only construtors can be applied */ + | Redundant(option(error_pat)) | Common(error_common); [@deriving (show({with_path: false}), sexp, yojson)] @@ -214,6 +216,7 @@ type pat = { cls: Term.Cls.t, status: status_pat, ty: Typ.t, + constraint_: Constraint.t, }; [@deriving (show({with_path: false}), sexp, yojson)] @@ -316,6 +319,7 @@ let exp_co_ctx: exp => CoCtx.t = ({co_ctx, _}) => co_ctx; let exp_ty: exp => Typ.t = ({ty, _}) => ty; let pat_ctx: pat => Ctx.t = ({ctx, _}) => ctx; let pat_ty: pat => Typ.t = ({ty, _}) => ty; +let pat_constraint: pat => Constraint.t = ({constraint_, _}) => constraint_; let rec status_common = (ctx: Ctx.t, mode: Mode.t, self: Self.t): status_common => @@ -370,8 +374,20 @@ 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) { + | (_, 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 | SynTypFun | Ana(_), Common(self_pat)) | (SynFun, Common(IsConstructor(_) as self_pat)) => /* Little bit of a hack. Anything other than a bound ctr will, in @@ -391,9 +407,24 @@ let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => depending on the mode, which represents the expectations of the surrounding syntactic context, and the self which represents the makeup of the expression / pattern itself. */ -let status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp => +let rec status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp => switch (self, mode) { | (Free(name), _) => InHole(FreeVariable(name)) + | (InexhaustiveMatch(self), _) => + let additional_err = + switch (status_exp(ctx, mode, self)) { + | InHole(Common(Inconsistent(Internal(_)) as inconsistent_err)) => + Some(inconsistent_err) + | NotInHole(_) + | InHole(Common(Inconsistent(Expectation(_) | WithArrow(_)))) => None /* Type checking should fail and these errors would be nullified */ + | InHole(Common(NoType(_))) + | InHole( + FreeVariable(_) | InexhaustiveMatch(_) | UnusedDeferral | + BadPartialAp(_), + ) => + failwith("InHole(InexhaustiveMatch(impossible_err))") + }; + InHole(InexhaustiveMatch(additional_err)); | (IsDeferral(InAp), Ana(ana)) => NotInHole(AnaDeferralConsistent(ana)) | (IsDeferral(_), _) => InHole(UnusedDeferral) | (IsBadPartialAp(_ as info), _) => InHole(BadPartialAp(info)) @@ -509,11 +540,36 @@ 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 = + ( + upat: UPat.t, + ctx, + mode: Mode.t, + self: Self.pat, + constraint_: Constraint.t, + ) + : Constraint.t => + switch (upat.term) { + | TypeAnn(_) => constraint_ + | _ => + switch (fixed_typ_pat(ctx, mode, self)) { + | Unknown(_) => Constraint.Hole + | _ => constraint_ + } + }; let fixed_typ_exp = (ctx, mode: Mode.t, self: Self.exp): Typ.t => switch (status_exp(ctx, mode, self)) { @@ -533,11 +589,24 @@ let derived_exp = /* Add derivable attributes for pattern terms */ let derived_pat = - (~upat: UPat.t, ~ctx, ~co_ctx, ~mode, ~ancestors, ~self): pat => { + (~upat: UPat.t, ~ctx, ~co_ctx, ~mode, ~ancestors, ~self, ~constraint_) + : pat => { let cls = Cls.Pat(UPat.cls_of_term(upat.term)); let status = status_pat(ctx, mode, self); let ty = fixed_typ_pat(ctx, mode, self); - {cls, self, mode, ty, status, ctx, co_ctx, ancestors, term: upat}; + let constraint_ = fixed_constraint_pat(upat, ctx, mode, self, constraint_); + { + cls, + self, + mode, + ty, + status, + ctx, + co_ctx, + ancestors, + term: upat, + constraint_, + }; }; /* Add derivable attributes for types */ diff --git a/src/haz3lcore/statics/Self.re b/src/haz3lcore/statics/Self.re index 89e8352d41..052bf581ef 100644 --- a/src/haz3lcore/statics/Self.re +++ b/src/haz3lcore/statics/Self.re @@ -49,12 +49,14 @@ type error_partial_ap = [@deriving (show({with_path: false}), sexp, yojson)] type exp = | Free(Var.t) + | InexhaustiveMatch(exp) | IsDeferral(Term.UExp.deferral_position) | IsBadPartialAp(error_partial_ap) | Common(t); [@deriving (show({with_path: false}), sexp, yojson)] type pat = + | Redundant(pat) | Common(t); let join_of = (j: join_type, ty: Typ.t): Typ.t => @@ -80,13 +82,15 @@ let typ_of_exp: (Ctx.t, exp) => option(Typ.t) = ctx => fun | Free(_) + | InexhaustiveMatch(_) | IsDeferral(_) | IsBadPartialAp(_) => 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(pat) => typ_of_pat(ctx, pat) | Common(self) => typ_of(ctx, self); /* The self of a var depends on the ctx; if the diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 637dbdf6b0..73d4f02265 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -348,11 +348,12 @@ and uexp_to_info_map = /* add co_ctx to pattern */ let (p, m) = go_pat(~is_synswitch=false, ~co_ctx=e.co_ctx, ~mode=mode_pat, p, m); - add( - ~self=Just(Arrow(p.ty, e.ty)), - ~co_ctx=CoCtx.mk(ctx, p.ctx, e.co_ctx), - m, - ); + // TODO: factor out code + let unwrapped_self: Self.exp = Common(Just(Arrow(p.ty, e.ty))); + let is_exhaustive = p |> Info.pat_constraint |> Incon.is_exhaustive; + let self = + is_exhaustive ? unwrapped_self : InexhaustiveMatch(unwrapped_self); + add'(~self, ~co_ctx=CoCtx.mk(ctx, p.ctx, e.co_ctx), m); | TypFun({term: Var(name), _} as utpat, body) when !Ctx.shadows_typ(ctx, name) => let mode_body = Mode.of_forall(ctx, Some(name), mode); @@ -425,8 +426,13 @@ and uexp_to_info_map = p, m, ); - add( - ~self=Just(body.ty), + // TODO: factor out code + let unwrapped_self: Self.exp = Common(Just(body.ty)); + let is_exhaustive = p_ana |> Info.pat_constraint |> Incon.is_exhaustive; + let self = + is_exhaustive ? unwrapped_self : InexhaustiveMatch(unwrapped_self); + add'( + ~self, ~co_ctx= CoCtx.union([def.co_ctx, CoCtx.mk(ctx, p_ana.ctx, body.co_ctx)]), m, @@ -467,19 +473,91 @@ and uexp_to_info_map = let e_tys = List.map(Info.exp_ty, es); 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), - List.combine(ps, e_co_ctxs), - m, - ); - add( - ~self=Self.match(ctx, e_tys, branch_ids), - ~co_ctx=CoCtx.union([scrut.co_ctx] @ e_co_ctxs), - m, - ); + let unwrapped_self: Self.exp = + Common(Self.match(ctx, e_tys, branch_ids)); + let constraint_ty = + switch (scrut.ty) { + | Unknown(_) => + map_m(go_pat(~is_synswitch=false, ~co_ctx=CoCtx.empty), ps, m) + |> fst + |> List.map(Info.pat_ty) + |> Typ.join_all(~empty=Unknown(Internal), ctx) + | ty => Some(ty) + }; + let (self, m) = + switch (constraint_ty) { + | Some(constraint_ty) => + let pats_to_info_map = (ps: list(UPat.t), m) => { + /* Add co-ctxs to patterns */ + List.fold_left( + ((m, acc_constraint), (p, co_ctx)) => { + let p_constraint = + go_pat( + ~is_synswitch=false, + ~co_ctx, + ~mode=Mode.Ana(constraint_ty), + p, + m, + ) + |> fst + |> Info.pat_constraint; + let (p, m) = + go_pat( + ~is_synswitch=false, + ~co_ctx, + ~mode=Mode.Ana(scrut.ty), + p, + m, + ); + let is_redundant = + Incon.is_redundant(p_constraint, acc_constraint); + let self = is_redundant ? Self.Redundant(p.self) : p.self; + let info = + Info.derived_pat( + ~upat=p.term, + ~ctx=p.ctx, + ~co_ctx=p.co_ctx, + ~mode=p.mode, + ~ancestors=p.ancestors, + ~self, + // Mark patterns as redundant at the top level + // because redundancy doesn't make sense in a smaller context + ~constraint_=p_constraint, + ); + ( + // Override the info for the single upat + add_info(p.term.ids, InfoPat(info), m), + is_redundant + ? acc_constraint // Redundant patterns are ignored + : Constraint.Or(p_constraint, acc_constraint), + ); + }, + (m, Constraint.Falsity), + List.combine(ps, e_co_ctxs), + ); + }; + let (m, final_constraint) = pats_to_info_map(ps, m); + let is_exhaustive = Incon.is_exhaustive(final_constraint); + let self = + is_exhaustive ? unwrapped_self : InexhaustiveMatch(unwrapped_self); + (self, m); + | None => + /* 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, + ), + List.combine(ps, e_co_ctxs), + m, + ); + (unwrapped_self, m); + }; + add'(~self, ~co_ctx=CoCtx.union([scrut.co_ctx] @ e_co_ctxs), m); | TyAlias(typat, utyp, body) => let m = utpat_to_info_map(~ctx, ~ancestors, typat, m) |> snd; switch (typat.term) { @@ -553,7 +631,7 @@ and upat_to_info_map = m: Map.t, ) : (Info.pat, Map.t) => { - let add = (~self, ~ctx, m) => { + let add = (~self, ~ctx, ~constraint_, m) => { let info = Info.derived_pat( ~upat, @@ -562,42 +640,74 @@ and upat_to_info_map = ~mode, ~ancestors, ~self=Common(self), + ~constraint_, ); (info, add_info(ids, InfoPat(info), m)); }; - let atomic = self => add(~self, ~ctx, m); + let atomic = (self, constraint_) => add(~self, ~ctx, ~constraint_, m); let ancestors = [UPat.rep_id(upat)] @ ancestors; let go = upat_to_info_map(~is_synswitch, ~ancestors, ~co_ctx); let unknown = Typ.Unknown(is_synswitch ? SynSwitch : Internal); let ctx_fold = (ctx: Ctx.t, m) => List.fold_left2( - ((ctx, tys, m), e, mode) => + ((ctx, tys, cons, m), e, mode) => go(~ctx, ~mode, e, m) - |> (((info, m)) => (info.ctx, tys @ [info.ty], m)), - (ctx, [], m), + |> ( + ((info, m)) => ( + info.ctx, + tys @ [info.ty], + cons @ [info.constraint_], + m, + ) + ), + (ctx, [], [], m), ); + let hole = self => atomic(self, Constraint.Hole); switch (term) { | MultiHole(tms) => let (_, m) = multi(~ctx, ~ancestors, m, tms); - add(~self=IsMulti, ~ctx, m); - | Invalid(token) => atomic(BadToken(token)) - | EmptyHole => atomic(Just(unknown)) - | Int(_) => atomic(Just(Int)) - | Float(_) => atomic(Just(Float)) - | Triv => atomic(Just(Prod([]))) - | Bool(_) => atomic(Just(Bool)) - | String(_) => atomic(Just(String)) + add(~self=IsMulti, ~ctx, ~constraint_=Constraint.Hole, m); + | Invalid(token) => hole(BadToken(token)) + | EmptyHole => hole(Just(unknown)) + | Int(int) => atomic(Just(Int), Constraint.Int(int)) + | Float(float) => atomic(Just(Float), Constraint.Float(float)) + | Triv => atomic(Just(Prod([])), Constraint.Truth) + | Bool(bool) => + atomic( + Just(Bool), + bool + ? Constraint.InjL(Constraint.Truth) + : Constraint.InjR(Constraint.Truth), + ) + | String(string) => atomic(Just(String), Constraint.String(string)) | ListLit(ps) => let ids = List.map(UPat.rep_id, ps); let modes = Mode.of_list_lit(ctx, List.length(ps), mode); - let (ctx, tys, m) = ctx_fold(ctx, m, ps, modes); - add(~self=Self.listlit(~empty=unknown, ctx, tys, ids), ~ctx, m); + let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes); + let rec cons_fold_list = cs => + switch (cs) { + | [] => Constraint.InjL(Constraint.Truth) // Left = nil, Right = cons + | [hd, ...tl] => + Constraint.InjR(Constraint.Pair(hd, cons_fold_list(tl))) + }; + add( + ~self=Self.listlit(~empty=unknown, ctx, tys, ids), + ~ctx, + ~constraint_=cons_fold_list(cons), + m, + ); | Cons(hd, tl) => let (hd, m) = go(~ctx, ~mode=Mode.of_cons_hd(ctx, mode), hd, m); let (tl, m) = go(~ctx=hd.ctx, ~mode=Mode.of_cons_tl(ctx, mode, hd.ty), tl, m); - add(~self=Just(List(hd.ty)), ~ctx=tl.ctx, m); - | Wild => atomic(Just(unknown)) + add( + ~self=Just(List(hd.ty)), + ~ctx=tl.ctx, + ~constraint_= + Constraint.InjR(Constraint.Pair(hd.constraint_, tl.constraint_)), + m, + ); + | Wild => atomic(Just(unknown), Constraint.Truth) | Var(name) => /* NOTE: The self type assigned to pattern variables (Unknown) may be SynSwitch, but SynSwitch is never added to the context; @@ -605,25 +715,50 @@ and upat_to_info_map = let ctx_typ = Info.fixed_typ_pat(ctx, mode, Common(Just(Unknown(Internal)))); let entry = Ctx.VarEntry({name, id: UPat.rep_id(upat), typ: ctx_typ}); - add(~self=Just(unknown), ~ctx=Ctx.extend(ctx, entry), m); + add( + ~self=Just(unknown), + ~ctx=Ctx.extend(ctx, entry), + ~constraint_=Constraint.Truth, + m, + ); | Tuple(ps) => let modes = Mode.of_prod(ctx, mode, List.length(ps)); - let (ctx, tys, m) = ctx_fold(ctx, m, ps, modes); - add(~self=Just(Prod(tys)), ~ctx, m); + let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes); + let rec cons_fold_tuple = cs => + switch (cs) { + | [] => Constraint.Truth + | [elt] => elt + | [hd, ...tl] => Constraint.Pair(hd, cons_fold_tuple(tl)) + }; + add( + ~self=Just(Prod(tys)), + ~ctx, + ~constraint_=cons_fold_tuple(cons), + m, + ); | Parens(p) => let (p, m) = go(~ctx, ~mode, p, m); - add(~self=Just(p.ty), ~ctx=p.ctx, m); - | Constructor(ctr) => atomic(Self.of_ctr(ctx, ctr)) + add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m); + | Constructor(ctr) => + let self = Self.of_ctr(ctx, ctr); + atomic(self, Constraint.of_ctr(ctx, mode, ctr, self)); | Ap(fn, arg) => - let fn_mode = Mode.of_ap(ctx, mode, UPat.ctr_name(fn)); + let ctr = UPat.ctr_name(fn); + let fn_mode = Mode.of_ap(ctx, mode, ctr); let (fn, m) = go(~ctx, ~mode=fn_mode, fn, m); let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty); let (arg, m) = go(~ctx, ~mode=Ana(ty_in), arg, m); - add(~self=Just(ty_out), ~ctx=arg.ctx, m); + add( + ~self=Just(ty_out), + ~ctx=arg.ctx, + ~constraint_= + Constraint.of_ap(ctx, mode, ctr, arg.constraint_, Some(ty_out)), + m, + ); | TypeAnn(p, ann) => let (ann, m) = utyp_to_info_map(~ctx, ~ancestors, ann, m); let (p, m) = go(~ctx, ~mode=Ana(ann.ty), p, m); - add(~self=Just(ann.ty), ~ctx=p.ctx, m); + add(~self=Just(ann.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m); }; } and utyp_to_info_map = diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 4bc9a68d35..99ed8fd0fb 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -173,10 +173,21 @@ let typ_err_view = (ok: Info.error_typ) => ] }; -let exp_view = (cls: Term.Cls.t, status: Info.status_exp) => +let rec exp_view = (cls: Term.Cls.t, status: Info.status_exp) => switch (status) { | InHole(FreeVariable(name)) => div_err([code_err(name), text("not found")]) + | InHole(InexhaustiveMatch(additional_err)) => + let cls_str = Term.Cls.show(cls); + switch (additional_err) { + | None => div_err([text(cls_str ++ " is inexhaustive")]) + | Some(err) => + let cls_str = String.uncapitalize_ascii(cls_str); + div_err([ + exp_view(cls, InHole(Common(err))), + text("; " ++ cls_str ++ " is inexhaustive"), + ]); + }; | InHole(UnusedDeferral) => div_err([text("Deferral must appear as a function argument")]) | InHole(BadPartialAp(NoDeferredArgs)) => @@ -199,9 +210,15 @@ let exp_view = (cls: Term.Cls.t, status: Info.status_exp) => | NotInHole(Common(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 redundant")]) + | Some(err) => + 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)) };