From 310521db71e18305b04f6a32ab753c87e30bfa19 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Sun, 29 Jul 2012 12:24:02 -0700
Subject: Dafny: added structural refinement check

---
 Dafny/Resolver.cs | 33 +++++++++++++++++++--------------
 1 file changed, 19 insertions(+), 14 deletions(-)

(limited to 'Dafny/Resolver.cs')

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 8c14cb0c..0761d865 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -144,7 +144,7 @@ namespace Microsoft.Dafny
         h++;
       }
 
-      var refinementTransformer = new RefinementTransformer(this);
+      var refinementTransformer = new RefinementTransformer(this, prog);
 
       IRewriter rewriter = new AutoContractsRewriter();
       systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);
@@ -216,11 +216,14 @@ namespace Microsoft.Dafny
             ModuleSignature compileSig;
             if (abs.CompilePath != null) {
               if (ResolvePath(abs.CompileRoot, abs.CompilePath, out compileSig)) {
-                if (refinementTransformer.CheckIsRefinement(compileSig, p, abs.CompilePath[0],
-                  "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of " + Util.Comma(".", abs.Path, x => x.val))) {
+                if (refinementTransformer.CheckIsRefinement(compileSig, p)) {
                   abs.Signature.CompileSignature = compileSig;
-                  abs.Signature.IsGhost = compileSig.IsGhost;
+                } else {
+                  Error(abs.CompilePath[0],
+                  "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of " + Util.Comma(".", abs.Path, x => x.val));
                 }
+                abs.Signature.IsGhost = compileSig.IsGhost;
+                // always keep the ghost information, to supress a spurious error message when the compile module isn't actually a refinement
               }
             }
           } else {
@@ -305,17 +308,17 @@ namespace Microsoft.Dafny
           var subdecl = (LiteralModuleDecl)tld;
           var subBindings = BindModuleNames(subdecl.ModuleDef, bindings);
           if (!bindings.BindName(subdecl.Name, subdecl, subBindings)) {
-            Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name);
+            Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name);
           }
         } else if (tld is AbstractModuleDecl) {
           var subdecl = (AbstractModuleDecl)tld;
           if (!bindings.BindName(subdecl.Name, subdecl, null)) {
-            Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name);
+            Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name);
           }
         } else if (tld is AliasModuleDecl) {
           var subdecl = (AliasModuleDecl)tld;
           if (!bindings.BindName(subdecl.Name, subdecl, null)) {
-            Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name);
+            Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name);
           }
         }
       }
@@ -853,7 +856,7 @@ namespace Microsoft.Dafny
       foreach (TopLevelDecl d in declarations) {
         Contract.Assert(d != null);
         allTypeParameters.PushMarker();
-        ResolveTypeParameters(d.TypeArgs, true, d);
+        ResolveTypeParameters(d.TypeArgs, true, d, true);
         if (d is ArbitraryTypeDecl) {
           // nothing to do
         } else if (d is ClassDecl) {
@@ -889,7 +892,7 @@ namespace Microsoft.Dafny
       foreach (TopLevelDecl d in declarations) {
         Contract.Assert(d != null);
         allTypeParameters.PushMarker();
-        ResolveTypeParameters(d.TypeArgs, false, d);
+        ResolveTypeParameters(d.TypeArgs, false, d, true);
         if (d is ClassDecl) {
           ResolveClassMemberBodies((ClassDecl)d);
         }
@@ -1520,14 +1523,14 @@ namespace Microsoft.Dafny
         } else if (member is Function) {
           Function f = (Function)member;
           allTypeParameters.PushMarker();
-          ResolveTypeParameters(f.TypeArgs, true, f);
+          ResolveTypeParameters(f.TypeArgs, true, f, false);
           ResolveFunctionSignature(f);
           allTypeParameters.PopMarker();
 
         } else if (member is Method) {
           Method m = (Method)member;
           allTypeParameters.PushMarker();
-          ResolveTypeParameters(m.TypeArgs, true, m);
+          ResolveTypeParameters(m.TypeArgs, true, m, false);
           ResolveMethodSignature(m);
           allTypeParameters.PopMarker();
 
@@ -1556,14 +1559,14 @@ namespace Microsoft.Dafny
         } else if (member is Function) {
           Function f = (Function)member;
           allTypeParameters.PushMarker();
-          ResolveTypeParameters(f.TypeArgs, false, f);
+          ResolveTypeParameters(f.TypeArgs, false, f, false);
           ResolveFunction(f);
           allTypeParameters.PopMarker();
 
         } else if (member is Method) {
           Method m = (Method)member;
           allTypeParameters.PushMarker();
-          ResolveTypeParameters(m.TypeArgs, false, m);
+          ResolveTypeParameters(m.TypeArgs, false, m, false);
           ResolveMethod(m);
           allTypeParameters.PopMarker();
         } else {
@@ -1832,16 +1835,18 @@ namespace Microsoft.Dafny
       }
     }
 
-    void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {
+    void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent, bool isToplevel) {
 
       Contract.Requires(tparams != null);
       Contract.Requires(parent != null);
       // push non-duplicated type parameter names
+      int index = 0;
       foreach (TypeParameter tp in tparams) {
         Contract.Assert(tp != null);
         if (emitErrors) {
           // we're seeing this TypeParameter for the first time
           tp.Parent = parent;
+          tp.PositionalIndex = index;
         }
         if (!allTypeParameters.Push(tp.Name, tp) && emitErrors) {
           Error(tp, "Duplicate type-parameter name: {0}", tp.Name);
-- 
cgit v1.2.3