summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar Jason Koenig <unknown>2011-07-15 18:08:08 -0700
committerGravatar Jason Koenig <unknown>2011-07-15 18:08:08 -0700
commitb32e450d37de5797eb143dce80866e863d498102 (patch)
tree877bded3befc7db1599061dcced086d464c73242 /Source/Dafny
parent1f850973d1c80f9474a9b07571c35d37a1a25368 (diff)
parentfb0960efe49ccb771ffee57e2cfaccdac6db4e04 (diff)
Merge
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Compiler.cs108
-rw-r--r--Source/Dafny/Dafny.atg149
-rw-r--r--Source/Dafny/DafnyAst.cs20
-rw-r--r--Source/Dafny/DafnyMain.cs14
-rw-r--r--Source/Dafny/DafnyPipeline.csproj6
-rw-r--r--Source/Dafny/Printer.cs118
-rw-r--r--Source/Dafny/Resolver.cs256
-rw-r--r--Source/Dafny/SccGraph.cs54
-rw-r--r--Source/Dafny/Translator.cs400
9 files changed, 501 insertions, 624 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 6fa9440a..6a448172 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -19,13 +19,13 @@ namespace Microsoft.Dafny {
}
[ContractInvariantMethod]
- void ObjectInvariant()
+ void ObjectInvariant()
{
Contract.Invariant(wr!=null);
}
TextWriter wr;
-
+
public int ErrorCount;
void Error(string msg, params object[] args) {Contract.Requires(msg != null);
string s = string.Format("Compilation error: " + msg, args);
@@ -33,7 +33,7 @@ namespace Microsoft.Dafny {
wr.WriteLine("/* {0} */", s);
ErrorCount++;
}
-
+
void ReadRuntimeSystem() {
string codebase = cce.NonNull( System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
string path = System.IO.Path.Combine(codebase, "DafnyRuntime.cs");
@@ -226,7 +226,7 @@ namespace Microsoft.Dafny {
Indent(indent); wr.WriteLine("}");
}
}
-
+
void CompileDatatypeStruct(DatatypeDecl dt, int indent) {
Contract.Requires(dt != null);
@@ -254,23 +254,23 @@ namespace Microsoft.Dafny {
if (dt.TypeArgs.Count != 0) {
DtT += "<" + TypeParameters(dt.TypeArgs) + ">";
}
-
+
Indent(indent);
wr.WriteLine("public struct @{0} {{", DtT);
int ind = indent + IndentAmount;
-
+
Indent(ind);
wr.WriteLine("Base_{0} d;", DtT);
-
+
Indent(ind);
wr.WriteLine("public Base_{0} _D {{", DtT);
Indent(ind + IndentAmount);
wr.WriteLine("get { if (d == null) { d = Default; } return d; }");
Indent(ind); wr.WriteLine("}");
-
+
Indent(ind);
wr.WriteLine("public @{0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT);
-
+
Indent(ind);
wr.WriteLine("public static Base_{0} Default {{", DtT);
Indent(ind + IndentAmount);
@@ -320,7 +320,7 @@ namespace Microsoft.Dafny {
Indent(indent);
wr.WriteLine("}");
}
-
+
int WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals)
{
Contract.Requires(sep != null);
@@ -336,20 +336,20 @@ namespace Microsoft.Dafny {
}
return i; // the number of formals written
}
-
+
string FormalName(Formal formal, int i) {
Contract.Requires(formal != null);
Contract.Ensures(Contract.Result<string>() != null);
return formal.HasName ? formal.Name : "_a" + i;
}
-
+
string DtCtorName(DatatypeCtor ctor) {
Contract.Requires(ctor != null);Contract.Ensures(Contract.Result<string>() != null);
return cce.NonNull(ctor.EnclosingDatatype).Name + "_" + ctor.Name;
}
-
+
void CompileClassMembers(ClassDecl c, int indent)
{
Contract.Requires(c != null);
@@ -360,7 +360,7 @@ namespace Microsoft.Dafny {
Indent(indent);
wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type));
}
-
+
} else if (member is Function) {
Function f = (Function)member;
if (f.IsGhost) {
@@ -379,7 +379,7 @@ namespace Microsoft.Dafny {
CompileReturnBody(f.Body, indent);
Indent(indent); wr.WriteLine("}");
}
-
+
} else if (member is Method) {
Method m = (Method)member;
if (!m.IsGhost) {
@@ -487,7 +487,7 @@ namespace Microsoft.Dafny {
readonly string DafnySetClass = "Dafny.Set";
readonly string DafnyMultiSetClass = "Dafny.MultiSet";
readonly string DafnySeqClass = "Dafny.Sequence";
-
+
string TypeName(Type type)
{
Contract.Requires(type != null);
@@ -504,7 +504,7 @@ namespace Microsoft.Dafny {
type = tp.T;
}
}
-
+
if (type is BoolType) {
return "bool";
} else if (type is IntType) {
@@ -565,7 +565,7 @@ namespace Microsoft.Dafny {
}
return s;
}
-
+
string/*!*/ TypeParameters(List<TypeParameter/*!*/>/*!*/ targs) {
Contract.Requires(cce.NonNullElements(targs));
Contract.Ensures(Contract.Result<string>() != null);
@@ -578,7 +578,7 @@ namespace Microsoft.Dafny {
}
return s;
}
-
+
string DefaultValue(Type type)
{
Contract.Requires(type != null);
@@ -595,7 +595,7 @@ namespace Microsoft.Dafny {
type = tp.T;
}
}
-
+
if (type is BoolType) {
return "false";
} else if (type is IntType) {
@@ -622,16 +622,16 @@ namespace Microsoft.Dafny {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
-
+
// ----- Stmt ---------------------------------------------------------------------------------
-
+
void TrStmt(Statement stmt, int indent)
{
Contract.Requires(stmt != null);
if (stmt.IsGhost) {
return;
}
-
+
if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
foreach (Attributes.Argument arg in s.Args) {
@@ -732,19 +732,19 @@ namespace Microsoft.Dafny {
} else {
TrRhs(null, s.Lhs, s.Rhs, indent);
}
-
+
} else if (stmt is VarDecl) {
TrVarDecl((VarDecl)stmt, true, indent);
-
+
} else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
TrCallStmt(s, null, indent);
-
+
} else if (stmt is BlockStmt) {
Indent(indent); wr.WriteLine("{");
TrStmtList(((BlockStmt)stmt).Body, indent);
Indent(indent); wr.WriteLine("}");
-
+
} else if (stmt is IfStmt) {
IfStmt s = (IfStmt)stmt;
Indent(indent);
@@ -755,7 +755,7 @@ namespace Microsoft.Dafny {
TrExpr(s.Guard);
wr.WriteLine(")");
}
-
+
TrStmt(s.Thn, indent);
if (s.Els != null && s.Guard != null) {
Indent(indent); wr.WriteLine("else");
@@ -825,20 +825,20 @@ namespace Microsoft.Dafny {
tmpVarCount++;
string TType = TypeName(s.BoundVar.Type);
string RhsType = TypeName(cce.NonNull(s.BodyAssign.Lhs.Type));
-
+
Indent(indent);
wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);
-
+
Indent(indent);
wr.Write("foreach ({0} @{1} in (", TType, s.BoundVar.Name);
TrExpr(s.Collection);
wr.WriteLine(").Elements) {");
-
+
Indent(indent + IndentAmount);
wr.Write("if (");
TrExpr(s.Range);
wr.WriteLine(") {");
-
+
foreach (PredicateStmt p in s.BodyPrefix) {
TrStmt(p, indent + 2*IndentAmount);
}
@@ -851,7 +851,7 @@ namespace Microsoft.Dafny {
wr.Write(DefaultValue(s.BodyAssign.Lhs.Type));
}
wr.WriteLine("))");
-
+
Indent(indent + IndentAmount); wr.WriteLine("}");
Indent(indent); wr.WriteLine("}");
@@ -860,7 +860,7 @@ namespace Microsoft.Dafny {
FieldSelectExpr fse = (FieldSelectExpr)s.BodyAssign.Lhs;
wr.WriteLine("{0}.Car.{1} = {0}.Cdr;", pr, fse.FieldName);
Indent(indent); wr.WriteLine("}");
-
+
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
// Type source = e;
@@ -1044,16 +1044,16 @@ namespace Microsoft.Dafny {
}
Contract.Assert(j == outTmps.Count);
}
-
+
int tmpVarCount = 0;
-
+
void TrAssignmentRhs(AssignmentRhs rhs) {
Contract.Requires(rhs != null);
Contract.Requires(!(rhs is HavocRhs));
if (rhs is ExprRhs) {
ExprRhs e = (ExprRhs)rhs;
TrExpr(e.Expr);
-
+
} else {
TypeRhs tp = (TypeRhs)rhs;
if (tp.ArrayDimensions == null) {
@@ -1083,7 +1083,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent) {Contract.Requires(cce.NonNullElements(stmts));
foreach (Statement ss in stmts) {
TrStmt(ss, indent + IndentAmount);
@@ -1140,7 +1140,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
// ----- Expression ---------------------------------------------------------------------------
void TrParenExpr(string prefix, Expression expr) {
@@ -1156,7 +1156,7 @@ namespace Microsoft.Dafny {
TrExpr(expr);
wr.Write(")");
}
-
+
void TrExprList(List<Expression/*!*/>/*!*/ exprs) {
Contract.Requires(cce.NonNullElements(exprs));
wr.Write("(");
@@ -1188,10 +1188,10 @@ namespace Microsoft.Dafny {
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal
}
-
+
} else if (expr is ThisExpr) {
wr.Write("this");
-
+
} else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
wr.Write("@" + e.Var.Name);
@@ -1213,7 +1213,7 @@ namespace Microsoft.Dafny {
Type elType = cce.NonNull((SeqType)e.Type).Arg;
wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));
TrExprList(e.Elements);
-
+
} else if (expr is FieldSelectExpr) {
FieldSelectExpr e = (FieldSelectExpr)expr;
SpecialField sf = e.Field as SpecialField;
@@ -1226,7 +1226,7 @@ namespace Microsoft.Dafny {
TrParenExpr(e.Obj);
wr.Write(".@{0}", e.Field.Name);
}
-
+
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
Contract.Assert(e.Seq.Type != null);
@@ -1288,7 +1288,7 @@ namespace Microsoft.Dafny {
wr.Write(", ");
TrExpr(e.Value);
wr.Write(")");
-
+
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
Function f = cce.NonNull(e.Function);
@@ -1308,7 +1308,7 @@ namespace Microsoft.Dafny {
}
}
wr.Write(")");
-
+
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved
@@ -1327,13 +1327,13 @@ namespace Microsoft.Dafny {
}
}
wr.Write("))");
-
+
} else if (expr is OldExpr) {
Contract.Assert(false); throw new cce.UnreachableException(); // 'old' is always a ghost (right?)
-
+
} else if (expr is FreshExpr) {
Contract.Assert(false); throw new cce.UnreachableException(); // 'fresh' is always a ghost
-
+
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
switch (e.Op) {
@@ -1358,13 +1358,13 @@ namespace Microsoft.Dafny {
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression
}
-
+
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
string opString = null;
string preOpString = "";
string callString = null;
-
+
switch (e.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.Iff:
opString = "=="; break;
@@ -1374,7 +1374,7 @@ namespace Microsoft.Dafny {
opString = "||"; break;
case BinaryExpr.ResolvedOpcode.And:
opString = "&&"; break;
-
+
case BinaryExpr.ResolvedOpcode.EqCommon: {
Type t = cce.NonNull(e.E0.Type);
if (t.IsDatatype || t.IsTypeParameter) {
@@ -1394,7 +1394,7 @@ namespace Microsoft.Dafny {
}
break;
}
-
+
case BinaryExpr.ResolvedOpcode.Lt:
opString = "<"; break;
case BinaryExpr.ResolvedOpcode.Le:
@@ -1506,7 +1506,7 @@ namespace Microsoft.Dafny {
TrExpr(e.E1);
wr.Write(")");
}
-
+
} else if (expr is QuantifierExpr) {
var e = (QuantifierExpr)expr;
Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 665cf33f..028d6826 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -3,39 +3,29 @@
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------*/
-
/*---------------------------------------------------------------------------
// Dafny
// Rustan Leino, first created 25 January 2008
//--------------------------------------------------------------------------*/
-
using System.Collections.Generic;
using System.Numerics;
using Microsoft.Boogie;
using System.IO;
using System.Text;
-
-
COMPILER Dafny
-
/*--------------------------------------------------------------------------*/
-
static List<ModuleDecl/*!*/> theModules;
static BuiltIns theBuiltIns;
-
-
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static int anonymousIds = 0;
-
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
public bool IsUnlimited;
}
-
// helper routine for parsing call statements
private static Expression/*!*/ ConvertToLocal(Expression/*!*/ e)
{
@@ -47,7 +37,6 @@ Contract.Ensures(Contract.Result<Expression>() != null);
}
return e; // cannot convert to IdentifierExpr (or is already an IdentifierExpr)
}
-
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "modules".
@@ -68,7 +57,6 @@ public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ module
}
}
}
-
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "modules".
@@ -82,7 +70,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Errors errors = new Errors();
return Parse(s, filename, modules, builtIns, errors);
}
-
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "modules".
@@ -108,7 +95,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
theBuiltIns = oldBuiltIns;
return parser.errors.count;
}
-
/*--------------------------------------------------------------------------*/
CHARACTERS
letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
@@ -116,25 +102,20 @@ CHARACTERS
posDigit = "123456789".
special = "'_?\\".
glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
-
cr = '\r'.
lf = '\n'.
tab = '\t'.
-
space = ' '.
quote = '"'.
-
nondigit = letter + special.
idchar = nondigit + digit.
nonquote = letter + digit + space + glyph.
-
/* exclude the characters in 'array' */
nondigitMinusA = nondigit - 'a'.
idcharMinusA = idchar - 'a'.
idcharMinusR = idchar - 'r'.
idcharMinusY = idchar - 'y'.
idcharMinusPosDigit = idchar - posDigit.
-
/*------------------------------------------------------------------------*/
TOKENS
ident = nondigitMinusA {idchar} /* if char 0 is not an 'a', then anything else is fine */
@@ -147,23 +128,16 @@ TOKENS
digits = digit {digit}.
arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].
string = quote {nonquote} quote.
-
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
-
IGNORE cr + lf + tab
-
-
/*------------------------------------------------------------------------*/
PRODUCTIONS
-
Dafny
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
-
List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
ModuleDecl module;
-
// to support multiple files, create a default module only if theModules doesn't already contain one
DefaultModuleDecl defaultModule = null;
foreach (ModuleDecl mdecl in theModules) {
@@ -206,7 +180,6 @@ Dafny
.)
EOF
.
-
ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
@@ -227,16 +200,15 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
"{" (. bodyStart = t; .)
{ ClassMemberDecl<members, true>
}
- "}"
- (. if (optionalId == null)
+ "}"
+ (. if (optionalId == null)
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
- else
+ else
c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
.)
.
-
ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
= (. Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
@@ -247,13 +219,12 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
| "static" (. mmod.IsStatic = true; .)
| "unlimited" (. mmod.IsUnlimited = true; .)
}
- ( FieldDecl<mmod, mm>
+ ( FieldDecl<mmod, mm>
| FunctionDecl<mmod, out f> (. mm.Add(f); .)
| MethodDecl<mmod, allowConstructors, out m> (. mm.Add(m); .)
- | CouplingInvDecl<mmod, mm>
+ | CouplingInvDecl<mmod, mm>
)
.
-
DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
@@ -276,7 +247,6 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
dt.BodyEndTok = t;
.)
.
-
DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
= (. Contract.Requires(cce.NonNullElements(ctors));
Attributes attrs = null;
@@ -288,7 +258,6 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
[ FormalsOptionalIds<formals> ]
(. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)
.
-
FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
@@ -304,7 +273,6 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
}
";"
.
-
CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
@@ -317,17 +285,15 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }
if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }
.)
- { Attribute<ref attrs> }
+ { Attribute<ref attrs> }
Ident<out id> (. ids.Add(id); .)
{ "," Ident<out id> (. ids.Add(id); .)
}
- "by"
+ "by"
Expression<out e>
";"
- (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)
+ (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)
.
-
-
GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>
/* isGhost always returns as false if allowGhostKeyword is false */
= (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
@@ -337,14 +303,12 @@ GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out boo
]
IdentType<out id, out ty>
.
-
IdentType<out IToken/*!*/ id, out Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
Ident<out id>
":"
Type<out ty>
.
-
LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
= (. IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
@@ -353,7 +317,6 @@ LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
]
(. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
.
-
IdentTypeOptional<out BoundVar/*!*/ var>
= (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
@@ -362,7 +325,6 @@ IdentTypeOptional<out BoundVar/*!*/ var>
]
(. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
.
-
TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost>
= (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
@@ -389,9 +351,7 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t
}
.)
.
-
/*------------------------------------------------------------------------*/
-
GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
= (. Contract.Requires(cce.NonNullElements(typeArgs));
IToken/*!*/ id; .)
@@ -401,9 +361,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
}
">"
.
-
/*------------------------------------------------------------------------*/
-
MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
IToken/*!*/ id;
@@ -447,11 +405,9 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
[ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
Formals<false, !mmod.IsGhost, outs>
]
-
{ MethodSpec<req, mod, ens, dec> }
[ BlockStmt<out bb, out bodyStart, out bodyEnd> (. body = (BlockStmt)bb; .)
]
-
(. if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
else if (isConstructor)
@@ -462,7 +418,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
m.BodyEndTok = bodyEnd;
.)
.
-
MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
List<Expression/*!*/>/*!*/ decreases.>
= (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
@@ -480,8 +435,7 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
| "decreases" DecreasesList<decreases, false> ";"
)
.
-
-Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
+Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; .)
"("
[
@@ -491,8 +445,7 @@ Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
]
")"
.
-
-FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
+FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; .)
"("
[
@@ -502,14 +455,11 @@ FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
]
")"
.
-
/*------------------------------------------------------------------------*/
-
Type<out Type/*!*/ ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; .)
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;
@@ -529,7 +479,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
}
ty = new MultiSetType(gt[0]);
.)
-
| "seq" (. tok = t; gt = new List<Type/*!*/>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("seq type expects exactly one type argument");
@@ -539,7 +488,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
| ReferenceType<out tok, out 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*/
@@ -560,7 +508,6 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
[ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
)
.
-
GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
= (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .)
"<"
@@ -569,9 +516,7 @@ GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
}
">"
.
-
/*------------------------------------------------------------------------*/
-
FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
= (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
Attributes attrs = null;
@@ -594,7 +539,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
(. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute<ref attrs> }
- Ident<out id>
+ Ident<out id>
[ GenericParameters<typeArgs> ]
Formals<true, isFunctionMethod, formals>
":"
@@ -607,7 +552,6 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
f.BodyEndTok = bodyEnd;
.)
.
-
FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>
= (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; .)
@@ -620,7 +564,6 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r
| "decreases" DecreasesList<decreases, false> ";"
)
.
-
PossiblyWildExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr; .)
@@ -631,7 +574,6 @@ PossiblyWildExpression<out Expression/*!*/ e>
| Expression<out e>
)
.
-
PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; .)
/* A reads clause can list a wildcard, which allows the enclosing function to
@@ -644,7 +586,6 @@ PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
| FrameExpression<out fe>
)
.
-
FrameExpression<out FrameExpression/*!*/ fe>
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; .)
Expression<out e>
@@ -652,16 +593,13 @@ FrameExpression<out FrameExpression/*!*/ fe>
]
(. fe = new FrameExpression(e, fieldName); .)
.
-
FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
"{" (. bodyStart = t; .)
Expression<out e>
"}" (. bodyEnd = t; .)
.
-
/*------------------------------------------------------------------------*/
-
BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);
List<Statement/*!*/> body = new List<Statement/*!*/>();
@@ -672,13 +610,11 @@ BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
"}" (. bodyEnd = t;
block = new BlockStmt(bodyStart, body); .)
.
-
Stmt<.List<Statement/*!*/>/*!*/ ss.>
= (. Statement/*!*/ s;
.)
OneStmt<out s> (. ss.Add(s); .)
.
-
OneStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
@@ -708,7 +644,6 @@ OneStmt<out Statement/*!*/ s>
| ReturnStmt<out s>
)
.
-
ReturnStmt<out Statement/*!*/ s>
= (.
IToken returnTok = null;
@@ -744,7 +679,6 @@ UpdateStmt<out Statement/*!*/ s>
)
(. s = new UpdateStmt(x, lhss, rhss); .)
.
-
Rhs<out AssignmentRhs r, Expression receiverForInitCall>
= (. IToken/*!*/ x, newToken; Expression/*!*/ e;
List<Expression> ee = null;
@@ -772,17 +706,13 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
r = new TypeRhs(newToken, ty, initCall);
}
.)
-
/* One day, the choose expression should be treated just as a special case of a method call. */
| "choose" (. x = t; .)
Expression<out e> (. r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); .)
-
| "*" (. r = new HavocRhs(t); .)
-
| Expression<out e> (. r = new ExprRhs(e); .)
)
.
-
VarDeclStatement<.out Statement/*!*/ s.>
= (. IToken x = null, assignTok = null; bool isGhost = false;
VarDecl/*!*/ d;
@@ -816,7 +746,6 @@ VarDeclStatement<.out Statement/*!*/ s.>
s = new VarDeclStmt(x, lhss, update);
.)
.
-
IfStmt<out Statement/*!*/ ifStmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
Expression guard;
@@ -842,7 +771,6 @@ IfStmt<out Statement/*!*/ ifStmt>
(. ifStmt = new AlternativeStmt(x, alternatives); .)
)
.
-
AlternativeBlock<.out List<GuardedAlternative> alternatives.>
= (. alternatives = new List<GuardedAlternative>();
IToken x;
@@ -859,7 +787,6 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.>
}
"}"
.
-
WhileStmt<out Statement/*!*/ stmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
Expression guard;
@@ -883,7 +810,6 @@ WhileStmt<out Statement/*!*/ stmt>
(. stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); .)
)
.
-
LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
@@ -904,7 +830,6 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
] ";"
}
.
-
DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
= (. Expression/*!*/ e; .)
PossiblyWildExpression<out e> (. if (!allowWildcard && e is WildcardExpr) {
@@ -921,7 +846,6 @@ DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
.)
}
.
-
Guard<out Expression e> /* null represents demonic-choice */
= (. Expression/*!*/ ee; e = null; .)
"("
@@ -930,7 +854,6 @@ Guard<out Expression e> /* null represents demonic-choice */
)
")"
.
-
MatchStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
@@ -943,7 +866,6 @@ MatchStmt<out Statement/*!*/ s>
"}"
(. s = new MatchStmt(x, e, cases); .)
.
-
CaseStatement<out MatchCaseStmt/*!*/ c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ x, id, arg;
@@ -961,9 +883,7 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
{ Stmt<body> }
(. c = new MatchCaseStmt(x, id.val, arguments, body); .)
.
-
/*------------------------------------------------------------------------*/
-
ForeachStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
IToken/*!*/ x, boundVar;
@@ -994,19 +914,16 @@ ForeachStmt<out Statement/*!*/ s>
}
.)
.
-
AssertStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"assert" (. x = t; .)
Expression<out e> ";" (. s = new AssertStmt(x, e); .)
.
-
AssumeStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"assume" (. x = t; .)
Expression<out e> ";" (. s = new AssumeStmt(x, e); .)
.
-
PrintStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
@@ -1017,13 +934,11 @@ PrintStmt<out Statement/*!*/ s>
}
";" (. s = new PrintStmt(x, args); .)
.
-
/*------------------------------------------------------------------------*/
Expression<out Expression/*!*/ e>
=
EquivExpression<out e>
.
-
/*------------------------------------------------------------------------*/
EquivExpression<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
@@ -1032,9 +947,7 @@ EquivExpression<out Expression/*!*/ e0>
ImpliesExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)
}
.
-
EquivOp = "<==>" | '\u21d4'.
-
/*------------------------------------------------------------------------*/
ImpliesExpression<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
@@ -1043,9 +956,7 @@ ImpliesExpression<out Expression/*!*/ e0>
ImpliesExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
]
.
-
ImpliesOp = "==>" | '\u21d2'.
-
/*------------------------------------------------------------------------*/
LogicalExpression<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
@@ -1062,10 +973,8 @@ LogicalExpression<out Expression/*!*/ e0>
}
]
.
-
AndOp = "&&" | '\u2227'.
OrOp = "||" | '\u2228'.
-
/*------------------------------------------------------------------------*/
RelationalExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
@@ -1149,7 +1058,6 @@ RelationalExpression<out Expression/*!*/ e>
}
.)
.
-
RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .)
@@ -1166,7 +1074,6 @@ RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
| '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .)
)
.
-
/*------------------------------------------------------------------------*/
Term<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; .)
@@ -1175,14 +1082,12 @@ Term<out Expression/*!*/ e0>
Factor<out e1> (. e0 = new BinaryExpr(x, op, e0, e1); .)
}
.
-
AddOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/; .)
( "+" (. x = t; op = BinaryExpr.Opcode.Add; .)
| "-" (. x = t; op = BinaryExpr.Opcode.Sub; .)
)
.
-
/*------------------------------------------------------------------------*/
Factor<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; .)
@@ -1191,7 +1096,6 @@ Factor<out Expression/*!*/ e0>
UnaryExpression<out e1> (. e0 = new BinaryExpr(x, op, e0, e1); .)
}
.
-
MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
( "*" (. x = t; op = BinaryExpr.Opcode.Mul; .)
@@ -1199,7 +1103,6 @@ MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
| "%" (. x = t; op = BinaryExpr.Opcode.Mod; .)
)
.
-
/*------------------------------------------------------------------------*/
UnaryExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; .)
@@ -1216,7 +1119,6 @@ UnaryExpression<out Expression/*!*/ e>
{ Suffix<ref e> }
)
.
-
Lhs<out Expression e>
= (. e = null; // to please the compiler
.)
@@ -1227,9 +1129,7 @@ Lhs<out Expression e>
{ Suffix<ref e> }
)
.
-
NegOp = "!" | '\u00ac'.
-
/* A ConstAtomExpression is never an l-value. Also, a ConstAtomExpression is never followed by
* an open paren (but could very well have a suffix that starts with a period or a square bracket).
* (The "Also..." part may change if expressions in Dafny could yield functions.)
@@ -1258,7 +1158,6 @@ ConstAtomExpression<out Expression/*!*/ e>
")"
)
.
-
DisplayExpr<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
@@ -1287,7 +1186,6 @@ MultiSetExpr<out Expression e>
| (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)
)
.
-
EndlessExpression<out Expression e>
= (. IToken/*!*/ x;
Expression e0, e1;
@@ -1302,7 +1200,6 @@ EndlessExpression<out Expression e>
| ComprehensionExpr<out e>
)
.
-
MatchExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
@@ -1316,7 +1213,6 @@ MatchExpression<out Expression/*!*/ e>
}
(. e = new MatchExpr(x, e, cases); .)
.
-
CaseExpression<out MatchCaseExpr/*!*/ c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
@@ -1332,9 +1228,7 @@ CaseExpression<out MatchCaseExpr/*!*/ c>
"=>"
Expression<out body> (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
.
-
/*------------------------------------------------------------------------*/
-
DottedIdentifiersAndFunction<out Expression e>
= (. IToken id; IToken openParen = null;
List<Expression> args = null;
@@ -1350,7 +1244,6 @@ DottedIdentifiersAndFunction<out Expression e>
]
(. e = new IdentifierSequence(idents, openParen, args); .)
.
-
Suffix<ref Expression/*!*/ e>
= (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x; List<Expression/*!*/>/*!*/ args;
Expression e0 = null; Expression e1 = null; Expression/*!*/ ee; bool anyDots = false;
@@ -1363,7 +1256,6 @@ Suffix<ref Expression/*!*/ e>
[ Expressions<args> ]
")" (. e = new FunctionCallExpr(id, id.val, e, args); .)
] (. if (!func) { e = new FieldSelectExpr(id, e, id.val); } .)
-
| "[" (. x = t; .)
( Expression<out ee> (. e0 = ee; .)
( ".." (. anyDots = true; .)
@@ -1408,9 +1300,7 @@ Suffix<ref Expression/*!*/ e>
"]"
)
.
-
/*------------------------------------------------------------------------*/
-
QuantifierGuts<out Expression/*!*/ q>
= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;
bool univ = false;
@@ -1441,11 +1331,9 @@ QuantifierGuts<out Expression/*!*/ q>
}
.)
.
-
Forall = "forall" | '\u2200'.
Exists = "exists" | '\u2203'.
QSep = "::" | '\u2022'.
-
ComprehensionExpr<out Expression/*!*/ q>
= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
IToken/*!*/ x = Token.NoToken;
@@ -1468,22 +1356,18 @@ ComprehensionExpr<out Expression/*!*/ q>
q = new SetComprehension(x, bvars, range, body);
.)
.
-
Expressions<.List<Expression/*!*/>/*!*/ args.>
= (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)
Expression<out e> (. args.Add(e); .)
{ "," Expression<out e> (. args.Add(e); .)
}
.
-
/*------------------------------------------------------------------------*/
-
Attribute<ref Attributes attrs>
= "{"
AttributeBody<ref attrs>
"}"
.
-
AttributeBody<ref Attributes attrs>
= (. string aName;
List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
@@ -1495,14 +1379,12 @@ AttributeBody<ref Attributes attrs>
}
] (. attrs = new Attributes(aName, aArgs, attrs); .)
.
-
AttributeArg<out Attributes.Argument/*!*/ arg>
= (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg; .)
( string (. arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); .)
| Expression<out e> (. arg = new Attributes.Argument(e); .)
)
.
-
AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
= (. List<Expression/*!*/> es = new List<Expression/*!*/>();
.)
@@ -1513,21 +1395,17 @@ AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
)
"}"
.
-
/*------------------------------------------------------------------------*/
-
Idents<.List<string/*!*/>/*!*/ ids.>
= (. IToken/*!*/ id; .)
Ident<out id> (. ids.Add(id.val); .)
{ "," Ident<out id> (. ids.Add(id.val); .)
}
.
-
Ident<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
ident (. x = t; .)
.
-
Nat<out BigInteger n>
=
digits
@@ -1537,7 +1415,6 @@ Nat<out BigInteger n>
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
}
- .)
+ .)
.
-
-END Dafny. \ No newline at end of file
+END Dafny.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 871a8b34..218f95e5 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -413,13 +413,13 @@ namespace Microsoft.Dafny {
/// <summary>
/// This proxy stands for any type.
- /// </summary>
+ /// </summary>
public class InferredTypeProxy : UnrestrictedTypeProxy {
}
/// <summary>
/// This proxy stands for any type, but it originates from an instantiated type parameter.
- /// </summary>
+ /// </summary>
public class ParamTypeProxy : UnrestrictedTypeProxy {
TypeParameter orig;
[ContractInvariantMethod]
@@ -445,7 +445,7 @@ namespace Microsoft.Dafny {
/// <summary>
/// This proxy stands for any datatype.
- /// </summary>
+ /// </summary>
public class DatatypeProxy : RestrictedTypeProxy {
public override int OrderID {
get {
@@ -456,7 +456,7 @@ namespace Microsoft.Dafny {
/// <summary>
/// This proxy stands for object or any class/array type.
- /// </summary>
+ /// </summary>
public class ObjectTypeProxy : RestrictedTypeProxy {
public override int OrderID {
get {
@@ -504,7 +504,7 @@ namespace Microsoft.Dafny {
/// if AllowSeq, or:
/// int or set or multiset
/// if !AllowSeq.
- /// </summary>
+ /// </summary>
public class OperationTypeProxy : RestrictedTypeProxy {
public readonly bool AllowSeq;
public OperationTypeProxy(bool allowSeq) {
@@ -688,7 +688,7 @@ namespace Microsoft.Dafny {
public class ClassRefinementDecl : ClassDecl {
public readonly IToken/*!*/ RefinedClass;
- public ClassDecl Refined; // filled in during resolution
+ public ClassDecl Refined; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(RefinedClass != null);
@@ -733,7 +733,7 @@ namespace Microsoft.Dafny {
Dims = dims;
}
}
-
+
public class DatatypeDecl : TopLevelDecl {
public readonly List<DatatypeCtor/*!*/>/*!*/ Ctors;
[ContractInvariantMethod]
@@ -1698,7 +1698,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(Mod == null || cce.NonNullElements(Mod));
}
public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)
- : base(tok)
+ : base(tok)
{
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(invariants));
@@ -2564,7 +2564,7 @@ namespace Microsoft.Dafny {
public List<BoundedPool> Bounds; // initialized and filled in by resolver
// invariant Bounds == null || Bounds.Count == BoundVars.Count;
- public List<BoundVar> MissingBounds; // filled in during resolution; remains "null" if bounds can be found
+ public List<BoundVar> MissingBounds; // filled in during resolution; remains "null" if bounds can be found
// invariant Bounds == null || MissingBounds == null;
public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression/*!*/ term, Attributes attrs)
@@ -2582,7 +2582,7 @@ namespace Microsoft.Dafny {
public override IEnumerable<Expression> SubExpressions {
get {
if (Range != null) { yield return Range; }
- yield return Term;
+ yield return Term;
}
}
}
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index a18ea938..3f0b6e97 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -27,21 +27,21 @@ namespace Microsoft.Dafny {
if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {
Bpl.CommandLineOptions.Clo.XmlSink.WriteFileFragment(dafnyFileName);
}
- if (Bpl.CommandLineOptions.Clo.Trace)
+ if (Bpl.CommandLineOptions.Clo.Trace)
{
Console.WriteLine("Parsing " + dafnyFileName);
}
int errorCount;
- try
+ try
{
errorCount = Dafny.Parser.Parse(dafnyFileName, modules, builtIns);
- if (errorCount != 0)
+ if (errorCount != 0)
{
return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName);
}
- }
- catch (IOException e)
+ }
+ catch (IOException e)
{
return string.Format("Error opening file \"{0}\": {1}", dafnyFileName, e.Message);
}
@@ -61,7 +61,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }
Dafny.Resolver r = new Dafny.Resolver(program);
@@ -73,4 +73,4 @@ namespace Microsoft.Dafny {
return null; // success
}
}
-} \ No newline at end of file
+}
diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 7f063c2c..6a15b1f7 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -147,11 +147,11 @@
</BootstrapperPackage>
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
- <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
Other similar extension points exist, see Microsoft.Common.targets.
<Target Name="BeforeBuild">
</Target>
<Target Name="AfterBuild">
</Target>
-->
-</Project> \ No newline at end of file
+</Project>
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 15a3f65d..63b5f926 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Dafny {
class Printer {
TextWriter wr;
[ContractInvariantMethod]
- void ObjectInvariant()
+ void ObjectInvariant()
{
Contract.Invariant(wr!=null);
}
@@ -23,7 +23,7 @@ namespace Microsoft.Dafny {
Contract.Requires(wr != null);
this.wr = wr;
}
-
+
public void PrintProgram(Program prog) {
Contract.Requires(prog != null);
if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) {
@@ -56,7 +56,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
public void PrintTopLevelDecls(List<TopLevelDecl> classes, int indent) {
Contract.Requires(classes!= null);
int i = 0;
@@ -79,7 +79,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
public void PrintClass(ClassDecl c, int indent) {
Contract.Requires(c != null);
Indent(indent);
@@ -97,12 +97,12 @@ namespace Microsoft.Dafny {
wr.WriteLine("}");
}
}
-
+
public void PrintClass_Members(ClassDecl c, int indent)
{
Contract.Requires(c != null);
Contract.Requires( c.Members.Count != 0);
-
+
int state = 0; // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field
foreach (MemberDecl m in c.Members) {
if (m is Method) {
@@ -126,7 +126,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
void PrintClassMethodHelper(string kind, Attributes attrs, string name, List<TypeParameter> typeArgs) {
Contract.Requires(kind != null);
Contract.Requires(name != null);
@@ -147,7 +147,7 @@ namespace Microsoft.Dafny {
wr.Write(">");
}
}
-
+
public void PrintDatatype(DatatypeDecl dt, int indent) {
Contract.Requires(dt != null);
Indent(indent);
@@ -164,17 +164,17 @@ namespace Microsoft.Dafny {
}
wr.WriteLine(";");
}
-
+
public void PrintAttributes(Attributes a) {
if (a != null) {
PrintAttributes(a.Prev);
-
+
wr.Write("{{:{0}", a.Name);
PrintAttributeArgs(a.Args);
wr.Write("} ");
}
}
-
+
public void PrintAttributeArgs(List<Attributes.Argument> args) {
Contract.Requires(args != null);
string prefix = " ";
@@ -190,7 +190,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
public void PrintField(Field field, int indent) {
Contract.Requires(field != null);
Indent(indent);
@@ -203,7 +203,7 @@ namespace Microsoft.Dafny {
PrintType(field.Type);
wr.WriteLine(";");
}
-
+
public void PrintCouplingInvariant(CouplingInvariant inv, int indent) {
Contract.Requires(inv != null);
Indent(indent);
@@ -218,7 +218,7 @@ namespace Microsoft.Dafny {
PrintExpression(inv.Expr);
wr.WriteLine(";");
}
-
+
public void PrintFunction(Function f, int indent) {
Contract.Requires(f != null);
Indent(indent);
@@ -245,20 +245,20 @@ namespace Microsoft.Dafny {
wr.WriteLine("}");
}
}
-
+
// ----------------------------- PrintMethod -----------------------------
const int IndentAmount = 2;
const string BunchaSpaces = " ";
void Indent(int amount)
{ Contract.Requires( 0 <= amount);
-
+
while (0 < amount) {
wr.Write(BunchaSpaces.Substring(0, amount));
amount -= BunchaSpaces.Length;
}
}
-
+
public void PrintMethod(Method method, int indent) {
Contract.Requires(method != null);
Indent(indent);
@@ -284,14 +284,14 @@ namespace Microsoft.Dafny {
PrintFrameSpecLine("modifies", method.Mod, ind);
PrintSpec("ensures", method.Ens, ind);
PrintSpecLine("decreases", method.Decreases, ind);
-
+
if (method.Body != null) {
Indent(indent);
PrintStatement(method.Body, indent);
wr.WriteLine();
}
}
-
+
void PrintFormals(List<Formal> ff) {
Contract.Requires(ff!=null);
wr.Write("(");
@@ -304,7 +304,7 @@ namespace Microsoft.Dafny {
}
wr.Write(")");
}
-
+
void PrintFormal(Formal f) {
Contract.Requires(f != null);
if (f.IsGhost) {
@@ -315,7 +315,7 @@ namespace Microsoft.Dafny {
}
PrintType(f.Type);
}
-
+
void PrintSpec(string kind, List<Expression> ee, int indent) {
Contract.Requires(kind != null);
Contract.Requires(ee != null);
@@ -363,7 +363,7 @@ namespace Microsoft.Dafny {
}
// ----------------------------- PrintType -----------------------------
-
+
public void PrintType(Type ty) {
Contract.Requires(ty != null);
wr.Write(ty.ToString());
@@ -379,7 +379,7 @@ namespace Microsoft.Dafny {
}
// ----------------------------- PrintStatement -----------------------------
-
+
/// <summary>
/// Prints from the current position of the current line.
/// If the statement requires several lines, subsequent lines are indented at "indent".
@@ -393,23 +393,23 @@ namespace Microsoft.Dafny {
Indent(indent);
}
}
-
+
if (stmt is AssertStmt) {
wr.Write("assert ");
PrintExpression(((AssertStmt)stmt).Expr);
wr.Write(";");
-
+
} else if (stmt is AssumeStmt) {
wr.Write("assume ");
PrintExpression(((AssumeStmt)stmt).Expr);
wr.Write(";");
-
+
} else if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
wr.Write("print");
PrintAttributeArgs(s.Args);
wr.Write(";");
-
+
} else if (stmt is BreakStmt) {
BreakStmt s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
@@ -422,7 +422,7 @@ namespace Microsoft.Dafny {
}
wr.Write(";");
}
-
+
} else if (stmt is ReturnStmt) {
var s = (ReturnStmt) stmt;
wr.Write("return");
@@ -435,14 +435,14 @@ namespace Microsoft.Dafny {
}
}
wr.Write(";");
-
+
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
PrintExpression(s.Lhs);
wr.Write(" := ");
PrintRhs(s.Rhs);
wr.Write(";");
-
+
} else if (stmt is VarDecl) {
VarDecl s = (VarDecl)stmt;
if (s.IsGhost) {
@@ -451,7 +451,7 @@ namespace Microsoft.Dafny {
wr.Write("var {0}", s.Name);
PrintType(": ", s.OptionalType);
wr.Write(";");
-
+
} else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
wr.Write("call ");
@@ -471,7 +471,7 @@ namespace Microsoft.Dafny {
wr.Write("{0}(", s.MethodName);
PrintExpressionList(s.Args);
wr.Write(");");
-
+
} else if (stmt is BlockStmt) {
wr.WriteLine("{");
int ind = indent + IndentAmount;
@@ -482,7 +482,7 @@ namespace Microsoft.Dafny {
}
Indent(indent);
wr.Write("}");
-
+
} else if (stmt is IfStmt) {
IfStmt s = (IfStmt)stmt;
while (true) {
@@ -508,7 +508,7 @@ namespace Microsoft.Dafny {
PrintAlternatives(indent, s.Alternatives);
Indent(indent);
wr.Write("}");
-
+
} else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
wr.Write("while (");
@@ -556,7 +556,7 @@ namespace Microsoft.Dafny {
wr.WriteLine();
Indent(indent);
wr.Write("}");
-
+
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
wr.Write("match ");
@@ -644,7 +644,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
void PrintRhs(AssignmentRhs rhs) {
Contract.Requires(rhs != null);
if (rhs is ExprRhs) {
@@ -673,7 +673,7 @@ namespace Microsoft.Dafny {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS
}
}
-
+
void PrintGuard(Expression guard) {
if (guard == null) {
wr.Write("*");
@@ -681,7 +681,7 @@ namespace Microsoft.Dafny {
PrintExpression(guard);
}
}
-
+
// ----------------------------- PrintExpression -----------------------------
public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {
@@ -739,12 +739,12 @@ namespace Microsoft.Dafny {
wr.WriteLine(endWithCloseParen ? ")" : "");
}
}
-
+
public void PrintExpression(Expression expr) {
Contract.Requires(expr != null);
PrintExpr(expr, 0, false, true, -1);
}
-
+
/// <summary>
/// An indent of -1 means print the entire expression on one line.
/// </summary>
@@ -752,7 +752,7 @@ namespace Microsoft.Dafny {
Contract.Requires(expr != null);
PrintExpr(expr, 0, false, true, indent);
}
-
+
/// <summary>
/// An indent of -1 means print the entire expression on one line.
/// </summary>
@@ -770,13 +770,13 @@ namespace Microsoft.Dafny {
} else {
wr.Write((BigInteger)e.Value);
}
-
+
} else if (expr is ThisExpr) {
wr.Write("this");
-
+
} else if (expr is IdentifierExpr) {
wr.Write(((IdentifierExpr)expr).Name);
-
+
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);
@@ -785,14 +785,14 @@ namespace Microsoft.Dafny {
PrintExpressionList(dtv.Arguments);
wr.Write(")");
}
-
+
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
if (e is MultiSetDisplayExpr) wr.Write("multiset");
wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "{" : "[");
PrintExpressionList(e.Elements);
wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "}" : "]");
-
+
} else if (expr is FieldSelectExpr) {
FieldSelectExpr e = (FieldSelectExpr)expr;
// determine if parens are needed
@@ -800,7 +800,7 @@ namespace Microsoft.Dafny {
bool parensNeeded = !(e.Obj is ImplicitThisExpr) &&
opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
-
+
if (parensNeeded) { wr.Write("("); }
if (!(e.Obj is ImplicitThisExpr)) {
PrintExpr(e.Obj, opBindingStrength, false, false, -1);
@@ -815,7 +815,7 @@ namespace Microsoft.Dafny {
int opBindingStrength = 0x70;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
-
+
if (parensNeeded) { wr.Write("("); }
PrintExpr(e.Seq, 0x00, false, false, indent); // BOGUS: fix me
wr.Write("[");
@@ -859,7 +859,7 @@ namespace Microsoft.Dafny {
int opBindingStrength = 0x70;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
-
+
if (parensNeeded) { wr.Write("("); }
PrintExpr(e.Seq, 00, false, false, indent); // BOGUS: fix me
wr.Write("[");
@@ -868,7 +868,7 @@ namespace Microsoft.Dafny {
PrintExpression(e.Value);
wr.Write("]");
if (parensNeeded) { wr.Write(")"); }
-
+
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
// determine if parens are needed
@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
bool parensNeeded = !(e.Receiver is ImplicitThisExpr) &&
opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
-
+
if (parensNeeded) { wr.Write("("); }
if (!(e.Receiver is ImplicitThisExpr)) {
PrintExpr(e.Receiver, opBindingStrength, false, false, -1);
@@ -935,14 +935,14 @@ namespace Microsoft.Dafny {
PrintExpr(e.E, opBindingStrength, false, parensNeeded || isRightmost, -1);
if (parensNeeded) { wr.Write(")"); }
}
-
+
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
// determine if parens are needed
int opBindingStrength;
bool fragileLeftContext = false; // false means "allow same binding power on left without parens"
bool fragileRightContext = false; // false means "allow same binding power on right without parens"
- switch (e.Op)
+ switch (e.Op)
{
case BinaryExpr.Opcode.Add:
opBindingStrength = 0x40; break;
@@ -1070,7 +1070,7 @@ namespace Microsoft.Dafny {
} else if (expr is WildcardExpr) {
wr.Write("*");
-
+
} else if (expr is ITEExpr) {
ITEExpr ite = (ITEExpr)expr;
bool parensNeeded = !isRightmost;
@@ -1082,7 +1082,7 @@ namespace Microsoft.Dafny {
wr.Write(" else ");
PrintExpression(ite.Els);
if (parensNeeded) { wr.Write(")"); }
-
+
} else if (expr is ParensExpression) {
var e = (ParensExpression)expr;
// printing of parentheses is done optimally, not according to the parentheses in the given program
@@ -1100,24 +1100,24 @@ namespace Microsoft.Dafny {
PrintExpressionList(e.Arguments);
wr.Write(")");
}
-
+
} else if (expr is MatchExpr) {
Contract.Assert(false); throw new cce.UnreachableException(); // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
}
-
+
void PrintTriggers(Triggers trigs) {
if (trigs != null) {
PrintTriggers(trigs.Prev);
-
+
wr.Write("{ ");
PrintExpressionList(trigs.Terms);
wr.Write(" } ");
}
}
-
+
void PrintExpressionList(List<Expression> exprs) {
Contract.Requires(exprs != null);
string sep = "";
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1321a987..098dbad2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -67,7 +67,7 @@ namespace Microsoft.Dafny {
}
bool checkRefinements = true; // used to indicate a cycle in refinements
-
+
public void ResolveProgram(Program prog) {
Contract.Requires(prog != null);
// register modules
@@ -119,15 +119,15 @@ namespace Microsoft.Dafny {
}
}
- // resolve top-level declarations of refinements
- foreach (ModuleDecl m in prog.Modules)
- foreach (TopLevelDecl decl in m.TopLevelDecls)
+ // resolve top-level declarations of refinements
+ foreach (ModuleDecl m in prog.Modules)
+ foreach (TopLevelDecl decl in m.TopLevelDecls)
if (decl is ClassRefinementDecl) {
ClassRefinementDecl rdecl = (ClassRefinementDecl) decl;
ResolveTopLevelRefinement(rdecl);
if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);
}
-
+
// attempt finding refinement cycles
List<TopLevelDecl> refinesCycle = refines.TryFindCycle();
if (refinesCycle != null) {
@@ -139,8 +139,8 @@ namespace Microsoft.Dafny {
}
Error(refinesCycle[0], "Detected a cyclic refinement declaration: {0}", cy);
checkRefinements = false;
- }
-
+ }
+
// resolve top-level declarations
Graph<DatatypeDecl> datatypeDependencies = new Graph<DatatypeDecl>();
foreach (ModuleDecl m in prog.Modules) {
@@ -168,7 +168,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
public void RegisterTopLevelDecls(List<TopLevelDecl> declarations) {
Contract.Requires(declarations != null);
foreach (TopLevelDecl d in declarations) {
@@ -209,7 +209,7 @@ namespace Microsoft.Dafny {
// ... and of the other members
Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();
datatypeMembers.Add(dt, members);
-
+
foreach (DatatypeCtor ctor in dt.Ctors) {
if (ctor.Name.EndsWith("?")) {
Error(ctor, "a datatype constructor name is not allowed to end with '?'");
@@ -224,7 +224,7 @@ namespace Microsoft.Dafny {
query.EnclosingClass = dt; // resolve here
members.Add(queryName, query);
ctor.QueryField = query;
-
+
// also register the constructor name globally
Tuple<DatatypeCtor, bool> pair;
if (allDatatypeCtors.TryGetValue(ctor.Name, out pair)) {
@@ -268,9 +268,9 @@ namespace Microsoft.Dafny {
}
decl.Refined = cce.NonNull((ClassDecl) a);
// TODO: copy over remaining members of a
- }
- }
-
+ }
+ }
+
public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
Contract.Requires(declarations != null);
Contract.Requires(cce.NonNullElements(datatypeDependencies));
@@ -286,7 +286,7 @@ namespace Microsoft.Dafny {
allTypeParameters.PopMarker();
}
}
-
+
public void ResolveTopLevelDecls_Meat(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
Contract.Requires(declarations != null);
Contract.Requires(cce.NonNullElements(datatypeDependencies));
@@ -306,7 +306,7 @@ namespace Microsoft.Dafny {
allTypeParameters.PopMarker();
}
}
-
+
ClassDecl currentClass;
Function currentFunction;
readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();
@@ -314,7 +314,7 @@ namespace Microsoft.Dafny {
readonly Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
readonly List<Statement> loopStack = new List<Statement>(); // the enclosing loops (from which it is possible to break out)
readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
-
+
/// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
@@ -323,13 +323,13 @@ namespace Microsoft.Dafny {
Contract.Requires(cl != null);
Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
-
+
currentClass = cl;
foreach (MemberDecl member in cl.Members) {
member.EnclosingClass = cl;
if (member is Field) {
ResolveType(member.tok, ((Field)member).Type);
-
+
} else if (member is Function) {
Function f = (Function)member;
allTypeParameters.PushMarker();
@@ -343,15 +343,15 @@ namespace Microsoft.Dafny {
ResolveTypeParameters(m.TypeArgs, true, m);
ResolveMethodSignature(m);
allTypeParameters.PopMarker();
-
+
} else if (member is CouplingInvariant) {
CouplingInvariant inv = (CouplingInvariant)member;
- if (currentClass is ClassRefinementDecl) {
+ if (currentClass is ClassRefinementDecl) {
ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
if (refined != null) {
Contract.Assert(classMembers.ContainsKey(refined));
Dictionary<string,MemberDecl> members = classMembers[refined];
-
+
// resolve abstracted fields in the refined class
List<Field> fields = new List<Field>();
foreach (IToken tok in inv.Toks) {
@@ -359,29 +359,29 @@ namespace Microsoft.Dafny {
Error(tok, "Refined class does not declare a field: {0}", tok.val);
else {
MemberDecl field = members[tok.val];
- if (!(field is Field))
+ if (!(field is Field))
Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);
else if (fields.Contains(cce.NonNull((Field)field)))
Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);
else
fields.Add(cce.NonNull((Field)field));
- }
- }
+ }
+ }
inv.Refined = fields;
}
-
+
} else {
Error(member, "Coupling invariants can only be declared in refinement classes");
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
}
-
- if (currentClass is ClassRefinementDecl) {
+
+ if (currentClass is ClassRefinementDecl) {
ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
if (refined != null) {
Contract.Assert(classMembers.ContainsKey(refined));
-
+
// there is a member with the same name in refined class if and only if the member is a refined method
if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))
Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);
@@ -399,14 +399,14 @@ namespace Microsoft.Dafny {
Contract.Requires(cl != null);
Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
-
+
ResolveAttributes(cl.Attributes, false);
currentClass = cl;
foreach (MemberDecl member in cl.Members) {
ResolveAttributes(member.Attributes, false);
if (member is Field) {
// nothing more to do
-
+
} else if (member is Function) {
Function f = (Function)member;
allTypeParameters.PushMarker();
@@ -420,13 +420,13 @@ namespace Microsoft.Dafny {
ResolveTypeParameters(m.TypeArgs, false, m);
ResolveMethod(m);
allTypeParameters.PopMarker();
-
+
// check if signature of the refined method matches the refinement method
if (member is MethodRefinement) {
MethodRefinement mf = (MethodRefinement)member;
if (currentClass is ClassRefinementDecl) {
// should have already been resolved
- if (((ClassRefinementDecl)currentClass).Refined != null) {
+ if (((ClassRefinementDecl)currentClass).Refined != null) {
MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];
if (d is Method) {
mf.Refined = (Method)d;
@@ -434,18 +434,18 @@ namespace Microsoft.Dafny {
Error(mf, "Different number of input variables");
if (mf.Outs.Count != mf.Refined.Outs.Count)
Error(mf, "Different number of output variables");
- if (mf.IsStatic || mf.Refined.IsStatic)
+ if (mf.IsStatic || mf.Refined.IsStatic)
Error(mf, "Refined methods cannot be static");
} else {
Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);
- }
+ }
}
} else {
Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);
}
}
-
- } else if (member is CouplingInvariant) {
+
+ } else if (member is CouplingInvariant) {
CouplingInvariant inv = (CouplingInvariant)member;
if (inv.Refined != null) {
inv.Formals = new List<Formal>();
@@ -460,7 +460,7 @@ namespace Microsoft.Dafny {
}
ResolveExpression(inv.Expr, false);
scope.PopMarker();
- }
+ }
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
}
@@ -476,13 +476,13 @@ namespace Microsoft.Dafny {
Contract.Requires(dt != null);
Contract.Requires(cce.NonNullElements(dependencies));
foreach (DatatypeCtor ctor in dt.Ctors) {
-
+
ctor.EnclosingDatatype = dt;
allTypeParameters.PushMarker();
ResolveCtorSignature(ctor);
allTypeParameters.PopMarker();
-
+
foreach (Formal p in ctor.Formals) {
DatatypeDecl dependee = p.Type.AsDatatype;
if (dependee != null) {
@@ -497,7 +497,7 @@ namespace Microsoft.Dafny {
/// datatype has some value that can be constructed from datatypes in lower stratospheres only.
/// The algorithm used here is quadratic in the number of datatypes in the SCC. Since that number is
/// deemed to be rather small, this seems okay.
- /// </summary>
+ /// </summary>
void SccStratosphereCheck(DatatypeDecl startingPoint, Graph<DatatypeDecl/*!*/>/*!*/ dependencies)
{
Contract.Requires(startingPoint != null);
@@ -573,7 +573,7 @@ namespace Microsoft.Dafny {
ResolveAttributeArgs(attrs.Args, twoState);
}
}
-
+
void ResolveAttributeArgs(List<Attributes.Argument/*!*/>/*!*/ args, bool twoState) {
Contract.Requires(args != null);
foreach (Attributes.Argument aa in args) {
@@ -583,7 +583,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
void ResolveTriggers(Triggers trigs, bool twoState) {
// order does not matter for resolution, so resolve them in reverse order
for (; trigs != null; trigs = trigs.Prev) {
@@ -592,9 +592,9 @@ namespace Microsoft.Dafny {
}
}
}
-
+
void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {
-
+
Contract.Requires(tparams != null);
Contract.Requires(parent != null);
// push type arguments of the refined class
@@ -603,7 +603,7 @@ namespace Microsoft.Dafny {
if (refined != null)
ResolveTypeParameters(refined.TypeArgs, false, refined);
}
-
+
// push non-duplicated type parameter names
foreach (TypeParameter tp in tparams) {
Contract.Assert(tp != null);
@@ -616,7 +616,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
/// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
@@ -683,7 +683,7 @@ namespace Microsoft.Dafny {
currentFunction = null;
scope.PopMarker();
}
-
+
void ResolveFrameExpression(FrameExpression fe, string kind) {
Contract.Requires(fe != null);
Contract.Requires(kind != null);
@@ -717,7 +717,7 @@ namespace Microsoft.Dafny {
Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);
}
}
-
+
/// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
@@ -740,7 +740,7 @@ namespace Microsoft.Dafny {
}
scope.PopMarker();
}
-
+
/// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
@@ -754,7 +754,7 @@ namespace Microsoft.Dafny {
foreach (Formal p in m.Ins) {
scope.Push(p.Name, p);
}
-
+
// Start resolving specification...
foreach (MaybeFreeExpression e in m.Req) {
ResolveExpression(e.E, false);
@@ -770,7 +770,7 @@ namespace Microsoft.Dafny {
ResolveExpression(e, false);
// any type is fine
}
-
+
// Add out-parameters to a new scope that will also include the outermost-level locals of the body
// Don't care about any duplication errors among the out-parameters, since they have already been reported
scope.PushMarker();
@@ -786,16 +786,16 @@ namespace Microsoft.Dafny {
Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
}
}
-
+
// Resolve body
if (m.Body != null) {
ResolveBlockStatement(m.Body, m.IsGhost, m);
}
-
+
scope.PopMarker(); // for the out-parameters and outermost-level locals
scope.PopMarker(); // for the in-parameters
}
-
+
void ResolveCtorSignature(DatatypeCtor ctor) {
Contract.Requires(ctor != null);
foreach (Formal p in ctor.Formals) {
@@ -839,18 +839,18 @@ namespace Microsoft.Dafny {
Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);
}
}
-
+
} else if (type is TypeProxy) {
TypeProxy t = (TypeProxy)type;
if (t.T != null) {
ResolveType(tok, t.T);
}
-
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
-
+
public bool UnifyTypes(Type a, Type b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
@@ -866,7 +866,7 @@ namespace Microsoft.Dafny {
a = proxy.T;
}
}
-
+
while (b is TypeProxy) {
TypeProxy proxy = (TypeProxy)b;
if (proxy.T == null) {
@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
b = proxy.T;
}
}
-
+
#if !NO_CHEAP_OBJECT_WORKAROUND
if (a is ObjectType || b is ObjectType) { // TODO: remove this temporary hack
var other = a is ObjectType ? b : a;
@@ -888,7 +888,7 @@ namespace Microsoft.Dafny {
}
#endif
// Now, a and b are non-proxies and stand for the same things as the original a and b, respectively.
-
+
if (a is BoolType) {
return b is BoolType;
} else if (a is IntType) {
@@ -925,12 +925,12 @@ namespace Microsoft.Dafny {
// something is wrong; either aa or bb wasn't properly resolved, or they don't unify
return false;
}
-
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
-
+
bool AssignProxy(TypeProxy proxy, Type t){
Contract.Requires(proxy != null);
Contract.Requires(t != null);
@@ -941,15 +941,15 @@ namespace Microsoft.Dafny {
if (proxy == t) {
// they are already in the same equivalence class
return true;
-
+
} else if (proxy is UnrestrictedTypeProxy) {
// it's fine to redirect proxy to t (done below)
-
+
} else if (t is UnrestrictedTypeProxy) {
// merge proxy and t by redirecting t to proxy, rather than the other way around
((TypeProxy)t).T = proxy;
return true;
-
+
} else if (t is RestrictedTypeProxy) {
// Both proxy and t are restricted type proxies. To simplify unification, order proxy and t
// according to their types.
@@ -960,7 +960,7 @@ namespace Microsoft.Dafny {
} else {
return AssignRestrictedProxies(r1, r0);
}
-
+
// In the remaining cases, proxy is a restricted proxy and t is a non-proxy
} else if (proxy is DatatypeProxy) {
if (t.IsDatatype) {
@@ -968,14 +968,14 @@ namespace Microsoft.Dafny {
} else {
return false;
}
-
+
} else if (proxy is ObjectTypeProxy) {
if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
// all is fine, proxy can be redirected to t
} else {
return false;
}
-
+
} else if (proxy is ObjectsTypeProxy) {
if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
// all is good
@@ -983,7 +983,7 @@ namespace Microsoft.Dafny {
proxy.T = new CollectionTypeProxy(new ObjectTypeProxy());
return UnifyTypes(proxy.T, t);
}
-
+
} else if (proxy is CollectionTypeProxy) {
CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;
if (t is CollectionType) {
@@ -993,7 +993,7 @@ namespace Microsoft.Dafny {
} else {
return false;
}
-
+
} else if (proxy is OperationTypeProxy) {
OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
if (t is IntType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {
@@ -1016,11 +1016,11 @@ namespace Microsoft.Dafny {
} else {
return false;
}
-
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected proxy type
}
-
+
// do the merge, but never infer a subrange type
if (t is NatType) {
proxy.T = Type.Int;
@@ -1029,7 +1029,7 @@ namespace Microsoft.Dafny {
}
return true;
}
-
+
bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b)
{ Contract.Requires(a != null);
Contract.Requires(b != null);
@@ -1038,7 +1038,7 @@ namespace Microsoft.Dafny {
Contract.Requires(a.OrderID <= b.OrderID);
//modifies a.T, b.T;
Contract.Ensures(Contract.Result<bool>() || a.T != null || b.T != null);
-
+
if (a is DatatypeProxy) {
if (b is DatatypeProxy) {
// all is fine
@@ -1064,7 +1064,7 @@ namespace Microsoft.Dafny {
} else {
return false;
}
-
+
} else if (a is ObjectsTypeProxy) {
if (b is ObjectsTypeProxy) {
// fine
@@ -1095,7 +1095,7 @@ namespace Microsoft.Dafny {
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
}
-
+
} else if (a is CollectionTypeProxy) {
if (b is CollectionTypeProxy) {
a.T = b;
@@ -1119,7 +1119,7 @@ namespace Microsoft.Dafny {
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
}
-
+
} else if (a is OperationTypeProxy) {
OperationTypeProxy pa = (OperationTypeProxy)a;
if (b is OperationTypeProxy) {
@@ -1140,12 +1140,12 @@ namespace Microsoft.Dafny {
return false;
}
}
-
+
} else if (a is IndexableTypeProxy) {
Contract.Assert(b is IndexableTypeProxy); // else we have unexpected restricted-proxy type
a.T = b;
return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg);
-
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
}
@@ -1166,14 +1166,14 @@ namespace Microsoft.Dafny {
if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
}
-
+
} else if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
ResolveAttributeArgs(s.Args, false);
if (specContextOnly) {
Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
-
+
} else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
@@ -1323,7 +1323,7 @@ namespace Microsoft.Dafny {
} else {
Error(stmt, "LHS of assignment must denote a mutable variable or field");
}
-
+
s.IsGhost = lvalueIsGhost;
Type lhsType = s.Lhs.Type;
if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
@@ -1378,16 +1378,16 @@ namespace Microsoft.Dafny {
// a local variable in a specification-only context might as well be ghost
s.IsGhost = true;
}
-
+
} else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
ResolveCallStmt(s, specContextOnly, method, null);
-
+
} else if (stmt is BlockStmt) {
scope.PushMarker();
ResolveBlockStatement((BlockStmt)stmt, specContextOnly, method);
scope.PopMarker();
-
+
} else if (stmt is IfStmt) {
IfStmt s = (IfStmt)stmt;
bool branchesAreSpecOnly = specContextOnly;
@@ -1481,20 +1481,20 @@ namespace Microsoft.Dafny {
if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) {
Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type);
}
-
+
scope.PushMarker();
bool b = scope.Push(s.BoundVar.Name, s.BoundVar);
Contract.Assert(b); // since we just pushed a marker, we expect the Push to succeed
ResolveType(s.BoundVar.tok, s.BoundVar.Type);
int prevErrorCount = ErrorCount;
-
+
ResolveExpression(s.Range, true);
Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(s.Range.Type, Type.Bool)) {
Error(s.Range, "range condition is expected to be of type {0}, but is {1}", Type.Bool, s.Range.Type);
}
bool successfullyResolvedCollectionAndRange = ErrorCount == prevErrorCount;
-
+
foreach (PredicateStmt ss in s.BodyPrefix) {
ResolveStatement(ss, specContextOnly, method);
}
@@ -1528,7 +1528,7 @@ namespace Microsoft.Dafny {
}
scope.PopMarker();
-
+
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
bool bodyIsSpecOnly = specContextOnly;
@@ -1554,14 +1554,14 @@ namespace Microsoft.Dafny {
Contract.Assert(sourceType != null); // dtd and sourceType are set together above
ctors = datatypeCtors[dtd];
Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
-
+
// build the type-parameter substitution map for this use of the datatype
for (int i = 0; i < dtd.TypeArgs.Count; i++) {
subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
}
}
s.IsGhost = bodyIsSpecOnly;
-
+
Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>(); // this is really a set
foreach (MatchCaseStmt mc in s.Cases) {
DatatypeCtor ctor = null;
@@ -1616,8 +1616,8 @@ namespace Microsoft.Dafny {
}
Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);
}
-
-
+
+
} else {
Contract.Assert(false); throw new cce.UnreachableException();
}
@@ -2186,7 +2186,7 @@ namespace Microsoft.Dafny {
}
/// <summary>
- /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression;
+ /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression;
/// if null, no "match" expression will be allowed.
/// </summary>
void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext) {
@@ -2197,7 +2197,7 @@ namespace Microsoft.Dafny {
// expression has already been resovled
return;
}
-
+
// The following cases will resolve the subexpressions and will attempt to assign a type of expr. However, if errors occur
// and it cannot be determined what the type of expr is, then it is fine to leave expr.Type as null. In that case, the end
// of this method will assign proxy type to the expression, which reduces the number of error messages that are produced
@@ -2230,13 +2230,13 @@ namespace Microsoft.Dafny {
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal type
}
-
+
} else if (expr is ThisExpr) {
if (!scope.AllowInstance) {
Error(expr, "'this' is not allowed in a 'static' context");
}
expr.Type = GetThisType(expr.tok, currentClass); // do this regardless of scope.AllowInstance, for better error reporting
-
+
} else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
e.Var = scope.Find(e.Name);
@@ -2245,7 +2245,7 @@ namespace Microsoft.Dafny {
} else {
expr.Type = e.Var.Type;
}
-
+
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
TopLevelDecl d;
@@ -2266,7 +2266,7 @@ namespace Microsoft.Dafny {
}
expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);
ResolveType(expr.tok, expr.Type);
-
+
DatatypeCtor ctor;
if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {
Error(expr.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);
@@ -2291,7 +2291,7 @@ namespace Microsoft.Dafny {
j++;
}
}
-
+
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
Type elementType = new InferredTypeProxy();
@@ -2309,7 +2309,7 @@ namespace Microsoft.Dafny {
} else {
expr.Type = new SeqType(elementType);
}
-
+
} else if (expr is FieldSelectExpr) {
var e = (FieldSelectExpr)expr;
ResolveExpression(e.Obj, twoState);
@@ -2336,7 +2336,7 @@ namespace Microsoft.Dafny {
}
e.Type = SubstType(e.Field.Type, subst);
}
-
+
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
ResolveSeqSelectExpr(e, twoState, true);
@@ -2385,7 +2385,7 @@ namespace Microsoft.Dafny {
if (!seqErr) {
expr.Type = e.Seq.Type;
}
-
+
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
ResolveFunctionCallExpr(e, twoState, false);
@@ -2459,7 +2459,7 @@ namespace Microsoft.Dafny {
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator
}
-
+
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
ResolveExpression(e.E0, twoState);
@@ -2479,7 +2479,7 @@ namespace Microsoft.Dafny {
}
expr.Type = Type.Bool;
break;
-
+
case BinaryExpr.Opcode.Eq:
case BinaryExpr.Opcode.Neq:
if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
@@ -2487,7 +2487,7 @@ namespace Microsoft.Dafny {
}
expr.Type = Type.Bool;
break;
-
+
case BinaryExpr.Opcode.Disjoint:
// TODO: the error messages are backwards from what (ideally) they should be. this is necessary because UnifyTypes can't backtrack.
if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
@@ -2498,7 +2498,7 @@ namespace Microsoft.Dafny {
}
expr.Type = Type.Bool;
break;
-
+
case BinaryExpr.Opcode.Lt:
case BinaryExpr.Opcode.Le:
case BinaryExpr.Opcode.Add:
@@ -2526,7 +2526,7 @@ namespace Microsoft.Dafny {
}
}
break;
-
+
case BinaryExpr.Opcode.Sub:
case BinaryExpr.Opcode.Mul:
case BinaryExpr.Opcode.Gt:
@@ -2563,7 +2563,7 @@ namespace Microsoft.Dafny {
}
expr.Type = Type.Bool;
break;
-
+
case BinaryExpr.Opcode.Div:
case BinaryExpr.Opcode.Mod:
if (!UnifyTypes(e.E0.Type, Type.Int)) {
@@ -2574,12 +2574,12 @@ namespace Microsoft.Dafny {
}
expr.Type = Type.Int;
break;
-
+
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected operator
}
e.ResolvedOp = ResolveOp(e.Op, e.E1.Type);
-
+
} else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
int prevErrorCount = ErrorCount;
@@ -2652,7 +2652,7 @@ namespace Microsoft.Dafny {
} else if (expr is WildcardExpr) {
expr.Type = new SetType(new ObjectType());
-
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
ResolveExpression(e.Test, twoState);
@@ -2669,7 +2669,7 @@ namespace Microsoft.Dafny {
} else {
Error(expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type);
}
-
+
} else if (expr is MatchExpr) {
MatchExpr me = (MatchExpr)expr;
Contract.Assert(!twoState); // currently, match expressions are allowed only at the outermost level of function bodies
@@ -2695,7 +2695,7 @@ namespace Microsoft.Dafny {
Contract.Assert(sourceType != null); // dtd and sourceType are set together above
ctors = datatypeCtors[dtd];
Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
-
+
IdentifierExpr ie = me.Source.Resolved as IdentifierExpr;
if (ie == null || !(ie.Var is Formal || ie.Var is BoundVar)) {
Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function or an enclosing match expression");
@@ -2704,13 +2704,13 @@ namespace Microsoft.Dafny {
} else {
goodMatchVariable = ie.Var;
}
-
+
// build the type-parameter substitution map for this use of the datatype
for (int i = 0; i < dtd.TypeArgs.Count; i++) {
subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
}
}
-
+
Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>(); // this is really a set
expr.Type = new InferredTypeProxy();
foreach (MatchCaseExpr mc in me.Cases) {
@@ -2773,7 +2773,7 @@ namespace Microsoft.Dafny {
}
Contract.Assert(memberNamesUsed.Count + me.MissingCases.Count == dtd.Ctors.Count);
}
-
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
@@ -3498,13 +3498,13 @@ namespace Microsoft.Dafny {
return s == null ? new HashSet<IVariable>() : s;
}
}
-
+
void ResolveReceiver(Expression expr, bool twoState)
{
Contract.Requires(expr != null);
Contract.Requires(currentClass != null);
Contract.Ensures(expr.Type != null);
-
+
if (expr is ThisExpr) {
// Allow 'this' here, regardless of scope.AllowInstance. The caller is responsible for
// making sure 'this' does not really get used when it's not available.
@@ -3513,7 +3513,7 @@ namespace Microsoft.Dafny {
ResolveExpression(expr, twoState);
}
}
-
+
void ResolveSeqSelectExpr(SeqSelectExpr e, bool twoState, bool allowNonUnitArraySelection) {
Contract.Requires(e != null);
if (e.Type != null) {
@@ -3557,7 +3557,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
/// <summary>
/// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if
/// resolution of the binary expression failed. If so, an arbitrary resolved opcode is returned.
@@ -3693,7 +3693,7 @@ namespace Microsoft.Dafny {
{
Contract.Requires(expr != null);
Contract.Requires(currentClass != null);
-
+
if (expr is LiteralExpr) {
return false;
} else if (expr is ThisExpr) {
@@ -3769,7 +3769,7 @@ namespace Microsoft.Dafny {
[Rep] readonly List<string> names = new List<string>(); // a null means a marker
[Rep] readonly List<Thing> things = new List<Thing>();
[ContractInvariantMethod]
- void ObjectInvariant()
+ void ObjectInvariant()
{
Contract.Invariant(names != null);
Contract.Invariant(things != null);
@@ -3778,7 +3778,7 @@ namespace Microsoft.Dafny {
}
int scopeSizeWhereInstancesWereDisallowed = -1;
-
+
public bool AllowInstance {
get { return scopeSizeWhereInstancesWereDisallowed == -1; }
set
@@ -3791,7 +3791,7 @@ namespace Microsoft.Dafny {
names.Add(null);
things.Add(null);
}
-
+
public void PopMarker() {
int n = names.Count;
while (true) {
@@ -3806,7 +3806,7 @@ namespace Microsoft.Dafny {
scopeSizeWhereInstancesWereDisallowed = -1;
}
}
-
+
// Pushes name-->thing association and returns "true", if name has not already been pushed since the last marker.
// If name already has been pushed since the last marker, does nothing and returns "false".
public bool Push(string name, Thing thing) {
@@ -3820,7 +3820,7 @@ namespace Microsoft.Dafny {
return true;
}
}
-
+
Thing Find(string name, bool topScopeOnly) {
Contract.Requires(name != null);
for (int n = names.Count; 0 <= --n; ) {
@@ -3836,7 +3836,7 @@ namespace Microsoft.Dafny {
}
return null; // not present
}
-
+
public Thing Find(string name) {
Contract.Requires(name != null);
return Find(name, false);
diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs
index 9f4b22c5..4ae1c185 100644
--- a/Source/Dafny/SccGraph.cs
+++ b/Source/Dafny/SccGraph.cs
@@ -12,14 +12,14 @@ namespace Microsoft.Dafny {
public readonly List<Vertex/*!*/>/*!*/ Successors = new List<Vertex/*!*/>();
public List<Vertex/*!*/> SccMembers; // non-null only for the representative of the SCC
[ContractInvariantMethod]
- void ObjectInvariant()
+ void ObjectInvariant()
{
Contract.Invariant(cce.NonNullElements(Successors));
Contract.Invariant(SccMembers==null || cce.NonNullElements(SccMembers));
}
public Vertex SccRepresentative; // null if not computed
-
+
public int SccId; // valid only for SCC representatives; indicates position of this representative vertex in the graph's topological sort
// the following field is used during the computation of SCCs and of reachability
public VisitedStatus Visited;
@@ -28,7 +28,7 @@ namespace Microsoft.Dafny {
public int LowLink;
// the following field is used during a Reaches computation
public int Gen; // generation <= Gen means this vertex has been visited in the current generation
-
+
public Vertex(Node n) {
N = n;
}
@@ -40,7 +40,7 @@ namespace Microsoft.Dafny {
[ContractInvariantMethod]
- void ObjectInvariant()
+ void ObjectInvariant()
{
Contract.Invariant(vertices!=null);
Contract.Invariant(cce.NonNullElements(vertices.Values));
@@ -51,7 +51,7 @@ namespace Microsoft.Dafny {
Dictionary<Node, Vertex/*!*/>/*!*/ vertices = new Dictionary<Node, Vertex/*!*/>();
bool sccComputed = false;
List<Vertex/*!*/> topologicallySortedRepresentatives; // computed by the SCC computation
-
+
public int SccCount {
get {
ComputeSCCs();
@@ -60,11 +60,11 @@ namespace Microsoft.Dafny {
}
}
int generation = 0;
-
+
public Graph()
{
}
-
+
/// <summary>
/// Idempotently adds a vertex 'n' to the graph.
/// </summary>
@@ -74,7 +74,7 @@ namespace Microsoft.Dafny {
/// <summary>
/// Idempotently adds a vertex 'n' to the graph and then returns the Vertex for it.
- /// </summary>
+ /// </summary>
Vertex GetVertex(Node n) {
Contract.Ensures(Contract.Result<Vertex>() != null);
@@ -93,7 +93,7 @@ namespace Microsoft.Dafny {
}
return v;
}
-
+
/// <summary>
/// Returns the vertex for 'n' if 'n' is in the graph. Otherwise, returns null.
/// </summary>
@@ -117,7 +117,7 @@ namespace Microsoft.Dafny {
v0.AddSuccessor(v1);
sccComputed = false; // the addition of an edge may invalidate any previous computation of the graph's SCCs
}
-
+
/// <summary>
/// Idempotently adds 'n' as a vertex and then returns a Node that is the representative element of the
/// strongly connected component containing 'n'.
@@ -125,7 +125,7 @@ namespace Microsoft.Dafny {
public Node GetSCCRepresentative(Node n) {
return GetSCCRepr(n).N;
}
-
+
/// <summary>
/// Idempotently adds 'n' as a vertex. Then, returns the number of SCCs before the SCC of 'n' in the
/// topologically sorting of SCCs.
@@ -133,7 +133,7 @@ namespace Microsoft.Dafny {
public int GetSCCRepresentativeId(Node n) {
return GetSCCRepr(n).SccId;
}
-
+
Vertex GetSCCRepr(Node n) {
Contract.Ensures(Contract.Result<Vertex>() != null);
@@ -142,7 +142,7 @@ namespace Microsoft.Dafny {
Contract.Assert(v.SccRepresentative != null); // follows from what ComputeSCCs does
return v.SccRepresentative;
}
-
+
/// <summary>
/// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node.
/// </summary>
@@ -172,21 +172,21 @@ namespace Microsoft.Dafny {
}
return nn;
}
-
+
/// <summary>
/// Idempotently adds 'n' as a vertex and then returns the size of the set of Node's in the strongly connected component
/// that contains 'n'.
/// </summary>
public int GetSCCSize(Node n){
Contract.Ensures(1 <= Contract.Result<int>());
-
+
Vertex v = GetVertex(n);
ComputeSCCs();
Vertex repr = v.SccRepresentative;
Contract.Assert(repr != null && repr.SccMembers != null); // follows from postcondition of ComputeSCCs
return repr.SccMembers.Count;
}
-
+
/// <summary>
/// This method sets the SccRepresentative fields of the graph's vertices so that two
/// vertices have the same representative iff they are in the same strongly connected
@@ -197,7 +197,7 @@ namespace Microsoft.Dafny {
void ComputeSCCs()
{
Contract.Ensures(sccComputed);
-
+
if (sccComputed) { return; } // check if already computed
// reset all SCC information
@@ -217,7 +217,7 @@ namespace Microsoft.Dafny {
sccComputed = true;
}
-
+
/// <summary>
/// This is the 'SearchC' procedure from the Aho, Hopcroft, and Ullman book 'The Design and Analysis of Computer Algorithms'.
/// </summary>
@@ -227,13 +227,13 @@ namespace Microsoft.Dafny {
Contract.Requires(v.Visited == VisitedStatus.Unvisited);
Contract.Requires(topologicallySortedRepresentatives != null);
Contract.Ensures(v.Visited != VisitedStatus.Unvisited);
-
+
v.DfNumber = cnt;
cnt++;
v.LowLink = v.DfNumber;
stack.Push(v);
v.Visited = VisitedStatus.OnStack;
-
+
foreach (Vertex w in v.Successors) {
if (w.Visited == VisitedStatus.Unvisited) {
SearchC(w, stack, ref cnt);
@@ -243,7 +243,7 @@ namespace Microsoft.Dafny {
v.LowLink = Math.Min(v.LowLink, w.DfNumber);
}
}
-
+
if (v.LowLink == v.DfNumber) {
// The SCC containing 'v' has now been computed.
v.SccId = topologicallySortedRepresentatives.Count;
@@ -258,7 +258,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
/// <summary>
/// Returns null if the graph has no cycles. If the graph does contain some cycle, returns the list of
/// vertices on one such cycle.
@@ -268,7 +268,7 @@ namespace Microsoft.Dafny {
foreach (Vertex v in vertices.Values) {
v.Visited = VisitedStatus.Unvisited;
}
-
+
foreach (Vertex v in vertices.Values) {
Contract.Assert(v.Visited != VisitedStatus.OnStack);
if (v.Visited == VisitedStatus.Unvisited) {
@@ -284,7 +284,7 @@ namespace Microsoft.Dafny {
}
return null; // there are no cycles
}
-
+
/// <summary>
/// A return of null means there are no cycles involving any vertex in the subtree rooted at v.
/// A non-null return means a cycle has been found. Then:
@@ -300,7 +300,7 @@ namespace Microsoft.Dafny {
Contract.Ensures(v.Visited != VisitedStatus.Unvisited);
Contract.Ensures(Contract.Result<List<Vertex>>() != null || v.Visited == VisitedStatus.Visited);
Contract.Ensures(Contract.Result<List<Vertex>>() == null || Contract.Result<List<Vertex>>().Count != 0);
-
+
v.Visited = VisitedStatus.OnStack;
foreach (Vertex succ in v.Successors) {
// todo: I would use a 'switch' statement, but there seems to be a bug in the Spec# compiler's type checking.
@@ -337,7 +337,7 @@ namespace Microsoft.Dafny {
v.Visited = VisitedStatus.Visited; // there are no cycles from here on
return null;
}
-
+
/// <summary>
/// Returns whether or not 'source' reaches 'sink' in the graph.
/// 'source' and 'sink' need not be in the graph; if neither is, the return value
@@ -352,7 +352,7 @@ namespace Microsoft.Dafny {
generation++;
return ReachSearch(a, b);
}
-
+
bool ReachSearch(Vertex source, Vertex sink) {
Contract.Requires(source != null);
Contract.Requires(sink != null);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 4d84a5f5..cc97fb40 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -21,14 +21,14 @@ namespace Microsoft.Dafny {
predef = FindPredefinedDecls(boogieProgram);
}
}
-
+
// translation state
readonly Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>/*!*/ classes = new Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>();
readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();
readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();
[ContractInvariantMethod]
- void ObjectInvariant()
+ void ObjectInvariant()
{
Contract.Invariant(cce.NonNullDictionaryAndValues(classes));
Contract.Invariant(cce.NonNullDictionaryAndValues(fields));
@@ -81,7 +81,7 @@ namespace Microsoft.Dafny {
return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
}
-
+
public Bpl.Type MultiSetType(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
@@ -96,7 +96,7 @@ namespace Microsoft.Dafny {
Contract.Ensures(Contract.Result<Bpl.Type>() != null);
return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));
}
-
+
public Bpl.Type FieldName(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
@@ -104,7 +104,7 @@ namespace Microsoft.Dafny {
return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));
}
-
+
public Bpl.IdentifierExpr Alloc(IToken tok) {
Contract.Requires(tok != null);
Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);
@@ -150,7 +150,7 @@ namespace Microsoft.Dafny {
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
}
}
-
+
static PredefinedDecls FindPredefinedDecls(Bpl.Program prog) {
Contract.Requires(prog != null);
if (prog.Resolve() != 0) {
@@ -248,7 +248,7 @@ namespace Microsoft.Dafny {
}
return null;
}
-
+
static Bpl.Program ReadPrelude() {
string preludePath = Bpl.CommandLineOptions.Clo.DafnyPrelude;
if (preludePath == null)
@@ -257,7 +257,7 @@ namespace Microsoft.Dafny {
string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");
}
-
+
Bpl.Program prelude;
int errorCount = Bpl.Parser.Parse(preludePath, null, out prelude);
if (prelude == null || errorCount > 0) {
@@ -265,7 +265,7 @@ namespace Microsoft.Dafny {
} else {
return prelude;
}
-/*
+/*
List<string!> defines = new List<string!>();
using (System.IO.Stream stream = new System.IO.FileStream(preludePath, System.IO.FileMode.Open, System.IO.FileAccess.Read))
{
@@ -279,9 +279,9 @@ namespace Microsoft.Dafny {
return prelude;
}
}
-*/
+*/
}
-
+
public Bpl.Program Translate(Program program) {
Contract.Requires(program != null);
Contract.Ensures(Contract.Result<Bpl.Program>() != null);
@@ -310,13 +310,13 @@ namespace Microsoft.Dafny {
}
return sink;
}
-
+
void AddDatatype(DatatypeDecl dt)
{
Contract.Requires(dt != null);
Contract.Requires(sink != null && predef != null);
sink.TopLevelDeclarations.Add(GetClass(dt));
-
+
foreach (DatatypeCtor ctor in dt.Ctors) {
// Add: function #dt.ctor(paramTypes) returns (DatatypeType);
Bpl.VariableSeq argTypes = new Bpl.VariableSeq();
@@ -376,7 +376,7 @@ namespace Microsoft.Dafny {
fn.Body = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid)); // this uses the "cid" defined for the previous axiom
sink.TopLevelDeclarations.Add(fn);
- // Add: axiom (forall params, h: HeapType ::
+ // Add: axiom (forall params, h: HeapType ::
// { DtAlloc(#dt.ctor(params), h) }
// $IsGoodHeap(h) ==>
// (DtAlloc(#dt.ctor(params), h) <==> ...each param has its expected type...));
@@ -482,7 +482,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
void CreateBoundVariables(List<Formal/*!*/>/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List<Bpl.Expr/*!*/>/*!*/ args)
{
Contract.Requires(formals != null);
@@ -501,13 +501,13 @@ namespace Microsoft.Dafny {
args.Add(new Bpl.IdentifierExpr(arg.tok, bv));
}
}
-
+
void AddClassMembers(ClassDecl c)
{
Contract.Requires(sink != null && predef != null);
Contract.Requires(c != null);
sink.TopLevelDeclarations.Add(GetClass(c));
-
+
foreach (MemberDecl member in c.Members) {
if (member is Field) {
Field f = (Field)member;
@@ -521,7 +521,7 @@ namespace Microsoft.Dafny {
}
AddAllocationAxiom(f);
-
+
} else if (member is Function) {
Function f = (Function)member;
AddFunction(f);
@@ -543,7 +543,7 @@ namespace Microsoft.Dafny {
}
AddFrameAxiom(f);
AddWellformednessCheck(f);
-
+
} else if (member is Method) {
Method m = (Method)member;
// wellformedness check for method specification
@@ -557,14 +557,14 @@ namespace Microsoft.Dafny {
// ...and its implementation
AddMethodImpl(m, proc, false);
}
-
+
// refinement condition
if (member is MethodRefinement) {
AddMethodRefinement((MethodRefinement)member);
}
-
+
} else if (member is CouplingInvariant) {
- // TODO: define a well-foundedness condition to check
+ // TODO: define a well-foundedness condition to check
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member
@@ -659,9 +659,9 @@ namespace Microsoft.Dafny {
Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive && !f.IsUnlimited));
Contract.Requires(predef != null);
Contract.Requires(f.EnclosingClass != null);
-
+
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
-
+
// axiom
// mh < ModuleContextHeight ||
// (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext))
@@ -702,7 +702,7 @@ namespace Microsoft.Dafny {
args.Add(new Bpl.IdentifierExpr(f.tok, bv));
// ante: $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
-
+
Bpl.BoundVariable bvThis;
Bpl.Expr bvThisIdExpr;
if (f.IsStatic) {
@@ -754,7 +754,7 @@ namespace Microsoft.Dafny {
Bpl.Expr.Or(
Bpl.Expr.Le(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),
etran.InMethodContext())));
-
+
var substMap = new Dictionary<IVariable, Expression>();
if (specialization != null) {
substMap = specialization.SubstMap;
@@ -813,7 +813,7 @@ namespace Microsoft.Dafny {
}
return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);
}
-
+
void AddLimitedAxioms(Function f, int fromLayer) {
Contract.Requires(f != null);
Contract.Requires(f.IsRecursive && !f.IsUnlimited);
@@ -850,7 +850,7 @@ namespace Microsoft.Dafny {
Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);
Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer-1), TrType(f.ResultType)));
Bpl.Expr limitedFuncAppl = new Bpl.NAryExpr(f.tok, limitedFuncID, args);
-
+
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(origFuncAppl));
@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
}
return name;
}
-
+
/// <summary>
/// Generate:
/// axiom (forall h: [ref, Field x]x, o: ref ::
@@ -887,13 +887,13 @@ namespace Microsoft.Dafny {
{
Contract.Requires(f != null);
Contract.Requires(sink != null && predef != null);
-
+
Bpl.BoundVariable hVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h", predef.HeapType));
Bpl.Expr h = new Bpl.IdentifierExpr(f.tok, hVar);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, h);
Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
-
+
// h[o,f]
Bpl.Expr oDotF;
if (f.IsMutable) {
@@ -937,7 +937,7 @@ namespace Microsoft.Dafny {
}
return Bpl.Expr.And(lower, upper);
}
-
+
Method currentMethod = null; // the method whose implementation is currently being translated
int loopHeapVarCount = 0;
int otherTmpVarCount = 0;
@@ -970,7 +970,7 @@ namespace Microsoft.Dafny {
return GetTmpVar_IdExpr(tok, "$prevHeap", predef.HeapType, locals);
}
-
+
Bpl.IdentifierExpr GetNewVar_IdExpr(IToken tok, Bpl.VariableSeq locals) // local variable that's shared between statements that need it
{
Contract.Requires(tok != null);
@@ -1013,7 +1013,7 @@ namespace Microsoft.Dafny {
Contract.Requires(wellformednessProc || m.Body != null);
Contract.Requires(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
Contract.Ensures(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);
-
+
currentMethod = m;
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
@@ -1075,7 +1075,7 @@ namespace Microsoft.Dafny {
typeParams, inParams, outParams,
localVariables, stmts);
sink.TopLevelDeclarations.Add(impl);
-
+
currentMethod = null;
loopHeapVarCount = 0;
otherTmpVarCount = 0;
@@ -1090,7 +1090,7 @@ namespace Microsoft.Dafny {
Contract.Requires(builder != null);
Contract.Requires(localVariables != null);
Contract.Requires(predef != null);
-
+
// set up the information used to verify the method's modifies clause
DefineFrame(m.tok, m.Mod, builder, localVariables, null);
}
@@ -1107,14 +1107,14 @@ namespace Microsoft.Dafny {
Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);
return CaptureState(tok, null);
}
-
+
void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables, string name){
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(frameClause));
Contract.Requires(builder != null);
Contract.Requires(cce.NonNullElements(localVariables));
Contract.Requires(predef != null);
-
+
ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);
// Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
Bpl.IdentifierExpr theFrame = etran.TheFrame(tok); // this is a throw-away expression, used only to extract the type of the $_Frame variable
@@ -1131,7 +1131,7 @@ namespace Microsoft.Dafny {
Bpl.Expr consequent = InRWClause(tok, o, f, frameClause, etran, null, null);
Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null,
Bpl.Expr.Imp(ante, consequent));
-
+
builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));
}
@@ -1162,7 +1162,7 @@ namespace Microsoft.Dafny {
Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame));
builder.Add(Assert(tok, q, errorMessage, kv));
}
-
+
/// <summary>
/// Generates:
/// axiom (forall h0: HeapType, h1: HeapType, formals... ::
@@ -1184,18 +1184,18 @@ namespace Microsoft.Dafny {
{
Contract.Requires(f != null);
Contract.Requires(sink != null && predef != null);
-
+
Bpl.BoundVariable h0Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h0", predef.HeapType));
Bpl.BoundVariable h1Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h1", predef.HeapType));
Bpl.Expr h0 = new Bpl.IdentifierExpr(f.tok, h0Var);
Bpl.Expr h1 = new Bpl.IdentifierExpr(f.tok, h1Var);
ExpressionTranslator etran0 = new ExpressionTranslator(this, predef, h0);
ExpressionTranslator etran1 = new ExpressionTranslator(this, predef, h1);
-
+
Bpl.Expr wellFormed = Bpl.Expr.And(
FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr),
FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran1.HeapExpr));
-
+
Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha");
Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
@@ -1204,12 +1204,12 @@ namespace Microsoft.Dafny {
Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));
Bpl.Expr unchanged = Bpl.Expr.Eq(ExpressionTranslator.ReadHeap(f.tok, h0, o, field), ExpressionTranslator.ReadHeap(f.tok, h1, o, field));
-
+
Bpl.Expr heapSucc = FunctionCall(f.tok, BuiltinFunction.HeapSucc, null, h0, h1);
Bpl.Expr r0 = InRWClause(f.tok, o, field, f.Reads, etran0, null, null);
Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),
Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));
-
+
// bvars: h0, h1, formals
// f0args: h0, formals
// f1args: h1, formals
@@ -1243,7 +1243,7 @@ namespace Microsoft.Dafny {
wh = GetWhereClause(p.tok, formal, p.Type, etran1);
if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
}
-
+
string axiomComment = "frame axiom for " + f.FullName;
Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
while (fn != null) {
@@ -1251,7 +1251,7 @@ namespace Microsoft.Dafny {
Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);
Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(heapSucc, F1));
-
+
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,
Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),
@@ -1265,7 +1265,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
Bpl.Expr/*!*/ InRWClause(IToken/*!*/ tok, Bpl.Expr/*!*/ o, Bpl.Expr/*!*/ f, List<FrameExpression/*!*/>/*!*/ rw, ExpressionTranslator/*!*/ etran,
Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap) {
Contract.Requires(tok != null);
@@ -1280,7 +1280,7 @@ namespace Microsoft.Dafny {
// requires o to denote an expression of type RefType
// "rw" is is allowed to contain a WildcardExpr
-
+
Bpl.Expr disjunction = null;
foreach (FrameExpression rwComponent in rw) {
Expression e = rwComponent.E;
@@ -1323,12 +1323,12 @@ namespace Microsoft.Dafny {
return disjunction;
}
}
-
+
void AddWellformednessCheck(Function f) {
Contract.Requires(f != null);
Contract.Requires(sink != null && predef != null);
Contract.Requires(f.EnclosingClass != null);
-
+
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
// parameters of the procedure
Bpl.VariableSeq inParams = new Bpl.VariableSeq();
@@ -1360,7 +1360,7 @@ namespace Microsoft.Dafny {
VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);
Bpl.VariableSeq locals = new Bpl.VariableSeq();
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
-
+
// check well-formedness of the preconditions (including termination, but no reads checks), and then
// assume each one of them
foreach (Expression p in f.Req) {
@@ -1466,7 +1466,7 @@ namespace Microsoft.Dafny {
Contract.Requires(expr != null);Contract.Requires(etran != null);
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
-
+
if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
return Bpl.Expr.True;
} else if (expr is DisplayExpression) {
@@ -1632,7 +1632,7 @@ namespace Microsoft.Dafny {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
}
-
+
Bpl.Expr/*!*/ IsTotal(List<Expression/*!*/>/*!*/ exprs, ExpressionTranslator/*!*/ etran) {
Contract.Requires(etran != null);
Contract.Requires(exprs != null);
@@ -1795,7 +1795,7 @@ namespace Microsoft.Dafny {
return Bpl.Expr.And(a, b);
}
}
-
+
Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
@@ -1807,14 +1807,14 @@ namespace Microsoft.Dafny {
return Bpl.Expr.Imp(a, b);
}
}
-
+
void CheckNonNull(IToken tok, Expression e, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Bpl.QKeyValue kv) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
Contract.Requires(builder != null);
Contract.Requires(etran != null);
Contract.Requires(predef != null);
-
+
if (e is ThisExpr) {
// already known to be non-null
} else {
@@ -1889,7 +1889,7 @@ namespace Microsoft.Dafny {
Contract.Requires(builder != null);
Contract.Requires(etran != null);
Contract.Requires(predef != null);
-
+
if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
// always allowed
} else if (expr is DisplayExpression) {
@@ -2136,7 +2136,7 @@ namespace Microsoft.Dafny {
CheckWellformed(e.Thn, options, locals, bThen, etran);
CheckWellformed(e.Els, options, locals, bElse, etran);
builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.Test), bThen.Collect(expr.tok), null, bElse.Collect(expr.tok)));
-
+
} else if (expr is MatchExpr) {
MatchExpr me = (MatchExpr)expr;
CheckWellformed(me.Source, options, locals, builder, etran);
@@ -2360,7 +2360,7 @@ namespace Microsoft.Dafny {
return s;
}
}
-
+
Bpl.Constant GetClass(TopLevelDecl cl)
{
Contract.Requires(cl != null);
@@ -2376,7 +2376,7 @@ namespace Microsoft.Dafny {
}
return cc;
}
-
+
Bpl.Expr GetTypeExpr(IToken tok, Type type)
{
Contract.Requires(tok != null);
@@ -2425,13 +2425,13 @@ namespace Microsoft.Dafny {
return t;
}
}
-
+
Bpl.Constant GetField(Field f)
{
Contract.Requires(f != null && f.IsMutable);
Contract.Requires(sink != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.Constant>() != null);
-
+
Bpl.Constant fc;
if (fields.TryGetValue(f, out fc)) {
Contract.Assert(fc != null);
@@ -2490,13 +2490,13 @@ namespace Microsoft.Dafny {
Contract.Requires(fse != null);
Contract.Requires(fse.Field != null && fse.Field.IsMutable);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
-
+
return new Bpl.IdentifierExpr(fse.tok, GetField(fse.Field));
}
/// <summary>
/// This method is expected to be called just once for each function in the program.
- /// </summary>
+ /// </summary>
void AddFunction(Function f)
{
Contract.Requires(f != null);
@@ -2513,7 +2513,7 @@ namespace Microsoft.Dafny {
Bpl.Formal res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false);
Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);
sink.TopLevelDeclarations.Add(func);
-
+
if (f.IsRecursive && !f.IsUnlimited) {
sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 0), args, res));
sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 2), args, res));
@@ -2523,12 +2523,12 @@ namespace Microsoft.Dafny {
Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullName + "#canCall", args, res);
sink.TopLevelDeclarations.Add(canCallF);
}
-
+
/// <summary>
/// This method is expected to be called just twice for each procedure in the program (once with
/// wellformednessProc set to true, once with wellformednessProc set to false).
/// In addition, it is used once to generate refinement conditions.
- /// </summary>
+ /// </summary>
Bpl.Procedure AddMethod(Method m, bool wellformednessProc, bool skipEnsures)
{
Contract.Requires(m != null);
@@ -2538,7 +2538,7 @@ namespace Microsoft.Dafny {
Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
-
+
Bpl.VariableSeq inParams = new Bpl.VariableSeq();
Bpl.VariableSeq outParams = new Bpl.VariableSeq();
if (!m.IsStatic) {
@@ -2558,7 +2558,7 @@ namespace Microsoft.Dafny {
Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));
}
-
+
Bpl.RequiresSeq req = new Bpl.RequiresSeq();
Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();
Bpl.EnsuresSeq ens = new Bpl.EnsuresSeq();
@@ -2569,7 +2569,7 @@ namespace Microsoft.Dafny {
req.Add(Requires(m.tok, true, context, null, null));
mod.Add(etran.HeapExpr);
mod.Add(etran.Tick());
-
+
if (!wellformednessProc) {
string comment = "user-defined preconditions";
foreach (MaybeFreeExpression p in m.Req) {
@@ -2607,54 +2607,54 @@ namespace Microsoft.Dafny {
return proc;
}
- #region Refinement extension
-
- void AddMethodRefinement(MethodRefinement m)
+ #region Refinement extension
+
+ void AddMethodRefinement(MethodRefinement m)
{
Contract.Requires(m != null);
Contract.Requires(sink != null && predef != null);
- // r is abstract, m is concrete
+ // r is abstract, m is concrete
Method r = m.Refined;
Contract.Assert(r != null);
Contract.Assert(m.EnclosingClass != null);
string name = "Refinement$$" + m.FullName;
string that = "that";
-
+
Bpl.IdentifierExpr heap = new Bpl.IdentifierExpr(m.tok, predef.HeapVarName, predef.HeapType);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, heap, that);
-
+
// TODO: this straight inlining does not handle recursive calls
- // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames
-
+ // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames
+
// generate procedure declaration with pre-condition wp(r, true)
Bpl.Procedure proc = AddMethod(r, false, true);
proc.Name = name;
-
+
// create "that" for m
Bpl.Expr wh = Bpl.Expr.And(
Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, that, predef.RefType), predef.Null),
etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, that, predef.RefType), Resolver.GetReceiverType(m.tok, m)));
Bpl.Formal thatVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, that, predef.RefType, wh), true);
proc.InParams.Add(thatVar);
-
- // add outs of m to the outs of the refinement procedure
+
+ // add outs of m to the outs of the refinement procedure
foreach (Formal p in m.Outs) {
Bpl.Type varType = TrType(p.Type);
Bpl.Expr w = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
proc.OutParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, w), false));
}
sink.TopLevelDeclarations.Add(proc);
-
- // generate procedure implementation:
+
+ // generate procedure implementation:
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
-
+
Contract.Assert(m.Body != null);
Contract.Assert(r.Body != null);
-
+
// declare a frame variable that allows anything to be changed (not checking modifies clauses)
Bpl.IdentifierExpr theFrame = etran.TheFrame(m.tok);
Contract.Assert(theFrame.Type != null);
@@ -2666,12 +2666,12 @@ namespace Microsoft.Dafny {
Bpl.BoundVariable fVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$f", predef.FieldName(m.tok, alpha)));
Bpl.Expr lambda = new Bpl.LambdaExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, Bpl.Expr.True);
builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));
-
- // assume I($Heap, $Heap)
+
+ // assume I($Heap, $Heap)
builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));
-
+
// assign input formals of m (except "this")
- for (int i = 0; i < m.Ins.Count; i++) {
+ for (int i = 0; i < m.Ins.Count; i++) {
Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName, TrType(m.Ins[i].Type)));
localVariables.Add(arg);
Bpl.Variable var = inParams[i+1];
@@ -2684,7 +2684,7 @@ namespace Microsoft.Dafny {
loopHeapVarCount = 0;
otherTmpVarCount = 0;
_tmpIEs.Clear();
-
+
// call inlined m;
TrStmt(m.Body, builder, localVariables, etran);
@@ -2692,10 +2692,10 @@ namespace Microsoft.Dafny {
Bpl.LocalVariable heap2 = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, heap.Name+"2", predef.HeapType));
localVariables.Add(heap2);
builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, heap2), etran.HeapExpr));
-
+
// $Heap := old($Heap);
builder.Add(Bpl.Cmd.SimpleAssign(m.tok, heap, new Bpl.OldExpr(m.tok, heap)));
-
+
// call inlined r;
currentMethod = r;
etran = new ExpressionTranslator(this, predef, heap);
@@ -2706,7 +2706,7 @@ namespace Microsoft.Dafny {
loopHeapVarCount = 0;
otherTmpVarCount = 0;
_tmpIEs.Clear();
-
+
// assert output variables of r and m are pairwise equal
Contract.Assert(outParams.Length % 2 == 0);
int k = outParams.Length / 2;
@@ -2714,21 +2714,21 @@ namespace Microsoft.Dafny {
Bpl.Variable rOut = outParams[i];
Bpl.Variable mOut = outParams[i+k];
Contract.Assert(rOut != null && mOut != null);
- builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)),
+ builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)),
"Refinement method may not produce the same value for output variable " + m.Outs[i].Name));
}
-
- // assert I($Heap1, $Heap)
+
+ // assert I($Heap1, $Heap)
builder.Add(Assert(m.tok, TrCouplingInvariant(m, heap, "this", new Bpl.IdentifierExpr(m.tok, heap2), that),
"Refinement method may not preserve the coupling invariant"));
-
+
Bpl.StmtList stmts = builder.Collect(m.tok);
Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
typeParams, inParams, outParams,
localVariables, stmts);
sink.TopLevelDeclarations.Add(impl);
}
-
+
private sealed class NominalSubstituter : Duplicator
{
private readonly Dictionary<string,Bpl.Expr> subst;
@@ -2742,7 +2742,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(cce.NonNullDictionaryAndValues(subst));
}
-
+
public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node)
{
Contract.Requires(node != null);
@@ -2750,7 +2750,7 @@ namespace Microsoft.Dafny {
if (subst.ContainsKey(node.Name))
return subst[node.Name];
- else
+ else
return base.VisitIdentifierExpr(node);
}
}
@@ -2767,32 +2767,32 @@ namespace Microsoft.Dafny {
ClassRefinementDecl c = m.EnclosingClass as ClassRefinementDecl;
Contract.Assert(c != null);
ExpressionTranslator etran = new ExpressionTranslator(this, predef, conHeap, conThis);
-
- foreach (MemberDecl d in c.Members)
+
+ foreach (MemberDecl d in c.Members)
if (d is CouplingInvariant) {
CouplingInvariant inv = (CouplingInvariant)d;
Contract.Assert(inv.Refined != null);
Contract.Assert(inv.Formals != null);
-
- // replace formals with field dereferences
+
+ // replace formals with field dereferences
Dictionary<string,Bpl.Expr> map = new Dictionary<string,Bpl.Expr>();
Bpl.Expr absVar = new Bpl.IdentifierExpr(d.tok, absThis, predef.RefType);
- for (int i = 0; i < inv.Refined.Count; i++) {
+ for (int i = 0; i < inv.Refined.Count; i++) {
// TODO: boxing/unboxing?
Bpl.Expr result = ExpressionTranslator.ReadHeap(inv.Toks[i], absHeap, absVar, new Bpl.IdentifierExpr(inv.Toks[i], GetField(cce.NonNull(inv.Refined[i]))));
map.Add(inv.Formals[i].UniqueName, result);
}
-
+
Bpl.Expr e = new NominalSubstituter(map).VisitExpr(etran.TrExpr(inv.Expr));
cond = Bpl.Expr.And(cond, e);
}
-
+
return cond;
}
-
+
#endregion
-
+
class BoilerplateTriple { // a triple that is now a quintuple
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -2820,7 +2820,7 @@ namespace Microsoft.Dafny {
Comment = comment;
}
}
-
+
/// <summary>
/// There are 3 states of interest when generating two-state boilerplate:
/// S0. the beginning of the method or loop, which is where the modifies clause is interpreted
@@ -2837,17 +2837,17 @@ namespace Microsoft.Dafny {
Contract.Ensures(cce.NonNullElements(Contract.Result<List<BoilerplateTriple>>()));
List<BoilerplateTriple> boilerplate = new List<BoilerplateTriple>();
-
+
// the frame condition, which is free since it is checked with every heap update and call
boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, etranPre, etran, etranMod), null, "frame condition"));
// HeapSucc(S1, S2)
Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);
boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate"));
-
+
return boilerplate;
}
-
+
/// <summary>
/// There are 3 states of interest when generating a frame condition:
/// S0. the beginning of the method/loop, which is where the modifies clause is interpreted
@@ -2879,9 +2879,9 @@ namespace Microsoft.Dafny {
Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);
Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranMod.IsAlloced(tok, o));
Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
-
+
consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etranMod, null, null));
-
+
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
}
@@ -2913,15 +2913,15 @@ namespace Microsoft.Dafny {
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
- }
+ }
// ----- Type ---------------------------------------------------------------------------------
-
+
Bpl.Type TrType(Type type)
{
Contract.Requires(type != null);
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result<Bpl.Type>() != null);
-
+
while (true) {
TypeProxy tp = type as TypeProxy;
if (tp == null) {
@@ -2933,7 +2933,7 @@ namespace Microsoft.Dafny {
type = tp.T;
}
}
-
+
if (type is BoolType) {
return Bpl.Type.Bool;
} else if (type is IntType) {
@@ -2955,7 +2955,7 @@ namespace Microsoft.Dafny {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
-
+
Bpl.TypeVariableSeq TrTypeParamDecls(List<TypeParameter/*!*/>/*!*/ tps)
{
Contract.Requires(cce.NonNullElements(tps));
@@ -2966,7 +2966,7 @@ namespace Microsoft.Dafny {
}
// ----- Statement ----------------------------------------------------------------------------
-
+
Bpl.AssertCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)
{
Contract.Requires(tok != null);
@@ -3036,10 +3036,10 @@ namespace Microsoft.Dafny {
Contract.Requires(etran != null);
Contract.Requires(currentMethod != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
-
+
return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);
}
-
+
Bpl.StmtList TrStmt2StmtList(Bpl.StmtListBuilder builder, Statement block, Bpl.VariableSeq locals, ExpressionTranslator etran)
{
Contract.Requires(builder != null);
@@ -3048,11 +3048,11 @@ namespace Microsoft.Dafny {
Contract.Requires(etran != null);
Contract.Requires(currentMethod != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
-
+
TrStmt(block, builder, locals, etran);
return builder.Collect(block.Tok); // TODO: would be nice to have an end-curly location for "block"
}
-
+
void TrStmt(Statement stmt, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran)
{
Contract.Requires(stmt != null);
@@ -3093,7 +3093,7 @@ namespace Microsoft.Dafny {
TrStmt_CheckWellformed(arg.E, builder, locals, etran, false);
}
}
-
+
} else if (stmt is BreakStmt) {
AddComment(builder, stmt, "break statement");
var s = (BreakStmt)stmt;
@@ -3316,7 +3316,7 @@ namespace Microsoft.Dafny {
Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);
builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined")); // totality check
}
-
+
// Here comes: assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));
Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
@@ -3350,14 +3350,14 @@ namespace Microsoft.Dafny {
qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
}
-
+
builder.Add(CaptureState(stmt.Tok));
-
+
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);
Bpl.Expr source = etran.TrExpr(s.Source);
-
+
var b = new Bpl.StmtListBuilder();
b.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));
Bpl.StmtList els = b.Collect(stmt.Tok);
@@ -3512,7 +3512,7 @@ namespace Microsoft.Dafny {
}
// add a free invariant which says that the heap hasn't changed outside of the modifies clause.
invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));
-
+
// include a free invariant that says that all completed iterations so far have only decreased the termination metric
if (initDecr != null) {
List<IToken> toks = new List<IToken>();
@@ -3669,7 +3669,7 @@ namespace Microsoft.Dafny {
Contract.Requires(builder != null);
Contract.Requires(locals != null);
Contract.Requires(etran != null);
-
+
Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver);
Bpl.ExprSeq ins = new Bpl.ExprSeq();
if (!method.IsStatic) {
@@ -3754,7 +3754,7 @@ namespace Microsoft.Dafny {
}
}
}
-
+
static Expression CreateIntLiteral(IToken tok, int n)
{
Contract.Requires(tok != null);
@@ -3768,13 +3768,13 @@ namespace Microsoft.Dafny {
return CreateIntSub(tok, CreateIntLiteral(tok, 0), CreateIntLiteral(tok, -n));
}
}
-
+
static Expression CreateIntSub(IToken tok, Expression e0, Expression e1)
{
Contract.Requires(tok != null);
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
-
+
Contract.Requires(e0.Type is IntType && e1.Type is IntType);
Contract.Ensures(Contract.Result<Expression>() != null);
@@ -3783,7 +3783,7 @@ namespace Microsoft.Dafny {
s.Type = Type.Int; // resolve here
return s;
}
-
+
static Expression CreateIntITE(IToken tok, Expression test, Expression e0, Expression e1)
{
Contract.Requires(tok != null);
@@ -3797,7 +3797,7 @@ namespace Microsoft.Dafny {
ite.Type = Type.Int; // resolve here
return ite;
}
-
+
public IEnumerable<Expression> Conjuncts(Expression expr)
{
Contract.Requires(expr != null);
@@ -3835,7 +3835,7 @@ namespace Microsoft.Dafny {
// record value of each decreases expression at beginning of the loop iteration
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(e.tok, bf, etran.TrExpr(e));
builder.Add(cmd);
-
+
c++;
}
return oldBfs;
@@ -3887,7 +3887,7 @@ namespace Microsoft.Dafny {
}
builder.Add(Assert(tok, decrExpr, inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure"));
}
-
+
/// <summary>
/// Returns the expression that says whether or not the decreases function has gone down (if !allowNoChange)
/// or has gone down or stayed the same (if allowNoChange).
@@ -3908,7 +3908,7 @@ namespace Microsoft.Dafny {
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
int N = types.Count;
-
+
// compute eq and less for each component of the lexicographic pair
List<Bpl.Expr> Eq = new List<Bpl.Expr>(N);
List<Bpl.Expr> Less = new List<Bpl.Expr>(N);
@@ -3975,7 +3975,7 @@ namespace Microsoft.Dafny {
return false; // don't consider any type parameters to be the same (since we have no comparison function for them anyway)
}
}
-
+
void ComputeLessEq(IToken/*!*/ tok, Type/*!*/ ty, Bpl.Expr/*!*/ e0, Bpl.Expr/*!*/ e1, out Bpl.Expr/*!*/ less, out Bpl.Expr/*!*/ atmost, out Bpl.Expr/*!*/ eq,
ExpressionTranslator/*!*/ etran, bool includeLowerBound)
{
@@ -3988,7 +3988,7 @@ namespace Microsoft.Dafny {
Contract.Ensures(Contract.ValueAtReturn(out less)!=null);
Contract.Ensures(Contract.ValueAtReturn(out atmost)!=null);
Contract.Ensures(Contract.ValueAtReturn(out eq)!=null);
-
+
if (ty is BoolType) {
eq = Bpl.Expr.Iff(e0, e1);
less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
@@ -4017,7 +4017,7 @@ namespace Microsoft.Dafny {
eq = Bpl.Expr.Eq(b0, b1);
less = Bpl.Expr.Lt(b0, b1);
atmost = Bpl.Expr.Le(b0, b1);
-
+
} else {
// reference type
Bpl.Expr b0 = Bpl.Expr.Neq(e0, predef.Null);
@@ -4027,14 +4027,14 @@ namespace Microsoft.Dafny {
atmost = Bpl.Expr.Imp(b0, b1);
}
}
-
+
void AddComment(Bpl.StmtListBuilder builder, Statement stmt, string comment) {
Contract.Requires(builder != null);
Contract.Requires(stmt != null);
Contract.Requires(comment != null);
builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));
- }
-
+ }
+
Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran)
{
Contract.Requires(tok != null);
@@ -4063,7 +4063,7 @@ namespace Microsoft.Dafny {
} else if (type is BoolType || type is IntType) {
// nothing todo
-
+
} else if (type is SetType) {
SetType st = (SetType)type;
// (forall t: BoxType :: { x[t] } x[t] ==> Unbox(t)-has-the-expected-type)
@@ -4131,7 +4131,7 @@ namespace Microsoft.Dafny {
} else if (type.IsTypeParameter) {
return FunctionCall(tok, BuiltinFunction.GenericAlloc, null, x, etran.HeapExpr);
-
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
@@ -4322,7 +4322,7 @@ namespace Microsoft.Dafny {
var obj = SaveInTemp(etran.TrExpr(mse.Array), rhsCanAffectPreviouslyKnownExpressions,
"$obj" + i, predef.RefType, builder, locals);
- var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions,
+ var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions,
"$index" + i, predef.FieldName(mse.tok, predef.BoxType), builder, locals);
prevObj[i] = obj;
prevIndex[i] = fieldName;
@@ -4512,7 +4512,7 @@ namespace Microsoft.Dafny {
readonly int layerOffset = 0;
public int Statistics_FunctionCount = 0;
[ContractInvariantMethod]
- void ObjectInvariant()
+ void ObjectInvariant()
{
Contract.Invariant(HeapExpr != null);
Contract.Invariant(predef != null);
@@ -4531,7 +4531,7 @@ namespace Microsoft.Dafny {
this.HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);
this.This = "this";
}
-
+
public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap) {
Contract.Requires(translator != null);
Contract.Requires(predef != null);
@@ -4541,7 +4541,7 @@ namespace Microsoft.Dafny {
this.HeapExpr = heap;
this.This = "this";
}
-
+
public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar) {
Contract.Requires(translator != null);
Contract.Requires(predef != null);
@@ -4599,7 +4599,7 @@ namespace Microsoft.Dafny {
return HeapExpr is Bpl.OldExpr;
}
}
-
+
public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction) {
Contract.Requires(applyLimited_CurrentFunction != null);
Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
@@ -4674,10 +4674,10 @@ namespace Microsoft.Dafny {
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal
}
-
+
} else if (expr is ThisExpr) {
return new Bpl.IdentifierExpr(expr.tok, This, predef.RefType);
-
+
} else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
return TrVar(expr.tok, cce.NonNull(e.Var));
@@ -4714,7 +4714,7 @@ namespace Microsoft.Dafny {
i++;
}
return s;
-
+
} else if (expr is FieldSelectExpr) {
FieldSelectExpr e = (FieldSelectExpr)expr;
Contract.Assert(e.Field != null);
@@ -4766,7 +4766,7 @@ namespace Microsoft.Dafny {
// if e0 == null && e1 == null, then we have the identity operation seq[..] == seq;
return seq;
}
-
+
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
Bpl.Expr seq = TrExpr(e.Seq);
@@ -4804,7 +4804,7 @@ namespace Microsoft.Dafny {
Bpl.ExprSeq args = FunctionInvocationArguments(e);
Bpl.Expr result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(id), args);
return CondApplyUnbox(expr.tok, result, e.Function.ResultType, expr.Type);
-
+
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved
@@ -4890,7 +4890,7 @@ namespace Microsoft.Dafny {
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression
}
-
+
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
Bpl.Expr e0 = TrExpr(e.E0);
@@ -4916,12 +4916,12 @@ namespace Microsoft.Dafny {
bOpcode = BinaryOperator.Opcode.And; break;
case BinaryExpr.ResolvedOpcode.Or:
bOpcode = BinaryOperator.Opcode.Or; break;
-
+
case BinaryExpr.ResolvedOpcode.EqCommon:
bOpcode = BinaryOperator.Opcode.Eq; break;
case BinaryExpr.ResolvedOpcode.NeqCommon:
bOpcode = BinaryOperator.Opcode.Neq; break;
-
+
case BinaryExpr.ResolvedOpcode.Lt:
bOpcode = BinaryOperator.Opcode.Lt; break;
case BinaryExpr.ResolvedOpcode.Le:
@@ -5031,12 +5031,12 @@ namespace Microsoft.Dafny {
return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Gt,
translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e0),
translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e1));
-
+
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected binary expression
}
return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);
-
+
} else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
@@ -5055,7 +5055,7 @@ namespace Microsoft.Dafny {
antecedent = Bpl.Expr.And(antecedent, TrExpr(e.Range));
}
Bpl.Expr body = TrExpr(e.Term);
-
+
if (e is ForallExpr) {
return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(antecedent, body));
} else {
@@ -5094,11 +5094,11 @@ namespace Microsoft.Dafny {
} else if (expr is BoxingCastExpr) {
BoxingCastExpr e = (BoxingCastExpr)expr;
return CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
-
+
} else if (expr is UnboxingCastExpr) {
UnboxingCastExpr e = (UnboxingCastExpr)expr;
return CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
-
+
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
@@ -5107,7 +5107,7 @@ namespace Microsoft.Dafny {
public Bpl.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, Bpl.VariableSeq bvars) {
Contract.Requires(boundVars != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
-
+
Bpl.Expr typeAntecedent = Bpl.Expr.True;
foreach (BoundVar bv in boundVars) {
Bpl.Variable bvar = new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type)));
@@ -5186,7 +5186,7 @@ namespace Microsoft.Dafny {
return e;
}
}
-
+
public Bpl.Expr BoxIfNecessary(IToken tok, Bpl.Expr e, Type fromType) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
@@ -5195,7 +5195,7 @@ namespace Microsoft.Dafny {
return CondApplyBox(tok, e, fromType, null);
}
-
+
public Bpl.Expr CondApplyUnbox(IToken tok, Bpl.Expr e, Type fromType, Type toType) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
@@ -5209,7 +5209,7 @@ namespace Microsoft.Dafny {
return e;
}
}
-
+
public static bool ModeledAsBoxType(Type t) {
Contract.Requires(t != null);
while (true) {
@@ -5371,7 +5371,7 @@ namespace Microsoft.Dafny {
}
return kv;
}
-
+
// --------------- help routines ---------------
public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e) {
@@ -5381,7 +5381,7 @@ namespace Microsoft.Dafny {
return IsAlloced(tok, e, HeapExpr);
}
-
+
Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e, Bpl.Expr heap) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
@@ -5390,7 +5390,7 @@ namespace Microsoft.Dafny {
return ReadHeap(tok, heap, e, predef.Alloc(tok));
}
-
+
public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
@@ -5405,7 +5405,7 @@ namespace Microsoft.Dafny {
return IsAlloced(tok, e);
}
}
-
+
public Bpl.Expr GoodRef_Class(IToken tok, Bpl.Expr e, UserDefinedType type, bool isNew)
{
Contract.Requires(tok != null);
@@ -5427,12 +5427,12 @@ namespace Microsoft.Dafny {
if (isNew) {
r = Bpl.Expr.Not(r); // use the conjunct: !Heap[e, alloc]
}
-
+
// dtype(e) == C
Bpl.Expr dtypeFunc = translator.FunctionCall(tok, BuiltinFunction.DynamicType, null, e);
Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, type);
r = r == null ? dtype : Bpl.Expr.And(r, dtype);
-
+
// TypeParams(e, #) == T
int n = 0;
foreach (Type arg in typeArgs) {
@@ -5443,7 +5443,7 @@ namespace Microsoft.Dafny {
}
n++;
}
-
+
return r;
}
@@ -5471,7 +5471,7 @@ namespace Microsoft.Dafny {
return r;
}
}
-
+
enum BuiltinFunction {
SetEmpty,
SetUnionOne,
@@ -5507,17 +5507,17 @@ namespace Microsoft.Dafny {
SeqEqual,
SeqSameUntil,
SeqFromArray,
-
+
IndexField,
MultiIndexField,
-
+
Box,
Unbox,
IsCanonicalBoolBox,
IsGoodHeap,
HeapSucc,
-
+
DynamicType, // allocated type (of object reference)
DtType, // type of datatype value
TypeParams, // type parameters of allocated type
@@ -5532,7 +5532,7 @@ namespace Microsoft.Dafny {
GenericAlloc,
}
-
+
// The "typeInstantiation" argument is passed in to help construct the result type of the function.
Bpl.NAryExpr FunctionCall(IToken tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[] args)
{
@@ -5684,7 +5684,7 @@ namespace Microsoft.Dafny {
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#FromArray", typeInstantiation, args);
-
+
case BuiltinFunction.IndexField:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
@@ -5767,7 +5767,7 @@ namespace Microsoft.Dafny {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected built-in function
}
}
-
+
Bpl.NAryExpr FunctionCall(IToken tok, string function, Bpl.Type returnType, params Bpl.Expr[] args)
{
Contract.Requires(tok != null);
@@ -6238,7 +6238,7 @@ namespace Microsoft.Dafny {
for (int i = 0; i < dt.TypeArgs.Count; i++) {
subst.Add(dt.TypeArgs[i], instantiatedType.TypeArgs[i]);
}
-
+
foreach (DatatypeCtor ctor in dt.Ctors) {
Bpl.VariableSeq bvs;
List<Bpl.Expr> args;
@@ -6293,7 +6293,7 @@ namespace Microsoft.Dafny {
newExpr = new SeqDisplayExpr(expr.tok, newElements);
}
}
-
+
} else if (expr is FieldSelectExpr) {
FieldSelectExpr fse = (FieldSelectExpr)expr;
Expression substE = Substitute(fse.Obj, receiverReplacement, substMap);
@@ -6302,7 +6302,7 @@ namespace Microsoft.Dafny {
fseNew.Field = fse.Field; // resolve on the fly (and fseExpr.Type is set at end of method)
newExpr = fseNew;
}
-
+
} else if (expr is SeqSelectExpr) {
SeqSelectExpr sse = (SeqSelectExpr)expr;
Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);
@@ -6311,7 +6311,7 @@ namespace Microsoft.Dafny {
if (seq != sse.Seq || e0 != sse.E0 || e1 != sse.E1) {
newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);
}
-
+
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr sse = (SeqUpdateExpr)expr;
Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);
@@ -6338,7 +6338,7 @@ namespace Microsoft.Dafny {
newFce.Function = e.Function; // resolve on the fly (and set newFce.Type below, at end)
newExpr = newFce;
}
-
+
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
List<Expression> newArgs = SubstituteExprList(dtv.Arguments, receiverReplacement, substMap);
@@ -6381,7 +6381,7 @@ namespace Microsoft.Dafny {
newBin.ResolvedOp = e.ResolvedOp; // part of what needs to be done to resolve on the fly (newBin.Type is set below, at end)
newExpr = newBin;
}
-
+
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);
@@ -6404,7 +6404,7 @@ namespace Microsoft.Dafny {
} else {
Contract.Assume(false); // unexpected ComprehensionExpr
}
-
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
Expression test = Substitute(e.Test, receiverReplacement, substMap);
@@ -6418,7 +6418,7 @@ namespace Microsoft.Dafny {
var e = (ConcreteSyntaxExpression)expr;
return Substitute(e.ResolvedExpression, receiverReplacement, substMap);
}
-
+
if (newExpr == null) {
return expr;
} else {
@@ -6426,18 +6426,18 @@ namespace Microsoft.Dafny {
return newExpr;
}
}
-
+
static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,
Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(cce.NonNullElements(elist));
Contract.Requires((receiverReplacement == null) == (substMap == null));
Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));
-
+
List<Expression> newElist = null; // initialized lazily
for (int i = 0; i < elist.Count; i++)
{cce.LoopInvariant( newElist == null || newElist.Count == i);
-
+
Expression substE = Substitute(elist[i], receiverReplacement, substMap);
if (substE != elist[i] && newElist == null) {
newElist = new List<Expression>();
@@ -6455,7 +6455,7 @@ namespace Microsoft.Dafny {
return newElist;
}
}
-
+
static Triggers SubstTriggers(Triggers trigs, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
if (trigs != null) {
@@ -6487,7 +6487,7 @@ namespace Microsoft.Dafny {
if (!anyArgSubst) {
newArgs = attrs.Args;
}
-
+
Attributes prev = SubstAttributes(attrs.Prev, receiverReplacement, substMap);
if (newArgs != attrs.Args || prev != attrs.Prev) {
return new Attributes(attrs.Name, newArgs, prev);
@@ -6495,6 +6495,6 @@ namespace Microsoft.Dafny {
}
return attrs;
}
-
+
}
-} \ No newline at end of file
+}