Skip to content

Commit 9e95987

Browse files
authored
Evaluator streaming (#2339)
2 parents e879aca + 9da202b commit 9e95987

68 files changed

Lines changed: 11900 additions & 1763 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.changetours/2339-evaluator-streaming.changetour.md

Lines changed: 8187 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

.gitattributes

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ src/web/exercises/**/*.ml linguist-generated
1313
hazel.opam linguist-generated
1414
hazel.opam.locked linguist-generated
1515
package-lock.json linguist-generated
16+
.changetours/** linguist-generated
1617

1718
*.md linguist-documentation
1819
docs/** linguist-documentation

src/CLI/Grade.re

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ let gen_code_grading_report = (exercise): report => {
7777
);
7878
switch (evaluated) {
7979
| StepLimitExceeded => None
80-
| Completed((_, evaluated)) =>
80+
| LimitedCompleted((_, evaluated)) =>
8181
evaluated
8282
|> EvaluatorState.get_tests
8383
|> TestResults.mk_results

src/CLI/Run.re

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,12 +19,17 @@ let evaluate = (exp: Exp.t): Exp.t => {
1919
};
2020

2121
let evaluate_incremental =
22-
(~prev: IncrEval.t=IncrEval.empty, exp: Exp.t): (Exp.t, IncrEval.t) => {
22+
(~prev: EvaluatorState.incr_eval=IncrEval.empty, exp: Exp.t)
23+
: (Exp.t, EvaluatorState.incr_eval) => {
2324
let (info_map, elab) = statics_and_elab(exp);
24-
let info_map =
25-
EvalInfoMap.of_info_map(~probe_all=CoreSettings.on.probe_all, info_map);
25+
let eval_info =
26+
EvalInfo.of_info_map(
27+
~probe_all=CoreSettings.on.probe_all,
28+
~targets=Id.Map.empty,
29+
info_map,
30+
);
2631
let (result, state) =
27-
Evaluator.evaluate(~prev, ~info_map, ~env=Builtins.env_init, elab);
32+
Evaluator.evaluate(~prev, ~eval_info, ~env=Builtins.env_init, elab);
2833
(result, state.incr_eval);
2934
};
3035

@@ -43,7 +48,7 @@ let evaluate_with_probe_map =
4348
let elaborated = elaborate(exp);
4449
let (result, state) =
4550
Evaluator.evaluate(
46-
~targets=sample_map,
51+
~eval_info=EvalInfo.of_targets(sample_map),
4752
~env=Builtins.env_init,
4853
elaborated,
4954
);

src/haz3lcore/ProbePerform.re

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -734,7 +734,7 @@ let is_jump_target = (info_map: Statics.Map.t, z: Zipper.t): option(Id.t) => {
734734
let step_into_call_stack =
735735
(
736736
~syntax: CachedSyntax.t,
737-
~call_stack: Sample.call_stack,
737+
~call_stack: CallStack.t,
738738
~ap_id: Id.t,
739739
info_map: Statics.Map.t,
740740
z: Zipper.t,
@@ -780,14 +780,7 @@ let step_into_call_stack =
780780
};
781781

782782
/* Set pin and dyn cursor using the call_stack */
783-
let new_stack: Sample.call_stack = [
784-
{
785-
id: ap_id,
786-
name: None,
787-
fn_def_id: None,
788-
},
789-
...call_stack,
790-
];
783+
let new_stack = CallStack.extend(ap_id, call_stack);
791784

792785
/* Determine where to jump and where to look for samples.
793786
* For function literals:

src/haz3lcore/derived/Indentation.re

Lines changed: 37 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -9,23 +9,23 @@ let trim_non_content: Segment.t => Segment.t =
99

1010
let prev_pieces = (seg: Segment.t): list(option(Piece.t)) => {
1111
let rec go =
12-
(xs: list(Piece.t), prev: option(Piece.t))
12+
(acc, xs: list(Piece.t), prev: option(Piece.t))
1313
: list(option(Piece.t)) =>
1414
switch (xs) {
15-
| [] => []
16-
| [x, ...xs] => [prev, ...go(xs, Some(x))]
15+
| [] => List.rev(acc)
16+
| [x, ...xs] => go([prev, ...acc], xs, Some(x))
1717
};
18-
go(seg, None);
18+
go([], seg, None);
1919
};
2020

2121
let next_pieces = (seg: Segment.t): list(option(Piece.t)) => {
22-
let rec go = (xs: list(Piece.t)): list(option(Piece.t)) =>
22+
let rec go = (acc, xs: list(Piece.t)): list(option(Piece.t)) =>
2323
switch (xs) {
24-
| [] => []
25-
| [_] => [None]
26-
| [_, next, ...rest] => [Some(next), ...go([next, ...rest])]
24+
| [] => List.rev(acc)
25+
| [_] => List.rev([None, ...acc])
26+
| [_, next, ...rest] => go([Some(next), ...acc], [next, ...rest])
2727
};
28-
go(seg);
28+
go([], seg);
2929
};
3030

3131
let union_all =
@@ -35,20 +35,27 @@ let union_all =
3535
);
3636

3737
/* This does not strictly 'complete' a segment but rather does a
38-
* rough version of it that suffices for indentation calculation */
39-
let rec shallow_complete_segment = (seg: Segment.t): Segment.t =>
40-
switch (seg) {
41-
| [] => []
42-
| [Tile(t), ...rest] when !Tile.is_complete(t) => [
43-
Tile({
44-
...t,
45-
shards: List.init(List.length(t.label), i => i),
46-
children: t.children @ [shallow_complete_segment(rest)],
47-
/* Note: Potentially wrong number of children */
48-
}),
49-
]
50-
| [p, ...rest] => [p, ...shallow_complete_segment(rest)]
51-
};
38+
* rough version of it that suffices for indentation calculation.
39+
* Tail-recursive in segment length (recursion depth is bounded by
40+
* the number of incomplete tiles, not the number of pieces). */
41+
let rec shallow_complete_segment = (seg: Segment.t): Segment.t => {
42+
let rec go = (acc, seg: Segment.t): Segment.t =>
43+
switch (seg) {
44+
| [] => List.rev(acc)
45+
| [Tile(t), ...rest] when !Tile.is_complete(t) =>
46+
List.rev([
47+
Piece.Tile({
48+
...t,
49+
shards: List.init(List.length(t.label), i => i),
50+
children: t.children @ [shallow_complete_segment(rest)],
51+
/* Note: Potentially wrong number of children */
52+
}),
53+
...acc,
54+
])
55+
| [p, ...rest] => go([p, ...acc], rest)
56+
};
57+
go([], seg);
58+
};
5259

5360
/* Find the shortest prefix of the segment containing all incomplete tiles
5461
* followed by two consecutive linebreaks (aka a blank line) */
@@ -174,9 +181,13 @@ let rec go' = ((not_top, base: int, seg: Segment.t)) => {
174181
},
175182
(base, Id.Map.empty),
176183
complete_trimmed_seg,
177-
List.combine(
178-
prev_pieces(complete_trimmed_seg),
179-
next_pieces(complete_trimmed_seg),
184+
/* stack-safe zip (List.combine is not tail-recursive) */
185+
List.rev(
186+
List.rev_map2(
187+
(prev, next) => (prev, next),
188+
prev_pieces(complete_trimmed_seg),
189+
next_pieces(complete_trimmed_seg),
190+
),
180191
),
181192
);
182193
map;

0 commit comments

Comments
 (0)