Derivation trees

[GuoDCZ]

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

• [x] Port judgement type Judgement and component types Prop, Ctx to builtin functions
• [x] Write expression syntax
• [x] Port Rule type to builtin functions (Judgement, [Judgement]) -> Bool. The rule function takes conclusion and premises as input, correctness as output.
• [x] Port VerificationError to builtin errors and rewrite rule functions to (Judgement, [Judgement]) -> (). Verify failure results in dynamic error. Evaluation stops at error.
• [x] Rewrite rule functions to (Judgement, [Judgement]) -> Judgement. The output echo conclusion. This will support tree structure of derivations.
• [x] Write new pattern (a syntax sugar for function application) for derivation: der·\·of·, where · filled with any expression.
• [x] Add a enumerator to Judgement type: Verified: Verified / Wrong / Partial. The reason to introduce Partial is to allow user to check the correctness of a single derivation while the premises might not be correct/completed yet.
  • Typed judgement (without derivation) is Wrong
  • Incorrect derivation yield Wrong Judgement
  • Correct derivation with all premises Verified yield Verified Judgement
  • Correct derivation with some premises not Verified (Wrong or Partial) yield Partial Judgement
  • Derivation might enforce conclusion to be Wrong judgement
• [ ] Refactor Derivation Exercise mode integration
  • Introduce Exercise mode choice: normal & derivation
  • Better editor dynamic result acquisition and error handling
  • Exercise scoring
• [ ] Sidebar development
  • Click on rule label summon the sidebar
  • Introduction to the current rule
  • Result of the current derivation: Pending, Error, Correct, Partial…
  • Choice of rule (click on the rules to switch)
  • (future) copy & paste utility
• [ ] (future) Abbreviation Derivation
  • Click on the button (between Derivation and Prelude) compose a derivation binding
  • Sidebar can choose either rules or derivation abbreviation (legal binding)
  • Easy Copy, Paste, Cut & Delete
• [ ] (future) LaTeX Export
  • Metaprogramming: Translate plain code to latex
  • Comments act as specifiers.