The equation compiler uses different strategies for processing
recursive equations. Some of them may produce unclear runtime cost
model. For example, the following fibonacci functions was running in
linear time instead of exponential time because the equation compiler
used the brec_on recursor.
def fib : nat → nat
| 0 := 1
| 1 := 1
| (n+2) := fib (n+1) + fib n
@dselsam and @jroesch have reported examples were the equation compiler
produces a negative performance impact. The new test (`eval` function)
captures the problem reported by @jroesch. In this example, the runtime
should not depend on the "amount of fuel".
This commit addresses this issue.
Motivations:
- Clear execution cost semantics for recursive functions.
- Auxiliary meta definition may assist recursive definition unfolding in the type_context object.
Next step: use meta auxiliary definition at code generation.
Comment from parser.h
This commit makes sure that all declaration parameters must be surrounded with some kind of bracket. (e.g., '()', '{}', '[]').
The goal is to avoid counter-intuitive declarations such as:
example p : false := trivial
def main proof : false := trivial
which would be parsed as
example (p : false) : _ := trivial
def main (proof : false) : _ := trivial
where `_` in both cases is elaborated into `true`. This issue was raised by @gebner in the slack channel.
Remark: we still want implicit delimiters for lambda/pi expressions. That is, we want to write
fun x : t, s
or
fun x, s
instead of
fun (x : t), s
To make the equation compiler more convenient to use, we will add a
couple of preprocessing steps.
This commit adds the first one of them. In this step, we use
type inference to refine pattern variables, and we relax the
restrictions on inaccessible annotations.
We will also add a preprocessing step that implements the "complete
transition" step before we execute the elim_match step.
Reason: vector in in init folder was introducing an overload (`::`) for
all Lean users. The workaround (use `local infix ::`) was
counterintuitive.
We currently have no special support for bitvectors in the code
generator. Thus, there is no need to have vector and bitvec in the init
folder right now. Moreover, the new parser and elaborator (issue #1674) should
provide better ways of managing overloaded symbols.
The issue was that instantiate_mvars(infer(m)) had a metavariable, while
infer(instantiate_mvars(m)) did not. Changing the call from assign to
is_def_eq also unifies the type, assigning the metavariable inside the
type.
