nikomatsakis/rust-redex — pull request #3 by anasazi (2014-03-12 07:06:45+00:00)
Title: Initial iteration of typing judgment

My plan for achieving a typing judgment is to start with a tiny part of the language, push it all the way through (typing, evaluation, checks for progress+preservation, etc.), and then add features individually (making sure they can get through the whole system) until the typed version reaches parity with Patina.

This initial part is *super* basic: integers, addition, variables, assignment, statement sequencing, shallow destruction, and blocks. I'm using a sequencing statement rather than a redex list of statements because I found it was easier to write judgments that threaded the heap along statements that way. Same thing goes for variable contexts. I merged blocks with statements to avoid having mutually recursive judgments (I'm not sure if PLT Redex even supports them and it was easy enough to merge that I didn't bother looking).

Currently, the typing judgment ensures both that all variables are destructed before they go out of scope (by requiring the scope after a block to be a subset of the scope before) and that they cannot be used after destruction (by removing the variable from the context after destruction).

Known issues:
- raises a PLT redex error when using an undefined variable rather than simply failing to typecheck (no clause matches the case because I wasn't sure what to return)

TODO list:
- evaluation, progress, and preservation for existing stuff
- unique pointers (~ ty, new lv)
- structs + partial destruction (struct types and expressions, destroy x.a)
- references (& and *, lifetime and mutability checking)
- enums (enum types and expressions, match)
- vectors + DST (vec, pack)
- functions