Skip to content

Commit 5c4fcb2

Browse files
committed
Rip out probes on types
1 parent 14c1ed0 commit 5c4fcb2

File tree

12 files changed

+153
-323
lines changed

12 files changed

+153
-323
lines changed

src/haz3lcore/ProbePerform.re

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -87,13 +87,12 @@ let rec target_subterm_ids = (id: Id.t, info_map: Statics.Map.t) =>
8787
]
8888
| _ => [id]
8989
}
90-
/* Filter out terms that can't meaningfully be probed (type patterns, labels, etc.) */
90+
/* Filter out terms that can't meaningfully be probed */
9191
| info when !Info.is_typable_term(info) => []
9292
/* Default: use rep_id for expressions and patterns to handle multi-tile forms
9393
(tuples, list literals, case expressions) where non-representative tile IDs
9494
would otherwise cause probe_map/evaluator ID mismatch */
9595
| Some(InfoExp({term, _})) => [IdTagged.rep_id(term)]
96-
| Some(InfoTyp({term, _})) => [IdTagged.rep_id(term)]
9796
| Some(InfoPat({term, _})) => [Pat.rep_id(term)]
9897
| _ => [id]
9998
};
@@ -530,10 +529,9 @@ let rm_probes_in_selection =
530529
);
531530
};
532531

533-
/* Check if type annotation is allowed for the given id.
534-
Uses target_subterm_ids to support types (which redirect to their parent expressions). */
532+
/* Check if type annotation is allowed for the given id. */
535533
let can_statics = (id: Id.t, info_map: Statics.Map.t): bool =>
536-
target_subterm_ids(id, info_map) != [];
534+
Info.is_typable_term(Statics.Map.lookup(id, info_map));
537535

538536
/* Toggle type annotation on the indicated term.
539537
Unlike probes, type annotations don't support auto mode or pins. */

src/haz3lcore/projectors/implementations/ProbeProj.re

Lines changed: 8 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -833,9 +833,12 @@ let move_cursor =
833833
/* Cursor would be outside window, reset to next visible sample */
834834
| Some(idx) =>
835835
let next_idx_maybe = idx - offset;
836-
switch (List.nth_opt(samples, next_idx_maybe)) {
837-
| Some(sample) => parent(SampleCursor(Capture(sample, ap_id)))
838-
| None => Effect.Ignore
836+
if (next_idx_maybe >= 0 && next_idx_maybe < List.length(samples)) {
837+
parent(
838+
SampleCursor(Capture(List.nth(samples, next_idx_maybe), ap_id)),
839+
);
840+
} else {
841+
Effect.Ignore;
839842
};
840843
| _ => Effect.Ignore
841844
};
@@ -1170,7 +1173,6 @@ module M: Projector = {
11701173
| Exp(_)
11711174
| Pat(_) => Some()
11721175
| Any(_) => Some() /* Grout don't have sorts rn */
1173-
| Typ(_) => Some()
11741176
| _ => None
11751177
};
11761178

@@ -1189,16 +1191,8 @@ module M: Projector = {
11891191
let view = ({info, local, parent, view_seg, _}: View.args(model, action)) => {
11901192
let settings = Settings.s^;
11911193
/* Wrap view_seg to fix single_line=true for all probe displays */
1192-
let view_seg_single_line =
1193-
(~background=?, ~text_only: option(bool)=?, sort, segment) =>
1194-
view_seg(
1195-
~single_line=true,
1196-
~background?,
1197-
~text_only?,
1198-
~is_dynamic=?None,
1199-
sort,
1200-
segment,
1201-
);
1194+
let view_seg_single_line = (~background=?, ~text_only=?, sort, segment) =>
1195+
view_seg(~single_line=true, ~background?, ~text_only?, sort, segment);
12021196
View.{
12031197
inline: Node.div([]),
12041198
overlay: Some(overlay_view(info)),

src/haz3lcore/projectors/implementations/TypeProj.re

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ let self_ty = (info: option(Info.t)): option(Typ.t) =>
1515
switch (info) {
1616
| Some(InfoExp({self, _})) => Self.typ_of_exp(self)
1717
| Some(InfoPat({self, _})) => Self.typ_of_pat(self)
18-
| Some(InfoTyp({term, _})) => Some(term)
1918
| _ => None
2019
};
2120

0 commit comments

Comments
 (0)