[pull] main from B-Lang-org:main#173
Merged
Merged
Conversation
Things would be much easier for me if I found this README sooner. I think HLS is a pretty important part of devenv and should be mentioned in the top level document. --------- Co-authored-by: Julie Schwartz <quark@bluespec.com>
Since PR 939 and 966, this test needed more than the 272 M of heap on some of the macOS VMs with certain GHC versions. Hopefully this was just hitting the edge, so we Bump the size to 275.
* Fix post-inference IAp assert for ATF-bearing class instances ISyntaxCheck.eqTypeNum's satisfy call couldn't prove equality between a fresh metavariable and an ATF application whose parent class dict had been decomposed by an Add-style instance (e.g. Bits (a, b) sab <= (Bits a sa, Bits b sb, Add sa sb sab) loses the SizeOf (a, b) ≡ sab link). The fundep-derived sub-goal NumEq sa sa' couldn't be discharged because the env's EC --- where sa ≡ sa' is recorded --- was not visible to satisfy. Fix: inject the env's numeric-kind EC equivalences as explicit NumEq preds before calling satisfy. A spanning-tree's worth of pairs per class (n-1, not n*(n-1)/2) suffices since satisfy chases equalities transitively. Also fixes a latent kind bug in iTAdd/iTMax/iTMin/iTMul/iTDiv: IKFun is left-associative as a backtick operator, so the unparenthesized `IKNum \`IKFun\` IKNum \`IKFun\` IKNum` form represented `(KNum -> KNum) -> KNum` rather than `KNum -> KNum -> KNum`. The new eqTypeNum code calls kCheck on EC entries, which is the first path to actually query these kinds. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * Add regression test for ATF pair-Add-decomposition assert Minimal repro for the post-inference IAp assert fixed in the prior commit: a rank-2 polymorphic struct field whose proviso uses a class whose 2-ary instance decomposes the ATF target into TAdd of the component ATFs. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * Revert accidental change to debug expression --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
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 subscribe to this conversation on GitHub.
Already have an account?
Sign in.
3 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.
See Commits and Changes for more details.
Created by
pull[bot] (v2.0.0-alpha.4)
Can you help keep this open source service alive? 💖 Please sponsor : )