| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
| |
preparation for reifying barrett; tweaked definition of cc_l
|
|
|
|
| |
This will be required to correctly stringify the syntax tree for the error message
|
|
|
|
|
| |
As per
https://github.com/mit-plv/fiat-crypto/issues/344#issuecomment-381424442
|
|
|
|
|
|
|
| |
Because pipes eat error codes, we were previously succeeding when
display targets fail. This meant that we didn't catch
https://github.com/mit-plv/fiat-crypto/issues/344#issuecomment-381422896
on Travis. Now we will.
|
| |
|
|
|
|
|
|
| |
This was causing issues with bug minimization because some hints seem to
follow [Require], not [Import], and so when [eauto] got stronger, this
proof was failing.
|
|\
| |
| | |
comprehensive loops framework with complete proof theory
|
| |
| |
| |
| |
| | |
See https://github.com/coq/coq/issues/7291 and
https://github.com/mit-plv/fiat-crypto/issues/349#issuecomment-382180578
|
| | |
|
| |
| |
| |
| | |
This should fix #349 (or at least most of it).
|
| | |
|
| | |
|
| |
| |
| |
| | |
This should speed up the lite target on master
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
To updated version of https://github.com/coq/coq/pull/6597
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
After in-person discussion with Andres, we decided that, because the
previous form of uncurrying was only half-uncurried (not including
identifiers nor lambdas passed to other lambdas), and the strongest
driver of a full uncurrying pass would be having an easier-to-visualize
intermediate representation / knowing more clearly what the pipeline is
doing, and the changes required for making this a full uncurrying pass
would be global to the pipeline (require changing the type of
identifiers), we would instead go back the version of uncurrying that I
initially proposed, where we only uncurry the top-level function.
Note that we create a slightly more complicated term (with more
application nodes) than we have to; if we instead took in `@expr (@expr
var) t` rather than `@expr var t`, we wouldn't introduce needless
abstractions. However, the current form admits an extremely simple
proof of correctness, which doesn't even require well-formedness of the
expression tree.
|
| |
| |
| |
| |
| | |
This allows us to (a) consolidate the constant and non-constant
pipelines and (b) vastly simplify the call-with-id-continuation logic.
|
| |
| |
| |
| |
| | |
This pass uncurries all applied lambdas. Care is taken to not do beta
reduction and to not introduce spurious `Abs` or `App` nodes.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
the sqrt of the usual weight
|
| | |
|
| |
| |
| |
| | |
carries even in cases where w is not necessarily the square of w', but potentially some other power
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|