Represent declaration collections as maps of IDs to values

[shonfeder]

We currently cache the various declarations of a spec as sequences of terms:

https://github.com/informalsystems/apalache/blob/271ae9ae8bdaade091724dc5eeabe76eb595cfce/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDecl.scala#L21-L35

Then when we want to check whether particular properties of the declarations hold, we need need to iterate through these sequences. E.g.:

https://github.com/informalsystems/apalache/blob/271ae9ae8bdaade091724dc5eeabe76eb595cfce/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala#L277

and

https://github.com/informalsystems/apalache/blob/271ae9ae8bdaade091724dc5eeabe76eb595cfce/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala#L57

These traversals will be linear on the number of declarations in a spec in the worst case, but we could get O(1) for this kind of thing if the declarations were instead represented by maps.

[konnov]

The complexity note is correct. However, we usually do not have more than 30-40 declarations. We wanted to keep the order of the declarations, since we output the specs in various places. I think the type checker even relies on the linear order of declarations. Let's first try to identify the potential breaking changes.

[shonfeder]

Ah, if the spec size is always small and we don’t have to do repeated lookups, then probably not worth it to optimize. Tho we might still want to use something like a ListMap () just for more ergonomic lookups.

We could get both constant lookups and preserve the order by implementing a class that stored the list of keys in insertion order alongside a rhe map of names to values.

[konnov]

ListMap could be a good approach

[shonfeder]

List map is good for ergonomics (we could ditch some other code, I think, like BodyMap), but it doesn't give constant time lookups.

[shonfeder]

Just realized I was wrong about these caching the sequences: iiuc, they compute the sequences on invocation. This mean that on each invocation we re-filter out the subset of relevant declarations to form a new sequence, e.g., iiuc, we'll traverse all the declarations in the module 3 times in the following:

    val vcTraceInvs = module.operDeclarations.filter(d => d.name.startsWith(NormalizedNames.VC_TRACE_INV_PREFIX))
    val vcNotTraceInvs = module.operDeclarations.filter(d => d.name.startsWith(NormalizedNames.VC_NOT_TRACE_INV_PREFIX))
    // ...
    val optView = module.operDeclarations.find(_.name == NormalizedNames.VC_VIEW).map(_.body)

Since the base declarations attribute in the TlaModule is immutable, this may be a good place for lazy vals, which won't compute their value until we invoke them, but will then cache the result for future lookups.

[shonfeder]

(of course, this is still just a micro optimization if we only ever have small numbers of declarations :) ).