Derivation trees

[GuoDCZ]

Building educational UI for constructing rule-based derivations and integrate it into Exercises mode in Hazel.

Try it here!

Bugs

• [?] Fix Remolding issue
• Fix NumLit sort-inconsistency
• Restrict var regex for each sort.
• Fix "re-enter" space remolding issue
• Change d0 to d1
• (Potential bugs) check all rules implemented yet.
  • All Rules except Bidirection
• Info Error if got comma prop not on Entail left
• Occasionally take on weird color.
• Hole does not take on Info error.
• (potenital) Should verification start from Concl or Prems or either.
  • Fix by rebase how we verify
• Handle let pair bind to same var error
• Handle plus concatenation for type.
• Instructor mode not allowed to add abbr below
• For E-fix, E-fun, E-let, ann should be optional. Need separate request type.

Backend

• Proposition derivation sementic
  • Port judgement type Judgement and component types Prop, Ctx to builtin functions
  • Introduce /\, \/, ==>, |- operator
• Refactor Derivation Exercise mode integration
  • Introduce Exercise mode choice: Programming & Proof
  • Separate model mapping and code manipulation.
• Sorts for ALFA (Judgement, Ctx, ALFAExpr, ALFATyp, ALFAPat, ALFATPat)
• Undo: We only have this for each editor
• Enable PROP and EXP abbreviation in prelude & setup
  • Use hazel Exp Sort required in curly braces.
  • Fix Jdmt abbr failure
  • Rewrite remolding (A new sort exists in Drv Sort family)
• Make the editor truly requiring a JDMT sort
• Make the terms and inner token not stick with each other
• Allow ninja-keys searching rule mistype?
• Change MakeTerm Logic to not rely on Multihole
• Pop tree to abbr & push abbr back to tree
• Derivation collapsing
• Derivation automation
• Exercise spec export & import
• Write Sort info & sort term info for ExplainThis
• Write DHDoc_common for Drv terms
• LaTeX Export by translating plain code to latex comments act as specifiers.
• [?] refactor all I have written (not really)
• [?] refactor exercise mode

Frontend

• Hover above rule label summon the choice panel
• Result of the current derivation: Pending, Error, Correct
• Click on the rules to switch
• Add/Del premises button
• Add/Del abbr button
• Derivation exercise scoring scheme
• Click on the button (between Derivation and Prelude) compose a derivation binding
• In choice panel we can choose either rules or derivation abbreviation (legal binding)
• Show error messages in the side bar
• Show rule definitions in sidebar
• Make dots show only on hover using crazy CSS selector
• Label dragging
• Move popup menu to above and change the btn to summon Explainthis
• Re-style Cells, many be each for a abbreviation, and show the whole result at the bottom of the cell
• Re-style add abbreviation btn by tip words

*This is not an outline of my progress, but like a memo