From 5a482b37ce6e5216d4c74843bfefb768e843c950 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Tue, 21 May 2024 14:10:08 -0400 Subject: [PATCH] Delete DHDoc_Exp --- src/haz3lweb/view/TestView.re | 252 +++++---- src/haz3lweb/view/dhcode/DHCode.re | 201 ------- src/haz3lweb/view/dhcode/DHDecoration.re | 2 - src/haz3lweb/view/dhcode/Decoration_common.re | 182 ------ src/haz3lweb/view/dhcode/layout/DHAnnot.re | 22 - src/haz3lweb/view/dhcode/layout/DHDoc.re | 4 - src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 535 ------------------ src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re | 98 ---- src/haz3lweb/view/dhcode/layout/DHDoc_Typ.re | 12 - src/haz3lweb/view/dhcode/layout/DHDoc_Util.re | 107 ---- .../view/dhcode/layout/DHDoc_common.re | 139 ----- .../view/dhcode/layout/DHDoc_common.rei | 97 ---- src/haz3lweb/view/dhcode/layout/DHLayout.re | 4 - src/haz3lweb/view/dhcode/layout/DHLayout.rei | 2 - .../view/dhcode/layout/DHMeasuredLayout.re | 7 - src/haz3lweb/view/dhcode/layout/HTypAnnot.re | 5 - src/haz3lweb/view/dhcode/layout/HTypAnnot.rei | 5 - src/haz3lweb/view/dhcode/layout/HTypDoc.re | 183 ------ src/haz3lweb/view/dhcode/layout/HTypDoc.rei | 5 - 19 files changed, 131 insertions(+), 1731 deletions(-) delete mode 100644 src/haz3lweb/view/dhcode/DHCode.re delete mode 100644 src/haz3lweb/view/dhcode/DHDecoration.re delete mode 100644 src/haz3lweb/view/dhcode/Decoration_common.re delete mode 100644 src/haz3lweb/view/dhcode/layout/DHAnnot.re delete mode 100644 src/haz3lweb/view/dhcode/layout/DHDoc.re delete mode 100644 src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re delete mode 100644 src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re delete mode 100644 src/haz3lweb/view/dhcode/layout/DHDoc_Typ.re delete mode 100644 src/haz3lweb/view/dhcode/layout/DHDoc_Util.re delete mode 100644 src/haz3lweb/view/dhcode/layout/DHDoc_common.re delete mode 100644 src/haz3lweb/view/dhcode/layout/DHDoc_common.rei delete mode 100644 src/haz3lweb/view/dhcode/layout/DHLayout.re delete mode 100644 src/haz3lweb/view/dhcode/layout/DHLayout.rei delete mode 100644 src/haz3lweb/view/dhcode/layout/DHMeasuredLayout.re delete mode 100644 src/haz3lweb/view/dhcode/layout/HTypAnnot.re delete mode 100644 src/haz3lweb/view/dhcode/layout/HTypAnnot.rei delete mode 100644 src/haz3lweb/view/dhcode/layout/HTypDoc.re delete mode 100644 src/haz3lweb/view/dhcode/layout/HTypDoc.rei diff --git a/src/haz3lweb/view/TestView.re b/src/haz3lweb/view/TestView.re index 264694e28b..b6acb77f60 100644 --- a/src/haz3lweb/view/TestView.re +++ b/src/haz3lweb/view/TestView.re @@ -7,30 +7,40 @@ module TestMap = Haz3lcore.TestMap; module TestResults = Haz3lcore.TestResults; module Interface = Haz3lcore.Interface; -let test_instance_view = - ( - ~settings, - ~inject, - ~font_metrics, - ~infomap, - (d, status): TestMap.instance_report, - ) => - div( - ~attr= - Attr.many([clss(["test-instance", TestStatus.to_string(status)])]), - [ - DHCode.view( - ~inject, - ~settings, - ~selected_hole_instance=None, - ~font_metrics, - ~width=40, - ~result_key="", - ~infomap, - d, - ), - ], - ); +// let test_instance_view = +// ( +// ~settings, +// ~inject, +// ~font_metrics, +// ~infomap, +// (d, status): TestMap.instance_report, +// ) => +// div( +// ~attr= +// Attr.many([clss(["test-instance", TestStatus.to_string(status)])]), +// [ +// ReadOnlyEditor.view( +// ~inject, +// ~settings, +// ~font_metrics, +// ~width=40, +// ~result_key="", +// ~infomap, +// d, +// ), +// ) +// DHCode.view( +// ~inject, +// ~settings, +// ~selected_hole_instance=None, +// ~font_metrics, +// ~width=40, +// ~result_key="", +// ~infomap, +// d, +// ), +// ], +// ); let jump_to_test = (~inject, pos, id, _) => { let effect1 = inject(Update.MakeActive(Exercises(pos, MainEditor))); @@ -38,75 +48,75 @@ let jump_to_test = (~inject, pos, id, _) => { Effect.bind(effect1, ~f=_result1 => effect2); }; -let test_report_view = - ( - ~settings, - ~inject, - ~font_metrics, - ~description: option(string)=None, - ~infomap, - i: int, - (id, instance_reports): TestMap.report, - ) => { - let status = - instance_reports |> TestMap.joint_status |> TestStatus.to_string; - div( - ~attr= - Attr.many([ - Attr.class_("test-report"), - Attr.on_click(jump_to_test(~inject, YourTestsTesting, id)), - ]), - [ - div( - ~attr=clss(["test-id", "Test" ++ status]), - // note: prints lexical index, not id - [text(string_of_int(i + 1))], - ), - div( - ~attr=Attr.class_("test-instances"), - List.map( - test_instance_view(~infomap, ~settings, ~inject, ~font_metrics), - instance_reports, - ), - ), - ] - @ ( - switch (description) { - | None => [] - | Some(d) => [div(~attr=clss(["test-description"]), [text(d)])] - } - ), - ); -}; +// let test_report_view = +// ( +// ~settings, +// ~inject, +// ~font_metrics, +// ~description: option(string)=None, +// ~infomap, +// i: int, +// (id, instance_reports): TestMap.report, +// ) => { +// let status = +// instance_reports |> TestMap.joint_status |> TestStatus.to_string; +// div( +// ~attr= +// Attr.many([ +// Attr.class_("test-report"), +// Attr.on_click(jump_to_test(~inject, YourTestsTesting, id)), +// ]), +// [ +// div( +// ~attr=clss(["test-id", "Test" ++ status]), +// // note: prints lexical index, not id +// [text(string_of_int(i + 1))], +// ), +// div( +// ~attr=Attr.class_("test-instances"), +// List.map( +// test_instance_view(~infomap, ~settings, ~inject, ~font_metrics), +// instance_reports, +// ), +// ), +// ] +// @ ( +// switch (description) { +// | None => [] +// | Some(d) => [div(~attr=clss(["test-description"]), [text(d)])] +// } +// ), +// ); +// }; -let test_reports_view = - ( - ~settings, - ~inject, - ~font_metrics, - ~infomap, - ~test_results: option(TestResults.t), - ) => - div( - ~attr=clss(["panel-body", "test-reports"]), - switch (test_results) { - | None => [Node.text("No test report available.")] - | Some(test_results) => - List.mapi( - (i, r) => - test_report_view( - ~settings, - ~inject, - ~font_metrics, - ~infomap, - ~description=List.nth_opt(test_results.descriptions, i), - i, - r, - ), - test_results.test_map, - ) - }, - ); +// let test_reports_view = +// ( +// ~settings, +// ~inject, +// ~font_metrics, +// ~infomap, +// ~test_results: option(TestResults.t), +// ) => +// div( +// ~attr=clss(["panel-body", "test-reports"]), +// switch (test_results) { +// | None => [Node.text("No test report available.")] +// | Some(test_results) => +// List.mapi( +// (i, r) => +// test_report_view( +// ~settings, +// ~inject, +// ~font_metrics, +// ~infomap, +// ~description=List.nth_opt(test_results.descriptions, i), +// i, +// r, +// ), +// test_results.test_map, +// ) +// }, +// ); let test_bar_segment = (~inject, pos, (id, reports)) => { let status = reports |> TestMap.joint_status |> TestStatus.to_string; @@ -171,32 +181,32 @@ let view_of_main_title_bar = (title_text: string) => [Node.text(title_text)], ); -let inspector_view = - ( - ~settings, - ~inject, - ~font_metrics, - ~test_map: TestMap.t, - ~infomap, - id: Haz3lcore.Id.t, - ) - : option(t) => { - switch (TestMap.lookup(id, test_map)) { - | Some(instances) when TestMap.joint_status(instances) != Indet => - Some( - div( - ~attr=Attr.class_("test-inspector"), - [ - div( - ~attr=Attr.class_("test-instances"), - List.map( - test_instance_view(~settings, ~inject, ~font_metrics, ~infomap), - instances, - ), - ), - ], - ), - ) - | _ => None - }; -}; +// let inspector_view = +// ( +// ~settings, +// ~inject, +// ~font_metrics, +// ~test_map: TestMap.t, +// ~infomap, +// id: Haz3lcore.Id.t, +// ) +// : option(t) => { +// switch (TestMap.lookup(id, test_map)) { +// | Some(instances) when TestMap.joint_status(instances) != Indet => +// Some( +// div( +// ~attr=Attr.class_("test-inspector"), +// [ +// div( +// ~attr=Attr.class_("test-instances"), +// List.map( +// test_instance_view(~settings, ~inject, ~font_metrics, ~infomap), +// instances, +// ), +// ), +// ], +// ), +// ) +// | _ => None +// }; +// }; diff --git a/src/haz3lweb/view/dhcode/DHCode.re b/src/haz3lweb/view/dhcode/DHCode.re deleted file mode 100644 index 727cf703ed..0000000000 --- a/src/haz3lweb/view/dhcode/DHCode.re +++ /dev/null @@ -1,201 +0,0 @@ -open Virtual_dom; -open Virtual_dom.Vdom; -open Util; -open Pretty; -open Haz3lcore; - -let with_cls = cls => Node.span(~attr=Attr.classes([cls])); - -let view_of_layout = - (~inject, ~font_metrics: FontMetrics.t, ~result_key, l: DHLayout.t) - : Node.t => { - let corner_radii = Decoration_common.corner_radii(font_metrics); - let (text, decorations) = - DHMeasuredLayout.mk(l) - |> MeasuredLayout.pos_fold( - ~linebreak=_ => ([Node.br()], []), - ~text=(_, s) => ([Node.text(s)], []), - ~align= - (_, (txt, ds)) => - ([Node.div(~attr=Attr.classes(["Align"]), txt)], ds), - ~cat=(_, (txt1, ds1), (txt2, ds2)) => (txt1 @ txt2, ds1 @ ds2), - ~annot= - (~go, ~indent, ~start, annot: DHAnnot.t, m) => { - let (txt, ds) = go(m); - switch (annot) { - | Steppable(obj) => ( - [ - Node.span( - ~attr= - Attr.many([ - Attr.class_("steppable"), - Attr.on_click(_ => - inject( - UpdateAction.StepperAction( - result_key, - StepForward(obj), - ), - ) - ), - ]), - txt, - ), - ], - ds, - ) - | Stepped => ( - [ - Node.span(~attr=Attr.many([Attr.class_("stepped")]), txt), - ], - ds, - ) - | Substituted => ( - [ - Node.span( - ~attr=Attr.many([Attr.class_("substituted")]), - txt, - ), - ], - ds, - ) - | Step(_) - | Term => (txt, ds) - | Collapsed => ([with_cls("Collapsed", txt)], ds) - | HoleLabel => ([with_cls("HoleLabel", txt)], ds) - | Delim => ([with_cls("code-delim", txt)], ds) - | EmptyHole(selected, _inst) => ( - [ - Node.span( - ~attr= - Attr.many([ - Attr.classes([ - "EmptyHole", - ...selected ? ["selected"] : [], - ]), - Attr.on_click(_ => - Vdom.Effect.Many([ - Vdom.Effect.Stop_propagation, - //inject(ModelAction.SelectHoleInstance(inst)), - ]) - ), - ]), - txt, - ), - ], - ds, - ) - | FailedCastDelim => ([with_cls("FailedCastDelim", txt)], ds) - | FailedCastDecoration => ( - [with_cls("FailedCastDecoration", txt)], - ds, - ) - | CastDecoration => ([with_cls("CastDecoration", txt)], ds) - | OperationError( - DivideByZero | InvalidOfString | IndexOutOfBounds, - ) => ( - [with_cls("OperationError", txt)], - ds, - ) - | OperationError(NegativeExponent) => ( - [with_cls("OperationError", txt)], - ds, - ) - | OperationError(OutOfFuel) => ( - [with_cls("OperationError", txt)], - ds, - ) - | VarHole(_) => ([with_cls("InVarHole", txt)], ds) - | NonEmptyHole - | InconsistentBranches(_) - | Invalid => - let offset = start.col - indent; - let decoration = - Decoration_common.container( - ~container_type=Svg, - ~font_metrics, - ~height=MeasuredLayout.height(m), - ~width=MeasuredLayout.width(~offset, m), - ~origin=MeasuredPosition.{row: start.row, col: indent}, - ~cls="err-hole", - [DHDecoration.ErrHole.view(~corner_radii, (offset, m))], - ); - (txt, [decoration, ...ds]); - }; - }, - ); - Node.div( - ~attr=Attr.classes(["DHCode"]), - [with_cls("code", text), ...decorations], - ); -}; - -let _view = - ( - ~locked as _=false, // NOTE: When we add mouse events to this, ignore them if locked - ~inject, - ~settings: CoreSettings.Evaluation.t, - ~selected_hole_instance: option(Id.t), - ~font_metrics: FontMetrics.t, - ~width: int, - ~pos=0, - ~previous_step: option((EvaluatorStep.step, Id.t))=None, // The step that will be displayed above this one - ~hidden_steps: list((EvaluatorStep.step, Id.t))=[], // The hidden steps between the above and the current one - ~chosen_step: option(EvaluatorStep.step)=None, // The step that will be taken next - ~next_steps: list((int, Id.t))=[], - ~result_key: string, - ~infomap, - d: DHExp.t, - ) - : Node.t => { - DHDoc_Exp.mk( - ~previous_step, - ~hidden_steps, - ~chosen_step, - ~next_steps, - ~env=ClosureEnvironment.empty, - ~settings, - ~enforce_inline=false, - ~selected_hole_instance, - ~infomap, - d, - ) - |> LayoutOfDoc.layout_of_doc(~width, ~pos) - |> OptUtil.get(() => - failwith("unimplemented: view_of_dhexp on layout failure") - ) - |> view_of_layout(~inject, ~font_metrics, ~result_key); -}; - -type font_metrics = FontMetrics.t; - -let view = - ( - ~locked as _=false, // NOTE: When we add mouse events to this, ignore them if locked - ~inject as _, - ~settings, - ~selected_hole_instance as _: option(Id.t), - ~font_metrics: FontMetrics.t, - ~width as _: int, - ~pos as _=0, - ~previous_step as _: option((EvaluatorStep.step, Id.t))=None, // The step that will be displayed above this one - ~hidden_steps as _: list((EvaluatorStep.step, Id.t))=[], // The hidden steps between the above and the current one - ~chosen_step as _: option(EvaluatorStep.step)=None, // The step that will be taken next - ~next_steps as _: list((int, Id.t))=[], - ~result_key: string, - ~infomap as _, - d: DHExp.t, - ) => { - let parenthesized = ExpToSegment.parenthesize(d); - let options = ExpToSegment.exp_to_pretty(~inline=false, parenthesized); - let option = PrettySegment.select(options); - let editor = Editor.init(~read_only=true, Zipper.unzip(option)); - let code_text_view = - Code.view(~sort=Sort.root, ~font_metrics, ~settings, editor); - let code_view = - Node.div( - ~attr= - Attr.many([Attr.id(result_key), Attr.classes(["code-container"])]), - [code_text_view], - ); - code_view; -}; diff --git a/src/haz3lweb/view/dhcode/DHDecoration.re b/src/haz3lweb/view/dhcode/DHDecoration.re deleted file mode 100644 index acd8532f3c..0000000000 --- a/src/haz3lweb/view/dhcode/DHDecoration.re +++ /dev/null @@ -1,2 +0,0 @@ -module ErrHole = Decoration_common.ErrHole; -module VarErrHole = Decoration_common.VarErrHole; diff --git a/src/haz3lweb/view/dhcode/Decoration_common.re b/src/haz3lweb/view/dhcode/Decoration_common.re deleted file mode 100644 index b56135d99d..0000000000 --- a/src/haz3lweb/view/dhcode/Decoration_common.re +++ /dev/null @@ -1,182 +0,0 @@ -open Virtual_dom.Vdom; - -module MeasuredPosition = Pretty.MeasuredPosition; -module MeasuredLayout = Pretty.MeasuredLayout; - -type container_type = - | Svg - | Div; - -/** - * A buffered container for SVG elements so that strokes along - * the bounding box of the elements do not get clipped by the - * viewBox boundaries - */ -let container = - ( - ~container_type: container_type, - ~font_metrics: FontMetrics.t, - ~origin: MeasuredPosition.t, - ~height: int, - ~width: int, - ~cls: string, - contents: list(Node.t), - ) - : Node.t => { - let buffered_height = height; - let buffered_width = width; - - let buffered_height_px = - Float.of_int(buffered_height) *. font_metrics.row_height; - let buffered_width_px = - Float.of_int(buffered_width) *. font_metrics.col_width; - - let container_origin_x = - Float.of_int(origin.row) *. font_metrics.row_height; - let container_origin_y = Float.of_int(origin.col) *. font_metrics.col_width; - - let inner = - switch (container_type) { - | Div => - Node.div( - ~attr= - Attr.many([ - Attr.classes([ - "decoration-container", - Printf.sprintf("%s-container", cls), - ]), - Attr.create( - "style", - Printf.sprintf( - "width: %fpx; height: %fpx;", - buffered_width_px, - buffered_height_px, - ), - ), - ]), - contents, - ) - | Svg => - Node.create_svg( - "svg", - ~attr= - Attr.many([ - Attr.classes([cls]), - Attr.create( - "viewBox", - Printf.sprintf("0 0 %d %d", buffered_width, buffered_height), - ), - Attr.create("width", Printf.sprintf("%fpx", buffered_width_px)), - Attr.create( - "height", - Printf.sprintf("%fpx", buffered_height_px), - ), - Attr.create("preserveAspectRatio", "none"), - ]), - contents, - ) - }; - Node.div( - ~attr= - Attr.many([ - Attr.classes([ - "decoration-container", - Printf.sprintf("%s-container", cls), - ]), - Attr.create( - "style", - Printf.sprintf( - "top: calc(%fpx); left: %fpx;", - container_origin_x, - container_origin_y, - ), - ), - ]), - [inner], - ); -}; - -let corner_radii = (font_metrics: FontMetrics.t) => { - let r = 2.5; - (r /. font_metrics.col_width, r /. font_metrics.row_height); -}; - -let rects = - ( - ~indent=0, - ~vtrim=0.0, - start: MeasuredPosition.t, - m: MeasuredLayout.t(_), - ) - : list(SvgUtil.Rect.t) => { - let mk_rect = - ( - ~is_first=false, - ~is_last=false, - start: MeasuredPosition.t, - box: MeasuredLayout.box, - ) => - SvgUtil.Rect.{ - min: { - x: Float.of_int(start.col), - y: Float.of_int(start.row) +. (is_first ? vtrim : 0.0), - }, - width: Float.of_int(box.width), - height: - Float.of_int(box.height) - -. (is_first ? vtrim : 0.0) - -. (is_last ? vtrim : 0.0), - }; - let n = List.length(m.metrics); - m.metrics - |> List.mapi((i, box) => (i, box)) - |> List.fold_left_map( - (start: MeasuredPosition.t, (i, box: MeasuredLayout.box)) => - ( - {row: start.row + box.height, col: indent}, - mk_rect(~is_first=i == 0, ~is_last=i == n - 1, start, box), - ), - start, - ) - |> snd; -}; - -module ErrHole = { - let view = - ( - ~vtrim=0., - ~corner_radii: (float, float), - (offset, subject): MeasuredLayout.with_offset(_), - ) - : Node.t => - subject - |> rects(~vtrim, {row: 0, col: offset}) - |> SvgUtil.OrthogonalPolygon.mk(~corner_radii) - |> SvgUtil.Path.view( - ~attrs= - Attr.[ - classes(["err-hole"]), - create("vector-effect", "non-scaling-stroke"), - ], - ); -}; - -module VarErrHole = { - let view = - ( - ~vtrim=0., - ~corner_radii: (float, float), - (offset, subject): MeasuredLayout.with_offset(_), - ) - : Node.t => - subject - |> rects(~vtrim, {row: 0, col: offset}) - |> SvgUtil.OrthogonalPolygon.mk(~corner_radii) - |> SvgUtil.Path.view( - ~attrs= - Attr.[ - classes(["var-err-hole"]), - create("vector-effect", "non-scaling-stroke"), - ], - ); -}; diff --git a/src/haz3lweb/view/dhcode/layout/DHAnnot.re b/src/haz3lweb/view/dhcode/layout/DHAnnot.re deleted file mode 100644 index 71f650fb50..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHAnnot.re +++ /dev/null @@ -1,22 +0,0 @@ -open Sexplib.Std; -open Haz3lcore; - -[@deriving sexp] -type t = - | Collapsed - | Step(int) - | Term - | HoleLabel - | Delim - | EmptyHole(bool, ClosureEnvironment.t) - | NonEmptyHole - | VarHole(VarErrStatus.HoleReason.t, Id.t) - | InconsistentBranches(Id.t) - | Invalid - | FailedCastDelim - | FailedCastDecoration - | CastDecoration - | OperationError(InvalidOperationError.t) - | Steppable(int) - | Stepped - | Substituted; diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc.re b/src/haz3lweb/view/dhcode/layout/DHDoc.re deleted file mode 100644 index b9d19c57cf..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHDoc.re +++ /dev/null @@ -1,4 +0,0 @@ -open Pretty; - -[@deriving sexp] -type t = Doc.t(DHAnnot.t); diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re deleted file mode 100644 index b6af6652ba..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ /dev/null @@ -1,535 +0,0 @@ -open Haz3lcore; -open EvaluatorStep; -open Transition; -module Doc = Pretty.Doc; - -let mk_bin_bool_op = (op: Operators.op_bin_bool): DHDoc.t => - Doc.text(Operators.bool_op_to_string(op)); - -let mk_bin_int_op = (op: Operators.op_bin_int): DHDoc.t => - Doc.text(Operators.int_op_to_string(op)); - -let mk_bin_float_op = (op: Operators.op_bin_float): DHDoc.t => - Doc.text(Operators.float_op_to_string(op)); - -let mk_bin_string_op = (op: Operators.op_bin_string): DHDoc.t => - Doc.text(Operators.string_op_to_string(op)); - -let mk = - ( - ~settings: CoreSettings.Evaluation.t, - ~enforce_inline: bool, - ~selected_hole_instance: option(Id.t), - // The next four are used when drawing the stepper to track where we can annotate changes - ~previous_step: option((step, Id.t)), // The step that will be displayed above this one (an Id in included because it may have changed since the step was taken) - ~hidden_steps: list((step, Id.t)), // The hidden steps between the above and the current one (an Id in included because it may have changed since the step was taken) - ~chosen_step: option(step), // The step that will be taken next - ~next_steps: list((int, Id.t)), // The options for the next step, if it hasn't been chosen yet - ~env: ClosureEnvironment.t, - ~infomap: Statics.Map.t, - d: DHExp.t, - ) - : DHDoc.t => { - // // print_endline(""); - // // let _ = - // // List.map( - // // ((x, y)) => { - // // print_endline(Id.show(y)); - // // print_endline(show_step_kind(x.knd)); - // // }, - // // hidden_steps, - // // ); - // let _ = print_endline("============"); - let rec go = - ( - d: DHExp.t, - env: ClosureEnvironment.t, - enforce_inline: bool, - recent_subst: list(Var.t), - ) - : DHDoc.t => { - open Doc; - let recent_subst = - switch (previous_step) { - | Some((ps, id)) when id == DHExp.rep_id(d) => - switch (ps.knd, DHExp.term_of(ps.d_loc)) { - | (FunAp, Ap(_, d2, _)) => - switch (DHExp.term_of(d2)) { - | Fun(p, _, _, _) => DHPat.bound_vars(p) - | _ => [] - } - | (FunAp, _) => [] - | (LetBind, Let(p, _, _)) => DHPat.bound_vars(p) - | (LetBind, _) => [] - | (FixUnwrap, FixF(p, _, _)) => DHPat.bound_vars(p) - | (FixUnwrap, _) => [] - | (TypFunAp, _) // TODO: Could also do something here for type variable substitution like in FunAp? - | (InvalidStep, _) - | (VarLookup, _) - | (Seq, _) - | (FunClosure, _) - | (FixClosure, _) - | (DeferredAp, _) - | (UpdateTest, _) - | (CastTypAp, _) - | (CastAp, _) - | (BuiltinWrap, _) - | (UnOp(_), _) - | (BuiltinAp(_), _) - | (BinBoolOp(_), _) - | (BinIntOp(_), _) - | (BinFloatOp(_), _) - | (BinStringOp(_), _) - | (Projection, _) - | (ListCons, _) - | (ListConcat, _) - | (CaseApply, _) - | (CompleteClosure, _) - | (CompleteFilter, _) - | (Cast, _) - | (Conditional(_), _) - | (RemoveParens, _) - | (RemoveTypeAlias, _) => [] // Maybe this last one could count as a substitution? - } - | _ => recent_subst - }; - let go' = - ( - ~env=env, - ~enforce_inline=enforce_inline, - ~recent_subst=recent_subst, - d, - ) => { - go(d, env, enforce_inline, recent_subst); - }; - let go_case_rule = ((dp, dclause)): DHDoc.t => { - let hidden_clause = annot(DHAnnot.Collapsed, text(Unicode.ellipsis)); - let clause_doc = - settings.show_case_clauses - ? choices([ - hcats([space(), go'(~enforce_inline=true, dclause)]), - hcats([ - linebreak(), - indent_and_align(go'(~enforce_inline=false, dclause)), - ]), - ]) - : hcat(space(), hidden_clause); - hcats([ - DHDoc_common.Delim.bar_Rule, - DHDoc_Pat.mk(~infomap, ~show_casts=settings.show_casts, dp) - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline=false, - ), - DHDoc_common.Delim.arrow_Rule, - clause_doc, - ]); - }; - let go_case = (dscrut, drs) => - if (enforce_inline) { - fail(); - } else { - let scrut_doc = - choices([ - hcats([space(), go'(~enforce_inline=true, dscrut)]), - hcats([ - linebreak(), - indent_and_align(go'(~enforce_inline=false, dscrut)), - ]), - ]); - vseps( - List.concat([ - [hcat(DHDoc_common.Delim.open_Case, scrut_doc)], - drs |> List.map(go_case_rule), - [DHDoc_common.Delim.close_Case], - ]), - ); - }; - let go_formattable = (~enforce_inline) => go'(~enforce_inline); - let mk_left_associative_operands = (d1, d2) => (go'(d1), go'(d2)); - let mk_right_associative_operands = (d1, d2) => (go'(d1), go'(d2)); - let doc = { - switch (DHExp.term_of(d)) { - | Parens(d') => hseps([text("("), go'(d'), text(")")]) - | Closure(env', d') => go'(d', ~env=env') - | Filter(flt, d') => - if (settings.show_stepper_filters) { - switch (flt) { - | Filter({pat, act}) => - let keyword = FilterAction.string_of_t(act); - let flt_doc = go_formattable(pat); - vseps([ - hcats([ - DHDoc_common.Delim.mk(keyword), - flt_doc - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline=false, - ), - DHDoc_common.Delim.mk("in"), - ]), - go'(d'), - ]); - | Residue(_, act) => - let keyword = FilterAction.string_of_t(act); - vseps([DHDoc_common.Delim.mk(keyword), go'(d')]); - }; - } else { - switch (flt) { - | Residue(_) => go'(d') - | Filter(_) => go'(d') - }; - } - - /* Hole expressions must appear within a closure in - the postprocessed result */ - | EmptyHole => - DHDoc_common.mk_EmptyHole( - ~selected=Some(DHExp.rep_id(d)) == selected_hole_instance, - env, - ) - | MultiHole(_ds) => - //ds |> List.map(go') |> Doc.hcats - DHDoc_common.mk_EmptyHole( - ~selected=Some(DHExp.rep_id(d)) == selected_hole_instance, - env, - ) - | Invalid(t) => DHDoc_common.mk_InvalidText(t) - | Var(x) when settings.show_lookup_steps => text(x) - | Var(x) => - switch (ClosureEnvironment.lookup(env, x)) { - | None => text(x) - | Some(d') => - if (List.mem(x, recent_subst)) { - hcats([ - go'(~env=ClosureEnvironment.empty, d) - |> annot(DHAnnot.Substituted), - go'( - ~env=ClosureEnvironment.empty, - ~recent_subst=List.filter(u => u != x, recent_subst), - d', - ), - ]); - } else { - go'(~env=ClosureEnvironment.empty, d'); - } - } - | BuiltinFun(f) => text(f) - | Constructor(name) => DHDoc_common.mk_ConstructorLit(name) - | Bool(b) => DHDoc_common.mk_BoolLit(b) - | Int(n) => DHDoc_common.mk_IntLit(n) - | Float(f) => DHDoc_common.mk_FloatLit(f) - | String(s) => DHDoc_common.mk_StringLit(s) - | Test(d) => DHDoc_common.mk_Test(go'(d)) - | Deferral(_) => text("_") - | Seq(d1, d2) => - let (doc1, doc2) = (go'(d1), go'(d2)); - DHDoc_common.mk_Sequence(doc1, doc2); - | ListLit(d_list) => - let ol = d_list |> List.map(d => go'(d)); - DHDoc_common.mk_ListLit(ol); - | Ap(Forward, d1, d2) => - let (doc1, doc2) = (go'(d1), go'(d2)); - DHDoc_common.mk_Ap(doc1, doc2); - | DeferredAp(d1, d2) => - let (doc1, doc2) = (go'(d1), go'(Tuple(d2) |> DHExp.fresh)); - DHDoc_common.mk_Ap(doc1, doc2); - | TypAp(d1, ty) => - let doc1 = go'(d1); - let doc2 = DHDoc_Typ.mk(~enforce_inline=true, ty); - DHDoc_common.mk_TypAp(doc1, doc2); - | Ap(Reverse, d1, d2) => - let (doc1, doc2) = (go'(d1), go'(d2)); - DHDoc_common.mk_rev_Ap(doc2, doc1); - | UnOp(Meta(Unquote), d) => Doc.hcats([text("$"), go'(d)]) - | UnOp(Bool(Not), d) => Doc.hcats([text("!"), go'(d)]) - | UnOp(Int(Minus), d) => Doc.hcats([text("-"), go'(d)]) - | BinOp(Int(op), d1, d2) => - // TODO assumes all bin int ops are left associative - let (doc1, doc2) = mk_left_associative_operands(d1, d2); - hseps([doc1, mk_bin_int_op(op), doc2]); - | BinOp(Float(op), d1, d2) => - // TODO assumes all bin float ops are left associative - let (doc1, doc2) = mk_left_associative_operands(d1, d2); - hseps([doc1, mk_bin_float_op(op), doc2]); - | BinOp(String(op), d1, d2) => - // TODO assumes all bin string ops are left associative - let (doc1, doc2) = mk_left_associative_operands(d1, d2); - hseps([doc1, mk_bin_string_op(op), doc2]); - | Cons(d1, d2) => - let (doc1, doc2) = mk_right_associative_operands(d1, d2); - DHDoc_common.mk_Cons(doc1, doc2); - | ListConcat(d1, d2) => - let (doc1, doc2) = mk_right_associative_operands(d1, d2); - DHDoc_common.mk_ListConcat(doc1, doc2); - | BinOp(Bool(op), d1, d2) => - let (doc1, doc2) = mk_right_associative_operands(d1, d2); - hseps([doc1, mk_bin_bool_op(op), doc2]); - | Tuple([]) => DHDoc_common.Delim.triv - | Tuple(ds) => DHDoc_common.mk_Tuple(ds |> List.map(d => go'(d))) - | Match(dscrut, drs) => go_case(dscrut, drs) - | TyAlias(_, _, d) => go'(d) - | Cast(d, t1, t2) when settings.show_casts => - // TODO[Matt]: Roll multiple casts into one cast - let doc = go'(d); - Doc.( - hcat( - doc, - annot( - DHAnnot.CastDecoration, - hcats([ - DHDoc_common.Delim.open_Cast, - DHDoc_Typ.mk(~enforce_inline=true, t1), - DHDoc_common.Delim.arrow_Cast, - DHDoc_Typ.mk(~enforce_inline=true, t2), - DHDoc_common.Delim.close_Cast, - ]), - ), - ) - ); - | Cast(d, _, _) => - let doc = go'(d); - doc; - | Let(dp, ddef, dbody) => - if (enforce_inline) { - fail(); - } else { - let bindings = DHPat.bound_vars(dp); - let def_doc = go_formattable(ddef); - vseps([ - hcats([ - DHDoc_common.Delim.mk("let"), - DHDoc_Pat.mk(~infomap, ~show_casts=settings.show_casts, dp) - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline, - ), - DHDoc_common.Delim.mk("="), - def_doc - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline=false, - ), - DHDoc_common.Delim.mk("in"), - ]), - go'( - ~enforce_inline=false, - ~env=ClosureEnvironment.without_keys(bindings, env), - ~recent_subst= - List.filter(x => !List.mem(x, bindings), recent_subst), - dbody, - ), - ]); - } - | FailedCast(d1, ty1, ty3) => - let d_doc = go'(d1); - let cast_decoration = - hcats([ - DHDoc_common.Delim.open_FailedCast, - hseps([ - DHDoc_Typ.mk(~enforce_inline=true, ty1), - DHDoc_common.Delim.arrow_FailedCast, - DHDoc_Typ.mk(~enforce_inline=true, ty3), - ]), - DHDoc_common.Delim.close_FailedCast, - ]) - |> annot(DHAnnot.FailedCastDecoration); - hcats([d_doc, cast_decoration]); - | DynamicErrorHole(d, err) => - let d_doc = go'(d); - let decoration = - Doc.text(InvalidOperationError.err_msg(err)) - |> annot(DHAnnot.OperationError(err)); - hcats([d_doc, decoration]); - | If(c, d1, d2) => - let c_doc = go_formattable(c); - let d1_doc = go_formattable(d1); - let d2_doc = go_formattable(d2); - hcats([ - DHDoc_common.Delim.mk("("), - DHDoc_common.Delim.mk("if"), - c_doc - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline=false, - ), - DHDoc_common.Delim.mk("then"), - d1_doc - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline=false, - ), - DHDoc_common.Delim.mk("else"), - d2_doc - |> DHDoc_common.pad_child( - ~inline_padding=(space(), empty()), - ~enforce_inline=false, - ), - DHDoc_common.Delim.mk(")"), - ]); - | Fun(dp, d, Some(env'), s) => - if (settings.show_fn_bodies) { - let bindings = DHPat.bound_vars(dp); - let body_doc = - go_formattable( - Closure( - ClosureEnvironment.without_keys(Option.to_list(s), env'), - d, - ) - |> DHExp.fresh, - ~env= - ClosureEnvironment.without_keys( - DHPat.bound_vars(dp) @ Option.to_list(s), - env, - ), - ~recent_subst= - List.filter(x => !List.mem(x, bindings), recent_subst), - ); - hcats( - [ - DHDoc_common.Delim.sym_Fun, - DHDoc_Pat.mk(~infomap, ~show_casts=settings.show_casts, dp) - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline, - ), - ] - @ [ - DHDoc_common.Delim.arrow_Fun, - space(), - body_doc |> DHDoc_common.pad_child(~enforce_inline=false), - ], - ); - } else { - annot( - DHAnnot.Collapsed, - text( - switch (s) { - | None => "" - | Some(name) - when - !settings.show_fixpoints - && String.ends_with(~suffix="+", name) => - "<" ++ String.sub(name, 0, String.length(name) - 1) ++ ">" - | Some(name) => "<" ++ name ++ ">" - }, - ), - ); - } - | Fun(dp, dbody, None, s) => - if (settings.show_fn_bodies) { - let bindings = DHPat.bound_vars(dp); - let body_doc = - go_formattable( - dbody, - ~env=ClosureEnvironment.without_keys(bindings, env), - ~recent_subst= - List.filter(x => !List.mem(x, bindings), recent_subst), - ); - hcats( - [ - DHDoc_common.Delim.sym_Fun, - DHDoc_Pat.mk(~infomap, ~show_casts=settings.show_casts, dp) - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline, - ), - ] - @ [ - DHDoc_common.Delim.arrow_Fun, - space(), - body_doc |> DHDoc_common.pad_child(~enforce_inline), - ], - ); - } else { - switch (s) { - | None => annot(DHAnnot.Collapsed, text("")) - | Some(name) => annot(DHAnnot.Collapsed, text("<" ++ name ++ ">")) - }; - } - | TypFun(_tpat, _dbody, s) => - /* same display as with Fun but with anon typfn in the nameless case. */ - let name = - switch (s) { - | None => "anon typfn" - | Some(name) - when - !settings.show_fixpoints - && String.ends_with(~suffix="+", name) => - String.sub(name, 0, String.length(name) - 1) - | Some(name) => name - }; - annot(DHAnnot.Collapsed, text("<" ++ name ++ ">")); - | FixF(dp, dbody, _) - when settings.show_fn_bodies && settings.show_fixpoints => - let doc_body = - go_formattable( - dbody, - ~env=ClosureEnvironment.without_keys(DHPat.bound_vars(dp), env), - ); - hcats( - [ - DHDoc_common.Delim.fix_FixF, - space(), - DHDoc_Pat.mk( - ~infomap, - dp, - ~show_casts=settings.show_casts, - ~enforce_inline=true, - ), - ] - @ [ - space(), - DHDoc_common.Delim.arrow_FixF, - space(), - doc_body |> DHDoc_common.pad_child(~enforce_inline), - ], - ); - | FixF(_, {term: Fun(_, _, _, Some(x)), _}, _) => - if (String.ends_with(~suffix="+", x)) { - annot( - DHAnnot.Collapsed, - text("<" ++ String.sub(x, 0, String.length(x) - 1) ++ ">"), - ); - } else { - annot(DHAnnot.Collapsed, text("<" ++ x ++ ">")); - } - | FixF(_, _, _) => annot(DHAnnot.Collapsed, text("")) - }; - }; - let steppable = - next_steps |> List.find_opt(((_, id)) => id == DHExp.rep_id(d)); - let stepped = - chosen_step - |> Option.map(x => DHExp.rep_id(x.d_loc) == DHExp.rep_id(d)) - |> Option.value(~default=false); - let substitution = - hidden_steps - |> List.find_opt(((step, id)) => - step.knd == VarLookup - // HACK[Matt]: to prevent substitutions hiding inside casts - && id == DHExp.rep_id(d) - ); - let doc = - switch (substitution) { - | Some((step, _)) => - switch (DHExp.term_of(step.d_loc)) { - | Var(v) when List.mem(v, recent_subst) => - hcats([text(v) |> annot(DHAnnot.Substituted), doc]) - | _ => doc - } - | None => doc - }; - let doc = - if (stepped) { - annot(DHAnnot.Stepped, doc); - } else { - switch (steppable) { - | Some((i, _)) => annot(DHAnnot.Steppable(i), doc) - | None => doc - }; - }; - doc; - }; - go(d, env, enforce_inline, []); -}; diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re deleted file mode 100644 index 95743d8f3e..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re +++ /dev/null @@ -1,98 +0,0 @@ -open Pretty; -open Haz3lcore; - -let precedence = (dp: Pat.t) => - switch (DHPat.term_of(dp)) { - | EmptyHole - | MultiHole(_) - | Wild - | Invalid(_) - | Var(_) - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Constructor(_) => DHDoc_common.precedence_const - | Tuple(_) => DHDoc_common.precedence_Comma - | Cons(_) => DHDoc_common.precedence_Cons - | Ap(_) => DHDoc_common.precedence_Ap - | Parens(_) => DHDoc_common.precedence_const - | Cast(_) => DHDoc_common.precedence_Ap - }; - -let rec mk = - ( - ~infomap: Statics.Map.t, - ~parenthesize=false, - ~show_casts, - ~enforce_inline: bool, - dp: Pat.t, - ) - : DHDoc.t => { - let mk' = mk(~enforce_inline, ~infomap, ~show_casts); - let mk_left_associative_operands = (precedence_op, dp1, dp2) => ( - mk'(~parenthesize=precedence(dp1) > precedence_op, dp1), - mk'(~parenthesize=precedence(dp2) >= precedence_op, dp2), - ); - let mk_right_associative_operands = (precedence_op, dp1, dp2) => ( - mk'(~parenthesize=precedence(dp1) >= precedence_op, dp1), - mk'(~parenthesize=precedence(dp2) > precedence_op, dp2), - ); - let doc = - switch (DHPat.term_of(dp)) { - | MultiHole(_) - | EmptyHole => DHDoc_common.mk_EmptyHole(ClosureEnvironment.empty) - | Invalid(t) => DHDoc_common.mk_InvalidText(t) - | Var(x) => Doc.text(x) - | Wild => DHDoc_common.Delim.wild - | Constructor(name) => DHDoc_common.mk_ConstructorLit(name) - | Int(n) => DHDoc_common.mk_IntLit(n) - | Float(f) => DHDoc_common.mk_FloatLit(f) - | Bool(b) => DHDoc_common.mk_BoolLit(b) - | String(s) => DHDoc_common.mk_StringLit(s) - | ListLit(d_list) => - let ol = List.map(mk', d_list); - DHDoc_common.mk_ListLit(ol); - | Cons(dp1, dp2) => - let (doc1, doc2) = - mk_right_associative_operands(DHDoc_common.precedence_Cons, dp1, dp2); - DHDoc_common.mk_Cons(doc1, doc2); - | Tuple([]) => DHDoc_common.Delim.triv - | Tuple(ds) => DHDoc_common.mk_Tuple(List.map(mk', ds)) - // TODO: Print type annotations - | Cast(dp, t1, t2) when show_casts => - Doc.hcats([ - mk'(dp), - Doc.annot( - DHAnnot.CastDecoration, - Doc.hcats([ - DHDoc_common.Delim.open_Cast, - DHDoc_Typ.mk(~enforce_inline=true, t1), - DHDoc_common.Delim.back_arrow_Cast, - DHDoc_Typ.mk(~enforce_inline=true, t2), - DHDoc_common.Delim.close_Cast, - ]), - ), - ]) - | Cast(dp, _, _) => mk'(~parenthesize, dp) - | Parens(dp) => - mk(~enforce_inline, ~parenthesize=true, ~infomap, ~show_casts, dp) - | Ap(dp1, dp2) => - let (doc1, doc2) = - mk_left_associative_operands(DHDoc_common.precedence_Ap, dp1, dp2); - DHDoc_common.mk_Ap(doc1, doc2); - }; - let doc = - switch (Statics.get_pat_error_at(infomap, DHPat.rep_id(dp))) { - | Some(_) => Doc.annot(DHAnnot.NonEmptyHole, doc) - | None => doc - }; - parenthesize - ? Doc.hcats([ - DHDoc_common.Delim.open_Parenthesized, - doc, - DHDoc_common.Delim.close_Parenthesized, - ]) - : doc; -}; diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Typ.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Typ.re deleted file mode 100644 index 143e36d3e3..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Typ.re +++ /dev/null @@ -1,12 +0,0 @@ -open Haz3lcore; -open Pretty; - -let promote_annot = - fun - | HTypAnnot.Term => DHAnnot.Term - | HTypAnnot.Step(n) => DHAnnot.Step(n) - | HTypAnnot.HoleLabel => DHAnnot.HoleLabel - | HTypAnnot.Delim => DHAnnot.Delim; -let promote = (d: HTypDoc.t): DHDoc.t => d |> Doc.map_annot(promote_annot); -let mk = (~enforce_inline: bool, ty: Typ.t): DHDoc.t => - ty |> HTypDoc.mk(~enforce_inline) |> promote; diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Util.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Util.re deleted file mode 100644 index 9e9578d217..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Util.re +++ /dev/null @@ -1,107 +0,0 @@ -open Haz3lcore; - -module Doc = Pretty.Doc; - -[@deriving sexp] -type t = Doc.t(DHAnnot.t); - -type formattable_child = (~enforce_inline: bool) => t; - -let precedence_const = DHDoc_common.precedence_const; -let precedence_Ap = DHDoc_common.precedence_Ap; -let precedence_Times = DHDoc_common.precedence_Times; -let precedence_Divide = DHDoc_common.precedence_Divide; -let precedence_Plus = DHDoc_common.precedence_Plus; -let precedence_Minus = DHDoc_common.precedence_Minus; -let precedence_Cons = DHDoc_common.precedence_Cons; -let precedence_Equals = DHDoc_common.precedence_Equals; -let precedence_LessThan = DHDoc_common.precedence_LessThan; -let precedence_GreaterThan = DHDoc_common.precedence_GreaterThan; -let precedence_And = DHDoc_common.precedence_And; -let precedence_Or = DHDoc_common.precedence_Or; -let precedence_Comma = DHDoc_common.precedence_Comma; -let precedence_max = DHDoc_common.precedence_max; - -let pad_child = - ( - ~inline_padding as (l, r)=(Doc.empty(), Doc.empty()), - ~enforce_inline: bool, - child: formattable_child, - ) - : t => { - let inline_choice = Doc.hcats([l, child(~enforce_inline=true), r]); - let para_choice = - Doc.( - hcats([ - linebreak(), - indent_and_align(child(~enforce_inline=false)), - linebreak(), - ]) - ); - enforce_inline ? inline_choice : Doc.choice(inline_choice, para_choice); -}; - -module Delim = { - let mk = (delim_text: string): t => - Doc.text(delim_text) |> Doc.annot(DHAnnot.Delim); - - let empty_hole = (_env: ClosureEnvironment.t): t => { - let lbl = "-"; - Doc.text(lbl) - |> Doc.annot(DHAnnot.HoleLabel) - |> Doc.annot(DHAnnot.Delim); - }; - - let list_nil = mk("[]"); - let triv = mk("()"); - let wild = mk("_"); - - let open_Parenthesized = mk("("); - let close_Parenthesized = mk(")"); - - let sym_Fun = mk("fun"); - let colon_Lam = mk(":"); - let open_Lam = mk(".{"); - let close_Lam = mk("}"); - - let fix_FixF = mk("fix"); - let colon_FixF = mk(":"); - let open_FixF = mk(".{"); - let close_FixF = mk("}"); - let open_Case = mk("case"); - let close_Case = mk("end"); - - let bar_Rule = mk("|"); - let arrow_Rule = mk("=>"); - - let open_Cast = mk("<"); - let arrow_Cast = mk(Unicode.castArrowSym); - let close_Cast = mk(">"); - - let open_FailedCast = open_Cast |> Doc.annot(DHAnnot.FailedCastDelim); - let arrow_FailedCast = - mk(Unicode.castArrowSym) |> Doc.annot(DHAnnot.FailedCastDelim); - let close_FailedCast = close_Cast |> Doc.annot(DHAnnot.FailedCastDelim); -}; - -let mk_EmptyHole = (~selected=false, env) => - Delim.empty_hole(env) |> Doc.annot(DHAnnot.EmptyHole(selected, env)); - -let mk_IntLit = n => Doc.text(string_of_int(n)); - -let mk_FloatLit = (f: float) => - switch (f < 0., Float.is_infinite(f), Float.is_nan(f)) { - | (false, true, _) => Doc.text("Inf") - /* TODO: NegInf is temporarily introduced until unary minus is introduced to Hazel */ - | (true, true, _) => Doc.text("NegInf") - | (_, _, true) => Doc.text("NaN") - | _ => Doc.text(string_of_float(f)) - }; - -let mk_BoolLit = b => Doc.text(string_of_bool(b)); - -let mk_Cons = (hd, tl) => Doc.(hcats([hd, text("::"), tl])); - -let mk_Pair = (doc1, doc2) => Doc.(hcats([doc1, text(", "), doc2])); - -let mk_Ap = (doc1, doc2) => Doc.hseps([doc1, doc2]); diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re b/src/haz3lweb/view/dhcode/layout/DHDoc_common.re deleted file mode 100644 index 8f3d5a2479..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_common.re +++ /dev/null @@ -1,139 +0,0 @@ -module Doc = Pretty.Doc; -open Haz3lcore; -open DHDoc; - -type formattable_child = (~enforce_inline: bool) => t; - -module P = Precedence; -let precedence_const = P.max; -let precedence_Ap = P.ap; -let precedence_Power = P.power; -let precedence_Not = P.not_; -let precedence_Times = P.mult; -let precedence_Divide = P.mult; -let precedence_Plus = P.plus; -let precedence_Minus = P.plus; -let precedence_Cons = P.cons; -let precedence_Equals = P.eqs; -let precedence_LessThan = P.eqs; -let precedence_GreaterThan = P.eqs; -let precedence_And = P.and_; -let precedence_Or = P.or_; -let precedence_Comma = P.prod; -let precedence_max = P.min; - -let pad_child = - ( - ~inline_padding as (l, r)=(Doc.empty(), Doc.empty()), - ~enforce_inline: bool, - child: formattable_child, - ) - : t => { - let inline_choice = Doc.hcats([l, child(~enforce_inline=true), r]); - let para_choice = - Doc.( - hcats([ - linebreak(), - indent_and_align(child(~enforce_inline=false)), - linebreak(), - ]) - ); - enforce_inline ? inline_choice : Doc.choice(inline_choice, para_choice); -}; - -module Delim = { - let mk = (delim_text: string): t => - Doc.text(delim_text) |> Doc.annot(DHAnnot.Delim); - - let empty_hole = (_env: ClosureEnvironment.t): t => { - let lbl = - //StringUtil.cat([string_of_int(u + 1), ":", string_of_int(i + 1)]); - "?"; - Doc.text(lbl) - |> Doc.annot(DHAnnot.HoleLabel) - |> Doc.annot(DHAnnot.Delim); - }; - - let list_nil = mk("[]"); - let triv = mk("()"); - let wild = mk("_"); - - let open_Parenthesized = mk("("); - let close_Parenthesized = mk(")"); - - let sym_Fun = mk("fun"); - let colon_Fun = mk(":"); - let arrow_Fun = mk("->"); - - let fix_FixF = mk("fix"); - - let arrow_FixF = mk("->"); - let colon_FixF = mk(":"); - - let open_Case = mk("case"); - let close_Case = mk("end"); - - let bar_Rule = mk("|"); - let arrow_Rule = mk("=>"); - - let open_Cast = mk("<"); - let arrow_Cast = mk(Unicode.castArrowSym); - let back_arrow_Cast = mk(Unicode.castBackArrowSym); - let close_Cast = mk(">"); - - let open_FailedCast = open_Cast |> Doc.annot(DHAnnot.FailedCastDelim); - let arrow_FailedCast = - mk(Unicode.castArrowSym) |> Doc.annot(DHAnnot.FailedCastDelim); - let close_FailedCast = close_Cast |> Doc.annot(DHAnnot.FailedCastDelim); -}; - -let mk_EmptyHole = (~selected=false, env: ClosureEnvironment.t) => - Delim.empty_hole(env) |> Doc.annot(DHAnnot.EmptyHole(selected, env)); - -let mk_InvalidText = t => Doc.text(t) |> Doc.annot(DHAnnot.Invalid); - -let mk_Sequence = (doc1, doc2) => Doc.(hcats([doc1, linebreak(), doc2])); - -let mk_IntLit = n => Doc.text(string_of_int(n)); - -let mk_StringLit = s => Doc.text(Form.string_quote(s)); - -let mk_Test = t => Doc.(hcats([text("Test"), t, text("End")])); - -let mk_FloatLit = (f: float) => - switch (f < 0., Float.is_infinite(f), Float.is_nan(f)) { - | (false, true, _) => Doc.text("Inf") /* TODO: NegInf is temporarily introduced until unary minus is introduced to Hazel */ - | (true, true, _) => Doc.text("NegInf") - | (_, _, true) => Doc.text("NaN") - | _ => Doc.text(string_of_float(f)) - }; - -let mk_BoolLit = b => Doc.text(string_of_bool(b)); - -let mk_ConstructorLit = Doc.text; - -let mk_Cons = (hd, tl) => Doc.(hcats([hd, text("::"), tl])); -let mk_ListConcat = (hd, tl) => Doc.(hcats([hd, text("@"), tl])); - -let mk_comma_seq = (ld, rd, l) => { - let rec mk_comma_seq_inner = l => { - switch (l) { - | [] => [] - | [hd] => [hd] - | [hd, ...tl] => Doc.([hd, text(", ")] @ mk_comma_seq_inner(tl)) - }; - }; - Doc.(hcats([text(ld)] @ mk_comma_seq_inner(l) @ [text(rd)])); -}; - -let mk_ListLit = l => mk_comma_seq("[", "]", l); - -let mk_Tuple = elts => mk_comma_seq("", "", elts); - -let mk_TypAp = (doc1, doc2) => - Doc.(hcats([doc1, text("@<"), doc2, text(">")])); - -let mk_Ap = (doc1, doc2) => - Doc.(hcats([doc1, text("("), doc2, text(")")])); - -let mk_rev_Ap = (doc1, doc2) => Doc.(hcats([doc1, text(" |> "), doc2])); diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei b/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei deleted file mode 100644 index c7d3af3622..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_common.rei +++ /dev/null @@ -1,97 +0,0 @@ -open Haz3lcore; - -type formattable_child = (~enforce_inline: bool) => DHDoc.t; - -let precedence_const: int; -let precedence_Ap: int; -let precedence_Times: int; -let precedence_Power: int; -let precedence_Divide: int; -let precedence_Plus: int; -let precedence_Minus: int; -let precedence_Not: int; -let precedence_Cons: int; -let precedence_Equals: int; -let precedence_LessThan: int; -let precedence_GreaterThan: int; -let precedence_And: int; -let precedence_Or: int; -let precedence_Comma: int; -let precedence_max: int; - -let pad_child: - ( - ~inline_padding: (Pretty.Doc.t(DHAnnot.t), Pretty.Doc.t(DHAnnot.t))=?, - ~enforce_inline: bool, - formattable_child - ) => - DHDoc.t; - -module Delim: { - let mk: string => DHDoc.t; - - let empty_hole: ClosureEnvironment.t => DHDoc.t; - - let list_nil: DHDoc.t; - let triv: DHDoc.t; - let wild: DHDoc.t; - - let open_Parenthesized: DHDoc.t; - let close_Parenthesized: DHDoc.t; - - let sym_Fun: DHDoc.t; - let colon_Fun: DHDoc.t; - let arrow_Fun: DHDoc.t; - - let fix_FixF: DHDoc.t; - let arrow_FixF: DHDoc.t; - let colon_FixF: DHDoc.t; - - let open_Case: DHDoc.t; - let close_Case: DHDoc.t; - - let bar_Rule: DHDoc.t; - let arrow_Rule: DHDoc.t; - - let open_Cast: DHDoc.t; - let arrow_Cast: DHDoc.t; - let back_arrow_Cast: DHDoc.t; - let close_Cast: DHDoc.t; - - let open_FailedCast: Pretty.Doc.t(DHAnnot.t); - let arrow_FailedCast: Pretty.Doc.t(DHAnnot.t); - let close_FailedCast: Pretty.Doc.t(DHAnnot.t); -}; - -let mk_EmptyHole: - (~selected: bool=?, ClosureEnvironment.t) => Pretty.Doc.t(DHAnnot.t); - -let mk_InvalidText: string => Pretty.Doc.t(DHAnnot.t); - -let mk_Sequence: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a); - -let mk_Test: Pretty.Doc.t('a) => Pretty.Doc.t('a); - -let mk_IntLit: int => Pretty.Doc.t('a); - -let mk_FloatLit: float => Pretty.Doc.t('a); - -let mk_BoolLit: bool => Pretty.Doc.t('a); - -let mk_ConstructorLit: string => Pretty.Doc.t('a); - -let mk_StringLit: string => Pretty.Doc.t('a); - -let mk_Cons: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a); - -let mk_ListConcat: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a); - -let mk_ListLit: list(Pretty.Doc.t('a)) => Pretty.Doc.t('a); - -let mk_Tuple: list(Pretty.Doc.t('a)) => Pretty.Doc.t('a); - -let mk_TypAp: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a); - -let mk_Ap: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a); - -let mk_rev_Ap: (Pretty.Doc.t('a), Pretty.Doc.t('a)) => Pretty.Doc.t('a); diff --git a/src/haz3lweb/view/dhcode/layout/DHLayout.re b/src/haz3lweb/view/dhcode/layout/DHLayout.re deleted file mode 100644 index 139dc52c36..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHLayout.re +++ /dev/null @@ -1,4 +0,0 @@ -open Pretty; - -[@deriving sexp] -type t = Layout.t(DHAnnot.t); diff --git a/src/haz3lweb/view/dhcode/layout/DHLayout.rei b/src/haz3lweb/view/dhcode/layout/DHLayout.rei deleted file mode 100644 index ae26af88da..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHLayout.rei +++ /dev/null @@ -1,2 +0,0 @@ -[@deriving sexp] -type t = Pretty.Layout.t(DHAnnot.t); diff --git a/src/haz3lweb/view/dhcode/layout/DHMeasuredLayout.re b/src/haz3lweb/view/dhcode/layout/DHMeasuredLayout.re deleted file mode 100644 index dd582ce455..0000000000 --- a/src/haz3lweb/view/dhcode/layout/DHMeasuredLayout.re +++ /dev/null @@ -1,7 +0,0 @@ -module MeasuredPosition = Pretty.MeasuredPosition; -module MeasuredLayout = Pretty.MeasuredLayout; - -[@deriving sexp] -type t = MeasuredLayout.t(DHAnnot.t); -type with_offset = MeasuredLayout.with_offset(DHAnnot.t); -include MeasuredLayout.Make(WeakMap); diff --git a/src/haz3lweb/view/dhcode/layout/HTypAnnot.re b/src/haz3lweb/view/dhcode/layout/HTypAnnot.re deleted file mode 100644 index a879bcafc7..0000000000 --- a/src/haz3lweb/view/dhcode/layout/HTypAnnot.re +++ /dev/null @@ -1,5 +0,0 @@ -type t = - | HoleLabel - | Delim - | Step(int) - | Term; diff --git a/src/haz3lweb/view/dhcode/layout/HTypAnnot.rei b/src/haz3lweb/view/dhcode/layout/HTypAnnot.rei deleted file mode 100644 index a879bcafc7..0000000000 --- a/src/haz3lweb/view/dhcode/layout/HTypAnnot.rei +++ /dev/null @@ -1,5 +0,0 @@ -type t = - | HoleLabel - | Delim - | Step(int) - | Term; diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re deleted file mode 100644 index 996d01f607..0000000000 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re +++ /dev/null @@ -1,183 +0,0 @@ -open Util; -open Haz3lcore; -module Doc = Pretty.Doc; - -type t = Doc.t(HTypAnnot.t); - -type formattable_child = (~enforce_inline: bool) => t; - -let precedence_Prod = 1; -let precedence_Arrow = 2; -let precedence_Sum = 3; -let precedence_Ap = 4; -let precedence_Const = 5; - -let precedence = (ty: Typ.t): int => - switch (Typ.term_of(ty)) { - | Int - | Float - | Bool - | String - | Unknown(_) - | Var(_) - | Forall(_) - | Rec(_) - | Sum(_) => precedence_Sum - | List(_) => precedence_Const - | Prod(_) => precedence_Prod - | Arrow(_, _) => precedence_Arrow - | Parens(_) => precedence_Const - | Ap(_) => precedence_Ap - }; - -let pad_child = - ( - ~inline_padding as (l, r)=(Doc.empty(), Doc.empty()), - ~enforce_inline: bool, - child: formattable_child, - ) - : t => { - let inline_choice = Doc.hcats([l, child(~enforce_inline=true), r]); - let para_choice = - Doc.( - hcats([ - linebreak(), - indent_and_align(child(~enforce_inline)), - linebreak(), - ]) - ); - enforce_inline ? inline_choice : Doc.choice(inline_choice, para_choice); -}; - -let mk_delim = s => Doc.(annot(HTypAnnot.Delim, text(s))); - -let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { - open Doc; - let mk' = mk(~enforce_inline); - let mk_right_associative_operands = (precedence_op, ty1, ty2) => ( - annot( - HTypAnnot.Step(0), - mk'(~parenthesize=precedence(ty1) <= precedence_op, ty1), - ), - annot( - HTypAnnot.Step(1), - mk'(~parenthesize=precedence(ty2) < precedence_op, ty2), - ), - ); - let (doc, parenthesize) = - switch (Typ.term_of(ty)) { - | Parens(ty) => (mk(~parenthesize=true, ~enforce_inline, ty), false) - | Unknown(_) => ( - annot(HTypAnnot.Delim, annot(HTypAnnot.HoleLabel, text("?"))), - parenthesize, - ) - | Int => (text("Int"), parenthesize) - | Float => (text("Float"), parenthesize) - | Bool => (text("Bool"), parenthesize) - | String => (text("String"), parenthesize) - | Var(name) => (text(name), parenthesize) - | List(ty) => ( - hcats([ - mk_delim("["), - ( - (~enforce_inline) => - annot(HTypAnnot.Step(0), mk(~enforce_inline, ty)) - ) - |> pad_child(~enforce_inline), - mk_delim("]"), - ]), - parenthesize, - ) - | Arrow(ty1, ty2) => - let (d1, d2) = - mk_right_associative_operands(precedence_Arrow, ty1, ty2); - ( - hcats([ - d1, - hcats([ - choices([linebreak(), space()]), - text(Unicode.typeArrowSym ++ " "), - ]), - d2, - ]), - parenthesize, - ); - | Prod([]) => (text("()"), parenthesize) - | Prod([head, ...tail]) => - let center = - [ - annot( - HTypAnnot.Step(0), - mk'(~parenthesize=precedence(head) <= precedence_Prod, head), - ), - ...List.mapi( - (i, ty) => - annot( - HTypAnnot.Step(i + 1), - mk'(~parenthesize=precedence(ty) <= precedence_Prod, ty), - ), - tail, - ), - ] - |> ListUtil.join( - hcats([text(","), choices([linebreak(), space()])]), - ) - |> hcats; - (center, true); - | Rec(name, ty) => ( - hcats([ - text("rec " ++ Type.tpat_view(name) ++ "->{"), - ( - (~enforce_inline) => - annot(HTypAnnot.Step(0), mk(~enforce_inline, ty)) - ) - |> pad_child(~enforce_inline), - mk_delim("}"), - ]), - parenthesize, - ) - | Forall(name, ty) => ( - hcats([ - text("forall " ++ Type.tpat_view(name) ++ "->{"), - ( - (~enforce_inline) => - annot(HTypAnnot.Step(0), mk(~enforce_inline, ty)) - ) - |> pad_child(~enforce_inline), - mk_delim("}"), - ]), - parenthesize, - ) - | Sum(sum_map) => - let center = - List.mapi( - (i, vr) => { - ConstructorMap.( - switch (vr) { - | Variant(ctr, _, None) => - annot(HTypAnnot.Step(i + 1), text(ctr)) - | Variant(ctr, _, Some(ty)) => - annot( - HTypAnnot.Step(i + 1), - hcats([text(ctr ++ "("), mk'(ty), text(")")]), - ) - | BadEntry(ty) => - annot(HTypAnnot.Step(i + 1), hcats([mk'(ty)])) - } - ) - }, - sum_map, - ) - |> ListUtil.join( - hcats([text(" +"), choices([linebreak(), space()])]), - ) - |> hcats; - (center, true); - | Ap(t1, t2) => ( - hcats([mk'(t1), text("("), mk'(t2), text(")")]), - parenthesize, - ) - }; - let doc = annot(HTypAnnot.Term, doc); - parenthesize ? Doc.hcats([mk_delim("("), doc, mk_delim(")")]) : doc; -}; diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.rei b/src/haz3lweb/view/dhcode/layout/HTypDoc.rei deleted file mode 100644 index ab07b0e81e..0000000000 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.rei +++ /dev/null @@ -1,5 +0,0 @@ -open Haz3lcore; - -type t = Pretty.Doc.t(HTypAnnot.t); - -let mk: (~parenthesize: bool=?, ~enforce_inline: bool, Typ.t) => t;