6.4.1 Matrix Operations🔗

matrix.rhm provides an implementation of matrices. It stores a matrix in row-major order in one flat array: cell (i, j) of an r-by-c matrix lives at slot i·c + j. The file defines make, index, get, set, fill, transpose, add, and twice, which transposes a matrix twice. However, the file intentionally does not verify. One refinement is missing, one is wrong, and one piece of code is wrong. Make the file verify.

Do not weaken the refinements that one would expect. get and set must keep their preconditions. The refinement on twice also stays because it states a valuable lightweight theorem: transposing a matrix twice gives a matrix with the same dimensions as the original. The checker should be able to prove this theorem from the type of transpose alone.

For each successful change you make: record the error message that you got rid of, and explain how the error message led you to make the fix. That is, don’t just blindly change characters around; read the messages carefully, understand what they’re saying, and explain how they helped you find the error. You will hand in this record with your code.

Shplait has no loop form, so a loop over the cells is a recursive function over (i, j), and its bounds are its preconditions.

6.4.2 Matrix Representation🔗

The previous part represented a matrix by a flat array. That means there are two notions of a “position”: the positions (i, j) of the matrix, which we will call cells, and the positions 0 to r·c − 1 of the array, which we will call slots. representation.rhm has the maps between them: index, from a cell to its slot, as before, and row_of and col_of, from a slot back to its cell. Three theorems say that the maps fit together in the desired ways:

• Two different cells never share a slot.

• If you go from a cell to its slot with index, then go from that slot back to a cell with row_of and col_of, you get the cell you started with.

• If you take a slot to a cell with row_of and col_of, then take that cell back to a slot with index, you get the slot you started with.

We represent “theorems” here by functions that compute a Boolean; specifically, their return value must be #true. If the checker successfully type-checks such a function, we can conclude that the theorem holds.

Theorems 1 and 3 are written for you. The file does not verify as it stands; make it verify, then state theorem 2 in the same form as the other two and make it verify as well. Hint: Along the way, the checker will tell you that it knows something about row_of and col_of but not enough. You will need to strengthen them. The refinement on index may be helpful.

6.4.3 A Well-Scoped Interpreter🔗

Our interpreters have a case for an unbound variable. However, it’s not one we ever want to encounter, because it means the program given to the interpreter has a very basic kind of error. That is, unbound variables make the interpreter partial, and we would like it to be total (in this regard).

The interpreter in interp.rhm is one in which that case is unreachable, and the type checker proves it. It handles a fragment of the language from Interpreter, with the constructor names you used there: numbers, +, variables, functions, application.

The proof depends on three measures: names, the names an environment binds; bound, whether a given name is among them; and closed_in, whether an expression mentions only bound names. interp_env requires its expression to be closed in the names of its environment. When a closure is applied, the expression being interpreted is the closure’s body and the environment is the closure’s own, extended with the argument (that is what static scoping means). To check that call, the checker has to know that the body is closed in that environment, and the way to do so is a refinement on v_fun.

Read the datatypes and the measures first; they are correct, and so is the code. Two refinements are missing, and the file does not verify. Make it verify.