Memoize level computation to avoid exponential behavior

[damiendoligez]

Follow-up to #148 (comment)
Should make #186 unnecessary.

cc @kape1395

[kape1395]

I tried to use these changes with the updated_enabled_cdot branch.
It still takes 10s of seconds to parse the document.

[damiendoligez]

Can you provide the TLA file, if it's not confidential? Do you have a recipe for reproducing the problem on the command line? That would be much more convenient for tracking down the slowdown.

[kape1395]

I'm sorry for the late response.

For example, the slow behaviour can be observed with https://github.com/tlaplus/CommunityModules/blob/master/modules/FiniteSetsExt_theorems_proofs.tla and tlapm build from branch https://github.com/tlaplus/tlapm/tree/updated_enabled_cdot-optimize-level-computation.

The VSCode/LSP blocks for 5-8 seconds on my machine after each edit (or before the proof step icons are shown).
But maybe that's related to the parser's use in LSP, since running tlapm --toolbox 0 0 FiniteSetsExt_theorems_proofs.tla doesn't look slow. At least it doesn't wait 5 seconds before reporting the first obligations.