(fix) Adjust generated code for main/init

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

mechanization/Ergo/Lang/ErgoExpand.v

@@ -85,8 +85,12 @@ Section ErgoExpand.
       match_of_sigs namespace v0 effparam0 effparamrest ss
     end.
 
+  Definition filter_init sigs :=
+    filter (fun s => if (string_dec s.(cto_signature_name) clause_init_name) then false else true) sigs.
+
   Definition create_main_clause_for_contract (namespace:string) (c:ergo_contract) : eresult ergo_clause :=
     let sigs := lookup_contract_signatures c in
+    let sigs := filter_init sigs in
     let effparams := EVar "request"%string :: nil in
     elift
       (fun disp =>

mechanization/Translation/ErgoCalculustoJavaScriptCicero.v

@@ -121,29 +121,33 @@ Section ErgoCalculustoJavaScriptCicero.
     match sigs with
     | nil => nil
     | sig :: rest =>
-      let fname := sig.(cto_signature_name) in
-      let params := sig.(cto_signature_params) in
-      let outtype := sig.(cto_signature_output) in
-      let emitstype := sig.(cto_signature_emits) in
-      match params with
-      | nil => filter_signatures namespace rest
-      | (_,reqtype)::nil =>
-        match reqtype, outtype, emitstype with
-        | CTOClassRef reqname, CTOClassRef outname, Some (CTOClassRef emitsname) =>
-          let qreqname := absolute_ref_of_relative_ref namespace reqname in
-          let qoutname := absolute_ref_of_relative_ref namespace outname in
-          let qemitsname := absolute_ref_of_relative_ref namespace emitsname in
-          (fname,qreqname,qoutname,qemitsname) :: (filter_signatures namespace rest)
-        | CTOClassRef reqname, CTOClassRef outname, None =>
-          let qreqname := absolute_ref_of_relative_ref namespace reqname in
-          let qoutname := absolute_ref_of_relative_ref namespace outname in
-          let qemitsname := default_emits in
-          (fname,qreqname,qoutname,qemitsname) :: (filter_signatures namespace rest)
-        | _, _, _ =>
-          filter_signatures namespace rest
+      if (string_dec sig.(cto_signature_name) clause_main_name)
+      then
+        filter_signatures namespace rest
+      else
+        let fname := sig.(cto_signature_name) in
+        let params := sig.(cto_signature_params) in
+        let outtype := sig.(cto_signature_output) in
+        let emitstype := sig.(cto_signature_emits) in
+        match params with
+        | nil => filter_signatures namespace rest
+        | (_,reqtype)::nil =>
+          match reqtype, outtype, emitstype with
+          | CTOClassRef reqname, CTOClassRef outname, Some (CTOClassRef emitsname) =>
+            let qreqname := absolute_ref_of_relative_ref namespace reqname in
+            let qoutname := absolute_ref_of_relative_ref namespace outname in
+            let qemitsname := absolute_ref_of_relative_ref namespace emitsname in
+            (fname,qreqname,qoutname,qemitsname) :: (filter_signatures namespace rest)
+          | CTOClassRef reqname, CTOClassRef outname, None =>
+            let qreqname := absolute_ref_of_relative_ref namespace reqname in
+            let qoutname := absolute_ref_of_relative_ref namespace outname in
+            let qemitsname := default_emits in
+            (fname,qreqname,qoutname,qemitsname) :: (filter_signatures namespace rest)
+          | _, _, _ =>
+            filter_signatures namespace rest
+          end
+        | _ :: _ => filter_signatures namespace rest
         end
-      | _ :: _ => filter_signatures namespace rest
-      end
     end.
 
   Definition ergoc_package_to_javascript_cicero