Recursively exclude examples/incomplete from testing targets#1
Merged
Conversation
strub
added a commit
that referenced
this pull request
Apr 30, 2026
…hange) Splits the existing TcCtt resolution logic into three named local helpers — strat_tvar_via_tvtc, strat_abs_via_decl, strat_infer_by_carrier — corresponding to catalog modes #5, #6, and #1/#2 in doc/typeclasses-inference.md. Behavior is identical: same dispatch order, same failures, same pickup of [Tvar a]/[Tconstr p] cases, same parking of univar carriers. The refactor exists so Phase 3 can drop a By-args strategy in without disturbing the existing logic.
strub
added a commit
that referenced
this pull request
Apr 30, 2026
Adds Mode #3 from doc/typeclasses-inference.md: when a TcCtt has a Tunivar carrier, walk all instances and pick the unique one whose tc_args match (Tunivars in the goal are wildcards for matching). On a unique match, push TyUni equations binding goal Tunivars to the candidate's substituted patterns and the carrier to tci_type; the deferred witness is then produced by Mode #1 on re-fire. Also restores deref_tc inside eq_tc which Phase 2's refactor inadvertently dropped — needed because tvtc stores TC constraints with Tunivars that get merged in [uf] later. Lax matching: TyMatch.doit_type now treats Tunivar on the [ty] side as a wildcard (matches any pattern). Safe because the downstream [check_tcinstance] post-match still requires every instance tparam to be bound, so partial matches are rejected at the final witness-construction step. Closes the bare-op gap for parametric-carrier multi-param TCs: [multi-param-bare-ops.ec](tests/tc/multi-param-bare-ops.ec) covers four shapes: bare both sides, in a lemma, fixed result type only, fixed source type only. multi-param.ec simplified to use bare ops where applicable.
strub
added a commit
that referenced
this pull request
May 6, 2026
Companion to the previous commit (bug #2: per-path synthesis + tci_parents lookup). With multi-flavor inheritance, a single carrier may have multiple synthesised instances of the same TC (e.g. a comring on int has both an addmonoid- and a mulmonoid-derived monoid instance). When applying a polymorphic monoid lemma to a goal whose operator carries a SPECIFIC witness via an abbrev (e.g. [bigM] or the [( * )] alias), the unifier was committing arbitrarily to one of the candidates via [strat_infer_by_carrier], then failing later when the goal's [TcTw] equation pinned the other view. Fix: detect ambiguity at strategy-resolution time. When [infer_all] returns more than one candidate witness for [(carrier, tc)], DEFER — leave the witness univar unresolved instead of committing. A subsequent [TcTw] equation from the surrounding goal will bind the univar to the concrete witness via [bind_uni], picking the correct view from context. The dispatch in [select_op] gains a fourth case alongside (resolved / park-on-arg-deps / failure): if no resolution AND ambiguity detected, hold the constraint live without failing. If unification later doesn't narrow it, the resulting unbound univar surfaces as the usual "type-ambiguous" error elsewhere. Adds [EcTypeClass.infer_all : env -> ty -> typeclass -> tcwitness list] (companion to [infer]). Effect: with both bug fixes in place, [apply big_cat] (on [monoid]) discharges goals stated with [bigA] / [bigM] wrappers at concrete carriers — previously failing because the unifier picked the wrong view. The full multi-flavor factory pattern (e.g. [comring <: addgroup & (mulmonoid with idm = oner, (+) = ( * ))]) now works end-to-end: [\sum] and [\prod]-style notations both fold correctly, and lemmas on [monoid] apply to either flavor without needing per-flavor restatements. Regression: all existing TC examples build clean under --profile=ci.
strub
added a commit
that referenced
this pull request
May 6, 2026
Update the inline comment in TcRing.ec to reflect investigation findings: bugs #1 and #2 are fixed for concrete-carrier use cases (e.g. [bigA] / [bigM] on [int]), but section-internal proofs with a Tvar carrier and multi-parent inheritance hit a [TCIAbstract.lift] representation limit — the [lift] field is a single integer that can't disambiguate among multiple parent walks of different lengths to the same target ancestor TC. Practical effect: declaring a class as [comring <: addgroup & (mulmonoid with ...)] would WORK for [bigA]/[bigM] on concrete carriers but not for proofs of generic comring lemmas inside a section. Until the witness representation supports multi-parent walks (path-encoded lift), [comring] stays single-parent with multiplicative axioms re-stated.
strub
added a commit
that referenced
this pull request
May 7, 2026
Closes the parametric-Path-B witness encoding gap that left class- lemma applications at parametric carriers ([apply (addrC<:c poly>)] inside [section ; declare type c <: comring]) unusable. **The bug.** [opentvi] creates a [TCIUni] for each opened tparam's TC bound and posts a [`TcCtt] problem, but doesn't itself drain the queue. The TCIUni stays parked in [tcenv.problems] until something else triggers [unify_core]. Meanwhile a proof-term carrying [(+)<:c poly[TCIUni #a [0;0]]>] arrives at the matcher's [try_delta], which tries [Op.tc_reducible env (+) tys] — and [tc_core_reduce] raises [NotReducible] on TCIUni witnesses, since it can only walk [TCIConcrete]/[TCIAbstract] forms. So [try_delta] falls through to [default]'s [is_conv], which doesn't TC-reduce either; matching fails, [pf_form_match] raises MatchFailure, [t_apply] reports "the given proof-term proves: ... it does not apply to the goal". **The fix.** Two changes: 1. [EcUnify.UniEnv.flush_tc_problems env ue] (new): runs [Unify.unify_core] on a trivial-true [`TyUni] problem, which re-pushes every parked [`TcCtt] in [tcenv.problems] and lets the strategy dispatcher resolve them. After the call, the resolution map contains a witness for every [TCIUni] that any strategy (Modes #1..#6) could pin. 2. In [EcMatching.f_match_core]'s [try_delta]: before destructuring the heads, call [flush_tc_problems env ue] and re-normalise both sides via [norm]. The substitution machinery in [tcw_subst] (ecCoreSubst.ml:209) dereferences resolved TCIUnis through [fs_tw_uni], so after [norm] both forms carry the concrete witness; [tc_reducible] then succeeds and [doit_tc_reduce] produces the renamed structural op (e.g. [polyD] for poly's addgroup-via-class-(+)), which conv'ing against the goal succeeds. Combined with the earlier framework fixes [0dd7d21] (infer-via- abs-decl) and [c182895] (alpha-equivalent chain reuse), this lets [apply (addrC<:c poly> p q)] and [apply (mulrA<:c poly> p q r)] inside a [c <: comring] section discharge directly, without requiring users to fall back to the underlying [polyD_addrC<:c>] / [polyM_mulrA] structural lemmas. The TcPoly port's structural-form workaround in Phase 6 / Phase 7 / smoke test stays as-is for the already-written code, but new code can use the natural class form. Validates: tcalgebra suite (TcMonoid/TcRing/TcInt/TcBigop/TcBigalg/ TcNumber/TcPoly/TcPolySmokeTest) all pass; the parametric Path B reproducer at /tmp/repro_pathb.ec now closes [test_path_b] via [apply (addrC<:c poly>)] without admit.
strub
added a commit
that referenced
this pull request
May 31, 2026
Three small additions to make REPL-driven proof exploration pleasant without weakening +strict_bullets for saved scripts. 1. Bullet relaxation for REPL input. EcCommands.disable_repl_bullets is called at every REPL phrase; it drops pm_strict_bullets and clears puc_bullets on the active proof so REPL-typed tactics are not rejected for missing bullets. Files loaded via LOAD still respect their own pragma; only direct REPL input is relaxed. 2. TREE / TREE ALL meta-commands. List all open subgoals as a flat numbered enumeration with the focused goal marked. TREE shows a one-line conclusion per goal; TREE ALL shows the full goal bodies. Backed by EcCommands.pp_tree on top of EcCoreGoal.all_opened. 3. [focus: k/N] reply tag. When more than one subgoal is open, both tactic replies and the LOAD response carry [focus: 1/N] alongside any other tag, so the caller knows the next tactic targets goal #1 of N. Supporting plumbing: EcScope.set_xgoal exposes a way to swap the active proof_uc without going through the tactic engine.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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 extends the runtest script with recursive exclusions, and makes the examples/incomplete exclusion recursive.
Submitted as a pull request for code review/refactoring and checking that it does not break things downstream.