diff options
| author |  Rustan Leino <unknown> | 2014-01-08 19:28:24 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-08 19:28:24 -0800 |
| commit | de8338b233b3a4daec0f0cfcfeca59115e32e574 (patch) | |
| tree | 45f3cfdd78400b0d2fdbbcc10014499528bb832e /Source/Dafny | |
| parent | ecb53212d30f7e8ef6145bcca9f40517e1999956 (diff) | |
Manually adjusted merge
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Cloner.cs | 23 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 17 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 2 |
4 files changed, 35 insertions, 11 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 6928d9b9..fa6d635c 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -123,7 +123,7 @@ namespace Microsoft.Dafny }
}
- virtual public Type CloneType(Type t) {
+ public virtual Type CloneType(Type t) {
if (t is BasicType) {
return t;
} else if (t is SetType) {
@@ -349,10 +349,12 @@ namespace Microsoft.Dafny }
}
- public CasePattern CloneCasePattern(CasePattern pat) {
+ public virtual CasePattern CloneCasePattern(CasePattern pat) {
Contract.Requires(pat != null);
- if (pat.Arguments == null) {
+ if (pat.Var != null) {
return new CasePattern(pat.tok, CloneBoundVar(pat.Var));
+ } else if (pat.Arguments == null) {
+ return new CasePattern(pat.tok, pat.Id, null);
} else {
return new CasePattern(pat.tok, pat.Id, pat.Arguments.ConvertAll(CloneCasePattern));
}
@@ -725,6 +727,21 @@ namespace Microsoft.Dafny return new_t;
}
+
+ public override CasePattern CloneCasePattern(CasePattern pat) {
+ if (pat.Var != null) {
+ var newPat = new CasePattern(pat.tok, CloneBoundVar(pat.Var));
+ newPat.AssembleExpr(null);
+ return newPat;
+ } else {
+ var newArgs = pat.Arguments == null ? null : pat.Arguments.ConvertAll(CloneCasePattern);
+ var patE = (DatatypeValue)pat.Expr;
+ var newPat = new CasePattern(pat.tok, pat.Id, newArgs);
+ newPat.Ctor = pat.Ctor;
+ newPat.AssembleExpr(patE.InferredTypeArgs.ConvertAll(CloneType));
+ return newPat;
+ }
+ }
}
}
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index a0530a5b..5afac116 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4100,17 +4100,22 @@ namespace Microsoft.Dafny { /// <summary>
/// Create a let expression with a resolved type and fresh variables
/// </summary>
- public static Expression CreateLet(IToken tok, List<BoundVar> vars, List<Expression> RHSs, Expression body, bool exact) {
+ public static Expression CreateLet(IToken tok, List<CasePattern> LHSs, List<Expression> RHSs, Expression body, bool exact) {
Contract.Requires(tok != null);
- Contract.Requires(vars != null && RHSs != null);
- Contract.Requires(vars.Count == RHSs.Count);
+ Contract.Requires(LHSs != null && RHSs != null);
+ Contract.Requires(LHSs.Count == RHSs.Count);
Contract.Requires(body != null);
ResolvedCloner cloner = new ResolvedCloner();
- var newVars = vars.ConvertAll(cloner.CloneBoundVar);
- body = VarSubstituter(vars, newVars, body);
+ var newLHSs = LHSs.ConvertAll(cloner.CloneCasePattern);
- var let = new LetExpr(tok, newVars, RHSs, body, exact);
+ var oldVars = new List<BoundVar>();
+ LHSs.Iter(p => oldVars.AddRange(p.Vars));
+ var newVars = new List<BoundVar>();
+ newLHSs.Iter(p => newVars.AddRange(p.Vars));
+ body = VarSubstituter(oldVars, newVars, body);
+
+ var let = new LetExpr(tok, newLHSs, RHSs, body, exact);
let.Type = body.Type; // resolve here
return let;
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index bd6c1d8b..f8880f92 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1299,8 +1299,10 @@ namespace Microsoft.Dafny public CasePattern CloneCasePattern(CasePattern pat) {
Contract.Requires(pat != null);
- if (pat.Arguments == null) {
+ if (pat.Var != null) {
return new CasePattern(pat.tok, CloneBoundVar(pat.Var));
+ } else if (pat.Arguments == null) {
+ return new CasePattern(pat.tok, pat.Id, null);
} else {
return new CasePattern(pat.tok, pat.Id, pat.Arguments.ConvertAll(CloneCasePattern));
}
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 601ef935..d1c89965 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -753,7 +753,7 @@ namespace Microsoft.Dafny }
var new_reqs = generateAutoReqs(e.Body);
if (new_reqs.Count > 0) {
- reqs.Add(Expression.CreateLet(e.tok, e.Vars, e.RHSs, andify(e.tok, new_reqs), e.Exact));
+ reqs.Add(Expression.CreateLet(e.tok, e.LHSs, e.RHSs, andify(e.tok, new_reqs), e.Exact));
}
} else {
// TODO: Still need to figure out what the right choice is here:
|