0

我对字段的加法操作有以下简化定义：

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 代码中使用中缀表示法，或者有解决方案？

4

1 回答 1

1

这里的问题是您定义的隐式类在您创建时不可见y+y（您需要导入 Field._ 使其可见）。

我不记得在 Scala 中究竟是如何进行隐式解析的，所以在 Curve 对象中添加可能import Field._ 会覆盖来自 inox DSL 的 + （这是你编写时应用的那个y+y，给你一个算术加表达式，期望整数参数，因此类型错误）。否则，不幸的是，您会在隐式解析中产生歧义，而且我不确定在这种情况下是否可以使用中缀 + 运算符而不放弃整个 dsl。

于 2017-04-14T17:29:46.000 回答