diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 8 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 7 |
2 files changed, 11 insertions, 4 deletions
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 3c206066..96ae33c6 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -173,7 +173,6 @@ namespace Microsoft.Dafny { }
decl.Refined = (ClassDecl!) a;
// TODO: copy over remaining members of a
- // TODO: extend with type parameters for refinements
}
}
@@ -469,6 +468,13 @@ namespace Microsoft.Dafny { }
void ResolveTypeParameters(List<TypeParameter!>! tparams, bool emitErrors, TypeParameter.ParentType! parent) {
+ // push type arguments of the refined class
+ if (parent is ClassRefinementDecl) {
+ ClassDecl refined = ((ClassRefinementDecl)parent).Refined;
+ assert refined != null;
+ ResolveTypeParameters(refined.TypeArgs, false, refined);
+ }
+
// push non-duplicated type parameter names
foreach (TypeParameter tp in tparams) {
if (emitErrors) {
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index f6fc5142..ff88c67f 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -1797,12 +1797,13 @@ namespace Microsoft.Dafny { // assume I($Heap, $Heap)
builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));
- // assign input formals of m
+ // assign input formals of m (except "this")
for (int i = 0; i < m.Ins.Count; i++) {
Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName, TrType(m.Ins[i].Type)));
localVariables.Add(arg);
- assert inParams[i+1] != null;
- builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, arg), new Bpl.IdentifierExpr(m.tok, inParams[i+1])));
+ Bpl.Variable var = inParams[i+1];
+ assert var != null;
+ builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, arg), new Bpl.IdentifierExpr(m.tok, var)));
}
// call inlined m;
|