Add import with function renaming

[robby-phd]

Cryptol currently support qualified imports to avoid function name clashes.
For example, consider AES S-Box and T-Box specifications whose top-level encryption and decryption functions are named aesEncrypt and aesDecrypt, respectively.

When trying to prove equivalences of their specification, one can currently use Cryptol qualified imports as follows:

// import aesEncrypt and aesDecrypt in AES as qualified names AESSBox::aesEncrypt and AESSBox::aesDecrypt
import AES as AESSBox(aesEncrypt, aesDecrypt)

// import aesEncrypt and aesDecrypt in AESTBox as qualified names AESTBox::aesEncrypt and AESTBox::aesDecrypt
import AESTBox as AESTBox(aesEncrypt, aesDecrypt)

Another approach that would be nice to have is renaming the imported functions, as follows:

// import function aesEncrypt and aesDecrypt in AES as top-level functions sboxEncrypt and sboxDecrypt
import AES(aesEncrypt => sboxEncrypt, aesDecrypt => sboxDecrypt)

// import function aesEncrypt and aesDecrypt in AESTBox as top-level functions tboxEncrypt and tboxDecrypt
import AESTBox(aesEncrypt => tboxEncrypt, aesDecrypt => tboxDecrypt)

This way, one can use unqualified names to refer to the functions, which would be especially useful for long module names.

[yav]

You should be able to get a very similar result like this:

import AES as SBox
import AESTBox as TBox

sboxEncrypt = SBox::aesEncrypt
sboxDecrypt = SBox::aesDecrypt
tboxEncrypt = TBox::aesEncrypt
tboxDecrypt = TBox::aesDecrypt

[robby-phd]

Sure, that also works.

[brianhuffman]

It seems like we have an acceptable workaround, so I'm closing this one.