viper: error source mappings in moc.js

[rvanasa]

Passes the lookup function through moc.js to facilitate source mapping in VS Code.

[rvanasa]

There is currently a bug hiding somewhere in the way that moc.js initializes or calls the lookup function from Viper.Pretty.prog_mapped.

I expect this to be a quick fix tomorrow, but I would appreciate a second pair of eyes in case anyone gets a chance to skim this PR. This is most likely the final step to a working demo for source locations.

Here's a command to reproduce the issue:

make -C src moc.js && node -e "const {Motoko} = require('./src/moc.js'); Motoko.saveFile('File.mo', 'actor { public func abc(): async () { } };'); console.log('Result:', Motoko.viper(['File.mo']).code.lookup('', [0,0,0,0]))"

Replacing ...lookup('', [0,0,0,0])) with any other values (filename, [leftLine, leftCol, rightLine, rightCol]) always seems to return null (indicating None is returned from the lookup function). This probably has something to do with this PR's changes in Pipeline.viper_files', since I checked that the js_of_ocaml conversions work as expected.

Does anything stand out as the issue? Otherwise I'll continue narrowing this down tomorrow morning.

[ggreif]

The filename passed in must be the one that the Viper-side diagnostic points to.

[ggreif]

Does anything stand out as the issue?

My hunch is that the let inside function in Pretty.prog_mapped takes filenames in account, so that may fail. We could beef up inside to skip the name comparison when the filename passed to Pretty.prog_mapped is empty.

EDIT: Oh, I see, passing "" in already effectively deactivates the comparison.

2nd hunch: reverse mappings only exist for Motoko/Viper statements, but your code has an empty body.

Found a hit:

make -C src moc.js && node -e "const {Motoko} = require('./src/moc.js'); Motoko.saveFile('File.mo', 'actor { var v = -1; public func abc(): async () { v := 1; v := 12; v := 14; v := 15; v := 16; v := 19; } };'); console.log('Result:', Motoko.viper(['File.mo']).code.lookup('', [13,6,13,6]))"

gives

Result: { start: { line: 0, character: 94 }, end: { line: 0, character: 101 } }

Which corresponds to the statement v := 19. Previous lines accordingly (e.g. [8,5,8,19] --> v := 1). So there is no bug at all, you only have to poke at the right place. Good work!

[ggreif]

@rvanasa can this go in?

[ggreif]

LGTM

[rvanasa]

Merging. If anything needs a quick fix, I'll just commit directly to the viper branch.