From a46696a3648bb71662026a073f68ab52adf59e01 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 16 Jan 2012 14:36:39 -0800
Subject: Dafny: Recheck specifications that contain refined (extended)
 predicates, even if they are contained inside a split expression.
 Superposition is thought to be sound.

---
 Source/Dafny/DafnyAst.cs | 57 ++++++++++++++++++++++++++++++------------------
 1 file changed, 36 insertions(+), 21 deletions(-)

(limited to 'Source/Dafny/DafnyAst.cs')

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index e8fe2780..35829a15 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1098,11 +1098,14 @@ namespace Microsoft.Dafny {
 
   public class Predicate : Function
   {
+    public readonly bool BodyIsExtended;  // says that this predicate definition is a refinement extension of a predicate definition is a refining module
     public Predicate(IToken tok, string name, bool isStatic, bool isGhost, bool isUnlimited,
                      List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,
                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
-                     Expression body, Attributes attributes)
+                     Expression body, bool bodyIsExtended, Attributes attributes)
       : base(tok, name, isStatic, isGhost, isUnlimited, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes) {
+      Contract.Requires(!bodyIsExtended || body != null);
+      BodyIsExtended = bodyIsExtended;
     }
   }
 
@@ -1908,44 +1911,56 @@ namespace Microsoft.Dafny {
 
   // ------------------------------------------------------------------------------------------------------
 
-  public class NestedToken : IToken
+  public abstract class TokenWrapper : IToken
   {
-    public NestedToken(IToken outer, IToken inner) {
-      Outer = outer;
-      Inner = inner;
+    protected readonly IToken WrappedToken;
+    protected TokenWrapper(IToken wrappedToken) {
+      Contract.Requires(wrappedToken != null);
+      WrappedToken = wrappedToken;
     }
-    public readonly IToken Outer;
-    public readonly IToken Inner;
 
     public int col {
-      get { return Outer.col; }
-      set { Outer.col = value; }
+      get { return WrappedToken.col; }
+      set { throw new NotSupportedException(); }
     }
-    public string filename {
-      get { return Outer.filename; }
-      set { Outer.filename = value; }
+    public virtual string filename {
+      get { return WrappedToken.filename; }
+      set { throw new NotSupportedException(); }
     }
     public bool IsValid {
-      get { return Outer.IsValid; }
+      get { return WrappedToken.IsValid; }
     }
     public int kind {
-      get { return Outer.kind; }
-      set { Outer.kind = value; }
+      get { return WrappedToken.kind; }
+      set { throw new NotSupportedException(); }
     }
     public int line {
-      get { return Outer.line; }
-      set { Outer.line = value; }
+      get { return WrappedToken.line; }
+      set { throw new NotSupportedException(); }
     }
     public int pos {
-      get { return Outer.pos; }
-      set { Outer.pos = value; }
+      get { return WrappedToken.pos; }
+      set { throw new NotSupportedException(); }
     }
     public string val {
-      get { return Outer.val; }
-      set { Outer.val = value; }
+      get { return WrappedToken.val; }
+      set { throw new NotSupportedException(); }
     }
   }
 
+  public class NestedToken : TokenWrapper
+  {
+    public NestedToken(IToken outer, IToken inner)
+      : base(outer)
+    {
+      Contract.Requires(outer != null);
+      Contract.Requires(inner != null);
+      Inner = inner;
+    }
+    public IToken Outer { get { return WrappedToken; } }
+    public readonly IToken Inner;
+  }
+
   // ------------------------------------------------------------------------------------------------------
 
   public abstract class Expression
-- 
cgit v1.2.3