(WIP) Bypasses Coq's String library for final code-generation

Signed-off-by: Jerome Simeon <[email protected]>
accordproject · Jan 14, 2019 · 3a12032 · 3a12032
1 parent ee939d8
commit 3a12032
Show file tree

Hide file tree

Showing 12 changed files with 19,748 additions and 19,667 deletions.
diff --git a/extraction/ErgoExtraction.v b/extraction/ErgoExtraction.v
@@ -36,6 +36,11 @@ Extract Constant Misc.coq_toposort => "(fun label file l -> Util.coq_toposort la
 Extract Constant Misc.coq_time => "(fun msg f x -> Util.coq_time msg f x)".
 Extract Constant Misc.get_local_part => "(fun name -> Util.get_local_part name)".
 
+Extract Constant estring => "string".
+Extract Constant string_to_estring => "(fun s1 -> Util.string_of_char_list s1)".
+Extract Constant estring_to_string => "(fun s1 -> Util.char_list_of_string s1)".
+Extract Constant estring_concat => "(fun s1 s2 -> s1 ^ s2)".
+
 (* Ergo modules *)
 Require ErgoCompiler.
 Extraction "ErgoComp" ErgoCompiler.ErgoCompiler.
diff --git a/extraction/src/ErgoCompile.ml b/extraction/src/ErgoCompile.ml
@@ -21,7 +21,7 @@ open PrettyIL
 
 let res_convert code =
   (* Printf.printf "NNRC Module: %s" (pretty_nnrc_module false 0 false (Jarray []) false code.res_nnrc); *)
-  (string_of_char_list code.res_file, string_of_char_list code.res_content)
+  (string_of_char_list code.res_file, code.res_content)
 
 let compile_module_to_javascript version inputs =
   let code = ErgoCompiler.ergo_module_to_javascript version inputs in

diff --git a/mechanization/Backend/Lib/ECodeGen.v b/mechanization/Backend/Lib/ECodeGen.v
@@ -17,6 +17,7 @@ Require String.
 Require Qcert.Compiler.Driver.CompLang.
 Require Import Qcert.Compiler.Driver.CompDriver.
 
+Require Import ErgoSpec.Utils.Misc.
 Require Import ErgoSpec.Backend.Model.ErgoBackendModel.
 Require Import ErgoSpec.Backend.Model.ErgoBackendRuntime.
 
@@ -40,9 +41,8 @@ Module ECodeGen(ergomodel:ErgoBackendModel).
 
   Definition javascript_identifier_sanitizer := ENNRCtoJavaScript.jsIdentifierSanitize.
 
-  Definition javascript := CompLang.javascript.
+  Definition ejavascript := Misc.ejavascript.
 
-
   Definition nnrc_expr_javascript_unshadow n t1 t2 s1 s2 v h :=
     ENNRCtoJavaScript.nnrcToJSunshadow (nnrc_optim n) t1 t2 s1 s2 v h.
 
@@ -57,8 +57,8 @@ Module ECodeGen(ergomodel:ErgoBackendModel).
              (fname:String.string)
              (input_v:String.string)
              (init_indent:nat)
-             (eol:String.string)
-             (quotel:String.string) : javascript :=
+             (eol:estring)
+             (quotel:estring) : ejavascript :=
     cNNRC.lift_nnrc_core
         (fun e => ENNRCtoJavaScript.nnrcToJSFun input_v e init_indent eol quotel (input_v::nil) fname)
         (NNRC.nnrc_to_nnrc_core e).

diff --git a/mechanization/Backend/Lib/ENNRCtoJavaScript.v b/mechanization/Backend/Lib/ENNRCtoJavaScript.v
diff --git a/mechanization/Compiler/ErgoDriver.v b/mechanization/Compiler/ErgoDriver.v
@@ -202,7 +202,7 @@ Section ErgoDriver.
     Definition ergo_module_to_javascript
                (version:jsversion)
                (ctxt:compilation_context)
-               (p:laergo_module) : eresult (nnrc_module * ErgoCodeGen.javascript) :=
+               (p:laergo_module) : eresult (nnrc_module * ErgoCodeGen.ejavascript) :=
       let pc := ergo_module_to_ergoct ctxt p in
       let pn :=
           coq_time "ergoc(typed)->nnrc"
@@ -242,6 +242,8 @@ Section ErgoDriver.
 
   Section CompilerTop.
 
+    Local Open Scope estring_scope.
+
     Definition ergo_module_to_javascript_top
                (version:jsversion)
                (inputs:list lrergo_input) : eresult result_file :=
@@ -264,7 +266,7 @@ Section ErgoDriver.
                 eolift (fun init : laergo_module * compilation_context =>
                           let (p, ctxt) := init in
                           let res := ergo_module_to_java ctxt p in
-                          elift (fun xy => mkResultFile p.(module_file) (fst xy) (snd xy)) res)
+                          elift (fun xy => mkResultFile p.(module_file) (fst xy) (string_to_estring (snd xy))) res)
                        cinit) bm.
 
     Definition ergo_module_to_cicero_top

diff --git a/mechanization/ErgoNNRC/Lang/ErgoNNRC.v b/mechanization/ErgoNNRC/Lang/ErgoNNRC.v
@@ -17,6 +17,7 @@
 (** * Abstract Syntax *)
 
 Require Import String.
+Require Import ErgoSpec.Utils.Misc.
 Require Import ErgoSpec.Types.ErgoType.
 Require Import ErgoSpec.Backend.ErgoBackend.
 
@@ -65,7 +66,7 @@ Section ErgoNNRC.
     mkResultFile {
         res_file : string;
         res_nnrc : nnrc_module;
-        res_content : string;
+        res_content : estring;
       }.
 
   Section Semantics.

diff --git a/mechanization/Translation/ErgoNNRCtoCicero.v b/mechanization/Translation/ErgoNNRCtoCicero.v
@@ -27,25 +27,26 @@ Require Import ErgoSpec.Translation.ErgoNNRCtoJavaScript.
 
 Section ErgoNNRCtoCicero.
   Local Open Scope string_scope.
+  Local Open Scope estring_scope.
 
   Definition accord_annotation
              (clause_name:string)
              (request_type:string)
              (response_type:string)
              (emit_type:string)
              (state_type:string)
-             (eol:string)
-             (quotel:string) :=
-    "/**" ++ eol
-          ++ " * Execute the smart clause" ++ eol
-          ++ " * @param {Context} context - the Accord context" ++ eol
-          ++ " * @param {" ++ request_type ++ "} context.request - the incoming request" ++ eol
-          ++ " * @param {" ++ response_type ++ "} context.response - the response" ++ eol
-          ++ " * @param {" ++ emit_type ++ "} context.emit - the emitted events" ++ eol
-          ++ " * @param {" ++ state_type ++ "} context.state - the state" ++ eol
-          ++ (if string_dec clause_name clause_init_name then " * @AccordClauseLogicInit" ++ eol else "")
-          ++ " * @AccordClauseLogic" ++ eol
-          ++ " */" ++ eol.
+             (eol:estring)
+             (quotel:estring) : estring :=
+    `"/**" +++ eol
+           +++ `" * Execute the smart clause" +++ eol
+           +++ `" * @param {Context} context - the Accord context" +++ eol
+           +++ `" * @param {" +++ `request_type +++ `"} context.request - the incoming request" +++ eol
+           +++ `" * @param {" +++ `response_type +++ `"} context.response - the response" +++ eol
+           +++ `" * @param {" +++ `emit_type +++ `"} context.emit - the emitted events" +++ eol
+           +++ `" * @param {" +++ `state_type +++ `"} context.state - the state" +++ eol
+           +++ (if string_dec clause_name clause_init_name then `" * @AccordClauseLogicInit" +++ eol else `"")
+           +++ `" * @AccordClauseLogic" +++ eol
+           +++ `" */" +++ eol.
 
   (** Note: this adjusts the external interface to that currently expected in Cicero. Namely:
 - This serialized/deserialized ErgoType objects to/from JSON
@@ -61,14 +62,14 @@ Section ErgoNNRCtoCicero.
              (state_type:string)
              (contract_name:string)
              (clause_name:string)
-             (eol:string)
-             (quotel:string) : string :=
+             (eol:estring)
+             (quotel:estring) : estring :=
     let state_init :=
         if string_dec clause_name clause_init_name
         then
-          "{ '$class': 'org.accordproject.cicero.contract.AccordContractState', 'stateId' : 'org.accordproject.cicero.contract.AccordContractState#1' }"
+          `"{ '$class': 'org.accordproject.cicero.contract.AccordContractState', 'stateId' : 'org.accordproject.cicero.contract.AccordContractState#1' }"
         else
-          "serializer.toJSON(context.state,{permitResourcesForRelationships:true})"
+          `"serializer.toJSON(context.state,{permitResourcesForRelationships:true})"
     in
     (accord_annotation
        clause_name
@@ -78,71 +79,73 @@ Section ErgoNNRCtoCicero.
        state_type
        eol
        quotel)
-      ++ "function " ++ fun_name ++ "(context) {" ++ eol
-      ++ "  let pcontext = { '" ++ request_param ++ "' : serializer.toJSON(context.request,{permitResourcesForRelationships:true}), 'state': " ++ state_init ++ ", 'contract': serializer.toJSON(context.contract,{permitResourcesForRelationships:true}), 'emit': context.emit, 'now': context.now};" ++ eol
-      ++ "  //logger.info('ergo context: '+JSON.stringify(pcontext))" ++ eol
-      ++ "  let result = new " ++ ErgoCodeGen.javascript_identifier_sanitizer contract_name ++ "()." ++ ErgoCodeGen.javascript_identifier_sanitizer clause_name ++ "(pcontext);" ++ eol
-      ++ "  if (result.hasOwnProperty('left')) {" ++ eol
-      ++ "    //logger.info('ergo result: '+JSON.stringify(result))" ++ eol
-      ++ "    context.response = serializer.fromJSON(result.left.response, {validate: false, acceptResourcesForRelationships: true},{permitResourcesForRelationships:true});" ++ eol
-      ++ "    context.state = serializer.fromJSON(result.left.state, {validate: false, acceptResourcesForRelationships: true});" ++ eol
-      ++ "    let emitResult = [];" ++ eol
-      ++ "    for (let i = 0; i < result.left.emit.length; i++) {" ++ eol
-      ++ "      emitResult.push(serializer.fromJSON(result.left.emit[i], {validate: false, acceptResourcesForRelationships: true}));" ++ eol
-      ++ "    }" ++ eol
-      ++ "    context.emit = emitResult;" ++ eol
-      ++ "    return context;" ++ eol
-      ++ "  } else {" ++ eol
-      ++ "    throw new Error(result.right.message);" ++ eol
-      ++ "  }" ++ eol
-      ++ "}" ++ eol.
+      +++ `"function " +++ `fun_name +++ `"(context) {" +++ eol
+      +++ `"  let pcontext = { '" +++ `request_param +++ `"' : serializer.toJSON(context.request,{permitResourcesForRelationships:true}), 'state': " +++ state_init +++ `", 'contract': serializer.toJSON(context.contract,{permitResourcesForRelationships:true}), 'emit': context.emit, 'now': context.now};" +++ eol
+      +++ `"  //logger.info('ergo context: '+JSON.stringify(pcontext))" +++ eol
+      +++ `"  let result = new " +++ `ErgoCodeGen.javascript_identifier_sanitizer contract_name +++ `"()." +++ `ErgoCodeGen.javascript_identifier_sanitizer clause_name +++ `"(pcontext);" +++ eol
+      +++ `"  if (result.hasOwnProperty('left')) {" +++ eol
+      +++ `"    //logger.info('ergo result: '+JSON.stringify(result))" +++ eol
+      +++ `"    context.response = serializer.fromJSON(result.left.response, {validate: false, acceptResourcesForRelationships: true},{permitResourcesForRelationships:true});" +++ eol
+      +++ `"    context.state = serializer.fromJSON(result.left.state, {validate: false, acceptResourcesForRelationships: true});" +++ eol
+      +++ `"    let emitResult = [];" +++ eol
+      +++ `"    for (let i = 0; i < result.left.emit.length; i++) {" +++ eol
+      +++ `"      emitResult.push(serializer.fromJSON(result.left.emit[i], {validate: false, acceptResourcesForRelationships: true}));" +++ eol
+      +++ `"    }" +++ eol
+      +++ `"    context.emit = emitResult;" +++ eol
+      +++ `"    return context;" +++ eol
+      +++ `"  } else {" +++ eol
+      +++ `"    throw new Error(result.right.message);" +++ eol
+      +++ `"  }" +++ eol
+      +++ `"}" +++ eol.
 
   Definition apply_wrapper_function
              (contract_name:string)
              (contract_state_type:string)
              (signature: string * string * string * string * string)
-             (eol:string)
-             (quotel:string) : ErgoCodeGen.javascript :=
+             (eol:estring)
+             (quotel:estring) : ErgoCodeGen.ejavascript :=
     let '(clause_name, request_name, request_type, response_type, emit_type) := signature in
-    let fun_name := ErgoCodeGen.javascript_identifier_sanitizer contract_name ++ "_" ++ ErgoCodeGen.javascript_identifier_sanitizer clause_name in
+    let fun_name : string :=
+        ErgoCodeGen.javascript_identifier_sanitizer contract_name ++ "_"%string ++ ErgoCodeGen.javascript_identifier_sanitizer clause_name
+    in
     wrapper_function
       fun_name request_name request_type response_type emit_type contract_state_type contract_name clause_name eol quotel.
 
   Definition wrapper_functions
              (contract_name:string)
              (signatures:list (string * string * string * string * string) * string)
-             (eol:string)
-             (quotel:string) : ErgoCodeGen.javascript :=
-    String.concat eol
-                  (List.map (fun sig => apply_wrapper_function
-                                          contract_name
-                                          (snd signatures)
-                                          sig
-                                          eol
-                                          quotel) (fst signatures)).
+             (eol:estring)
+             (quotel:estring) : ErgoCodeGen.ejavascript :=
+    econcat eol
+            (List.map (fun sig => apply_wrapper_function
+                                    contract_name
+                                    (snd signatures)
+                                    sig
+                                    eol
+                                    quotel) (fst signatures)).
   Definition javascript_main_dispatch_and_init
              (contract_name:string)
-             (eol:string)
-             (quotel:string) : ErgoCodeGen.javascript :=
-    "" ++ "const contract = new " ++ ErgoCodeGen.javascript_identifier_sanitizer contract_name ++ "();" ++ eol
-       ++ "function dispatch(context) {" ++ eol
-       ++ "  return contract.main(context);" ++ eol
-       ++ "}" ++ eol
-       ++ "function init(context) {" ++ eol
-       ++ "  return contract.init(context);" ++ eol
-       ++ "}" ++ eol.
+             (eol:estring)
+             (quotel:estring) : ErgoCodeGen.ejavascript :=
+    `"" +++ `"const contract = new " +++ `ErgoCodeGen.javascript_identifier_sanitizer contract_name +++ `"();" +++ eol
+        +++ `"function dispatch(context) {" +++ eol
+        +++ `"  return contract.main(context);" +++ eol
+        +++ `"}" +++ eol
+        +++ `"function init(context) {" +++ eol
+        +++ `"  return contract.init(context);" +++ eol
+        +++ `"}" +++ eol.
 
   Definition javascript_of_module_with_dispatch
              (contract_name:string)
              (signatures:list (string * string * string * string * string) * string)
              (p:nnrc_module)
-             (eol:string)
-             (quotel:string) : ErgoCodeGen.javascript :=
-    (preamble eol) ++ eol
-                   ++ (wrapper_functions contract_name signatures eol quotel)
-                   ++ (javascript_of_declarations ES6 p.(modulen_declarations) 0 0 eol quotel)
-                   ++ (javascript_main_dispatch_and_init contract_name eol quotel)
-                   ++ (postamble eol).
+             (eol:estring)
+             (quotel:estring) : ErgoCodeGen.ejavascript :=
+    (preamble eol) +++ eol
+                   +++ (wrapper_functions contract_name signatures eol quotel)
+                   +++ (javascript_of_declarations ES6 p.(modulen_declarations) 0 0 eol quotel)
+                   +++ (javascript_main_dispatch_and_init contract_name eol quotel)
+                   +++ (postamble eol).
 
   Fixpoint filter_signatures
            (namespace:string)
@@ -191,7 +194,7 @@ Section ErgoNNRCtoCicero.
              (contract_name:string)
              (contract_state_type:option ergo_type)
              (sigs: list (string * ergo_type_signature))
-             (p:nnrc_module) : ErgoCodeGen.javascript :=
+             (p:nnrc_module) : ErgoCodeGen.ejavascript :=
     javascript_of_module_with_dispatch
       contract_name
       (filter_signatures_with_state p.(modulen_namespace) contract_state_type sigs)