-
Notifications
You must be signed in to change notification settings - Fork 45
Description
Kore.Step.Step.targetRuleVariables accounts for up to 40% of run time. targetRuleVariables is used on every rewrite rule, which is wasteful because most rules cannot unify. The run time is divided approximately evenly between these three stages:
- The first call to
mapVariablesusingmkElementTargetandmkSetTarget. - In
refreshRule, callingrefreshVariablesto get new names for all the free variables. - In
refreshRule, callingmapVariablesto apply the new names.
As a temporary measure, we can improve performance by moving the first call to mapVariables out of targetRuleVariables; this step need only run once for all the rules. This requires that we specialize the variable types in Kore.Step.RewriteStep to Variable, but in practice this was always the concrete type anyway.
A proper solution is to give the rule and configuration variables a permanent Either-like tag which establishes two separate namespaces of variables (internally). After applying a rewrite rule, we would re-tag any rule variables which entered the configuration. Because we would only rename rule variables for successfully-applied rules, and because we already must traverse the entire term when constructing the result, this would make renaming essentially free.
After: #1545