Infix (misfix?) operators #14

New issue

Open

opened 2024-12-05 19:34:06 -08:00 by wball · 3 comments

wball commented

2024-12-05 19:34:06 -08:00

Owner

This together with #3 would really start making this feel like even more of a real proof assistant.

wball added the

parser

label 2024-12-05 19:47:37 -08:00

wball commented

2024-12-10 20:38:23 -08:00

Author

Owner

f9e0ec40bd got this started, allowing for basic custom infix operators, but there's still more work to do.

Update the documentation.
Rethink how symbols and identifiers are parsed (feels very janky right now).
Update the pretty printer/Expr to remember and respect fixity declarations.
Implement section/operator syntax from Haskell? Some kind of operator syntax at least would be helpful.
Update the tree-sitter parser

f9e0ec40bd got this started, allowing for basic custom infix operators, but there's still more work to do. - [x] Update the documentation. - [ ] Rethink how symbols and identifiers are parsed (feels very janky right now). - [ ] Update the pretty printer/`Expr` to remember and respect fixity declarations. - [x] Implement section/operator syntax from Haskell? Some kind of operator syntax at least would be helpful. - [x] Update the tree-sitter parser

wball commented

2024-12-10 23:39:18 -08:00

Author

Owner

Basic Haskell operator syntax added in e6f9d71c57, but we'll have to wait for type inference in #2 to get full operator sections.

Basic Haskell operator syntax added in e6f9d71c57, but we'll have to wait for type inference in #2 to get full operator sections.

wball commented

2024-12-13 22:12:24 -08:00

Author

Owner

Found a bug: fixity declarations are not respected in the REPL. Will probably want the parser wrapper to return the state as well (i.e. switch to runStateT from evalStateT), so the REPL can use that state when parsing commands.

Found a bug: fixity declarations are not respected in the REPL. Will probably want the parser wrapper to return the state as well (i.e. switch to `runStateT` from `evalStateT`), so the REPL can use that state when parsing commands.