Merge

1 files changed, 53 insertions, 16 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 7c8536a3..78e7675e 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -536,8 +536,8 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
 ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>

 = (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

      tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

-     IToken moduleName = null;

      List<Type/*!*/>/*!*/ gt;

+     List<IToken> path;

   .)

   ( "object"                        (. tok = t;  ty = new ObjectType(); .)

   | arrayToken                      (. tok = t;  gt = new List<Type/*!*/>(); .)

@@ -550,11 +550,12 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
                                        }

                                        ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

                                     .)

-  | Ident<out tok>                  (. gt = new List<Type/*!*/>(); .)

-    [                               (. moduleName = tok; .)

-      "." Ident<out tok>

-    ]

-    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt, moduleName); .)

+  | Ident<out tok>                  (. gt = new List<Type/*!*/>();

+                                       path = new List<IToken>(); .)

+    {                               (. path.Add(tok); .)

+      "." Ident<out tok>           

+    }

+    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt, path); .)

   )

   .

 GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>

@@ -756,10 +757,23 @@ OneStmt<out Statement/*!*/ s>
     SYNC

     ";"                                (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)

   | ReturnStmt<out s>

-  | "..."                              (. s = new SkeletonStatement(t); .)

+  | SkeletonStmt<out s> 

     ";"

   )

   .

+

+SkeletonStmt<out Statement s>

+= (. List<IToken> names = null;

+     List<Expression> exprs = null;

+     IToken tok, dotdotdot;

+     Expression e; .)

+  "..."                                (. dotdotdot = t; .)

+  ["where"                             (. names = new List<IToken>(); exprs = new List<Expression>(); .)

+     Ident<out tok> "=" Expression<out e>        (. names.Add(tok); exprs.Add(e); .)

+     {"," Ident<out tok> "=" Expression<out e> } (. names.Add(tok); exprs.Add(e); .)

+  ]

+                                       (. s = new SkeletonStatement(dotdotdot, names, exprs); .)

+  .

 ReturnStmt<out Statement/*!*/ s>

 = (.

    IToken returnTok = null;

@@ -829,16 +843,18 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
       "]"                              (. // make sure an array class with this dimensionality exists

                                           UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

                                        .)

-    | "." Ident<out x>

-      "("                              (. args = new List<Expression/*!*/>(); .)

+    | "." Ident<out x>                 

+      "("                              (. // This case happens when we have type<typeargs>.Constructor(args)

+                                          // There is no ambiguity about where the constructor is or whether one exists.

+                                          args = new List<Expression/*!*/>(); .)

         [ Expressions<args> ]

       ")"                              (. initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); .)

     | "("                              (. var udf = ty as UserDefinedType;

-                                          if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) {

-                                            // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as

+                                          if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) {

+                                            // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as

                                             // the name of the constructor that's being invoked.

                                             x = udf.tok;

-                                            ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List<Type>(), null);

+                                            ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List<Type>(), udf.Path.GetRange(0,udf.Path.Count-1));

                                           } else {

                                             SemErr(t, "expected '.'");

                                             x = null;

@@ -1467,8 +1483,6 @@ EndlessExpression<out Expression e>
 = (. IToken/*!*/ x;

      Expression e0, e1;

      e = dummyExpr;

-     BoundVar d;

-     List<BoundVar> letVars;  List<Expression> letRHSs;

   .)

   ( "if"                            (. x = t; .)

     Expression<out e>

@@ -1483,7 +1497,18 @@ EndlessExpression<out Expression e>
   | "assume"                        (. x = t; .)

     Expression<out e0> ";"

     Expression<out e1>              (. e = new AssumeExpr(x, e0, e1); .)

-  | "var"                           (. x = t;

+  | LetExpr<out e>

+  | NamedExpr<out e>

+  )

+  .

+

+LetExpr<out Expression e>

+= (. IToken/*!*/ x;

+     e = dummyExpr;

+     BoundVar d;

+     List<BoundVar> letVars;  List<Expression> letRHSs;

+  .)

+    "var"                           (. x = t;

                                        letVars = new List<BoundVar>();

                                        letRHSs = new List<Expression>(); .)

     IdentTypeOptional<out d>        (. letVars.Add(d); .)

@@ -1495,8 +1520,20 @@ EndlessExpression<out Expression e>
     }

     ";"

     Expression<out e>               (. e = new LetExpr(x, letVars, letRHSs, e); .)

-  )

   .

+

+NamedExpr<out Expression e>

+= (. IToken/*!*/ x, d;

+     e = dummyExpr;

+     Expression expr;

+  .)

+    "expr"                          (. x = t; .)

+    NoUSIdent<out d>

+    ":"

+    Expression<out e>               (. expr = e;

+                                       e = new NamedExpr(x, d.val, expr); .)

+  .

+

 MatchExpression<out Expression/*!*/ e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

      List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();