diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-10-30 19:24:29 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-10-30 19:24:29 -0400 |
| commit | 9f4911d5a10d06b2a78262c0ba81a1540570c56c (patch) | |
| tree | be70db0946ded2bfb39e288a94e42e0fd93bf5fa /.gitignore | |
| parent | 47d73a9f76ed16ec2ca719f60d717ec9e16eef86 (diff) | |
Refactor/generalize some pipeline definitions/proofs
When we do rewriting after casts, we will need to do extra passes of DCE
and subst01 to fully reduce things, so we generalize some of the interp
proofs over cast behavior.
For ease of rewriting, we make [ident.interp] an alias (notation) for
[ident.gen_interp], rather than a [Definition].
We also factor out the rewriting wrapper inside the pipeline module into
its own definition.
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 51f1d10ce..a832118d6 100644 --- a/.gitignore +++ b/.gitignore @@ -45,6 +45,8 @@ nra.cache /time-of-build-pretty.log /time-of-build.log +/*.out + # compilation outputs /*.o etc/tscfreq |