Semantic Lists; Input/Output Streaming

In this lesson we add semantics to the read and print IMP++ constructs. In doing so, we also learn how to use semantic lists and how to connect cells holding semantic lists to the standard input and standard output. This allows us to turn the K semantics into an interactive interpreter.

We start by adding two new cells to the configuration,

<in color="magenta"> .List </in>
<out color="Orchid"> .List </out>

each holding a semantic list, initially empty. Semantic lists are space-separated sequences of items, each item being a term of the form ListItem(t), where t is a term of sort K. Recall that the semantic maps, which we use for states, environments, stores, etc., are sets of pairs t1 |-> t2, where t1 and t2 are terms of sort K. The ListItem wrapper is currently needed, to avoid parsing ambiguities.

Since we want the print statement to also print strings, we need to tell K that strings are results. To make it more interesting, let us also overload the + symbol on arithmetic expressions to also take strings and, as a result, to concatenate them. Since + is already strict, we only need to add a rule reducing the IMP addition of strings to the builtin operation +String which concatenates two strings.

The semantics of read is immediate: read and consumes the first integer item from the <in/> cell; note that our read only reads integer values (it gets stuck if the first item in the <in/> cell is not an integer).

The semantics of print is a bit trickier. Recall that print takes an arbitrary number of arithmetic expression arguments, and evaluates and outputs each of them in order, from left to right. For example, print("Hello", 3/0, "Bye"); outputs "Hello" and then gets stuck on the illegal division by zero operation. In other words, we do not want it to first evaluate all its arguments and then print them, because that would miss outputting potentially valuable information. So the first step is to evaluate the first argument of print. In some sense, what we'd like to say is that print has the evaluation strategy strict(1). However, strictness attributes only work with individual language constructs, while what we need is an evaluation strategy that involves two constructs: print and the list (comma) construct of AExps. If we naively associate print the strict(1) evaluation strategy then its first and unique argument, an AExps list, will be scheduled for evaluation and the execution will get stuck because we have no rules for evaluating AExps terms. If we make the list construct of AExps strict then we get the wrong semantics for print which first evaluates all its arguments and then outputs them. The correct way to tell K that print should evaluate only its first argument is by using a context declaration:

context print(HOLE:AExp, _);

Note the HOLE of sort AExp above. Contexts allow us to define finer-grain evaluation strategies than the strictness attributes, involving potentially more than one language construct, like above. The HOLE indicates the argument which is requested to be evaluated. For example, the strict attribute of division corresponds to two contexts:

context HOLE / _
context _ / HOLE

In their full generality, contexts can be any terms with precisely one occurrence of a HOLE, and with arbitrary side conditions on any variables occurring in the context term as well as on the HOLE. See Part 6 of the tutorial for more examples.

Once evaluated, the first argument of print is expected to become either an integer or a string. Since we want to print both integers and string values, to avoid writing two rules, one for each type of value, we instead add a new syntactic category, Printable, which is the union of integers and strings.

Let us kompile and krun the io.imp program discussed in Lesson 1. As expected, it gets stuck with a read construct on top of the computation and with an empty <in/> cell. To run it, we need to provide some items in the <in/> cell, so that the rule of read can match. Let us add

<in> ListItem(3) ListItem(5) ListItem(7) </in>

Now, if we krun io.imp, we can see that its execution completes normally (the <k/> cell is empty), that the first two items have been removed by the two read constructs from the <in/> cell, and that the desired strings and numbers have been placed into the <out/> cell.

Cells holding semantic lists can be connected to the standard input and standard output buffers, and krun knows how to handle these appropriately. Let us connect the <in/> cell to the standard input using the cell attribute stream="stdin" and the <out/> cell to the standard output with the attribute stream="sdtout". A cell connected to the standard input will take its items from the standard input and block the rewriting process when an input is needed until an item is available in the standard input buffer. A cell connected to the standard output buffer will send all its items, in order, to the standard output.

Let us kompile and krun io.imp again. It prints the message and then waits for your input numbers. Type in two numbers, then press <Enter>. A message with their sum is then printed, followed by the final configuration. If you do not want to see the final configuration, and thus obtain a realistic interpreter for our language, then call krun with the option --output none:

krun io.imp --output none

Let us now krun our interactive sum program, which continuously reads numbers from the console and prints the sum of numbers up to them:

krun sum-io.imp

Try a few numbers, then 0. Note that the program terminated, but with junk in the <k/> cell, essentially with a halt statement on its top. Of course, because halt has been reached and it has no semantics yet.

In the next lesson we give the semantics of halt and also fix the semantics of blocks with local variable declarations.

Go to Lesson 5, IMP++: Deleting, Saving and Restoring Cell Contents.

MOVIE (out of date) [05'21"]