GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

Parameterized modules in the REPL #998

Open ghost opened 3 years ago

ghost commented 3 years ago

How can I interact with a parameterized module when it is loaded in the REPL?

I usually make a second, single line module that "backtick" imports the parameterized one, but I saw in #815 that this is up for removal. It got me wondering if there is (or will be) a way that I can set and change parameters from within the REPL when such a module is loaded.

robdockins commented 3 years ago

We're still in the design phase on the new module system, so things are a bit fluid. Let me see if I understand the use case you are concerned about. You'd like to be able to load a parameterized module at the REPL by setting the parameters directly from the prompt; is that right?

ghost commented 3 years ago

Right. At the REPL, I'd like some way to use the definitions from a parameterized module without needing to make a new file for a specific instantiation or for a "backtick" import like I do now. Otherwise why can I load parameterized modules at all?

I originally intended to ask if a parameterized module could behave as if it was "backtick" imported when loaded with :l, but then I saw the redesign post. If those imports are removed, maybe :l could accept additional arguments for setting parameters from the prompt.

yav commented 3 years ago

Loading an uninstantiated parameterized module is quite useful, for example:

  1. to check that module loads during development, or
  2. so you can browse the contents of a module So we'll likely continue to support loading uninstantiated modules.

The new design is not yet solidified, but one of our goals is to make it more convenient to instantiate parameterized modules, so perhaps this would be less of an issue, but we could still consider some mechanism for setting parameters on the REPL.