From c558eecdcd6444919c0314043c0f328c85ca3b22 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 26 Feb 2016 16:50:38 -0800 Subject: Fix issue 139. Allow bound variables in nested case patterns to shadow variables declared outside the enclosing match. --- Source/Dafny/Resolver.cs | 12 +++++++++++- Test/dafny4/Bug139.dfy | 25 +++++++++++++++++++++++++ Test/dafny4/Bug139.dfy.expect | 2 ++ 3 files changed, 38 insertions(+), 1 deletion(-) create mode 100644 Test/dafny4/Bug139.dfy create mode 100644 Test/dafny4/Bug139.dfy.expect diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 5a63b4e3..d3b59b51 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6376,7 +6376,12 @@ namespace Microsoft.Dafny if (topLevel) { ScopePushAndReport(scope, v, "parameter"); } else { - if (scope.Find(v.Name) != null) { + // For cons(a, const(b, c)): + // this handles check to see if 'b' or 'c' is duplicate with 'a', + // the duplication check between 'b' and 'c' is handled in the desugared + // form (to avoid reporting the same error twice), that is why we don't + // push 'b' and 'c' onto the scope, only find. + if (scope.FindInCurrentScope(v.Name) != null) { reporter.Error(MessageSource.Resolver, v, "Duplicate parameter name: {0}", v.Name); } } @@ -11069,6 +11074,11 @@ namespace Microsoft.Dafny return Find(name, false); } + public Thing FindInCurrentScope(string name) { + Contract.Requires(name != null); + return Find(name, true); + } + public bool ContainsDecl(Thing t) { return things.Exists(thing => thing == t); } diff --git a/Test/dafny4/Bug139.dfy b/Test/dafny4/Bug139.dfy new file mode 100644 index 00000000..bd4ded73 --- /dev/null +++ b/Test/dafny4/Bug139.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +datatype List = Nil | Cons(int, List) + +method R(xs: List) +{ + var a: int; + var b: int; + match xs + case Nil => + case Cons(a, Nil()) => // this 'a' is allowed + case Cons(x, Cons(b, tail)) => // this 'b' (which is in a nested position) generates an error +} + +function F(xs: List): int +{ + var a := 4; + var b := 7; + match xs + case Nil => 0 + case Cons(a, Nil()) => 1 + case Cons(x, Cons(b, tail)) => 2 +} + diff --git a/Test/dafny4/Bug139.dfy.expect b/Test/dafny4/Bug139.dfy.expect new file mode 100644 index 00000000..52595bf9 --- /dev/null +++ b/Test/dafny4/Bug139.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 3 verified, 0 errors -- cgit v1.2.3 From 45e7bb72d4a8676796cb71cd8d11787dd6f91e17 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 29 Feb 2016 12:44:54 -0800 Subject: Revert change 1997 (bfe7c149bef1). IDE performance. Don't delay the resolver until the editor is idle for 5 second. --- Source/DafnyExtension/ResolverTagger.cs | 38 +++++---------------------------- 1 file changed, 5 insertions(+), 33 deletions(-) diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs index b711c276..4a50a4e8 100644 --- a/Source/DafnyExtension/ResolverTagger.cs +++ b/Source/DafnyExtension/ResolverTagger.cs @@ -15,7 +15,6 @@ using System.Linq; using System.Text.RegularExpressions; using System.Windows.Shapes; using Microsoft.VisualStudio; -using System.Windows.Threading; using Microsoft.VisualStudio.Shell; using Microsoft.VisualStudio.Shell.Interop; using Microsoft.VisualStudio.Text; @@ -130,8 +129,6 @@ namespace DafnyLanguage ErrorListProvider _errorProvider; private bool m_disposed; - readonly DispatcherTimer timer; - // The 'Snapshot' and 'Program' fields should be updated and read together, so they are protected by "this" public ITextSnapshot Snapshot; // may be null public Dafny.Program Program; // non-null only if the snapshot contains a Dafny program that type checks @@ -230,13 +227,7 @@ namespace DafnyLanguage Snapshot = null; // this makes sure the next snapshot will look different _errorProvider = new ErrorListProvider(serviceProvider); - BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, UponIdle); - - // keep track idle time after BufferIdleEvent has been handled. - timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle); - timer.Interval = TimeSpan.FromMilliseconds(5000); - timer.Tick += new EventHandler(ResolveBuffer); - buffer.Changed += BufferChanged; + BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer); } public void Dispose() @@ -266,9 +257,7 @@ namespace DafnyLanguage _errorProvider.Dispose(); _errorProvider = null; } - BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, UponIdle); - timer.Tick -= ResolveBuffer; - _buffer.Changed -= BufferChanged; + BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer); if (_document != null && _document.TextBuffer != null) { ResolverTaggers.Remove(_document.TextBuffer); @@ -328,21 +317,9 @@ namespace DafnyLanguage /// /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly. /// - void ResolveBuffer(object sender, EventArgs args) - { - timer.Stop(); - ParseAndResolveBuffer(sender, args, true); - } - - void UponIdle(object sender, EventArgs args) { - timer.Stop(); - ParseAndResolveBuffer(sender, args, false); - timer.Start(); - } - - void ParseAndResolveBuffer(object sender, EventArgs args, bool runResolver) { + void ResolveBuffer(object sender, EventArgs args) { ITextSnapshot snapshot = _buffer.CurrentSnapshot; - if (snapshot == Snapshot && !runResolver) + if (snapshot == Snapshot) return; // we've already done this snapshot string filename = _document != null ? _document.FilePath : ""; @@ -351,7 +328,7 @@ namespace DafnyLanguage Dafny.Program program; try { - program = driver.ProcessResolution(runResolver); + program = driver.ProcessResolution(true); newErrors = driver.Errors; } catch (Exception e) @@ -380,11 +357,6 @@ namespace DafnyLanguage UpdateErrorList(snapshot); } - void BufferChanged(object sender, TextContentChangedEventArgs e) { - timer.Stop(); - timer.Start(); - } - public void UpdateErrorList(ITextSnapshot snapshot) { if (_errorProvider != null && !m_disposed) -- cgit v1.2.3