[IronDafny] implemented workaround for "import opened" bug(s).

14 files changed, 161 insertions, 55 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 6e64c7ec..fe9795d3 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -44,9 +44,9 @@ namespace Microsoft.Dafny
       } else if (d is NewtypeDecl) {

         var dd = (NewtypeDecl)d;

         if (dd.Var == null) {

-          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes));

+          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes), dd);

         } else {

-          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes));

+          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes), dd);

         }

       } else if (d is TupleTypeDecl) {

         var dd = (TupleTypeDecl)d;

@@ -55,7 +55,7 @@ namespace Microsoft.Dafny
         var dd = (IndDatatypeDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

         var ctors = dd.Ctors.ConvertAll(CloneCtor);

-        var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes));

+        var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes), dd);

         return dt;

       } else if (d is CoDatatypeDecl) {

         var dd = (CoDatatypeDecl)d;

@@ -108,7 +108,7 @@ namespace Microsoft.Dafny
         if (d is DefaultClassDecl) {

           return new DefaultClassDecl(m, mm);

         } else {

-          return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType));

+          return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType), dd);

         }

       } else if (d is ModuleDecl) {

         if (d is LiteralModuleDecl) {

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 7b51fb5e..6e939968 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -515,7 +515,7 @@ Dafny
   | OtherTypeDecl<defaultModule, out td>        (. defaultModule.TopLevelDecls.Add(td); .)

   | IteratorDecl<defaultModule, out iter>       (. defaultModule.TopLevelDecls.Add(iter); .)

   | TraitDecl<defaultModule, out trait>    (. defaultModule.TopLevelDecls.Add(trait); .)

-  | ClassMemberDecl<membersDefaultClass, false, !DafnyOptions.O.AllowGlobals>

+  | ClassMemberDecl<membersDefaultClass, false, !DafnyOptions.O.AllowGlobals, false>

   }

   (. // find the default class in the default module, then append membersDefaultClass to its member list

      DefaultClassDecl defaultClass = null;

@@ -561,7 +561,7 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
         | NewtypeDecl<module, out td>                  (. module.TopLevelDecls.Add(td); .)

         | OtherTypeDecl<module, out td>                (. module.TopLevelDecls.Add(td); .)

         | IteratorDecl<module, out iter>               (. module.TopLevelDecls.Add(iter); .)

-        | ClassMemberDecl<namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals>

+        | ClassMemberDecl<namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals, true>

         }

       "}"                                  (. module.BodyEndTok = t;

                                               module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));

@@ -618,7 +618,7 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
   {"," Type<out trait>  (. traits.Add(trait); .) }

   ]         

   "{"                                            (. bodyStart = t;  .)

-  { ClassMemberDecl<members, true, false>

+  { ClassMemberDecl<members, true, false, false>

   }

   "}"

   (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits);

@@ -642,7 +642,7 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
 	NoUSIdent<out id>

 	[ GenericParameters<typeArgs> ]

 	"{"                                            (. bodyStart = t; .)

-    { ClassMemberDecl<members, true, false>

+    { ClassMemberDecl<members, true, false, false>

     }

     "}"

 	(. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);

@@ -651,7 +651,7 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
     .)

 	.

 

-ClassMemberDecl<.List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDecl.>

+ClassMemberDecl<.List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDecl, bool permitAbstractDecl.>

 = (. Contract.Requires(cce.NonNullElements(mm));

      Method/*!*/ m;

      Function/*!*/ f;

@@ -685,7 +685,7 @@ ClassMemberDecl<.List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDe
          mmod.IsProtected = false;

        }

     .)

-    MethodDecl<mmod, allowConstructors, out m>  (. mm.Add(m); .)

+    MethodDecl<mmod, allowConstructors, permitAbstractDecl, out m>  (. mm.Add(m); .)

   )

   .

 DatatypeDecl<ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt>

@@ -937,7 +937,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
   ">"

   .

 /*------------------------------------------------------------------------*/

-MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>

+MethodDecl<MemberModifiers mmod, bool allowConstructor, bool permitAbstractDecl, out Method/*!*/ m>

 = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);

      IToken/*!*/ id = Token.NoToken;

      bool hasName = false;  IToken keywordToken;

@@ -1018,7 +1018,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   [ BlockStmt<out body, out bodyStart, out bodyEnd>

   ]

   (.

-     if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {

+     if (!permitAbstractDecl && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {

         SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

      }

 

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index d14d82a3..c90755a3 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1777,6 +1777,14 @@ namespace Microsoft.Dafny {
       this.refinementBase = null;

       Includes = new List<Include>();

       IsBuiltinName = isBuiltinName;

+

+      if (isExclusiveRefinement && !DafnyOptions.O.IronDafny) {

+        parser.errors.SynErr(

+          tok.filename,

+          tok.line,

+          tok.col,

+          "The exclusively keyword is experimental and only available when IronDafny features are enabled (/ironDafny).");

+      }

     }

     public virtual bool IsDefaultModule {

       get {

@@ -1990,8 +1998,8 @@ namespace Microsoft.Dafny {
     }

 

     public ClassDecl(IToken tok, string name, ModuleDefinition module,

-      List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, List<Type> traits)

-      : base(tok, name, module, typeArgs, attributes) {

+      List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, List<Type> traits, ClassDecl clonedFrom = null)

+      : base(tok, name, module, typeArgs, attributes, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(module != null);

@@ -2005,6 +2013,12 @@ namespace Microsoft.Dafny {
         return false;

       }

     }

+

+    public new ClassDecl ClonedFrom {

+      get {

+        return (ClassDecl)base.ClonedFrom; 

+      }

+    }

   }

 

   public class DefaultClassDecl : ClassDecl {

@@ -2067,8 +2081,8 @@ namespace Microsoft.Dafny {
     }

 

     public DatatypeDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,

-      [Captured] List<DatatypeCtor> ctors, Attributes attributes)

-      : base(tok, name, module, typeArgs, attributes) {

+      [Captured] List<DatatypeCtor> ctors, Attributes attributes, DatatypeDecl clonedFrom = null)

+      : base(tok, name, module, typeArgs, attributes, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(module != null);

@@ -2082,6 +2096,12 @@ namespace Microsoft.Dafny {
         return (TypeArgs.Count == 0 && Ctors.TrueForAll(ctr => ctr.Formals.Count == 0));

       }

     }

+

+    public new DatatypeDecl ClonedFrom {

+      get {

+        return (DatatypeDecl)base.ClonedFrom; 

+      }

+    }

   }

 

   public class IndDatatypeDecl : DatatypeDecl

@@ -2094,8 +2114,8 @@ namespace Microsoft.Dafny {
     public ES EqualitySupport = ES.NotYetComputed;

 

     public IndDatatypeDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,

-      [Captured] List<DatatypeCtor> ctors, Attributes attributes)

-      : base(tok, name, module, typeArgs, ctors, attributes) {

+      [Captured] List<DatatypeCtor> ctors, Attributes attributes, IndDatatypeDecl clonedFrom = null)

+      : base(tok, name, module, typeArgs, ctors, attributes, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(module != null);

@@ -2103,6 +2123,12 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(ctors));

       Contract.Requires(1 <= ctors.Count);

     }

+

+    public new IndDatatypeDecl ClonedFrom {

+      get {

+        return (IndDatatypeDecl)base.ClonedFrom;

+      }

+    }

   }

 

   public class TupleTypeDecl : IndDatatypeDecl

@@ -2578,16 +2604,16 @@ namespace Microsoft.Dafny {
     public readonly BoundVar Var;  // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType))

     public readonly Expression Constraint;  // is null iff Var is

     public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers)

-    public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes)

-      : base(tok, name, module, new List<TypeParameter>(), attributes) {

+    public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes, NewtypeDecl clonedFrom = null)

+      : base(tok, name, module, new List<TypeParameter>(), attributes, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(module != null);

       Contract.Requires(baseType != null);

       BaseType = baseType;

     }

-    public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes)

-      : base(tok, name, module, new List<TypeParameter>(), attributes) {

+    public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes, NewtypeDecl clonedFrom = null)

+      : base(tok, name, module, new List<TypeParameter>(), attributes, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(module != null);

@@ -2618,6 +2644,12 @@ namespace Microsoft.Dafny {
       get { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases

       set { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases

     }

+

+    public new NewtypeDecl ClonedFrom {

+      get {

+        return (NewtypeDecl)base.ClonedFrom;

+      }

+    }

   }

 

   public class TypeSynonymDecl : TopLevelDecl, RedirectingTypeDecl

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index a3b26f2a..978525f3 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -15,7 +15,11 @@ namespace Microsoft.Dafny
 

     public override string VersionNumber {

       get {

-        return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion;

+        return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion

+#if ENABLE_IRONDAFNY

+          + "[IronDafny]"

+#endif

+          ;

       }

     }

     public override string VersionSuffix {

@@ -59,6 +63,13 @@ namespace Microsoft.Dafny
     public bool PrintStats = false;

     public bool PrintFunctionCallGraph = false;

     public bool WarnShadowing = false;

+    public bool IronDafny = 

+#if ENABLE_IRONDAFNY 

+      true

+#else

+      false

+#endif

+    ;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -201,6 +212,16 @@ namespace Microsoft.Dafny
             return true;

         }

 

+        case "noIronDafny": {

+            IronDafny = false;

+            return true;

+        }

+

+        case "ironDafny": {

+            IronDafny = true;

+            return true;

+        }

+

         default:

           break;

       }

@@ -301,6 +322,10 @@ namespace Microsoft.Dafny
   /funcCallGraph Print out the function call graph.  Format is: func,mod=callee*

   /warnShadowing  Emits a warning if the name of a declared variable caused another variable

                 to be shadowed

+  /ironDafny    Enable experimental features needed to support Ironclad/Ironfleet. Use of

+                these features may cause your code to become incompatible with future

+                releases of Dafny.

+  /noIronDafny  Disable Ironclad/Ironfleet features, if enabled by default.

 ");

       base.Usage();  // also print the Boogie options

     }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index a90e650a..0c88cc22 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -576,7 +576,7 @@ bool IsType(ref IToken pt) {
 				break;

 			}

 			case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: {

-				ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals);

+				ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals, false);

 				break;

 			}

 			}

@@ -672,7 +672,7 @@ bool IsType(ref IToken pt) {
 					break;

 				}

 				case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: {

-					ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals);

+					ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals, true);

 					break;

 				}

 				}

@@ -750,7 +750,7 @@ bool IsType(ref IToken pt) {
 		Expect(45);

 		bodyStart = t;  

 		while (StartOf(2)) {

-			ClassMemberDecl(members, true, false);

+			ClassMemberDecl(members, true, false, false);

 		}

 		Expect(46);

 		c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits);

@@ -961,7 +961,7 @@ bool IsType(ref IToken pt) {
 		Expect(45);

 		bodyStart = t; 

 		while (StartOf(2)) {

-			ClassMemberDecl(members, true, false);

+			ClassMemberDecl(members, true, false, false);

 		}

 		Expect(46);

 		trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);

@@ -970,7 +970,7 @@ bool IsType(ref IToken pt) {
 		

 	}

 

-	void ClassMemberDecl(List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDecl) {

+	void ClassMemberDecl(List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDecl, bool permitAbstractDecl) {

 		Contract.Requires(cce.NonNullElements(mm));

 		Method/*!*/ m;

 		Function/*!*/ f;

@@ -1015,7 +1015,7 @@ bool IsType(ref IToken pt) {
 			 mmod.IsProtected = false;

 			}

 			

-			MethodDecl(mmod, allowConstructors, out m);

+			MethodDecl(mmod, allowConstructors, permitAbstractDecl, out m);

 			mm.Add(m); 

 		} else SynErr(151);

 	}

@@ -1273,7 +1273,7 @@ bool IsType(ref IToken pt) {
 		

 	}

 

-	void MethodDecl(MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m) {

+	void MethodDecl(MemberModifiers mmod, bool allowConstructor, bool permitAbstractDecl, out Method/*!*/ m) {

 		Contract.Ensures(Contract.ValueAtReturn(out m) !=null);

 		IToken/*!*/ id = Token.NoToken;

 		bool hasName = false;  IToken keywordToken;

@@ -1393,7 +1393,7 @@ bool IsType(ref IToken pt) {
 		if (la.kind == 45) {

 			BlockStmt(out body, out bodyStart, out bodyEnd);

 		}

-		if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {

+		if (!permitAbstractDecl && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {

 		  SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

 		}

 		

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 3e308e76..460859db 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -919,20 +919,27 @@ namespace Microsoft.Dafny
       sig.IsGhost = moduleDef.IsAbstract;

       List<TopLevelDecl> declarations = moduleDef.TopLevelDecls;

 

-      if (useImports) {

-        // First go through and add anything from the opened imports

-        foreach (var im in declarations) {

-          if (im is ModuleDecl && ((ModuleDecl)im).Opened) {

-            var s = GetSignature(((ModuleDecl)im).Signature);

+      // First go through and add anything from the opened imports

+      foreach (var im in declarations) {

+        if (im is ModuleDecl && ((ModuleDecl)im).Opened) {

+          var s = GetSignature(((ModuleDecl)im).Signature);

+

+          if (useImports || DafnyOptions.O.IronDafny) {

             // classes:

             foreach (var kv in s.TopLevels) {

-              TopLevelDecl d;

-              if (sig.TopLevels.TryGetValue(kv.Key, out d)) {

-                sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value);

-              } else {

-                sig.TopLevels.Add(kv.Key, kv.Value);

+              // IronDafny: we need to pull the members of the opened module's _default class in so that they can be merged.

+              if (useImports || string.Equals(kv.Key, "_default", StringComparison.InvariantCulture)) {

+                TopLevelDecl d;

+                if (sig.TopLevels.TryGetValue(kv.Key, out d)) {

+                  sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value);

+                } else {

+                  sig.TopLevels.Add(kv.Key, kv.Value);

+                }

               }

             }

+          }

+

+          if (useImports) {

             // constructors:

             foreach (var kv in s.Ctors) {

               Tuple<DatatypeCtor, bool> pair;

@@ -948,6 +955,9 @@ namespace Microsoft.Dafny
                 sig.Ctors.Add(kv.Key, kv.Value);

               }

             }

+          }

+

+          if (useImports || DafnyOptions.O.IronDafny) {

             // static members:

             foreach (var kv in s.StaticMembers) {

               MemberDecl md;

@@ -957,7 +967,7 @@ namespace Microsoft.Dafny
                 // add new

                 sig.StaticMembers.Add(kv.Key, kv.Value);

               }

-            }

+            }              

           }

         }

       }

@@ -4406,8 +4416,23 @@ namespace Microsoft.Dafny
           return false;

         }

         var aa = (UserDefinedType)a;

+        var rca = aa.ResolvedClass;

         var bb = (UserDefinedType)b;

-        if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) {

+        var rcb = bb.ResolvedClass;

+        if (DafnyOptions.O.IronDafny)

+        {

+          while (rca != null && rca.Module.IsAbstract && rca.ClonedFrom != null)

+          {

+            // todo: should ClonedFrom be a TopLevelDecl?

+            // todo: should ClonedFrom be moved to TopLevelDecl?

+            rca = (TopLevelDecl)rca.ClonedFrom;

+          }

+          while (rcb != null && rcb.Module.IsAbstract && rcb.ClonedFrom != null)

+          {

+            rcb = (TopLevelDecl)rcb.ClonedFrom;

+          }

+        }

+        if (rca != null && rca == rcb) {

           // these are both resolved class/datatype types

           Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count);

           bool successSoFar = true;

@@ -4416,12 +4441,12 @@ namespace Microsoft.Dafny
           }

           return successSoFar;

         }

-        else if ((bb.ResolvedClass is TraitDecl) && (aa.ResolvedClass is TraitDecl)) {

-            return ((TraitDecl)bb.ResolvedClass).FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;

-        } else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl)) {

-            return ((ClassDecl)bb.ResolvedClass).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName);

-        } else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl)) {

-            return ((ClassDecl)aa.ResolvedClass).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName);

+        else if ((rcb is TraitDecl) && (rca is TraitDecl)) {

+            return ((TraitDecl)rcb).FullCompileName == ((TraitDecl)rca).FullCompileName;

+        } else if ((rcb is ClassDecl) && (rca is TraitDecl)) {

+            return ((ClassDecl)rcb).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rca).FullCompileName);

+        } else if ((rca is ClassDecl) && (rcb is TraitDecl)) {

+            return ((ClassDecl)rca).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rcb).FullCompileName);

         } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {

           // type parameters

           if (aa.TypeArgs.Count != bb.TypeArgs.Count) {

diff --git a/Test/irondafny0/FIFO.dfy b/Test/irondafny0/FIFO.dfy
index 1256b55d..ded8f567 100644
--- a/Test/irondafny0/FIFO.dfy
+++ b/Test/irondafny0/FIFO.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 include "Queue.dfyi"

diff --git a/Test/irondafny0/LIFO.dfy b/Test/irondafny0/LIFO.dfy
index bac08fba..8c0a08e8 100644
--- a/Test/irondafny0/LIFO.dfy
+++ b/Test/irondafny0/LIFO.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 include "Queue.dfyi"

diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy
new file mode 100644
index 00000000..7464c346
--- /dev/null
+++ b/Test/irondafny0/opened_workaround.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /ironDafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+module A {

+

+    predicate P() 

+

+    class C

+    {

+        static method{:axiom} M()

+            ensures P();

+    } 

+}

+

+abstract module B {

+    import opened A

+}

+

+abstract module C {

+    import Bee as B       // Works

+}

diff --git a/Test/irondafny0/opened_workaround.dfy.expect b/Test/irondafny0/opened_workaround.dfy.expect
new file mode 100644
index 00000000..0be94b4c
--- /dev/null
+++ b/Test/irondafny0/opened_workaround.dfy.expect
@@ -0,0 +1,3 @@
+

+Dafny program verifier finished with 3 verified, 0 errors

+Compilation error: Function _0_A_Compile._default.P has no body

diff --git a/Test/irondafny0/xrefine0.dfy b/Test/irondafny0/xrefine0.dfy
index 35993ce8..b849111c 100644
--- a/Test/irondafny0/xrefine0.dfy
+++ b/Test/irondafny0/xrefine0.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /ironDafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 abstract module Delicious {}

diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy
index 10d25f53..4b085e6b 100644
--- a/Test/irondafny0/xrefine1.dfy
+++ b/Test/irondafny0/xrefine1.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 abstract module ProtocolSpec {

diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy
index 7578b424..1de4e201 100644
--- a/Test/irondafny0/xrefine2.dfy
+++ b/Test/irondafny0/xrefine2.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 abstract module ProtocolSpec {

diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy
index 69c5bc27..44add7cc 100644
--- a/Test/irondafny0/xrefine3.dfy
+++ b/Test/irondafny0/xrefine3.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 abstract module AlphaSpec {