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 123 forks source link

`Connection.modules` does not recognize parameterized module with explicit `interface`(s) as `parameterized` #1756

Closed WeeknightMVP closed 2 days ago

WeeknightMVP commented 6 days ago
modules$ for cry in *.cry; do echo "// $cry"; cat $cry; echo; done
// Functor.cry
module Functor where
  import interface I1
  import interface I2

// I1.cry
interface module I1 where
  type v: *

// I2.cry
interface module I2 where
  type w: *

modules$ export CRYPTOLPATH="$(pwd)"
modules$ python
>>> from pprint import pprint
>>> from cryptol import connect
>>> pprint(load_result := c.load_module('Functor').result())
[]
>>> pprint(modules := c.modules().result())
[{'module': 'Functor', 'parameterized': False},
 {'module': 'Cryptol', 'parameterized': False}]
WeeknightMVP commented 6 days ago

Actually, functors that explicitly import a single interface are also not recognized:

modules$ cat Functor1.cry
module Functor1 where
  import interface I1
modules$ python
Python 3.12.5 (main, Aug 17 2024, 16:46:07) [GCC 9.4.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from pprint import pprint
>>> from cryptol import connect
>>> c = connect()
>>> pprint(load_result := c.load_module('Functor1').result())
[]
>>> pprint(modules := c.modules().result())
[{'module': 'Functor1', 'parameterized': False},
 {'module': 'Cryptol', 'parameterized': False}]