From f011e32f5a4a62b241c0c1301ab8010878b1bc7b Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 30 Nov 2015 13:03:21 -0800 Subject: Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr when trying to substitute the nested CasePattern with the BoundVar. --- Source/Dafny/Resolver.cs | 33 ++++++++++++++++----------------- Source/Dafny/Rewriter.cs | 22 +++++++++++++--------- 2 files changed, 29 insertions(+), 26 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index eff7d97d..52845c3f 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -5950,13 +5950,9 @@ namespace Microsoft.Dafny } // convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr. - Type type = new InferredTypeProxy(); - string name = FreshTempVarName("_mc#", codeContext); - MatchCaseToken mcToken = new MatchCaseToken(s.Tok); - BoundVar bv = new BoundVar(mcToken, name, type); - List patternSubst = new List(); + List> patternSubst = new List>(); if (dtd != null) { - DesugarMatchCaseStmt(s, dtd, bv, patternSubst, codeContext); + DesugarMatchCaseStmt(s, dtd, patternSubst, codeContext); } ISet memberNamesUsed = new HashSet(); @@ -6008,7 +6004,7 @@ namespace Microsoft.Dafny // substitute body to replace the case pat with v. This needs to happen // after the body is resolved so we can scope the bv correctly. if (patternSubst.Count > 0) { - MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst, bv); + MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst); List list = new List(); foreach (Statement ss in mc.Body) { Statement clone = cloner.CloneStmt(ss); @@ -6125,7 +6121,7 @@ namespace Microsoft.Dafny * case Nil => y * case Cons(z, zs) => last(ys) */ - void DesugarMatchCaseStmt(MatchStmt s, DatatypeDecl dtd, BoundVar sourceVar, List patterns, ICodeContext codeContext) { + void DesugarMatchCaseStmt(MatchStmt s, DatatypeDecl dtd, List> patterns, ICodeContext codeContext) { Contract.Assert(dtd != null); Dictionary ctors = datatypeCtors[dtd]; if (ctors == null) { @@ -6133,6 +6129,8 @@ namespace Microsoft.Dafny return; } + Type type = new InferredTypeProxy(); + string name = FreshTempVarName("_mc#", codeContext); foreach (MatchCaseStmt mc in s.Cases) { if (mc.Arguments != null) { // already desugared. This happens during the second pass resolver after cloning. @@ -6140,6 +6138,7 @@ namespace Microsoft.Dafny return; } + BoundVar sourceVar = new BoundVar(new MatchCaseToken(s.Tok), name, type); Contract.Assert(mc.Arguments == null); Contract.Assert(mc.CasePatterns != null); Contract.Assert(ctors != null); @@ -6157,7 +6156,7 @@ namespace Microsoft.Dafny arguments.Add(v); } else { DesugarMatchCasePattern(mc, pat, sourceVar); - patterns.Add(pat); + patterns.Add(new Tuple(pat, sourceVar)); arguments.Add(sourceVar); } } @@ -8249,12 +8248,9 @@ namespace Microsoft.Dafny } // convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr. - Type type = new InferredTypeProxy(); - string name = FreshTempVarName("_mc#", opts.codeContext); - BoundVar bv = new BoundVar(new MatchCaseToken(me.tok), name, type); - List patternSubst = new List(); + List> patternSubst = new List>(); if (dtd != null) { - DesugarMatchCaseExpr(me, dtd, bv, patternSubst, opts.codeContext); + DesugarMatchCaseExpr(me, dtd, patternSubst, opts.codeContext); } ISet memberNamesUsed = new HashSet(); @@ -8306,7 +8302,7 @@ namespace Microsoft.Dafny // substitute body to replace the case pat with v. This needs to happen // after the body is resolved so we can scope the bv correctly. if (patternSubst.Count > 0) { - MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst, bv); + MatchCaseExprSubstituteCloner cloner = new MatchCaseExprSubstituteCloner(patternSubst); mc.UpdateBody(cloner.CloneExpr(mc.Body)); // resolve it again since we just cloned it. ResolveExpression(mc.Body, opts); @@ -8408,7 +8404,7 @@ namespace Microsoft.Dafny * case Nil => y * case Cons(z, zs) => last(ys) * */ - void DesugarMatchCaseExpr(MatchExpr me, DatatypeDecl dtd, BoundVar sourceVar, List patterns, ICodeContext codeContext) { + void DesugarMatchCaseExpr(MatchExpr me, DatatypeDecl dtd, List> patterns, ICodeContext codeContext) { Contract.Assert(dtd != null); Dictionary ctors = datatypeCtors[dtd]; if (ctors == null) { @@ -8416,6 +8412,8 @@ namespace Microsoft.Dafny return; } + Type type = new InferredTypeProxy(); + string name = FreshTempVarName("_mc#", codeContext); foreach (MatchCaseExpr mc in me.Cases) { if (mc.Arguments != null) { // already desugared. This happens during the second pass resolver after cloning. @@ -8423,6 +8421,7 @@ namespace Microsoft.Dafny return; } + BoundVar sourceVar = new BoundVar(new MatchCaseToken(me.tok), name, type); Contract.Assert(mc.Arguments == null); Contract.Assert(mc.CasePatterns != null); Contract.Assert(ctors != null); @@ -8439,7 +8438,7 @@ namespace Microsoft.Dafny arguments.Add(v); } else { DesugarMatchCasePattern(mc, pat, sourceVar); - patterns.Add(pat); + patterns.Add(new Tuple(pat, sourceVar)); arguments.Add(sourceVar); } } diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 9a898cbe..13b16066 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -1429,16 +1429,16 @@ namespace Microsoft.Dafny class MatchCaseExprSubstituteCloner : Cloner { - private List patternSubst; + private List> patternSubst; private BoundVar oldvar; private BoundVar var; // the cloner is called after resolving the body of matchexpr, trying // to replace casepattern in the body that has been replaced by bv - public MatchCaseExprSubstituteCloner(List subst, BoundVar var) { + public MatchCaseExprSubstituteCloner(List> subst) { this.patternSubst = subst; this.oldvar = null; - this.var = var; + this.var = null; } public MatchCaseExprSubstituteCloner(BoundVar oldvar, BoundVar var) { @@ -1471,21 +1471,23 @@ namespace Microsoft.Dafny public override Expression CloneApplySuffix(ApplySuffix e) { // if the ApplySuffix matches the CasePattern, then replace it with the BoundVar. CasePattern cp = null; - if (FindMatchingPattern(e, out cp)) { - if (this.var.tok is MatchCaseToken) { + BoundVar bv = null; + if (FindMatchingPattern(e, out cp, out bv)) { + if (bv.tok is MatchCaseToken) { Contract.Assert(e.Args.Count == cp.Arguments.Count); for (int i = 0; i < e.Args.Count; i++) { - ((MatchCaseToken)this.var.tok).AddVar(e.Args[i].tok, cp.Arguments[i].Var, false); + ((MatchCaseToken)bv.tok).AddVar(e.Args[i].tok, cp.Arguments[i].Var, false); } } - return new NameSegment(new AutoGeneratedToken(e.tok), this.var.Name, null); + return new NameSegment(new AutoGeneratedToken(e.tok), bv.Name, null); } else { return new ApplySuffix(Tok(e.tok), CloneExpr(e.Lhs), e.Args.ConvertAll(CloneExpr)); } } - private bool FindMatchingPattern(ApplySuffix e, out CasePattern pattern) { + private bool FindMatchingPattern(ApplySuffix e, out CasePattern pattern, out BoundVar bv) { pattern = null; + bv = null; if (patternSubst == null) { return false; } @@ -1494,7 +1496,8 @@ namespace Microsoft.Dafny return false; } string applyName = ((NameSegment)lhs).Name; - foreach (CasePattern cp in patternSubst) { + foreach (Tuple pair in patternSubst) { + CasePattern cp = pair.Item1; string ctorName = cp.Id; if (!(applyName.Equals(ctorName)) || (e.Args.Count != cp.Arguments.Count)) { continue; @@ -1514,6 +1517,7 @@ namespace Microsoft.Dafny } if (found) { pattern = cp; + bv = pair.Item2; return true; } } -- cgit v1.2.3