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.

Sign up for GitHub

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

Jump to bottom

3.0 #176

Merged
merged 39 commits into from
Jun 21, 2023
Merged

3.0 #176

merged 39 commits into from
Jun 21, 2023

Conversation

jeromesimeon
Copy link
Member

Numerous changes

OQL:

  • Improved and more complete OQL semantics including an alternative denotational semantics separate from interpreter
  • Support for order by clause and sorting
  • Support for in ...cast and multicast

Runtime:

  • Switch JavaScript runtime and codegen to use BigInt rather than number consistent with semantics

Build:

  • Switch extraction to use native Ocaml strings rather than char list
  • Switch to Coq 8.15 & 8.16 (8.17 needs Ocaml upgrades and WASM upgrades)
  • Clean up npm packages for node.js
  • Clean up of WASM and runtime build
  • Clean up CI scripts and build
  • Clean up opam metadata & dependencies

Misc:

  • Clean up typescript interface
  • Clean up of Imp optimizer code
  • Fixes to NNRC optimizer code
  • Clean up old demo and corresponding build path

Bug fixes:

  • Fixes JavaScript runtime bug in union operator
  • Fixes JavaScript runtime bug in sort operator

@jeromesimeon
build(*): Switch extraction to native OCaml strings (on Coq 8.15)
b327905 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
refactor(core): Apply attribute to Hints and Instances, remove Coq 8.…
2ee6492 
…15 warnings

Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
build(opam): Impose Coq >= 8.15 for this branch
1f6cb0b 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
proof(imp): Clean up of existing Imp optimizer code
7bb034a 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
core(imp): Break down for optim into two steps
f4d2226 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
compiler(source): A denotational semantics for OQL
187aeb6 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
compiler(source): Clean up and document OQL denotational semantics
74091f2 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(doc): Update README and instructions for building documentation
9ba20fd 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
compiler(source): Some initial typing and proof for OQL SFWO blocks
48e50f0 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
compiler(source): Type preservation for current OQL select from where…
0348812 
… typing

Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
compiler(source): Add typing for OQL's IN with CAST clause
48343ba 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
source(OQL): Full typing rules for OQL's SELECT FROM WHERE expressions
f947ac8 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
source(OQL): generalize OQL In-cast to multiple class names
cf5ed8c 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
refactor(nnrc): Minor fixes to NNRC optimizer code
1012357 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(build): Adjust opam and CircleCI scripts
5314800 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(doc): Update README
a5cfef8 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
semantics(OQL): Cleanup for OQL's whole query semantics
bd60ee6 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
refactor(parser): Common module to resolve function calls in source q…
aa0363b 
…ueries

Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
runtime(javascript): Switch natural numbers to JavaScript BigInt
cdb1451 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(runtime): Cleanup JavaScript runtime, fixes bug in union
3a90446 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
build(js): Cleanup and packaging for JavaScript support code
e51e706 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(build): Update node packages version numbers (and test publication)
22c4bb3 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(js): Addresses various issues with npm packages
1648f3b 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(runtime): Clean up and build for WASM / assemblyscript runtime
5964e8e 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
core(sort): Generalize basic support for orderby
898a447 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
core(OQL): WIP for OQL order by
21dbf36 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(js): Fix buggy sort function in JavaScript runtime + OQL orderby
4040b91 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(java): Order by in OQL parser and Java runtime
2985044 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(OQL): Proof of OQL ORDER BY interpretor is correct wrt sem
280131c 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
proof(oql): At last, proof of order by type soundness
921c536 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
core(OQL): Proof of correctness for translation of OQL orderby to NRAEnv
b8d11ed 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(core): Remove some printing directives
efa1f27 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(doc): Update demo code
9ca35ee 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(api): Update to TypeScript interface for compiler
12b7ee7 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(doc): Remove old / duplicated demo
13b9c9f 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
chore(core): Fixes for Coq 8.16 compatibility
e449136 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(build): opam constraints on OCaml and Coq
f0efb06 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(core): Clean up remaining admits, remove OQL interp completness l…
959571d 
…ikely untrue

Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon
fix(build): updates to package-lock.json files
5d32dff 
Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
@jeromesimeon jeromesimeon merged commit f091ec3 into master Jun 21, 2023
4 checks passed
@jeromesimeon jeromesimeon deleted the 3.0 branch June 21, 2023 23:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
1 participant
@jeromesimeon