From 552938392fc780fe6df5c707a1e937887b7d20ef Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 18 Nov 2024 10:28:06 -0500 Subject: [PATCH] Progress on improving cursor inspector for automatic labelling --- src/haz3lcore/statics/Statics.re | 7 ++- src/haz3lweb/view/CursorInspector.re | 84 +++++++++++++++++++++------- 2 files changed, 71 insertions(+), 20 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index e95840f38..0bb12f77b 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -184,7 +184,8 @@ and uexp_to_info_map = | Ana({term: Unknown(SynSwitch), _}) => Mode.Syn | _ => mode }; - let add' = (~lifted_ty=?, ~self, ~co_ctx, m) => { + let add' = + (~lifted_ty=?, ~unelaborated_info=?, ~sugar_info=?, ~self, ~co_ctx, m) => { let info = Info.derived_exp( ~uexp, @@ -194,6 +195,8 @@ and uexp_to_info_map = ~self, ~co_ctx, ~lifted_ty, + ~unelaborated_info, + ~sugar_info, ); (info, add_info(ids, InfoExp(info), m)); @@ -272,6 +275,8 @@ and uexp_to_info_map = ...info, status: original_info.status, lifted_ty: Some(info.ty), + unelaborated_info: Some(original_info), + sugar_info: Some(AutoLabel(l)), }; (info, add_info(elaborated_exp.ids, InfoExp(info), m)); diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 6e05fcd76..9c6898ae4 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -9,7 +9,7 @@ let okc = "ok"; let div_err = div(~attrs=[clss(["status", errc])]); let div_ok = div(~attrs=[clss(["status", okc])]); -let code_err = (code: string): Node.t => +let code = (code: string): Node.t => div(~attrs=[clss(["code"])], [text(code)]); let explain_this_toggle = (~inject, ~show_explain_this: bool): Node.t => { @@ -67,7 +67,12 @@ let elements_noun: Cls.t => string = | _ => failwith("elements_noun: Cls doesn't have elements"); let common_err_view = - (~lifted_ty: option(Typ.t)=?, cls: Cls.t, err: Info.error_common) => + ( + ~lifted_ty as _: option(Typ.t)=?, + ~sugar_info: option(Info.sugar)=?, + cls: Cls.t, + err: Info.error_common, + ) => switch (err) { | NoType(BadToken(token)) => switch (Form.bad_token_cls(token)) { @@ -80,7 +85,7 @@ let common_err_view = text("inconsistent with"), Type.view(Prod([]) |> Typ.fresh), ] - | NoType(FreeConstructor(name)) => [code_err(name), text("not found")] + | NoType(FreeConstructor(name)) => [code(name), text("not found")] | DuplicateLabels(_) => [text("Duplicate labels within a tuple")] | Duplicate(_) => [text("Duplicated Label")] | Inconsistent(WithArrow(typ)) => [ @@ -96,9 +101,12 @@ let common_err_view = Type.view(ana), ] @ ( - switch (lifted_ty) { + switch (sugar_info) { | None => [] - | Some(lifted) => [text("lifted to"), Type.view(lifted)] + | Some(AutoLabel(label)) => [ + text(" automatically added label "), + code(label), + ] // TODO Figure out styling as well as how to handle nested labels } ) | Inconsistent(Internal(tys)) => [ @@ -108,7 +116,12 @@ let common_err_view = }; let common_ok_view = - (~lifted_ty: option(Typ.t)=?, cls: Cls.t, ok: Info.ok_common) => { + ( + ~lifted_ty: option(Typ.t)=?, + ~sugar_info: option(Info.sugar)=?, + cls: Cls.t, + ok: Info.ok_common, + ) => { switch (cls, ok) { | (Exp(MultiHole) | Pat(MultiHole), _) => [ text("Expecting operator or delimiter"), @@ -128,11 +141,24 @@ let common_ok_view = text(":"), Type.view(ana), ] - | (_, Ana(Consistent({ana, syn, _}))) when ana == syn => [ - text(":"), - Type.view(syn), - text("equals expected type"), - ] + | (_, Ana(Consistent({ana, syn, _}))) when ana == syn => + [text(":"), Type.view(syn), text("equals expected type")] + @ ( + switch (lifted_ty) { + | None => [] + | Some(lifted) => [text(" lifted to"), Type.view(lifted)] + } + ) + @ ( + switch (sugar_info) { + | None => [] + | Some(AutoLabel(label)) => [ + text(" automatically added label "), + code(label), + ] // TODO Figure out styling as well as how to handle nested labels + } + ) + | (_, Ana(Consistent({ana, syn, _}))) => // print_endline("Id: " ++) [ @@ -147,6 +173,15 @@ let common_ok_view = | Some(lifted) => [text("lifted to"), Type.view(lifted)] } ) + @ ( + switch (sugar_info) { + | None => [] + | Some(AutoLabel(label)) => [ + text(" automatically added label "), + code(label), + ] // TODO Figure out styling as well as how to handle nested labels + } + ) | (_, Ana(InternallyInconsistent({ana, nojoin: tys}))) => [ text(elements_noun(cls) ++ " have inconsistent types:"), @@ -182,10 +217,7 @@ let typ_err_view = (ok: Info.error_typ) => Type.view(Var(name) |> Typ.fresh), text("not found"), ] - | BadToken(token) => [ - code_err(token), - text("not a type or type operator"), - ] + | BadToken(token) => [code(token), text("not a type or type operator")] | WantConstructorFoundAp | WantConstructorFoundType(_) => [text("Expected a constructor")] | WantTypeFoundAp => [text("Must be part of a sum type")] @@ -201,8 +233,7 @@ let typ_err_view = (ok: Info.error_typ) => 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")]) + | InHole(FreeVariable(name)) => div_err([code(name), text("not found")]) | InHole(InexhaustiveMatch(additional_err)) => let cls_str = Cls.show(cls); switch (additional_err) { @@ -231,11 +262,25 @@ let rec exp_view = (cls: Cls.t, status: Info.status_exp, info: Info.exp) => ), ]) | InHole(Common(error)) => - div_err(common_err_view(~lifted_ty=?info.lifted_ty, cls, error)) + div_err( + common_err_view( + ~lifted_ty=?info.lifted_ty, + ~sugar_info=?info.sugar_info, + cls, + error, + ), + ) | NotInHole(AnaDeferralConsistent(ana)) => div_ok([text("Expecting type"), Type.view(ana)]) | NotInHole(Common(ok)) => - div_ok(common_ok_view(~lifted_ty=?info.lifted_ty, cls, ok)) + div_ok( + common_ok_view( + ~lifted_ty=?info.lifted_ty, + ~sugar_info=?info.sugar_info, + cls, + ok, + ), + ) }; let rec pat_view = (cls: Cls.t, status: Info.status_pat) => @@ -284,6 +329,7 @@ let tpat_view = (_: Cls.t, status: Info.status_tpat) => let secondary_view = (cls: Cls.t) => div_ok([text(cls |> Cls.show)]); let view_of_info = (~inject, ~settings, ci): list(Node.t) => { + print_endline("CI: " ++ Info.show(ci)); let wrapper = status_view => [ term_view(~inject, ~settings, ci), status_view,