Кабина Дафни использует импортированный ADT в команде матча

Привет, у меня проблемы с тайм-аутом, и я пытаюсь разбить свой файл на разные модули в надежде, что проверенный модуль не нужно будет повторно проверять в коде VS при работе с модулем, который его импортирует. Если кто-нибудь знает, является ли это разумным способом избежать проблем с тайм-аутом, я хотел бы услышать.

Но более основная проблема, которую я обнаружил, заключается в том, что после импорта АТД я могу использовать операторы in in if, но не операторы 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,l,r) => TL.Node(v,r,l)
 }  
}

person david streader    schedule 22.09.2020    source источник


Ответы (3)


Извините за вопрос - сработало следующее.

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,r) => TL.Node(v,TL.Leaf,r)
       case Node(v,Node(vl,ll,rl),r) => TL.Node(vl,ll,TL.Node(v,rl,r))       
  }
person david streader    schedule 22.09.2020
comment
Оба они работают для меня. В чем проблема со вторым? - person Rustan Leino; 23.09.2020

Ответ на первый вопрос был дан Джеймсом Уилкоксом, и его можно найти в Какие отношения между импортом, включением и проверкой в ​​Dafny? но для удобства повторю ниже:

import не имеет прямого влияния на то, проверен ли импортированный модуль или нет. Модули в других файлах не будут проверены, если их файл не указан в командной строке. Модули в текущем файле всегда проверяются (независимо от того, импортированы они кем-либо или нет).

Основной вопрос, который я поднял в https://github.com/dafny-lang/dafny/issues/870

Большое спасибо всем — научить пользоваться Dafny без переполнения стека было бы намного сложнее.

person david streader    schedule 22.09.2020

Несколько странно, что имена конструкторов, которые следуют за каждым ключевым словом case, должны быть неквалифицированными. Они ищутся в типе выражения, следующего за match. Странно, что не разрешены полные имена, и это, вероятно, будет исправлено в будущем (я думал, что на github есть проблема с Dafny, но я не могу ее найти).

person Rustan Leino    schedule 23.09.2020