search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
690 stars 33 forks source link

Evaluator for closed expressions #228

Open valis opened 4 years ago

valis commented 4 years ago

It is possible to implement a more efficient evaluator for closed expressions. For example, a function defined by recursion over Nat can be evaluated using a for-loop instead of recursion. This will help with some stack overflow errors.

ice1000 commented 4 years ago

Is this fixed? I recall @valis has implemented tail-call optimization.

Can we have some benchmark tests?

valis commented 4 years ago

No. It is still easy to get stack overflow. I'm going to fix this, but it still makes sense to implement a separate evaluator (or even compiler) for closed expressions.