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] Instantiate functor while importing #1368

Closed
Tracked by #1363
rybla opened this issue Jun 21, 2022 · 1 comment
Closed
Tracked by #1363

[New module system] Instantiate functor while importing #1368

rybla opened this issue Jun 21, 2022 · 1 comment
Assignees
Labels
language Changes or extensions to the language parameterized modules Related to Cryptol's parameterized modules

Comments

@rybla
Copy link
Collaborator

rybla commented Jun 21, 2022

#1363 feature request

I would be extremely convenient to be able to instantiate a functor while importing it. The following example demonstrates how a module App can import a functor Lib by instantiating it with I_inst an instance of the interface I that Lib is parametrized by.

module interface I where
a : *
x : a

module I_inst = I where
a = [8]
x = 1

module Lib where
import interface I

module App where
import Lib { I = I_inst }

Additionally, the following example demonstrates how a module App can import a functor Lib that is parametrized by an anonymous module (encoded by the parameter syntax) by immediately instantiating its parameters right after the import statement using a where clause.

module Lib where
parameter
  a : *
  x : a

module App where
import Lib where
  a = [8]
  x = 1
@rybla rybla added parameterized modules Related to Cryptol's parameterized modules language Changes or extensions to the language labels Jun 21, 2022
@rybla rybla changed the title Instantiate functor while importing [New module system] Instantiate functor while importing Jun 23, 2022
@yav yav self-assigned this Jul 14, 2022
@m-yac
Copy link
Contributor

m-yac commented Jul 14, 2022

Fixed in #1363.

@m-yac m-yac closed this as completed Jul 14, 2022
@m-yac m-yac mentioned this issue Jul 14, 2022
8 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
language Changes or extensions to the language parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
Development

No branches or pull requests

3 participants