lundi 3 août 2020

What nested patterns are valid in dafny?

This may be a limitation or a bug either in dafny or in my understanding. Any help understanding this much appreciated.

The following dafny function verifies

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"
 }  

Whereas then next function fails:

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

The error states that "member Leaf appears in more than one case" which I know is correct but as member Node appears in more than one case in the previous valid function I am not sure when this error actually applies.

Aucun commentaire:

Enregistrer un commentaire