diff --git a/src/lib_utils/PP.ml b/src/lib_utils/PP.ml
index 87eb5e87b..1665d4a57 100644
--- a/src/lib_utils/PP.ml
+++ b/src/lib_utils/PP.ml
@@ -9,6 +9,7 @@ let rec new_lines n ppf () =
 let const const : formatter -> unit -> unit = fun ppf () -> fprintf ppf "%s" const
 let comment : formatter -> string -> unit = fun ppf s -> fprintf ppf "(* %s *)" s
 let list_sep value separator = pp_print_list ~pp_sep:separator value
+let list value = pp_print_list ~pp_sep:(tag "") value
 let ne_list_sep value separator ppf (hd, tl) =
   value ppf hd ;
   separator ppf () ;
@@ -24,3 +25,19 @@ let smap_sep value sep ppf m =
   let new_pp ppf (k, v) = fprintf ppf "%s -> %a" k value v in
   let lst = List.rev @@ SMap.fold aux m [] in
   fprintf ppf "%a" (list_sep new_pp sep) lst
+
+(* TODO: remove all uses. this is bad. *)
+let printer : ('a -> unit) -> _ -> 'a -> unit = fun f ppf x ->
+  let oldstdout = Unix.dup Unix.stdout in
+  let name = "/tmp/wtf-" ^ (string_of_int @@ Random.bits ()) in
+  let newstdout = open_out name in
+  Unix.dup2 (Unix.descr_of_out_channel newstdout) Unix.stdout;
+  f x;
+  flush stdout;
+  Unix.dup2 oldstdout Unix.stdout;
+  let ic = open_in name in
+  let n = in_channel_length ic in
+  let s = Bytes.create n in
+  really_input ic s 0 n;
+  close_in ic;
+  fprintf ppf "%s" (Bytes.to_string s)
diff --git a/src/lib_utils/x_list.ml b/src/lib_utils/x_list.ml
index e79d2a783..ca76bcc32 100644
--- a/src/lib_utils/x_list.ml
+++ b/src/lib_utils/x_list.ml
@@ -70,6 +70,18 @@ let until n lst =
   in
   rev (aux [] n lst)
 
+let uncons_opt = function
+  | [] -> None
+  | hd :: tl -> Some (hd, tl)
+
+let rev_uncons_opt = function
+  | [] -> None
+  | lst ->
+      let r = rev lst in
+      let last = hd r in
+      let hds = rev @@ tl r in
+      Some (hds, last)
+
 module Ne = struct
 
   type 'a t = 'a * 'a list
diff --git a/src/lib_utils/x_tezos_micheline.ml b/src/lib_utils/x_tezos_micheline.ml
index 468306784..1cfea900f 100644
--- a/src/lib_utils/x_tezos_micheline.ml
+++ b/src/lib_utils/x_tezos_micheline.ml
@@ -37,6 +37,8 @@ module Michelson = struct
   let i_piar = seq [ i_swap ; i_pair ]
   let i_push ty code = prim ~children:[ty;code] I_PUSH
   let i_push_unit = i_push t_unit d_unit
+  let i_none ty = prim ~children:[ty] I_NONE
+  let i_some = prim I_SOME
   let i_lambda arg ret body = prim ~children:[arg;ret;body] I_LAMBDA
   let i_drop = prim I_DROP
 
diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml
index 59f910963..428d74295 100644
--- a/src/ligo/ast_simplified.ml
+++ b/src/ligo/ast_simplified.ml
@@ -230,9 +230,27 @@ module Rename = struct
 
     let rec rename_instruction (r:renamings) (i:instruction) : instruction result =
       match i with
-      | I_assignment ({name;annotated_expression = e} as a) ->
-          let%bind annotated_expression = rename_annotated_expression (filter r name) e in
-          ok (I_assignment {a with annotated_expression})
+      | I_assignment ({name;annotated_expression = e} as a) -> (
+          match List.assoc_opt name r with
+          | None ->
+              let%bind annotated_expression = rename_annotated_expression (filter r name) e in
+              ok (I_assignment {a with annotated_expression})
+          | Some (name', lst) -> (
+              let%bind annotated_expression = rename_annotated_expression r e in
+              match lst with
+              | [] -> ok (I_assignment {name = name' ; annotated_expression})
+              | lst ->
+                  let (hds, tl) =
+                    let open List in
+                    let r = rev lst in
+                    rev @@ tl r, hd r
+                  in
+                  let%bind tl' = match tl with
+                    | Access_record n -> ok n
+                    | Access_tuple _ -> simple_fail "no support for renaming into tuples yet" in
+                  ok (I_record_patch (name', hds, [tl', annotated_expression]))
+            )
+        )
       | I_skip -> ok I_skip
       | I_fail e ->
           let%bind e' = rename_annotated_expression r e in
@@ -254,8 +272,8 @@ module Rename = struct
           | None -> (
               ok (I_record_patch (v, path, lst'))
             )
-          | Some (v, path') -> (
-              ok (I_record_patch (v, path' @ path, lst'))
+          | Some (v', path') -> (
+              ok (I_record_patch (v', path' @ path, lst'))
             )
     and rename_block (r:renamings) (bl:block) : block result =
       bind_map_list (rename_instruction r) bl
diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml
index 85af2fd29..d91e023ec 100644
--- a/src/ligo/ast_typed.ml
+++ b/src/ligo/ast_typed.ml
@@ -37,10 +37,15 @@ and type_value' =
   | T_function of tv * tv
 
 and type_value = {
-  type_value : type_value' ;
+  type_value' : type_value' ;
   simplified : S.type_expression option ;
 }
 
+and named_type_value = {
+  type_name: name ;
+  type_value : type_value ;
+}
+
 and lambda = {
   binder: name ;
   input_type: tv ;
@@ -89,6 +94,11 @@ and instruction =
   | I_loop of ae * b
   | I_skip
   | I_fail of ae
+  | I_patch of named_type_value * access_path * ae
+
+and access = Ast_simplified.access
+
+and access_path = Ast_simplified.access_path
 
 and 'a matching =
   | Match_bool of {
@@ -112,7 +122,7 @@ and matching_expr = ae matching
 open! Trace
 
 
-let type_value type_value simplified = { type_value ; simplified }
+let type_value type_value' simplified = { type_value' ; simplified }
 let annotated_expression expression type_annotation = { expression ; type_annotation }
 let get_type_annotation x = x.type_annotation
 
@@ -151,7 +161,7 @@ module PP = struct
     | T_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n
 
   and type_value ppf (tv:type_value) : unit =
-    type_value' ppf tv.type_value
+    type_value' ppf tv.type_value'
 
   let rec annotated_expression ppf (ae:annotated_expression) : unit =
     match ae.type_annotation.simplified with
@@ -205,6 +215,10 @@ module PP = struct
     | Match_option {match_none ; match_some = (some, match_some)} ->
         fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none (fst some) f match_some
 
+  and pre_access ppf (a:access) = match a with
+    | Access_record n -> fprintf ppf ".%s" n
+    | Access_tuple i -> fprintf ppf ".%d" i
+
   and instruction ppf (i:instruction) = match i with
     | I_skip -> fprintf ppf "skip"
     | I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
@@ -213,6 +227,10 @@ module PP = struct
         fprintf ppf "%s := %a" name annotated_expression ae
     | I_matching (ae, m) ->
         fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
+    | I_patch (s, p, e) ->
+        fprintf ppf "%s%a := %a"
+          s.type_name (fun ppf -> List.iter (pre_access ppf)) p
+          annotated_expression e
 
   let declaration ppf (d:declaration) =
     match d with
@@ -252,7 +270,7 @@ module Errors = struct
 end
 open Errors
 
-let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value, b.type_value) with
+let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with
   | T_tuple ta, T_tuple tb -> (
       let%bind _ =
         trace_strong (different_size_tuples a b)
@@ -450,36 +468,36 @@ module Combinators = struct
 
   let get_annotation (x:annotated_expression) = x.type_annotation
 
-  let get_t_bool (t:type_value) : unit result = match t.type_value with
+  let get_t_bool (t:type_value) : unit result = match t.type_value' with
     | T_constant ("bool", []) -> ok ()
     | _ -> simple_fail "not a bool"
 
-  let get_t_option (t:type_value) : type_value result = match t.type_value with
+  let get_t_option (t:type_value) : type_value result = match t.type_value' with
     | T_constant ("option", [o]) -> ok o
     | _ -> simple_fail "not a option"
 
-  let get_t_list (t:type_value) : type_value result = match t.type_value with
+  let get_t_list (t:type_value) : type_value result = match t.type_value' with
     | T_constant ("list", [o]) -> ok o
     | _ -> simple_fail "not a list"
 
-  let get_t_tuple (t:type_value) : type_value list result = match t.type_value with
+  let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
     | T_tuple lst -> ok lst
     | _ -> simple_fail "not a tuple"
 
-  let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value with
+  let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value' with
     | T_sum m -> ok m
     | _ -> simple_fail "not a sum"
 
-  let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value with
+  let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value' with
     | T_record m -> ok m
     | _ -> simple_fail "not a record"
 
   let get_t_map (t:type_value) : (type_value * type_value) result =
-    match t.type_value with
+    match t.type_value' with
     | T_constant ("map", [k;v]) -> ok (k, v)
     | _ -> simple_fail "not a map"
   let assert_t_map (t:type_value) : unit result =
-    match t.type_value with
+    match t.type_value' with
     | T_constant ("map", [_ ; _]) -> ok ()
     | _ -> simple_fail "not a map"
 
diff --git a/src/ligo/contracts/heap.ligo b/src/ligo/contracts/heap.ligo
index 143b7ed4d..82c1045ff 100644
--- a/src/ligo/contracts/heap.ligo
+++ b/src/ligo/contracts/heap.ligo
@@ -5,3 +5,10 @@ function is_empty (const h : heap) : bool is
 
 function get_top (const h : heap) : heap_element is
   block {skip} with get_force(0, h)
+
+function pop (const h : heap) : heap_element is
+  block {
+   const result : heap_element := get_top (h) ;
+   const s : nat = size(h) ;
+   
+  } with result ;
diff --git a/src/ligo/contracts/map.ligo b/src/ligo/contracts/map.ligo
index 1248c6c0c..f99ddea57 100644
--- a/src/ligo/contracts/map.ligo
+++ b/src/ligo/contracts/map.ligo
@@ -1,15 +1,24 @@
 type foobar is map(int, int)
 
-function size_ (const m : foobar) : nat is
-  block {skip} with (size(m))
-
-function gf (const m : foobar) : int is begin skip end with get_force(23, m)
-
 const fb : foobar = map
   23 -> 0 ;
   42 -> 0 ;
 end
 
+function set_ (var n : int ; var m : foobar) : foobar is block {
+  m[n] := n ;
+} with m
+
+
+function rm (var m : foobar) : foobar is block {
+  remove 42 from map m
+} with m
+
+function size_ (const m : foobar) : nat is
+  block {skip} with (size(m))
+
+function gf (const m : foobar) : int is begin skip end with get_force(23, m)
+
 function get (const m : foobar) : option(int) is
   begin
     skip
@@ -22,4 +31,3 @@ const bm : foobar = map
   120 -> 23 ;
   421 -> 23 ;
 end
-
diff --git a/src/ligo/ligo_parser/AST.mli b/src/ligo/ligo_parser/AST.mli
index 39a0f08b3..46905ddde 100644
--- a/src/ligo/ligo_parser/AST.mli
+++ b/src/ligo/ligo_parser/AST.mli
@@ -663,3 +663,4 @@ val selection_to_region  : selection -> Region.t
 (* Printing *)
 
 val print_tokens : t -> unit
+val print_path : path -> unit
diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml
index 432ba604a..381bc113c 100644
--- a/src/ligo/mini_c.ml
+++ b/src/ligo/mini_c.ml
@@ -77,6 +77,7 @@ and assignment = var_name * expression
 and statement' =
   | Assignment of assignment
   | I_Cond of expression * block * block
+  | I_patch of string * [`Left | `Right] list * expression
   | If_None of expression * block * (var_name * block)
   | While of expression * block
 
@@ -195,6 +196,9 @@ module PP = struct
   and statement ppf ((s, _) : statement) = match s with
     | Assignment ass -> assignment ppf ass
     | I_Cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
+    | I_patch (r, path, e) ->
+        let aux = fun ppf -> function `Left -> fprintf ppf ".L" | `Right -> fprintf ppf ".R" in
+        fprintf ppf "%s%a := %a" r (list aux) path expression e
     | If_None (expr, none, (name, some)) -> fprintf ppf "if (%a) %a %s.%a" expression expr block none name block some
     | While (e, b) -> fprintf ppf "while (%a) %a" expression e block b
 
@@ -207,6 +211,7 @@ module PP = struct
     fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p
 end
 
+
 module Translate_type = struct
   module O = Tezos_utils.Micheline.Michelson
 
@@ -623,6 +628,134 @@ module Environment = struct
     ok @@ seq [ i_comment "set" ; code ]
 end
 
+module Combinators = struct
+
+  let get_bool (v:value) = match v with
+    | D_bool b -> ok b
+    | _ -> simple_fail "not a bool"
+
+  let get_int (v:value) = match v with
+    | D_int n -> ok n
+    | _ -> simple_fail "not an int"
+
+  let get_nat (v:value) = match v with
+    | D_nat n -> ok n
+    | _ -> simple_fail "not a nat"
+
+  let get_string (v:value) = match v with
+    | D_string s -> ok s
+    | _ -> simple_fail "not a string"
+
+  let get_bytes (v:value) = match v with
+    | D_bytes b -> ok b
+    | _ -> simple_fail "not a bytes"
+
+  let get_unit (v:value) = match v with
+    | D_unit -> ok ()
+    | _ -> simple_fail "not a unit"
+
+  let get_option (v:value) = match v with
+    | D_none -> ok None
+    | D_some s -> ok (Some s)
+    | _ -> simple_fail "not an option"
+
+  let get_map (v:value) = match v with
+    | D_map lst -> ok lst
+    | _ -> simple_fail "not a map"
+
+  let get_t_option (v:type_value) = match v with
+    | T_option t -> ok t
+    | _ -> simple_fail "not an option"
+
+  let get_pair (v:value) = match v with
+    | D_pair (a, b) -> ok (a, b)
+    | _ -> simple_fail "not a pair"
+
+  let get_t_pair (t:type_value) = match t with
+    | T_pair (a, b) -> ok (a, b)
+    | _ -> simple_fail "not a type pair"
+
+  let get_t_map (t:type_value) = match t with
+    | T_map kv -> ok kv
+    | _ -> simple_fail "not a type map"
+
+  let get_left (v:value) = match v with
+    | D_left b -> ok b
+    | _ -> simple_fail "not a left"
+
+  let get_right (v:value) = match v with
+    | D_right b -> ok b
+    | _ -> simple_fail "not a right"
+
+  let get_or (v:value) = match v with
+    | D_left b -> ok (false, b)
+    | D_right b -> ok (true, b)
+    | _ -> simple_fail "not a left/right"
+
+  let get_last_statement ((b', _):block) : statement result =
+    let aux lst = match lst with
+      | [] -> simple_fail "get_last: empty list"
+      | lst -> ok List.(nth lst (length lst - 1)) in
+    aux b'
+
+  let t_int : type_value = T_base Base_int
+  let t_nat : type_value = T_base Base_nat
+
+  let quote binder input output body result : anon_function =
+    let content : anon_function_content = {
+      binder ; input ; output ;
+      body ; result ; capture_type = No_capture ;
+    } in
+    { content ; capture = None }
+
+  let basic_quote i o b : anon_function result =
+    let%bind (_, e) = get_last_statement b in
+    let r : expression = (E_variable "output", o, e.post_environment) in
+    ok @@ quote "input" i o b r
+
+  let basic_int_quote b : anon_function result =
+    basic_quote t_int t_int b
+
+  let basic_int_quote_env : environment =
+    let e = Environment.empty in
+    Environment.add ("input", t_int) e
+
+  let e_int expr env : expression = (expr, t_int, env)
+  let e_var_int name env : expression = e_int (E_variable name) env
+
+  let d_unit : value = D_unit
+
+  let environment_wrap pre_environment post_environment = { pre_environment ; post_environment }
+  let id_environment_wrap e = environment_wrap e e
+
+  let statement s' e : statement =
+    match s' with
+    | I_Cond _ -> s', id_environment_wrap e
+    | If_None _ -> s', id_environment_wrap e
+    | While _ -> s', id_environment_wrap e
+    | I_patch _ -> s', id_environment_wrap e
+    | Assignment (name, (_, t, _)) -> s', environment_wrap e (Environment.add (name, t) e)
+
+  let block (statements:statement list) : block result =
+    match statements with
+    | [] -> simple_fail "no statements in block"
+    | lst ->
+        let first = List.hd lst in
+        let last = List.(nth lst (length lst - 1)) in
+        ok (lst, environment_wrap (snd first).pre_environment (snd last).post_environment)
+
+  let statements (lst:(environment -> statement) list) e : statement list =
+    let rec aux lst e = match lst with
+      | [] -> []
+      | hd :: tl ->
+          let s = hd e in
+          s :: aux tl (snd s).post_environment
+    in
+    aux lst e
+
+end
+
+
 module Translate_program = struct
   open Tezos_utils.Micheline.Michelson
 
@@ -648,7 +781,8 @@ module Translate_program = struct
       i_unpair ; dip i_unpair ; dip (dip i_unpair) ; i_swap ; dip i_swap ; i_swap ; c ; i_pair ;
     ])
 
-  let rec get_predicate : string -> predicate result = function
+  let rec get_predicate : string -> expression list -> predicate result = fun s lst ->
+    match s with
     | "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD
     | "ADD_NAT" -> ok @@ simple_binary @@ prim I_ADD
     | "NEG" -> ok @@ simple_unary @@ prim I_NEG
@@ -664,6 +798,16 @@ module Translate_program = struct
     | "GET_FORCE" -> ok @@ simple_binary @@ seq [prim I_GET ; i_assert_some]
     | "GET" -> ok @@ simple_binary @@ prim I_GET
     | "SIZE" -> ok @@ simple_unary @@ prim I_SIZE
+    | "MAP_REMOVE" ->
+        let%bind v = match lst with
+          | [ _ ; (_, m, _) ] ->
+              let%bind (_, v) = Combinators.get_t_map m in
+              ok v
+          | _ -> simple_fail "mini_c . MAP_REMOVE" in
+        let%bind v_ty = Translate_type.type_ v in
+        ok @@ simple_binary @@ seq [dip (i_none v_ty) ; prim I_UPDATE ]
+    | "MAP_UPDATE" ->
+        ok @@ simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]
     | x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist"
 
   and translate_value (v:value) : michelson result = match v with
@@ -765,13 +909,13 @@ module Translate_program = struct
           i_piar ;
         ]
       | E_constant(str, lst) ->
-        let%bind lst = bind_list @@ List.map translate_expression lst in
-        let%bind predicate = get_predicate str in
+        let%bind lst' = bind_list @@ List.map translate_expression lst in
+        let%bind predicate = get_predicate str lst in
         let%bind code = match (predicate, List.length lst) with
-          | Constant c, 0 -> ok (seq @@ lst @ [c])
-          | Unary f, 1 -> ok (seq @@ lst @ [f])
-          | Binary f, 2 -> ok (seq @@ lst @ [f])
-          | Ternary f, 3 -> ok (seq @@ lst @ [f])
+          | Constant c, 0 -> ok (seq @@ lst' @ [c])
+          | Unary f, 1 -> ok (seq @@ lst' @ [f])
+          | Binary f, 2 -> ok (seq @@ lst' @ [f])
+          | Ternary f, 3 -> ok (seq @@ lst' @ [f])
           | _ -> simple_fail "bad arity"
         in
         ok code
@@ -928,6 +1072,7 @@ module Translate_program = struct
             Environment.to_michelson_restrict ;
             i_push_unit ; expr ; i_car]] I_LOOP ;
       ])
+    | I_patch _ -> ()
     in
 
     let%bind () =
@@ -1157,130 +1302,3 @@ module Run = struct
         @@ Format.asprintf "%a" PP.expression e
 
 end
-
-
-module Combinators = struct
-
-  let get_bool (v:value) = match v with
-    | D_bool b -> ok b
-    | _ -> simple_fail "not a bool"
-
-  let get_int (v:value) = match v with
-    | D_int n -> ok n
-    | _ -> simple_fail "not an int"
-
-  let get_nat (v:value) = match v with
-    | D_nat n -> ok n
-    | _ -> simple_fail "not a nat"
-
-  let get_string (v:value) = match v with
-    | D_string s -> ok s
-    | _ -> simple_fail "not a string"
-
-  let get_bytes (v:value) = match v with
-    | D_bytes b -> ok b
-    | _ -> simple_fail "not a bytes"
-
-  let get_unit (v:value) = match v with
-    | D_unit -> ok ()
-    | _ -> simple_fail "not a unit"
-
-  let get_option (v:value) = match v with
-    | D_none -> ok None
-    | D_some s -> ok (Some s)
-    | _ -> simple_fail "not an option"
-
-  let get_map (v:value) = match v with
-    | D_map lst -> ok lst
-    | _ -> simple_fail "not a map"
-
-  let get_t_option (v:type_value) = match v with
-    | T_option t -> ok t
-    | _ -> simple_fail "not an option"
-
-  let get_pair (v:value) = match v with
-    | D_pair (a, b) -> ok (a, b)
-    | _ -> simple_fail "not a pair"
-
-  let get_t_pair (t:type_value) = match t with
-    | T_pair (a, b) -> ok (a, b)
-    | _ -> simple_fail "not a type pair"
-
-  let get_t_map (t:type_value) = match t with
-    | T_map kv -> ok kv
-    | _ -> simple_fail "not a type map"
-
-  let get_left (v:value) = match v with
-    | D_left b -> ok b
-    | _ -> simple_fail "not a left"
-
-  let get_right (v:value) = match v with
-    | D_right b -> ok b
-    | _ -> simple_fail "not a right"
-
-  let get_or (v:value) = match v with
-    | D_left b -> ok (false, b)
-    | D_right b -> ok (true, b)
-    | _ -> simple_fail "not a left/right"
-
-  let get_last_statement ((b', _):block) : statement result =
-    let aux lst = match lst with
-      | [] -> simple_fail "get_last: empty list"
-      | lst -> ok List.(nth lst (length lst - 1)) in
-    aux b'
-
-  let t_int : type_value = T_base Base_int
-  let t_nat : type_value = T_base Base_nat
-
-  let quote binder input output body result : anon_function =
-    let content : anon_function_content = {
-      binder ; input ; output ;
-      body ; result ; capture_type = No_capture ;
-    } in
-    { content ; capture = None }
-
-  let basic_quote i o b : anon_function result =
-    let%bind (_, e) = get_last_statement b in
-    let r : expression = (E_variable "output", o, e.post_environment) in
-    ok @@ quote "input" i o b r
-
-  let basic_int_quote b : anon_function result =
-    basic_quote t_int t_int b
-
-  let basic_int_quote_env : environment =
-    let e = Environment.empty in
-    Environment.add ("input", t_int) e
-
-  let e_int expr env : expression = (expr, t_int, env)
-  let e_var_int name env : expression = e_int (E_variable name) env
-
-  let d_unit : value = D_unit
-
-  let environment_wrap pre_environment post_environment = { pre_environment ; post_environment }
-  let id_environment_wrap e = environment_wrap e e
-
-  let statement s' e : statement =
-    match s' with
-    | I_Cond _ -> s', id_environment_wrap e
-    | If_None _ -> s', id_environment_wrap e
-    | While _ -> s', id_environment_wrap e
-    | Assignment (name, (_, t, _)) -> s', environment_wrap e (Environment.add (name, t) e)
-
-  let block (statements:statement list) : block result =
-    match statements with
-    | [] -> simple_fail "no statements in block"
-    | lst ->
-        let first = List.hd lst in
-        let last = List.(nth lst (length lst - 1)) in
-        ok (lst, environment_wrap (snd first).pre_environment (snd last).post_environment)
-
-  let statements (lst:(environment -> statement) list) e : statement list =
-    let rec aux lst e = match lst with
-      | [] -> []
-      | hd :: tl ->
-          let s = hd e in
-          s :: aux tl (snd s).post_environment
-    in
-    aux lst e
-
-end
diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml
index c11d95f43..3d2865ef3 100644
--- a/src/ligo/simplify.ml
+++ b/src/ligo/simplify.ml
@@ -387,17 +387,31 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
         | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i]
         | ClauseBlock b -> simpl_statements @@ fst b.value.inside in
       ok @@ I_matching (expr, (Match_bool {match_true; match_false}))
-  | Assign a ->
+  | Assign a -> (
       let a = a.value in
-      let%bind name = match a.lhs with
-        | Path (Name v) -> ok v.value
-        | _ -> simple_fail "no complex assignments yet"
-      in
-      let%bind annotated_expression = match a.rhs with
+      let%bind value_expr = match a.rhs with
         | Expr e -> simpl_expression e
         | _ -> simple_fail "no weird assignments yet"
       in
-      ok @@ I_assignment {name ; annotated_expression}
+      match a.lhs with
+        | Path (Name name) -> (
+            ok @@ I_assignment {name = name.value ; annotated_expression = value_expr}
+          )
+        | Path path -> (
+            let err_content = Format.asprintf "%a" (Tezos_utils.PP.printer Raw.print_path) path in
+            fail @@ error "no path assignments" err_content
+          )
+        | MapPath v -> (
+            let v' = v.value in
+            let%bind name = match v'.path with
+              | Name name -> ok name
+              | _ -> simple_fail "no complex map assignments yet" in
+            let%bind key_expr = simpl_expression v'.index.value.inside in
+            let old_expr = ae @@ E_variable name.value in
+            let expr' = ae @@ E_constant ("MAP_UPDATE", [key_expr ; value_expr ; old_expr]) in
+            ok @@ I_assignment {name = name.value ; annotated_expression = expr'}
+          )
+    )
   | CaseInstr c ->
       let c = c.value in
       let%bind expr = simpl_expression c.expr in
@@ -410,20 +424,32 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
         @@ npseq_to_list c.cases.value in
       let%bind m = simpl_cases cases in
       ok @@ I_matching (expr, m)
-  | RecordPatch r ->
+  | RecordPatch r -> (
       let r = r.value in
       let%bind record = match r.path with
         | Name v -> ok v.value
-        | _ -> simple_fail "no complex assignments yet"
+        | path -> (
+            let err_content = Format.asprintf "%a" (Tezos_utils.PP.printer Raw.print_path) path in
+            fail @@ error "no complex record patch yet" err_content
+          )
       in
       let%bind inj = bind_list
         @@ List.map (fun (x:Raw.field_assign) -> let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e))
         @@ List.map (fun (x:_ Raw.reg) -> x.value)
         @@ npseq_to_list r.record_inj.value.fields in
       ok @@ I_record_patch (record, [], inj)
+    )
   | MapPatch _ -> simple_fail "no map patch yet"
   | SetPatch _ -> simple_fail "no set patch yet"
-  | MapRemove _ -> simple_fail "no map remove yet"
+  | MapRemove r ->
+      let v = r.value in
+      let key = v.key in
+      let%bind map = match v.map with
+        | Name v -> ok v.value
+        | _ -> simple_fail "no complex map remove yet" in
+      let%bind key' = simpl_expression key in
+      let expr = E_constant ("MAP_REMOVE", [key' ; ae (E_variable map)]) in
+      ok @@ I_assignment {name = map ; annotated_expression = ae expr}
   | SetRemove _ -> simple_fail "no set remove yet"
 
 and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t ->
diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml
index fc26c76c5..78a93a879 100644
--- a/src/ligo/test/integration_tests.ml
+++ b/src/ligo/test/integration_tests.ml
@@ -207,6 +207,15 @@ let map () : unit result =
     let expect = ez [(23, 0) ; (42, 0)] in
     AST_Typed.assert_value_eq (expect, result)
   in
+  let%bind _set = trace (simple_error "set") @@
+    let aux n =
+      let input = ez List.(map (fun x -> (x, x)) @@ range n) in
+      let%bind result = easy_run_typed "set_" program input in
+      let expect = ez [(23, n) ; (42, 0)] in
+      AST_Typed.assert_value_eq (expect, result)
+    in
+    bind_map_list aux [1 ; 10 ; 3]
+  in
   let%bind _get = trace (simple_error "get") @@
     let aux n =
       let input = ez [(23, n) ; (42, 4)] in
@@ -221,6 +230,12 @@ let map () : unit result =
     let expect = ez @@ List.map (fun x -> (x, 23)) [144 ; 51 ; 42 ; 120 ; 421] in
     AST_Typed.assert_value_eq (expect, result)
   in
+  let%bind _remove = trace (simple_error "rm") @@
+    let input = ez [(23, 23) ; (42, 42)] in
+    let%bind result = easy_run_typed "rm" program input in
+    let expect = ez [23, 23] in
+    AST_Typed.assert_value_eq (expect, result)
+  in
   ok ()
 
 let condition () : unit result =
diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml
index 535a2e0e6..a0d28deb3 100644
--- a/src/ligo/transpiler.ml
+++ b/src/ligo/transpiler.ml
@@ -78,6 +78,13 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
         | true -> env
         | false -> Environment.add (name, t) env in
       return ~env' (Assignment (name, expression))
+  | I_patch (r, s, v) ->
+      let ty = Environment.get r in
+      let aux (prev, acc) cur = ()
+      in
+      let s' = List.fold_left aux (ty, []) s in
+      let v' = translate_annotated_expression env v in
+      return (I_patch (r, s', v'))
   | I_matching (expr, m) -> (
       let%bind expr' = translate_annotated_expression env expr in
       let env' = Environment.extend env in
diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml
index 16d549496..af30fa8e9 100644
--- a/src/ligo/typer.ml
+++ b/src/ligo/typer.ml
@@ -24,7 +24,7 @@ module Environment = struct
   let get_constructor (e:t) (s:string) : (ele * ele) option =
     let rec aux = function
       | [] -> None
-      | (_, (O.{type_value=(O.T_sum m)} as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv)
+      | (_, (O.{type_value'=(O.T_sum m)} as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv)
       | _ :: tl -> aux tl
     in
     aux e.environment
@@ -124,7 +124,7 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
 and type_block_full (e:environment) (b:I.block) : (O.block * environment) result =
   let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) =
     let%bind (e', i') = type_instruction e i in
-    ok (e', i' :: acc)
+    ok (e', i' @ acc)
   in
   let%bind (e', lst) = bind_fold_list aux (e, []) b in
   ok @@ (List.rev lst, e')
@@ -133,42 +133,67 @@ and type_block (e:environment) (b:I.block) : O.block result =
   let%bind (block, _) = type_block_full e b in
   ok block
 
-and type_instruction (e:environment) : I.instruction -> (environment * O.instruction) result = function
-  | I_skip -> ok (e, O.I_skip)
+and type_instruction (e:environment) : I.instruction -> (environment * O.instruction list) result = fun i ->
+  let return x = ok (e, [x]) in
+  match i with
+  | I_skip -> return O.I_skip
   | I_fail x ->
       let%bind expression = type_annotated_expression e x in
-      ok (e, O.I_fail expression)
+      return @@ O.I_fail expression
   | I_loop (cond, body) ->
       let%bind cond = type_annotated_expression e cond in
       let%bind _ =
         O.assert_type_value_eq (cond.type_annotation, t_bool ()) in
       let%bind body = type_block e body in
-      ok (e, O.I_loop (cond, body))
+      return @@ O.I_loop (cond, body)
   | I_assignment {name;annotated_expression} -> (
       match annotated_expression.type_annotation, Environment.get e name with
       | None, None -> simple_fail "Initial assignments need type"
       | Some _, None ->
           let%bind annotated_expression = type_annotated_expression e annotated_expression in
           let e' = Environment.add e name annotated_expression.type_annotation in
-          ok (e', O.I_assignment {name;annotated_expression})
+          ok (e', [O.I_assignment {name;annotated_expression}])
       | None, Some prev ->
           let%bind annotated_expression = type_annotated_expression e annotated_expression in
           let e' = Environment.add e name annotated_expression.type_annotation in
           let%bind _ =
             O.assert_type_value_eq (annotated_expression.type_annotation, prev) in
-          ok (e', O.I_assignment {name;annotated_expression})
+          ok (e', [O.I_assignment {name;annotated_expression}])
       | Some _, Some prev ->
           let%bind annotated_expression = type_annotated_expression e annotated_expression in
           let%bind _assert = trace (simple_error "Annotation doesn't match environment")
             @@ O.assert_type_value_eq (annotated_expression.type_annotation, prev) in
           let e' = Environment.add e name annotated_expression.type_annotation in
-          ok (e', O.I_assignment {name;annotated_expression})
+          ok (e', [O.I_assignment {name;annotated_expression}])
     )
   | I_matching (ex, m) ->
       let%bind ex' = type_annotated_expression e ex in
       let%bind m' = type_match type_block e ex'.type_annotation m in
-      ok (e, O.I_matching (ex', m'))
-  | I_record_patch _ -> simple_fail "no record_patch yet"
+      return @@ O.I_matching (ex', m')
+  | I_record_patch (r, path, lst) ->
+      let aux (s, ae) =
+        let%bind ae' = type_annotated_expression e ae in
+        let%bind ty =
+          trace_option (simple_error "unbound variable in record_patch") @@
+          Environment.get e r in
+        let tv = O.{type_name = r ; type_value = ty} in
+        let aux ty access =
+          match access with
+          | I.Access_record s ->
+              let%bind m = O.Combinators.get_t_record ty in
+              trace_option (simple_error "unbound record access in record_patch") @@
+              Map.String.find_opt s m
+          | Access_tuple i ->
+              let%bind t = O.Combinators.get_t_tuple ty in
+              generic_try (simple_error "unbound tuple access in record_patch") @@
+              (fun () -> List.nth t i)
+        in
+        let%bind _assert = bind_fold_list aux ty (path @ [Access_record s]) in
+        ok @@ O.I_patch (tv, path @ [Access_record s], ae')
+      in
+      let%bind lst' = bind_map_list aux lst in
+      ok (e, lst')
+
 
 and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> o O.matching result =
   fun f e t i -> match i with
@@ -375,7 +400,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
   | E_application (f, arg) ->
       let%bind f = type_annotated_expression e f in
       let%bind arg = type_annotated_expression e arg in
-      let%bind type_annotation = match f.type_annotation.type_value with
+      let%bind type_annotation = match f.type_annotation.type_value' with
         | T_function (param, result) ->
             let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
             ok result
@@ -428,6 +453,17 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
   | "NONE", _ -> simple_fail "bad number of params to NONE"
   | "SOME", [s] -> ok ("SOME", t_option s ())
   | "SOME", _ -> simple_fail "bad number of params to SOME"
+  | "MAP_REMOVE", [k ; m] ->
+      let%bind (src, _) = get_t_map m in
+      let%bind () = O.assert_type_value_eq (src, k) in
+      ok ("MAP_REMOVE", m)
+  | "MAP_REMOVE", _ -> simple_fail "bad number of params to MAP_REMOVE"
+  | "MAP_UPDATE", [k ; v ; m] ->
+      let%bind (src, dst) = get_t_map m in
+      let%bind () = O.assert_type_value_eq (src, k) in
+      let%bind () = O.assert_type_value_eq (dst, v) in
+      ok ("MAP_UPDATE", m)
+  | "MAP_UPDATE", _ -> simple_fail "bad number of params to MAP_UPDATE"
   | "get_force", [i_ty;m_ty] ->
       let%bind (src, dst) = get_t_map m_ty in
       let%bind _ = O.assert_type_value_eq (src, i_ty) in
@@ -527,6 +563,15 @@ and untype_instruction (i:O.instruction) : (I.instruction) result =
       let%bind e' = untype_annotated_expression e in
       let%bind m' = untype_matching untype_block m in
       ok @@ I_matching (e', m')
+  | I_patch (s, p, e) ->
+      let%bind e' = untype_annotated_expression e in
+      let%bind (hds, tl) =
+        trace_option (simple_error "patch without path") @@
+        List.rev_uncons_opt p in
+      let%bind tl_name = match tl with
+        | Access_record n -> ok n
+        | Access_tuple _ -> simple_fail "last element of patch is tuple" in
+      ok @@ I_record_patch (s.type_name, hds, [tl_name, e'])
 
 and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
   let open I in