diff --git a/src/haz3lcore/dynamics/Probe.re b/src/haz3lcore/dynamics/Probe.re index be7e51a66..bf4da4dc9 100644 --- a/src/haz3lcore/dynamics/Probe.re +++ b/src/haz3lcore/dynamics/Probe.re @@ -1,5 +1,13 @@ open Util; +/* A syntax probe is inserted into syntax to capture + * information during evaluation. The tag type below, + * for the probe case, is used to collect binding ids + * which are used to faciltate capturing the values + * of certain variables in the environment. This captured + * information is, for a given closure, encoded in + * the `frame` type. */ + [@deriving (show({with_path: false}), sexp, yojson)] type t = { refs: Binding.s, @@ -11,15 +19,25 @@ type tag = | Paren | Probe(t); +/* Information about the evaluation of an ap */ [@deriving (show({with_path: false}), sexp, yojson)] type frame = { - env_id: Id.t, - frame_id: Id.t, + closure_id: Id.t, /* Primary ID (Unique) */ + ap_id: Id.t, /* Syntax ID of the ap */ + env_id: Id.t /* ID of ClosureEnv created by ap */ }; +/* List of applications prior to some evaluation */ [@deriving (show({with_path: false}), sexp, yojson)] type stack = list(frame); -let empty = {refs: [], stem: []}; +let empty: t = {refs: [], stem: []}; + +let env_stack: list(frame) => list(Id.t) = + List.map((en: frame) => en.env_id); -let env_stack = List.map((en: frame) => en.env_id); +let mk_frame = (~env_id: Id.t, ~ap_id: Id.t): frame => { + closure_id: Id.mk(), + env_id, + ap_id, +}; diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 31283b1dc..1a651ec1d 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -13,13 +13,23 @@ open Util; open Any; +/* Hack: Temporary construct internal to maketerm + * to handle probe parsing; see `tokens` below */ +let probe_wrap = ["@@@@@", "@@@@@"]; +let is_probe_wrap = (==)(probe_wrap); + // TODO make less hacky let tokens = Piece.get( _ => [], _ => [" "], (t: Tile.t) => t.shards |> List.map(List.nth(t.label)), - _ => [], + _ => + /* Hack: These act as temporary wrappers for projectors, + * which are retained through maketerm so as to be used in + * dynamics. These are inserted and removed entirely internal + * to maketerm. */ + probe_wrap, ); [@deriving (show({with_path: false}), sexp, yojson)] @@ -112,21 +122,13 @@ let return = (wrap, ids, tm) => { /* Map to collect projector ids */ let projectors: ref(Id.Map.t(Piece.projector)) = ref(Id.Map.empty); -/* Temporary form to persist projector dynamics probe to segments */ -let mk_probe = (id, e: list(Piece.t)) => - Piece.mk_tile_id( - id, - Form.mk(Form.ii, ["@@", "@@"], Mold.mk_op(Exp, [Exp])), - [e], - ); - /* Strip a projector from a segment and log it in the map */ -let rm_and_log_projectors = (seg: Segment.t): Segment.t => +let log_projectors = (seg: Segment.t): Segment.t => List.map( fun | Piece.Projector(pr) => { projectors := Id.Map.add(pr.id, pr, projectors^); - mk_probe(pr.id, [pr.syntax]); + Piece.Projector(pr); } | x => x, seg, @@ -200,7 +202,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | ([t], []) when Form.is_ctr(t) => ret(Constructor(t, Unknown(Internal) |> Typ.temp)) | (["(", ")"], [Exp(body)]) => ret(Parens(body, Paren)) - | (["@@", "@@"], [Exp(body)]) => + | (label, [Exp(body)]) when is_probe_wrap(label) => // Temporary wrapping form to persist projector probes ret(Parens(body, Probe(Probe.empty))) | (["[", "]"], [Exp(body)]) => @@ -365,6 +367,7 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { | ([t], []) when t != " " && !Form.is_explicit_hole(t) => Invalid(t) | (["(", ")"], [Pat(body)]) => Parens(body) + | (label, [Pat(body)]) when is_probe_wrap(label) => Parens(body) | (["[", "]"], [Pat(body)]) => switch (body) { | {term: Tuple(ps), _} => ListLit(ps) @@ -425,6 +428,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = { | (["String"], []) => String | ([t], []) when Form.is_typ_var(t) => Var(t) | (["(", ")"], [Typ(body)]) => Parens(body) + | (label, [Typ(body)]) when is_probe_wrap(label) => Parens(body) | (["[", "]"], [Typ(body)]) => List(body) | ([t], []) when t != " " && !Form.is_explicit_hole(t) => Unknown(Hole(Invalid(t))) @@ -534,12 +538,17 @@ and rul = (unsorted: unsorted): Rul.t => { and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => { /* Remove projectors. We do this here as opposed to removing * them in an external call to save a whole-syntax pass. */ - let seg = rm_and_log_projectors(seg); + let _ = log_projectors(seg); let tile_kids = (p: Piece.t): list(Term.Any.t) => switch (p) { | Secondary(_) | Grout(_) => [] - | Projector(_) => [] + | Projector({syntax, id: _, _}) => + let sort = Piece.sort(syntax) |> fst; + let seg = [syntax]; + //let seg = [mk_probe(id, seg)]; + //print_endline("unsorted projector case"); + [go_s(sort, Segment.skel(seg), seg)]; | Tile({mold, shards, children, _}) => Aba.aba_triples(Aba.mk(shards, children)) |> List.map(((l, kid, r)) => { diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 8cecdfd92..e3e34020e 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -976,12 +976,12 @@ and ClosureEnvironment: { let without_keys = keys => update_env(Environment.without_keys(keys)); - let update_stack = (frame: option(Id.t), env) => { + let update_stack = (ap_id: option(Id.t), env) => { let stack = - switch (frame) { + switch (ap_id) { | None => stack_of(env) - | Some(frame) => [ - {env_id: id_of(env), frame_id: frame}, + | Some(ap_id) => [ + Probe.mk_frame(~env_id=id_of(env), ~ap_id), ...stack_of(env), ] }; diff --git a/src/haz3lcore/zipper/projectors/ProbeProj.re b/src/haz3lcore/zipper/projectors/ProbeProj.re index e58626392..e846755df 100644 --- a/src/haz3lcore/zipper/projectors/ProbeProj.re +++ b/src/haz3lcore/zipper/projectors/ProbeProj.re @@ -39,11 +39,13 @@ type a = let stack = stack => stack |> List.rev - |> List.map(({env_id, frame_id}: Probe.frame) => + |> List.map(({env_id, ap_id, closure_id}: Probe.frame) => "" + ++ String.sub(Id.to_string(closure_id), 0, 2) + ++ "\n" ++ String.sub(Id.to_string(env_id), 0, 2) ++ "\n" - ++ String.sub(Id.to_string(frame_id), 0, 2) + ++ String.sub(Id.to_string(ap_id), 0, 2) ) |> String.concat("\n");