在焊机中定义中缀运算符

Question

我对字段的加法运算有以下简单定义：

import inox._
import inox.trees.{forall => _, _}
import inox.trees.dsl._
object Field { 
  val element = FreshIdentifier("element")
  val zero = FreshIdentifier("zero")
  val one = FreshIdentifier("one")
  val elementADT = mkSort(element)()(Seq(zero, one))
  val zeroADT = mkConstructor(zero)()(Some(element)) {_ => Seq()}
  val oneADT = mkConstructor(one)()(Some(element)) {_ => Seq()}
  val addID = FreshIdentifier("add")
  val addFunction = mkFunDef(addID)("element") { case Seq(eT) => 
    val args: Seq[ValDef] = Seq("f1" :: eT, "f2" :: eT)  
    val retType: Type = eT
    val body: Seq[Variable] => Expr = { case Seq(f1,f2) =>
      //do the addition for this field
      f1 //do something better...
    } 
    (args, retType, body)
  }
  //-------Helper functions for arithmetic operations and zero element of field----------------
  implicit class ExprOperands(private val lhs: Expr) extends AnyVal{
    def +(rhs: Expr): Expr = E(addID)(T(element)())(lhs, rhs)
  }
}

我希望此操作与中缀符号一起使用，并且此处给出了我在 Scala 中找到的当前解决方案。这就是为什么我在底部包含隐式类的原因。

假设现在我想使用加法的这个定义：

import inox._
import inox.trees.{forall => _, _}
import inox.trees.dsl._
import welder._
object Curve{
  val affinePoint = FreshIdentifier("affinePoint")
  val infinitePoint = FreshIdentifier("infinitePoint")
  val finitePoint = FreshIdentifier("finitePoint")
  val first = FreshIdentifier("first")
  val second = FreshIdentifier("second")
  val affinePointADT = mkSort(affinePoint)("F")(Seq(infinitePoint,finitePoint))
  val infiniteADT = mkConstructor(infinitePoint)("F")(Some(affinePoint))(_ => Seq())
  val finiteADT = mkConstructor(finitePoint)("F")(Some(affinePoint)){ case Seq(fT) =>
    Seq(ValDef(first, fT), ValDef(second, fT))
  }
  val F = T(Field.element)()
  val affine = T(affinePoint)(F)
  val infinite = T(infinitePoint)(F)
  val finite = T(finitePoint)(F)
  val onCurveID = FreshIdentifier("onCurve")
  val onCurveFunction = mkFunDef(onCurveID)() { case Seq() => 
    val args: Seq[ValDef] = Seq("p" :: affine, "a" :: F, "b" :: F)
    val retType: Type = BooleanType
    val body: Seq[Variable] => Expr = { case Seq(p,a,b) =>
      if_(p.isInstOf(finite)){
        val x: Expr = p.asInstOf(finite).getField(first)
        val y: Expr = p.asInstOf(finite).getField(second)
        x === y+y
      } else_ {
        BooleanLiteral(true)
      }
    }
    (args, retType, body)
  }
  //---------------------------Registering elements-----------------------------------
  val symbols = NoSymbols
    .withADTs(Seq(affinePointADT, 
                  infiniteADT, 
                  finiteADT,
                  Field.zeroADT,
                  Field.oneADT,
                  Field.elementADT))
    .withFunctions(Seq(Field.addFunction, 
                        onCurveFunction))
  val program = InoxProgram(Context.empty, symbols)
  val theory = theoryOf(program)
  import theory._
  val expr = (E(BigInt(1)) + E(BigInt(1))) === E(BigInt(2))
  val theorem: Theorem = prove(expr)
}

这不会编译给出以下错误：

java.lang.ExceptionInInitializerError
    at Main$.main(Main.scala:4)
    at Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
Caused by: inox.ast.TypeOps$TypeErrorException: Type error: if (p.isInstanceOf[finitePoint[element]]) {
  p.asInstanceOf[finitePoint[element]].first == p.asInstanceOf[finitePoint[element]].second + p.asInstanceOf[finitePoint[element]].second
} else {
  true
}, expected Boolean, found <untyped>
    at inox.ast.TypeOps$TypeErrorException$.apply(TypeOps.scala:24)
    at inox.ast.TypeOps$class.typeCheck(TypeOps.scala:264)
    at inox.ast.SimpleSymbols$SimpleSymbols.typeCheck(SimpleSymbols.scala:12)
    at inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormed$2.apply(Definitions.scala:166)
    at inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormed$2.apply(Definitions.scala:165)
    at scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
    at scala.collection.immutable.Map$Map2.foreach(Map.scala:137)
    at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
    at inox.ast.Definitions$AbstractSymbols$class.ensureWellFormed(Definitions.scala:165)
    at inox.ast.SimpleSymbols$SimpleSymbols.ensureWellFormed$lzycompute(SimpleSymbols.scala:12)
    at inox.ast.SimpleSymbols$SimpleSymbols.ensureWellFormed(SimpleSymbols.scala:12)
    at inox.solvers.unrolling.AbstractUnrollingSolver$class.assertCnstr(UnrollingSolver.scala:129)
    at inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$1.inox$tip$TipDebugger$$super$assertCnstr(SolverFactory.scala:115)
    at inox.tip.TipDebugger$class.assertCnstr(TipDebugger.scala:52)
    at inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$1.assertCnstr(SolverFactory.scala:115)
    at inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$1.assertCnstr(SolverFactory.scala:115)
    at welder.Solvers$class.prove(Solvers.scala:51)
    at welder.package$$anon$1.prove(package.scala:10)
    at welder.Solvers$class.prove(Solvers.scala:23)
    at welder.package$$anon$1.prove(package.scala:10)
    at Curve$.<init>(curve.scala:61)
    at Curve$.<clinit>(curve.scala)
    at Main$.main(Main.scala:4)
    at Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)

事实上，正在发生的事情是在表达式 x === y+y 中，+ 没有正确应用，因此它是非类型化的。我记得在 Welder 证明的对象中，人们无法定义嵌套对象或类，我不知道这是否与此有关。

无论如何，我是否必须忘记在 Welder 代码中使用中缀符号，或者有解决方案？

Answer 1

这里的问题是，当您创建y+y时，您定义的隐式类不可见(您需要导入Field._才能使其可见(。

我不记得隐式解析在 Scala 中是如何发生的，所以也许在 Curve 对象中添加import Field._会覆盖来自 inox DSL 的 +(这是你编写 y+y 时应用的那个，给你一个需要整数参数的算术加表达式，因此类型错误(。否则，不幸的是，您将在隐式解决方案中产生歧义，并且我不确定在这种情况下是否可以在不放弃整个 dsl 的情况下使用 infix + 运算符。