Skip to content

Commit

Permalink
probe projector ap descent indication
Browse files Browse the repository at this point in the history
  • Loading branch information
disconcision committed Dec 28, 2024
1 parent 8ea387e commit 6fb7a52
Show file tree
Hide file tree
Showing 6 changed files with 102 additions and 30 deletions.
7 changes: 6 additions & 1 deletion src/haz3lcore/dynamics/PatternMatch.re
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,14 @@ let capture_closure = (pr, id: Id.t, d, inner_match: match_result): unit =>
| IndetMatch => ()
| Matches(env) =>
print_endline("Pattern Match: capturing a closure");
let dyn_stack = []; //TODO(andrew)
closure_closures :=
List.cons(
stack => (id, Dynamics.Probe.Closure.mk(d, {env, stack, id}, pr)),
stack =>
(
id,
Dynamics.Probe.Closure.mk(d, {env, stack, dyn_stack, id}, pr),
),
closure_closures^,
);
};
Expand Down
1 change: 1 addition & 0 deletions src/haz3lcore/dynamics/Transition.re
Original file line number Diff line number Diff line change
Expand Up @@ -361,6 +361,7 @@ module Transition = (EV: EV_MODE) => {
let env'' =
evaluate_extend_env(
~frame=Some(Term.Exp.rep_id(d)),
~dyn_env=env,
env'',
env',
);
Expand Down
2 changes: 2 additions & 0 deletions src/haz3lcore/prog/Dynamics.re
Original file line number Diff line number Diff line change
Expand Up @@ -68,12 +68,14 @@ module Probe = {
value: DHExp.t,
env: Env.t,
stack: Probe.stack,
dyn_stack: Probe.stack,
};

let mk = (value: DHExp.t, env: ClosureEnvironment.t, pr: Probe.t) => {
closure_id: Id.mk(),
value,
stack: ClosureEnvironment.stack_of(env),
dyn_stack: ClosureEnvironment.dyn_stack_of(env),
env: Env.mk(ClosureEnvironment.map_of(env), pr.refs),
};
};
Expand Down
35 changes: 23 additions & 12 deletions src/haz3lcore/statics/TermBase.re
Original file line number Diff line number Diff line change
Expand Up @@ -151,6 +151,7 @@ and closure_environment_t = {
id: Id.t,
env: environment_t,
stack: Probe.stack,
dyn_stack: Probe.stack,
}
and stepper_filter_kind_t =
| Filter(filter)
Expand Down Expand Up @@ -929,12 +930,14 @@ and ClosureEnvironment: {
let id_of: t => Id.t;
let map_of: t => Environment.t;
let stack_of: t => list(Probe.frame);
let dyn_stack_of: t => list(Probe.frame);

let id_equal: (closure_environment_t, closure_environment_t) => bool;

let lookup: (t, Var.t) => option(Exp.t);
let update_env: (Environment.t => Environment.t, t) => t;
let extend_eval: (~frame: option(Id.t)=?, Environment.t, t) => t;
let extend_eval:
(~frame: option(Id.t)=?, ~dyn_env: t=?, Environment.t, t) => t;

let to_list: t => list((Var.t, Exp.t));
let without_keys: (list(Var.t), t) => t;
Expand All @@ -943,20 +946,22 @@ and ClosureEnvironment: {
[@deriving (show({with_path: false}), sexp, yojson)]
type t = closure_environment_t;

let wrap: (Id.t, Environment.t, Probe.stack) => t;
let wrap: (Id.t, Environment.t, Probe.stack, Probe.stack) => t;

let id_of: t => Id.t;
let map_of: t => Environment.t;
let stack_of: t => list(Probe.frame);
let dyn_stack_of: t => list(Probe.frame);
} = {
[@deriving (show({with_path: false}), sexp, yojson)]
type t = closure_environment_t;

let wrap = (id, env, stack): t => {id, env, stack};
let wrap = (id, env, stack, dyn_stack): t => {id, env, stack, dyn_stack};

let id_of = t => t.id;
let map_of = t => t.env;
let stack_of = t => t.stack;
let dyn_stack_of = t => t.dyn_stack;

let (sexp_of_t, t_of_sexp) =
StructureShareSexp.structure_share_here(id_of, sexp_of_t, t_of_sexp);
Expand All @@ -965,7 +970,7 @@ and ClosureEnvironment: {

let to_list = env => env |> map_of |> Environment.to_listo;

let of_environment = env => wrap(Id.mk(), env, []);
let of_environment = env => wrap(Id.mk(), env, [], []);

/* Equals only needs to check environment id's (faster than structural equality
* checking.) */
Expand All @@ -981,15 +986,14 @@ and ClosureEnvironment: {
let without_keys = keys => update_env(Environment.without_keys(keys));

let update_stack = (ap_id: option(Id.t), env) => {
let stack =
let (stack, dyn_stack) =
switch (ap_id) {
| None => stack_of(env)
| Some(ap_id) => [
Probe.mk_frame(~env_id=id_of(env), ~ap_id),
...stack_of(env),
]
| None => (stack_of(env), dyn_stack_of(env))
| Some(ap_id) =>
let frame = Probe.mk_frame(~env_id=id_of(env), ~ap_id);
([frame, ...stack_of(env)], [frame, ...dyn_stack_of(env)]);
};
{...env, stack};
{...env, stack, dyn_stack};
};

/* Extend the environment with new bindings. ~frame is an optional argument which
Expand All @@ -998,12 +1002,19 @@ and ClosureEnvironment: {
* frames for each environment created by a function application, and the
* syntax ids of those applications are used as the Id for the frame */
let extend_eval =
(~frame: option(Id.t)=None, new_bindings: Environment.t, to_extend: t)
(
~frame: option(Id.t)=None,
~dyn_env: t=empty,
new_bindings: Environment.t,
to_extend: t,
)
: t =>
{
id: Id.mk(),
env: Environment.union(new_bindings, map_of(to_extend)),
stack: stack_of(to_extend),
dyn_stack:
dyn_stack_of(dyn_env.env == Environment.empty ? to_extend : dyn_env) //TODO(andrew): cleanup
}
|> update_stack(frame);
}
Expand Down
69 changes: 55 additions & 14 deletions src/haz3lcore/zipper/projectors/ProbeProj.re
Original file line number Diff line number Diff line change
Expand Up @@ -34,19 +34,20 @@ let model'_of_sexp = (sexp): model' =>
| x => x
};

// let stack = stack =>
// stack
// |> List.rev
// |> List.map(({env_id, ap_id}: Probe.frame) =>
// ""
// ++ String.sub(Id.to_string(env_id), 0, 2)
// ++ "\n"
// ++ String.sub(Id.to_string(ap_id), 0, 2)
// )
// |> String.concat("\n");
let stack = stack =>
stack
|> List.rev
|> List.map(({env_id, ap_id}: Probe.frame) =>
""
++ String.sub(Id.to_string(env_id), 0, 2)
++ " : "
++ String.sub(Id.to_string(ap_id), 0, 2)
)
|> String.concat("\n");

let env_cursor: ref(list(Id.t)) = ref([]);
let last_target: ref(list('a)) = ref([]);
let cur_ap: ref(option(Id.t)) = ref(Option.None);
let mousedown: ref(option(Js.t(Dom_html.element))) = ref(Option.None);

let common_suffix_length = (s1, s2) =>
Expand Down Expand Up @@ -89,9 +90,19 @@ let get_goal = (utility: utility, e: Js.t(Dom_html.mouseEvent)) =>
e |> Js.Unsafe.coerce,
);

let cur_ap_id = (info: info) =>
switch (info.statics) {
| Some(InfoExp({term: {term: Ap(_), _} as ap, _})) =>
Some(Term.Exp.rep_id(ap))
| Some(InfoExp({term: {term: Parens({term: Ap(_), _} as ap, _), _}, _})) =>
Some(Term.Exp.rep_id(ap))
| _ => None
};

let resizable_val =
(
~resizable=false,
info: info,
model,
utility,
local,
Expand All @@ -103,6 +114,7 @@ let resizable_val =
mousedown := Some(target);
env_cursor := Probe.env_stack(closure.stack);
last_target := [target];
cur_ap := cur_ap_id(info);
Effect.Ignore;
};

Expand All @@ -126,11 +138,30 @@ let resizable_val =
| _ => Effect.Ignore
};

//TODO(andrew): cleanup
let dyn_ind =
switch (info.statics) {
| _
when
Option.is_some(
List.find_opt(
({ap_id, _}: Probe.frame) => Some(ap_id) == cur_ap^,
closure.dyn_stack,
),
) => [
"dyn-cursor",
]
| _ => []
};

div(
~attrs=[
//Attr.title(stack(closure.stack)),
Attr.title(stack(closure.dyn_stack)),
Attr.classes(
["val-resize"] @ (show_indicator(closure.stack) ? ["cursor"] : []),
["val-resize"]
@ dyn_ind
@ (Option.is_some(cur_ap_id(info)) ? ["ap"] : [])
@ (show_indicator(closure.stack) ? ["cursor"] : []),
),
Attr.on_double_click(_ => local(ToggleShowAllVals)),
Attr.on_pointerdown(val_pointerdown),
Expand Down Expand Up @@ -192,7 +223,16 @@ let closure_view =
["closure"] @ (show_indicator(closure.stack) ? ["cursor"] : []),
),
],
[resizable_val(~resizable=index == 0, model, utility, local, closure)]
[
resizable_val(
~resizable=index == 0,
info,
model,
utility,
local,
closure,
),
]
@ (is_var_ref(info) ? [] : [env_view(closure, utility)]),
);

Expand Down Expand Up @@ -293,7 +333,7 @@ let syntax_view = (info: info) => info |> syntax_str |> text;
let placeholder = (_m, info) =>
Inline(3 + String.length(syntax_str(info)));

let icon = div(~attrs=[Attr.classes(["icon"])], [text("🔍")]);
// let icon = div(~attrs=[Attr.classes(["icon"])], [text("🔍")]);
let icon = div(~attrs=[Attr.classes(["icon"])], []);

let view = (model: model', ~info, ~local, ~parent as _, ~utility: utility) => {
Expand All @@ -304,6 +344,7 @@ let view = (model: model', ~info, ~local, ~parent as _, ~utility: utility) => {
Attr.classes(["main"]),
Attr.on_click(_ => {
env_cursor := [];
cur_ap := None;
Effect.Ignore;
}),
],
Expand Down
18 changes: 15 additions & 3 deletions src/haz3lweb/www/style/projectors/probe.css
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/* Probe Projector */
:root{
:root {
--exp_base: #c7e6c6;
--pat_base: #c6e6e1;

Expand All @@ -11,6 +11,8 @@

--exp_cell: #9eca9b;
--pat_cell: #9bcabe;

--ap-highlight: #c9aaf3;
}

.projector.probe {
Expand Down Expand Up @@ -73,7 +75,7 @@
z-index: var(--code-emblems-z);
}
.projector.probe.Pat .num-closures {
background-color: var(--pat_indicated);
background-color: var(--pat_indicated);
}
.projector.probe.selected .num-closures {
background-color: var(--Y1);
Expand Down Expand Up @@ -125,6 +127,13 @@
filter: none;
opacity: 100%;
}
.projector.probe .val-resize.dyn-cursor .code-text {
/* outline: 1.6px solid var(--G0);
outline-style: dotted; */
filter: none;
opacity: 100%;
background-color: var(--ap-highlight);
}

.projector.probe .val-resize .code-text {
opacity: 40%;
Expand Down Expand Up @@ -176,9 +185,12 @@
background: none;
outline: 2.8px solid var(--exp_indicated);
}
.projector.probe.indicated .val-resize.cursor.ap .code-text {
outline-color: var(--ap-highlight);
}
.projector.probe.indicated.Pat .val-resize.cursor .code-text {
outline-color: var(--pat_indicated);
}
}

.projector.probe.indicated .closure:hover .live-env {
display: block;
Expand Down

0 comments on commit 6fb7a52

Please sign in to comment.