hazel
hazel copied to clipboard
Derivation trees
Building educational UI for constructing rule-based derivations and integrate it into Exercises mode in Hazel.
- [x] Port judgement type
Judgement
and component typesProp
,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.