diff options
| -rw-r--r-- | Source/Dafny/Cloner.cs | 7 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 14 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 48 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 21 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 66 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 31 | ||||
| -rw-r--r-- | Test/dafny4/NumberRepresentations.dfy | 2 |
7 files changed, 75 insertions, 114 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 97e88e3d..385bfd78 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -438,10 +438,6 @@ namespace Microsoft.Dafny var s = (AssignStmt)stmt;
r = new AssignStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Lhs), CloneRHS(s.Rhs));
- } else if (stmt is VarDecl) {
- var s = (VarDecl)stmt;
- r = new VarDecl(Tok(s.Tok), Tok(s.EndTok), s.Name, CloneType(s.OptionalType), s.IsGhost);
-
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
r = new CallStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhs.ConvertAll(CloneExpr), CloneExpr(s.Receiver), s.MethodName, s.Args.ConvertAll(CloneExpr));
@@ -488,7 +484,8 @@ namespace Microsoft.Dafny } else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
- r = new VarDeclStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhss.ConvertAll(c => (VarDecl)CloneStmt(c)), (ConcreteUpdateStatement)CloneStmt(s.Update));
+ var lhss = s.Lhss.ConvertAll(c => new VarDecl(Tok(c.Tok), Tok(c.EndTok), c.Name, CloneType(c.OptionalType), c.IsGhost));
+ r = new VarDeclStmt(Tok(s.Tok), Tok(s.EndTok), lhss, (ConcreteUpdateStatement)CloneStmt(s.Update));
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 4b57b1a4..97c21a89 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1237,9 +1237,6 @@ namespace Microsoft.Dafny { wr.WriteLine("{0}: ;", doneLabel);
}
- } else if (stmt is VarDecl) {
- TrVarDecl((VarDecl)stmt, true, indent);
-
} else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
TrCallStmt(s, null, indent);
@@ -1557,10 +1554,13 @@ namespace Microsoft.Dafny { Indent(indent); wr.WriteLine("}");
}
- } else if (stmt is ConcreteSyntaxStatement) {
- var s = (ConcreteSyntaxStatement)stmt;
- foreach (var ss in s.ResolvedStatements) {
- TrStmt(ss, indent);
+ } else if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ foreach (var lhs in s.Lhss) {
+ TrVarDecl(lhs, true, indent);
+ }
+ if (s.Update != null) {
+ TrStmt(s.Update, indent);
}
} else {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 2682938e..47059763 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2374,10 +2374,6 @@ namespace Microsoft.Dafny { }
}
- public bool HasAttributes() {
- return Attributes != null;
- }
-
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Tok != null);
@@ -2834,21 +2830,7 @@ namespace Microsoft.Dafny { public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }
}
- public abstract class ConcreteSyntaxStatement : Statement
- {
- public List<Statement> ResolvedStatements = new List<Statement>(); // contents filled in during resolution
- public ConcreteSyntaxStatement(IToken tok, IToken endTok)
- : base(tok, endTok) {
- Contract.Requires(tok != null);
- Contract.Requires(endTok != null);
- }
-
- public override IEnumerable<Statement> SubStatements {
- get { return ResolvedStatements; }
- }
- }
-
- public class VarDeclStmt : ConcreteSyntaxStatement
+ public class VarDeclStmt : Statement
{
public readonly List<VarDecl> Lhss;
public readonly ConcreteUpdateStatement Update;
@@ -2867,6 +2849,10 @@ namespace Microsoft.Dafny { Lhss = lhss;
Update = update;
}
+
+ public override IEnumerable<Statement> SubStatements {
+ get { if (Update != null) { yield return Update; } }
+ }
}
/// <summary>
@@ -3020,21 +3006,26 @@ namespace Microsoft.Dafny { }
}
- public class VarDecl : Statement, IVariable {
+ public class VarDecl : /*Statement,*/ IVariable {
+ public readonly IToken Tok;
+ public readonly IToken EndTok; // typically a terminating semi-colon or end-curly-brace
readonly string name;
+ public Attributes Attributes;
+ public bool IsGhost;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(name != null);
Contract.Invariant(OptionalType != null);
}
- public VarDecl(IToken tok, IToken endTok, string name, Type type, bool isGhost)
- : base(tok, endTok) {
+ public VarDecl(IToken tok, IToken endTok, string name, Type type, bool isGhost) {
Contract.Requires(tok != null);
Contract.Requires(endTok != null);
Contract.Requires(name != null);
Contract.Requires(type != null); // can be a proxy, though
+ this.Tok = tok;
+ this.EndTok = endTok;
this.name = name;
this.OptionalType = type;
this.IsGhost = isGhost;
@@ -3106,14 +3097,14 @@ namespace Microsoft.Dafny { }
bool IVariable.IsGhost {
get {
- return base.IsGhost;
+ return this.IsGhost;
}
}
/// <summary>
/// This method retrospectively makes the VarDecl a ghost. It is to be used only during resolution.
/// </summary>
public void MakeGhost() {
- base.IsGhost = true;
+ this.IsGhost = true;
}
IToken IVariable.Tok {
get {
@@ -3468,20 +3459,17 @@ namespace Microsoft.Dafny { var block = s as BlockStmt;
if (block != null && block.Body.Count == 1) {
s = block.Body[0];
+ // dig further into s
} else if (s is UpdateStmt) {
var update = (UpdateStmt)s;
if (update.ResolvedStatements.Count == 1) {
s = update.ResolvedStatements[0];
+ // dig further into s
} else {
return s;
}
} else {
- var conc = s as ConcreteSyntaxStatement;
- if (conc != null && conc.ResolvedStatements.Count == 1) {
- s = conc.ResolvedStatements[0];
- } else {
- return s;
- }
+ return s;
}
}
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index a5057286..b370b507 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -607,7 +607,7 @@ namespace Microsoft.Dafny { if (stmt is PredicateStmt) {
Expression expr = ((PredicateStmt)stmt).Expr;
wr.Write(stmt is AssertStmt ? "assert" : "assume");
- if (stmt.HasAttributes()) {
+ if (stmt.Attributes != null) {
PrintAttributes(stmt.Attributes);
}
wr.Write(" ");
@@ -653,20 +653,6 @@ namespace Microsoft.Dafny { PrintRhs(s.Rhs);
wr.Write(";");
- } else if (stmt is VarDecl) {
- VarDecl s = (VarDecl)stmt;
- if (s.IsGhost) {
- wr.Write("ghost ");
- }
- wr.Write("var");
- if (s.HasAttributes())
- {
- PrintAttributes(s.Attributes);
- }
- wr.Write(" {0}", s.DisplayName);
- PrintType(": ", s.OptionalType);
- wr.Write(";");
-
} else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
if (s.Lhs.Count != 0) {
@@ -821,15 +807,14 @@ namespace Microsoft.Dafny { } else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
- if (s.Lhss[0].IsGhost) {
+ if (s.Lhss.Exists(v => v.IsGhost)) {
wr.Write("ghost ");
}
wr.Write("var");
string sep = "";
foreach (var lhs in s.Lhss) {
wr.Write(sep);
- if (lhs.HasAttributes())
- {
+ if (lhs.Attributes != null) {
PrintAttributes(lhs.Attributes);
}
wr.Write(" {0}", lhs.DisplayName);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 3c4dfb55..c551e91f 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1871,9 +1871,11 @@ namespace Microsoft.Dafny Contract.Requires(resolver != null);
}
protected override void VisitOneStmt(Statement stmt) {
- if (stmt is VarDecl) {
- var s = (VarDecl)stmt;
- CheckTypeIsDetermined(s.Tok, s.Type, "local variable");
+ if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ foreach (var lhs in s.Lhss) {
+ CheckTypeIsDetermined(lhs.Tok, lhs.Type, "local variable");
+ }
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));
@@ -1977,7 +1979,6 @@ namespace Microsoft.Dafny return CheckTailRecursive(s.hiddenUpdate, enclosingMethod, ref tailCall, reportErrors);
}
} else if (stmt is AssignStmt) {
- } else if (stmt is VarDecl) {
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
if (s.Method == enclosingMethod) {
@@ -2078,9 +2079,11 @@ namespace Microsoft.Dafny } else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
return CheckTailRecursive(s.ResolvedStatements, enclosingMethod, ref tailCall, reportErrors);
- } else if (stmt is ConcreteSyntaxStatement) {
- var s = (ConcreteSyntaxStatement)stmt;
- return CheckTailRecursive(s.ResolvedStatements, enclosingMethod, ref tailCall, reportErrors);
+ } else if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ if (s.Update != null) {
+ return CheckTailRecursive(s.Update, enclosingMethod, ref tailCall, reportErrors);
+ }
} else {
Contract.Assert(false); // unexpected statement type
}
@@ -4055,13 +4058,20 @@ namespace Microsoft.Dafny ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
- foreach (var vd in s.Lhss) {
- ResolveStatement(vd, specContextOnly, codeContext);
- s.ResolvedStatements.Add(vd);
+ foreach (var v in s.Lhss) {
+ ResolveType(v.Tok, v.OptionalType, ResolveTypeOption.InferTypeProxies, null);
+ v.type = v.OptionalType;
+ // now that the declaration has been processed, add the name to the scope
+ if (!scope.Push(v.Name, v)) {
+ Error(v.Tok, "Duplicate local-variable name: {0}", v.Name);
+ }
+ if (specContextOnly) {
+ // a local variable in a specification-only context might as well be ghost
+ v.IsGhost = true;
+ }
}
if (s.Update != null) {
- ResolveStatement(s.Update, specContextOnly, codeContext);
- s.ResolvedStatements.Add(s.Update);
+ ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);
}
if (!s.IsGhost) {
s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Lhss.All(v => v.IsGhost);
@@ -4168,18 +4178,6 @@ namespace Microsoft.Dafny } else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS
}
- } else if (stmt is VarDecl) {
- var s = (VarDecl)stmt;
- ResolveType(stmt.Tok, s.OptionalType, ResolveTypeOption.InferTypeProxies, null);
- s.type = s.OptionalType;
- // now that the declaration has been processed, add the name to the scope
- if (!scope.Push(s.Name, s)) {
- Error(s, "Duplicate local-variable name: {0}", s.Name);
- }
- if (specContextOnly) {
- // 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;
@@ -5036,10 +5034,10 @@ namespace Microsoft.Dafny foreach (var ss in s.ResolvedStatements) {
CheckForallStatementBodyRestrictions(ss, kind);
}
- } else if (stmt is ConcreteSyntaxStatement) {
- var s = (ConcreteSyntaxStatement)stmt;
- foreach (var ss in s.ResolvedStatements) {
- CheckForallStatementBodyRestrictions(ss, kind);
+ } else if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ if (s.Update != null) {
+ CheckForallStatementBodyRestrictions(s.Update, kind);
}
} else if (stmt is AssignStmt) {
var s = (AssignStmt)stmt;
@@ -5052,8 +5050,6 @@ namespace Microsoft.Dafny Error(rhs.Tok, "new allocation not allowed in ghost context");
}
}
- } else if (stmt is VarDecl) {
- // cool
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
foreach (var lhs in s.Lhs) {
@@ -5179,8 +5175,6 @@ namespace Microsoft.Dafny } else if (stmt is AssignStmt) {
var s = (AssignStmt)stmt;
CheckHintLhs(s.Tok, s.Lhs.Resolved);
- } else if (stmt is VarDecl) {
- // cool
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
if (s.Method.Mod.Expressions.Count != 0) {
@@ -5191,10 +5185,10 @@ namespace Microsoft.Dafny foreach (var ss in s.ResolvedStatements) {
CheckHintRestrictions(ss);
}
- } else if (stmt is ConcreteSyntaxStatement) {
- var s = (ConcreteSyntaxStatement)stmt;
- foreach (var ss in s.ResolvedStatements) {
- CheckHintRestrictions(ss);
+ } else if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ if (s.Update != null) {
+ CheckHintRestrictions(s.Update);
}
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index c6c82193..0fee723a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5158,14 +5158,6 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "assignment statement");
AssignStmt s = (AssignStmt)stmt;
TrAssignment(stmt, s.Lhs.Resolved, s.Rhs, builder, locals, etran);
- } else if (stmt is VarDecl) {
- AddComment(builder, stmt, "var-declaration statement");
- VarDecl s = (VarDecl)stmt;
- Bpl.Type varType = TrType(s.Type);
- Bpl.Expr wh = GetWhereClause(stmt.Tok, new Bpl.IdentifierExpr(stmt.Tok, s.AssignUniqueName(currentDeclaration), varType), s.Type, etran);
- Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.AssignUniqueName(currentDeclaration), varType, wh));
- var.Attributes = etran.TrAttributes(s.Attributes, null);;
- locals.Add(var);
} else if (stmt is CallStmt) {
AddComment(builder, stmt, "call statement");
@@ -5415,9 +5407,18 @@ namespace Microsoft.Dafny { Contract.Assert(ifCmd != null); // follows from the fact that s.Cases.Count + s.MissingCases.Count != 0.
builder.Add(ifCmd);
- } else if (stmt is ConcreteSyntaxStatement) {
- var s = (ConcreteSyntaxStatement)stmt;
- TrStmtList(s.ResolvedStatements, builder, locals, etran);
+ } else if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ foreach (var lhs in s.Lhss) {
+ Bpl.Type varType = TrType(lhs.Type);
+ Bpl.Expr wh = GetWhereClause(lhs.Tok, new Bpl.IdentifierExpr(lhs.Tok, lhs.AssignUniqueName(currentDeclaration), varType), lhs.Type, etran);
+ Bpl.LocalVariable var = new Bpl.LocalVariable(lhs.Tok, new Bpl.TypedIdent(lhs.Tok, lhs.AssignUniqueName(currentDeclaration), varType, wh));
+ var.Attributes = etran.TrAttributes(lhs.Attributes, null); ;
+ locals.Add(var);
+ }
+ if (s.Update != null) {
+ TrStmt(s.Update, builder, locals, etran);
+ }
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
@@ -10829,10 +10830,6 @@ namespace Microsoft.Dafny { } else if (stmt is AssignStmt) {
var s = (AssignStmt)stmt;
r = new AssignStmt(s.Tok, s.EndTok, Substitute(s.Lhs), SubstRHS(s.Rhs));
- } else if (stmt is VarDecl) {
- var s = (VarDecl)stmt;
- var tt = s.OptionalType == null ? null : Resolver.SubstType(s.OptionalType, typeMap);
- r = new VarDecl(s.Tok, s.EndTok, s.Name, tt, s.IsGhost);
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
var rr = new CallStmt(s.Tok, s.EndTok, s.Lhs.ConvertAll(Substitute), Substitute(s.Receiver), s.MethodName, s.Args.ConvertAll(Substitute));
@@ -10892,8 +10889,8 @@ namespace Microsoft.Dafny { r = rr;
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
- var rr = new VarDeclStmt(s.Tok, s.EndTok, s.Lhss.ConvertAll(c => (VarDecl)SubstStmt(c)), (ConcreteUpdateStatement)SubstStmt(s.Update));
- rr.ResolvedStatements.AddRange(s.ResolvedStatements.ConvertAll(SubstStmt));
+ var lhss = s.Lhss.ConvertAll(c => new VarDecl(c.Tok, c.EndTok, c.Name, c.OptionalType == null ? null : Resolver.SubstType(c.OptionalType, typeMap), c.IsGhost));
+ var rr = new VarDeclStmt(s.Tok, s.EndTok, lhss, (ConcreteUpdateStatement)SubstStmt(s.Update));
r = rr;
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 2f31c006..b8c261d7 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -77,7 +77,7 @@ lemma CompleteNat(n: nat, base: nat) returns (digits: seq<int>) base * n <= n;
(base - 1) * n + n <= n;
(base - 1) * n <= 0;
- ==> { MulSign(base - 1, n); }
+ ==> { assert (base - 1) * n <= 0; MulSign(base - 1, n); }
(base - 1) <= 0 || n <= 0;
{ assert 0 < n; }
(base - 1) <= 0;
|