Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

3.0 #176

Merged
merged 39 commits into from
Jun 21, 2023
Merged

3.0 #176

merged 39 commits into from
Jun 21, 2023

Commits on Jun 21, 2023

  1. build(*): Switch extraction to native OCaml strings (on Coq 8.15)

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    b327905 View commit details
    Browse the repository at this point in the history
  2. refactor(core): Apply attribute to Hints and Instances, remove Coq 8.…

    …15 warnings
    
    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    2ee6492 View commit details
    Browse the repository at this point in the history
  3. build(opam): Impose Coq >= 8.15 for this branch

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    1f6cb0b View commit details
    Browse the repository at this point in the history
  4. proof(imp): Clean up of existing Imp optimizer code

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    7bb034a View commit details
    Browse the repository at this point in the history
  5. core(imp): Break down for optim into two steps

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    f4d2226 View commit details
    Browse the repository at this point in the history
  6. compiler(source): A denotational semantics for OQL

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    187aeb6 View commit details
    Browse the repository at this point in the history
  7. compiler(source): Clean up and document OQL denotational semantics

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    74091f2 View commit details
    Browse the repository at this point in the history
  8. fix(doc): Update README and instructions for building documentation

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    9ba20fd View commit details
    Browse the repository at this point in the history
  9. compiler(source): Some initial typing and proof for OQL SFWO blocks

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    48e50f0 View commit details
    Browse the repository at this point in the history
  10. compiler(source): Type preservation for current OQL select from where…

    … typing
    
    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    0348812 View commit details
    Browse the repository at this point in the history
  11. compiler(source): Add typing for OQL's IN with CAST clause

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    48343ba View commit details
    Browse the repository at this point in the history
  12. source(OQL): Full typing rules for OQL's SELECT FROM WHERE expressions

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    f947ac8 View commit details
    Browse the repository at this point in the history
  13. source(OQL): generalize OQL In-cast to multiple class names

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    cf5ed8c View commit details
    Browse the repository at this point in the history
  14. refactor(nnrc): Minor fixes to NNRC optimizer code

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    1012357 View commit details
    Browse the repository at this point in the history
  15. fix(build): Adjust opam and CircleCI scripts

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    5314800 View commit details
    Browse the repository at this point in the history
  16. fix(doc): Update README

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    a5cfef8 View commit details
    Browse the repository at this point in the history
  17. semantics(OQL): Cleanup for OQL's whole query semantics

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    bd60ee6 View commit details
    Browse the repository at this point in the history
  18. refactor(parser): Common module to resolve function calls in source q…

    …ueries
    
    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    aa0363b View commit details
    Browse the repository at this point in the history
  19. runtime(javascript): Switch natural numbers to JavaScript BigInt

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    cdb1451 View commit details
    Browse the repository at this point in the history
  20. fix(runtime): Cleanup JavaScript runtime, fixes bug in union

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    3a90446 View commit details
    Browse the repository at this point in the history
  21. build(js): Cleanup and packaging for JavaScript support code

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    e51e706 View commit details
    Browse the repository at this point in the history
  22. fix(build): Update node packages version numbers (and test publication)

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    22c4bb3 View commit details
    Browse the repository at this point in the history
  23. fix(js): Addresses various issues with npm packages

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    1648f3b View commit details
    Browse the repository at this point in the history
  24. fix(runtime): Clean up and build for WASM / assemblyscript runtime

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    5964e8e View commit details
    Browse the repository at this point in the history
  25. core(sort): Generalize basic support for orderby

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    898a447 View commit details
    Browse the repository at this point in the history
  26. core(OQL): WIP for OQL order by

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    21dbf36 View commit details
    Browse the repository at this point in the history
  27. fix(js): Fix buggy sort function in JavaScript runtime + OQL orderby

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    4040b91 View commit details
    Browse the repository at this point in the history
  28. fix(java): Order by in OQL parser and Java runtime

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    2985044 View commit details
    Browse the repository at this point in the history
  29. fix(OQL): Proof of OQL ORDER BY interpretor is correct wrt sem

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    280131c View commit details
    Browse the repository at this point in the history
  30. proof(oql): At last, proof of order by type soundness

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    921c536 View commit details
    Browse the repository at this point in the history
  31. core(OQL): Proof of correctness for translation of OQL orderby to NRAEnv

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    b8d11ed View commit details
    Browse the repository at this point in the history
  32. fix(core): Remove some printing directives

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    efa1f27 View commit details
    Browse the repository at this point in the history
  33. fix(doc): Update demo code

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    9ca35ee View commit details
    Browse the repository at this point in the history
  34. fix(api): Update to TypeScript interface for compiler

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    12b7ee7 View commit details
    Browse the repository at this point in the history
  35. fix(doc): Remove old / duplicated demo

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    13b9c9f View commit details
    Browse the repository at this point in the history
  36. chore(core): Fixes for Coq 8.16 compatibility

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    e449136 View commit details
    Browse the repository at this point in the history
  37. fix(build): opam constraints on OCaml and Coq

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    f0efb06 View commit details
    Browse the repository at this point in the history
  38. fix(core): Clean up remaining admits, remove OQL interp completness l…

    …ikely untrue
    
    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    959571d View commit details
    Browse the repository at this point in the history
  39. fix(build): updates to package-lock.json files

    Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
    jeromesimeon committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    5d32dff View commit details
    Browse the repository at this point in the history