Cab Dafny在match命令中使用导入的ADT

问题描述

嗨，我遇到了超时问题，并试图将我的文件分解为不同的模块，希望在处理导入了该模块的模块时，不必以VS代码重新验证一个经过验证的模块。如果有人知道这是否是避免超时的合理方法，我想听听。

但是我发现的更基本的问题是，一旦导入ADT，我就可以在if语句中使用in，但不能在match语句中使用。有关示例，请参见下面的代码。关于我在做什么错的任何想法吗？

module inner {
    datatype Twee = Node(value : int,left : Twee,right : Twee) | Leaf
    function rot(t:Twee) :Twee
  {
    match t 
       case Leaf => t 
       case Node(v,l,r) => Node(v,r,l)
  }
}
module outer {
import TL = inner 
function workingIf(t:TL.Twee) :TL.Twee
  { if (t == TL.Leaf) then TL.Leaf else t }  
function failingMatch(t:TL.Twee) :TL.Twee
  {
    match t 
       case TL.Leaf => t  // error "darrow expected"
       case TL.Node(v,r) => TL.Node(v,l)
 }  
}

解决方法

很抱歉提出这个问题-以下内容奏效了。

function failingMatch(t:TL.Twee) :TL.Twee
  {
    match t 
       case Leaf => t  
       case Node(v,l,r) => TL.Node(v,r,l)
 }

效果很好，但以下操作失败

function rotateLeft(t:TL.Twee) :TL.Twee
  {
    match t 
       case Leaf => t 
       case Node(v,Leaf,TL.Leaf,r)
       case Node(v,Node(vl,ll,rl),r) => TL.Node(vl,TL.Node(v,rl,r))       
  }

第一个问题的答案由James Wilcox给出，可以在What are the relationships among imports,includes,and verification in Dafny?中找到但为方便起见，我在下面重复：

“ import对导入的模块是否经过验证没有直接影响。其他文件中的模块除非在命令行中列出了它们的文件，否则将不进行验证。当前文件中的模块始终经过验证（无论是否经过验证）。由任何人导入。”

我在https://github.com/dafny-lang/dafny/issues/870中提出的主要问题

非常感谢大家-教如何在没有堆栈溢出的情况下使用Dafny会非常困难。

有些奇怪的是，每个case关键字后面的构造函数名称都应该是不合格的。在match之后的表达式类型中查找它们。奇怪的是，不允许使用合格的名称，这很可能会在将来得到更正（我认为github上对此存在Dafny问题，但我找不到）。

adt adt dafny module module