Declare primitive types and constraints in the Cryptol prelude

[brianhuffman]

Putting declarations for primitive Cryptol types, type functions, and type constraints into Cryptol.cry would have various advantages:

• Parser and renamer code could be simplified; special cases for primitives would no longer be necessary
• It would make the Cryptol internals more uniform for types vs expressions
• We could put all the doc-strings in one place (currently the doc-strings for primitive types are in module Cryptol.Prims.Syntax, while doc-strings for primitive values are in Cryptol.cry)
• It would be easier to add support for things like user-defined infix type operators
• Adding new primitive types or type constraints in the future will require less work (i.e. fewer bits of code will have to be modified)

We will probably need to have a syntax that looks something like that below, with kind annotations. Here's what I believe is the complete list of declarations we'll need currently:

primitive type Bit : *
primitive type Integer : *
primitive type Z : # -> *
primitive type (->) : * -> * -> *
primitive type inf : #

primitive type (==) : # -> # -> constraint
primitive type (!=) : # -> # -> constraint
primitive type (>=) : # -> # -> constraint
primitive type fin : # -> constraint
primitive type Zero : * -> constraint
primitive type Logic : * -> constraint
primitive type Arith : * -> constraint
primitive type Cmp : * -> constraint
primitive type SignedCmp : * -> constraint
primitive type Literal : # -> * -> constraint

primitive type (+) : # -> # -> #
primitive type (-) : # -> # -> #
primitive type (*) : # -> # -> #
primitive type (/) : # -> # -> #
primitive type (%) : # -> # -> #
primitive type (^^) : # -> # -> #
primitive type (/^) : # -> # -> #
primitive type (%^) : # -> # -> #
primitive type width : # -> #
primitive type min : # -> # -> #
primitive type max : # -> # -> #
primitive type lengthFromThenTo : # -> # -> # -> #

[brianhuffman]

This was fixed in 72068cb.