Importing Infix Operators

[smithnormform]

Is it possible to import infix operators (both at the type and value levels) without importing the entire module?

For example, here I define monus:

module foo::monus where 

infixl 80 ∸

type a ∸ b = max a b - b

(∸) : {a} (Cmp a, Ring a) =>
a ∸ b = if a > b then a - b else zero

The commented lines in the following fail (they also fail after adding parentheses around ∸), but importing everything succeeds:

module foo::example where

/* import foo::monus(∸)
 * x = 5 ∸ 2
 */

/* import foo::monus as monus
 * x = 5 (monus::∸) 2
 */

import foo::monus

x = 5 ∸ 2

[brianhuffman]

Apparently Cryptol doesn't allow infix operators in import lists at the moment. It would be good to add support for this.

Haskell does support infix operators in import lists; the syntax is to put parens around the operator. I suggest we do the same. So we ought to be able to write an import declaration like this:

import Monus((∸))

or, if imported with other items from the same module, like this:

import Monus(foo, bar, (∸), baz)

[robdockins]

Do we also need to have a way to specify the namespace? Suppose you want to import a type operator, but not a value operator that share a name (operator or otherwise); or vice-versa...

[brianhuffman]

I'm pretty sure we don't. We should probably open a separate ticket for that, because it would make sense to implement that feature separately.