Recursively exclude examples/incomplete from testing targets#1
Merged
strub merged 2 commits intoEasyCrypt:1.0from Sep 28, 2017
fdupress:1.0
Merged
Recursively exclude examples/incomplete from testing targets#1strub merged 2 commits intoEasyCrypt:1.0from fdupress:1.0
strub merged 2 commits intoEasyCrypt:1.0from
fdupress:1.0
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.
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.