Add new declaration forms that can be parsed at the REPL

[robdockins]

In particular, we can now define operators using let in the
same way that they can be inside modules and where.

In addition, we allow type and type constraint definitions
at the REPL, and infix, infixl and infixr declarations.

Becase it is an error for an infix declaration to be stated
without its corresponding declaration, we have added the ability
to enter multiple definitions at once, separated by ;. This
is also useful for definition mutually recursive definitions using
let.

[robdockins]

For some reason, type declarations at the REPL produce unused name warnings, and I'm not sure what is the best way to suppress them. Ideas, @yav?

Cryptol> type X n = [n]Integer
[warning] at <interactive>:1:6--1:7 Unused name: <interactive>::X
Cryptol> take [1...]: (X 100)
[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19,
 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36,
 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53,
 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70,
 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87,
 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100]

[yav]

I guess the warning is because X is not used, as it is the only declaration being checked. Perhaps we need some way to suppress these kinds of warnings for that use case.

[yav]

In general I am not a fan of declarations at the REPL, as one tends to end up with environments that are non-trivial to reproduce, and my personal preference is to have "read only" REPLs. I know that folks do ask for these features tough, so if someone finds it helpful I am fine with adding it.

I think we should start thinking of making DynamicEnv a little less ad-hoc though (not in this pull request). In particular, I wonder if DynamicEnv should be essentially a pair of an interface (i.e., static information) and a value environment (the dynamic information).

[robdockins]

I guess what's surprising to me is that value let declaration doesn't seem to produce the unused name warning, and I'm not sure what makes the difference. I expected to find some special-case code that suppresses the warning, but I didn't find it, so I'm not sure where is the best place to add logic for the type declarations.

[robdockins]

Regarding DynamicEnv, I agree. I thought about doing something along those lines here, but decided for a more minimal change for now.

[yav]

@robdockins if I remember correctly we only report "unused" variables for types. We started doing that because sometimes mis-spelling a type, resulted in an unused type parameter (as in \(x : integer) -> x)