-
Notifications
You must be signed in to change notification settings - Fork 61
Dynamic typing feedback into static marking #1988
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
base: dyntype-proj
Are you sure you want to change the base?
Conversation
Added DynamicStatics module for type mapping and integrated ~dynamics parameter across statics functions in Statics.re, Info.re, and CustomStatics.re. This enables dynamic type lookups and overrides in expression derivation, enhancing type inference with runtime-like information for better debugging and analysis.
- Introduce dynamic_info_map and dynamic_error_ids to CachedStatics for handling dynamic analysis - Update CodeWithStatics to filter and display dynamic errors separately from static ones - Modify Arms.Errors module to support dynamic error styling and rendering - Enhance editor UI to show dynamic error decorations alongside static ones for improved code feedback
Add a new `dynamic_feedback` boolean setting to core language settings, allowing users to toggle dynamic error and info computation in the code editor. This feature conditionally enables/disables dynamic statics calculation based on user preference, improving performance and user control. Updated related UI components, shortcuts, and menu for seamless integration.
- Introduce `~probe_unknowns` flag in `Elaborator.elaborate`, `elaborate_pattern`, and `uexp_elab` functions to conditionally enable probing for unknown types in expressions and patterns. - Update `CachedStatics.elaborate` to accept and pass the flag, using `settings.dynamic_feedback` as the value. - Modify CLI and test files to explicitly set `~probe_unknowns=false` for consistent behavior. - This change allows fine-grained control over elaboration behavior, improving flexibility for handling unknown types without always triggering probes.
- Introduce `dynamic_info` field to cursor type in Cursor.re for tracking dynamic information - Update CodeWithStatics.re to compute and include dynamic info from statics map - Modify CursorInspector.re to prioritize and display dynamic errors over static info, improving user feedback on runtime issues
Changes `calculate_dynamic_type` in derived functions across Info.re, CustomStatics.re, and Statics.re from returning plain Typ.t to option(Typ.t). This prevents using invalid types when errors exist in the map, providing a fallback via Option.value with Unknown(Internal) | Typ.temp.
Replace Typ.consistent_join with Typ.join_all in dynamic type calculations across TypeProj.re, Info.re, and CursorInspector.re. This change improves type joining robustness by handling empty lists with a temporary unknown type, addressing potential inconsistencies in dynamic type inference. Simplify CursorInspector by directly using Info.ty instead of computing from closures.
Add optional `is_dynamic` parameter (defaulting to false) to `view`, `view_segment`, `view_typ`, and `view_any` functions in CodeViewable.re to enable distinguishing dynamic elements in code rendering. Updated the CodeWithStatics.re view call and Arms.Errors.of_ids invocation to pass the required parameters, ensuring compatibility with dynamic features in the Haz3l editor.
6931e86 to
9cff4f4
Compare
61f1237 to
dc89770
Compare
c439145 to
c002301
Compare
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## dyntype-proj #1988 +/- ##
================================================
+ Coverage 49.92% 49.99% +0.06%
================================================
Files 221 222 +1
Lines 23285 23530 +245
================================================
+ Hits 11626 11763 +137
- Misses 11659 11767 +108
🚀 New features to boost your workflow:
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Pull Request Overview
This PR implements dynamic feedback in the Hazel editor, which displays runtime type information from evaluation to help users identify type errors discovered during execution. The feature allows types computed at runtime to be displayed alongside static types, with visual differentiation for dynamic errors.
Key Changes:
- Adds a "Dynamic Feedback" toggle in settings to enable/disable the feature
- Implements dynamic type inference by running statics on runtime values captured during evaluation
- Adds visual styling for dynamic errors with animated decorations to distinguish them from static errors
Reviewed Changes
Copilot reviewed 40 out of 40 changed files in this pull request and generated 8 comments.
Show a summary per file
| File | Description |
|---|---|
| test/evaluator/Test_Evaluator_DynamicFeedback.re | New test file verifying dynamic feedback computation for complex expressions |
| test/evaluator/Test_Evaluator_Probe.re | Adds test for probe functionality on constructor patterns |
| test/evaluator/Test_Evaluator.re | Registers new dynamic feedback test suite |
| src/web/www/style/variables.css | Adds CSS variable for dynamic error stroke color |
| src/web/www/style/editor.css | Adds styling and animations for dynamic errors and formatting improvements |
| src/web/www/style/cursor-inspector.css | Adds styling for dynamic error state in cursor inspector |
| src/web/view/TutorialMode.re | Updates to extract values from Calc types and adds dynamic_statics field |
| src/web/view/NutMenu.re | Adds Dynamic Feedback toggle to settings menu |
| src/web/view/ExerciseMode.re | Updates to handle Calc-wrapped dynamics and dynamic_statics |
| src/web/util/WorkerServer.re | Wraps evaluation in timing measurement |
| src/web/util/WorkerClient.re | Increases worker timeout from 20s to 60s |
| src/web/app/inspector/CursorInspector.re | Implements dynamic type display and comparison in inspector |
| src/web/app/input/Shortcut.re | Adds keyboard shortcut for toggling dynamic feedback |
| src/web/app/helpful-assistant/ChatLSP.re | Adds empty dynamics parameter to statics calls |
| src/web/app/explainthis/ExplainThis.re | Adds dynamic_statics field initialization |
| src/web/app/editors/stepper/*.re | Wraps empty dynamics maps in Calc.OldValue |
| src/web/app/editors/result/EvalResult.re | Refactors dynamics extraction from result to use Calc |
| src/web/app/editors/decoration/Arms.re | Adds is_dynamic parameter for rendering dynamic error decorations |
| src/web/app/editors/code/*.re | Implements dynamic statics calculation and rendering |
| src/web/app/editors/cell/CellEditor.re | Adds dynamic_statics field to model |
| src/web/app/Cursor.re | Adds dynamic_info field to cursor type |
| src/web/Settings.re | Adds dynamic_feedback boolean setting |
| src/util/Calc.re | Adds map function for transforming Calc values |
| src/language/term/Typ.re | Refactors diff function to use helper for collecting all IDs |
| src/language/statics/*.re | Threads dynamics parameter through statics and adds dynamic type computation |
| src/language/dynamics/transition/PatternMatch.re | Handles pattern matching with probed constructors |
| src/language/CoreSettings.re | Adds dynamic_feedback setting to core settings |
| src/haz3lcore/projectors/implementations/TypeProj.re | Updates to use join_all instead of consistent_join |
| src/haz3lcore/derived/CachedStatics.re | Adds dynamic_info_map and dynamic_error_ids fields |
Comments suppressed due to low confidence (1)
src/language/statics/Statics.re:1
- The ~expected_labels parameter is missing from this uexp_to_info_map call, while other similar calls in the same function include it. This inconsistency should be verified and corrected to ensure consistent behavior.
/* STATICS.re
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| /* These are very simple tests to make sure we're not | ||
| doing exponential blowup in the evaluator */ |
Copilot
AI
Nov 4, 2025
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The comment describes preventing 'exponential blowup in the evaluator,' but the test is actually about dynamic in-editor feedback functionality, not performance. The comment should be updated to accurately describe the purpose of these tests.
| @keyframes stroke-pulse { | ||
| 0%, 100% { stroke-dashoffset: 0; opacity: 1; } | ||
| 50% { stroke-dashoffset: 4; opacity: 0.7; } | ||
| } |
Copilot
AI
Nov 4, 2025
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The magic number '4' for stroke-dashoffset should be defined as a CSS variable (e.g., --dynamic-error-pulse-offset) for maintainability and consistency with the rest of the codebase.
src/language/statics/Statics.re
Outdated
| ~calculate_dynamic_type= | ||
| uexp => { | ||
| let (ie, m) = | ||
| uexp_to_info_map(~ctx, uexp, StaticsBase.Map.empty); |
Copilot
AI
Nov 4, 2025
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Missing ~dynamics parameter in uexp_to_info_map call. The function signature requires ~dynamics as indicated by other calls in the same file. This will cause a compilation error or incorrect behavior.
| uexp_to_info_map(~ctx, uexp, StaticsBase.Map.empty); | |
| uexp_to_info_map(~dynamics, ~ctx, uexp, StaticsBase.Map.empty); |
| let get_ids = () => { | ||
| let ids = ref([]); | ||
| let _ = | ||
| Grammar.map_typ_annotation( | ||
| (t: IdTagged.IdTag.t) => { | ||
| ids := t.ids @ ids^; | ||
| t; | ||
| }, | ||
| ty': t, | ||
| ); | ||
| ids^; | ||
| }; |
Copilot
AI
Nov 4, 2025
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The variable name 'get_ids' is misleading as it's a function that mutates a ref rather than just 'getting' IDs. Consider renaming to 'collect_all_ids' or refactoring to avoid the mutable ref pattern.
| : statics; | ||
|
|
||
| let ctx_init: Language.Ctx.t = Language.Builtins.ctx_init(Some(Int)); | ||
| // This should be a fold over the dynamics map getitng the type for each value |
Copilot
AI
Nov 4, 2025
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Corrected spelling of 'getitng' to 'getting'.
| // This should be a fold over the dynamics map getitng the type for each value | |
| // This should be a fold over the dynamics map getting the type for each value |
Extract the inline `calculate_dynamic_type` function into a shared method in the `ExpressionStatics` module to eliminate code duplication and centralize the logic for determining dynamic types in static contexts. This refactor improves maintainability by reducing repetitive code across CustomStatics and Statics modules.
Add optional warning parameter to toggle_named widget to display⚠️ icon with tooltip for cautioned settings. Updated settings menu to include performance warning for "Dynamic Feedback" toggle, informing users of potential slowdowns. This enhances user experience by providing upfront guidance on resource-intensive features.
|
Move the lightning bolt in the error message to the right side of the cursor inspector |
Dynamic Feeback
This PR adds a new toggleable feature that provides in-editor type feedback based off the runtime dynamic types observed in program execution. It accomplishes this by running the program and probing any expression with a statically unknown type. Then re-running statics with t he additional typing information.
Example
Screencast.From.2025-11-18.13-45-45.webm
Probe selection
The implementation is integrated with the
Probepinning system so it's possible to get dynamic types for specific function applications by pinning a specific function application in the probe system.Screencast From 2025-11-18 13-53-21.webm
Todos
(typfun a -> fun x : a -> x)@<String>("")should not give a dynamic error on x