Patrik Keller

Results 31 comments of Patrik Keller

The array operators are missing on this list. They are probably important? https://github.com/querycert/qcert/blob/wasm/compiler/core/EJson/Operators/EJsonRuntimeOperators.v#L48-L51 RuntimeArray is n-ary and the n is not known locally. I need to know the n for...

Just updated the list to reflect the latest state. Also added the non-runtime operators.

I made some progress in 95782518286. I think implementing and debugging the runtime would benefit from a set of unit tests per operator. How would you do it? My current...

I'd implement them in imp_ejson. Makes them reusable for other backends / runtime implementations.

Your imp_ejson parser undestands runtime operators like `Runtime.array(arg0, ...)`. How much effort is it to do something similar for non-runtime Operators? E.g. something like `Op.object(keys)(val1, val2)` which translates directly to...

Now I get what you meant with "syntax for those things". I think we could do something like this. ```json { "name": "Runtime Operator Equal", "operator": "EJsonRuntimeEqual", "type": "ejson_runtime_op", "inputs":...

> Will need to figure out how to write ejson values (in JSON? maybe that's too obvious) Yes in JSON. I think you already have serializer/parsers? That's my main reason...

Coming back to the operator unit test proposed above. I think we save a lot of time by coding the tests in OCaml. I've a basic proof-of-concept working. I compose...

Further, it seems that the JS implementation of `EJsonRuntimeEqual` which is based on the above `compare` does not align with the Coq/ImpEJson specification. Javascript runtime yields: ``` > compare ([1,...

My wasm implementation can be found here https://github.com/querycert/qcert/blob/a9a5365be5e0c82b861d52a65a43ec81dee66c86/runtimes/assemblyscript/assembly/index.ts#L627-L652. It aligns with ImpEJson eval according to a few tests. It easily translates to javascript. Should I open a PR?