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] Submodule with structural assignment hangs while loading #1439

Closed
WeeknightMVP opened this issue Sep 20, 2022 · 1 comment
Assignees
Labels
bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules

Comments

@WeeknightMVP
Copy link

WeeknightMVP commented Sep 20, 2022

// T.cry
module T where
  // sanity check: functions outside submodule each load
  f : {n} [1][n] -> [n]
  f [x] = x

  p : {a,b} (a,b) -> a
  p (x,_) = x

  interface submodule I where
    type n : #

  submodule F where
    import interface submodule I

    h : [1][n] -> [n]
    h [x] = x         // hangs
    // h = f             // loads
    // h = head          // loads
    // h x = x @ 0       // loads

    g : {m} [1][m] -> [m]
    g [x] = x         // hangs
    // g = f             // loads
    // g = head          // loads
    // g x = x @ 0       // loads

    q : {b} (b,_) -> b
    q (x,_) = x       // hangs
    // q x = x.0         // hangs
    // q x = y           // hangs
    //   where
    //     (y,z) = x
    // q = p             // loads
    // q = undefined     // loads

  submodule P1 where
    type n = 1

  submodule S = submodule F { submodule P1 }

  import submodule S
$ git clone https://github.com/GaloisInc/cryptol
$ cd cryptol
$ git submodule update --init --recursive
$ git switch functors-merge
$ ./cry build
$ ./cry run
Cryptol> :l T.cry
Loading module Cryptol
Loading module T
[hangs]

Submodule definitions with structural assignments or tuple accessors (regardless of interface imports or parameter use) cause load attempts to hang, whereas corresponding definitions outside submodules load quickly.

@yav yav self-assigned this Sep 21, 2022
@yav yav added bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules labels Sep 21, 2022
yav added a commit that referenced this issue Sep 22, 2022
This fixes #1439

See the comment on the new function `selectorScope`
for details.
@yav
Copy link
Member

yav commented Sep 22, 2022

Thanks for reporting this! I just pushed a commit that should hopefully solve the issue. Please let us know if you encounter any other issues.

@yav yav closed this as completed Oct 13, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
Development

No branches or pull requests

2 participants