Otherwise the already computed weights of an operator can
rely on the arity of the operator before the dependence on
parameters of the definition (`Foo(x) == INSTANCE Inner`)
is added to the instantiated operator signature.

Parametric instantiation changes the arity of operators,
so the weights list needs to be recomputed, based on the
arity after instantiation has been performed.

This change ensures that the testing commands
are read after the closing horizontal rule (`=====*`)
of the module.

To do this, the nesting depth of submodules is tracked,
by incrementing the counter `submodule_nesting_depth` when
encountering a module opening (`-----*\s*MODULE`), and
decrementing this counter when encountering
a module closing (`=====*`).

Commands are read after the module's end.
Previously, commands were read after the first module closing
(`=====*`), which results in errors in the presence
of submodules.

"VARIABLES" otherwise.

that prints the names of modules in
a module context.

When instantiating inside a LET, definitions are kept,
and other module units omitted. A negative shift is
applied to the remaining module units. This negative shift
should equal minus the number of hypotheses that the
omitted module unit introduces in the context.

The number of hypotheses for each module unit is
computed by the function `M_t.hyps_of_modunit`.

`Module.Elab` replaces each `INSTANCE` statement
with definitions. If the instantiated module
extends the module `TLAPS`, then the definitions
include backend pragmas (constructor `Bpragma`).

`Module.Elab` replaces each `INSTANCE` statement
with definitions. If the instantiated module
extends the module `TLAPS`, then the definitions
include backend pragmas (constructor `Bpragma`).

…nstance

This change makes fingerprints take into account
the result of the proof directive AutoUSE.

Previously, fingerprinting was done before any
expansion of definitions, normalization, and
automated expansion of definitions, expansion of
ENABLED and of \cdot.

This approach worked correctly for BY DEF definitions,
because those definitions were included in the
fingerprint as context.

With this change, only for proof obligations that
include the proof directive AutoUSE, the fingerprint
is computed after expansion of definitions, normalization,
automated expansion of definitions, expansion of ENABLED,
and of \cdot. This change ensures that the proof
obligation is fingerprinted with all automatic
expansions of definitions applied.

A test is added that catches this error.

summary of changes

- test fingerprints by running `tlapm` twice
- add new proof directive `ENABLEDrules`
- rewrite `ENABLEDaxioms` to remove the
  Boolean typeness assumptions
- rewrite two proof rules that previously were in
  `ENABLEDaxioms` and now are in `ENABLEDrules`,
  to remove the Boolean typeness assumptions
- correct soundness check for `ENABLEDrules`
  (previously for `ENABLEDaxioms`)
- fingerprint the level correctness of proof obligations
- revise renaming of variables in `ExpandENABLED`

- removal of older implementation of `ENABLEDaxioms`
- `ENABLEDaxioms` was not correctly collecting primed variables
- use expression level in fingerprint of definition
- record name of `Bpragma` in fingerprint
- implement rewriting system for `ENABLEDrewrites`
- add new proof directive `ENABLEDrewrites`
- add test modules

These changes are for now kept as a separate
commit, in case further rebasing is needed
before preparing the pull request for the
branch `update_enabled_cdot`.

… in ocaml 4.13

Signed-off-by: Karolis Petrauskas <[email protected]>

Signed-off-by: Karolis Petrauskas <[email protected]>

Signed-off-by: Karolis Petrauskas <[email protected]>

Signed-off-by: Karolis Petrauskas <[email protected]>

Signed-off-by: Karolis Petrauskas <[email protected]>

Signed-off-by: Karolis Petrauskas <[email protected]>

Signed-off-by: Karolis Petrauskas <[email protected]>

Signed-off-by: Karolis Petrauskas <[email protected]>