(WIP) set state attribute

Signed-off-by: Jerome Simeon <[email protected]>
jeromesimeon · Oct 7, 2019 · bf43a97 · bf43a97
1 parent 698f739
commit bf43a97
Show file tree

Hide file tree

Showing 14 changed files with 29,896 additions and 29,458 deletions.
diff --git a/examples/helloworldstate/logic.ergo b/examples/helloworldstate/logic.ergo
@@ -17,9 +17,7 @@ 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;
     return MyResponse{
       output: "Hello " ++ contract.name ++
 			" (" ++ request.input ++ ")" ++ " (" ++ toString(state.counter) ++ ")"

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; e2 ]]
+     ==
+     brand tname (([name : e1] ⊕ !state))
+   *)
+  Definition setStateDot (prov:provenance) name tname e1 e2 : ergoc_expr :=
+    ELet prov local_state None
+         (EUnaryBuiltin prov (OpBrand (tname::nil))
+                        (EBinaryBuiltin prov OpRecConcat
+                                        (EUnaryBuiltin prov (OpRec name) e1)
+                                        (EUnaryBuiltin prov OpUnbrand (EVar prov local_state))))
+         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)

diff --git a/mechanization/Types/ErgoType.v b/mechanization/Types/ErgoType.v
@@ -234,4 +234,10 @@ Section ErgoType.
       List.concat (List.map type_declaration_extend_rel decls).
   End Extends.
 
+  Definition type_name_of_type (t:laergo_type) : option string :=
+    match t with
+    | ErgoTypeClassRef _ tname => Some tname
+    | _ => None
+    end.
+
 End ErgoType.