diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-08-11 16:07:38 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-08-11 16:07:38 -0700 |
| commit | 8797f054f44d114147562689d80c9970d8ea4f82 (patch) | |
| tree | 6a9e99a6a39126f946c0e7dd55cf0fa03a1a0ca7 /Source/Dafny/RefinementTransformer.cs | |
| parent | 4cbe4583b329a39dee2b4b456758cafbe7e2fa79 (diff) | |
| parent | 08ab990d6f1a188c6cc039d6a2289daf41ff52d3 (diff) | |
Merge
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index d90d2362..a7989cba 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -830,6 +830,90 @@ namespace Microsoft.Dafny }
}
+ public void CheckOverride_FunctionParameters(Function nw, Function f)
+ {
+ CheckOverride_TypeParameters(nw.tok, f.TypeArgs, nw.TypeArgs, nw.Name, "function", false);
+ CheckOverrideResolvedParameters(nw.tok, f.Formals, nw.Formals, nw.Name, "function", "parameter");
+ if (!ResolvedTypesAreTheSame(nw.ResultType, f.ResultType))
+ {
+ reporter.Error(nw, "the result type of function '{0}' ({1}) differs from the result type of the corresponding function in the module it overrides ({2})", nw.Name, nw.ResultType, f.ResultType);
+ }
+ }
+
+ public void CheckOverride_MethodParameters(Method nw, Method f)
+ {
+ CheckOverride_TypeParameters(nw.tok, f.TypeArgs, nw.TypeArgs, nw.Name, "method", false);
+ CheckOverrideResolvedParameters(nw.tok, f.Ins, nw.Ins, nw.Name, "method", "in-parameter");
+ CheckOverrideResolvedParameters(nw.tok, f.Outs, nw.Outs, nw.Name, "method", "out-parameter");
+ }
+
+ public void CheckOverride_TypeParameters(IToken tok, List<TypeParameter> old, List<TypeParameter> nw, string name, string thing, bool checkNames = true)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(old != null);
+ Contract.Requires(nw != null);
+ Contract.Requires(name != null);
+ Contract.Requires(thing != null);
+ if (old.Count != nw.Count)
+ {
+ reporter.Error(tok, "{0} '{1}' is declared with a different number of type parameters ({2} instead of {3}) than the corresponding {0} in the module it overrides", thing, name, nw.Count, old.Count);
+ }
+ else
+ {
+ for (int i = 0; i < old.Count; i++)
+ {
+ var o = old[i];
+ var n = nw[i];
+ if (o.Name != n.Name && checkNames)
+ { // if checkNames is false, then just treat the parameters positionally.
+ reporter.Error(n.tok, "type parameters are not allowed to be renamed from the names given in the {0} in the module being overriden (expected '{1}', found '{2}')", thing, o.Name, n.Name);
+ }
+ else
+ {
+ // Here's how we actually compute it:
+ if (o.EqualitySupport != TypeParameter.EqualitySupportValue.InferredRequired && o.EqualitySupport != n.EqualitySupport)
+ {
+ reporter.Error(n.tok, "type parameter '{0}' is not allowed to change the requirement of supporting equality", n.Name);
+ }
+ }
+ }
+ }
+ }
+
+ public void CheckOverrideResolvedParameters(IToken tok, List<Formal> old, List<Formal> nw, string name, string thing, string parameterKind)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(old != null);
+ Contract.Requires(nw != null);
+ Contract.Requires(name != null);
+ Contract.Requires(thing != null);
+ Contract.Requires(parameterKind != null);
+ if (old.Count != nw.Count)
+ {
+ reporter.Error(tok, "{0} '{1}' is declared with a different number of {2} ({3} instead of {4}) than the corresponding {0} in the module it overrides", thing, name, parameterKind, nw.Count, old.Count);
+ }
+ else
+ {
+ for (int i = 0; i < old.Count; i++)
+ {
+ var o = old[i];
+ var n = nw[i];
+ if (!o.IsGhost && n.IsGhost)
+ {
+ reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it overrides, from non-ghost to ghost", parameterKind, n.Name, thing, name);
+ }
+ else if (o.IsGhost && !n.IsGhost)
+ {
+ reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it overrides, from ghost to non-ghost", parameterKind, n.Name, thing, name);
+ }
+ else if (!ResolvedTypesAreTheSame(o.Type, n.Type))
+ {
+ reporter.Error(n.tok, "the type of {0} '{1}' is different from the type of the same {0} in the corresponding {2} in the module it overrides ('{3}' instead of '{4}')", parameterKind, n.Name, thing, n.Type, o.Type);
+ }
+ }
+ }
+ }
+
void CheckAgreement_Parameters(IToken tok, List<Formal> old, List<Formal> nw, string name, string thing, string parameterKind) {
Contract.Requires(tok != null);
Contract.Requires(old != null);
|