-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Improve rules for nameonly/positional/nameless and required/optional … #3864
Changes from 2 commits
6a10fc5
5377a31
837505d
75b30b1
47b323c
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -4673,26 +4673,53 @@ public void ResolveParameterDefaultValues(List<Formal> formals, ResolutionContex | |
|
||
Contract.Assume(AllTypeConstraints.Count == 0); | ||
|
||
// Formal parameters have three ways to indicate how they are to be passed in: | ||
// * nameonly: the only way to give a specific argument value is to name the parameter | ||
// * positional only: these are nameless parameters (which are allowed only for datatype constructor parameters) | ||
// * either positional or by name: this is the most common parameter | ||
// A parameter is either required or optional: | ||
// * required: a caller has to supply an argument | ||
// * optional: the parameter has a default value that is used if a caller omits passing a specific argument | ||
// | ||
// The syntax for giving a positional-only (i.e., nameless) parameter does not a default-value expression, so | ||
// a positional-only parameter is always required. | ||
// | ||
// At a call site, positional arguments are not allowed to follow named arguments. Therefore, if "x" is | ||
// a nameonly parameter, then there is no way to supply the parameters after "x" by position. Thus, any | ||
// parameter that follows "x" must either by passed by name or have a default value. That is, if a later | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
|
||
// parameter does not have a default value, it is _effectively_ nameonly. We impose the rule that | ||
// * an effectively nameonly parameter must be declared as nameonly | ||
// | ||
// For a positional-only parameter "x", every parameter preceding "x" is _effectively_ required. We impose | ||
// the rule that | ||
// * an effectively required parameter must not have a default-value expression | ||
var dependencies = new Graph<IVariable>(); | ||
var allowMoreRequiredParameters = true; | ||
var allowNamelessParameters = true; | ||
string nameOfMostRecentNameonlyParameter = null; | ||
var previousParametersWithDefaultValue = new HashSet<Formal>(); | ||
foreach (var formal in formals) { | ||
if (!formal.HasName) { | ||
foreach (var previousFormal in previousParametersWithDefaultValue) { | ||
reporter.Error(MessageSource.Resolver, previousFormal.DefaultValue.tok, | ||
$"because of a later nameless parameter, this default value is never used; remove it or name all subsequent parameters"); | ||
} | ||
previousParametersWithDefaultValue.Clear(); | ||
} | ||
var d = formal.DefaultValue; | ||
if (d != null) { | ||
allowMoreRequiredParameters = false; | ||
ResolveExpression(d, resolutionContext); | ||
AddAssignableConstraint(d.tok, formal.Type, d.Type, "default-value expression (of type '{1}') is not assignable to formal (of type '{0}')"); | ||
foreach (var v in FreeVariables(d)) { | ||
dependencies.AddEdge(formal, v); | ||
} | ||
} else if (!allowMoreRequiredParameters) { | ||
reporter.Error(MessageSource.Resolver, formal.tok, "a required parameter must precede all optional parameters"); | ||
} | ||
if (!allowNamelessParameters && !formal.HasName) { | ||
reporter.Error(MessageSource.Resolver, formal.tok, "a nameless parameter must precede all nameonly parameters"); | ||
previousParametersWithDefaultValue.Add(formal); | ||
} else if (nameOfMostRecentNameonlyParameter != null && !formal.IsNameOnly) { | ||
// "formal" is preceded by a nameonly parameter, but itself is neither nameonly nor has a default value | ||
reporter.Error(MessageSource.Resolver, formal.tok, | ||
$"this parameter is effectively nameonly (because of the earlier nameonly parameter '{nameOfMostRecentNameonlyParameter}'); " + | ||
"declare it as nameonly or give it an default-value expression"); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
|
||
} | ||
if (formal.IsNameOnly) { | ||
allowNamelessParameters = false; | ||
nameOfMostRecentNameonlyParameter = formal.Name; | ||
} | ||
} | ||
SolveAllTypeConstraints(); | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -198,11 +198,11 @@ module TypesAreDetermined { | |
datatype Record = Record(y: int := F()) // error: type parameter X not determined | ||
} | ||
|
||
module RequiresBeforeOptional { | ||
datatype Color = Blue(x: int := y, y: int) // error: required parameters must precede optional parameters | ||
iterator Iter(x: int := y, y: int) // error: required parameters must precede optional parameters (reported twice) | ||
lemma Lemma(x: int := y, y: int) // error: required parameters must precede optional parameters | ||
least predicate Least(x: int := y, y: int) // error: required parameters must precede optional parameters | ||
module RequiredBeforeOptional { | ||
datatype Color = Blue(x: int := y, y: int) | ||
iterator Iter(x: int := y, y: int) | ||
lemma Lemma(x: int := y, y: int) | ||
least predicate Least(x: int := y, y: int) | ||
} | ||
|
||
module TwoState { | ||
|
@@ -275,15 +275,15 @@ module NameOnlyParameters { | |
least predicate LP(a: int, nameonly b: int, c: int := 100) | ||
static greatest predicate GP(a: int, nameonly b: int := 75, c: int := 100) | ||
} | ||
iterator Iter(nameonly u: int, x: int) | ||
iterator Iter(nameonly u: int, x: int) // error (x2, because of the desugaring of iterators): x is effectively nameonly, but not declared as such | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Maybe we should come up with a testing file format where you can specify the expected error messages inline : ) There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I do like being able to read the expected outcome in the test file itself. Therefore, I always put such "error" comments in the tests. But these comments aren't the exact error messages, don't capture column information, and in some cases are even placed only on a nearby line. It's plausible that we could turn these into a formally recognized testing file format. |
||
datatype D = | ||
| DD(a: int, nameonly b: int) | ||
| DE(int, 0: int, real, nameonly 1: int, c: int) | ||
| DE(int, 0: int, real, nameonly 1: int, c: int) // error: c is effective nameonly, but not declared as such | ||
| DF(800: int, nameonly 900: int, 9_0_0: int := 100) | ||
datatype E = | ||
| E0(a: int, b: int := 6, int) // error: required parameters must preceded optional parameters | ||
| E1(a: int, nameonly b: int := 6, u: int) // error: required parameters must preceded optional parameters | ||
| E2(a: int, nameonly b: int, int) // error: after a 'nameonly' parameter, all remaining parameters must have names | ||
| E0(a: int, b: int := 6, int) // error: there is no way for the default value of 'b' to be used | ||
| E1(a: int, nameonly b: int := 6, u: int) // u is effectively nameonly | ||
| E2(a: int, nameonly b: int, int) // error: after a 'nameonly' parameter, all remaining parameters must be nameonly or have a default value | ||
|
||
method Test() { | ||
var c: C; | ||
|
@@ -355,4 +355,26 @@ module NameOnlyParameters { | |
d := DF(2, 0900 := 3, 9_0_0 := 4); // error (x2): no parameter is named '0900'; no argument passed for parameter '900' | ||
d := DF(2, 900 := 3, 90_0 := 4); // error: no parameter is named '90_0' | ||
} | ||
|
||
// Issue 3859 | ||
datatype Foo = Foo(nameonly bar: string := "", nameonly baz: string, qux: int := 8) | ||
function FooF(nameonly bar: string := "", nameonly baz: string, qux: int := 8): int | ||
method FooM(nameonly bar: string := "", nameonly baz: string, qux: int := 8) | ||
|
||
datatype XFoo = XFoo(bar: string := "", nameonly baz: string, qux: int := 8) | ||
function XFooF(bar: string := "", nameonly baz: string, qux: int := 8): int | ||
method XFooM(bar: string := "", nameonly baz: string, qux: int := 8) | ||
|
||
datatype YFoo = YFoo(bar: string := "", nameonly baz: string, qux: int := 8, ohno: int, quux: real := 2.0) // error: onho is effectively nameonly, but not declared as such | ||
function YFooF(bar: string := "", nameonly baz: string, qux: int := 8, ohno: int, quux: real := 2.0): int // error: onho is effectively nameonly, but not declared as such | ||
method YFooM(bar: string := "", nameonly baz: string, qux: int := 8, ohno: int, quux: real := 2.0) // error: onho is effectively nameonly, but not declared as such | ||
|
||
method FooUse() { | ||
var f := Foo(baz := "yeah"); | ||
f := Foo(baz := "yeah", bar := "fun"); | ||
f := Foo(bar := "fun", baz := "yeah", qux := 10); | ||
f := Foo(qux := 10, baz := "yeah"); | ||
f := Foo(); // error: baz is missing | ||
var y := YFoo(baz := "a", ohno := 21); | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Improved rules for nameonly parameters and parameter default-value expressions |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
does not a
=>does not allow a