Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[New module system] Cryptol Prelude not available when instantiating top-level modules #1455

Closed
yav opened this issue Oct 13, 2022 · 4 comments · Fixed by #1559
Closed

[New module system] Cryptol Prelude not available when instantiating top-level modules #1455

yav opened this issue Oct 13, 2022 · 4 comments · Fixed by #1559
Assignees
Labels
command-line-repl Related to Cryptol's text-based UI importing instantiations parameterized modules Related to Cryptol's parameterized modules UX Issues related to the user experience (e.g., improved error messages)

Comments

@yav
Copy link
Member

yav commented Oct 13, 2022

Here are some examples:

// in file F.cry
module F where
  parameter
    y : [32]
  f x = x + y

// In file A.cry
module A where
  y = 5

// In file X.cry
module X = F where
   y = 5

// In file Y.cry
module Y = F { A }

When loading X.cry or Y.cry the modules load correctly and the things defined in them are accessible, but things from the Cryptol Prelude are not. For example:

f 2 == 5

Complains with == is not defined. Using the :browse confirms that the Cryptol Prelude is not in scope.

@yav yav added bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules labels Oct 13, 2022
@yav yav changed the title Cryptol Prelude not available when instantiating top-level modules [New module system] Cryptol Prelude not available when instantiating top-level modules Oct 13, 2022
@yav yav self-assigned this Oct 13, 2022
@yav
Copy link
Member Author

yav commented Oct 13, 2022

Upon further investigation, the same thing would happen when instantiating any module, not just top level ones---it is just that we have no way to look inside those directly.

This happens because module instantiations, such as module M = F { X } are synthetic modules and so it is not really clear what should be "in scope" for them---we know what's in scope in F and X separately but what about M? This is not really important when writing normal Cryptol programs, as there is no way to check what's in scope in a module. However, when exploring such a module at the REPL, is would be convenient to have some more stuff available, rather than just what's defined by M, which is the current behavior. Some possibilities:

  1. Use the things that are in scope of F, but with the defined things replaced by M's instantiated definitions
  2. Use the things that are in scope at the location where M is defined
  3. Some sort of combination of (1) and (2) (i.e., the things in scope at M + things imported by F + things defined by M)
  4. Treat this as a special case and say that on the REPL you can access the Prelude + whatever is defined in the module.

(2) wouldn't really work for top-level modules as, again, nothing is in scope there
(1) is probably more intuitive, although it could be confusing as normal nested modules and instantiations could behave quite differently (although currently we have no way to "go inside" nested modules at the REPL, but it'd be nice to come up with a consistent behavior, that would be compatible with such a feature)
(4) seems somewhat ad-hoc
(3) might be the most intuitive, as it is what you'd get if you were to write the definition of M by hand (i.e., copy pasted the functor and replaced the instantiated things)

@yav yav added command-line-repl Related to Cryptol's text-based UI UX Issues related to the user experience (e.g., improved error messages) importing instantiations and removed bug Something not working correctly labels Oct 13, 2022
@qsctr qsctr self-assigned this Jul 24, 2023
@yav
Copy link
Member Author

yav commented Jul 24, 2023

While we are implementing a solution for this, a quick workaround is to import that instantiated module into a separate file and load that into the REPL. Here is an example:

module A where                                                                   
  parameter                                                                           
    x : [8]                                                                        
  a = x + 1  

module B where                                                                   
  x = 2   

module C = A { B }       

module Test where
  import C

Cryptol> :load Test
Main> 2 * a
0x06

@qsctr
Copy link
Contributor

qsctr commented Jul 25, 2023

We are working on implementing option 1 from #1455 (comment). Currently, since there is no way to focus on submodules in the REPL, options 1 and 3 behave the same. When we do implement focusing on submodules at some point, the difference is that option 3 would also bring surrounding names from the parent module into scope when loading an instantiated submodule, while option 1 would not. We can explore implementing the additional names for option 3 later on when we implement focusing on submodules.

Turns out implementing option 3 wasn't really harder than option 1 so we just did option 3.

@qsctr
Copy link
Contributor

qsctr commented Jul 27, 2023

Since this has not been mentioned explicitly yet: in particular, the instantiations of the functor parameters will also be in scope at the REPL when the instantiated module is focused.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
command-line-repl Related to Cryptol's text-based UI importing instantiations parameterized modules Related to Cryptol's parameterized modules UX Issues related to the user experience (e.g., improved error messages)
Projects
None yet
2 participants