Refactor type environment and unique identifier checks #184
Conversation
atomb
left a comment
There was a problem hiding this comment.
This seems like a good change to me. And I've checked on some large examples that it doesn't slow down type checking.
| substitution and fresh variable generation, and a `KnownTypes` to track the | ||
| supported type constructors. It also has type information about a | ||
| factory of user-specified functions, which is used during type checking. | ||
| supported type constructors. |
There was a problem hiding this comment.
I think this comment is outdated - it does not use TState anymore, and also it isn't a stack of contexts (but this had existed even before this PR).
|
Actually, I think that after this patch |
Yes, I see what you mean. This PR was a combination of splitting up the |
|
Thanks for confirming - I made #190. :) |
…te` to `TState` (#190) *Description of changes:* #184 factored out members in `structure TEnv` that don't change during typing. This made `TState` somewhat less useful because (1) its `TGenState` member is already included in `TGenEnv` and (2) type substitution info is already in `TEnv`. Considering that `TEnv` is still the top-level data structure that is passed around typing functions, whenever one wants to use `TState`, `TEnv` can be used instead. The diff of this PR indeed shows that the data structure was redundant and every use case through `.state.substInfo` could be replaced with `stateSubstInfo`. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Description of changes:
This PR makes 3 main changes:
Identifiers.lean) for checking dupliates more efficiently (with a hash table rather than a list)LContext, which provides contextual information that does not change during Lambda typechecking (Factory,KnownTypes, and identifiers), andTEnv, which does (inferred types, substitutions, etc).ProgramType.lean. In particular, this no longer requires a separate check fornodupsin the Program decl list; rather, it adds each identifier to the context as it is seen, automatically checking for uniqueness. This has the effect of performing more well-formedness checks in Lambda typechecking rather than in Boogie.There are also two smaller changes:
4. Due to the above, proving that well-typed Boogie programs have unique names is no longer trivial, and this proof is added in
ProgramWF.lean.5. This PR does some other refactoring of
TEnv, splitting it into the name-generation part and the rest. This will be needed for the bounded ints and/or function precondition PR, but is not immediately needed yet.The bulk of the changes are in
Identifiers.lean,LExprTypeEnv.lean,ProgramType.lean, andProgramWF.lean.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.