Skip to content

Commit

Permalink
Stepper printing bugs
Browse files Browse the repository at this point in the history
  • Loading branch information
Negabinary committed Nov 21, 2024
1 parent 5d0629d commit 7eb9fa5
Show file tree
Hide file tree
Showing 3 changed files with 34 additions and 5 deletions.
22 changes: 21 additions & 1 deletion src/haz3lcore/pretty/ExpToSegment.re
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,11 @@ let should_add_space = (s1, s2) =>
| _ when String.starts_with(s2, ~prefix=" ") => false
| _ when String.ends_with(s1, ~suffix="\n") => false
| _ when String.starts_with(s2, ~prefix="\n") => false
| _
when
String.ends_with(s1, ~suffix="PROJECTOR")
&& String.starts_with(s2, ~prefix="(") =>
false
| _
when
String.ends_with(s1, ~suffix=")")
Expand Down Expand Up @@ -214,7 +219,22 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
let id = exp |> Exp.rep_id;
let+ es = es |> List.map(any_to_pretty(~settings)) |> all;
ListUtil.flat_intersperse(Grout({id, shape: Concave}), es);
| Parens({term: Fun(p, e, _, _), _})
| Parens({term: Fun(p, e, _, _), _} as inner_exp) =>
// TODO: Add optional newlines
let id = inner_exp |> Exp.rep_id;
let+ p = pat_to_pretty(~settings: Settings.t, p)
and+ e = go(e);
let name = Exp.get_fn_name(exp) |> Option.value(~default="anon fun");
let name =
if (settings.hide_fixpoints && String.ends_with(~suffix="+", name)) {
String.sub(name, 0, String.length(name) - 1);
} else {
name;
};
let name = "<" ++ name ++ ">";
let fun_form = [mk_form("fun_", id, [p])] @ e;
[mk_form("parens_exp", exp |> Exp.rep_id, [fun_form])]
|> fold_fun_if(settings.fold_fn_bodies, name);
| Fun(p, e, _, _) =>
// TODO: Add optional newlines
let id = exp |> Exp.rep_id;
Expand Down
1 change: 0 additions & 1 deletion src/haz3lweb/app/editors/result/EvalResult.re
Original file line number Diff line number Diff line change
Expand Up @@ -288,7 +288,6 @@ module Selection = {
type t =
| Evaluation(CodeSelectable.Selection.t)
| Stepper(Stepper.Selection.t);
// TODO: Selection in stepper

let get_cursor_info = (~selection: t, mr: Model.t): cursor(Update.t) =>
switch (selection, mr.result) {
Expand Down
16 changes: 13 additions & 3 deletions src/haz3lweb/app/editors/result/Stepper.re
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,7 @@ module Update = {
// Only perform below if either previous a or settings have changed
|> {
let.calc {expr: _, state, previous_substitutions, next_steps, _} = prev_a
and.calc settings = settings;
and.calc settings: Calc.t(CoreSettings.t) = settings;

// Check b is valid
let* b =
Expand Down Expand Up @@ -206,7 +206,11 @@ module Update = {
)
);
let next_expr =
EvalCtx.compose(b.step.ctx, next_expr) |> Typ.replace_temp_exp;
EvalCtx.compose(b.step.ctx, next_expr)
|> (
settings.evaluation.show_casts ? x => x : Haz3lcore.DHExp.strip_casts
)
|> Typ.replace_temp_exp;
let editor = CodeWithStatics.Model.mk_from_exp(~settings, next_expr);
let next_steps = calc_next_steps(settings, next_expr, next_state);
(
Expand Down Expand Up @@ -293,7 +297,13 @@ module Update = {
|> {
let.calc elab = elab
and.calc settings = settings;
let elab = elab |> Typ.replace_temp_exp;
let elab =
elab
|> (
settings.evaluation.show_casts
? x => x : Haz3lcore.DHExp.strip_casts
)
|> Typ.replace_temp_exp;
let editor = CodeWithStatics.Model.mk_from_exp(~settings, elab);
let next_steps =
calc_next_steps(settings, elab, EvaluatorState.init);
Expand Down

0 comments on commit 7eb9fa5

Please sign in to comment.