feature(setState) New statement to set a specific state variable #143

Signed-off-by: Jerome Simeon <[email protected]>
accordproject · Oct 8, 2019 · 73851b8 · 73851b8
1 parent 698f739
commit 73851b8
Show file tree

Hide file tree

Showing 24 changed files with 30,117 additions and 29,534 deletions.
diff --git a/backends/javascript/ergo-runtime.js b/backends/javascript/ergo-runtime.js
@@ -30,11 +30,11 @@ function unwrap(doc) {
 }
 function concat(r1, r2) {
     var result = { };
-    for (var key1 in r1)
-        result[key1] = r1[key1];
     for (var key2 in r2)
-        if (!(key2 in r1))
-            result[key2] = r2[key2];
+        result[key2] = r2[key2];
+    for (var key1 in r1)
+        if (!(key1 in r2))
+            result[key1] = r1[key1];
     return result;
 }
 function contains(v, b) {

diff --git a/examples/helloworldstate/logic.ergo b/examples/helloworldstate/logic.ergo
@@ -17,18 +17,18 @@ namespace org.accordproject.helloworldstate
 contract HelloWorldState over TemplateModel state State {
   // Simple Clause
   clause helloworldstate(request : MyRequest) : MyResponse {
-    set state State{
-      counter: state.counter + 1.0
-    };
+    set state.counter = state.counter + 1.0;
+    set state.lastInput = request.input;
     return MyResponse{
       output: "Hello " ++ contract.name ++
-			" (" ++ request.input ++ ")" ++ " (" ++ toString(state.counter) ++ ")"
+      " (" ++ request.input ++ ")" ++ " (" ++ toString(state.counter) ++ ")"
     }
   }
 
   clause init() : Unit {
     set state State{
-      counter: 0.0
+      counter: 0.0,
+      lastInput: ""
     };
     return
   }

diff --git a/examples/helloworldstate/logicOld.ergo b/examples/helloworldstate/logicOld.ergo
@@ -0,0 +1,37 @@
+/*
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+namespace org.accordproject.helloworldstate
+
+contract HelloWorldState over TemplateModel state State {
+  // Simple Clause
+  clause helloworldstate(request : MyRequest) : MyResponse {
+		set state State{
+			counter: state.counter + 1.0,
+			lastInput: request.input
+		};
+    return MyResponse{
+      output: "Hello " ++ contract.name ++
+      " (" ++ request.input ++ ")" ++ " (" ++ toString(state.counter) ++ ")"
+    }
+  }
+
+  clause init() : Unit {
+    set state State{
+      counter: 0.0,
+      lastInput: ""
+    };
+    return
+  }
+}
diff --git a/examples/helloworldstate/model.cto b/examples/helloworldstate/model.cto
@@ -24,6 +24,7 @@ transaction MyResponse {
 
 concept State {
   o Double counter
+  o String lastInput
 }
 
 /**

diff --git a/examples/helloworldstate/request.json → examples/helloworldstate/request1.json b/examples/helloworldstate/request.json → examples/helloworldstate/request1.json
diff --git a/examples/helloworldstate/request2.json b/examples/helloworldstate/request2.json
@@ -0,0 +1,4 @@
+{
+    "$class": "org.accordproject.helloworldstate.MyRequest",
+    "input": "Linux Foundation"
+}
diff --git a/examples/helloworldstate/state.json → examples/helloworldstate/state1.json b/examples/helloworldstate/state.json → examples/helloworldstate/state1.json
@@ -1,4 +1,5 @@
 {
     "$class": "org.accordproject.helloworldstate.State",
-		"counter" : 0
+		"counter" : 0,
+    "lastInput" : ""
 }
diff --git a/examples/helloworldstate/state2.json b/examples/helloworldstate/state2.json
@@ -0,0 +1,5 @@
+{
+    "$class": "org.accordproject.helloworldstate.State",
+		"counter" : 1,
+    "lastInput" : "Accord Project"
+}
diff --git a/extraction/src/ErgoParser.mly b/extraction/src/ErgoParser.mly
@@ -418,6 +418,8 @@ stmt:
     { ErgoCompiler.senforce (mk_provenance $startpos $endpos) e1 None s3 }
 | SET STATE e1 = expr SEMI s2 = stmt
     { ErgoCompiler.ssetstate (mk_provenance $startpos $endpos) e1 s2 }
+| SET STATE DOT a = safeident EQUAL e2 = expr SEMI s2 = stmt
+    { ErgoCompiler.ssetstatedot (mk_provenance $startpos $endpos) a e2 s2 }
 | EMIT e1 = expr SEMI s2 = stmt
     { ErgoCompiler.semit (mk_provenance $startpos $endpos) e1 s2 }
 | MATCH e0 = expr csd = cases_stmt

diff --git a/mechanization/Common/Result.v b/mechanization/Common/Result.v
@@ -177,6 +177,8 @@ Section Result.
       efailure (ECompilationError prov "Cannot use 'clause' variable outside of a clause").
     Definition case_option_not_on_either_error {A} prov : eresult A :=
       efailure (ECompilationError prov "Cannot match unless against an option type").
+    Definition set_state_on_non_brand_error {A} prov name : eresult A :=
+      efailure (ECompilationError prov ("Cannot use 'set state." ++ name ++ " on non-objet state")).
 
     (* CTO errors *)
     Definition import_not_found_error {A} prov (import:string) : eresult A :=

diff --git a/mechanization/Compiler/ErgoCompiler.v b/mechanization/Compiler/ErgoCompiler.v
@@ -269,6 +269,8 @@ Module ErgoCompiler.
     Ergo.SCallContract prov e0 (e1::nil).
   Definition ssetstate prov e s : ergo_stmt :=
     Ergo.SSetState prov e s.
+  Definition ssetstatedot prov a e s : ergo_stmt :=
+    Ergo.SSetStateDot prov a e s.
   Definition semit prov e s : ergo_stmt :=
     Ergo.SEmit prov e s.
   Definition slet prov (v:String.string) (t:option ErgoType.ergo_type) (e1:ergo_expr) (s2:ergo_stmt) : ergo_stmt :=

diff --git a/mechanization/Ergo/Lang/Ergo.v b/mechanization/Ergo/Lang/Ergo.v
@@ -100,6 +100,7 @@ Section Ergo.
     | SCallClause : A -> ergo_expr -> string -> list ergo_expr -> ergo_stmt (**r clause call *)
     | SCallContract : A -> ergo_expr -> list ergo_expr -> ergo_stmt (**r contract call *)
     | SSetState : A -> ergo_expr -> ergo_stmt -> ergo_stmt
+    | SSetStateDot : A -> string -> ergo_expr -> ergo_stmt -> ergo_stmt
     | SEmit : A -> ergo_expr -> ergo_stmt -> ergo_stmt
     | SLet : A -> string -> option (@ergo_type A N) -> ergo_expr -> ergo_stmt -> ergo_stmt (**r local variable *)
     | SPrint : A -> ergo_expr -> ergo_stmt -> ergo_stmt (**r local variable *)
@@ -116,6 +117,7 @@ Section Ergo.
       | SCallClause a _ _ _ => a
       | SCallContract a _ _ => a
       | SSetState a _ _ => a
+      | SSetStateDot a _ _ _ => a
       | SEmit a _ _ => a
       | SLet a _ _ _ _ => a
       | SPrint a _ _ => a

diff --git a/mechanization/ErgoC/Lang/ErgoCSugar.v b/mechanization/ErgoC/Lang/ErgoCSugar.v
@@ -41,6 +41,18 @@ Section ErgoCSugar.
   Definition thisThis (prov:provenance) : ergoc_expr :=
     EVar prov this_this.
 
+  (* [[ set state.name = e1; s2 ]]
+     ==
+     brand tname (([name : e1] ⊕ !state))
+   *)
+  Definition setStateDot (prov:provenance) name tname e1 e2 : ergoc_expr :=
+    setState prov
+             (EUnaryBuiltin prov (OpBrand (tname::nil))
+                            (EBinaryBuiltin prov OpRecConcat
+                                            (EUnaryBuiltin prov OpUnbrand (EVar prov local_state))
+                                            (EUnaryBuiltin prov (OpRec name) e1)))
+             e2.
+
   Definition thisContract (prov:provenance) : ergoc_expr :=
     let prov := ProvThisContract (loc_of_provenance prov) in
     EVar prov this_contract.

diff --git a/mechanization/Translation/ErgoCompContext.v b/mechanization/Translation/ErgoCompContext.v
@@ -47,6 +47,7 @@ Section ErgoCompContext.
         compilation_context_type_decls : list laergo_type_declaration;     (**r type declarations *)
         compilation_context_new_type_decls : list laergo_type_declaration; (**r new type declarations *)
         compilation_context_warnings : list ewarning;                      (**r warnings up to that point *)
+        compilation_context_state_type : option laergo_type;               (**r current state type *)
       }.
 
   Definition namespace_ctxt_of_compilation_context (ctxt:compilation_context) : namespace_ctxt :=
@@ -65,7 +66,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_update_function_env
              (ctxt : compilation_context)
@@ -82,7 +84,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition update_function_group_env
              (gname:string)
@@ -110,7 +113,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_update_global_env
              (ctxt : compilation_context)
@@ -127,7 +131,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_update_local_env
              (ctxt : compilation_context)
@@ -144,7 +149,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_set_local_env
              (ctxt : compilation_context)
@@ -160,7 +166,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_update_params_env
              (ctxt : compilation_context)
@@ -176,7 +183,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_set_params_env
              (ctxt : compilation_context)
@@ -192,7 +200,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition set_namespace_in_compilation_context
              (ns:namespace_name)
@@ -205,7 +214,8 @@ Section ErgoCompContext.
          (namespace_ctxt_of_compilation_context ctxt)
          ns).
 
-  Definition set_current_contract (ctxt:compilation_context) (cname:string) : compilation_context :=
+  Definition set_current_contract (ctxt:compilation_context) (cname:string) (tname:option laergo_type)
+    : compilation_context :=
     mkCompCtxt ctxt.(compilation_context_namespace)
                ctxt.(compilation_context_function_env)
                ctxt.(compilation_context_function_group_env)
@@ -217,7 +227,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               tname.
 
   Definition set_current_clause (ctxt:compilation_context) (cname:string) : compilation_context :=
     mkCompCtxt ctxt.(compilation_context_namespace)
@@ -231,7 +242,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_update_type_ctxt
              (ctxt: compilation_context)
@@ -247,7 +259,8 @@ Section ErgoCompContext.
                nctxt
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_update_type_declarations
              (ctxt: compilation_context)
@@ -264,7 +277,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                (sort_decls old_decls)
                (sort_decls new_decls)
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_add_new_type_declaration
              (ctxt: compilation_context)
@@ -280,7 +294,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                (sort_decls (ctxt.(compilation_context_new_type_decls) ++ (decl::nil)))
-               ctxt.(compilation_context_warnings).
+               ctxt.(compilation_context_warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_add_warnings
              (ctxt: compilation_context)
@@ -296,7 +311,8 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               (ctxt.(compilation_context_warnings) ++ warnings).
+               (ctxt.(compilation_context_warnings) ++ warnings)
+               ctxt.(compilation_context_state_type).
 
   Definition compilation_context_reset_warnings
              (ctxt: compilation_context) : compilation_context :=
@@ -311,13 +327,14 @@ Section ErgoCompContext.
                ctxt.(compilation_context_type_ctxt)
                ctxt.(compilation_context_type_decls)
                ctxt.(compilation_context_new_type_decls)
-               nil.
+               nil
+               ctxt.(compilation_context_state_type).
 
   Definition get_all_decls ctxt : list laergo_type_declaration :=
     sort_decls (ctxt.(compilation_context_type_decls) ++ ctxt.(compilation_context_new_type_decls)).
 
   Definition init_compilation_context nsctxt decls : compilation_context :=
-    mkCompCtxt nsctxt nil nil nil nil nil None None empty_type_context decls nil nil.
+    mkCompCtxt nsctxt nil nil nil nil nil None None empty_type_context decls nil nil None.
 
   Definition is_abstract_class
              (ctxt: compilation_context)
@@ -326,4 +343,8 @@ Section ErgoCompContext.
     then true
     else false.
 
+  Definition is_state_type_branded (ctxt: compilation_context) : option string :=
+    let t := ctxt.(compilation_context_state_type) in
+    olift type_name_of_type t.
+
 End ErgoCompContext.
diff --git a/mechanization/Translation/ErgoNameResolve.v b/mechanization/Translation/ErgoNameResolve.v
@@ -510,6 +510,10 @@ Section ErgoNameResolution.
         elift2 (SSetState prov)
                (resolve_ergo_expr nsctxt e1)
                (resolve_ergo_stmt nsctxt s2)
+      | SSetStateDot prov a e1 s2 =>
+        elift2 (SSetStateDot prov a)
+               (resolve_ergo_expr nsctxt e1)
+               (resolve_ergo_stmt nsctxt s2)
       | SEmit prov e1 s2 =>
         elift2 (SEmit prov)
                (resolve_ergo_expr nsctxt e1)

diff --git a/mechanization/Translation/ErgotoErgoC.v b/mechanization/Translation/ErgotoErgoC.v
@@ -238,6 +238,15 @@ Section ErgotoErgoC.
       elift2 (setState prov)
              (ergo_expr_to_ergoc_expr ctxt e1)
              (ergo_stmt_to_expr ctxt s2)
+    | SSetStateDot prov a e1 s2 =>
+      match is_state_type_branded ctxt with
+      | None =>
+        set_state_on_non_brand_error (expr_annot e1) a
+      | Some tname =>
+        elift2 (setStateDot prov a tname)
+               (ergo_expr_to_ergoc_expr ctxt e1)
+               (ergo_stmt_to_expr ctxt s2)
+      end
     | SEmit prov e1 s2 =>
       elift2 (pushEmit prov)
              (ergo_expr_to_ergoc_expr ctxt e1)
@@ -389,10 +398,11 @@ Section ErgotoErgoC.
       elift
         (fun x => (x::nil, ctxt))
         (elift (DCContract prov cn)
-               (let ctxt := set_current_contract ctxt cn in
+               (let statet := c.(contract_state) in
+                let ctxt := set_current_contract ctxt cn statet in
                 contract_to_calculus ctxt c))
     | DSetContract prov cn e1 =>
-      let ctxt := set_current_contract ctxt cn in
+      let ctxt := set_current_contract ctxt cn None in
       elift
         (fun x => (x :: (DCConstant prov this_state None (EConst prov dunit)) :: nil,ctxt))
         (elift (DCConstant prov this_contract None)
-Original file line number
+Diff line change
@@ Expand Up / @@ -24,6 +24,7 @@ transaction MyResponse { @@
     concept State {
       o Double counter
+      o String lastInput
     }
     /**
@@ Expand Down @@