function mprint(m) {
    return JSON.stringify(m);
}