Update the language manual on modules

[konnov]

We have to update the manual with the description of import ... from.

[bugarela]

@konnov I think this is a duplicate of https://github.com/informalsystems/quint/issues/530, which is the next item in my queue. I can assign it to you if you want to do it :smile:

[shonfeder]

We should include docs on how to use modules to structure specs, and the limits of that usage.

As a special case, we should makes sure to document how module parameters (i.e. "constants") are "inherited" via importing modules. E.g.,

module m {
  const C:int
}

module n {
  import m.*

  def c = C
}

module o {
  import n(C=42) as n_inst
  def c = n_inst::c
}

Gives us

$  echo 'c' | quint -r t.qnt::o
Quint REPL 0.18.1
Type ".exit" to exit, or ".help" for more information
>>> c
42
>>> 

This was discussed with @p-offtermatt today.

Also relevant is whether this behavior and syntax is really ideal, or if we should find a way to make this much more explicit. See https://github.com/informalsystems/quint/discussions/949 for previous related discussion.

I take fully documenting our current module behavior to be a step towards evaluating whether it is suitable and to thinking carefully about what alternatives we might prefer.

[bugarela]

Just a note: that only works if C is referenced somehow in n. If it is not, we get a flattening error:

module m {
  const C:int
}

module n {
  import m.*

}

module o {
  import n(C=42) as n_inst
  def c = n_inst::C
}

Error: Internal error while flattening [QNT406] Instantiation error: 'C' not found in 'n',[QNT404] Name 'n_inst::C' not found,[QNT404] Name 'n_inst::C' not found