Stackless ProofScript

[phlegmaticprogrammer]

Scala is based on Java and has therefore a limited conceptual stack size. For example:

    object TestRecursion {

      def even(n : Int) : Boolean = {
        if (n > 0) odd(n - 1)
        else if (n < 0) odd(n + 1)
        else true
      }
      def odd(n : Int) : Boolean = {
        if (n > 0) even(n - 1)
        else if (n < 0) even(n + 1)
        else false
      }

      def main(args : Array[String]) {
        val t = even(10000)
        println("even = " + t)
      }

    }

Running this program will lead to a StackOverflowError. Because the interpreter of ProofScript is written in Scala, if no special measures are taken, ProofScript will inherit the limited stack size property, even much more severely so, because each ProofScript call translates into many Scala calls. Therefore the goal is to convert the ProofScript interpreter to continuation passing style and use a trampoline.

[phlegmaticprogrammer]

After converting evalExpr and evalBlock and most related functions to continuation-passing-style, the following theory checks successfully:

theory issue46
extends \root

def 
  even n if n > 0 = odd (n - 1)
  even n if n < 0 = odd (n + 1)
  even n = true

  odd n if n > 0 = even (n - 1)
  odd n if n < 0 = even (n + 1)
  odd n = false

assert even 100000

[phlegmaticprogrammer]

ProofScript is stackless now.