Use string interpolation to specify formulas partially as strings and partially as scala code

[SimonGuilloud]

String interpollation should allow to refer to formulas previously existing inside a string. Example:

val phi = forall(x, P(x) ==> P(f(x)))
val psi = P(x) ==> P(f(f(x)))

f"$phi ⇒ $psi" // equivalent to StringContext

This is transformed to `

StringContext("", " ⇒ ", "").f(phi, psi)

and hence requires to define

  implicit class MyConverter(val sc: StringContext) {

    def f(args: Any*): theory.Theorem = ???

  }

[vkuncak]

You can also check how it is done in Inox: https://github.com/epfl-lara/inox/blob/master/doc/interpolations.md

[vkuncak]

The interpolators were defined using standard parsing combinators, which are a bit more flexible, but more dangerous to use. https://www.scala-lang.org/api/2.12.8/scala-parser-combinators/scala/util/parsing/combinator/Parsers.html