querycert / qcert

Compilation and Verification of Data-Centric Languages
https://querycert.github.io/
Apache License 2.0
56 stars 9 forks source link

WIP(Imp) An ImpEJson parser proof of concept #134

Closed jeromesimeon closed 4 years ago

jeromesimeon commented 4 years ago

Signed-off-by: Jerome Simeon jeromesimeon@me.com

Hi @pkel

A sneak peek into a possible direction for imp parsing with a couple of examples in ./tests/imp_ejson

Runtime function would be called using Runtime.name where name is the name of the runtime function. Haven't quite made up my mind about operators yet. I shied away from trying to make an entirely generic imp parser because I couldn't quite figure out what to do with constants and operators...

You can test imp_ejson eval and js eval by doing:

make tests
make imp_ejson-tests 

Suggestions for syntax and what might be useful to support most welcome.

Flags

pkel commented 4 years ago

Great! I quickly skimmed the changes and it looks already super useful. I'll use what you have for implementing if and for. In the future, we can grow support on the imp parser and the wasm backend in parallel.

jeromesimeon commented 4 years ago

Great! I quickly skimmed the changes and it looks already super useful. I'll use what you have for implementing if and for. In the future, we can grow support on the imp parser and the wasm backend in parallel.

That sounds great. It's been a pleasantly easy exercise but also reveals some interesting things about Imp and how to make parsing easier, and how to improve the internal AST for Imp which I'm mulling over. I'll try and do a bit more between now and tomorrow, notably get some basic structure for operators and a few more examples.

jeromesimeon commented 4 years ago

@pkel Since you like the general direction, I'll likely merge whatever I have at the end of today so you can play with it tomorrow.

jeromesimeon commented 4 years ago

Fun fact: along with https://homepages.inf.ed.ac.uk/libkin/papers/icdt01.pdf the examples in this PR prove that Imp + arithmetics is strictly more expressive than the relational algebra. (i.e., you can express aggregation without adding aggregate functions to the language).