在 Inox 中使用 TypedADT 结构

Question

inox 文档说明如下

Inox provides the utility types TypedADTSort and TypedADTConstructor (see file inox/ast/Definitions.scala) that correspond to ADT definitions whose type parameters have been instantiated with concrete types. One can use these to access parameters/fields and enclosed expressions with instantiated types.

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

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))

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

Answer 1

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

abstract class Element
abstract class AffinePoint[T]

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

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

在 Inox 中使用 TypedADT 结构

Using TypedADT constructs in Inox

scala

leon