nested patterns?

Dec 3, 2013 at 12:12 PM
Edited Dec 3, 2013 at 12:12 PM
Hi,

I found that the following is not possible
predicate sorted(list: List<int>)
     {
        match list
        case Nil => true
        case Cons(h1, Nil) => true
        case Cons(h1, Cons(h2,tl2)) => (h1 <= h2 && sorted(tl2))                      
     }
Neither the following
     {
        match list
        case Nil => true
        case Cons(h1, tl1) => { math tl1 
                                                   case Nil => ..
                                                   case Cons(h2,tl2) =>
                                                 }                    
     }
Could you tell me if there is some way to use nested patterns?
Thanks in advance,
Paqui
Dec 3, 2013 at 10:16 PM
Nested patterns are not supported, but nested match expressions are. You write:
predicate sorted(list: List<int>)
{
  match list
  case Nil => true
  case Cons(h1, tail) => (match tail
                          case Nil => true
                          case Cons(h2, _) =>
                            h1 <= h2 && sorted(tail))
}
Note, the parentheses (not curly braces) around the inner match are not necessary in this case.

Please see the Dafny Quick Reference, which has some information about syntax: http://research.microsoft.com/en-us/projects/dafny/reference.aspx
It mentions the (somewhat unfortunate, but consistent) use of curly braces in statement forms of "if" and "match", whereas the expression forms of these constructs do not have curly braces (but can have parentheses, if needed or desired). Also, it mentions that match expressions are currently supported only at the top level of function/predicate bodies, as in this example.

By the way, if you prefer, you can also write this predicate without a match, if you instead use discriminators and destructors. Here is an example:
predicate sorted_alt(list: List<int>)
{
  list.Cons? && list.tail.Cons? ==> list.head <= list.tail.head && sorted_alt(list.tail)
}
For fun, here are these definitions, together with a proof that sorted and sorted_alt are the same predicate: http://rise4fun.com/Dafny/NnzJ

Rustan
Dec 4, 2013 at 9:22 AM