Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Remove the bits of the new reflective pipeline in master | 2017-04-02 | |
| | | | | This way, we can keep all of new pipeline code together in the PR | ||
* | Remove all the .v files in SpecificGen | 2017-04-02 | |
| | | | | This gets most of the way to 10 in #14. | ||
* | More extensive comment in NewBaseSystem | 2017-04-02 | |
| | | | | As per Andres' request on #138. | ||
* | Work around bug #5434 | 2017-04-02 | |
| | | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5434, [vm_compute] breaks an invariant asserted on line 115 of pretyping/constr_matching.ml. This was triggering whenever we tried to reify one of the operations. | ||
* | Coalesce Tuple.pointwise2 and Tuple.fieldwise | 2017-04-02 | |
| | | | | | | We don't need both of them. We keep the definition of pointwise2 because it's needed for reification to work, and we keep the name of fieldwise because it's used in more places. This closes #137. | ||
* | Generalize Z.InterpInlineConst | 2017-04-02 | |
| | |||
* | Better version of inversion_ProcessedReflectivePackage | 2017-04-02 | |
| | | | | Now it doesn't introduce needless dependencies | ||
* | Add inversion_ProcessedReflectivePackage | 2017-04-02 | |
| | |||
* | Add PreDefinitions pipeline file | 2017-04-02 | |
| | |||
* | Add Z instantiations of InlineConst | 2017-04-02 | |
| | |||
* | Add Z.Bounds.MapCastByDeBruijn instantiation | 2017-04-02 | |
| | |||
* | Add Z instantiation of MapCastByDeBruijnInterp | 2017-04-02 | |
| | |||
* | Add reflective_interp rewrite db | 2017-04-02 | |
| | |||
* | Rewrite in Op arguments before rewriting in Op | 2017-04-01 | |
| | | | | This fixes the rewriter to actually simplify deeply nested expressions. | ||
* | Also do eta under lets in Reflection/Eta.v | 2017-04-01 | |
| | |||
* | Add an initial glue file in the pipeline, no option in bounds | 2017-04-01 | |
| | | | | | | | We can do bounds analysis without options. Also, add some tactics from another branch for the glue to start the reflective pipeline. | ||
* | Fix definition of BoundedWord | 2017-04-01 | |
| | | | | | | | We need to take log2, because wordT takes lg(wordsize). We need to pass None rather than Some, because None means "the original output type of the function we're reifying is a tuple of Z" (as opposed to a tuple of words), which is the situation we're in. | ||
* | Split off BoundedWord.v from IntegrationTest.v | 2017-04-01 | |
| | |||
* | Add back word hex constant notations | 2017-04-01 | |
| | |||
* | Add RenameBinders | 2017-04-01 | |
| | | | | | It will someday allow for nicely named PHOAS binders (conditional on https://coq.inria.fr/bugs/show_bug.cgi?id=5414 being solved). | ||
* | Add wf proof for arithmetic simplifer | 2017-04-01 | |
| | |||
* | Fix a name (sprurious interp) | 2017-04-01 | |
| | |||
* | Add interp proof for arithmetic simplifier | 2017-04-01 | |
| | |||
* | Handle inversion of homogenous products in reflective type inversion | 2017-04-01 | |
| | |||
* | Add an arithmetic simplifier | 2017-04-01 | |
| | |||
* | Add correctness of Rewriter | 2017-04-01 | |
| | |||
* | Add Reflection/Rewriter.v | 2017-04-01 | |
| | |||
* | Split out Tactics.SubstLet | 2017-04-01 | |
| | |||
* | Remove trailing whitespace in NewBaseSystem | 2017-04-01 | |
| | |||
* | Add Tuple.eta | 2017-04-01 | |
| | |||
* | insert a reduce step in the correct place of the carry chain | 2017-04-01 | |
| | |||
* | Alter relax_output_bounds statement | 2017-04-01 | |
| | | | | It needs to fit the actual statement of MapBounds correctness | ||
* | Add a bounds relaxation lemma | 2017-03-31 | |
| | |||
* | Add Z.log2_up_le_pow2_full | 2017-03-31 | |
| | |||
* | Fix inversion_base_type | 2017-03-31 | |
| | |||
* | Add inversion_base_type for Z.Syntax.base_type | 2017-03-31 | |
| | |||
* | Add Bounds.is_tighter_thanb | 2017-03-31 | |
| | |||
* | Use a better order of arguments for Bounds.is_bounded_by | 2017-03-31 | |
| | | | | This lines up with conventions that we use elsewhere | ||
* | Add is_tighter_than_bool to zrange | 2017-03-31 | |
| | |||
* | More compatibility for etransitivity | 2017-03-31 | |
| | |||
* | Add [change_with_curried] to Curry.v | 2017-03-31 | |
| | |||
* | Add [etransitivity y], [etransitivity_rev] tactics | 2017-03-31 | |
| | |||
* | use improved fsatz on various elliptic curve things | 2017-03-31 | |
| | | | | | | | | partial correctness of projective addition stronger projective addition proof fixup | ||
* | Add a comment explaining bounds_exp | 2017-03-30 | |
| | |||
* | Add wordToZ{_gen,}_range | 2017-03-30 | |
| | |||
* | Update IntegrationTest with actual bounds | 2017-03-30 | |
| | | | | Also make mulZ not opaque. | ||
* | Start instantiating MapCastByDeBruijn in Z/ | 2017-03-30 | |
| | |||
* | Created test file for newbasesystem/word-size-selection integration | 2017-03-30 | |
| | |||
* | turn [Let]s into [Definition]s so they persist after the section | 2017-03-30 | |
| | |||
* | Reorder arguments to Wf_MapCast for eauto | 2017-03-30 | |
| | | | | This way we pick up the equality hypothesis first. |