multiple changes...

- fix for requirement inheritance in refinement.
- minimimally viable implementation of exclusive refinement feature.

1 files changed, 7 insertions, 4 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index e313ffac..6e64c7ec 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -17,12 +17,15 @@ namespace Microsoft.Dafny
       if (m is DefaultModuleDecl) {

         nw = new DefaultModuleDecl();

       } else {

-        nw = new ModuleDefinition(Tok(m.tok), name, m.IsAbstract, m.IsFacade, m.RefinementBaseName, m.Module, CloneAttributes(m.Attributes), true);

+        nw = new ModuleDefinition(Tok(m.tok), name, m.IsAbstract, m.IsFacade, m.IsExclusiveRefinement, m.RefinementBaseName, m.Module, CloneAttributes(m.Attributes), true);

       }

       foreach (var d in m.TopLevelDecls) {

         nw.TopLevelDecls.Add(CloneDeclaration(d, nw));

       }

-      nw.RefinementBase = m.RefinementBase;

+      if (null != m.RefinementBase) {

+          nw.RefinementBase = m.RefinementBase;

+      }

+      nw.ClonedFrom = m;

       nw.Height = m.Height;

       return nw;

     }

@@ -33,7 +36,7 @@ namespace Microsoft.Dafny
 

       if (d is OpaqueTypeDecl) {

         var dd = (OpaqueTypeDecl)d;

-        return new OpaqueTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), CloneAttributes(dd.Attributes));

+        return new OpaqueTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), CloneAttributes(dd.Attributes), d);

       } else if (d is TypeSynonymDecl) {

         var dd = (TypeSynonymDecl)d;

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

@@ -138,7 +141,7 @@ namespace Microsoft.Dafny
     }

 

     public TypeParameter CloneTypeParam(TypeParameter tp) {

-      return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport);

+      return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport, tp);

     }

 

     public MemberDecl CloneMember(MemberDecl member) {