From e29ca07f28a9c54c46f4c45a3d77c3cf7254d07f Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 9 Jan 2012 10:29:11 -0800
Subject: Dafny: disallow changes of datatypes in refinements

---
 Source/Dafny/RefinementTransformer.cs | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

(limited to 'Source/Dafny')

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index a25d1eb8..adf99859 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -104,11 +104,7 @@ namespace Microsoft.Dafny {
           } else if (nw is ArbitraryTypeDecl) {
             reporter.Error(nw, "an arbitrary type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);
           } else if (nw is DatatypeDecl) {
-            if (d is ClassDecl) {
-              reporter.Error(nw, "a datatype declaration ({0}) in a refining module cannot replace a class declaration in the refinement base", nw.Name);
-            } else {
-              m.TopLevelDecls[index] = MergeDatatype((DatatypeDecl)nw, (DatatypeDecl)d);
-            }
+            reporter.Error(nw, "a datatype declaration ({0}) in a refinement module can only replace an arbitrary-type declaration", nw.Name);
           } else {
             Contract.Assert(nw is ClassDecl);
             if (d is DatatypeDecl) {
@@ -502,11 +498,6 @@ namespace Microsoft.Dafny {
 
     // -------------------------------------------------- Merging ---------------------------------------------------------------
 
-    DatatypeDecl MergeDatatype(DatatypeDecl nw, DatatypeDecl prev) {
-      // TODO
-      return nw;
-    }
-
     ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {
       // TODO
       return nw;
-- 
cgit v1.2.3