diff options
author | 2011-05-24 22:43:11 -0700 | |
---|---|---|
committer | 2011-05-24 22:43:11 -0700 | |
commit | f7877ab8f223dcf3ea37ddc8a0b588316eb451a5 (patch) | |
tree | 27566eb79aa955d2fa89cb57f800370c20ff12e4 /Source/Dafny/DafnyAst.cs | |
parent | f205409381a6e13beb4d5e9d88dfb31a67500116 (diff) |
Dafny: changed local "var" introductions to use new VarDeclStmt instead of parsing as the old VarDecl's with RHS's
To-do: automatically make some variables introduce ghost variables, depending on RHS of initial assignment
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 49 |
1 files changed, 32 insertions, 17 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 1f46d5ba..47a3198c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1417,6 +1417,25 @@ namespace Microsoft.Dafny { }
}
+ public class VarDeclStmt : ConcreteSyntaxStatement
+ {
+ public readonly List<VarDecl> Lhss;
+ public readonly UpdateStmt Update;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(Lhss));
+ }
+
+ public VarDeclStmt(IToken tok, List<VarDecl> lhss, UpdateStmt update)
+ : base(tok)
+ {
+ Contract.Requires(lhss != null);
+
+ Lhss = lhss;
+ Update = update;
+ }
+ }
+
public class UpdateStmt : ConcreteSyntaxStatement
{
public readonly List<Expression> Lhss;
@@ -1496,7 +1515,18 @@ namespace Microsoft.Dafny { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(name != null);
- Contract.Invariant(OptionalType != null || Rhs != null);
+ Contract.Invariant(OptionalType != null);
+ }
+
+ public VarDecl(IToken tok, string name, Type type, bool isGhost)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(type != null); // can be a proxy, though
+
+ this.name = name;
+ this.OptionalType = type;
+ this.IsGhost = isGhost;
}
public string/*!*/ Name {
@@ -1543,27 +1573,12 @@ namespace Microsoft.Dafny { return base.IsGhost;
}
}
-
- public readonly DeterminedAssignmentRhs Rhs;
-
- public VarDecl(IToken tok, string name, Type type, bool isGhost, DeterminedAssignmentRhs rhs)
- : base(tok) {
- Contract.Requires(tok != null);
- Contract.Requires(name != null);
- Contract.Requires(type != null || rhs != null);
-
- this.name = name;
- this.OptionalType = type;
- this.IsGhost = isGhost;
- this.Rhs = rhs;
-
- }
}
public class AutoVarDecl : VarDecl {
public readonly int Index;
public AutoVarDecl(IToken tok, string name, Type type, int index)
- : base(tok, name, type, false, null) {
+ : base(tok, name, type, false) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Index = index;
|