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
• Fix "re-enter" space remolding issue
• (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.
• Setup not stitched
• parens from right to left may become hole
• !! Merge Exercise.re
• 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)
• Enable PROP and EXP abbreviation in prelude & setup
  • Use hazel Exp Sort required in curly braces.
• Make the editor truly requiring a JDMT sort
• Allow ninja-keys searching rule mistype?
• Pop tree to abbr & push abbr back to tree
• Write Sort info & sort term info for ExplainThis
• Write DHDoc_common for Drv terms
• 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
• 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

Future

• [-] Undo: We only have this for each editor
• [-] Make the terms and inner token not stick with each other
• [-] Change MakeTerm Logic to not rely on Multihole
• [-] Remove DrvSyntax (avoid elab stage)
• [-] Derivation collapsing
• [-] Derivation automation
• [-] Exercise spec export & import
• [-] Label dragging
• [-] LaTeX Export by translating plain code to latex comments act as specifiers.

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

[codecov]

Codecov Report

Attention: Patch coverage is 22.17886% with 2393 lines in your changes missing coverage. Please review.

Project coverage is 46.20%. Comparing base (6df1774) to head (0c64d6d).

Files with missing lines	Patch %	Lines
src/haz3lcore/derivation/DrvTermBase.re	0.24%	411 Missing ⚠️
src/haz3lcore/pretty/ExpToSegment.re	0.28%	345 Missing ⚠️
src/haz3lcore/derivation/RuleVerify.re	2.85%	272 Missing ⚠️
src/haz3lcore/derivation/DrvTerm.re	1.81%	270 Missing ⚠️
src/haz3lcore/lang/term/Grammar.re	4.34%	220 Missing ⚠️
src/haz3lcore/statics/MakeTerm.re	4.54%	168 Missing ⚠️
src/haz3lcore/derivation/Rule.re	0.67%	147 Missing ⚠️
src/haz3lcore/dynamics/Transition.re	0.00%	117 Missing ⚠️
src/haz3lcore/statics/Statics.re	1.00%	99 Missing ⚠️
src/haz3lcore/derivation/DrvInfo.re	0.00%	88 Missing ⚠️
... and 20 more

Additional details and impacted files

@@            Coverage Diff             @@
##              dev    #1302      +/-   ##
==========================================
- Coverage   53.25%   46.20%   -7.05%     
==========================================
  Files         103      111       +8     
  Lines       10583    13625    +3042     
==========================================
+ Hits         5636     6296     +660     
- Misses       4947     7329    +2382     

Files with missing lines	Coverage Δ
src/haz3lcore/lang/Precedence.re	97.91% <100.00%> (ø)
src/haz3lcore/zipper/Ancestors.re	61.11% <100.00%> (ø)
src/haz3lcore/zipper/Relatives.re	52.27% <100.00%> (ø)
src/haz3lcore/zipper/Zipper.re	57.06% <100.00%> (ø)
src/haz3lcore/derivation/SymbolMap.re	97.91% <97.91%> (ø)
src/haz3lcore/dynamics/Casts.re	79.00% <0.00%> (-0.80%)	⬇️
src/haz3lcore/dynamics/DHExp.re	32.91% <0.00%> (-0.43%)	⬇️
src/haz3lcore/lang/Form.re	87.01% <99.10%> (+7.68%)	⬆️
src/haz3lcore/statics/Coverage.re	71.35% <0.00%> (-0.38%)	⬇️
src/haz3lcore/dynamics/Unboxing.re	21.67% <0.00%> (-0.16%)	⬇️
... and 24 more

... and 2 files 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.