Algebraic universes everywhere and new constraint algorithm #19537
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
coqbot-app
bot
added
the
needs: full CI
mattam82
force-pushed
the
universes-clauses
branch
from
18b4354 to
1e9bfd3
Compare
9 tasks
This comment was marked as resolved.
This comment was marked as resolved.
github-actions
bot
added
the
needs: rebase
mattam82
force-pushed
the
universes-clauses
branch
from
d454c77 to
2a87290
Compare
coqbot-app
bot
removed
the
needs: rebase
github-actions
bot
added
the
needs: rebase
|
The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed. |
Integrate new algorithm Fixed constraints_of, add preliminary union-find structure Debugging in univMinim and uState Model modified by side-effect, not necessarily a good optimization Back to a purely functional implementation of the model Implements clauses for a given conclusion as a set to avoid duplicate clauses Optimize simplify_clauses_between to use marking Implement less efficient ClausesOf.filter_map as it is available only in ocaml >= 4.11.0 Avoid rechecking model if possible after equating universes Reorganize infer_extension/enforce functions No need to update_model in the current setting Change ClausesForward representation WIP on more efficient folding over updated constraints Forward and backward clauses sets Working version with forward clauses Working version with clauses attached to canonical nodes Cleanup and avoid recomputing a model update at each constraint introduction Revert univMinim changes WIP fixing check_* functions Working version with recursive check_clause_holds Use a proper non-empty list datatype for premises check_eq corresponds to equality of canonical nodes add_clause to the model before computing first update_model Backward search checking leq Fixed enforce_eq_can returning wrong canonical node! !! Temporary !! test-suite output fix Allocate less intermediary structures when checking/enforcing a single constraint Minor optimizations and add some path compression for equiv nodes Remove no longer necessary data from the structure Avoid recomputing the cardinals of CanSets in the main loop Avoid recomputing the cardinal of canonical universes at each check (fixes perf issue in n_polymorphic_universes in performance-tests) Fix perf issue in check_clause Fix simplify_clauses_between missing some paths Debugging in univMinim Fix enforce_eq definition Fix initialisation issue, missing some updated constraints Performance tuning of check_clause Name anonymous functions for easier tracing Add fast path to enforce_leq if the constraint is already present Use a local hash-table instead of mutable marks Stop early in find_to_merge based on the values in the model Fix find_to_merge: we might have loops already in the clauses Rebased on latest master Introduce partial models using `nat option` values commerntd Fix wrong use of physical equality Remove bug 17002 testing not implemented yet explanations Move model values outside of canonical nodes Add a "Check Constraint" vernacular command Before separate W set No more w in check Changing check_model_fwd_aux to take w into account fails Fix synchronization of w and cls structures Implement entailment entirely using check Add a fast path for checking implications Use the alternative checking function Add a Check Constraint test-suite file More efficient early stop for checking TODO on universes Try to optimize checks Remove lift_lower, no longer used Dubious optimization Shortcut checking >= Set constraints, always valid Shortcut Set <= i checks Allow general universes in instances of universe-polymorphic functions. Adaptation to allow algebraic universes in instances/constraints Try to debug issue of missing constraint Fix side-effect issue with add_can_clause Remove special handling for algebraic universes Followup algebraics Implement Equiv (l, k) nodes, now a + 1 = b can be handled efficiently mend Simplify univMinim WIP debugging broken invariants Fixed partition_clauses for more than one premise All of stdlib passes now. Careful with morphisms for constructive reals which have to be annotated with Set Annotate ConstructiveReals instances Reinstate clause filtering Fix template poly, API change in do_constraint, check_leq and checker values TODO: fix minimization Working loop-checking algorithm on algebraics Check Constraint syntax change Change extensible universe binders syntax from + to ? Remove debug commands from v file Improve compat for CRelationClasses, not exporting new internally used type constructors Fix constraints_for to build a transitive closure Fix restriction algorithm BAD! Fixme printing of univ inconsistency explanation Fixed module issue FIXME printing of u+1 <= ? Better minimization Better minimization FIXME: Deactivated private univs Not an error, at least the unification seems fine to me Better minimization Better and more predictable minimization. Minim to Set is more agressive Fix ml code of plugin test Better minimization Improve constraints for CMorphisms, and fix setoid_test Fix restrict_universe_context Fix print universe subgraph: TODO cleanup Fix dumping of universes and sorting of universe graphs Fix printing of univs graphs for compatibility Fix computation of sorted universes Fixes after rebase on master Fix parsing issue Fix value definitions in the checker Modified grammar Modified universe binding syntax Fix ML plugin code Fix printers file due to renaming Fix and cleanup pretyping of sorts and universes Compiling universes as bytecode Fix compilation of universe instances in the VM hack hack Comment potentially costly assertions Optimized loop-checking Documentation Avoid simplify_between in the most trivial cases (already seen clause) Guard simplify_between: only call when there is a potential safe loop to collapse to equality. Extrude a let-binding for perf improvement Revert "Guard simplify_between: only call when there is a potential safe loop to collapse to equality." This reverts commit e0fad03. Better debug message for start of unification Cleanup and document find_to_merge_bwd/fwd etc Comment statistics debug code WIP adding maps/set with cardinals Use more abstract module types, and store cardinal for w sets as well Choose heuristically to search forward or backward for universes to merge Fixes after rebase Keep using backward search in find_to_merge Optimize `repr` functions to allocate less WIP on shrinking premises Support two ways to store values: associated to the canonical node (for inference) or as a separate map (for checks) Fixes after rebase Update fullGrammar Update grammar and document "Check Constraint" Fix find_to_merge_bwd to go through max() premises as well Add overlay file for this PR. Equations fixed Fix incompleteness of check_eq_level_expr due to incompleteness of find_to_merge Fix trailing whitespace Remove spurious test file Fixes after rebase Fix parsing and grammar for algebraics Fix parsing issue (+ vs ?) Remove commented code from pretyping.ml Fix ForwardClausesRepr.repr_clauses Experiment using union rather than the expensive union_upto when merging universes Switch back to union_upto Fix rewrite-rules.rst universe notation Fix constraints_for Fix refman rst Fix universe-polymorphism.rst Fix private polymorphic universes Fix whitespace removal mistake Fix after merge Fix script Instance syntax change Use "?" for extension consistently (also resolves + ambiguity for variance decls) Fixes after rebase Overlay for elpi Improve simplify_clauses_bwd's completeness w.r.t. max() clauses find_to_merge_bwd generalization for any clause WIP fixing ideal computations Fix ideal computation FIXME different output Modified syntax for extensible instances New universe tests Make CEquivalence Polymorphic! Fix after rebase Update grammar for new parsing rule for extensible (?) variances Fix test-suite due to different debug output and new variance extension syntax Implement get_explanation Fix after rebase Fix output tests, now with good explanations dealing with casts in eliminators Allow any natural number as universe expression WIP adding a `set` function to the graph API Proper printing of numeric universe levels (starting at 0, replacing Set) Fix debug printing of loop_checking Catch InconsistentEquality exception from `set` and backtrack on enforcing the equality for a proper error message No more refresh needed in unify_to_type(esp not with a Rigid!) Cleanup calls to refresh_universes (remove onlyalgs calls no longer needed) remove call to refresh_universes with ~onlyalg:true Fixes after rebase Update grammar for natural number levels
…rather than generate universe identifiers
…ance information for definitions
…ces in sort polymorphism
…omputed_variances for non-cumulative defs
Also use this distinction to compute the default relevances (still allowing irrelevant universes in inductives/defs to be inferred, for compat with template-poly inductive interpretations)
…es from the evar_map for Check
…onger arbitrary v <= u minimizations allowed)
mattam82
force-pushed
the
universes-clauses
branch
from
05d0901 to
6e461f9
Compare
coqbot-app
bot
removed
needs: rebase
github-actions
bot
added
the
needs: rebase
|
The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This resurrects #18903, rebased on current master.
make doc_gram_rsts.