Search code examples
alloy

Declaring a field as `f: elems[g] -> one h` is producing a name-not-found error. What am I missing?


In a model I am writing, I would like to say that a reading of a manuscript identifies a sequence of tokens in the manuscript and maps them to types; the mapping should be defined for all tokens in the manuscript and should identify exactly one type for each token. (Types and tokens here are as described by Peirce's type/token distinction.)

When I write

sig Document, Type, Token {}
sig Reading {
  doc: Document,
  tokens: seq Token,
  mapping:  elems[tokens] -> one Type
}
run {} for 3

an attempt to execute the run command produces the error message

The name "elems" cannot be found.

If I replace elems[tokens] with seq/Int.tokens (borrowing from the definition of elems in util/sequiv) or (simplifying) Int.tokens or univ.tokens, I get the results I expect.

If I replace elems[tokens] with ran[tokens] (and include open util/relation), I get a similar complaint about the name ran.

Using these names elsewhere in the model (not shown) does not elicit this error, so I infer that the problem is not that the functions in question are unknown but that function invocations are unwelcome in the right hand side of a field declaration.

The grammar says of the right-hand side of a field declaration only that it is an expression, and function invocations are allowed as expressions. So I suppose there is a constraint expressed elsewhere that explains why my initial formulation does not work. Can anyone tell me what it is?

I can make do with univ.tokens for now, but I would prefer the original formulation as easier for my expected readers to understand -- they can squint and think of it as a function call, whereas with dot join I need to pause to explain it to them, which distracts from the core task of the model. My thanks for any help.


Solution

  • I toyed a bit with the example and it seems your inference is correct. One can't reference a function in field declarations (even if the grammar states otherwise)

    What you proposed (univ.tokens or Int.tokens) is for me the cleanest workaround.

    What Peter proposed in his comment does indeed the trick, but redefining elems looks too fishy, especially since the elems function is already clearly defined for your readers. It could be a source of confusion.

    Another idea if you really really insist on using elems[token] would be to define mapping as a relation from Token to Type and then to constrain the left-handside of the relation to consist only of those Token present in the sequence. Here would then be your model:

    sig Document, Type, Token {}
    sig Reading {
      doc: Document,
      tokens: seq Token,
      mapping: Token -> one Type
    }{
        mapping.Type =elems[tokens]
    }
    
    run {} for 3