Add Core-to-Core function inlining transforms#1007
Open
tautschnig wants to merge 2 commits intomainfrom
Open
Conversation
Add function inlining transforms in Strata/Transform/FunctionInlining.lean: - inlineFuncDefs: replace non-recursive function calls with their bodies, with optional postProcess hook for composing with other transforms - collectFuncDefs: collect non-recursive function definitions - inlineRecFuncDefs: bounded unrolling of recursive function calls These operate at the expression level (pure function applications), complementing the existing ProcedureInlining which operates at the statement level (imperative procedure calls). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Pull request overview
Adds a new Core-to-Core transform module for inlining pure function applications at the expression level, complementing existing statement-level procedure inlining.
Changes:
- Introduces
inlineFuncDefsfor inlining fully-applied non-recursive functions with an optionalpostProcesshook. - Adds
collectFuncDefsto extract eligible (non-recursive, monomorphic) function bodies from aCore.Program. - Introduces
inlineRecFuncDefsfor bounded unrolling of recursive function calls.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Replaces the manual defs-list approach with Factory.callOfLFunc + LFunc.computeTypeSubst + LExpr.applySubst, matching the inlining path in LExprEval.eval. This enables: - Polymorphic function inlining (type substitution via computeTypeSubst) - Correct function lookup via the factory (same as the evaluator) - Shared tryInlineCall helper used by both inlineFuncDefs and inlineRecFuncDefs Also addresses Copilot review: - substFvarsLifting for capture-safe substitution (Threads 4, 5) - getLFuncCall replaced by callOfLFunc (Thread 1) - Metadata preserved via factory (Thread 2) - Tests added (Thread 3) - Removed collectFuncDefs (no longer needed — factory has all defs) Co-authored-by: Kiro <kiro-agent@users.noreply.github.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 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.
Add function inlining transforms in Strata/Transform/FunctionInlining.lean:
These operate at the expression level (pure function applications), complementing the existing ProcedureInlining which operates at the statement level (imperative procedure calls).
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.