Entering Terms in the Term Editor

  This tutorial introduces you to using the Nuprl term editor to enter terms. You should first take a quick glance at the chapter of the Nuprl Reference Manual on the ML Top Loop. We illustrate use of the term editor for editing terms by considering the entry of terms from Nuprl's object language as ML objects of type term.

Start with a text cursor at a fresh ML prompt and type $\langle$C-O$\rangle$.The ML top loop should look like:

When entering ML text, the command $\langle$C-O$\rangle$ opens up a position for a term that is to be considered as an ML object of type term. The [term] is a placeholder. Placeholders are delimited by []'s and include a text string which suggests the kind of term that should be inserted. You get a placeholder when some text or term is missing. The box around [term] indicates that a term cursor is positioned at the placeholder. Term cursors are shown on the screen by highlighting.

When you have a term cursor at a placeholder and you type printing characters, the characters are interpreted as the name of a term to insert. Type

As the letters m u l are typed, they are shown highlighted on the screen. Use to correct any typo's. After , the system inserts a multiplication term and the ML Top Loop should now look like:

When you have a term cursor, is a null command and serves to terminate names of terms. The names of some common terms that you might find useful are listed in Section 12.8. Any name not matching a predefined name and including a letter is interpreted as a variable, and a variable term is inserted. If the name entered consists of all numbers, a natural number term is inserted.

Use to move the cursor around. Try clicking on the left [int], the right [int] and the * symbol. It is easiest to move the cursor around using the mouse, although you can also use various keyboard commands. If by accident some mouse click results in a new window being opened up, click in that window and then key $\langle$C-Q$\rangle$ to close it.

Click on the left [int] and key

to enter the variable x . You should get the display:

The key is another useful name terminator. It causes the cursor to jump to the next empty slot in preorder order.

Say that what we really wanted to do was enter the variable y instead of the variable x. To edit the variable name. Click on the x to get a text cursor to the left of the x, and then key $\langle$C-D$\rangle$. The display should now look like:

The [variable] is an example of a an empty text slot. Enter y to fill it with the character y. The variable term is considered distinct from its text slot. To set a term cursor at a variable term you have to use $\langle$C- $\rangle$, not . Try it. gives you a text cursor if one is appropriate, but $\langle$C- $\rangle$ always gives you a term cursor sitting at the closest surrounding term containing the character you are pointing at.

To delete a term at a term cursor, use $\langle$C-K$\rangle$. Delete the variable y, using $\langle$C- $\rangle$ to first position the cursor at the variable. If you ever mis-type the name of a term and get some other term inserted instead, this is one way of getting rid of it.

Try entering a couple more terms. Starting with the ML Top Loop in state:

Enter

to get:

Note how the editor has an idea about precedence; it automatically inserts parentheses around the +, but not the second *. The cursor stays at the 5 after the last because there is no other empty slot to jump to.

The ML evaluator evaluates data objects such objects of type term to themselves. Try evaluating what you've just entered. Click on the space before the ;; to get a text cursor, and then key . In the shell window you should see:

There is a Nuprl ML function compute which has type term -> term. It invokes an evaluator for terms that lie in Nuprl's object language. To try it, key $\langle$C-R$\rangle$ to recall the term you just entered, click on the first ' character to get a text cursor just before the term, and enter

Click on the space between the second ' and the first ; to get a text cursor after the Nuprl term. The display should look like:

Enter to evaluate and get the result:

You now should know enough to experiment with typing in other expressions from Nuprl's object language and seeing how they evaluate using the object language evaluator.