Skip to content

Break out semantics to library #1619

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: projector-gadts
Choose a base branch
from
Open

Conversation

disconcision
Copy link
Member

@disconcision disconcision commented Apr 17, 2025

This is a speculative breaking semantics out of core. Wanted to see how clean it was. Answer is: better than I thought, but not perfect.

Semantics contains what you'd expect, I think. Borderline cases are things like Operators which are maybe more aware of the surface syntax than is strictly seemly.

Haz3lcore is a bit more fraught. Currently it contains:

  • tylrCore proper (Editor.re and dependencies)
  • maketerm + expToSeg (Interface between tylr and semantics)
  • TyDi (most logic could live in Semantics, but not sure if appropriate. I feel @7h3kk1d's Introduce is in a similar boat)
  • projectors

@Negabinary at this point I'm wondering if our first-order move here for splices is proceed with this PR, removing haz3lcore entirely and just moving all contents to haz3lweb, most but not all to a new tylr subfolder, but leaving the resolving the tylr/projectors API to future work.

TODO:

  • rm unnecessary deps from semantics

@7h3kk1d
Copy link
Contributor

7h3kk1d commented Apr 18, 2025

I would like for introduce to live on the ast but there's some issues with cursor position for empty containers. To where if you get the ID from an expression in the AST and move to that in the zipper the cursor is outside of it. i.e on empty lists the cursor ends up outside the list. The only way I can see to address it is by having a path/zipper on the AST and a translation back to the tylr zipper.

Sidenote: i think if we remove the is dependency for this the property tests will be a bit faster and debuggers will work.

@disconcision
Copy link
Member Author

disconcision commented Apr 18, 2025

yeah i have the same issue with TyDi. there might be a slightly more lightweight option than full paths, e.g. term->term transformations plus an additional value representing an existing structural movement action to take after replacement, e.g. whether the caret should advance to the first hole after replacement.

@7h3kk1d
Copy link
Contributor

7h3kk1d commented Apr 18, 2025

e.g. whether the caret should advance to the first hole after replacement.

That's what I had done for introduce but Cyrus didn't like introduce on lists being singleton lists and otherwise there's no hole. Either way you have the same issue on empty strings. Maybe go to empty lists and string should go inside but that also seems sketchy. It's currently a flag to go left once

@disconcision
Copy link
Member Author

I guess you could still abstract this; identify a more general notion of 'go to next point of interest', in the sense of per form defined ~ canonical cursor positions to effectuate structured transformations (eg middle of token for [|] to do [] => [?|]). (for tydi I went worse to tho, I just did all syntax construction as strings).

Copy link

codecov bot commented Apr 18, 2025

Codecov Report

Attention: Patch coverage is 6.31579% with 89 lines in your changes missing coverage. Please review.

Project coverage is 46.18%. Comparing base (7997def) to head (30f562d).

Files with missing lines Patch % Lines
src/semantics/term/Sort.re 0.00% 23 Missing ⚠️
src/haz3lcore/zipper/action/Select.re 0.00% 11 Missing ⚠️
src/haz3lcore/TyDi/TyDi.re 0.00% 8 Missing ⚠️
src/semantics/statics/Ctx.re 0.00% 7 Missing ⚠️
src/haz3lcore/lang/MakeTerm.re 0.00% 5 Missing ⚠️
src/haz3lcore/TyDi/TyDiForms.re 0.00% 4 Missing ⚠️
src/haz3lcore/TyDi/TyDiSuggestion.re 0.00% 4 Missing ⚠️
src/haz3lcore/TyDi/TyDiCtx.re 0.00% 3 Missing ⚠️
src/haz3lcore/projectors/ProjectorBase.re 0.00% 3 Missing ⚠️
src/haz3lcore/zipper/action/Indicated.re 0.00% 3 Missing ⚠️
... and 10 more
Additional details and impacted files
@@                 Coverage Diff                 @@
##           projector-gadts    #1619      +/-   ##
===================================================
+ Coverage            46.05%   46.18%   +0.13%     
===================================================
  Files                  126      126              
  Lines                14046    13991      -55     
===================================================
- Hits                  6469     6462       -7     
+ Misses                7577     7529      -48     
Files with missing lines Coverage Δ
src/haz3lcore/derived/Measured.re 47.54% <ø> (ø)
src/haz3lcore/derived/TermMap.re 100.00% <100.00%> (ø)
src/haz3lcore/derived/TermRanges.re 93.75% <ø> (ø)
src/haz3lcore/derived/TileMap.re 100.00% <ø> (ø)
src/haz3lcore/lang/Precedence.re 92.00% <ø> (-2.00%) ⬇️
src/haz3lcore/pretty/ExpToSegment.re 75.57% <ø> (ø)
src/haz3lcore/projectors/ProjectorInfo.re 18.18% <ø> (ø)
src/haz3lcore/projectors/ProjectorInit.re 11.11% <ø> (ø)
...c/haz3lcore/projectors/implementations/CardProj.re 0.35% <ø> (ø)
...z3lcore/projectors/implementations/CheckboxProj.re 0.00% <ø> (ø)
... and 68 more

... and 1 file with indirect coverage changes

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@7h3kk1d
Copy link
Contributor

7h3kk1d commented Apr 18, 2025

Yeah, I'd have to think more about how it would look. Maybe there's only a single position for most forms.

Copy link
Contributor

@7h3kk1d 7h3kk1d left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This all seemed surprisingly unproblematic. Not sure how it fits into the longer term projector work and I would like to see the semantics and AST be split out as much as possible in the future but this seems like a positive improvement.

| Typ => "type"
| Rul => "rule"
| Exp => "expression";
include Semantics.Sort;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are we planning on these diverging or is this just just an alias?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

just an alias, as Sort is used hundreds of times across tylr. not sure what best practices here should be; i definitely do this reluctantly. I only aliased Sort and Id in this manner

Comment on lines +82 to +87
statics: option(Semantics.Statics.Info.t),
/* Dynamic information about the syntax including
* live values of the syntax. Dynamics may be
* disabled by the user; this case (None) must be
* handled by projector authors */
dynamics: option(Dynamics.Info.t),
dynamics: option(Semantics.Dynamics.Info.t),
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You shouldn't need to namespace this given the open above.

@@ -183,7 +183,8 @@ let gen_constructor_ident: QCheck.Gen.t(string) =
let* leading = char_range('A', 'Z');
let+ tail = string_size(~gen=char_range('a', 'z'), int_range(1, 4));
let ident = String.make(1, leading) ++ tail;
if (List.exists(a => a == ident, Haz3lcore.Form.base_typs)) {
//TODO(andrew): copied list of base types below to remove Form dep...
if (List.exists(a => a == ident, ["String", "Int", "Float", "Bool"])) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should reconsider this as well since (from what I recall) those are excluded as constructor names in parsing and I think that should happen in statics if anything. This doesn't happen for other non-base types.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

how would you handle this for the moment? remove this and leave it to statics to decide?
(seems reasonable to defer as much as possible to statics; the proximate situation is going to be that all of tylr, semantics, and the parser all implicitly depend on a shared but non-materialized language definition. i don't think we have an easy path for actually abstracting this is the implementation. this particular one (base types) already has multiple divergences in the implementation (i counted three different sets of base types used in different places))

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This needs to be consistent with the tylr version. Im fine with it being either hard coded here or a list defined in semantics somewhere. If we define it in semantics can't all 3 libraries use the same defn?

Comment on lines -225 to -226
settings.flip_animations && Action.should_animate(a)
? Animation.request([Animation.Actions.move("caret")]) : ();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know this is happening on perform now, but can I get some context.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

the animation system I created requires (a) capturing DOM state before an action is triggered, (b) storing that state so that it is persisted into the next MVU loop, and (c) capturing DOM state after the action has been formed, after the DOM is regenerated, but before draw occurs. (a) was done here; now i've moved it slightly so that Animation can live in Web. (b) happens in Main.re.

The reason why it was here to begin with (aside from the lazy fact that core has web dep due to projectors), is that in general we want to trigger animations based on the particular action taken, possibly with explicit dependence on both the before and after state of the model. I'm continually torn on whether effects like this should be handled as part of an entirely separate switch; i like the separation of concerns, but also think that it's not terrible to be forced to think about the effect when you change an action. I had started moving in the separation direction, but ended up punting, forgetting about it, and leaving it in an intermediate state. I think now that the effect should probably be abstracted to the Action.should_animate function, which should take the before and after models as well as the action, and produce an effect.

@@ -87,7 +87,7 @@ type pos =
type spec = p(Zipper.t);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This file or at least locally below might benefit from opening Semantics

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My biggest question with the PR is the what the medium term plan for semantics is. Naming-wise it's a bit confusing semantics defines the AST of the language. I would expect it to just be typechecking, elaboration, dynamics. But that's a huge change.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we could put term files in a separate target, but not clear to me what we gain from that at the moment. i look at this change as a first-order movement to obtain some basic directional separation between hazel-the-language and hazel-the-editor, motivated partially by thinking through clarifying projector versus tylr dependencies. alternatively, we could call this library language.

more broadly, i'm trying to iteratively clarify the overall structure of the codebase. it's not obvious to be the current web/core division makes sense, even in principle. increasingly i feel like we're going to want multiple components which can interact with the 'language server', and theses components may have tightly integrated backends and frontends, where the backend refers to some edit action calculi specific to how their UI is surfaced to the user. these components might reasonably decide to divide internally into front and back build targets, particularly if they want to support multiple frontends, but this feels different to be than enforcing a front-back distinction on the codebase entire. but the big incoming question i think is how grove fits in

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think language ic clearer but I might be being pedantic.

we could put term files in a separate target, but not clear to me what we gain from that at the moment.

I don't think it's tenable/necessary know but long term I think the menhir parser, and tylr could only depend on the AST and not the semantics. It's also beneficial from an enforced separation of concerns standpoint.

it's not obvious to be the current web/core division makes sense, even in principle. increasingly i feel like we're going to want multiple components which can interact with the 'language server', and theses components may have tightly integrated backends and frontends, where the backend refers to some edit action calculi specific to how their UI is surfaced to the user. these components might reasonably decide to divide internally into front and back build targets, particularly if they want to support multiple frontends, but this feels different to be than enforcing a front-back distinction on the codebase entire. but the big incoming question i think is how grove fits in

I agree there's multiple concerns here. My main medium term priority is to have a build of tylr/semantics/syntax minus projectors so that we can run the non-web parts of hazel without the js of ocaml requirement. I don't think it requires fully separating the frontend/backend divide. For any components where we can inject their dependencies so that they can be tested or run on the backend.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

i went through and update dependencies somewhat; a lot of the tests depend purely on semantics now. probably breaking makterm and expToSeg out would do most of the rest?

Comment on lines +12 to +17
let consistent = (s, s') =>
switch (s, s') {
| (Any, _)
| (_, Any) => true
| _ => s == s'
};
Copy link
Contributor

@7h3kk1d 7h3kk1d Apr 18, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we just add deriving eq to t and make consistent equal to equals?

Comment on lines +19 to +26
let to_string =
fun
| Any => "Any"
| Pat => "Pat"
| TPat => "TPat"
| Typ => "Typ"
| Rul => "Rul"
| Exp => "Exp";
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can derive this using ppx_variants_conv.

open Haz3lcore;
open Semantics;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there anything clashing if we open both?

Comment on lines +4 to +7
//TODO(andrew): ...
module Secondary2 = Secondary;
open Semantics;
module Secondary = Secondary2;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this a intermediate step while you're seeing if you can remove Semantics.Secondary? Otherwise I don't see why they can't be aliases.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants