1 files changed, 20 insertions, 11 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 3811cbbf..2d3d93d6 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -143,9 +143,9 @@ bool IsIdentParen() {
   return la.kind == _ident && x.kind == _openparen;
 }
 
-bool IsIdentColon() {
+bool IsIdentColonOrBar() {
   Token x = scanner.Peek();
-  return la.kind == _ident && x.kind == _colon;
+  return la.kind == _ident && (x.kind == _colon || x.kind == _verticalbar);
 }
 
 bool SemiFollowsCall(bool allowSemi, Expression e) {
@@ -200,6 +200,7 @@ TOKENS
   arrayToken = "array" [posDigit {digit}].
   string = quote {nonquote} quote.
   colon = ':'.
+  verticalbar = '|'.
   semi = ';'.
   darrow = "=>".
   arrow = "->".
@@ -457,20 +458,19 @@ NewtypeDecl<ModuleDefinition module, out TopLevelDecl td>
 = (. IToken id, bvId;
      Attributes attrs = null;
      td = null;
-     Type baseType;
+     Type baseType = null;
      Expression wh;
   .)
   "newtype"
   { Attribute<ref attrs> }
   NoUSIdent<out id>
   "="
-  ( IF(IsIdentColon())
+  ( IF(IsIdentColonOrBar())
     NoUSIdent<out bvId>
-    ":"
-    Type<out baseType>
-    "where"
-    Expression<out wh, false, true>  (. td = new DerivedTypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
-  | Type<out baseType>               (. td = new DerivedTypeDecl(id, id.val, module, baseType, attrs); .)
+    [ ":" Type<out baseType> ]       (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false); } .)
+    "|"
+    Expression<out wh, false, true>  (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
+  | Type<out baseType>               (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .)
   )
   [ SYNC ";"
       // In a future version of Dafny, including the following warning message:
@@ -890,11 +890,13 @@ TypeAndToken<out IToken tok, out Type ty>
     | ReferenceType<out tok, out ty>
   )
   [ (. Type t2; .)
-    "->" Type<out t2>
+    "->"                  (. tok = t; .)
+    Type<out t2>
     (. if (gt == null) {
          gt = new List<Type>{ ty };
        }
-       ty = new ArrowType(gt, t2);
+       ty = new ArrowType(tok, gt, t2);
+       theBuiltIns.CreateArrowTypeDecl(gt.Count);
     .)
   ]
 
@@ -1019,6 +1021,11 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
      }
      f.BodyStartTok = bodyStart;
      f.BodyEndTok = bodyEnd;
+     theBuiltIns.CreateArrowTypeDecl(formals.Count);
+     if (isCoPredicate) {
+       // also create an arrow type for the corresponding prefix predicate
+       theBuiltIns.CreateArrowTypeDecl(formals.Count);
+     }
   .)
   .
 FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases.>
@@ -2081,6 +2088,7 @@ ParensExpression<out Expression e, bool allowSemi, bool allowLambda>
          }
        }
        e = new LambdaExpr(x, oneShot, bvs, req, reads, body);
+       theBuiltIns.CreateArrowTypeDecl(bvs.Count);
        isLambda = true;
     .)
   ]
@@ -2353,6 +2361,7 @@ DottedIdentifiersAndFunction<out Expression e, bool allowSemi, bool allowLambda>
        }
        BoundVar bv = new BoundVar(id, UnwildIdent(id.val, true),  new InferredTypeProxy());
        e = new LambdaExpr(id, oneShot, new List<BoundVar>{ bv }, req, reads, body);
+       theBuiltIns.CreateArrowTypeDecl(1);
     .)
   ]
   // If it wasn't a lambda expression, then it indeed is an identifier sequence