From dc8ebfe484d9bfe26716f501dc33606f10997619 Mon Sep 17 00:00:00 2001 From: disconcision Date: Sun, 15 Dec 2024 21:19:14 -0500 Subject: [PATCH] projectors live cleanup --- src/haz3lcore/dynamics/Transition.re | 9 +---- src/haz3lcore/pretty/ExpToSegment.re | 4 +- src/haz3lcore/statics/MakeTerm.re | 7 +--- src/haz3lcore/statics/Statics.re | 38 +++++++++---------- src/haz3lweb/app/editors/result/EvalResult.re | 2 +- 5 files changed, 27 insertions(+), 33 deletions(-) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index c60fa53678..583b07cbb1 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -358,13 +358,6 @@ module Transition = (EV: EV_MODE) => { is_value: false, }); } - // let.match env'' = (env', matches(dp, d2')); - // Step({ - // expr: Closure(env'', d3) |> fresh, - // state_update, - // kind: FunAp, - // is_value: false, - // }); | Cast( d3', {term: Arrow(ty1, ty2), _}, @@ -783,6 +776,8 @@ module Transition = (EV: EV_MODE) => { let. _ = otherwise(env, d); Indet; | Parens(d'', Probe(pr)) => + /* When evaluated, a probe adds a dynamics info entry + * reflecting the evaluation of the contained expression */ let. _ = otherwise(env, ((d, _)) => Parens(d, Probe(pr)) |> rewrap) and. (d', _) = req_final_or_value( diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re index c11da79308..f1e3791856 100644 --- a/src/haz3lcore/pretty/ExpToSegment.re +++ b/src/haz3lcore/pretty/ExpToSegment.re @@ -49,7 +49,9 @@ let should_add_space = (s1, s2) => && !Form.is_keyword(s1) && String.starts_with(s2, ~prefix="(") => false - | _ when String.ends_with(s1, ~suffix="…") => false + | _ when String.ends_with(s1, ~suffix="…") => + /* Hack case for probe projector abbreviations */ + false | _ => true }; diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 1a651ec1de..38c00f5951 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -15,7 +15,7 @@ open Any; /* Hack: Temporary construct internal to maketerm * to handle probe parsing; see `tokens` below */ -let probe_wrap = ["@@@@@", "@@@@@"]; +let probe_wrap = ["PROBE_WRAP", "PROBE_WRAP"]; let is_probe_wrap = (==)(probe_wrap); // TODO make less hacky @@ -545,10 +545,7 @@ and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => { | Grout(_) => [] | 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)]; + [go_s(sort, Segment.skel([syntax]), [syntax])]; | Tile({mold, shards, children, _}) => Aba.aba_triples(Aba.mk(shards, children)) |> List.map(((l, kid, r)) => { diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index ac8dcdb122..f20e3f8e57 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -1,29 +1,29 @@ /* STATICS.re - This module determines the statics semantics of a program. - It makes use of the following modules: + This module determines the statics semantics of a program. + It makes use of the following modules: - INFO.re: Defines the Info.t type which is used to represent the - static STATUS of a term. This STATUS can be either OK or ERROR, - and is determined by reconcilling two sources of typing information, - the MODE and the SELF. + INFO.re: Defines the Info.t type which is used to represent the + static STATUS of a term. This STATUS can be either OK or ERROR, + and is determined by reconcilling two sources of typing information, + the MODE and the SELF. - MODE.re: Defines the Mode.t type which is used to represent the - typing expectations imposed by a term's ancestors. + MODE.re: Defines the Mode.t type which is used to represent the + typing expectations imposed by a term's ancestors. - SELF.re: Define the Self.t type which is used to represent the - type information derivable from the term itself. + SELF.re: Define the Self.t type which is used to represent the + type information derivable from the term itself. - The point of STATICS.re itself is to derive a map between each - term's unique id and that term's static INFO. The below functions - are intended mostly as infrastructure: The point is to define a - traversal through the syntax tree which, for each term, passes - down the MODE, passes up the SELF, calculates the INFO, and adds - it to the map. + The point of STATICS.re itself is to derive a map between each + term's unique id and that term's static INFO. The below functions + are intended mostly as infrastructure: The point is to define a + traversal through the syntax tree which, for each term, passes + down the MODE, passes up the SELF, calculates the INFO, and adds + it to the map. - The architectural intention here is that most type-manipulation - logic is defined in INFO, MODE, and SELF, and the STATICS module - itself is dedicated to the piping necessary to (A) introduce and + The architectural intention here is that most type-manipulation + logic is defined in INFO, MODE, and SELF, and the STATICS module + itself is dedicated to the piping necessary to (A) introduce and (B) propagate the necessary information through the syntax tree. */ diff --git a/src/haz3lweb/app/editors/result/EvalResult.re b/src/haz3lweb/app/editors/result/EvalResult.re index 62f655a7ab..840f2b0961 100644 --- a/src/haz3lweb/app/editors/result/EvalResult.re +++ b/src/haz3lweb/app/editors/result/EvalResult.re @@ -93,7 +93,7 @@ module Model = { switch (model.result) { | Evaluation({result: OldValue(ResultOk((_, state))), _}) | Evaluation({result: NewValue(ResultOk((_, state))), _}) => - Some(state |> Haz3lcore.EvaluatorState.get_probes) + Some(Haz3lcore.EvaluatorState.get_probes(state)) | Stepper(s) => Some( s.history