diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index ee6e9bc0b5e..5a3261a6b1c 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -40,7 +40,9 @@ public partial class PreTypeResolver { } else if (expr is NegationExpression) { var e = (NegationExpression)expr; ResolveExpression(e.E, resolutionContext); - e.PreType = e.E.PreType; + e.PreType = CreatePreTypeProxy("result of unary -"); + AddSubtypeConstraint(e.PreType, e.E.PreType, e.E.tok, + $"type of argument to unary - ({{1}}) must agree with the result type ({{0}})"); AddConfirmation(PreTypeConstraints.CommonConfirmationBag.NumericOrBitvector, e.E.PreType, e.E.tok, "type of unary - must be of a numeric or bitvector type (instead got {0})"); // Note, e.ResolvedExpression will be filled in during CheckTypeInference, at which time e.PreType has been determined diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs b/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs index 474ae83373f..855a427baaa 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs @@ -174,7 +174,7 @@ class PreTypeToTypeVisitor : ASTVisitor { } // Case: fixed pre-type type - if (expr is LiteralExpr or ThisExpr or UnaryExpr or BinaryExpr) { + if (expr is LiteralExpr or ThisExpr or UnaryExpr or BinaryExpr or NegationExpression) { // Note, for the LiteralExpr "null", we expect to get a possibly-null type, whereas for a reference-type ThisExpr, we expect // to get the non-null type. The .PreType of these two distinguish between those cases, because the latter has a .PrintablePreType // field that gives the non-null type. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy index cfd65a9f6b1..b76128e5e31 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy @@ -962,35 +962,51 @@ module StaticReceivers { } } +module UnaryMinus { + // This modules contains some regression tests to make sure that -nat is an int, not a nat. + // This remains a problem in the old resolver, and was once a problem (for different reasons) + // in the new resolver. -/**************************************************************************************** - ******** TO DO ************************************************************************* - **************************************************************************************** + predicate Simple(n: nat, d: nat) { + var x := -d; // type of x should be inferred to be int, not nat + n == x + } -module StaticReceivers { - ghost predicate Caller0(s: seq, list: LinkedList) - { - s == list.StaticFunction(s) // uses "list" as an object to discard + function Abs(n: int): nat { + if n < 0 then -n else n } - ghost predicate Caller1(s: seq) + predicate IsNat(n: int) + ensures IsNat(n) <==> 0 <= n { - s == LinkedList.StaticFunction(s) // type parameters inferred + AtMost(n, 0) } - ghost predicate Caller2(s: seq) + predicate AtMost(n: int, d: nat) + requires d <= Abs(n) + ensures AtMost(n, d) <==> d <= n + decreases Abs(n) - d { - s == LinkedList.StaticFunction(s) + n == d || (n + d != 0 && AtMost(n, d + 1)) } - method Caller3() + predicate AtMost'(n: int, d: nat) + requires d <= Abs(n) + ensures AtMost'(n, d) <==> d <= n + decreases Abs(n) - d { - var s: seq; - var b := s == LinkedList.StaticFunction(s); + if n == d then + true + else if n == -d then // the -d here should not pose any problems + false + else + AtMost'(n, d + 1) } - class LinkedList { - static ghost function StaticFunction(sq: seq): seq + lemma Same(n: int, d: nat) + requires d <= Abs(n) + ensures AtMost(n, d) == AtMost'(n, d) + { } } @@ -1032,34 +1048,4 @@ datatype Tree = // Dafny rejects the call to MaxF, claiming that forall t | t in ts :: default <= f(t) might not hold. But default is 0 and f(t) // has type nat, so it should hold — and in fact just uncommenting the definition of fn above solves the issue… even if fn isn’t used. - -// ------------------ -// In this program, one has to write "n + d != 0" instead of "n != -d", because of a previously known problem with type inference - -predicate method ge0'(n: int) - ensures ge0'(n) <==> 0 <= n -{ - downup_search'(n, 0) -} - -function method Abs(n: int): nat { - if n < 0 then -n else n -} - -predicate method downup_search'(n: int, d: nat) - requires d <= Abs(n) - ensures downup_search'(n, d) <==> d <= n - decreases Abs(n) - d -{ - n == d || (n + d != 0 && downup_search'(n, d + 1)) - /* - if n - d == 0 then - true - else if n + d == 0 then - false - else - downup_search'(n, d + 1) - */ -} - ****************************************************************************************/ diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect index f8a277ab429..1f4e7c13098 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect @@ -11,4 +11,4 @@ TypeInferenceRefresh.dfy(633,24): Error: value does not satisfy the subset const TypeInferenceRefresh.dfy(145,30): Error: element might not be in domain TypeInferenceRefresh.dfy(216,26): Error: result of operation might violate newtype constraint for 'int8' -Dafny program verifier finished with 77 verified, 10 errors +Dafny program verifier finished with 83 verified, 10 errors diff --git a/docs/dev/news/4737.fix b/docs/dev/news/4737.fix new file mode 100644 index 00000000000..1c51f55dbdf --- /dev/null +++ b/docs/dev/news/4737.fix @@ -0,0 +1 @@ +Fix resolution of unary minus in new resolver