diff --git a/src/haz3lcore/prog/Dynamics.re b/src/haz3lcore/prog/Dynamics.re index 1cd326045..ac1e69977 100644 --- a/src/haz3lcore/prog/Dynamics.re +++ b/src/haz3lcore/prog/Dynamics.re @@ -103,7 +103,7 @@ module Probe = { /* Intercepts a probe form and adds in static semantic information * to guide dynamic information gathering */ - let instrument = + let instrument_exp = (m: Statics.Map.t, id: Id.t, probe_tag: Probe.tag): Probe.tag => switch (probe_tag) { | Paren => Paren diff --git a/src/haz3lcore/statics/Elaborator.re b/src/haz3lcore/statics/Elaborator.re index 653e3de57..1f0e46dfe 100644 --- a/src/haz3lcore/statics/Elaborator.re +++ b/src/haz3lcore/statics/Elaborator.re @@ -243,7 +243,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { e' |> cast_from(ty); | Parens(e, probe) => let (e', ty) = elaborate(m, e); - let probe = Dynamics.Probe.instrument(m, Exp.rep_id(uexp), probe); + let probe = Dynamics.Probe.instrument_exp(m, Exp.rep_id(uexp), probe); Parens(e' |> cast_from(ty), probe) |> rewrap; | Deferral(_) => uexp | Int(_) => uexp |> cast_from(Int |> Typ.temp) diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 2f79eae90..7bfbba123 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -127,6 +127,17 @@ let log_projector = (pr: Base.projector): unit => { projectors := Id.Map.add(pr.id, pr, projectors^); }; +/* Check if a term should be instrumented with a probe. + * Precondition: The relevant projector must have been + * logged before this is called */ +let should_instrument = (id: Id.t): bool => + switch (Id.Map.find_opt(id, projectors^)) { + | Some(pr) => + let (module P) = Projector.to_module(pr.kind); + P.dynamics; + | None => failwith("MakeTerm.exp: projector not found") + }; + let parse_sum_term: UTyp.t => ConstructorMap.variant(UTyp.t) = fun | {term: Var(ctr), ids, _} => Variant(ctr, ids, None) @@ -197,7 +208,10 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["(", ")"], [Exp(body)]) => ret(Parens(body, Paren)) | (label, [Exp(body)]) when is_probe_wrap(label) => // Temporary wrapping form to persist projector probes - ret(Parens(body, Probe(Probe.empty))) + ret( + should_instrument(Exp.rep_id(body)) + ? Parens(body, Probe(Probe.empty)) : body.term, + ) | (["[", "]"], [Exp(body)]) => switch (body) { | {ids, copied: false, term: Tuple(es)} => (ListLit(es), ids) @@ -361,7 +375,8 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { Invalid(t) | (["(", ")"], [Pat(body)]) => Parens(body, Paren) | (label, [Pat(body)]) when is_probe_wrap(label) => - Parens(body, Probe(Probe.empty)) + should_instrument(Pat.rep_id(body)) + ? Parens(body, Probe(Probe.empty)) : body.term | (["[", "]"], [Pat(body)]) => switch (body) { | {term: Tuple(ps), _} => ListLit(ps) @@ -536,7 +551,7 @@ and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => { switch (p) { | Secondary(_) | Grout(_) => [] - | Projector({syntax, id: _, _} as pr) => + | Projector({syntax, _} as pr) => let _ = log_projector(pr); let sort = Piece.sort(syntax) |> fst; [go_s(sort, Segment.skel([syntax]), [syntax])]; diff --git a/src/haz3lcore/zipper/ProjectorBase.re b/src/haz3lcore/zipper/ProjectorBase.re index 24b224222..4f80671e0 100644 --- a/src/haz3lcore/zipper/ProjectorBase.re +++ b/src/haz3lcore/zipper/ProjectorBase.re @@ -100,6 +100,10 @@ module type Projector = { * and has two callbacks: ~parent for parent editor * actions(see external_action type above), and ~local * for this projector's local update function. */ + let dynamics: bool; + /* If dynamics is true, this projector will be + * instrumented with a probe to collect dynamic + * information during evaluation */ let view: ( model, @@ -146,6 +150,7 @@ module Cook = (C: Projector) : Cooked => { let init = C.init |> serialize_m; let can_project = C.can_project; let can_focus = C.can_focus; + let dynamics = C.dynamics; let view = (m, ~info, ~local, ~parent, ~utility) => C.view( deserialize_m(m), diff --git a/src/haz3lcore/zipper/projectors/CheckboxProj.re b/src/haz3lcore/zipper/projectors/CheckboxProj.re index 73c2c60b1..936ab7f79 100644 --- a/src/haz3lcore/zipper/projectors/CheckboxProj.re +++ b/src/haz3lcore/zipper/projectors/CheckboxProj.re @@ -52,6 +52,7 @@ module M: Projector = { let init = (); let can_project = p => state_of(p) != None; let can_focus = false; + let dynamics = false; let placeholder = (_, _) => Inline(2); let update = (model, _) => model; let view = view; diff --git a/src/haz3lcore/zipper/projectors/FoldProj.re b/src/haz3lcore/zipper/projectors/FoldProj.re index af47bb255..15d9dd5d7 100644 --- a/src/haz3lcore/zipper/projectors/FoldProj.re +++ b/src/haz3lcore/zipper/projectors/FoldProj.re @@ -17,6 +17,7 @@ module M: Projector = { let init = {text: "⋱"}; let can_project = _ => true; let can_focus = false; + let dynamics = false; let placeholder = (m, _) => Inline(m.text == "⋱" ? 2 : m.text |> String.length); let update = (m, _) => m; diff --git a/src/haz3lcore/zipper/projectors/InfoProj.re b/src/haz3lcore/zipper/projectors/InfoProj.re index 5f9fde027..9bd3e3e02 100644 --- a/src/haz3lcore/zipper/projectors/InfoProj.re +++ b/src/haz3lcore/zipper/projectors/InfoProj.re @@ -49,6 +49,7 @@ module M: Projector = { }; let can_focus = false; + let dynamics = false; let display_ty = (model, info) => switch (model) { diff --git a/src/haz3lcore/zipper/projectors/ProbeProj.re b/src/haz3lcore/zipper/projectors/ProbeProj.re index 3711c0ad6..091b76a86 100644 --- a/src/haz3lcore/zipper/projectors/ProbeProj.re +++ b/src/haz3lcore/zipper/projectors/ProbeProj.re @@ -198,8 +198,8 @@ let rm_opaques: /* Is the underlying syntax a variable reference? */ let is_var_ref = (info: info): bool => - switch (MakeTerm.go([info.syntax]).term.term) { - | Var(_) => true + switch (info.statics) { + | Some(InfoExp({term: {term: Var(_), _}, _})) => true | _ => false }; @@ -372,6 +372,7 @@ module M: Projector = { let init = init; let can_project = _ => true; let can_focus = false; + let dynamics = true; let placeholder = placeholder; let update = update; let view = view; diff --git a/src/haz3lcore/zipper/projectors/SliderFProj.re b/src/haz3lcore/zipper/projectors/SliderFProj.re index 713315d39..c14e8b356 100644 --- a/src/haz3lcore/zipper/projectors/SliderFProj.re +++ b/src/haz3lcore/zipper/projectors/SliderFProj.re @@ -24,6 +24,7 @@ module M: Projector = { let init = (); let can_project = p => get_opt(p) != None; let can_focus = false; + let dynamics = false; let placeholder = (_, _) => Inline(10); let update = (model, _) => model; let view = diff --git a/src/haz3lcore/zipper/projectors/SliderProj.re b/src/haz3lcore/zipper/projectors/SliderProj.re index 5d7b3fe5a..975cfc0b2 100644 --- a/src/haz3lcore/zipper/projectors/SliderProj.re +++ b/src/haz3lcore/zipper/projectors/SliderProj.re @@ -21,6 +21,7 @@ module M: Projector = { let init = (); let can_project = p => get_opt(p) != None; let can_focus = false; + let dynamics = false; let placeholder = (_, _) => Inline(10); let update = (model, _) => model; let view = diff --git a/src/haz3lcore/zipper/projectors/TextAreaProj.re b/src/haz3lcore/zipper/projectors/TextAreaProj.re index 63748ea0f..e0c64951b 100644 --- a/src/haz3lcore/zipper/projectors/TextAreaProj.re +++ b/src/haz3lcore/zipper/projectors/TextAreaProj.re @@ -98,6 +98,7 @@ module M: Projector = { let init = (); let can_project = _ => true; //TODO(andrew): restrict somehow let can_focus = true; + let dynamics = false; let placeholder = (_, info) => { let str = Form.strip_quotes(get(info.syntax)); Block({