dijkstracula / irving

there's no checking like bounded model checking
GNU Affero General Public License v3.0
1 stars 0 forks source link

Better post-parsing errors #48

Closed dijkstracula closed 1 year ago

dijkstracula commented 1 year ago

Currently parse errors are good, thanks to pest:

➜  irving git:(main) ✗ cargo run ~/school/phd/projects/ivy_synthesis/sandbox/chainrep.ivy extract ivy
    Finished dev [unoptimized + debuginfo] target(s) in 0.03s
     Running `target/debug/irving /Users/ntaylor/school/phd/projects/ivy_synthesis/sandbox/chainrep.ivy extract ivy`
Error:   --> 36:18
   |
36 |     alias byte = uint[8]
   |                  ^---
   |
   = expected builtin_type
➜  irving git:(main) ✗

But any semantic error like a typechecking error is terrible.

➜  irving git:(main) ✗ cargo run programs/200_chainrep.ivy extract java 2>&1 | tail -n1
Error: Sort Number mismatches SortVar(44)
➜  irving git:(main) ✗

This of course sucks. We don't have source file/line number info and certainly nothing like annotated snippets. The main problem is that our AST has no way of associating a node / subtree with a parser span. This should change.

Things to do:

[x] Accumulate an Rc in pest_consume::Node, which is our current program source; [] Modify TypeError to not hold any AST nodes, since Rc is not Sync and anyhow requires that it is [] Annotate leaf nodes / terminals of the AST with a parser span [] merge spans up the AST for non-terminals.

dijkstracula commented 1 year ago
➜  irving git:(main) cargo run -q programs/200_chainrep.ivy extract ivy
Typechecking error: Unbound variable end at:
   |
 1 | #lang ivy1.8
 2 |
 3 | #
 4 | # Use a strategy called "chain replication" to maintain a consistent
...
90 |             ensure forall P1:pid,P2:pid, I. msg_count = 0 ->
91 |                 host(P1).contents.end = host(P2).contents.end &
   |                                   ^^ here
   |
➜  irving git:(main)

This is good enough for the moment. It's far from complete but we can fault in spans for more parts of the AST as we come across them.

One thing that I would like to do is contemplate what we'd need in order to have more than one annotation for an error: for instance, for a "assign the wrong sort to a value" error, it'd be nice to point back to the original definition in the source. Probably just minor refactoring, and not important, but would be Pleasing.