Move FOR combinator into separate theory file.
Begin development of "monadic primitives", better modeling partiality.

This is so as to better capture undefinedness when reads or updates
are out of bounds.