aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Also inline Z_cast thingsGravatar Jason Gross2018-11-01
|
* Add some zrange lemmasGravatar Jason Gross2018-11-01
|
* Make pairs work in Z_cast2Gravatar Jason Gross2018-11-01
|
* Export ZRange operation notationsGravatar Jason Gross2018-11-01
|
* Add zrange notationsGravatar Jason Gross2018-11-01
|
* Fix a thing broken by previous commitGravatar Jason Gross2018-11-01
|
* Add more reserved notationsGravatar Jason Gross2018-11-01
|
* Add more zrange operationsGravatar Jason Gross2018-11-01
|
* Remove dead codeGravatar Jason Gross2018-11-01
|
* Tactic-in-term: ensuring same scope for all occurrences of a notation variable.Gravatar Hugo Herbelin2018-11-01
| | | | Follow-up of acc4c460.
* Fix a bug in 8.7 compilationGravatar Jason Gross2018-10-30
|
* Refactor/generalize some pipeline definitions/proofsGravatar Jason Gross2018-10-30
| | | | | | | | | | | | 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.
* Remove duplicate abstractionGravatar Jasper Hugunin2018-10-29
| | | | | `base_type` and `base_interp` are already abstracted by the section. For compatibility with coq/coq#8820.
* Add PositiveSet FactsGravatar Jason Gross2018-10-29
|
* Add eqlistA_eq_iffGravatar Jason Gross2018-10-29
|
* Add split_contravariant_orGravatar Jason Gross2018-10-29
|
* Add ex_eq_and tacticGravatar Jason Gross2018-10-29
|
* Add some lemmas about ex, and, eqGravatar Jason Gross2018-10-29
|
* Stricter check on types in the rewriterGravatar Jason Gross2018-10-29
|
* Add subst_relaxGravatar Jason Gross2018-10-29
|
* Add subst_Some_subst_default, subst_relax_evmGravatar Jason Gross2018-10-29
|
* Fix a proofGravatar Jason Gross2018-10-28
|
* Add an extra check in the rewriterGravatar Jason Gross2018-10-28
|
* Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tacticsGravatar Jason Gross2018-10-28
|
* Fix a bug in ensure_complex_continuationGravatar Jason Gross2018-10-28
|
* Add CPSId tacticsGravatar Jason Gross2018-10-28
|
* Add unify_extracted_cps_idGravatar Jason Gross2018-10-28
|
* Add app_lam_type_of_listGravatar Jason Gross2018-10-25
|
* Add under_forall_vars_relation1_lam_forall_vars, remove ↵Gravatar Jason Gross2018-10-25
| | | | forall2_type_of_list_cps alias of under_type_of_list_relation_cps
* Remove value'_interp_related1Gravatar Jason Gross2018-10-25
|
* Add value_interp_related1Gravatar Jason Gross2018-10-25
|
* Add interp_reify_and_let_binds_baseGravatar Jason Gross2018-10-25
|
* Add interp_reify_as_interpGravatar Jason Gross2018-10-24
|
* Add GallinaReify.reify_as_interpGravatar Jason Gross2018-10-24
|
* Add rawexpr_equiv_expr_to_type_of_rawexprGravatar Jason Gross2018-10-23
|
* Add a horribly manual proof of app_forall_vars_under_forall_vars_relation1Gravatar Jason Gross2018-10-23
| | | | | I guess I still haven't figured out how to automate reasoning about transport across equality.
* Add some equality lemmas about Positive{Map,Set}Gravatar Jason Gross2018-10-23
|
* Add under_with_unification_resultT'_relation1_gen_alwaysGravatar Jason Gross2018-10-23
|
* Add related1_app_type_of_list_under_type_of_list_relation1_cpsGravatar Jason Gross2018-10-23
|
* Update rewriter correctness conditionGravatar Jason Gross2018-10-23
| | | | | | Now we don't need any relation on values when going under binders to get the cps-id condition. This seems essential to getting the rewriter interp correctness proofs to work.
* Tactic-in-term: ensuring same scope for all occurrences of a notation variable.Gravatar Hugo Herbelin2018-10-23
|
* Add placeholder rewrite rules for rewriting after boundsGravatar Jason Gross2018-10-14
| | | | | | | | | | | | | | Currently, there aren't any interesting rewrite rules in the lists, but this allows us to move rewrite rules that depend on cast behavior to after bounds analysis. Unfortunately, it takes a lot of time to build from Rewriter.v to the standalone binaries, so it'll probably make sense to inline some stuff for more rapid development. Note that we also now have a tactic that does all of the evaluation for rewrite rules (assuming the right [Arguments] commands have been issued).
* Minor changes to rewriterGravatar Jason Gross2018-10-14
| | | | | These changes make it easier to prove things about the interpretation of the rewriter.
* Guarantee that casting always returns inrangeGravatar Jason Gross2018-10-12
| | | | | | | | | | | | | | We fuse the bounds relaxation pass with the abstract interpretation pass by folding bounds relaxation into the annotation method. This allows us to not need any particular assumptions about what happens when you cast outside the range. We can therefore now guarantee that the output of casting is always bounded by the given range (rather, by the normalized version of the range), which will be required to take advantage of bounds information in the rewriter (because otherwise we're not guaranteed that casting something to within a range actually outputs something within that range).
* Add some zrange lemmasGravatar Jason Gross2018-10-11
|
* Parameterize rewriter proofs over cast-outside-of-range behaviorGravatar Jason Gross2018-10-11
|
* Add interp-correctness condition for rewriterGravatar Jason Gross2018-10-11
| | | | | | | | | | | | The NBE-rewrite rules are proven correct. The arith and fancy rewrite rules are reduced to lemmas about Z, most of which are inconsistent (and therefore indicate rewrite rules which are missing side-conditions). One bad rewrite rule was found in this process, and corrected in 0842563b23f8d780f4ff1080d7620fc3f368191f The next step after this will be using the rewrite rule correctness to prove the rewriter correct.
* Export more tactics in Tactics.vGravatar Jason Gross2018-10-10
|
* Rename [normalize_commutative_identifier] file to match tactic nameGravatar Jason Gross2018-10-10
|
* Add [normalize_commutative_identifier] tacticGravatar Jason Gross2018-10-10
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 02:28:47 +0000