[RPC] Finish cleaning cryptoltypes.py

[m-yac]

This PR finishes cleaning up cryptoltypes.py, specifically:

• Finishes adding classes for all of the currently implemented Cryptol props (see Cryptol.TypeCheck.TCon and CryptolServer.Data.Type)
• Adds class for lengthFromTo type operator
• Adds type annotations for all instance variables
• Finishes implementing __str__ methods for all Cryptol types
• Uses @dataclass everywhere possible to avoid writing __repr__ and __eq__ methods
• Adds more docstrings
• Adds comments delineating sections

[pnwamk]

LGTM modulo minor comments.

[yav]

I haven't followed closely what's been happening with the Python API, but looking at the files here I am a getting worried that we are duplicating a whole bunch of Cryptol in Python, which might lead to maintenance headaches. I am thinking of some of the things in cryptoltypes.py specifically. If we do need such code, I wonder if we could, perhaps, auto-generate it from Haskell, which is likely to be less error prone and then if we make changes in Cryptol, they'll just get reflected in the python client. Thoughts?

[m-yac]

I haven't followed closely what's been happening with the Python API, but looking at the files here I am a getting worried that we are duplicating a whole bunch of Cryptol in Python, which might lead to maintenance headaches. I am thinking of some of the things in cryptoltypes.py specifically. If we do need such code, I wonder if we could, perhaps, auto-generate it from Haskell, which is likely to be less error prone and then if we make changes in Cryptol, they'll just get reflected in the python client. Thoughts?

This is an excellent idea! I have been uneasy about the fact that we're duplicating code here for a while, but I didn't get to the point where I realized we could just generate it. I'm going to experiment with this.

[pnwamk]

I haven't followed closely what's been happening with the Python API, but looking at the files here I am a getting worried that we are duplicating a whole bunch of Cryptol in Python, which might lead to maintenance headaches. I am thinking of some of the things in cryptoltypes.py specifically. If we do need such code, I wonder if we could, perhaps, auto-generate it from Haskell, which is likely to be less error prone and then if we make changes in Cryptol, they'll just get reflected in the python client. Thoughts?

I empathize with the overall concerns you describe.

This PR is specifically aimed at tidying up cryptoltypes.py. Perhaps while this is fresh in our minds, we could add some comments in this PR describing not only the "what" but the "why" for the code in here (specifically, why does the python client need to do these things, instead of delegating the work to the server? Some parts might be obvious, but I suspect there are a few design decisions/justifications which are more subtle we might forget from time to time).

As for auto generating the cryptoltypes.py file... it's not clear to me how much of a win/pain that would be. What kinds of changes in Cryptol would actually "break" the code in that file? How often are those likely to happen? Aren't we (or shouldn't we) already be testing for those exact kinds of things in our CI? I'm happy to dive into this further in more detail elsewhere; at the moment in my head it feels like a premature optimization/abstraction given the size and content, I dunno ¯\_(ツ)_/¯

[m-yac]

Inspired by a conversation between me and @pnwamk, I've taken the opposite approach and have deleted as many of these classes as I could. Specifically, I added the TypeOp subclass of CryptolType, which incorporates all of the type level operators (previously Plus, Max, etc.), so if one were to be removed/changed/added, we wouldn't have to update the Python interface. I also did the same for CryptolProps.

I also cleaned up CryptolTypeSchema and used it in the check_type command – so now check_type will work correctly on functions.

Finally, I updated test_types.py to reflect these changes.