Webassembly backend

.circleci/config.yml

@@ -58,6 +58,7 @@ common_steps: &common_steps
     - run:
         name: 'Testing'
         command:  |
+          eval $(opam env)
           make test
     # Save test results
     - store_test_results:

.gitignore

@@ -21,6 +21,7 @@ log/
 *.vo
 *.vos
 *.vok
+*.vio
 *.v.d
 *.glob
 *.aux

Makefile

@@ -28,8 +28,8 @@ all:
 	@$(MAKE) install-local
 
 build: 
-	@$(MAKE) qcert-compiler
 	@$(MAKE) MAKEFLAGS= qcert-runtimes
+	@$(MAKE) qcert-compiler
 	@$(MAKE) MAKEFLAGS= qcert-cli
 
 clean: Makefile.coq remove_all_derived
@@ -51,6 +51,7 @@ cleanmost: Makefile.coq
 	- @rm -f *~
 
 cleanall: Makefile.coq remove_all_derived
+	- @$(MAKE) cleanall-runtimes
 	- @$(MAKE) cleanall-qcert-compiler
 	- @$(MAKE) cleanmost
 
@@ -60,7 +61,7 @@ cleanall: Makefile.coq remove_all_derived
 install-coqdev:
 	@$(MAKE) -f Makefile.coq install
 
-install-local: 
+install-local:
 	@$(MAKE) install-ocaml
 ifneq ($(JAVASCRIPT),)
 	@$(MAKE) install-javascript
@@ -112,17 +113,11 @@ cleanmost-qcert-compiler:
 
 ## Configure
 
-runtimes/javascript/qcert_runtime.ml:
-	$(MAKE) -C runtimes/javascript
-
-compiler/lib/js_runtime.ml: runtimes/javascript/qcert_runtime.ml
-	cp runtimes/javascript/qcert_runtime.ml compiler/lib/js_runtime.ml
-
 compiler/lib/static_config.ml:
 	echo "(* This file is generated *)" > compiler/lib/static_config.ml
 	echo "let qcert_home = \"$(CURDIR)\"" >> compiler/lib/static_config.ml
 
-prepare: compiler/lib/js_runtime.ml compiler/lib/static_config.ml Makefile.coq
+prepare: compiler/lib/static_config.ml Makefile.coq
 
 configure:
 	@echo "[Q*cert] "
@@ -133,8 +128,6 @@ configure:
 clean-configure:
 
 cleanall-configure:
-	$(MAKE) -C runtimes/javascript cleanall
-	rm -rf compiler/lib/js_runtime.ml
 	rm -rf compiler/lib/static_config.ml
 	rm -f compiler/.merlin compiler/*/.merlin
 
@@ -242,22 +235,13 @@ qcert-runtimes:
 	@echo "[Q*cert] "
 	@echo "[Q*cert] Building runtimes"
 	@echo "[Q*cert] "
-ifneq ($(JAVASCRIPT),)
-	@$(MAKE) javascript-runtime
-endif
 ifneq ($(JAVA),)
 	@$(MAKE) java-runtime
 endif
 ifneq ($(SPARK),)
 	@$(MAKE) spark2-runtime
 endif
 
-javascript-runtime:
-	@echo "[Q*cert] "
-	@echo "[Q*cert] JavaScript runtime"
-	@echo "[Q*cert] "
-	@$(MAKE) -C runtimes/javascript
-
 java-runtime:
 	@echo "[Q*cert] "
 	@echo "[Q*cert] Java runtime"
@@ -271,14 +255,12 @@ spark2-runtime:
 	@$(MAKE) -C runtimes/spark2
 
 clean-runtimes:
-	- @$(MAKE) -C runtimes/javascript clean
 	- @$(MAKE) -C runtimes/java clean
 	- @$(MAKE) -C runtimes/spark2 clean
 	- @rm -rf bin/lib
 	- @rm -f bin/javaRunner.jar
 
 cleanall-runtimes:
-	- @$(MAKE) -C runtimes/javascript cleanall
 	- @$(MAKE) -C runtimes/java cleanall
 	- @$(MAKE) -C runtimes/spark2 cleanall
 	- @rm -rf bin/lib
@@ -336,10 +318,7 @@ demo:
 bin/qcertJS.js:
 	@$(MAKE) qcert-javascript
 
-runtimes/javascript/qcert-runtime.js:
-	@$(MAKE) javascript-runtime
-
-qcert-demo: bin/qcertJS.js runtimes/javascript/qcert-runtime.js
+qcert-demo: bin/qcertJS.js
 	@echo "[Q*cert] "
 	@echo "[Q*cert] Compiling Web Demo in TypeScript"
 	@echo "[Q*cert] "
@@ -355,6 +334,7 @@ cleanall-demo: clean-demo
 ## Tests
 
 test:
+	dune runtest
 	@$(MAKE) -C tests
 
 clean-test:
@@ -370,10 +350,10 @@ docs:
 ## Misc
 
 clean_detritus:
-	@find . \( -name '*.vo' -or -name '*.v.d' -or -name '*.glob'  -or -name '*.aux' \) -print0 | xargs -0 scripts/remove_detritus_derived_file.sh
+	@find . \( -name '*.vo' -or -name '*.vos' -or -name '*.vok' -or -name '*.v.d' -or -name '*.glob'  -or -name '*.aux' \) -print0 | xargs -0 scripts/remove_detritus_derived_file.sh
 
 remove_all_derived:
-	@find . \( -name '*.vo' -or -name '*.v.d' -or -name '*.glob'  -or -name '*.aux' \) -print0 | xargs -0 rm -f
+	@find . \( -name '*.vo' -or -name '*.vos' -or -name '*.vok' -or -name '*.v.d' -or -name '*.glob'  -or -name '*.aux' \) -print0 | xargs -0 rm -f
 
 Makefile.coq: Makefile Makefile.coq_modules $(FILES)
 	@coq_makefile -f _CoqProject $(FILES) -o Makefile.coq

Makefile.coq_modules

@@ -19,8 +19,8 @@ MODULES = \
 	Utils/ListAdd \
 	Utils/StringAdd \
 	Utils/SortingAdd \
+	Utils/FloatAdd \
 	Utils/NativeString \
-	Utils/Float \
 	Utils/Lattice \
 	Utils/Monoid \
 	Utils/Assoc \
@@ -63,6 +63,10 @@ MODULES = \
 	JSON/Model/JSONNorm \
 	JSON/JSONRuntime \
 	JSON/JSONSystem \
+	WSON/Model/ForeignWSON \
+	WSON/Operators/ForeignWSONRuntime \
+	WSON/WSONRuntime \
+	WSON/WSONSystem \
 	EJson/Model/ForeignEJson \
 	EJson/Model/EJson \
 	EJson/Model/EJsonNorm \
@@ -120,6 +124,7 @@ MODULES = \
 	Translation/Model/DataToEJson \
 	Translation/Model/ForeignEJsonToJSON \
 	Translation/Model/EJsonToJSON \
+	Translation/Model/ForeignEJsonToWSON \
 	Translation/Model/EJsonToEJsonMut \
 	Translation/Model/ForeignTypeToJSON \
 	Translation/Model/TypeToJSON \
@@ -261,6 +266,7 @@ MODULES = \
 	Imp/ImpSystem \
 	Imp/Optim/ImpOptimizerEngine \
 	Imp/Optim/ImpEJsonRewrite \
+	Imp/Optim/ImpEJsonBlockRewrite \
 	Imp/Optim/ImpEJsonOptimizer \
 	Imp/ImpOptim \
 	NNRCMR/Lang/ForeignReduceOps \
@@ -342,12 +348,19 @@ MODULES = \
 	SparkDF/Lang/SparkDF \
 	SparkDF/SparkDFRuntime \
 	SparkDF/SparkDFSystem \
+	WasmAst/Lang/WasmAst \
+	WasmAst/WasmAstRuntime \
+	WasmAst/WasmAstSystem \
+	WasmBinary/Lang/WasmBinary \
+	WasmBinary/WasmBinaryRuntime \
+	WasmBinary/WasmBinarySystem \
 	Translation/Operators/ForeignToReduceOps \
 	Translation/Operators/ForeignToJavaScriptAst \
 	Translation/Operators/ForeignToJava \
 	Translation/Operators/ForeignToScala \
 	Translation/Operators/ForeignToSpark \
 	Translation/Operators/ForeignToEJsonRuntime \
+	Translation/Operators/ForeignToWasmAst \
 	Translation/Lang/NRAtocNNRC \
 	Translation/Lang/cNRAEnvtocNNRC \
 	Translation/Lang/cNRAEnvtoNRA \
@@ -382,6 +395,8 @@ MODULES = \
 	Translation/Lang/NNRCtoJava \
 	Translation/Lang/DatatoSparkDF \
 	Translation/Lang/tDNNRCtoSparkDF \
+	Translation/Lang/ImpEJsontoWasmAst \
+	Translation/Lang/WasmAsttoWasmBinary \
 	Translation/Typing/TNRAtocNNRC \
 	Translation/Typing/TcNRAEnvtocNNRC \
 	Translation/Typing/TcNNRCtoCAMP \
@@ -426,8 +441,10 @@ MODULES = \
 	Compiler/Enhanced/EnhancedEJson \
 	Compiler/Enhanced/EnhancedDataToEJson \
 	Compiler/Enhanced/EnhancedEJsonToJSON \
+	Compiler/Enhanced/EnhancedEJsonToWSON \
 	Compiler/Enhanced/EnhancedToJava \
 	Compiler/Enhanced/EnhancedToJavascriptAst \
+	Compiler/Enhanced/EnhancedToWasmAst \
 	Compiler/Enhanced/EnhancedReduceOps \
 	Compiler/Enhanced/EnhancedToReduceOps \
 	Compiler/Enhanced/EnhancedToSpark \
@@ -453,4 +470,4 @@ MODULES = \
 	Tests/SQLTest \
 	Tests/LambdaNRATest \
 	Tests/CompilerTest \
-	Tests/HelloWorld \
+	Tests/HelloWorld

README.md

@@ -48,6 +48,13 @@ $ opam repo add coq-released https://coq.inria.fr/opam/released
 $ opam install . --deps-only
 ```
 
+*Warning:* It seems that coq and/or the Q\*cert build process does not like opam local switches.
+If you want to use a separate opam switch for Q\*cert, we recommend creating a new named global switch *before* executing the above steps.
+
+```
+$ opam switch create qcert 4.09.1
+```
+
 #### Java (Recommended)
 
 Parsers for SQL, SQL++, and ODM rules, the Q\*cert runtime for the Java compilation target, as well as utilities for running compiled queries are written in Java and require a Java 8 compiler.

cli/nodejs/lib/qcertRunner.js

@@ -127,7 +127,7 @@ class QcertRunner {
         const gconf = QcertRunner.configure('oql',schema,compiledQuery,output);
         input = BoxedCollections.boxColl(input);
         if (validate) {
-            if (output) {
+            if (output !== undefined) {
                 let result = QcertRunner.executeCompiled(schema,queryFile,compiledQuery,input);
                 result = BoxedCollections.unboxColl(result);
                 return QcertRunner.validate(gconf,queryFile,'js',output,result)

cli/ocaml/qcert.ml

@@ -17,7 +17,8 @@ open Qcert_lib
 open Util
 open Logger
 open Config
-open Core.EnhancedCompiler
+open CompLang
+open EnhancedCompiler.EnhancedCompiler
 open Logger_to_sexp
 
 (* Command line args *)
@@ -114,30 +115,30 @@ let args_list gconf =
 let anon_args input_files f = input_files := f :: !input_files
 
 let languages =
-  [ Core.L_camp_rule;
-    Core.L_camp;
-    Core.L_tech_rule;
-    Core.L_designer_rule;
-    Core.L_oql;
-    Core.L_sql;
-    Core.L_sqlpp;
-    Core.L_lambda_nra;
-    Core.L_nra;
-    Core.L_nraenv;
-    Core.L_nraenv_core;
-    Core.L_nnrc;
-    Core.L_nnrc_core;
-    Core.L_nnrs;
-    Core.L_nnrs_core;
-    Core.L_imp_data;
-    Core.L_imp_ejson;
-    Core.L_nnrcmr;
-    Core.L_dnnrc;
-    Core.L_dnnrc_typed;
-    Core.L_js_ast;
-    Core.L_javascript;
-    Core.L_java;
-    Core.L_spark_df; ]
+  [ L_camp_rule;
+    L_camp;
+    L_tech_rule;
+    L_designer_rule;
+    L_oql;
+    L_sql;
+    L_sqlpp;
+    L_lambda_nra;
+    L_nra;
+    L_nraenv;
+    L_nraenv_core;
+    L_nnrc;
+    L_nnrc_core;
+    L_nnrs;
+    L_nnrs_core;
+    L_imp_data;
+    L_imp_ejson;
+    L_nnrcmr;
+    L_dnnrc;
+    L_dnnrc_typed;
+    L_js_ast;
+    L_javascript;
+    L_java;
+    L_spark_df; ]
 
 
 let languages_string =
@@ -156,8 +157,8 @@ let parse_args () =
   let gconf =
     { gconf_qname = None;
       gconf_class_name = None;
-      gconf_source = Core.L_camp_rule;
-      gconf_target = Core.L_javascript;
+      gconf_source = L_camp_rule;
+      gconf_target = L_javascript;
       gconf_path = [];
       gconf_exact_path = false;
       gconf_dir = None;

cli/ocaml/qdata.ml

@@ -18,7 +18,7 @@ open Qcert_lib
 
 open Util
 open Config
-open Core.EnhancedCompiler
+open EnhancedCompiler.EnhancedCompiler
 
 let verbose = ref false
 
@@ -43,8 +43,8 @@ let parse_args () =
   let gconf =
     { gconf_qname = None;
       gconf_class_name = None;
-      gconf_source = Core.L_camp_rule;
-      gconf_target = Core.L_javascript;
+      gconf_source = L_camp_rule;
+      gconf_target = L_javascript;
       gconf_path = [];
       gconf_exact_path = false;
       gconf_dir = None;

compiler/core/Compiler/Component/SqlDateComponent.v

@@ -309,5 +309,26 @@ Section SqlDateOperators.
       | EJsonRuntimePeriodBetween => "periodBetween"
       end.
 
+    Definition ejson_sql_date_runtime_op_fromstring opname : option ejson_sql_date_runtime_op :=
+      match opname with
+      | "dateFromString" => Some EJsonRuntimeDateFromString
+      | "dateGetYear" => Some EJsonRuntimeDateGetYear
+      | "dateGetMonth" => Some EJsonRuntimeDateGetMonth
+      | "dateGetDay" => Some EJsonRuntimeDateGetDay
+      | "dateNe" => Some EJsonRuntimeDateNe
+      | "dateLt" => Some EJsonRuntimeDateLt
+      | "dateLe" => Some EJsonRuntimeDateLe
+      | "dateGt" => Some EJsonRuntimeDateGt
+      | "dateGe" => Some EJsonRuntimeDateGe
+      | "dateSetYear" => Some EJsonRuntimeDateSetYear
+      | "dateSetMonth" => Some EJsonRuntimeDateSetMonth
+      | "dateSetDay" => Some EJsonRuntimeDateSetDay
+      | "periodFromString" => Some EJsonRuntimePeriodFromString
+      | "periodPlus" => Some EJsonRuntimePeriodPlus
+      | "periodMinus" => Some EJsonRuntimePeriodMinus
+      | "periodBetween" => Some EJsonRuntimePeriodBetween
+      | _ => None
+      end.
+
   End toEJson.
 End SqlDateOperators.

compiler/core/Compiler/Component/UriComponent.v

@@ -81,5 +81,12 @@ Section UriOperators.
       | EJsonRuntimeUriDecode => "uriDecode"
       end.
 
+    Definition ejson_uri_runtime_op_fromstring opname : option ejson_uri_runtime_op :=
+      match opname with
+      | "uriEncode" => Some EJsonRuntimeUriEncode
+      | "uriDecode" => Some EJsonRuntimeUriDecode
+      | _ => None
+      end.
+
   End toEJson.
 End UriOperators.