diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index bfa9e3978..6202d262f 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -202,7 +202,8 @@ type exp = { co_ctx: CoCtx.t, /* Locally free variables */ cls: Cls.t, /* DERIVED: Syntax class (i.e. form name) */ status: status_exp, /* DERIVED: Ok/Error statuses for display */ - ty: Typ.t /* DERIVED: Type after nonempty hole fixing */ + ty: Typ.t, /* DERIVED: Type after nonempty hole fixing */ + lifted_ty: option(Typ.t) /* Type static-level elaboration */ }; [@deriving (show({with_path: false}), sexp, yojson)] @@ -630,11 +631,31 @@ let fixed_typ_exp = (ctx, mode: Mode.t, self: Self.exp): Typ.t => /* Add derivable attributes for expression terms */ let derived_exp = - (~uexp: UExp.t, ~ctx, ~mode, ~ancestors, ~self, ~co_ctx): exp => { + ( + ~uexp: UExp.t, + ~ctx, + ~mode, + ~ancestors, + ~self, + ~co_ctx, + ~lifted_ty: option(Typ.t), + ) + : exp => { let cls = Cls.Exp(UExp.cls_of_term(uexp.term)); let status = status_exp(ctx, mode, self); let ty = fixed_typ_exp(ctx, mode, self); - {cls, self, ty, mode, status, ctx, co_ctx, ancestors, term: uexp}; + { + cls, + self, + ty, + mode, + status, + ctx, + co_ctx, + ancestors, + lifted_ty, + term: uexp, + }; }; /* Add derivable attributes for pattern terms */ diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 3175df7bf..dc7b8b809 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -182,9 +182,17 @@ and uexp_to_info_map = | Ana({term: Unknown(SynSwitch), _}) => Mode.Syn | _ => mode }; - let add' = (~self, ~co_ctx, m) => { + let add' = (~lifted_ty=?, ~self, ~co_ctx, m) => { let info = - Info.derived_exp(~uexp, ~ctx, ~mode, ~ancestors, ~self, ~co_ctx); + Info.derived_exp( + ~uexp, + ~ctx, + ~mode, + ~ancestors, + ~self, + ~co_ctx, + ~lifted_ty, + ); (info, add_info(ids, InfoExp(info), m)); }; @@ -249,7 +257,11 @@ and uexp_to_info_map = uexp_to_info_map(~ctx, ~mode, ~ancestors, elaborated_exp, m); // We need to keep the original status of the expression to get error messages on the unelaborated expression - let info = {...info, status: original_info.status}; + let info = { + ...info, + status: original_info.status, + lifted_ty: Some(info.ty), + }; (info, add_info(elaborated_exp.ids, InfoExp(info), m)); }; diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index be3d3110e..17e36c948 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -66,7 +66,8 @@ let elements_noun: Cls.t => string = | Exp(ListConcat) => "Operands" | _ => failwith("elements_noun: Cls doesn't have elements"); -let common_err_view = (cls: Cls.t, err: Info.error_common) => +let common_err_view = + (~lifted_ty: option(Typ.t)=?, cls: Cls.t, err: Info.error_common) => switch (err) { | NoType(BadToken(token)) => switch (Form.bad_token_cls(token)) { @@ -85,19 +86,27 @@ let common_err_view = (cls: Cls.t, err: Info.error_common) => Type.view(typ), text("inconsistent with arrow type"), ] - | Inconsistent(Expectation({ana, syn})) => [ + | Inconsistent(Expectation({ana, syn})) => + [ text(":"), Type.view(syn), text("inconsistent with expected type"), Type.view(ana), ] + @ ( + switch (lifted_ty) { + | None => [] + | Some(lifted) => [text("lifted to"), Type.view(lifted)] + } + ) | Inconsistent(Internal(tys)) => [ text(elements_noun(cls) ++ " have inconsistent types:"), ...ListUtil.join(text(","), List.map(Type.view, tys)), ] }; -let common_ok_view = (cls: Cls.t, ok: Info.ok_pat) => { +let common_ok_view = + (~lifted_ty: option(Typ.t)=?, cls: Cls.t, ok: Info.ok_common) => { switch (cls, ok) { | (Exp(MultiHole) | Pat(MultiHole), _) => [ text("Expecting operator or delimiter"), @@ -122,12 +131,20 @@ let common_ok_view = (cls: Cls.t, ok: Info.ok_pat) => { Type.view(syn), text("equals expected type"), ] - | (_, Ana(Consistent({ana, syn, _}))) => [ + | (_, Ana(Consistent({ana, syn, _}))) => + // print_endline("Id: " ++) + [ text(":"), Type.view(syn), text("consistent with expected type"), Type.view(ana), ] + @ ( + switch (lifted_ty) { + | None => [] + | Some(lifted) => [text("lifted to"), Type.view(lifted)] + } + ) | (_, Ana(InternallyInconsistent({ana, nojoin: tys}))) => [ text(elements_noun(cls) ++ " have inconsistent types:"), @@ -177,7 +194,7 @@ let typ_err_view = (ok: Info.error_typ) => ] }; -let rec exp_view = (cls: Cls.t, status: Info.status_exp) => +let rec exp_view = (cls: Cls.t, status: Info.status_exp, info: Info.exp) => switch (status) { | InHole(FreeVariable(name)) => div_err([code_err(name), text("not found")]) @@ -188,7 +205,7 @@ let rec exp_view = (cls: Cls.t, status: Info.status_exp) => | Some(err) => let cls_str = String.uncapitalize_ascii(cls_str); div_err([ - exp_view(cls, InHole(Common(err))), + exp_view(cls, InHole(Common(err)), info), text("; " ++ cls_str ++ " is inexhaustive"), ]); }; @@ -208,10 +225,12 @@ let rec exp_view = (cls: Cls.t, status: Info.status_exp) => ++ " arguments", ), ]) - | InHole(Common(error)) => div_err(common_err_view(cls, error)) + | InHole(Common(error)) => + div_err(common_err_view(~lifted_ty=?info.lifted_ty, cls, error)) | NotInHole(AnaDeferralConsistent(ana)) => div_ok([text("Expecting type"), Type.view(ana)]) - | NotInHole(Common(ok)) => div_ok(common_ok_view(cls, ok)) + | NotInHole(Common(ok)) => + div_ok(common_ok_view(~lifted_ty=?info.lifted_ty, cls, ok)) }; let rec pat_view = (cls: Cls.t, status: Info.status_pat) => @@ -266,7 +285,7 @@ let view_of_info = (~inject, ~settings, ci): list(Node.t) => { ]; switch (ci) { | Secondary(_) => wrapper(div([])) - | InfoExp({cls, status, _}) => wrapper(exp_view(cls, status)) + | InfoExp({cls, status, _} as ie) => wrapper(exp_view(cls, status, ie)) | InfoPat({cls, status, _}) => wrapper(pat_view(cls, status)) | InfoTyp({cls, status, _}) => wrapper(typ_view(cls, status)) | InfoTPat({cls, status, _}) => wrapper(tpat_view(cls, status))