motoko-san: refactor assign_stmt

Make it possible to return multiple instructions (for arrays)

src/viper/trans.ml

@@ -398,12 +398,12 @@ and dec ctxt d =
     { ctxt with ids = Env.add x.it Local ctxt.ids },
     fun ctxt' ->
       ([ !!(id x, tr_typ e.note.M.note_typ) ],
-       [ !!(assign_stmt ctxt' (id x) e) ])
+       assign_stmt ctxt' (id x) e d.at)
   | M.(LetD ({it=VarP x;_}, e, None)) ->
      { ctxt with ids = Env.add x.it Local ctxt.ids },
      fun ctxt' ->
        ([ !!(id x, tr_typ e.note.M.note_typ) ],
-        [ !!(assign_stmt ctxt' (id x) e) ])
+        assign_stmt ctxt' (id x) e d.at)
   | M.(ExpD e) -> (* TODO: restrict to e of unit type? *)
      (ctxt,
       fun ctxt' ->
@@ -502,7 +502,7 @@ and stmt ctxt (s : M.exp) : seqn =
      begin match Env.find x.it ctxt.ids with
      | Local ->
         let loc = !!! (x.at) (x.it) in
-        !!([], [!!(assign_stmt ctxt loc e2)])
+        !!([], assign_stmt ctxt loc e2 s.at)
      | Field ->
        let fld = (self ctxt x.at, id x) in
        !!([],
@@ -532,19 +532,19 @@ and stmt ctxt (s : M.exp) : seqn =
        self_var :: call_args ctxt args))])
   | M.RetE e ->
      !!([],
-        [ !!(assign_stmt ctxt (!!! (Source.no_region) "$Res") e);
-          !!(GotoS(!!! (Source.no_region) "$Ret"))
-        ])
+        assign_stmt ctxt (!!! (Source.no_region) "$Res") e s.at
+        @ [ !!(GotoS(!!! (Source.no_region) "$Ret")) ])
   | _ ->
      unsupported s.at (Arrange.exp s)
 
-and assign_stmt ctxt x e =
+and assign_stmt ctxt x e at =
+  let (!!) p = !!! at p in
   match e with
   | M.({it = CallE({it = VarE m; _}, inst, args); _}) ->
-    MethodCallS ([x], id m,
-      let self_var = self ctxt m.at in
-      self_var :: call_args ctxt args)
-  | _ -> VarAssignS(x, exp ctxt e)
+     [ !!(MethodCallS ([x], id m,
+                       let self_var = self ctxt m.at in
+                       self_var :: call_args ctxt args))]
+  | _ -> [!! (VarAssignS(x, exp ctxt e))]
 
 and call_args ctxt e =
   match e with