Output typing map #345
Comments
|
Makes sense to me! I'm also not oppose to combining these 2 files into one, by adding the type information to the correspondent AST nodes (in the file, not in the IR). We do want to produce some human-readable dumps of the inferred types at some point. I believe the best solution for that would be to combine the pretty printed IR with the pretty printed correspondent types in some sort of annotation syntax (i.e. |
I'm not sure if this would make sense unless we wanted to use that representation in our IR. Otherwise it requires a different representation of the AST just for the purposes of serialization (at minimum, we'll have to add a field for inferred types to each node. I think we might just add an extra field to the JSON blob produced by |
Closes #215 This is introduced in a way to suggest turning to sweet-monads/either for sequencing our error-prone computations. The sequencing and composition of our top-level routines exposed by CLI is currently done via imperative early exits. This makes it hard to reason about the code in general, but also breaks our ability to compose these routines. Looking towards #345, we'll need typecheck to receive the output of parse, then add it's typing information, before finally printing to the `--out` location. This requires composing the routines while handling possible error states, and just bailing with exit codes won't work for that. Since we are already using `Either`, and since it is designed for facilitating the composition of error-prone code, I think we can massage these routines into shape with a few well-placed Either's. ;)
Closes #215 This is introduced in a way to suggest turning to sweet-monads/either for sequencing our error-prone computations. The sequencing and composition of our top-level routines exposed by CLI is currently done via imperative early exits. This makes it hard to reason about the code in general, but also breaks our ability to compose these routines. Looking towards #345, we'll need typecheck to receive the output of parse, then add it's typing information, before finally printing to the `--out` location. This requires composing the routines while handling possible error states, and just bailing with exit codes won't work for that. Since we are already using `Either`, and since it is designed for facilitating the composition of error-prone code, I think we can massage these routines into shape with a few well-placed Either's. ;)
As per recent TNT decisions, we plan to communicate specs to Apalache via (at least) two files:
Currently, afaict, we have no mechanism for obtaining (2), but we'll need that.
cc/ @bugarela, in case you have thoughts on this or I'm mistaken.
Either#357The text was updated successfully, but these errors were encountered: