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 by 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 parametes 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. 
+
+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.
+
+Formal parameters may also be declared `nameonly`, in which case a call site
+must explicitly name the formal when providing its actual argument.
+
+The above function may be called as
+<!-- %no-check -->
+```dafny
+var k := f(y:=10, x:=2);
+```
+using names; here, though there are no `nameonly` parameters so the names may be used 
+or the actual arguments may be given in order.
+
+If a function is declared with a `nameonly` formal, then that formal's value must be given with a named assignment.
+For example, a function `ff` declared as
+<!-- %check-resolve -->
+```dafny
+function ff(x: int, nameonly y: int): int
+```
+may be called only using `ff(0, y := 4)`. 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.
+Otherwise an error will result when an attempt is made to call the function or method with such a formal list.
+
+The formals of datatype constructors are not required to have names. Such formals may have default values but
+may not be declared `nameonly`. Such nameless formals must be declared before `nameonly` formals.
+
+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.