Documentation of nameonly and default values for formals

docs/DafnyRef/Expressions.md

@@ -1825,6 +1825,21 @@ Method calls, object-allocation calls (`new`), function calls, and
 datatype constructors can be called with both positional arguments
 and named arguments.
 
+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 allow 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 be passed by name or have a default value. 
+That is, if a later (in the formal parameter declaration) parameter does not have a default value, it is effectively nameonly. 
+
 Positional arguments must be given before any named arguments.
 Positional arguments are passed to the formals in the corresponding
 position. Named arguments are passed to the formal of the given
@@ -1837,32 +1852,7 @@ value for each optional parameter, and must never name
 non-existent formals. Any optional parameter that is not given a value
 takes on the default value declared in the callee for that optional parameter.
 
-## 9.37. Formal Parameters and Default-Value Expressions
-
-The formal parameters of a method, constructor in a class, iterator,
-function, or datatype constructor can be declared with an expression
-denoting a _default value_. This makes the parameter _optional_,
-as opposed to _required_. All required parameters must be declared
-before any optional parameters. All nameless parameters in a datatype
-constructor must be declared before any `nameonly` parameters.
-
-The default-value expression for a parameter is allowed to mention the
-other parameters, including `this` (for instance methods and instance
-functions), but not the implicit `_k` parameter in least and greatest
-predicates and lemmas. The default value of a parameter may mention
-both preceding and subsequent parameters, but there may not be any
-dependent cycle between the parameters and their default-value
-expressions.
-
-The well-formedness of default-value expressions is checked independent
-of the precondition of the enclosing declaration. For a function, the
-parameter default-value expressions may only read what the function's
-`reads` clause allows. For a datatype constructor, parameter default-value
-expressions may not read anything. A default-value expression may not be
-involved in any recursive or mutually recursive calls with the enclosing
-declaration.
-
-## 9.38. Compile-Time Constants {#sec-compile-time-constants}
+## 9.37. Compile-Time Constants {#sec-compile-time-constants}
 
 In certain situations in Dafny it is helpful to know what the value of a
 constant is during program analysis, before verification or execution takes
@@ -1903,7 +1893,7 @@ In Dafny, the following expressions are compile-time constants[^CTC], recursivel
 
 [^CTC]: This set of operations that are constant-folded may be enlarged in future versions of `dafny`.
 
-## 9.39. List of specification expressions {#sec-list-of-specification-expressions}
+## 9.38. List of specification expressions {#sec-list-of-specification-expressions}
 
 The following is a list of expressions that can only appear in specification contexts or in ghost blocks.
 

docs/DafnyRef/Types.md

@@ -1886,7 +1886,7 @@ Furthermore, for the compiler to be able to make an appropriate choice of
 representation, the constants in the defining expression as shown above must be
 known constants at compile-time. They need not be numeric literals; combinations
 of basic operations and symbolic constants are also allowed as described
-in [Section 9.38](#sec-compile-time-constants).
+in [Section 9.37](#sec-compile-time-constants).
 
 ### 5.7.1. Conversion operations {#sec-conversion}
 
@@ -4502,4 +4502,65 @@ imposed on the body of `ReachableVia` makes sure that, if the
 predicate returns `true`, then every object reference in `p` is as old
 as some object reference in another parameter to the predicate.
 
+## 6.5. Nameonly Formal Parameters and Default-Value Expressions
+
+A formal parameter of a method, constructor in a class, iterator,
+function, or datatype constructor can be declared with an expression
+denoting a _default value_. This makes the parameter _optional_,
+as opposed to _required_.
+
+For example,
+<!-- %check-resolve %save f.tmp -->
+```dafny
+function f(x: int, y: int := 10): int
+```
+may be called as either
+<!-- %check-resolve %use f.tmp -->
+```dafny
+const i := f(1, 2);
+const j := f(1);
+```
+where `f(1)` is equivalent to `f(1, 10)` in this case.
+
+The above function may also be called as
+<!-- %no-check -->
+```dafny
+var k := f(y := 10, x := 2);
+```
+using names; actual arguments with names may be given in any order,
+though they must be after actual arguments without names. 
+
+Formal parameters may also be declared `nameonly`, in which case a call site
+must always explicitly name the formal when providing its actual argument.
+
+For example, a function `ff` declared as
+<!-- %check-resolve -->
+```dafny
+function ff(x: int, nameonly y: int): int
+```
+must be called either by listing the value for x and then y with a name, 
+as in `ff(0, y := 4)` or by giving both actuals by name (in any order). 
+A `nameonly` formal may also have a default value and thus be optional.
+
+Any formals after a `nameonly` formal must either be `nameonly` themselves or have default values.
+
+The formals of datatype constructors are not required to have names.
+A nameless formal may not have a default value, nor may it follow a formal
+that has a default value.
+
+The default-value expression for a parameter is allowed to mention the
+other parameters, including `this` (for instance methods and instance
+functions), but not the implicit `_k` parameter in least and greatest
+predicates and lemmas. The default value of a parameter may mention
+both preceding and subsequent parameters, but there may not be any
+dependent cycle between the parameters and their default-value
+expressions.
+
+The well-formedness of default-value expressions is checked independent
+of the precondition of the enclosing declaration. For a function, the
+parameter default-value expressions may only read what the function's
+`reads` clause allows. For a datatype constructor, parameter default-value
+expressions may not read anything. A default-value expression may not be
+involved in any recursive or mutually recursive calls with the enclosing
+declaration.