aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Work around an anomaly in pretyping/constr_matchingGravatar Jason Gross2017-04-03
|
* Document some tactics from Jade's pipleine sideGravatar Jason Gross2017-04-03
| | | | | Also use more definitions and fewer tactics, and more general definitions.
* Fuse Pipeline.{Composition,ReflectiveTactics}Gravatar Jason Gross2017-04-03
| | | | | They need to be modified together to keep track of the ordering of side-conditions.
* Fix missing unfold in proofGravatar Jason Gross2017-04-03
|
* Add missing parenthesesGravatar Jason Gross2017-04-03
|
* Use projT2_mapGravatar Jason Gross2017-04-03
|
* Finally, a fully working IntegrationTestGravatar Jason Gross2017-04-03
|
* WIPGravatar Jason Gross2017-04-03
|
* WIP on integrationGravatar Jason Gross2017-04-03
|
* Rework and doc reflective pipeline (more Gallina)Gravatar Jason Gross2017-04-03
|
* Add an initial stab at doing the pipeline mostly in GallinaGravatar Jason Gross2017-04-03
|
* Add a bit more documentationGravatar Jason Gross2017-04-03
|
* Pipeline: reduce away reflective constantsGravatar Jason Gross2017-04-03
| | | | | This makes it so that the term that shows up when the reflective subgoal is solved doesn't include things like [Interp]
* Start adding comments to Pipeline/ReflectiveTactics.vGravatar Jason Gross2017-04-03
|
* Rename PreDefinitions to OutputTypeGravatar Jason Gross2017-04-03
| | | | As per https://github.com/mit-plv/fiat-crypto/pull/141#discussion_r109312653
* Add and update documentation in Pipeline/Glue.vGravatar Jason Gross2017-04-03
|
* An approximately first stab DeBruijn word-size-selGravatar Jason Gross2017-04-03
|
* Remove old reflective pipeline, making way the newGravatar Jason Gross2017-04-03
|
* Remove everything after the individual reified opsGravatar Jason Gross2017-04-03
| | | | | This includes extraction and associated targets. I've left the .hs files lying around, currently unused.
* Fix parsing issueGravatar Jason Gross2017-04-03
|
* Add proj2_sig_mapGravatar Jason Gross2017-04-03
|
* Don't require keeping track of which goals have evars; check that in tacticsGravatar Jason Gross2017-04-03
|
* Add UnifyAbstractReflexivity tacticsGravatar Jason Gross2017-04-03
|
* Fix a typoGravatar Jason Gross2017-04-02
|
* Add projT2_mapGravatar Jason Gross2017-04-02
|
* Add Tactics.EvarExistsGravatar Jason Gross2017-04-02
|
* Add Util.SigmaAssocGravatar Jason Gross2017-04-02
|
* clear before abstract so we can handle existentialsGravatar Jason Gross2017-04-02
|
* Add ap_transport to Equality.vGravatar Jason Gross2017-04-02
|
* Add InterpEtaGravatar Jason Gross2017-04-02
| | | | It's a version of [Interp] that works even when there are destructuring lets.
* Remove the bits of the new reflective pipeline in masterGravatar Jason Gross2017-04-02
| | | | This way, we can keep all of new pipeline code together in the PR
* Remove all the .v files in SpecificGenGravatar Jason Gross2017-04-02
| | | | This gets most of the way to 10 in #14.
* More extensive comment in NewBaseSystemGravatar Jason Gross2017-04-02
| | | | As per Andres' request on #138.
* Work around bug #5434Gravatar Jason Gross2017-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.fieldwiseGravatar Jason Gross2017-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.InterpInlineConstGravatar Jason Gross2017-04-02
|
* Better version of inversion_ProcessedReflectivePackageGravatar Jason Gross2017-04-02
| | | | Now it doesn't introduce needless dependencies
* Add inversion_ProcessedReflectivePackageGravatar Jason Gross2017-04-02
|
* Add PreDefinitions pipeline fileGravatar Jason Gross2017-04-02
|
* Add Z instantiations of InlineConstGravatar Jason Gross2017-04-02
|
* Add Z.Bounds.MapCastByDeBruijn instantiationGravatar Jason Gross2017-04-02
|
* Add Z instantiation of MapCastByDeBruijnInterpGravatar Jason Gross2017-04-02
|
* Add reflective_interp rewrite dbGravatar Jason Gross2017-04-02
|
* Rewrite in Op arguments before rewriting in OpGravatar Jason Gross2017-04-01
| | | | This fixes the rewriter to actually simplify deeply nested expressions.
* Also do eta under lets in Reflection/Eta.vGravatar Jason Gross2017-04-01
|
* Add an initial glue file in the pipeline, no option in boundsGravatar Jason Gross2017-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 BoundedWordGravatar Jason Gross2017-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.vGravatar Jason Gross2017-04-01
|
* Add back word hex constant notationsGravatar Jason Gross2017-04-01
|
* Add RenameBindersGravatar Jason Gross2017-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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 23:42:51 +0000