Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Ask for leb on op codes and base types, not flat types | 2017-04-14 | |
| | |||
* | Add support for cse-modulo-normalization | 2017-04-14 | |
| | |||
* | SOp needs to hold the type of the arguments, for denote | 2017-04-12 | |
| | |||
* | Hold types in SFst and SSnd | 2017-04-12 | |
| | | | | Needed for writing denote | ||
* | Extend cse context when inlining | 2017-04-11 | |
| | |||
* | Generalize prepend_prefix | 2017-04-10 | |
| | |||
* | Reorder parameters for ease of partial instantiation, add symbolic_expr_dec | 2017-04-10 | |
| | |||
* | Fix CSE to correctly symbolize expressions | 2017-04-10 | |
| | | | | | | The ones using variables from different parts of the same let-binder were getting stored as a reference to the let-binder, and losing information about which component they were in. | ||
* | Key on flat_type not base_type, in CSE | 2017-04-10 | |
| | | | | | | Using [lookup] and [extend] was causing issues in proving wf, and they were unnecessary. It's fine to treat each flat_type as a unit, because we'll never be looking for a projection of an expression in the context. | ||
* | Use Named.Context in CSE, so we can reuse context lemmas | 2017-04-10 | |
| | |||
* | rename-everything | 2017-04-06 | |