Re: [tlaplus] Arity of NEW operator in `tlapm`

[Ioannis Filippidis <jfili...@xxxxxxxxx>]

On Thu, May 11, 2017 at 2:45 PM, Ioannis Filippidis <jfili...@xxxxxxxxx> wrote:

```
****** SANY2 Version 2.1 created 24 February 2014

Parsing file test.tla
Parsing file /some/path/v2-tlapm/library/FiniteSets.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Naturals.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module test
Semantic errors:

*** Errors: 1

line 14, col 40 to line 14, col 45 of module test

Function 'f' is defined with 1 parameters, but is applied to 2 arguments.
```

This message appears to originate from the following area of code [1]:

```
            // If the function appears with numArgs >= 2 argument
            // expressions, it must be declared with exactly numArgs
            // parameters; and a function with numParms parameters in
            // its definition should be applied to exactly numParms
            // expressions, or 1 _expression_ (representing arguments in
            // tuple form), or 0 expressions (representing the
            // function itself).  Note: one cannot define a function
            // with 0 arguments in TLA+.
            if ( numArgs >= 2 && numParms != numArgs ) {
              errors.addError(treeNode.getLocation(),
                              "Function '" +
                                ((OpApplNode)sns[0]).getOperator().getName() +
                              "' is defined with " + numParms +
                              " parameters, but is applied to " +
                              numArgs + " arguments.");
              return nullOAN;
```

[1] https://github.com/tlaplus/tlaplus/blob/5527a0c0f6bbc18e0685bd1db302cda52f2236d3/tlatools/src/tla2sany/semantic/Generator.java#L3317

Best regards,

ioannis