Reorganisation of repl_funTheory

Define all the versions of the REPL in the logic, with informative names
and comments. State the desired correctness theorem at the end (but no
proofs updated yet).