Render inverse functions in prose, without ^(-1)

[jaehyun1ee]

This PR adds rendering logic for inverse function applications.

When translating EL/IL to AL, we sometimes introduce inverse functions. For example when translating the dynamic semantics of VBITMASK instruction, AL introduces an inverse function $ibits_1^-1(32, $ilt($lsize(Jnn), S, ci_1, 0)*). In AL AST, it corresponds to the expression node InvCallE.

;; EL
rule Step_pure/vbitmask:
  (VCONST V128 c) (VBITMASK (Jnn X M)) ~> (CONST I32 ci)
  -- if ci_1* = $lanes_(Jnn X M, c)
  -- if $ibits(32, ci) = $ilt($lsize(Jnn), S, ci_1, 0)*

;; AL
execution_of_VBITMASK (Jnn X N)
1. Assert: Due to validation, a value is on the top of the stack.
2. Pop the value (V128.CONST c) from the stack.
3. Let ci_1* be $lanes_((Jnn X N), c).
4. Let ci be $ibits_1^-1(32, $ilt($lsize(Jnn), S, ci_1, 0)*).
5. Push the value (I32.CONST ci) to the stack.

When rendering AL's InvCallE to EL's CallE, EL expects the function id to be of type string. So, the previous implementation passes string ibits^{-1}_{1} to the EL renderer. This breaks the correspondence between what is seen in the prose and the formal mathematical rules.

To properly render inverse functions newly introduced in AL, I can think of two solutions, where this PR implements the second one.

(1) Define the inverse function signatures in the spec watsup file and let display hints take care of the inverse signs.

For example, we can define

;; 3-runtime.watsup
def $invibits(N, bit*) : iN(N)   hint(show $ibits_(%)^(-1)#((%)))

Then in the AL renderer, translate AL InvCallE on ibits to EL CallE on invibits.

This is easy to implement and the logic is clear, but the downside is that spec writers must be aware of the fact that when they are using functions that will turn out to be inversed after translation, they should define the inversed signature with proper display hints.

(2) Elaborate inverse function in prose

Or we can elaborate inverse function application in prose (English), for it is essentially solving an equation.
As in the actual prose, the renderer elaborates "Let ... be the result for which ... = ...".

Sometimes, inverse function application appears without a let binding, where the prose renderer introduces a fresh variable. For example the second premise in rule Step_read/vload-splat-val is rendered as:

;; EL
rule Step_read/vload-splat-val:
  z; (CONST I32 i) (VLOAD V128 (SPLAT N) x ao)  ~>  (VCONST V128 c)
  ----
  -- if $ibytes(N, j) = $mem(z, x).BYTES[i + ao.OFFSET : N/8]
  -- if N = $lsize(Jnn)  ;; TODO(2, rossberg): relate implicitly
  -- if M = $(128/N)
  -- if c = $invlanes_(Jnn X M, j^M)

This is a more general solution than the first, but not sure if we all like the how the inverse function is elaborated prose.
I haven't implemented this in al/print.ml yet, it is only in backend-prose/render.ml now.

[rossberg]

I like the second form, IIRC it is what the manual prose did as well in some places.

There may be some work to be done wrt rendering of the "type of" condition, but that's a separate issue.