(feature) Compiles state type to an annotation for the javascript_cic…

…ero target

Signed-off-by: Jerome Simeon <[email protected]>

examples/installment-sale/logic.ergo

@@ -13,7 +13,7 @@
  */
  namespace org.accordproject.installmentsale
 
-contract InstallmentSale over TemplateModel {
+contract InstallmentSale over TemplateModel state InstallmentSaleState {
   clause init(request : InitializeRequest) : InitializeResponse {
     set state new InstallmentSaleState{
       stateId: "org.accordproject.installmentsale.InstallmentSaleState#1",

mechanization/Common/Types/ErgoType.v

@@ -315,4 +315,36 @@ Section ErgoType.
     (* Eval vm_compute in res. *)
   End Examples.
 
+  Definition lift_default_emits_type (emits:option ergo_type) : ergo_type :=
+    match emits with
+    | Some e => e
+    | None => ErgoTypeClassRef default_emits_type
+    end.
+
+  Definition lift_default_state_type (state:option ergo_type) : ergo_type :=
+    match state with
+    | Some e => e
+    | None => ErgoTypeClassRef default_state_type
+    end.
+
+  Definition lift_default_throws_type (emits:option ergo_type) : ergo_type :=
+    match emits with
+    | Some e => e
+    | None => ErgoTypeClassRef default_throws_type
+    end.
+
+  Definition mk_success_type (response_type state_type emit_type: ergo_type) :=
+    ErgoTypeRecord (("response",response_type)::("state",state_type)::("emit",emit_type)::nil)%string.
+  Definition mk_error_type (throw_type: ergo_type) :=
+    throw_type.
+  Definition mk_output_type (success_type error_type: ergo_type) :=
+    ErgoTypeSum success_type error_type.
+
+  Definition lift_default_state_name (state:option ergo_type) : eresult absolute_name :=
+    match state with
+    | None => esuccess default_state_name
+    | Some (ErgoTypeClassRef (AbsoluteRef r)) => esuccess r
+    | _ => unresolved_name_error
+    end.
+
 End ErgoType.

mechanization/Common/Utils/ENames.v

@@ -60,13 +60,13 @@ Section ENames.
   Section TypeNames.
     Definition default_request_name : string := "org.accordproject.cicero.runtime.Request".
     Definition default_response_name : string := "org.accordproject.cicero.runtime.Response".
-    Definition default_event_name : string := "org.hyperledger.composer.system.Event".
+    Definition default_emits_name : string := "org.hyperledger.composer.system.Event".
     Definition default_state_name : string := "org.accordproject.cicero.contract.AccordContractState".
     Definition default_throws_name : string := "org.accordproject.cicero.contract.ErrorResponse".
 
     Definition default_request_type := AbsoluteRef default_request_name.
     Definition default_response_type := AbsoluteRef default_response_name.
-    Definition default_event_type := AbsoluteRef default_event_name.
+    Definition default_emits_type := AbsoluteRef default_emits_name.
     Definition default_state_type := AbsoluteRef default_state_name.
     Definition default_throws_type := AbsoluteRef default_throws_name.
   End TypeNames.

mechanization/Common/Utils/EResult.v

@@ -86,6 +86,9 @@ Section EResult.
     Definition enforce_error_content : ErgoData.data :=
       ErgoData.dbrand (ergo_default_error_name::nil)
                       (ErgoData.drec (("message"%string, ErgoData.dstring "Enforce condition failed")::nil)).
+
+    Definition unresolved_name_error {A} : eresult A :=
+      efailure (CompilationError ("Unresolved name")).
   End Builtin.
 
 End EResult.

mechanization/Ergo/Lang/Ergo.v

@@ -141,6 +141,12 @@ Section Ergo.
 
     Definition lookup_single_contract (p:ergo_module) : eresult ergo_contract :=
       lookup_single_contract_in_declarations p.(module_declarations).
+
+    Definition lookup_single_contract_with_state (p:ergo_module) : eresult (ergo_contract * string) :=
+      eolift (fun ec =>
+               elift (fun ecstate =>
+                        (ec, ecstate)) (lift_default_state_name ec.(contract_state)))
+            (lookup_single_contract_in_declarations p.(module_declarations)).
 
   End Lookup.
 

mechanization/Ergo/Lang/ErgoExpand.v

@@ -126,7 +126,7 @@ Section ErgoExpand.
                 (("request"%string,(ErgoTypeClassRef default_request_type))::nil)
                 ErgoTypeNone
                 None
-                (Some (ErgoTypeClassRef default_event_type))
+                (Some (ErgoTypeClassRef default_emits_type))
                 init_body).
 
   Definition add_init_clause_to_contract (namespace:string) (c:ergo_contract) : ergo_contract :=

mechanization/Translation/ErgoNNRCtoJavaScriptCicero.v

@@ -31,15 +31,17 @@ Section ErgoNNRCtoJavaScriptCicero.
              (clause_name:string)
              (request_type:string)
              (response_type:string)
-             (emits_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 {" ++ emits_type ++ "} context.emit - the emitted events" ++ 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.
@@ -53,7 +55,8 @@ Section ErgoNNRCtoJavaScriptCicero.
              (fun_name:string)
              (request_type:string)
              (response_type:string)
-             (emits_type:string)
+             (emit_type:string)
+             (state_type:string)
              (contract_name:string)
              (clause_name:string)
              (eol:string)
@@ -69,7 +72,8 @@ Section ErgoNNRCtoJavaScriptCicero.
        clause_name
        request_type
        response_type
-       emits_type
+       emit_type
+       state_type
        eol
        quotel)
       ++ "function " ++ fun_name ++ "(context) {" ++ eol
@@ -93,24 +97,31 @@ Section ErgoNNRCtoJavaScriptCicero.
 
   Definition apply_wrapper_function
              (contract_name:string)
+             (contract_state_type:string)
              (signature:string * string * string * string)
              (eol:string)
              (quotel:string) : ErgoCodeGen.javascript :=
-    let '(clause_name, request_type, response_type, emits_type) := signature in
+    let '(clause_name, request_type, response_type, emit_type) := signature in
     let fun_name := contract_name ++ "_" ++ clause_name in
     wrapper_function
-      fun_name request_type response_type emits_type contract_name clause_name eol quotel.
+      fun_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))
+             (signatures:list (string * string * string * string) * string)
              (eol:string)
              (quotel:string) : ErgoCodeGen.javascript :=
-    String.concat eol (List.map (fun sig => apply_wrapper_function contract_name sig eol quotel) signatures).
+    String.concat eol
+                  (List.map (fun sig => apply_wrapper_function
+                                          contract_name
+                                          (snd signatures)
+                                          sig
+                                          eol
+                                          quotel) (fst signatures)).
 
   Definition javascript_of_module_with_dispatch
              (contract_name:string)
-             (signatures:list (string * string * string * string))
+             (signatures:list (string * string * string * string) * string)
              (p:nnrc_module)
              (eol:string)
              (quotel:string) : ErgoCodeGen.javascript :=
@@ -143,7 +154,7 @@ Section ErgoNNRCtoJavaScriptCicero.
           | ErgoTypeClassRef reqname, ErgoTypeClassRef outname, None =>
             let qreqname := absolute_name_of_name_ref namespace reqname in
             let qoutname := absolute_name_of_name_ref namespace outname in
-            let qemitsname := default_event_name in
+            let qemitsname := default_emits_name in
             (fname,qreqname,qoutname,qemitsname) :: (filter_signatures namespace rest)
           | _, _, _ =>
             filter_signatures namespace rest
@@ -152,13 +163,24 @@ Section ErgoNNRCtoJavaScriptCicero.
         end
     end.
 
+  Definition filter_signatures_with_state (namespace:string) (contract_state_type:option ergo_type) (sigs:list ergo_type_signature) : list (string * string * string * string) * string :=
+    match contract_state_type with
+    | None => (filter_signatures namespace sigs, default_state_name)
+    | Some (ErgoTypeClassRef statename) =>
+      let qstatename := absolute_name_of_name_ref namespace statename in
+      (filter_signatures namespace sigs, qstatename)
+    | _ =>
+      (nil, "")
+    end.
+
   Definition ergoc_module_to_javascript_cicero
-             (coname:string)
+             (contract_name:string)
+             (contract_state_type:option ergo_type)
              (sigs: list ergo_type_signature)
              (p:nnrc_module) : ErgoCodeGen.javascript :=
     javascript_of_module_with_dispatch
-      coname
-      (filter_signatures p.(modulen_namespace) sigs)
+      contract_name
+      (filter_signatures_with_state p.(modulen_namespace) contract_state_type sigs)
       p
       ErgoCodeGen.javascript_eol_newline
       ErgoCodeGen.javascript_quotel_double.

mechanization/Translation/ErgotoErgoCalculus.v

@@ -75,37 +75,12 @@ Section ErgotoErgoCalculus.
 
   (** Translate a clause to clause+calculus *)
 
-  Definition default_emits_in_clause (emits:option ergo_type) : ergo_type :=
-    match emits with
-    | Some e => e
-    | None => ErgoTypeClassRef default_event_type
-    end.
-
-  Definition default_state_in_clause (state:option ergo_type) : ergo_type :=
-    match state with
-    | Some e => e
-    | None => ErgoTypeClassRef default_state_type
-    end.
-
-  Definition default_throws_in_clause (emits:option ergo_type) : ergo_type :=
-    match emits with
-    | Some e => e
-    | None => ErgoTypeClassRef default_throws_type
-    end.
-
-  Definition mk_success_type (response_type state_type emit_type: ergo_type) :=
-    ErgoTypeRecord (("response",response_type)::("state",state_type)::("emit",emit_type)::nil)%string.
-  Definition mk_error_type (throw_type: ergo_type) :=
-    throw_type.
-  Definition mk_output_type (success_type error_type: ergo_type) :=
-    ErgoTypeSum success_type error_type.
-
   Definition clause_to_calculus (tem:ergo_type) (sta:option ergo_type) (c:ergo_clause) : ergoc_function :=
     let response_type := c.(clause_lambda).(lambda_output) in
-    let emit_type := default_emits_in_clause c.(clause_lambda).(lambda_emits) in
-    let state_type :=  default_state_in_clause sta in
+    let emit_type := lift_default_emits_type c.(clause_lambda).(lambda_emits) in
+    let state_type :=  lift_default_state_type sta in
     let success_type := mk_success_type response_type state_type emit_type in
-    let throw_type := default_throws_in_clause c.(clause_lambda).(lambda_throws) in
+    let throw_type := lift_default_throws_type c.(clause_lambda).(lambda_throws) in
     let error_type := mk_error_type throw_type in
     mkFuncC
       c.(clause_name)

mechanization/Translation/ErgotoJavaScriptCicero.v

@@ -38,13 +38,15 @@ Section ErgotoJavaScriptCicero.
              (p:ergo_module) : eresult javascript :=
     let p := ergo_module_expand p in
     let ec := eolift lookup_single_contract p in
-    let exy := elift (fun c => (c.(contract_name), lookup_contract_signatures c)) ec in
-    let pc := elift module_to_calculus p in
-    let etypes := map cto_package_to_ergo_type_module ctos in
-    let pn := eolift (module_to_nnrc etypes) pc in
-    eolift (fun xy =>
-              elift (ergoc_module_to_javascript_cicero (fst xy) (snd xy)) pn)
-           exy.
+    eolift
+      (fun c : ergo_contract =>
+         let contract_name := c.(contract_name) in 
+         let sigs := lookup_contract_signatures c in
+         let pc := elift module_to_calculus p in
+         let etypes := map cto_package_to_ergo_type_module ctos in
+         let pn := eolift (module_to_nnrc etypes) pc in
+         elift (ergoc_module_to_javascript_cicero contract_name c.(contract_state) sigs) pn)
+      ec.
 
 End ErgotoJavaScriptCicero.