You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If we were to allow foreign declarations in nested modules, it is possible to have multiple declarations with the same name, so we'd need some way to disambiguate between them.
To keep thing simple, we should only allow them at the top level. Of course, a nested module could easily define a Cryptol function that simply calls a foreign declaration defined in its ancestor, so this does not really loose any functionality.
The text was updated successfully, but these errors were encountered:
Also we should probably not allow foreign declarations in functors, even if they are top level. This is because it is not clear what should happen to such declarations when the functor is instantiated.
On further though, allowing foreign declarations in nested non-functor modules is OK, as long as no name clashes (i.e., the foreign declaration should all have a different Ident which is what we use to compute the name of the C function)
If we were to allow foreign declarations in nested modules, it is possible to have multiple declarations with the same name, so we'd need some way to disambiguate between them.
To keep thing simple, we should only allow them at the top level. Of course, a nested module could easily define a Cryptol function that simply calls a foreign declaration defined in its ancestor, so this does not really loose any functionality.
The text was updated successfully, but these errors were encountered: