add strings to data refinement and observable values

remaining tasks at least include: prove cheat about compilation of
string literals, and update implementation of bytecode Print
instruction. but might skip the latter since we might want to soon get
rid of the Print instruction...