Какие вложенные шаблоны допустимы в dafny? - PullRequest
Новая
       98

Какие вложенные шаблоны допустимы в dafny?

0 голосов
/ 03 августа 2020 
This may be a limitation or a bug either in dafny or in my understanding.

Любая помощь в понимании этого очень ценится.

Следующая функция dafny проверяет 

datatype Tree<T> = Leaf(data: T)
                 | Node(left: Tree<T>, right: Tree<T>)
 function   treetree(t: Tree<Color>) : string 
 {
     match t
         case Leaf(_) => "zero"
         case Node(Node(_,_),_) => "two"
         case Node(Leaf(_),_) => "one"
 }

Тогда как следующая функция не работает: 

function   treelist(t: Tree<List<string>>) : string 
 {
     match t
         case Leaf(Nil) => "zero"
         case Leaf(Cons(_,_)) => "list"
         case Node(_,_) => "two"
         
 }

Ошибка заявляет, что «элемент-лист появляется более чем в одном случае», что, как я знаю, является правильным, но поскольку элемент-узел появляется более чем в одном случае в предыдущей допустимой функции, я не уверен, когда эта ошибка действительно применяется.

Дополнительные сведения 

datatype Color = Red | Blue |  Named(name: string)
datatype Tree<T> = Leaf(data: T)
                 | Node(left: Tree<T>, right: Tree<T>)

Плюс я заметил, что следующее подтверждает 

function   leaflist(t: Tree<List<string>>) : string 
 {
     match t
         case Leaf(Nil) => "zero"
         case Leaf(Cons(_,_)) => "list"
         case Node(Node(_,_),_) => "two"
         case Node(Leaf(_),_) => "one"
 }
...