Skip to content

Tentative implementation of HasIRContext. - #417

Draft
math-fehr wants to merge 2 commits into
mainfrom
math-fehr/hasircontext
Draft

Tentative implementation of HasIRContext.#417
math-fehr wants to merge 2 commits into
mainfrom
math-fehr/hasircontext

Conversation

@math-fehr

Copy link
Copy Markdown
Collaborator

Currently, we have IRContext, WfIRContext, Rewriter, and WfRewriter that all "contains" an IRContext.
What we would like to have is a coercion from all of these to IRContext. However, as IRContext has a parameter that we always implicitely deduce, the coercion almost never works.

One of the solution would be to reimplement all getters so that they can use these different classes, but I wanted to try if there was another solution before trying this.

The implementation here uses a new typeclass HasIRContext, which is essentially just the coercion from the types to IRContext.

Please let me know what you think of the design

@math-fehr math-fehr self-assigned this Apr 13, 2026
@math-fehr

Copy link
Copy Markdown
Collaborator Author

!radar

@ineol

ineol commented Apr 13, 2026

Copy link
Copy Markdown
Collaborator

Benchmark results for 3a90a7a against c2650f2 are in! @math-fehr

Large changes (13🟥)

  • 🟥 build/module/Veir.IR.Basic//instructions: +1.3G (+3.87%)
  • 🟥 build/module/Veir.IR.Basic//lines: +19.0 (+0.91%)
  • 🟥 build/module/Veir.IR.Fields//instructions: +3.7G (+4.07%)
  • 🟥 build/module/Veir.IR.InBounds//instructions: +13.6G (+4.44%)
  • 🟥 build/module/Veir.Rewriter.InlineBlock//instructions: +2.3G (+2.12%)
  • 🟥 build/module/Veir.Rewriter.LinkedList.Basic//instructions: +534.3M (+2.69%)
  • 🟥 build/module/Veir.Rewriter.LinkedList.GetSet//instructions: +3.4G (+2.81%)
  • 🟥 build/module/Veir.Rewriter.WellFormed.BlockOperands//instructions: +2.3G (+1.57%)
  • 🟥 build/module/Veir.Rewriter.WellFormed.OpResults//instructions: +397.3M (+3.38%)
  • 🟥 build/module/Veir.Rewriter.WellFormed.Operation//instructions: +1.9G (+1.12%)
  • 🟥 build/module/Veir.Rewriter.WellFormed.ReplaceOp//instructions: +377.8M (+2.91%)
  • 🟥 build/module/Veir.Rewriter.WellFormed.Value//instructions: +334.4M (+0.69%)
  • 🟥 build/module/Veir.Rewriter.WfRewriter//instructions: +888.7M (+11.50%)

Medium changes (1🟥)

  • 🟥 build/module/Veir.Rewriter.WellFormed.OpRegion//instructions: +266.5M (+2.77%)

Small changes (7🟥)

  • 🟥 build/module/Veir.IR.GetSet//instructions: +3.5G (+1.27%)
  • 🟥 build/module/Veir.IR.Grind//instructions: +8.1M (+0.60%)
  • 🟥 build/module/Veir.PatternRewriter.Basic//instructions: +157.6M (+1.19%)
  • 🟥 build/module/Veir.Rewriter.LinkedList.WellFormed//instructions: +3.0G (+0.67%)
  • 🟥 build/module/Veir.Rewriter.WellFormed.Block//instructions: +114.3M (+1.10%)
  • 🟥 build/module/Veir.Rewriter.WellFormed.OpOperands//instructions: +777.0M (+2.01%)
  • 🟥 build/module/Veir.Rewriter.WellFormed.Region//instructions: +94.8M (+1.44%)

@github-actions github-actions Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

VeIR Benchmarks

Details
Benchmark suite Current: 205d7c1 Previous: 964db92 Ratio
add-fold-worklist/create 2611000 ns 2240000 ns 1.17
add-fold-worklist/rewrite 3806000 ns 3814000 ns 1.00
add-fold-worklist-local/create 2895000 ns 2265000 ns 1.28
add-fold-worklist-local/rewrite 3190000 ns 3205000 ns 1.00
add-zero-worklist/create 3281000 ns 2441000 ns 1.34
add-zero-worklist/rewrite 2550000 ns 2605000 ns 0.98
add-zero-reuse-worklist/create 2584000 ns 2025000 ns 1.28
add-zero-reuse-worklist/rewrite 2098000 ns 2000000 ns 1.05
mul-two-worklist/create 2855000 ns 2439000 ns 1.17
mul-two-worklist/rewrite 5324000 ns 5524000 ns 0.96
add-fold-forwards/create 3034000 ns 2262000 ns 1.34
add-fold-forwards/rewrite 3083000 ns 3141000 ns 0.98
add-zero-forwards/create 3050000 ns 2239000 ns 1.36
add-zero-forwards/rewrite 2062000 ns 2026000 ns 1.02
add-zero-reuse-forwards/create 2593000 ns 1850000 ns 1.40
add-zero-reuse-forwards/rewrite 1711000 ns 1580000 ns 1.08
mul-two-forwards/create 3001000 ns 2285000 ns 1.31
mul-two-forwards/rewrite 3717000 ns 3771000 ns 0.99
add-zero-reuse-first/create 2742000 ns 1865000 ns 1.47
add-zero-reuse-first/rewrite 8000 ns 8000 ns 1
add-zero-lots-of-reuse-first/create 2669000 ns 1834000 ns 1.46
add-zero-lots-of-reuse-first/rewrite 955000 ns 788000 ns 1.21

This comment was automatically generated by workflow using github-action-benchmark.

@math-fehr
math-fehr force-pushed the math-fehr/hasircontext branch 3 times, most recently from bacc378 to 876c9b5 Compare April 15, 2026 12:45
@math-fehr

Copy link
Copy Markdown
Collaborator Author

!radar

@ineol

ineol commented Apr 15, 2026

Copy link
Copy Markdown
Collaborator

Benchmark results for 876c9b5 against c2650f2 are in! @math-fehr

Large changes (23🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (1🟥)

  • 🟥 build/profile/grind mark subsingleton//wall-clock: +2s (+14.10%)

Small changes (5🟥)

  • 🟥 build/module/Veir.Benchmarks//instructions: +90.1M (+0.97%)
  • 🟥 build/module/Veir.Printer//instructions: +43.0M (+0.89%)
  • 🟥 build/module/Veir.Rewriter.Basic//instructions: +4.0G (+7.91%)
  • 🟥 build/module/Veir.Rewriter.InsertPoint//instructions: +1.4G (+3.09%)
  • 🟥 build/module/Veir.Rewriter.WellFormed.IRContext//instructions: +28.9M (+1.37%)

@ineol

ineol commented Apr 15, 2026

Copy link
Copy Markdown
Collaborator

Why did you replace all the grind call in IR/Basic.lean?

@math-fehr

Copy link
Copy Markdown
Collaborator Author

I'll update it again good point. The issue was originally that InBounds cannot be used by grind anymore, so I changed them.

But now I realized that you can use inBounds_def if the typeclass is already in grind, and it seems I missed some, I'll fix that.

@math-fehr
math-fehr force-pushed the math-fehr/hasircontext branch from 876c9b5 to 205d7c1 Compare April 15, 2026 15:38
@tobiasgrosser

Copy link
Copy Markdown
Collaborator

Nice. This seems to go in a great direction.

@math-fehr

Copy link
Copy Markdown
Collaborator Author

Just so you know, I'm first testing this on PatternRewriter before opening this for review.
I want to be sure that if we merge this, this will not cause us problems in the future. Right now this seems to work well for IRContext at least. I also ran the benchmarks and had no performance loss.

Tentative implementation on the entire file


Workaround a Lean bug
@math-fehr
math-fehr force-pushed the math-fehr/hasircontext branch from 205d7c1 to 3726a62 Compare April 17, 2026 17:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants