Add return types to procedures

src/base/Cashflow.ml

@@ -1876,9 +1876,7 @@ struct
       | AcceptPayment ->
           (AcceptPayment, param_env, field_env, local_env, ctr_tag_map, false)
       | Return i ->
-          let i_tag =
-            lub_tags NotMoney (lookup_var_tag2 i local_env param_env)
-          in
+          let i_tag = lub_tags NoInfo (lookup_var_tag2 i local_env param_env) in
           let new_i = update_id_tag i i_tag in
           let new_local_env, new_param_env =
             update_var_tag2 i i_tag local_env param_env

src/base/TypeChecker.ml

@@ -1022,7 +1022,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct
                   | None ->
                       fail
                         (mk_type_error1
-                           ~kind:"Return type for procedure not found"
+                           ~kind:"Procedure does not return a value"
                            ~inst:(as_error_string p)
                            (SR.get_loc (get_rep p))))
             in
@@ -1054,8 +1054,8 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct
                 fail
                   (mk_type_error1
                      ~kind:
-                       "Procedure with return type cannot be used in forall \
-                        statement"
+                       "Procedures with a return type cannot be used in forall \
+                        statements"
                      ~inst:(as_error_string p)
                      (SR.get_loc (get_rep p)))
             | _ ->
@@ -1114,6 +1114,21 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct
       | CompTrans -> is_legal_transition_parameter_type
       | CompProc -> is_legal_procedure_parameter_type
     in
+    (* Procedure return type has the same restrictions as parameters. *)
+    let%bind comp_return =
+      match comp_return with
+      | Some ret_ty ->
+          if param_checker ret_ty then pure @@ Some ret_ty
+          else
+            fail
+              (mk_type_error1
+                 ~kind:
+                   (sprintf "Type cannot be used as %s return value"
+                      component_type_string)
+                 ~inst:(pp_typ_error ret_ty)
+                 (SR.get_loc (get_rep comp_name)))
+      | None -> pure @@ None
+    in
     let%bind typed_cparams =
       mapM
         ~f:(fun (param, t) ->

tests/typecheck/contracts.t/typecheck-return-3.scilla

@@ -0,0 +1,12 @@
+scilla_version 0
+
+library TypecheckReturn3
+
+contract TypecheckReturn3()
+field f_m: Map Uint32 (Option Uint32) = Emp Uint32 (Option Uint32)
+
+procedure cannot_return_map() -> (Map String String)
+  m := f_m;
+  return m
+end
+

tests/typecheck/contracts.t/typecheck-return-3.scilla.gold

@@ -0,0 +1,4 @@
+
+tests/typecheck/contracts.t/typecheck-return-3.scilla:8:11: error: Type cannot be used as procedure return value: Map (String) (String)
+
+Gas remaining: 8000

tests/typecheck/contracts.t/typecheck-return-4.scilla

@@ -0,0 +1,14 @@
+scilla_version 0
+
+library TypecheckReturn4
+
+contract TypecheckReturn4()
+
+procedure cannot_be_used_in_forall() -> BNum
+  r = _creation_block;
+  return r
+end
+
+transition foo(l: List BNum)
+  forall l cannot_be_used_in_forall
+end

tests/typecheck/contracts.t/typecheck-return-4.scilla.gold

@@ -0,0 +1,4 @@
+
+tests/typecheck/contracts.t/typecheck-return-4.scilla:13:12: error: Procedures with a return type cannot be used in forall statements: cannot_be_used_in_forall
+
+Gas remaining: 8000