0

inox 文档说明了以下内容

Inox 提供了实用程序类型 TypedADTSort 和 TypedADTConstructor（参见文件 inox/ast/Definitions.scala），它们对应于类型参数已用具体类型实例化的 ADT 定义。可以使用这些来访问参数/字段和带有实例化类型的封闭表达式。

以下对象包含对数学领域建模所需的排序和构造函数。

import inox._
import inox.trees.{forall => _, _}
import inox.trees.dsl._

import welder._

object Field { 
  /*
    A non trivial field has elements different from zero.
    We can further assume the existence of a nonzero element called one.
    Any other element is of type notOne.

    field -> zero
          -> nonZero -> one
                     -> notOne
  */

  val element = FreshIdentifier("element")
  val zero = FreshIdentifier("zero")
  val nonZero = FreshIdentifier("nonZero")
  val one = FreshIdentifier("one")
  val notOne = FreshIdentifier("notOne")

  val elementADT = mkSort(element)()(Seq(zero, one, nonZero, notOne))
  val nonZeroADT = mkConstructor(nonZero)()(Some(element)) {_ => Seq()}
  val zeroADT = mkConstructor(zero)()(Some(element)) {_ => Seq()}
  val oneADT = mkConstructor(one)()(Some(nonZero)) {_ => Seq()}
  val notOneADT = mkConstructor(notOne)()(Some(nonZero)) {_ => Seq()}


  val symbols = NoSymbols
    .withADTs(Seq(elementADT, nonZeroADT, zeroADT, oneADT, notOneADT))
    .withFunctions(Seq(/*Register functions*/))

  val program = InoxProgram(Context.empty, symbols)

  val theory = theoryOf(program)
  import theory._
}

现在我介绍用于对椭圆曲线的仿射点进行建模的种类和构造。

import inox._
import inox.trees.{forall => _, _}
import inox.trees.dsl._

import welder._

object Curve {

  val F: ADTType = T(Field.element)()
  val affinePoint = FreshIdentifier("affinePoint")
  val infinitePoint = FreshIdentifier("infinitePoint")
  val finitePoint = FreshIdentifier("finitePoint")
  val x = FreshIdentifier("x")
  val y = FreshIdentifier("y")

  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(x, fT), ValDef(y, fT))
  }

  val affine = TypedADTSort(affinePointADT,Seq(F))
  val infinite = TypedADTConstructor(infiniteADT,Seq(F))
  val finite = TypedADTConstructor(finiteADT,Seq(F))

  val symbols = NoSymbols
    .withADTs(Seq(affinePointADT, infiniteADT, finiteADT))
    .withFunctions(Seq(/*Register functions here*/))
}

您可以观察到最后我使用TypedADTSort并TypedADTConstructor使用字段元素作为参数而不是通用参数。我需要这个来讨论仿射点上下文中对字段元素的操作。

编译错误

编译它会给出类型的错误

could not find implicit value for parameter symbols: inox.trees.Symbols
[error]   val affine = TypedADTSort(affinePointADT,Seq(F))
[error]                            ^
could not find implicit value for parameter symbols: inox.trees.Symbols
[error]   val infinite = TypedADTConstructor(infiniteADT,Seq(F))

为什么会这样？有哪些解决方案？

4

1 回答 1

0

在这种情况下，不需要使用 TypedADT 构造。使用排序和构造函数对以下层次结构进行建模就足够了。

abstract class Element
abstract class AffinePoint[T]

困难的部分可能是意识到这里AffinePoint[Element]可以T(affinePoint)(T(element)())使用 Inox DSL建模。

无论如何，我得到的编译错误源于我需要将隐式参数传递给相应的调用。

于 2017-04-13T13:31:32.390 回答