Currently, function inlining only occurs in some very restricted cases
When a function has no arguments, it can always be inlined.
When a function has arguments, but it only has one rule and all its patterns are variables, it can always be inlined.
When a function has other types of patterns, it can be inlined when the arguments are in normal form.
If a function calls other inlined functions recursively, we first solve the recursive inlining.
The first two rules include all functions in imperative programming languages, but we are still not able to inline something very simple like
U60.to_nat (n: U60) : Nat
U60.to_nat 0 = Nat.zero
U60.to_nat n = Nat.cons (U60.to_nat (- n 1))
...
(U60.to_nat 3)
Because (- n 1) is not normal.
Rule number 3 was made this way to avoid infinite recursion, but maybe we should allow any acyclic recursion patterns. It'll loop forever in some cases, but I think it's worth it. Maybe provide this in an extended inlining attribute like #inline_recursive.
Currently, function inlining only occurs in some very restricted cases
The first two rules include all functions in imperative programming languages, but we are still not able to inline something very simple like
Because
(- n 1)is not normal.Rule number 3 was made this way to avoid infinite recursion, but maybe we should allow any acyclic recursion patterns. It'll loop forever in some cases, but I think it's worth it. Maybe provide this in an extended inlining attribute like
#inline_recursive.