Dafny 4.0 suggestion: var pattern matching

[MikaelMayer]

The following is currently ambiguous

datatype C = LongName | OtherLongName
method f(c: C) {
  var y := match c {
    case Longname => assert c != OtherLongName; 1
  };
}

This fails because Longname is not the same as Longname. I know we are working on a warning system, but what about the following syntax introduction: the var pattern in c#, which is necessary to introduce a variable.

datatype C = LongName | OtherLongName
method f(c: C) {
  var y := match c {
    case var Longname => assert c != OtherLongName; 1
  };
}

That way, the first one would yield something like "Longname" is not recognized (that's perfect) and the second would clearly indicate that Longname is a variable (no ambiguity !)

The only caveat though would be that it will lengthen cases when extracting all parameters of a datatype

datatype C = D(int, int, int, int)
method f(c: C) {
  var y := match c {
    case D(var a, var b, var c, var d) => a+b+c+d
  };
}

Alternatively, we could also support the named syntax:

datatype C = D(a: int, ignored: int, b: int, ignored2: int)
method f(c: C) {
  var y := match c {
    case D(a := var x, b := var y) => x+y
  };
}

[cpitclaudel]

(Should we use the discussion feature for these discussions?)

This would make code extremely heavy and verbose fr large matches, like this:

      function method MapChildren_Expr(e: Expr, tr: BottomUpTransformer) :
        (e': Expr)
      {
        match e {
          case Var(_) => e
          case Literal(_) => e
          case Abs(var vars, var body) =>
            Expr.Abs(vars, Map_Expr(body, tr))
          case Apply(var aop, var exprs) =>
            var exprs' := Seq.Map(e requires e in exprs => Map_Expr(e, tr), exprs);
            Expr.Apply(aop, exprs');
          case Block(var exprs) =>
            var exprs' := Seq.Map(e requires e in exprs => Map_Expr(e, tr), exprs);
            Expr.Block(exprs');
          case Bind(var vars, var vals, var body) =>
            var vals' := Seq.Map(e requires e in vals => Map_Expr(e, tr), vals);
            Expr.Bind(vars, vals', Map_Expr(body, tr));
          case If(var cond, var thn, var els) =>
            Expr.If(Map_Expr(cond, tr), Map_Expr(thn, tr), Map_Expr(els, tr));
        }
      }

Additionally, it breaks the nice symmetry of constructors and destructors:

match x with 
  case Plus(a, b) => Plus(a, b)

versus

match x with 
  case Plus(var a, var b) => Plus(a, b)

Btw, C# doesn't require vars in all cases, right? x is SuperType y introduces y

[MikaelMayer]

I would have followed you for the assymetry, but we do require the "var" keyword to assign local variables, and this is an assymetry already.

You're partially right for c#, it only requires var when you don't provde the supertype, like this: x is var y. This is symmetrical ... to variable assignment.

We cannot do the same for dafny because type ascription cannot introduce local variables by itself, only the keyword var can outside of matches.

match x with 
  case Plus(a: int, b: int) => Plus(a: int, b: int)

[cpitclaudel]

we do require the "var" keyword to assign local variables, and this is an assymetry already.

To create local variables (not to assign them), but I'm not seeing the connection(?)

[MikaelMayer]

Yes to create local variables. You are not seeing the connection?

[cpitclaudel]

You are not seeing the connection?

No, not really :/

I was talking about the symmetry between match Plus(0, 1), case Plus(x, y) and => Plus(x, y) in case Plus(x, y) => Plus(x, y). You could argue that we have the same symmetry for variables: var Plus(x, y) := Plus(1, 2) (with var instead of match and := instead of case).

So I could see arguing for case var Plus(x, y), but isn't var redundant? And I wouldn't want to write var Plus(var x, var y) – that too sounds redundant.

[robin-aws]

I don't think the var pattern is an obvious right answer here, but I'm definitely still concerned about the ambiguity between matching and capturing, and fact that our new warnings don't cover the example in the issue description.

@keyboardDrummer Do we have any other pending warning cases that would catch this?

[keyboardDrummer]

/warnMissingConstructorParenthesis forces a clear syntactic difference between captured variables and constructors

(I'm not sure about the exact error messages so I've just made these up)

datatype C = LongName | OtherLongName
method f(c: C) {
  var y := match c {
    case LongName => assert c != OtherLongName; 1 // Error, constructors in case patterns must be followed by parentheses
  };
}

datatype C = LongName | OtherLongName
method f(c: C) {
  var y := match c {
    case Longname() => assert c != OtherLongName; 1 // Error, `Longname` is not a constructor
  };
}