Skip to content

Commit

Permalink
(fix) Alternative JavaScript code-generation with fix to integer cons…
Browse files Browse the repository at this point in the history
…tant serialization accordproject#484

Signed-off-by: Jerome Simeon <[email protected]>
  • Loading branch information
jeromesimeon committed Dec 14, 2018
1 parent a76e142 commit fc7dd0e
Show file tree
Hide file tree
Showing 6 changed files with 6,027 additions and 5,464 deletions.
1 change: 1 addition & 0 deletions Makefile.coq_modules
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ MODULES = \
Backend/Model/ErgoEnhancedModel \
Backend/Model/ErgoBackendModel \
Backend/Model/ErgoBackendRuntime \
Backend/Lib/ENNRCtoJavaScript \
Backend/Lib/ECType \
Backend/Lib/EData \
Backend/Lib/EOperators \
Expand Down
18 changes: 10 additions & 8 deletions mechanization/Backend/Lib/ECodeGen.v
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ Require Qcert.Compiler.Driver.CompLang.
Require Import ErgoSpec.Backend.Model.ErgoBackendModel.
Require Import ErgoSpec.Backend.Model.ErgoBackendRuntime.

Require Import ErgoSpec.Backend.Lib.ENNRCtoJavaScript.

Module ECodeGen(ergomodel:ErgoBackendModel).
(* NNRC *)
Definition nnrc_expr := NNRC.nnrc.
Expand All @@ -28,18 +30,18 @@ Module ECodeGen(ergomodel:ErgoBackendModel).
Definition nnrc_expr_java_unshadow := NNRCtoJava.nnrcToJavaunshadow.

(* JavaScript code generation *)
Definition javascript_indent := NNRCtoJavaScript.indent.
Definition javascript_quotel_double := NNRCtoJavaScript.quotel_double.
Definition javascript_eol_newline := NNRCtoJavaScript.eol_newline.
Definition javascript_indent := ENNRCtoJavaScript.indent.
Definition javascript_quotel_double := ENNRCtoJavaScript.quotel_double.
Definition javascript_eol_newline := ENNRCtoJavaScript.eol_newline.

Definition javascript_identifier_sanitizer := NNRCtoJavaScript.jsIdentifierSanitize.
Definition javascript_identifier_sanitizer := ENNRCtoJavaScript.jsIdentifierSanitize.

Definition javascript := CompLang.javascript.

Definition nnrc_expr_javascript_unshadow := NNRCtoJavaScript.nnrcToJSunshadow.
Definition nnrc_expr_to_javascript := NNRCtoJavaScript.nnrcToJS.
Definition nnrc_expr_javascript_unshadow := ENNRCtoJavaScript.nnrcToJSunshadow.
Definition nnrc_expr_to_javascript := ENNRCtoJavaScript.nnrcToJS.

Definition nnrc_expr_to_javascript_method := NNRCtoJavaScript.nnrcToJSMethod.
Definition nnrc_expr_to_javascript_method := ENNRCtoJavaScript.nnrcToJSMethod.

Definition nnrc_expr_to_javascript_fun_lift
(e:nnrc_expr)
Expand All @@ -49,7 +51,7 @@ Module ECodeGen(ergomodel:ErgoBackendModel).
(eol:String.string)
(quotel:String.string) : javascript :=
cNNRC.lift_nnrc_core
(fun e => NNRCtoJavaScript.nnrcToJSFun input_v e init_indent eol quotel (input_v::nil) fname)
(fun e => ENNRCtoJavaScript.nnrcToJSFun input_v e init_indent eol quotel (input_v::nil) fname)
(NNRC.nnrc_to_nnrc_core e).

(* Java code generation *)
Expand Down
Loading

0 comments on commit fc7dd0e

Please sign in to comment.