GSoC 2020: Webassembly backend for the Ergo compiler

.circleci/config.yml

@@ -40,7 +40,7 @@ common_steps: &common_steps
     - run:
         name: "Install OCaml deps"
         command: |
-          opam install -y -v --jobs=2 dune menhir base64 js_of_ocaml js_of_ocaml-ppx yojson atdgen re calendar uri
+          opam install -y -v --jobs=2 dune menhir base64 js_of_ocaml js_of_ocaml-ppx yojson atdgen re calendar uri wasm.1.0.1
     - run:
         name: "Install Coq"
         command: |

DEVELOPERS.md

@@ -53,7 +53,7 @@ To rebuild the compiler from the source, you will need Coq 8.12.0 and OCaml 4.11
 
 ```sh
 $ opam repo add coq-released https://coq.inria.fr/opam/released
-$ opam install dune menhir base64 js_of_ocaml js_of_ocaml-ppx yojson atdgen re calendar uri
+$ opam install dune menhir base64 js_of_ocaml js_of_ocaml-ppx yojson atdgen re calendar uri wasm.1.0.1
 $ opam install coq.8.12.0 coq-qcert.2.1.0
 ```
 

Makefile.config

@@ -13,4 +13,4 @@
 #
 
 ## Qcert compiler location
-#QCERT=../qcert-master
+QCERT=qcert

Makefile.coq_modules

@@ -72,6 +72,8 @@ MODULES = \
   ErgoNNRC/Lang/ErgoNNRC \
   ErgoNNRC/Lang/ErgoNNRCSugar \
   ErgoImp/Lang/ErgoImp \
+  ErgoWasmAst/Lang/ErgoWasmAst \
+  ErgoWasmBinary/Lang/ErgoWasmBinary \
   Translation/CTOtoErgo \
   Translation/ErgoNameResolve \
   Translation/ErgoAssembly \
@@ -82,6 +84,8 @@ MODULES = \
   Translation/ErgoNNRCtoErgoImp \
   Translation/ErgoImptoES6 \
   Translation/ErgoNNRCtoJava \
+  Translation/ErgoImptoWasmAst \
+  Translation/WasmAsttoWasmBinary \
   Compiler/ErgoDriver \
   Compiler/ErgoCompiler \
   Tests/HelloWorld

compiler/core/Backend/Component/DateTimeComponent.v

@@ -403,16 +403,16 @@ Section DateTimeOperators.
       | uop_date_time_get_months => "dateTimeGetMonths"
       | uop_date_time_get_quarters => "dateTimeGetQuarters"
       | uop_date_time_get_years => "dateTimeGetYears"
-      | uop_date_time_start_of_day => "dateTimeStartOf"
-      | uop_date_time_start_of_week => "dateTimeStartOf"
-      | uop_date_time_start_of_month => "dateTimeStartOf"
-      | uop_date_time_start_of_quarter => "dateTimeStartOf"
-      | uop_date_time_start_of_year => "dateTimeStartOf"
+      | uop_date_time_start_of_day => "dateTimeStartOfDay"
+      | uop_date_time_start_of_week => "dateTimeStartOfWeek"
+      | uop_date_time_start_of_month => "dateTimeStartOfMonth"
+      | uop_date_time_start_of_quarter => "dateTimeStartOfQuarter"
+      | uop_date_time_start_of_year => "dateTimeStartOfYear"
       | uop_date_time_end_of_day => "dateTimeEndOfDay"
       | uop_date_time_end_of_week => "dateTimeEndOfWeek"
       | uop_date_time_end_of_month => "dateTimeEndOfMonth"
       | uop_date_time_end_of_quarter => "dateTimeEndOfQuarter"
-      | uop_date_time_end_of_year => "dateTimeEndOfYears"
+      | uop_date_time_end_of_year => "dateTimeEndOfYear"
       | uop_date_time_format_from_string => "dateTimeFormatFromString"
       | uop_date_time_from_string => "DateTimeFromString"
       | uop_date_time_max => "dateTimeMax"
@@ -613,6 +613,57 @@ Section DateTimeOperators.
       | EJsonRuntimeDateTimeDiff => "dateTimeDiff"
       end.
 
+    Definition ejson_date_time_runtime_op_fromstring (s:string) : option ejson_date_time_runtime_op :=
+      match s with
+      (* Unary *)
+      | "dateTimeGetSeconds" => Some EJsonRuntimeDateTimeGetSeconds
+      | "dateTimeGetMinutes" => Some EJsonRuntimeDateTimeGetMinutes
+      | "dateTimeGetHours" => Some EJsonRuntimeDateTimeGetHours
+      | "dateTimeGetDays" => Some EJsonRuntimeDateTimeGetDays
+      | "dateTimeGetWeeks" => Some EJsonRuntimeDateTimeGetWeeks
+      | "dateTimeGetMonths" => Some EJsonRuntimeDateTimeGetMonths
+      | "dateTimeGetQuarters" => Some EJsonRuntimeDateTimeGetQuarters
+      | "dateTimeGetYears" => Some EJsonRuntimeDateTimeGetYears
+      | "dateTimeStartOfDay" => Some EJsonRuntimeDateTimeStartOfDay
+      | "dateTimeStartOfWeek" => Some EJsonRuntimeDateTimeStartOfWeek
+      | "dateTimeStartOfMonth" => Some EJsonRuntimeDateTimeStartOfMonth
+      | "dateTimeStartOfQuarter" => Some EJsonRuntimeDateTimeStartOfQuarter
+      | "dateTimeStartOfYear" => Some EJsonRuntimeDateTimeStartOfYear
+      | "dateTimeEndOfDay" => Some EJsonRuntimeDateTimeEndOfDay
+      | "dateTimeEndOfWeek" => Some EJsonRuntimeDateTimeEndOfWeek
+      | "dateTimeEndOfMonth" => Some EJsonRuntimeDateTimeEndOfMonth
+      | "dateTimeEndOfQuarter" => Some EJsonRuntimeDateTimeEndOfQuarter
+      | "dateTimeEndOfYear" => Some EJsonRuntimeDateTimeEndOfYear
+      | "dateTimeFormatFromString" => Some EJsonRuntimeDateTimeFormatFromString
+      | "dateTimeFromString" => Some EJsonRuntimeDateTimeFromString
+      | "dateTimeMax" => Some EJsonRuntimeDateTimeMax
+      | "dateTimeMin" => Some EJsonRuntimeDateTimeMin
+      | "dateTimeDurationAmount" => Some EJsonRuntimeDateTimeDurationAmount
+      | "dateTimeDurationFromString" => Some EJsonRuntimeDateTimeDurationFromString
+      | "dateTimePeriodFromString" => Some EJsonRuntimeDateTimePeriodFromString
+      | "dateTimeDurationFromSeconds" => Some EJsonRuntimeDateTimeDurationFromSeconds
+      | "dateTimeDurationFromMinutes" => Some EJsonRuntimeDateTimeDurationFromMinutes
+      | "dateTimeDurationFromHours" => Some EJsonRuntimeDateTimeDurationFromHours
+      | "dateTimeDurationFromDays" => Some EJsonRuntimeDateTimeDurationFromDays
+      | "dateTimeDurationFromWeeks" => Some EJsonRuntimeDateTimeDurationFromWeeks
+      | "dateTimePeriodFromDays" => Some EJsonRuntimeDateTimePeriodFromDays
+      | "dateTimePeriodFromWeeks" => Some EJsonRuntimeDateTimePeriodFromWeeks
+      | "dateTimePeriodFromMonths" => Some EJsonRuntimeDateTimePeriodFromMonths
+      | "dateTimePeriodFromQuarters" => Some EJsonRuntimeDateTimePeriodFromQuarters
+      | "dateTimePeriodFromYears" => Some EJsonRuntimeDateTimePeriodFromYears
+      (* Binary *)
+      | "dateTimeFormat" => Some EJsonRuntimeDateTimeFormat
+      | "dateTimeAdd" => Some EJsonRuntimeDateTimeAdd
+      | "dateTimeSubtract" => Some EJsonRuntimeDateTimeSubtract
+      | "dateTimeAddPeriod" => Some EJsonRuntimeDateTimeAddPeriod
+      | "dateTimeSubtractPeriod" => Some EJsonRuntimeDateTimeSubtractPeriod
+      | "dateTimeIsSame" => Some EJsonRuntimeDateTimeIsSame
+      | "dateTimeIsBefore" => Some EJsonRuntimeDateTimeIsBefore
+      | "dateTimeIsAfter" => Some EJsonRuntimeDateTimeIsAfter
+      | "dateTimeDiff" => Some EJsonRuntimeDateTimeDiff
+      | _ => None
+      end.
+
   End toEJson.
 
 End DateTimeOperators.

compiler/core/Backend/Component/LogComponent.v

@@ -71,5 +71,11 @@ Section LogOperators.
       | EJsonRuntimeLogString => "logString"
       end.
 
+    Definition ejson_log_runtime_op_fromstring (s:string) : option ejson_log_runtime_op :=
+      match s with
+      | "logString" => Some EJsonRuntimeLogString
+      | _ => None
+      end.
+
   End toEJson.
 End LogOperators.

compiler/core/Backend/Component/MathComponent.v

@@ -166,5 +166,20 @@ Section MathOperators.
       | EJsonRuntimeTanh => "tanh"
       end.
 
+    Definition ejson_math_runtime_op_fromstring (s:string) : option ejson_math_runtime_op :=
+      match s with
+      | "floatOfString" => Some EJsonRuntimeFloatOfString
+      | "acos" => Some EJsonRuntimeAcos
+      | "asin" => Some EJsonRuntimeAsin
+      | "atan" => Some EJsonRuntimeAtan
+      | "atan2" => Some EJsonRuntimeAtan2
+      | "cos" => Some EJsonRuntimeCos
+      | "cosh" => Some EJsonRuntimeCosh
+      | "sin" => Some EJsonRuntimeSin
+      | "sinh" => Some EJsonRuntimeSinh
+      | "tan" => Some EJsonRuntimeTan
+      | "tanh" => Some EJsonRuntimeTanh
+      | _ => None
+      end.
   End toEJson.
 End MathOperators.

compiler/core/Backend/Component/MonetaryAmountComponent.v

@@ -27,7 +27,7 @@ Import ListNotations.
 Local Open Scope string.
 Local Open Scope nstring_scope.
 
-Axiom MONETARY_AMOUNT_format : Float.float -> String.string -> String.string.
+Axiom MONETARY_AMOUNT_format : FloatAdd.float -> String.string -> String.string.
 Extract Inlined Constant MONETARY_AMOUNT_format => "(fun x1 f -> Util.char_list_of_string (MonetaryAmount.amount_to_string_format x1 (Util.string_of_char_list f)))".
 
 Axiom MONETARY_CODE_format : String.string -> String.string -> String.string.
@@ -75,6 +75,13 @@ Section MonetaryAmountOperators.
       | EJsonRuntimeMonetaryCodeFormat => "monetaryCodeFormat"
       end.
 
+    Definition ejson_monetary_amount_runtime_op_fromstring (s:string) : option ejson_monetary_amount_runtime_op :=
+      match s with
+      | "monetaryAmountFormat" => Some EJsonRuntimeMonetaryAmountFormat
+      | "monetaryCodeFormat" => Some EJsonRuntimeMonetaryCodeFormat
+      | _ => None
+      end.
+
   End toEJson.
 
 End MonetaryAmountOperators.

compiler/core/Backend/Lib/QBackendModel.v

@@ -18,6 +18,8 @@ Require Import ErgoSpec.Backend.Qcert.QcertModel.
 Require Import ErgoSpec.Backend.ForeignErgo.
 
 Module Type QBackendModel.
+  Definition ergo_foreign_ejson : Set := enhanced_ejson.
+  Definition ergo_foreign_ejson_runtime_op : Set := enhanced_foreign_ejson_runtime_op.
   Definition ergo_foreign_data : foreign_data := enhanced_foreign_data.
   Definition ergo_foreign_type : foreign_type := enhanced_foreign_type.
 End QBackendModel.

compiler/core/Backend/Lib/QBackendRuntime.v

@@ -21,6 +21,8 @@ Require Import QBackendModel.
 Module QBackendRuntime <: QBackendModel.
   Local Open Scope string.
 
+  Definition ergo_foreign_ejson : Set := enhanced_ejson.
+  Definition ergo_foreign_ejson_runtime_op : Set := enhanced_foreign_ejson_runtime_op.
   Definition ergo_foreign_data := enhanced_foreign_data.
   Definition ergo_foreign_type := enhanced_foreign_type.
 

compiler/core/Backend/Lib/QCodeGen.v

@@ -52,8 +52,9 @@ Module QCodeGen(ergomodel:QBackendModel).
   End Emit.
 
   Section Imp.
-    Definition imp_ejson_function := ImpEJson.imp_ejson_function.
-    Definition imp_ejson_lib := ImpEJson.imp_ejson.
+
+    Definition imp_ejson_function := @ImpEJson.imp_ejson_function ergomodel.ergo_foreign_ejson ergomodel.ergo_foreign_ejson_runtime_op.
+    Definition imp_ejson_lib := @ImpEJson.imp_ejson ergomodel.ergo_foreign_ejson ergomodel.ergo_foreign_ejson_runtime_op.
 
     Definition nnrc_expr_to_imp_ejson_function
       {bm:brand_model} :=

compiler/core/Backend/Qcert/QcertDataToEJson.v

@@ -38,8 +38,8 @@ Require Import QcertEJson.
 Import ListNotations.
 Local Open Scope list_scope.
 
-Program Instance enhanced_foreign_to_ejson : foreign_to_ejson
-  := mk_foreign_to_ejson enhanced_foreign_runtime enhanced_foreign_ejson _ _ _ _.
+Program Instance enhanced_foreign_to_ejson : foreign_to_ejson _ _
+  := mk_foreign_to_ejson enhanced_ejson enhanced_foreign_ejson_runtime_op enhanced_foreign_ejson enhanced_foreign_runtime _ _ _ _.
 Next Obligation.
   exact j. (* XXX enhanced_ejson is the same as enhanced_data *)
 Defined.
@@ -130,12 +130,12 @@ Proof.
                  (fun a : enhanced_data => QcertData.enhanced_foreign_data_obligation_4 a)
                  (fun (a : enhanced_data) (_ : QcertData.enhanced_foreign_data_obligation_2 a) =>
                   @eq_refl enhanced_data a) QcertData.enhanced_foreign_data_obligation_6))
-           (@ejson enhanced_foreign_ejson)
-           (@data_to_ejson enhanced_foreign_runtime enhanced_foreign_ejson enhanced_foreign_to_ejson) l)
+           (@ejson enhanced_ejson)
+           (@data_to_ejson enhanced_foreign_runtime enhanced_ejson enhanced_foreign_ejson enhanced_foreign_ejson_runtime_op enhanced_foreign_to_ejson) l)
           =
           (ejson_dates
-             (@map (@data (@foreign_runtime_data enhanced_foreign_runtime)) (@ejson enhanced_foreign_ejson)
-                   (@data_to_ejson enhanced_foreign_runtime enhanced_foreign_ejson enhanced_foreign_to_ejson) l))) by reflexivity.
+             (@map (@data (@foreign_runtime_data enhanced_foreign_runtime)) (@ejson enhanced_ejson)
+                   (@data_to_ejson enhanced_foreign_runtime enhanced_ejson enhanced_foreign_ejson enhanced_foreign_ejson_runtime_op enhanced_foreign_to_ejson) l))) by reflexivity.
   rewrite <- H in IHl.
   rewrite <- IHl; clear IHl.
   reflexivity.
@@ -234,12 +234,12 @@ Proof.
   - unfold ejsonLeftToString.
     rewrite IHd; clear IHd.
     destruct
-      (@data_to_ejson enhanced_foreign_runtime enhanced_foreign_ejson enhanced_foreign_to_ejson d);
+      (@data_to_ejson enhanced_foreign_runtime enhanced_ejson enhanced_foreign_ejson enhanced_foreign_ejson_runtime_op enhanced_foreign_to_ejson d);
       try reflexivity.
   - unfold ejsonRightToString.
     rewrite IHd; clear IHd.
     destruct
-      (@data_to_ejson enhanced_foreign_runtime enhanced_foreign_ejson enhanced_foreign_to_ejson d);
+      (@data_to_ejson enhanced_foreign_runtime enhanced_ejson enhanced_foreign_ejson enhanced_foreign_ejson_runtime_op enhanced_foreign_to_ejson d);
       try reflexivity.
   - admit.
 Admitted.
@@ -253,8 +253,10 @@ Admitted.
 
 Program Instance enhanced_foreign_to_ejson_runtime : foreign_to_ejson_runtime :=
   mk_foreign_to_ejson_runtime
-    enhanced_foreign_runtime
+    enhanced_ejson
+    enhanced_foreign_ejson_runtime_op
     enhanced_foreign_ejson
+    enhanced_foreign_runtime
     enhanced_foreign_to_ejson
     enhanced_foreign_ejson_runtime
     _ _ _ _ _ _.

compiler/core/Backend/Qcert/QcertEJson.v

@@ -38,7 +38,7 @@ Local Open Scope list_scope.
 
 Definition enhanced_ejson : Set := enhanced_data.
 
-Program Instance enhanced_foreign_ejson : foreign_ejson
+Program Instance enhanced_foreign_ejson : foreign_ejson enhanced_ejson
   := mk_foreign_ejson enhanced_ejson _ _ _ _ _ _.
 Next Obligation.
   red.
@@ -98,7 +98,29 @@ Definition enhanced_foreign_ejson_runtime_op_tostring op : string :=
   | enhanced_ejson_monetary_amount sop => ejson_monetary_amount_runtime_op_tostring sop
   end.
 
-Definition enhanced_ejson_uri_runtime_op_interp op (dl:list ejson) : option ejson :=
+Definition enhanced_foreign_ejson_runtime_op_fromstring (s:string) : option _ :=
+  match ejson_uri_runtime_op_fromstring s with
+  | Some op => Some (enhanced_ejson_uri op)
+  | None =>
+    match ejson_log_runtime_op_fromstring s with
+    | Some op => Some (enhanced_ejson_log op)
+    | None =>
+      match ejson_math_runtime_op_fromstring s with
+      | Some op => Some (enhanced_ejson_math op)
+      | None =>
+        match ejson_date_time_runtime_op_fromstring s with
+        | Some op => Some (enhanced_ejson_date_time op)
+        | None =>
+          match ejson_monetary_amount_runtime_op_fromstring s with
+          | Some op => Some (enhanced_ejson_monetary_amount op)
+          | None => None
+          end
+        end
+      end
+    end
+  end.
+
+Definition enhanced_ejson_uri_runtime_op_interp op (dl:list (@ejson enhanced_ejson)) : option ejson :=
   match op with
   | EJsonRuntimeUriEncode =>
     apply_unary
@@ -116,7 +138,7 @@ Definition enhanced_ejson_uri_runtime_op_interp op (dl:list ejson) : option ejso
          end) dl
   end.
 
-Definition onjstringunit (f : String.string -> unit) (j : ejson) : option ejson :=
+Definition onjstringunit (f : String.string -> unit) (j : (@ejson enhanced_ejson)) : option (@ejson enhanced_ejson) :=
   match j with
   | ejstring s =>
     match f s with                                            (* Call log *)
@@ -132,7 +154,7 @@ Definition enhanced_ejson_log_runtime_op_interp op (dl:list ejson) : option ejso
       (onjstringunit LOG_string) dl
   end.
 
-Definition enhanced_ejson_math_runtime_op_interp op (dl:list ejson) : option ejson :=
+Definition enhanced_ejson_math_runtime_op_interp op (dl:list (@ejson enhanced_ejson)) : option (@ejson enhanced_ejson) :=
   match op with
   | EJsonRuntimeFloatOfString =>
     apply_unary
@@ -588,7 +610,7 @@ Definition enhanced_ejson_date_time_runtime_op_interp op (dl:list ejson) : optio
          end) dl
   end.
 
-Definition enhanced_ejson_monetary_amount_runtime_op_interp op (dl:list ejson) : option ejson :=
+Definition enhanced_ejson_monetary_amount_runtime_op_interp op (dl:list (@ejson enhanced_ejson)) : option ejson :=
   match op with
   (* Binary *)
   | EJsonRuntimeMonetaryAmountFormat =>
@@ -624,7 +646,7 @@ Definition enhanced_foreign_ejson_runtime_op_interp op :=
   end.
 
 Section toString. (* XXX Maybe to move as a component ? *)
-  Fixpoint ejsonEnumToString (b:brands) (j:ejson) : string :=
+  Fixpoint ejsonEnumToString (b:brands) (j:@ejson enhanced_ejson) : string :=
     match j with
     | ejobject ((s1,j)::nil) =>
       if (string_dec s1 "$left") then
@@ -735,8 +757,8 @@ Section toString. (* XXX Maybe to move as a component ? *)
 
 End toString.
 
-Program Instance enhanced_foreign_ejson_runtime : foreign_ejson_runtime :=
-  mk_foreign_ejson_runtime enhanced_foreign_ejson enhanced_foreign_ejson_runtime_op _ _ _ _ _.
+Program Instance enhanced_foreign_ejson_runtime : foreign_ejson_runtime enhanced_foreign_ejson_runtime_op :=
+  mk_foreign_ejson_runtime enhanced_foreign_ejson_runtime_op enhanced_ejson enhanced_foreign_ejson _ _ _ _ _ _.
 Next Obligation.
   red; unfold equiv; intros.
   change ({x = y} + {x <> y}).
@@ -757,6 +779,9 @@ Defined.
 Next Obligation.
   exact (ejsonToString H).
 Defined.
+Next Obligation.
+  exact (enhanced_foreign_ejson_runtime_op_fromstring H).
+Defined.
 Next Obligation.
   exact (ejsonToText H).
 Defined.

compiler/core/Backend/Qcert/QcertEJsonToJSON.v

@@ -63,7 +63,7 @@ Definition enhanced_foreign_ejson_to_json (ej:enhanced_ejson) : json :=
   end.
 
 Program Instance enhanced_foreign_to_json : foreign_to_json
-  := mk_foreign_to_json enhanced_foreign_ejson _ _.
+  := mk_foreign_to_json enhanced_ejson enhanced_foreign_ejson _ _.
 Next Obligation.
   exact (enhanced_foreign_json_to_ejson fd).
 Defined.

compiler/core/Backend/Qcert/QcertModel.v

@@ -88,9 +88,13 @@ Module EnhancedModel(bm:CompilerBrandModel(EnhancedForeignType)) <: CompilerMode
     := @enhanced_basic_model bm.compiler_brand_model.
   Definition compiler_model_foreign_runtime : foreign_runtime
     := enhanced_foreign_runtime.
-  Definition compiler_model_foreign_ejson : foreign_ejson
+  Definition compiler_model_foreign_ejson_model : Set
+    := enhanced_ejson.
+  Definition compiler_model_foreign_ejson : foreign_ejson compiler_model_foreign_ejson_model
     := enhanced_foreign_ejson.
-  Definition compiler_model_foreign_to_ejson : foreign_to_ejson
+  Definition compiler_model_foreign_ejson_runtime_op : Set
+    := enhanced_foreign_ejson_runtime_op.
+  Definition compiler_model_foreign_to_ejson : foreign_to_ejson compiler_model_foreign_ejson_model compiler_model_foreign_ejson_runtime_op
     := enhanced_foreign_to_ejson.
   Definition compiler_model_foreign_to_ejson_runtime : foreign_to_ejson_runtime
     := enhanced_foreign_to_ejson_runtime.