Dafny: Record source positions of start/end curly braces for declaration constructs.

Dafny VS2010 extension:  link with Dafny and use it to parse and type check

4 files changed, 86 insertions, 37 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index cfb9be3e..eeb8024a 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -197,11 +197,12 @@ Dafny
     { Attribute<ref attrs> }

     Ident<out id>

     [ "imports" Idents<theImports> ]     (. module = new ModuleDecl(id, id.val, theImports, attrs); .)

-    "{"

+    "{"                                  (. module.BodyStartTok = t; .)

       { ClassDecl<module, out c>         (. module.TopLevelDecls.Add(c); .)

       | DatatypeDecl<module, out dt>     (. module.TopLevelDecls.Add(dt); .)

-      }                                  (. theModules.Add(module); .)

-    "}"

+      }

+    "}"                                  (. module.BodyEndTok = t;

+                                            theModules.Add(module); .)

   | ClassDecl<defaultModule, out c>      (. defaultModule.TopLevelDecls.Add(c); .)

   | DatatypeDecl<defaultModule, out dt>  (. defaultModule.TopLevelDecls.Add(dt); .)

   | ClassMemberDecl<membersDefaultClass>

@@ -232,6 +233,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
      IToken/*!*/ idRefined;

      IToken optionalId = null;

      List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

+     IToken bodyStart;

   .)

   "class"

   { Attribute<ref attrs> }

@@ -239,7 +241,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
   [ GenericParameters<typeArgs> ]

   [ "refines" Ident<out idRefined>               (. optionalId = idRefined; .)

   ]

-  "{"

+  "{"                                            (. bodyStart = t; .)

   { ClassMemberDecl<members>

   }

   "}"                                      

@@ -247,6 +249,8 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
        c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

      else 

        c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

+     c.BodyStartTok = bodyStart;

+     c.BodyEndTok = t;

   .)

   .

 

@@ -274,15 +278,19 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
      Attributes attrs = null;

      List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();

      List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();

+     IToken bodyStart;

   .)

   "datatype"

   { Attribute<ref attrs> }

   Ident<out id>

   [ GenericParameters<typeArgs> ]

-  "{"

+  "{"                                      (. bodyStart = t; .)

   { DatatypeMemberDecl<ctors>

   }

-  "}"                                      (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); .)

+  "}"                                      (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

+                                              dt.BodyStartTok = bodyStart;

+                                              dt.BodyEndTok = t;

+                                           .)

   .

 

 DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>

@@ -425,6 +433,8 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
      List<Expression/*!*/> dec = new List<Expression/*!*/>();

      Statement/*!*/ bb;  BlockStmt body = null;

      bool isRefinement = false;

+     IToken bodyStart = Token.NoToken;

+     IToken bodyEnd = Token.NoToken;

   .)

   ( "method"

   | "refines"                                               (. isRefinement = true; .)

@@ -441,7 +451,7 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
   ]

 

   ( ";" { MethodSpec<req, mod, ens, dec> }

-  | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb>    (. body = (BlockStmt)bb; .)

+  | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb, out bodyStart, out bodyEnd>    (. body = (BlockStmt)bb; .)

   )

   

   (. parseVarScope.PopMarker();

@@ -449,6 +459,8 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
        m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

      else 

        m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

+     m.BodyStartTok = bodyStart;

+     m.BodyEndTok = bodyEnd;

  .)

   .

 

@@ -566,6 +578,8 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
      List<Expression/*!*/> decreases = new List<Expression/*!*/>();

      Expression/*!*/ bb;  Expression body = null;

      bool isFunctionMethod = false;

+     IToken bodyStart = Token.NoToken;

+     IToken bodyEnd = Token.NoToken;

   .)

   "function"

   [ "method"                 (. isFunctionMethod = true; .)

@@ -582,10 +596,12 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   ( ";"

     { FunctionSpec<reqs, reads, decreases> }

   | { FunctionSpec<reqs, reads, decreases> }

-    FunctionBody<out bb>                (. body = bb; .)

+    FunctionBody<out bb, out bodyStart, out bodyEnd>  (. body = bb; .)

   )

   (. parseVarScope.PopMarker();

      f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);

+     f.BodyStartTok = bodyStart;

+     f.BodyEndTok = bodyEnd;

   .)

   .

 

@@ -633,13 +649,13 @@ FrameExpression<out FrameExpression/*!*/ fe>
   (. fe = new FrameExpression(e, fieldName); .)

   .

 

-FunctionBody<out Expression/*!*/ e>

+FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)

-  "{"

+  "{"                         (. bodyStart = t; .)

   ( MatchExpression<out e>

   | Expression<out e>

   )

-  "}"

+  "}"                         (. bodyEnd = t; .)

   .

   

 MatchExpression<out Expression/*!*/ e>

@@ -674,26 +690,29 @@ CaseExpression<out MatchCaseExpr/*!*/ c>
 

 /*------------------------------------------------------------------------*/

 

-BlockStmt<out Statement/*!*/ block>

-= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null); IToken/*!*/ x;

+BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>

+= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);

      List<Statement/*!*/> body = new List<Statement/*!*/>();

   .)

   (. parseVarScope.PushMarker(); .)

-  "{"                                  (. x = t; .)

+  "{"                                  (. bodyStart = t; .)

   { Stmt<body>

   }

-  "}"                                  (. block = new BlockStmt(x, body); .)

+  "}"                                  (. bodyEnd = t;

+                                          block = new BlockStmt(bodyStart, body); .)

   (. parseVarScope.PopMarker(); .)

   .

 

 Stmt<.List<Statement/*!*/>/*!*/ ss.>

-= (. Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s; .)

+= (. Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s;

+     IToken bodyStart, bodyEnd;

+  .)

   /* By first reading a sequence of block statements, we avoid problems in the generated parser, despite

      the ambiguity in the grammar.  See Note in ConstAtomExpression production.

   */

-  { BlockStmt<out s>                   (. ss.Add(s); .)

+  { BlockStmt<out s, out bodyStart, out bodyEnd>  (. ss.Add(s); .)

   }

-  ( OneStmt<out s>                     (. ss.Add(s); .)

+  ( OneStmt<out s>                                (. ss.Add(s); .)

   | VarDeclStmts<ss>

   )

   .

@@ -820,13 +839,14 @@ IfStmt<out Statement/*!*/ ifStmt>
      Statement/*!*/ thn;

      Statement/*!*/ s;

      Statement els = null;

+     IToken bodyStart, bodyEnd;

   .)

   "if"                       (. x = t; .)

   Guard<out guard>

-  BlockStmt<out thn>

+  BlockStmt<out thn, out bodyStart, out bodyEnd>

   [ "else"

-    ( IfStmt<out s>          (. els = s; .)

-    | BlockStmt<out s>       (. els = s; .)

+    ( IfStmt<out s>                                 (. els = s; .)

+    | BlockStmt<out s, out bodyStart, out bodyEnd>  (. els = s; .)

     )

   ]

   (. ifStmt = new IfStmt(x, guard, thn, els); .)

@@ -839,6 +859,7 @@ WhileStmt<out Statement/*!*/ stmt>
      List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();

      List<Expression/*!*/> decreases = new List<Expression/*!*/>();

      Statement/*!*/ body;

+     IToken bodyStart, bodyEnd;

   .)

   "while"                    (. x = t; .)

   Guard<out guard>           (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)

@@ -854,7 +875,7 @@ WhileStmt<out Statement/*!*/ stmt>
      }

      ";"

   }

-  BlockStmt<out body>        (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)

+  BlockStmt<out body, out bodyStart, out bodyEnd>  (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)

   .

 

 Guard<out Expression e>   /* null represents demonic-choice */

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 27f5e3a5..f83dd67a 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -505,6 +505,8 @@ namespace Microsoft.Dafny {
     }

 

     public IToken/*!*/ tok;

+    public IToken BodyStartTok = Token.NoToken;

+    public IToken BodyEndTok = Token.NoToken;

     public readonly string/*!*/ Name;

     public readonly Attributes Attributes;

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index cc295157..2dc77103 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -243,6 +243,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 				}

 				module = new ModuleDecl(id, id.val, theImports, attrs); 

 				Expect(7);

+				module.BodyStartTok = t; 

 				while (la.kind == 9 || la.kind == 14) {

 					if (la.kind == 9) {

 						ClassDecl(module, out c);

@@ -252,8 +253,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 						module.TopLevelDecls.Add(dt); 

 					}

 				}

-				theModules.Add(module); 

 				Expect(8);

+				module.BodyEndTok = t;

+				theModules.Add(module); 

 			} else if (la.kind == 9) {

 				ClassDecl(defaultModule, out c);

 				defaultModule.TopLevelDecls.Add(c); 

@@ -313,6 +315,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		IToken/*!*/ idRefined;

 		IToken optionalId = null;

 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

+		IToken bodyStart;

 		

 		Expect(9);

 		while (la.kind == 7) {

@@ -328,6 +331,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			optionalId = idRefined; 

 		}

 		Expect(7);

+		bodyStart = t; 

 		while (StartOf(2)) {

 			ClassMemberDecl(members);

 		}

@@ -336,6 +340,8 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		 c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

 		else 

 		  c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

+		c.BodyStartTok = bodyStart;

+		c.BodyEndTok = t;

 		

 	}

 

@@ -346,6 +352,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Attributes attrs = null;

 		List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();

 		List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();

+		IToken bodyStart;

 		

 		Expect(14);

 		while (la.kind == 7) {

@@ -356,11 +363,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			GenericParameters(typeArgs);

 		}

 		Expect(7);

+		bodyStart = t; 

 		while (la.kind == 1 || la.kind == 7) {

 			DatatypeMemberDecl(ctors);

 		}

 		Expect(8);

-		dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); 

+		dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

+		dt.BodyStartTok = bodyStart;

+		dt.BodyEndTok = t;

+		

 	}

 

 	void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm) {

@@ -442,6 +453,8 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		List<Expression/*!*/> decreases = new List<Expression/*!*/>();

 		Expression/*!*/ bb;  Expression body = null;

 		bool isFunctionMethod = false;

+		IToken bodyStart = Token.NoToken;

+		IToken bodyEnd = Token.NoToken;

 		

 		Expect(37);

 		if (la.kind == 23) {

@@ -470,11 +483,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			while (la.kind == 27 || la.kind == 29 || la.kind == 38) {

 				FunctionSpec(reqs, reads, decreases);

 			}

-			FunctionBody(out bb);

+			FunctionBody(out bb, out bodyStart, out bodyEnd);

 			body = bb; 

 		} else SynErr(105);

 		parseVarScope.PopMarker();

 		f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);

+		f.BodyStartTok = bodyStart;

+		f.BodyEndTok = bodyEnd;

 		

 	}

 

@@ -491,6 +506,8 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		List<Expression/*!*/> dec = new List<Expression/*!*/>();

 		Statement/*!*/ bb;  BlockStmt body = null;

 		bool isRefinement = false;

+		IToken bodyStart = Token.NoToken;

+		IToken bodyEnd = Token.NoToken;

 		

 		if (la.kind == 23) {

 			Get();

@@ -522,7 +539,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			while (StartOf(4)) {

 				MethodSpec(req, mod, ens, dec);

 			}

-			BlockStmt(out bb);

+			BlockStmt(out bb, out bodyStart, out bodyEnd);

 			body = (BlockStmt)bb; 

 		} else SynErr(107);

 		parseVarScope.PopMarker();

@@ -530,6 +547,8 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		  m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

 		else 

 		  m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

+		m.BodyStartTok = bodyStart;

+		m.BodyEndTok = bodyEnd;

 		

 	}

 

@@ -773,18 +792,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else SynErr(111);

 	}

 

-	void BlockStmt(out Statement/*!*/ block) {

-		Contract.Ensures(Contract.ValueAtReturn(out block) != null); IToken/*!*/ x;

+	void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {

+		Contract.Ensures(Contract.ValueAtReturn(out block) != null);

 		List<Statement/*!*/> body = new List<Statement/*!*/>();

 		

 		parseVarScope.PushMarker(); 

 		Expect(7);

-		x = t; 

+		bodyStart = t; 

 		while (StartOf(9)) {

 			Stmt(body);

 		}

 		Expect(8);

-		block = new BlockStmt(x, body); 

+		bodyEnd = t;

+		block = new BlockStmt(bodyStart, body); 

 		parseVarScope.PopMarker(); 

 	}

 

@@ -881,15 +901,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else SynErr(113);

 	}

 

-	void FunctionBody(out Expression/*!*/ e) {

+	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; 

 		Expect(7);

+		bodyStart = t; 

 		if (la.kind == 41) {

 			MatchExpression(out e);

 		} else if (StartOf(8)) {

 			Expression(out e);

 		} else SynErr(114);

 		Expect(8);

+		bodyEnd = t; 

 	}

 

 	void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {

@@ -955,9 +977,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void Stmt(List<Statement/*!*/>/*!*/ ss) {

-		Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s; 

+		Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s;

+		IToken bodyStart, bodyEnd;

+		

 		while (la.kind == 7) {

-			BlockStmt(out s);

+			BlockStmt(out s, out bodyStart, out bodyEnd);

 			ss.Add(s); 

 		}

 		if (StartOf(11)) {

@@ -1202,18 +1226,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Statement/*!*/ thn;

 		Statement/*!*/ s;

 		Statement els = null;

+		IToken bodyStart, bodyEnd;

 		

 		Expect(52);

 		x = t; 

 		Guard(out guard);

-		BlockStmt(out thn);

+		BlockStmt(out thn, out bodyStart, out bodyEnd);

 		if (la.kind == 53) {

 			Get();

 			if (la.kind == 52) {

 				IfStmt(out s);

 				els = s; 

 			} else if (la.kind == 7) {

-				BlockStmt(out s);

+				BlockStmt(out s, out bodyStart, out bodyEnd);

 				els = s; 

 			} else SynErr(119);

 		}

@@ -1227,6 +1252,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();

 		List<Expression/*!*/> decreases = new List<Expression/*!*/>();

 		Statement/*!*/ body;

+		IToken bodyStart, bodyEnd;

 		

 		Expect(54);

 		x = t; 

@@ -1255,7 +1281,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expect(15);

 			}

 		}

-		BlockStmt(out body);

+		BlockStmt(out body, out bodyStart, out bodyEnd);

 		stmt = new WhileStmt(x, guard, invariants, decreases, body); 

 	}

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2c1a9175..87ef94d5 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -12,7 +12,7 @@ using Microsoft.Boogie;
 namespace Microsoft.Dafny {

   public class Resolver {

     public int ErrorCount = 0;

-    void Error(IToken tok, string msg, params object[] args) {

+    protected virtual void Error(IToken tok, string msg, params object[] args) {

       Contract.Requires(tok != null);

       Contract.Requires(msg != null);

       ConsoleColor col = Console.ForegroundColor;