Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Compatibility after Coq PR#262. | 2018-05-14 | |
| | | | | | | | | | Coq PR#262 makes the inference of return clauses more uniform and general but unification is sometimes not strong enough to deal with this generality. See #5107 for details. One reduces the search space for a return clause by forbidding it to be obtained by small inversion. | ||
* | finish pushing through changes to dummy and factor out identifier match | 2018-05-07 | |
| | |||
* | replace dummy_var with dummy_arrow and change style of straightline tests to ↵ | 2018-05-07 | |
| | | | | be more robust | ||
* | clean up shared notations and constant-rewriting logic for prefancy | 2018-05-07 | |
| | |||
* | prefancy now works on barrett (modulo add-opp=>sub) | 2018-05-07 | |
| | |||
* | Move straightline and prefancy stuff above barrett reduction | 2018-05-07 | |
| | |||
* | Translating to 'pre-fancy' form now works on Montgomery | 2018-05-07 | |
| | |||
* | move depth to a more sensible location | 2018-05-07 | |
| | |||
* | Translation to straightline code now works correctly on montgomery256 | 2018-05-07 | |
| | |||
* | Translation to straightline code (first attempts, mostly working) | 2018-05-07 | |
| | |||
* | fix the placement of a dlet to make more sense | 2018-05-07 | |
| | |||
* | Backtrack on moving a notation to Notations.v, to fix conflict | 2018-05-06 | |
| | |||
* | Fix notations to not conflict with bbv | 2018-05-06 | |
| | |||
* | More reserved notations | 2018-05-06 | |
| | |||
* | Add another notation | 2018-05-06 | |
| | |||
* | Fix a typo in last commit | 2018-05-06 | |
| | |||
* | Add a reserved notation for #v | 2018-05-06 | |
| | |||
* | Don't use vm_compute with existentials | 2018-05-05 | |
| | |||
* | Update comment | 2018-05-05 | |
| | |||
* | Fully finish flat_map | 2018-05-05 | |
| | |||
* | Fix flat_map | 2018-05-05 | |
| | |||
* | WIP on lists as cons cells | 2018-05-05 | |
| | |||
* | Remove vinterp_arrow function | 2018-05-05 | |
| | |||
* | Revert "WIP on inductive base_value" | 2018-05-05 | |
| | | | | This reverts commit e38faaac1d3996c61d396144e20b8bb41809a253. | ||
* | WIP on inductive base_value | 2018-05-05 | |
| | |||
* | Revert "WIP with andres, not working pattern language" | 2018-05-05 | |
| | | | | This reverts commit 2fcf4cd6aabebb3b68cc0a807e5d7c78e9142cb5. | ||
* | WIP with andres, not working pattern language | 2018-05-05 | |
| | |||
* | Add comment about leaky abstraction | 2018-05-05 | |
| | |||
* | Split off specialization to base types from specialization to idents | 2018-05-05 | |
| | |||
* | make update-_CoqProject | 2018-05-05 | |
| | |||
* | Add type variables / substitutions | 2018-05-05 | |
| | | | | This allows more genericness in the ident-specific code | ||
* | Change some notations for more readability by Andres | 2018-05-05 | |
| | |||
* | Update cast -> annotate | 2018-05-05 | |
| | |||
* | Parameterize over types and identifiers | 2018-05-05 | |
| | |||
* | Add notes | 2018-05-05 | |
| | |||
* | Add partial evaluation | 2018-05-05 | |
| | |||
* | Some experiments with partial evaluation with letin without cps | 2018-05-05 | |
| | | | | Jason & Andres | ||
* | Bump versions of Coq we test on travis | 2018-05-02 | |
| | | | | | Now we test master, v8.8.dev, v8.7.dev, 8.8.0, and 8.7.2, instead of master, v8.7.dev, and 8.7.1. | ||
* | un-hardcode # of reductions | 2018-04-30 | |
| | |||
* | print saturated mulmod for p192 on 32-bit, add note about p256 | 2018-04-30 | |
| | |||
* | fixed too-many-additions problem by fixing number of limbs in from_associational | 2018-04-30 | |
| | |||
* | Fix some carry logic | 2018-04-30 | |
| | |||
* | First stab at generating code for saturated solinas modular | 2018-04-30 | |
| | | | | | multiplication (currently produces way too many expressions because 1*x and -1*x are not simplified for two-output mul) | ||
* | fix comment | 2018-04-30 | |
| | |||
* | Fix bounds analysis for saturated ops and remove unneeded comment | 2018-04-30 | |
| | |||
* | first stab at reifying barrett | 2018-04-30 | |
| | |||
* | fix definitions of saturated operations to avoid unnecessary work, and make ↵ | 2018-04-30 | |
| | | | | Montgomery use them | ||
* | tweak definition of flatten to use an index rather than check the length of ↵ | 2018-04-30 | |
| | | | | the output accumulator--this prevents the accumulator from repeatedly showing up in the expression and making the term huge | ||
* | fix the placement of a dlet to make more sense | 2018-04-30 | |
| | |||
* | Don't allow coqprime and coqprime-all to run in parallel | 2018-04-30 | |
| | | | | We only want one invocation of submake at a time. |