diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Cloner.cs | 3 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 11 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 83 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 98 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 107 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 13 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 3 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 20 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.csproj | 2 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 7 | ||||
| -rw-r--r-- | Source/DafnyExtension/TokenTagger.cs | 84 |
12 files changed, 346 insertions, 89 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 537dae1d..5b8f8cc5 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -30,6 +30,9 @@ namespace Microsoft.Dafny if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, CloneAttributes(dd.Attributes));
+ } else if (d is TupleTypeDecl) {
+ var dd = (TupleTypeDecl)d;
+ return new TupleTypeDecl(dd.Dims, dd.Module);
} else if (d is IndDatatypeDecl) {
var dd = (IndDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 56c6edc2..fcf8a2ca 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -107,6 +107,10 @@ namespace Microsoft.Dafny { indent += IndentAmount;
}
foreach (TopLevelDecl d in m.TopLevelDecls) {
+ bool compileIt = true;
+ if (Attributes.ContainsBool(d.Attributes, "compile", ref compileIt) && !compileIt) {
+ continue;
+ }
wr.WriteLine();
if (d is ArbitraryTypeDecl) {
var at = (ArbitraryTypeDecl)d;
@@ -411,7 +415,12 @@ namespace Microsoft.Dafny { if (dt is IndDatatypeDecl) {
Indent(ind); wr.WriteLine("public override string ToString() {");
- string nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;
+ string nm;
+ if (dt is TupleTypeDecl) {
+ nm = "";
+ } else {
+ nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;
+ }
Indent(ind + IndentAmount); wr.WriteLine("string s = \"{0}\";", nm);
if (ctor.Formals.Count != 0) {
Indent(ind + IndentAmount); wr.WriteLine("s += \"(\";");
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2ab70c4f..5c1148c6 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -739,8 +739,9 @@ Type<out Type/*!*/ ty> TypeAndToken<out tok, out ty>
.
TypeAndToken<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*/
- List<Type/*!*/>/*!*/ gt;
+= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
+ tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
+ List<Type> gt;
.)
( "bool" (. tok = t; .)
| "nat" (. tok = t; ty = new NatType(); .)
@@ -774,6 +775,20 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty> ty = new MapType(gt[0], gt[1]);
}
.)
+ | "(" (. tok = t; gt = new List<Type>(); .)
+ [ Type<out ty> (. gt.Add(ty); .)
+ { "," Type<out ty> (. gt.Add(ty); .)
+ }
+ ]
+ ")" (. if (gt.Count == 1) {
+ // just return the type 'ty'
+ } else {
+ // make sure the nullary tuple type exists
+ var dims = gt.Count;
+ var tmp = theBuiltIns.TupleType(tok, dims, true);
+ ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List<IToken>());
+ }
+ .)
| ReferenceType<out tok, out ty>
)
.
@@ -1876,25 +1891,51 @@ ConstAtomExpression<out Expression e> | "|" (. x = t; .)
Expression<out e, true> (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)
"|"
- | "(" (. x = t; .)
- Expression<out e, true> (. e = new ParensExpression(x, e); .)
- ")"
- | "real" (. x = t; .)
- "(" (. IToken openParen = t; .)
- Expression<out e, true>
- ")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
- IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
- e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
- .)
- | "int" (. x = t; .)
- "(" (. IToken openParen = t; .)
- Expression<out e, true>
- ")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
- IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";
- //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
- e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
- .)
+ | ParensExpression<out e>
+ | "real" (. x = t; .)
+ "(" (. IToken openParen = t; .)
+ Expression<out e, true>
+ ")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
+ IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
+ .)
+ | "int" (. x = t; .)
+ "(" (. IToken openParen = t; .)
+ Expression<out e, true>
+ ")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
+ IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
+ .)
+ )
+ .
+ParensExpression<out Expression e>
+= (. IToken x;
+ List<Expression> args = null;
+ .)
+ "(" (. x = t; e = null; .)
+ ( ")" (. // unit
+ // make sure the nullary tuple type exists
+ var tmp = theBuiltIns.TupleType(x, 0, true);
+ e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List<Expression>());
+ .)
+ | Expression<out e, true>
+ { "," (. if (args == null) {
+ args = new List<Expression>();
+ args.Add(e); // add the first argument, which was parsed above
+ }
+ .)
+ Expression<out e, true> (. args.Add(e); .)
+ }
+ ")" (. if (args == null) {
+ e = new ParensExpression(x, e);
+ } else {
+ // make sure the corresponding tuple type exists
+ var tmp = theBuiltIns.TupleType(x, args.Count, true);
+ e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);
+ }
+ .)
)
.
DisplayExpr<out Expression e>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ad98a0c0..55dc973f 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -88,15 +88,17 @@ namespace Microsoft.Dafny { {
public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, null, true);
Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();
+ Dictionary<int, TupleTypeDecl> tupleTypeDecls = new Dictionary<int, TupleTypeDecl>();
public readonly ClassDecl ObjectDecl;
public readonly ClassDecl RealClass;
//public readonly Function RealToInt;
//public readonly Function IntToReal;
public BuiltIns() {
// create class 'object'
- ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), null);
+ ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile());
SystemModule.TopLevelDecls.Add(ObjectDecl);
// add one-dimensional arrays, since they may arise during type checking
+ // Arrays of other dimensions may be added during parsing as the parser detects the need for these
UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);
// add real number functions
Function RealToInt = new Function(Token.NoToken, "RealToInt", true, true, new List<TypeParameter>(), Token.NoToken,
@@ -108,12 +110,19 @@ namespace Microsoft.Dafny { new List<FrameExpression>(), new List<Expression>(), new Specification<Expression>(new List<Expression>(), null),
null, null, Token.NoToken);
RealClass = new ClassDecl(Token.NoToken, "Real", SystemModule, new List<TypeParameter>(),
- new List<MemberDecl>() { RealToInt, IntToReal }, null);
+ new List<MemberDecl>() { RealToInt, IntToReal }, DontCompile());
RealToInt.EnclosingClass = RealClass;
IntToReal.EnclosingClass = RealClass;
RealToInt.IsBuiltin = true;
IntToReal.IsBuiltin = true;
SystemModule.TopLevelDecls.Add(RealClass);
+ // Note, in addition to these types, the _System module contains tuple types. These tuple types are added to SystemModule
+ // by the parser as the parser detects the need for these.
+ }
+
+ private Attributes DontCompile() {
+ var flse = new Attributes.Argument(Token.NoToken, Expression.CreateBoolLiteral(Token.NoToken, false));
+ return new Attributes("compile", new List<Attributes.Argument>() { flse }, null);
}
public UserDefinedType ArrayType(int dims, Type arg) {
@@ -129,7 +138,7 @@ namespace Microsoft.Dafny { typeArgs.Add(arg);
UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null);
if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
- ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);
+ ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile());
for (int d = 0; d < dims; d++) {
string name = dims == 1 ? "Length" : "Length" + d;
string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")";
@@ -152,6 +161,30 @@ namespace Microsoft.Dafny { return "array" + dims;
}
}
+
+ public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType) {
+ Contract.Requires(tok != null);
+ Contract.Requires(0 <= dims);
+ Contract.Ensures(Contract.Result<TupleTypeDecl>() != null);
+
+ TupleTypeDecl tt;
+ if (!tupleTypeDecls.TryGetValue(dims, out tt)) {
+ Contract.Assume(allowCreationOfNewType); // the parser should ensure that all needed tuple types exist by the time of resolution
+ tt = new TupleTypeDecl(dims, SystemModule);
+ tupleTypeDecls.Add(dims, tt);
+ SystemModule.TopLevelDecls.Add(tt);
+ }
+ return tt;
+ }
+ public static string TupleTypeName(int dims) {
+ Contract.Requires(0 <= dims);
+ return "_tuple#" + dims;
+ }
+ public static bool IsTupleTypeName(string s) {
+ Contract.Requires(s != null);
+ return s.StartsWith("_tuple#");
+ }
+ public const string TupleTypeCtorName = "_#Make"; // the printer wants this name to be uniquely recognizable
}
public class Attributes {
@@ -714,6 +747,9 @@ namespace Microsoft.Dafny { [Pure]
public override string TypeName(ModuleDefinition context) {
Contract.Ensures(Contract.Result<string>() != null);
+ if (BuiltIns.IsTupleTypeName(Name)) {
+ return "(" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ")";
+ }
string s = "";
foreach (var t in Path) {
if (context != null && t == context.tok) {
@@ -1355,10 +1391,10 @@ namespace Microsoft.Dafny { public class ArrayClassDecl : ClassDecl {
public readonly int Dims;
- public ArrayClassDecl(int dims, ModuleDefinition module)
+ public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs)
: base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,
new List<TypeParameter>(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),
- new List<MemberDecl>(), null)
+ new List<MemberDecl>(), attrs)
{
Contract.Requires(1 <= dims);
Contract.Requires(module != null);
@@ -1367,7 +1403,8 @@ namespace Microsoft.Dafny { }
}
- public abstract class DatatypeDecl : TopLevelDecl {
+ public abstract class DatatypeDecl : TopLevelDecl
+ {
public readonly List<DatatypeCtor> Ctors;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -1413,6 +1450,52 @@ namespace Microsoft.Dafny { }
}
+ public class TupleTypeDecl : IndDatatypeDecl
+ {
+ public readonly int Dims;
+ /// <summary>
+ /// Construct a resolved built-in tuple type with "dim" arguments. "systemModule" is expected to be the _System module.
+ /// </summary>
+ public TupleTypeDecl(int dims, ModuleDefinition systemModule)
+ : this(systemModule, CreateTypeParameters(dims)) {
+ Contract.Requires(0 <= dims);
+ Contract.Requires(systemModule != null);
+ }
+ private TupleTypeDecl(ModuleDefinition systemModule, List<TypeParameter> typeArgs)
+ : base(Token.NoToken, BuiltIns.TupleTypeName(typeArgs.Count), systemModule, typeArgs, CreateConstructors(typeArgs), null) {
+ Contract.Requires(systemModule != null);
+ Contract.Requires(typeArgs != null);
+ Dims = typeArgs.Count;
+ foreach (var ctor in Ctors) {
+ ctor.EnclosingDatatype = this; // resolve here
+ DefaultCtor = ctor;
+ TypeParametersUsedInConstructionByDefaultCtor = new bool[typeArgs.Count];
+ for (int i = 0; i < typeArgs.Count; i++) {
+ TypeParametersUsedInConstructionByDefaultCtor[i] = true;
+ }
+ }
+ }
+ private static List<TypeParameter> CreateTypeParameters(int dims) {
+ Contract.Requires(0 <= dims);
+ var ts = new List<TypeParameter>();
+ for (int i = 0; i < dims; i++) {
+ ts.Add(new TypeParameter(Token.NoToken, "T" + i));
+ }
+ return ts;
+ }
+ private static List<DatatypeCtor> CreateConstructors(List<TypeParameter> typeArgs) {
+ Contract.Requires(typeArgs != null);
+ var formals = new List<Formal>();
+ for (int i = 0; i < typeArgs.Count; i++) {
+ var tp = typeArgs[i];
+ var f = new Formal(Token.NoToken, i.ToString(), new UserDefinedType(Token.NoToken, tp.Name, tp), true, false);
+ formals.Add(f);
+ }
+ var ctor = new DatatypeCtor(Token.NoToken, BuiltIns.TupleTypeCtorName, formals, null);
+ return new List<DatatypeCtor>() { ctor };
+ }
+ }
+
public class CoDatatypeDecl : DatatypeDecl
{
public CoDatatypeDecl SscRepr; // filled in during resolution
@@ -1918,7 +2001,7 @@ namespace Microsoft.Dafny { }
return UniqueName;
}
- static char[] specialChars = new char[] { '\'', '_', '?', '\\' };
+ static char[] specialChars = new char[] { '\'', '_', '?', '\\', '#' };
public static string CompilerizeName(string nm) {
if ('0' <= nm[0] && nm[0] <= '9') {
// the identifier is one that consists of just digits
@@ -1942,6 +2025,7 @@ namespace Microsoft.Dafny { case '_': name += "__"; break;
case '?': name += "_q"; break;
case '\\': name += "_b"; break;
+ case '#': name += "_h"; break;
default:
Contract.Assume(false); // unexpected character
break;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 969774db..a7f058db 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1115,8 +1115,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { }
void TypeAndToken(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*/
- List<Type/*!*/>/*!*/ gt;
+ Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
+ tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
+ List<Type> gt;
switch (la.kind) {
case 52: {
@@ -1195,6 +1196,30 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { break;
}
+ case 11: {
+ Get();
+ tok = t; gt = new List<Type>();
+ if (StartOf(10)) {
+ Type(out ty);
+ gt.Add(ty);
+ while (la.kind == 31) {
+ Get();
+ Type(out ty);
+ gt.Add(ty);
+ }
+ }
+ Expect(12);
+ if (gt.Count == 1) {
+ // just return the type 'ty'
+ } else {
+ // make sure the nullary tuple type exists
+ var dims = gt.Count;
+ var tmp = theBuiltIns.TupleType(tok, dims, true);
+ ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List<IToken>());
+ }
+
+ break;
+ }
case 1: case 5: case 60: {
ReferenceType(out tok, out ty);
break;
@@ -3352,11 +3377,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break;
}
case 11: {
- Get();
- x = t;
- Expression(out e, true);
- e = new ParensExpression(x, e);
- Expect(12);
+ ParensExpression(out e);
break;
}
case 55: {
@@ -3427,6 +3448,41 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
+ void ParensExpression(out Expression e) {
+ IToken x;
+ List<Expression> args = null;
+
+ Expect(11);
+ x = t; e = null;
+ if (la.kind == 12) {
+ Get();
+ var tmp = theBuiltIns.TupleType(x, 0, true);
+ e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List<Expression>());
+
+ } else if (StartOf(16)) {
+ Expression(out e, true);
+ while (la.kind == 31) {
+ Get();
+ if (args == null) {
+ args = new List<Expression>();
+ args.Add(e); // add the first argument, which was parsed above
+ }
+
+ Expression(out e, true);
+ args.Add(e);
+ }
+ Expect(12);
+ if (args == null) {
+ e = new ParensExpression(x, e);
+ } else {
+ // make sure the corresponding tuple type exists
+ var tmp = theBuiltIns.TupleType(x, args.Count, true);
+ e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);
+ }
+
+ } else SynErr(223);
+ }
+
void MapLiteralExpressions(out List<ExpressionPair> elements) {
Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
@@ -3448,7 +3504,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 125) {
Get();
- } else SynErr(223);
+ } else SynErr(224);
}
void MatchExpression(out Expression e, bool allowSemi) {
@@ -3471,7 +3527,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(10);
} else if (StartOf(31)) {
if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); }
- } else SynErr(224);
+ } else SynErr(225);
e = new MatchExpr(x, e, cases, usesOptionalBrace);
}
@@ -3489,7 +3545,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 122 || la.kind == 123) {
Exists();
x = t;
- } else SynErr(225);
+ } else SynErr(226);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body, allowSemi);
@@ -3537,7 +3593,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s);
} else if (la.kind == 88) {
CalcStmt(out s);
- } else SynErr(226);
+ } else SynErr(227);
}
void LetExpr(out Expression e, bool allowSemi) {
@@ -3577,7 +3633,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- } else SynErr(227);
+ } else SynErr(228);
Expression(out e, false);
letRHSs.Add(e);
while (la.kind == 31) {
@@ -3628,7 +3684,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
pat = new CasePattern(bv.tok, bv);
- } else SynErr(228);
+ } else SynErr(229);
}
void CaseExpression(out MatchCaseExpr c, bool allowSemi) {
@@ -3661,7 +3717,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 121) {
Get();
- } else SynErr(229);
+ } else SynErr(230);
}
void Exists() {
@@ -3669,7 +3725,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 123) {
Get();
- } else SynErr(230);
+ } else SynErr(231);
}
void AttributeBody(ref Attributes attrs) {
@@ -3714,8 +3770,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,T,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,x,x, x,T,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
@@ -3986,14 +4042,15 @@ public class Errors { case 220: s = "invalid MultiSetExpr"; break;
case 221: s = "invalid ConstAtomExpression"; break;
case 222: s = "invalid Nat"; break;
- case 223: s = "invalid QSep"; break;
- case 224: s = "invalid MatchExpression"; break;
- case 225: s = "invalid QuantifierGuts"; break;
- case 226: s = "invalid StmtInExpr"; break;
- case 227: s = "invalid LetExpr"; break;
- case 228: s = "invalid CasePattern"; break;
- case 229: s = "invalid Forall"; break;
- case 230: s = "invalid Exists"; break;
+ case 223: s = "invalid ParensExpression"; break;
+ case 224: s = "invalid QSep"; break;
+ case 225: s = "invalid MatchExpression"; break;
+ case 226: s = "invalid QuantifierGuts"; break;
+ case 227: s = "invalid StmtInExpr"; break;
+ case 228: s = "invalid LetExpr"; break;
+ case 229: s = "invalid CasePattern"; break;
+ case 230: s = "invalid Forall"; break;
+ case 231: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 0a970498..5be5614d 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1191,9 +1191,16 @@ namespace Microsoft.Dafny { wr.Write(((IdentifierExpr)expr).Name);
} else if (expr is DatatypeValue) {
- DatatypeValue dtv = (DatatypeValue)expr;
- wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);
- if (dtv.Arguments.Count != 0) {
+ var dtv = (DatatypeValue)expr;
+ bool printParens;
+ if (dtv.MemberName == BuiltIns.TupleTypeCtorName) {
+ // we're looking at a tuple, whose printed constructor name is essentially the empty string
+ printParens = true;
+ } else {
+ wr.Write("{0}.{1}", dtv.DatatypeName, dtv.MemberName);
+ printParens = dtv.Arguments.Count != 0;
+ }
+ if (printParens) {
wr.Write("(");
PrintExpressionList(dtv.Arguments, false);
wr.Write(")");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 8de010fb..73925aef 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -197,6 +197,7 @@ namespace Microsoft.Dafny rewriters.Add(opaqueRewriter);
systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);
+ prog.CompileModules.Add(prog.BuiltIns.SystemModule);
foreach (var decl in sortedDecls) {
if (decl is LiteralModuleDecl) {
// The declaration is a literal module, so it has members and such that we need
@@ -1019,6 +1020,9 @@ namespace Microsoft.Dafny if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
return new ArbitraryTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, null);
+ } else if (d is TupleTypeDecl) {
+ var dd = (TupleTypeDecl)d;
+ return new TupleTypeDecl(dd.Dims, dd.Module);
} else if (d is IndDatatypeDecl) {
var dd = (IndDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index e2e7155d..3eb06ebc 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -17,6 +17,7 @@ namespace Microsoft.Dafny { public class Translator {
[NotDelayed]
public Translator() {
+ InsertChecksums = 0 < CommandLineOptions.Clo.VerifySnapshots;
Bpl.Program boogieProgram = ReadPrelude();
if (boogieProgram != null) {
sink = boogieProgram;
@@ -2507,7 +2508,7 @@ namespace Microsoft.Dafny { public void InsertUniqueIdForImplementation(Bpl.Declaration decl)
{
var impl = decl as Bpl.Implementation;
- var prefix = UniqueIdPrefix ?? decl.tok.filename;
+ var prefix = UniqueIdPrefix ?? System.Text.RegularExpressions.Regex.Replace(decl.tok.filename, @".v\d+.dfy", ".dfy");
if (impl != null && !string.IsNullOrEmpty(prefix))
{
decl.AddAttribute("id", prefix + ":" + impl.Name + ":0");
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 8f5b5300..01ee269e 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -99,7 +99,7 @@ namespace Microsoft.Dafny }
- static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames)
+ static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true)
{
Contract.Requires(cce.NonNullElements(fileNames));
@@ -110,7 +110,21 @@ namespace Microsoft.Dafny {
Console.WriteLine();
Console.WriteLine("-------------------- {0} --------------------", f);
- var ev = ProcessFiles(new List<string> { f });
+ var ev = ProcessFiles(new List<string> { f }, lookForSnapshots);
+ if (exitValue != ev && ev != ExitValue.VERIFIED)
+ {
+ exitValue = ev;
+ }
+ }
+ return exitValue;
+ }
+
+ if (0 < CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
+ {
+ var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames);
+ foreach (var s in snapshotsByVersion)
+ {
+ var ev = ProcessFiles(new List<string>(s), false);
if (exitValue != ev && ev != ExitValue.VERIFIED)
{
exitValue = ev;
@@ -213,7 +227,7 @@ namespace Microsoft.Dafny ExecutionEngine.CollectModSets(program);
ExecutionEngine.CoalesceBlocks(program);
ExecutionEngine.Inline(program);
- return ExecutionEngine.InferAndVerify(program, stats);
+ return ExecutionEngine.InferAndVerify(program, stats, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? "main_program_id" : null);
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome
diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index 631b0194..cf664364 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -20,7 +20,7 @@ <OldToolsVersion>3.5</OldToolsVersion>
<UpgradeBackupLocation />
<IsWebBootstrapper>false</IsWebBootstrapper>
- <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ <TargetFrameworkProfile></TargetFrameworkProfile>
<PublishUrl>publish\</PublishUrl>
<Install>true</Install>
<InstallFrom>Disk</InstallFrom>
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 36b07d60..ba01c04a 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -249,7 +249,8 @@ namespace DafnyLanguage resolver.ReInitializeVerificationErrors(requestId, boogieProgram.TopLevelDeclarations);
- PipelineOutcome oc = BoogiePipeline(boogieProgram, requestId, er);
+ // TODO(wuestholz): Maybe we should use a fixed program ID to limit the memory overhead due to the program cache in Boogie.
+ PipelineOutcome oc = BoogiePipeline(boogieProgram, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? uniqueIdPrefix : null, requestId, er);
switch (oc) {
case PipelineOutcome.Done:
case PipelineOutcome.VerificationCompleted:
@@ -267,7 +268,7 @@ namespace DafnyLanguage /// else. Hence, any resolution errors and type checking errors are due to errors in
/// the translation.
/// </summary>
- static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, string requestId, ErrorReporterDelegate er)
+ static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, string programId, string requestId, ErrorReporterDelegate er)
{
Contract.Requires(program != null);
@@ -277,7 +278,7 @@ namespace DafnyLanguage ExecutionEngine.CollectModSets(program);
ExecutionEngine.CoalesceBlocks(program);
ExecutionEngine.Inline(program);
- return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), er, requestId);
+ return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), programId, er, requestId);
}
return oc;
}
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index 48f5d1b4..5068354a 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -5,6 +5,7 @@ using System.Linq; using Microsoft.VisualStudio.Text;
using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Utilities;
+using System.Diagnostics.Contracts;
namespace DafnyLanguage
@@ -69,11 +70,12 @@ namespace DafnyLanguage }
}
- internal sealed class DafnyTokenTagger : ITagger<DafnyTokenTag>
+ internal sealed class DafnyTokenTagger : ITagger<DafnyTokenTag>, IDisposable
{
ITextBuffer _buffer;
ITextSnapshot _snapshot;
List<TokenRegion> _regions;
+ bool _disposed;
internal DafnyTokenTagger(ITextBuffer buffer) {
_buffer = buffer;
@@ -83,6 +85,19 @@ namespace DafnyLanguage _buffer.Changed += new EventHandler<TextContentChangedEventArgs>(ReparseFile);
}
+ public void Dispose() {
+ lock (this) {
+ if (!_disposed) {
+ _buffer.Changed -= ReparseFile;
+ _buffer = null;
+ _snapshot = null;
+ _regions = null;
+ _disposed = true;
+ }
+ }
+ GC.SuppressFinalize(this);
+ }
+
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
public IEnumerable<ITagSpan<DafnyTokenTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
@@ -148,20 +163,24 @@ namespace DafnyLanguage private static List<TokenRegion> Rescan(ITextSnapshot newSnapshot) {
List<TokenRegion> newRegions = new List<TokenRegion>();
- bool stillScanningLongComment = false;
- SnapshotPoint commentStart = new SnapshotPoint(); // used only when stillScanningLongComment
- SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint(); // used only when stillScanningLongComment
+ int longCommentDepth = 0;
+ SnapshotPoint commentStart = new SnapshotPoint(); // used only when longCommentDepth != 0
+ SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint(); // used only when longCommentDepth != 0
foreach (ITextSnapshotLine line in newSnapshot.Lines) {
string txt = line.GetText(); // the current line (without linebreak characters)
int N = txt.Length; // length of the current line
int cur = 0; // offset into the current line
- if (stillScanningLongComment) {
- if (ScanForEndOfComment(txt, ref cur)) {
+ if (longCommentDepth != 0) {
+ ScanForEndOfComment(txt, ref longCommentDepth, ref cur);
+ if (longCommentDepth == 0) {
+ // we just finished parsing a long comment
newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKind.Comment));
- stillScanningLongComment = false;
} else {
+ // we're still parsing the long comment
+ Contract.Assert(cur == txt.Length);
commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + cur);
+ goto OUTER_CONTINUE;
}
}
@@ -179,9 +198,9 @@ namespace DafnyLanguage if ('a' <= ch && ch <= 'z') break;
if ('A' <= ch && ch <= 'Z') break;
if ('0' <= ch && ch <= '9') { ty = DafnyTokenKind.Number; break; }
+ if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break; // parts of identifiers
if (ch == '"') { ty = DafnyTokenKind.String; break; }
if (ch == '/') { ty = DafnyTokenKind.Comment; break; }
- if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break; // parts of identifiers
}
// advance to the end of the token
@@ -211,7 +230,7 @@ namespace DafnyLanguage }
}
} else if (ty == DafnyTokenKind.Comment) {
- if (end == N) continue; // this was not the start of a comment
+ if (end == N) continue; // this was not the start of a comment; it was just a single "/" and we don't care to color it
char ch = txt[end];
if (ch == '/') {
// a short comment
@@ -220,15 +239,18 @@ namespace DafnyLanguage // a long comment; find the matching "*/"
end++;
commentStart = new SnapshotPoint(newSnapshot, line.Start + cur);
- if (ScanForEndOfComment(txt, ref end)) {
+ Contract.Assert(longCommentDepth == 0);
+ longCommentDepth = 1;
+ ScanForEndOfComment(txt, ref longCommentDepth, ref end);
+ if (longCommentDepth == 0) {
+ // we finished scanning a long comment, and "end" is set to right after it
newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKind.Comment));
} else {
- stillScanningLongComment = true;
commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + end);
}
continue;
} else {
- // not a comment
+ // not a comment; it was just a single "/" and we don't care to color it
continue;
}
} else {
@@ -322,7 +344,7 @@ namespace DafnyLanguage #endregion
break;
default:
- continue; // it was an identifier
+ continue; // it was an identifier, so we don't color it
}
}
}
@@ -332,26 +354,40 @@ namespace DafnyLanguage OUTER_CONTINUE: ;
}
- if (stillScanningLongComment) {
+ if (longCommentDepth != 0) {
+ // This was a malformed comment, running to the end of the buffer. Above, we let "commentEndAsWeKnowIt" be the end of the
+ // last line, so we can use it here.
newRegions.Add(new TokenRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKind.Comment));
}
return newRegions;
}
- private static bool ScanForEndOfComment(string txt, ref int end) {
- int N = txt.Length;
- for (; end < N; end++) {
+ /// <summary>
+ /// Scans "txt" beginning with depth "depth", which is assumed to be non-0. Any occurrences of "/*" or "*/"
+ /// increment or decrement "depth". If "depth" ever reaches 0, then "end" returns as the number of characters
+ /// consumed from "txt" (including the last "*/"). If "depth" is still non-0 when the entire "txt" has
+ /// been consumed, then "end" returns as the length of "txt". (Note, "end" may return as the length of "txt"
+ /// if "depth" is still non-0 or if "depth" became 0 from reading the last characters of "txt".)
+ /// </summary>
+ private static void ScanForEndOfComment(string txt, ref int depth, ref int end) {
+ Contract.Requires(depth > 0);
+
+ int Nminus1 = txt.Length - 1; // no reason ever to look at the last character of the line, unless the second-to-last character is '*' or '/'
+ for (; end < Nminus1; ) {
char ch = txt[end];
- if (ch == '*' && end + 1 < N) {
- ch = txt[end + 1];
- if (ch == '/') {
- end += 2;
- return true;
- }
+ if (ch == '*' && txt[end + 1] == '/') {
+ end += 2;
+ depth--;
+ if (depth == 0) { return; }
+ } else if (ch == '/' && txt[end + 1] == '*') {
+ end += 2;
+ depth++;
+ } else {
+ end++;
}
}
- return false; // hit end-of-line without finding end-of-comment
+ end = txt.Length; // we didn't look at the last character, but we still consumed all the output
}
}
|