Skip to content
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

Use Editor code to show outputs as well as inputs #1297

Draft
wants to merge 19 commits into
base: remove-dhexp
Choose a base branch
from

Conversation

Negabinary
Copy link
Contributor

@Negabinary Negabinary commented Apr 30, 2024

Editor Componentization

Motivation:

The goal of this refactor is to turn Haz3lWeb into a series of re-usable components. There is both a short-term, and long-term motivation to do this:

In the short-term, being able to re-use the editors, and statics highlighting in particular will allow us to select / edit outputs. This is important for the interactions that will be in the proof stepper but also for the flexibility to copy results back into code etc.

In the long-term, this componentization gets us closer to good coding practices in the hazel codebase. It creates a separation of concerns where each component can consider only its local state/updates, instead of needing to worry about global state/update.

image

Strategy:

Each component is a file that contains four modules:

  • Model: stores the model of this component, along with initializers and serialization methods
  • Update: gives the available actions on this component, and functions that perform those actions. There is also a function to re-calculate all the dependent data.
  • Selection: has methods for working out which editor on a screen is currently "active" and dispatches key events to the correct place
  • View: has methods for viewing the model and connecting up actions to the correct update.

Old Description:

Motivation:

Currently there are two different ways to print code on a screen, 1) the editor for editable expressions and examples, 2) the pretty printer for outputs. In this PR we want to use (1) to print both, this will allow us to select / edit outputs in future PRs (which will be particularly useful in proofs)

The main complexity this PR adds is that there is no longer a flat fixed list of zippers, but there can now be any number of zippers in a stepper or in results too. We solve this by creating a selection type that specifies where within the model the
 

Implementation Strategy

I'm currently imagining a two-step process:

  1. Take an expression and insert necessary parentheses
  2. Take an expression with parentheses and pretty print it into layout

For (2) we can borrow a lot of ideas from the current pretty printer

Progress

Converting outputs back to editors

  • Parenthesizer
    • Expression parentheses
    • Pattern parentheses
    • Type Parantheses
  • Expression to layout
  • Tidy up precedence code

Recreate the old stepper in this system

  • Highlighting eval contexts
  • Update on click
  • Highlight previous eval contexts
  • substitution strikethroughs?

Current bugs

  • Editors don't serialize right
  • Editor doesn't update with changes
  • Stepper doesn't update with changes
  • There's no way to step
  • TyDi is broken and thus disabled
  • In exercises mode, you can click on hidden tests and then edit them

All of these print weirdly:

  • 6/0 {6/6}
  • ?$$? {? ? ?}
  • 0.000000000000000000001 {1e-21}
  • `f() {split_kids index out of bounds}
  • () {split_kids index out of bounds}
  • let (a,b,c) = (1,2,3) i {invalid argument List.map2}
  • (fun (a,b) -> ?)(1,_ {invalid argument List.map2}
  • test 1 {Unhandled exception}
  • 1:: {invalid argument List.map2}
  • [1,2,3]@[4,5,6] {invalid argument List.map2}

check that I haven't broken:

  • Assistant / Resetting Assistant
  • School mode secrecy

@Negabinary Negabinary changed the base branch from dev to remove-dhexp April 30, 2024 20:20
@Negabinary Negabinary linked an issue May 1, 2024 that may be closed by this pull request
@Negabinary Negabinary mentioned this pull request May 1, 2024
43 tasks
@Negabinary Negabinary linked an issue May 2, 2024 that may be closed by this pull request
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.

Persist unbound type variables into Typ.t and show Make it possible to navigate through a DHExp with cursor
1 participant