Skip to content
Open
Show file tree
Hide file tree
Changes from 83 commits
Commits
Show all changes
94 commits
Select commit Hold shift + click to select a range
9222c73
Add DataFrame projector and related styles
7h3kk1d May 30, 2025
2954934
Abbreviate data in dataframes
7h3kk1d May 30, 2025
9d82322
Remove debug statements and fix build
7h3kk1d May 30, 2025
0fedf62
Remove commented-out color
7h3kk1d May 30, 2025
def7f47
Improve dynamic sizing of DataFrameProj
7h3kk1d May 30, 2025
870aa80
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jun 10, 2025
cbada86
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jun 11, 2025
99f44f2
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jun 11, 2025
001dbf5
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jun 12, 2025
53a9ce1
Merge remote-tracking branch 'origin/dataframe-projection' into dataf…
7h3kk1d Jun 13, 2025
07ffd37
Fix compilation
7h3kk1d Jun 13, 2025
173c4bd
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jun 23, 2025
5c85f9f
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jul 3, 2025
66c5794
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jul 3, 2025
99822a3
Fix: update abbreviation function to use strip_ascriptions instead of…
7h3kk1d Jul 3, 2025
fa4a07f
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jul 10, 2025
65bebf0
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jul 10, 2025
9d13288
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jul 16, 2025
bd4b665
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Jul 16, 2025
1295678
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Aug 1, 2025
8810c15
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Aug 1, 2025
accd35b
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Aug 4, 2025
b7cf243
for table projector
7h3kk1d Aug 5, 2025
a52715b
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Aug 6, 2025
9c4a797
Rename DataFrame to Table
7h3kk1d Aug 6, 2025
e876a01
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Aug 11, 2025
7c38c6b
Project tables in evaluation output
7h3kk1d Aug 11, 2025
aefdcf1
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Aug 18, 2025
98ddf77
Merge branch 'dataframe-projection' into dataframe-projector
7h3kk1d Aug 20, 2025
ea3f127
Merge branch 'dev' into dataframe-projector
7h3kk1d Aug 20, 2025
223262e
Merge branch 'dev' into dataframe-projector
7h3kk1d Aug 21, 2025
934a224
Merge branch 'dev' into dataframe-projector
7h3kk1d Aug 25, 2025
a833ece
Merge branch 'dev' into dataframe-projector
7h3kk1d Aug 28, 2025
5d504e8
Merge branch 'dev' into dataframe-projector
7h3kk1d Aug 29, 2025
c534142
Merge branch 'dev' into dataframe-projector
7h3kk1d Sep 3, 2025
ff267b2
Merge branch 'dev' into dataframe-projector
7h3kk1d Sep 10, 2025
04d9070
Merge branch 'dev' into dataframe-projector
7h3kk1d Sep 11, 2025
b0c6ac6
Merge branch 'dev' into dataframe-projector
7h3kk1d Sep 18, 2025
fe6096b
Beginning table projector dynamics
7h3kk1d Sep 19, 2025
b7e35f6
worst closure selector
7h3kk1d Sep 19, 2025
4007565
Add closure navigation buttons to table header
7h3kk1d Sep 19, 2025
490d757
add column drop to table probe projector
7h3kk1d Sep 19, 2025
3ba2a2b
Add column menu with options for dropping, renaming, and rearranging …
7h3kk1d Sep 22, 2025
f03b6df
Add close menu functionality to column menu actions
7h3kk1d Sep 22, 2025
80bb634
Mark params unused
7h3kk1d Sep 22, 2025
e8a2ec2
parse fields
7h3kk1d Sep 22, 2025
2b53b53
Submenu
7h3kk1d Sep 22, 2025
cb9c590
awaiting type hole inference
7h3kk1d Sep 22, 2025
6eba36a
parse to convert
7h3kk1d Sep 22, 2025
9882413
Add conversion functions for column types in TableProbe
7h3kk1d Sep 22, 2025
75b346c
Add comparison functions for int, float, sint, and nat types
7h3kk1d Sep 22, 2025
3b85132
Add sorting functionality for columns in TableProbe
7h3kk1d Sep 22, 2025
f02e1eb
Refactor column conversion functions to a single generic function
7h3kk1d Sep 22, 2025
e8db220
Update TableProbe name formatting
7h3kk1d Sep 22, 2025
d52e32e
Add column movement functionality
7h3kk1d Sep 22, 2025
fc76bd3
Refactor move_column function to accept dynamic type as a parameter
7h3kk1d Sep 22, 2025
dc96367
Refactor column movement logic to use a dedicated can_move_column fun…
7h3kk1d Sep 23, 2025
4fe6c68
dry
7h3kk1d Sep 23, 2025
24d073e
fix conversion functions
7h3kk1d Sep 23, 2025
fe1ba4e
Refactor conversion logic to use a dedicated conversion_functions fun…
7h3kk1d Sep 23, 2025
4051a0c
Refactor conversion functions to return tuples of display names and f…
7h3kk1d Sep 23, 2025
0303815
Cleanup
7h3kk1d Sep 23, 2025
eae4c3d
Add newline for reverse function ap
7h3kk1d Sep 23, 2025
0d2298d
Stop folding functions in projector syntax
7h3kk1d Sep 23, 2025
a9c29f4
More actions
7h3kk1d Sep 23, 2025
7f7b563
Fix exp to segment for reverse ap
7h3kk1d Sep 23, 2025
480f861
add helper functions for pipelining
7h3kk1d Sep 24, 2025
509bc31
Implement rename_column with prompt for now
7h3kk1d Sep 24, 2025
ea614f2
Switch get_dynamic_type to only get a single closures type
7h3kk1d Sep 24, 2025
bfb3a0a
spaces in projector names don't work
7h3kk1d Sep 24, 2025
3017e0e
Merge branch 'dev' into dataframe-projector
7h3kk1d Sep 29, 2025
89cf729
Merge remote-tracking branch 'origin/dev' into dataframe-projector
7h3kk1d Oct 6, 2025
6b575cd
Merge branch 'dev' into dataframe-projector
7h3kk1d Oct 17, 2025
fa730f8
Fix compilation
7h3kk1d Oct 17, 2025
90b2f6b
Merge branch 'dev' into dataframe-projector
7h3kk1d Oct 21, 2025
9bf045e
Merge branch 'dev' into dataframe-projector
7h3kk1d Oct 23, 2025
f4b005e
Merge branch 'dev' into dataframe-projector
7h3kk1d Nov 21, 2025
9021ccf
Merge remote-tracking branch 'origin/dev' into dataframe-projector
7h3kk1d Feb 4, 2026
75542da
Remove debug print statements from ExpToSegment and TableProj
7h3kk1d Feb 4, 2026
16f615d
Refactor project_table_if to remove unnecessary braces
7h3kk1d Feb 4, 2026
a95720c
Merge remote-tracking branch 'origin/dev' into dataframe-projector
7h3kk1d Feb 5, 2026
dd2ce82
Add Table to livelit projectors list
7h3kk1d Feb 5, 2026
0908972
Merge branch 'dev' into dataframe-projector
7h3kk1d Feb 6, 2026
c9a5754
Remove debug print statements from exp_to_pretty function
7h3kk1d Feb 10, 2026
28f2877
Fix error message in project_table_if function
7h3kk1d Feb 10, 2026
71a7cd5
Refactor extract_labeled_tuple_entries and table_of functionsto not u…
7h3kk1d Feb 10, 2026
afabba7
Use table projector in tables doc slide
7h3kk1d Feb 10, 2026
d56a5f2
Remove unused key_handler function from TableProj.re
7h3kk1d Feb 10, 2026
77a37b3
Update table styles and color variables for improved contrast
7h3kk1d Feb 10, 2026
0d6b44e
Remove unused code
7h3kk1d Feb 10, 2026
a65d591
Table styles
7h3kk1d Feb 11, 2026
78918c5
Merge branch 'dev' into dataframe-projector
7h3kk1d Feb 11, 2026
c87a990
Fix error message in get function for table retrieval
7h3kk1d Feb 11, 2026
698d3ee
Merge branch 'dev' into dataframe-projector
7h3kk1d Feb 11, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/CLI/Print.re
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ let exp_to_segment_settings: ExpToSegment.Settings.t = {
label_format: QuoteWhenNecessary,
inline: false,
fold_case_clauses: false,
project_tables: false,
fold_fn_bodies: `NoFold,
hide_fixpoints: false,
show_filters: true,
Expand Down
25 changes: 22 additions & 3 deletions src/haz3lcore/pretty/ExpToSegment.re
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ module Settings = {
| `Text
| `NoFold
],
project_tables: bool,
hide_fixpoints: bool,
show_filters: bool,
show_unknown_as_hole: bool,
Expand All @@ -51,6 +52,7 @@ module Settings = {
label_format: QuoteWhenNecessary,
inline,
fold_case_clauses: !settings.evaluation.show_case_clauses,
project_tables: settings.evaluation.project_tables,
fold_fn_bodies:
fold_fn_bodies
|> Option.value(
Expand All @@ -68,6 +70,7 @@ module Settings = {
label_format: QuoteWhenNecessary,
inline,
fold_case_clauses: false,
project_tables: false,
fold_fn_bodies: `NoFold,
hide_fixpoints: false,
show_filters: true,
Expand Down Expand Up @@ -470,8 +473,8 @@ let rec parenthesize =
| Ap(Reverse, e1, e2) =>
Ap(
Reverse,
parenthesize(e1) |> paren_assoc_at(Precedence.eqs),
parenthesize(e2) |> paren_at(Precedence.eqs),
parenthesize(e1) |> paren_at(Precedence.eqs), // Associativity is backwards because e2 goes before e1
parenthesize(e2) |> paren_assoc_at(Precedence.eqs),
)
|> rewrap
| TypAp(e, tp) =>
Expand Down Expand Up @@ -1056,6 +1059,15 @@ let fold_fun_if = (condition, f_name: string, pieces, exp) =>
| `NoFold => pieces
};

let project_table_if = (should_project, pieces) =>
if (should_project) {
switch (MakeTerm.for_projection([pieces])) {
| None => failwith("ExpToSegment.fold_if")
| Some(any) => [ProjectorInit.init_or_noop(Table, pieces, any)]
};
} else {
[pieces];
};
/* We assume that parentheses have already been added as necessary, and
that the expression has no Closures or DynamicErrorHoles
*/
Expand Down Expand Up @@ -1157,7 +1169,10 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
),
],
);
wrap(exp, p_just([form(x, xs)]));
wrap(
exp,
p_just(form(x, xs) |> project_table_if(settings.project_tables)),
);
// TODO: Add optional newlines
| Var(v) => wrap(exp, text_to_pretty(exp |> Exp.rep_id, Sort.Exp, v))
| BinOp(op, l, r) =>
Expand Down Expand Up @@ -1433,13 +1448,17 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
and+ e2 = go(e2);
wrap(exp, e1 @ [mk_form(ApExp, id, [e2])]);
| Ap(Reverse, e1, e2) =>
print_endline("Printing reverse application");
print_endline(Exp.show(exp));
// TODO: Add optional newlines
let id = exp |> Exp.rep_id;
let+ e1 = go(e1)
and+ e2 = go(e2);

wrap(
exp,
e2
@ (settings.inline ? [] : [Secondary(mk_newline(Id.mk()))])
@ [
Tile({
id,
Expand Down
1 change: 1 addition & 0 deletions src/haz3lcore/projectors/ProjectorInfo.re
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ let utility: ProjectorBase.utility = {
~settings={
...ExpToSegment.Settings.of_core(~inline=true, CoreSettings.off),
show_unknown_as_hole: false,
fold_fn_bodies: `NoFold,
},
);
let lift_syntax =
Expand Down
1 change: 1 addition & 0 deletions src/haz3lcore/projectors/ProjectorInit.re
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ let to_module = (kind: ProjectorCore.Kind.t): (module Cooked) =>
| TextArea => (module Cook(TextAreaProj.M))
| Livelit => (module Cook(LivelitProj.M))
| Card => (module Cook(CardProj.M))
| Table => (module Cook(TableProj.M))
| Csv => (module Cook(CSVProjector.M))
};

Expand Down
228 changes: 228 additions & 0 deletions src/haz3lcore/projectors/implementations/TableProj.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,228 @@
open Util;
open Virtual_dom.Vdom;
open ProjectorBase;
open Language;

let max_column_length = 12;

let table_of =
(any: Any.t): option((list(LabeledTuple.label), list(list(Exp.t)))) =>
switch (any) {
| Exp({term: ListLit(es), _}) =>
let data: list(option((list(string), list(TermBase.exp_t)))) =
List.map(
e => {
switch (Unboxing.unbox(LabeledTupleEntries, e)) {
// TODO Stop doing this with unboxing and deconstruct it here with the parens
| IndetMatch => None
| DoesNotMatch => None
| Matches(entries: list((option(string), TermBase.exp_t))) =>
let f: option(list((string, TermBase.exp_t))) =
OptUtil.sequence(
List.map(
((label, value)) =>
switch (label) {
| Some(l) => Some((l, value))
| None => None
},
entries,
),
);

let g: option((list(string), list(TermBase.exp_t))) =
f |> Option.map(List.split);

g;
}
},
es,
);

let data: option(list((list(string), list(TermBase.exp_t)))) =
OptUtil.sequence(data);
switch (data) {
| Some(data: list((list(string), list(TermBase.exp_t)))) =>
let (headers: list(list(string)), rows: list(list(TermBase.exp_t))) =
List.split(data);

// If all the headers aren't the same return None
switch (headers) {
| [] => None
| [h, ..._] when List.for_all(x => x == h, headers) =>
let headers = h;
Some((headers, rows));

| _ => None
};
| None => None
};
| _ => None
};

let get = (info: info): (list(LabeledTuple.label), list(list(Exp.t))) =>
switch (info.syntax |> info.utility.seg_to_term) {
| Some(s) =>
switch (table_of(s)) {
| Some(s) => s
| None => failwith("TextArea: get: Not a table")
}
| None => failwith("TextArea: get: Not a table")
};

let key_handler = (id, ~parent, evt) => {
open Effect;
let key = Key.mk(KeyDown, evt);

switch (key.key) {
| D("ArrowRight" | "ArrowDown")
when WebUtil.TextArea.is_last_pos(Id.cls(id)) =>
JsUtil.get_elem_by_id(Id.cls(id))##blur;
Many([parent(Escape(Right)), Stop_propagation]);
| D("ArrowLeft" | "ArrowUp")
when WebUtil.TextArea.is_first_pos(Id.cls(id)) =>
JsUtil.get_elem_by_id(Id.cls(id))##blur;
Many([parent(Escape(Left)), Stop_propagation]);
/* Defer to parent editor undo for now */
| D("z" | "Z" | "y" | "Y") when Key.ctrl_held(evt) || Key.meta_held(evt) =>
Many([Prevent_default])
| D("z" | "Z")
when Key.shift_held(evt) && (Key.ctrl_held(evt) || Key.meta_held(evt)) =>
Many([Prevent_default])
| D("\"") =>
/* Hide quotes from both the textarea and parent editor */
Many([Prevent_default, Stop_propagation])
| _ => Stop_propagation
};
};

let len_seg = (utility: utility, seg: Segment.t): int =>
seg |> utility.seg_to_string |> String.length;

let seg_of_exp = (utility: utility, exp: Exp.t): (Segment.t, int) => {
let seg = utility.term_to_seg(Exp(exp));
(seg, len_seg(utility, seg));
};

let abbreviated_seg_of =
(utility: utility, available: int, exp: Exp.t): (Segment.t, int) => {
let (abbr_exp, _length) =
exp |> DHExp.strip_ascriptions |> Abbreviate.abbreviate_exp(~available);
seg_of_exp(utility, abbr_exp);
};
let length_cls = (length: int): string =>
if (length > 10) {
"extra";
} else if (length > 9) {
"s6";
} else if (length > 8) {
"s5";
} else if (length > 7) {
"s4";
} else if (length > 6) {
"s3";
} else if (length > 5) {
"s2";
} else if (length > 4) {
"s1";
} else {
"s0";
};
let value_view = (_info: info, utility: utility, view_seg, exp) => {
let (seg, length) = abbreviated_seg_of(utility, max_column_length, exp);

Node.div(
~attrs=[
//Attr.title(DynCursor.Debug.str(info, closure)),
Attr.classes([
"value",
length_cls(length),
// @ DynCursor.clss(info, closure)
// @ (Option.is_some(cur_ap(info)) ? ["ap"] : [])
// @ (!is_value(closure.value) ? ["indet"] : []),
]),
// Attr.on_double_click(_ => local(ToggleShowAllVals(index))),
// Attr.on_pointerdown(val_pointerdown),
// Attr.on_pointerup(val_pointerup),
// Attr.on_mousemove(val_mousemove),
],
[view_seg(Sort.Exp, seg)],
);
};

let table =
(
info,
~parent as _: external_action => Ui_effect.t(unit),
(headers, rows): (list(LabeledTuple.label), list(list(Exp.t))),
~view_seg: (Sort.t, Segment.t) => Node.t,
) =>
Node.table(
~attrs=[Attr.classes(["table"])],
[
Node.thead([
Node.tr(List.map(h => Node.th([Node.text(h)]), headers)),
]),
Node.tbody(
List.map(
row =>
Node.tr(
List.map(
e => Node.td([value_view(info, info.utility, view_seg, e)]),
row,
),
),
rows,
),
),
],
);

module M: Projector = {
[@deriving (show({with_path: false}), sexp, yojson)]
type model = unit;
[@deriving (show({with_path: false}), sexp, yojson)]
type action = unit;

let init = (any: Any.t) =>
switch (table_of(any)) {
| Some(_) => Some()
| None => None
};

let focusable =
Focusable.{
pointer: None,
keyboard: None,
};
let dynamics = false;
let placeholder = (_, info) => {
let (header, rows): (list(string), list(list(TermBase.exp_t))) =
info |> get;
let max_header_length =
header |> List.map(String.length) |> List.fold_left((+), 0);
let max_row_length =
rows
|> List.map(row =>
row
|> List.map(e =>
Abbreviate.abbreviate_exp(~available=max_column_length, e)
|> snd
)
|> List.fold_left((+), 0, _)
)
|> List.fold_left(max, 0, _);
let max_length = max(max_header_length, max_row_length);

let num_rows = List.length(rows);
let num_cols = List.length(header);
ProjectorCore.Shape.{
vertical: Block(min(num_rows + 1, 10)), // +1 for header row
/* +2 for left and right padding */
horizontal: 4 + max_length * 1 + num_cols * 2 // +2 for left and right padding
};
};
let update = (model, _, _) => model;

let view = ({info, parent, view_seg, _}: View.args(model, action)): View.t =>
View.mk(table(info, ~view_seg, ~parent, info |> get));
};
1 change: 1 addition & 0 deletions src/haz3lcore/zipper/action/Introduce.re
Original file line number Diff line number Diff line change
Expand Up @@ -245,6 +245,7 @@ module Make =
label_format: QuoteWhenNecessary,
inline: true,
fold_case_clauses: false,
project_tables: false,
fold_fn_bodies: `NoFold,
hide_fixpoints: false,
show_filters: true,
Expand Down
2 changes: 2 additions & 0 deletions src/language/CoreSettings.re
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ module Evaluation = {
show_case_steps: bool,
show_lookup_steps: bool,
show_stepper_filters: bool,
project_tables: bool,
// TODO[Matt]: Move this to somewhere where it is a per-scratch setting
stepper_history: bool,
show_settings: bool,
Expand All @@ -25,6 +26,7 @@ module Evaluation = {
show_case_steps: false,
show_lookup_steps: false,
show_stepper_filters: false,
project_tables: false,
stepper_history: false,
show_settings: false,
show_hidden_steps: false,
Expand Down
4 changes: 4 additions & 0 deletions src/language/ProjectorKind.re
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ type t =
| Card
| Livelit
| TextArea
| Table
| Csv;

let livelit_projectors: list(t) = [
Expand All @@ -27,6 +28,7 @@ let livelit_projectors: list(t) = [
TextArea,
Card,
Livelit,
Table,
];

/* Note: Probe intentionally excluded - probes use separate action path */
Expand All @@ -51,6 +53,7 @@ let name = (p: t): string =>
| Livelit => "livelit"
| TextArea => "text"
| Csv => "csv"
| Table => "table"
};

/* This must be updated and kept 1-to-1 with the above
Expand All @@ -68,6 +71,7 @@ let of_name = (p: string): t =>
| "livelit" => Livelit
| "card" => Card
| "csv" => Csv
| "table" => Table
| _ => failwith("Unknown projector kind")
};

Expand Down
Loading