Editor Componentization

[Negabinary]

Editor Componentization

Warning: this is a huge change to the Haz3lweb portion of the codebase. I've tried to provide a guide below for merging this into your branch.

There are more details in docs/ui-architecture.md.

Motivation:

The goal of this refactor is to turn Haz3lWeb into a tree of re-usable, independent 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.

The Big Changes

• A lot of files in Haz3lweb have moved. I'm hoping git will handle this automatically.

• Model.re, UpdateAction.re and Update.re have been deleted. Each component of the UI now has its own Model and Update modules. If you had added any actions to UpdateAction.re, you will now want to add them to the Update module of the component in the ui tree "where the action takes place".

• DHDoc_Exp, and other functions for printing dynamic expressions are gone. Anything that was previously output that way will need to be output using one of the following:

  • new syntax in user expressions (e.g. users can now type fix, but this allows us to show them in output)
  • static errors (e.g. failed casts are now shown using static type errors in the results)
  • or wait until Leaf Projectors #1218 is merged in (e.g. we'll use projectors to hide functions when projectors are merged in)

Design:

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.

Pre-existing Dev bugs which became more obvious

• fixpoint constructor bug ( Fixpoints in SynFun position create static errors #1299 )

let odd: Int -> Bool =
 fun n -> if n == 0 then true else odd( ) 
in odd(5)

• types are wrong for function variables post-elaboration ( Elaboration of functions doesn't preserve types #1432 )

let f : Int -> Int = fun x -> x in
f

• shouldn't say odd not found in: ( Closures around indet expressions disappear #1431 )

let odd: Int -> Bool =
 fun n -> if n == 0 then true else odd( ) 
in odd(5)

Wontfixes:

• Steppers don't save (doesn't seem important to save it at the moment)
• Dynamic errors don't show up (e.g. divide by zero)