Merge branch 'dev' of gitlab.com:ligolang/ligo into feature/doc-pascaligo-loop

gitlab-pages/docs/api/cheat-sheet.md

@@ -4,6 +4,9 @@ title: Cheat Sheet
 ---
 <div class="cheatsheet">
 
+<!-- 
+Note that this table is not compiled before production and currently needs to be managed manually.
+-->
 
 <!--DOCUSAURUS_CODE_TABS-->
 <!--PascaLIGO-->
@@ -67,11 +70,42 @@ title: Cheat Sheet
 |Variants|<pre><code>type action =<br/>&#124; Increment of int<br/>&#124; Decrement of int</code></pre>|
 |Variant *(pattern)* matching|<pre><code>let a: action = Increment 5<br/>match a with<br/>&#124; Increment n -> n + 1<br/>&#124; Decrement n -> n - 1<br/></code></pre>|
 |Records|<pre><code>type person = {<br/>&nbsp;&nbsp;age: int ;<br/>&nbsp;&nbsp;name: string ;<br/>}<br/><br/>let john : person = {<br/>&nbsp;&nbsp;age = 18;<br/>&nbsp;&nbsp;name = "John Doe";<br/>}<br/><br/>let name: string = john.name</code></pre>|
-|Maps|<pre><code>type prices = (nat, tez) map<br/><br/>let prices : prices = Map.literal [<br/>&nbsp;&nbsp;(10n, 60mutez);<br/>&nbsp;&nbsp;(50n, 30mutez);<br/>&nbsp;&nbsp;(100n, 10mutez)<br/>]<br/><br/>let price: tez option = Map.find 50n prices<br/><br/>let prices: prices = Map.update 200n 5mutez prices</code></pre>|
+|Maps|<pre><code>type prices = (nat, tez) map<br/><br/>let prices : prices = Map.literal [<br/>&nbsp;&nbsp;(10n, 60mutez);<br/>&nbsp;&nbsp;(50n, 30mutez);<br/>&nbsp;&nbsp;(100n, 10mutez)<br/>]<br/><br/>let price: tez option = Map.find_opt 50n prices<br/><br/>let prices: prices = Map.update 200n (Some 5mutez) prices</code></pre>|
 |Contracts & Accounts|<pre><code>let destination_address : address = "tz1..."<br/>let contract : unit contract = <br/> Operation.get_contract destination_address</code></pre>|
-|Transactions|<pre><code>let payment : operation = <br/> Operation.transaction (unit, receiver, amount)</code></pre>|
+|Transactions|<pre><code>let payment : operation = <br/> Operation.transaction unit amount receiver</code></pre>|
 |Exception/Failure|`failwith("Your descriptive error message for the user goes here.")`|
 
+<!--ReasonLIGO-->
+
+|Primitive   	|Example|
+|---	|---|
+|Strings | `"Tezos"`|
+|Characters | `"t"`|
+|Integers | `42`, `7`|
+|Natural numbers | `42n`, `7n`|
+|Unit| `unit`|
+|Boolean|<pre><code>let has_drivers_license: bool = false;<br/>let adult: bool = true;</code></pre> |
+|Boolean Logic|<pre><code>(not true) = false = (false && true) = (false &#124;&#124; false)</code></pre>|
+|Mutez (micro tez)| `42mutez`, `7mutez` |
+|Address | `("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx": address)`, `("KT1JepfBfMSqkQyf9B1ndvURghGsSB8YCLMD": address)`|
+|Addition |`3 + 4`, `3n + 4n`|
+|Multiplication & Division| `3 * 4`, `3n * 4n`, `10 / 5`, `10n / 5n`|
+|Modulo| `10 mod 3`|
+|Tuples| <pre><code>type name = (string, string);<br/>let winner: name = ("John", "Doe");<br/>let first_name: string = winner[0];<br/>let last_name: string = winner[1];</code></pre>|
+|Types|`type age = int;`, `type name = string;`  |
+|Includes|```#include "library.mligo"```|
+|Functions |<pre><code>let add = (a: int, b: int) : int => a + b; </code></pre>|
+| If Statement | <pre><code>let new_id: int = if (age < 16) {<br/>  failwith("Too young to drive."); <br/> } else { prev_id + 1; }</code></pre>|
+|Options|<pre><code>type middle_name = option(string);<br/>let middle_name : middle_name = Some("Foo");<br/>let middle_name : middle_name = None;</code></pre>|
+|Variable Binding | ```let age: int = 5;```|
+|Type Annotations| ```("tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx" : address)```|
+|Variants|<pre><code>type action =<br/>&#124; Increment(int)<br/>&#124; Decrement(int);</code></pre>|
+|Variant *(pattern)* matching|<pre><code>let a: action = Increment(5);<br/>switch(a) {<br/>&#124; Increment(n) => n + 1<br/>&#124; Decrement(n) => n - 1;<br/> } <br/></code></pre>|
+|Records|<pre><code>type person = {<br/>&nbsp;&nbsp;age: int,<br/>&nbsp;&nbsp;name: string<br/>}<br/><br/>let john : person = {<br/>&nbsp;&nbsp;age: 18,<br/>&nbsp;&nbsp;name: "John Doe"<br/>};<br/><br/>let name: string = john.name;</code></pre>|
+|Maps|<pre><code>type prices = map(nat, tez);<br/><br/>let prices : prices = Map.literal([<br/>&nbsp;&nbsp;(10n, 60mutez),<br/>&nbsp;&nbsp;(50n, 30mutez),<br/>&nbsp;&nbsp;(100n, 10mutez)<br/>]);<br/><br/>let price: option(tez) = Map.find_opt(50n, prices);<br/><br/>let prices: prices = Map.update(200n, Some (5mutez), prices);</code></pre>|
+|Contracts & Accounts|<pre><code>let destination_address : address = "tz1...";<br/>let contract : contract(unit) = <br/> Operation.get_contract(destination_address);</code></pre>|
+|Transactions|<pre><code>let payment : operation = <br/> Operation.transaction (unit, amount, receiver);</code></pre>|
+|Exception/Failure|`failwith("Your descriptive error message for the user goes here.");`|
 
 
 <!--END_DOCUSAURUS_CODE_TABS-->

src/bin/expect_tests/typer_error_tests.ml

@@ -41,7 +41,7 @@ let%expect_test _ =
 
   run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_3.mligo" ; "main" ] ;
   [%expect {|
-    ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"tuple[int , string , bool]","b":"tuple[int , string]"}
+    ligo: in file "error_typer_3.mligo", line 3, characters 34-53. different number of arguments to type constructors: Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the TC_tuple type constructor, but they have 3 and 2 arguments, respectively) {"a":"(TO_tuple[int , string , bool])","b":"(TO_tuple[int , string])","op":"TC_tuple","len_a":"3","len_b":"2"}
 
 
      If you're not sure how to fix this error, you can

src/main/compile/of_mini_c.ml

@@ -9,15 +9,13 @@ let compile_contract : expression -> Compiler.compiled_expression result = fun e
   let%bind body = Compiler.Program.translate_function_body body [] input_ty in
   let expr = Self_michelson.optimize body in
   let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in
-  let open! Compiler.Program in
+  ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression)
-  ok { expr_ty ; expr }
 
 let compile_expression : expression -> Compiler.compiled_expression result = fun e ->
   let%bind expr = Compiler.Program.translate_expression e Compiler.Environment.empty in
   let expr = Self_michelson.optimize expr in
   let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in
-  let open! Compiler.Program in
+  ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression)
-  ok { expr_ty ; expr }
 
 let aggregate_and_compile = fun program form ->
   let%bind aggregated = aggregate_entry program form in

src/main/compile/of_simplified.ml

@@ -7,7 +7,8 @@ let compile (program : Ast_simplified.program) : (Ast_typed.program * Typer.Solv
 
 let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) (ae : Ast_simplified.expression)
     : (Ast_typed.value * Typer.Solver.state) result =
-  Typer.type_expression env state ae
+  let () = Typer.Solver.discard_state state in
+  Typer.type_expression_subst env state ae
 
 let apply (entry_point : string) (param : Ast_simplified.expression) : Ast_simplified.expression result =
   let name = Var.of_name entry_point in

src/main/compile/of_typed.ml

@@ -14,7 +14,7 @@ let assert_equal_contract_type : check_type -> string -> Ast_typed.program -> As
   match entry_point.type_annotation.type_value' with
   | T_arrow (args,_) -> (
       match args.type_value' with
-      | T_tuple [param_exp;storage_exp] -> (
+      | T_operator (TC_tuple [param_exp;storage_exp]) -> (
           match c with
           | Check_parameter -> assert_type_value_eq (param_exp,   param.type_annotation)
           | Check_storage   -> assert_type_value_eq (storage_exp, param.type_annotation)

src/passes/1-parser/cameligo/AST.ml

@@ -333,10 +333,15 @@ and update = {
   lbrace : lbrace;
   record : path;
   kwd_with : kwd_with;
-  updates : record reg;
+  updates : field_path_assign reg ne_injection reg;
   rbrace : rbrace;
 }
 
+and field_path_assign = {
+  field_path  : (field_name, dot) nsepseq;
+  assignment : equal;
+  field_expr : expr
+}
 and path =
   Name of variable
 | Path of projection reg

src/passes/1-parser/cameligo/Parser.mly

@@ -627,7 +627,7 @@ record_expr:
     in {region; value} }
 
 update_record:
-  "{" path "with" sep_or_term_list(field_assignment,";") "}" {
+  "{" path "with" sep_or_term_list(field_path_assignment,";") "}" {
     let region = cover $1 $5 in
     let ne_elements, terminator = $4 in
     let value = {
@@ -641,6 +641,14 @@ update_record:
       rbrace   = $5}
     in {region; value} }
 
+field_path_assignment :
+  nsepseq(field_name,".") "=" expr {
+    let region = cover (nsepseq_to_region (fun x -> x.region) $1) (expr_to_region $3) in
+    let value  = {field_path = $1;
+                  assignment = $2;
+                  field_expr = $3}
+    in {region; value}}
+
 field_assignment:
   field_name "=" expr {
     let start  = $1.region in

src/passes/1-parser/cameligo/ParserLog.ml

@@ -188,7 +188,7 @@ and print_update state {value; _} =
  print_token state lbrace "{";
  print_path   state record;
  print_token state kwd_with "with";
- print_record_expr state updates;
+ print_ne_injection state print_field_path_assign updates;
  print_token state rbrace "}"
 
 and print_path state = function
@@ -513,6 +513,12 @@ and print_field_assign state {value; _} =
   print_token state assignment "=";
   print_expr  state field_expr
 
+and print_field_path_assign state {value; _} =
+  let {field_path; assignment; field_expr} = value in
+  print_nsepseq state "." print_var field_path;
+  print_token state assignment "=";
+  print_expr  state field_expr
+
 and print_sequence state seq =
   print_injection state print_expr seq
 
@@ -905,7 +911,7 @@ and pp_projection state proj =
 
 and pp_update state update =
   pp_path state update.record;
-  pp_ne_injection pp_field_assign state update.updates.value
+  pp_ne_injection pp_field_path_assign state update.updates.value
 
 and pp_path state = function
   Name name ->
@@ -928,6 +934,12 @@ and pp_field_assign state {value; _} =
   pp_ident (state#pad 2 0) value.field_name;
   pp_expr  (state#pad 2 1) value.field_expr
 
+and pp_field_path_assign state {value; _} =
+  pp_node  state "<field path for update>";
+  let path = Utils.nsepseq_to_list value.field_path in
+  List.iter (pp_ident (state#pad 2 0)) path;
+  pp_expr  (state#pad 2 1) value.field_expr
+
 and pp_constr_expr state = function
   ENone region ->
     pp_loc_node state "ENone" region

src/passes/1-parser/pascaligo/AST.ml

@@ -577,7 +577,13 @@ and projection = {
 and update = {
   record : path;
   kwd_with : kwd_with;
-  updates : record reg;
+  updates : field_path_assign reg ne_injection reg
+}
+
+and field_path_assign = {
+  field_path  : (field_name, dot) nsepseq;
+  equal : equal;
+  field_expr : expr
 }
 
 and selection =

src/passes/1-parser/pascaligo/Parser.mly

@@ -937,7 +937,7 @@ record_expr:
    in {region; value} }
 
 update_record:
-  path "with" ne_injection("record",field_assignment){
+  path "with" ne_injection("record",field_path_assignment){
     let region = cover (path_to_region $1) $3.region in
     let value = {
       record = $1;
@@ -954,6 +954,14 @@ field_assignment:
                   field_expr = $3}
     in {region; value} }
 
+field_path_assignment:
+  nsepseq(field_name,".") "=" expr {
+    let region = cover (nsepseq_to_region (fun x -> x.region) $1) (expr_to_region $3)
+    and value  = {field_path = $1;
+                  equal      = $2;
+                  field_expr = $3}
+    in {region; value} }
+
 fun_call:
   fun_name arguments {
     let region = cover $1.region $2.region

src/passes/1-parser/pascaligo/ParserLog.ml

@@ -603,11 +603,18 @@ and print_field_assign state {value; _} =
   print_token state equal "=";
   print_expr  state field_expr
 
+and print_field_path_assign state {value; _} =
+  let {field_path; equal; field_expr} = value in
+  print_nsepseq state "field_path" print_var field_path;
+  print_token state equal "=";
+  print_expr  state field_expr
+  
 and print_update_expr state {value; _} = 
   let {record; kwd_with; updates} = value in
   print_path state record;
   print_token state kwd_with "with";
-  print_record_expr state updates
+  print_ne_injection state "updates field" print_field_path_assign updates
+
 
 and print_projection state {value; _} =
   let {struct_name; selector; field_path} = value in
@@ -1215,7 +1222,7 @@ and pp_projection state proj =
 
 and pp_update state update =
   pp_path state update.record;
-  pp_ne_injection pp_field_assign state update.updates.value
+  pp_ne_injection pp_field_path_assign state update.updates.value
 
 and pp_selection state = function
   FieldName name ->
@@ -1320,6 +1327,12 @@ and pp_field_assign state {value; _} =
   pp_ident (state#pad 2 0) value.field_name;
   pp_expr  (state#pad 2 1) value.field_expr
 
+and pp_field_path_assign state {value; _} =
+  pp_node  state "<field path for update>";
+  let path = Utils.nsepseq_to_list value.field_path in
+  List.iter (pp_ident (state#pad 2 0)) path;
+  pp_expr  (state#pad 2 1) value.field_expr
+
 and pp_map_patch state patch =
   pp_path (state#pad 2 0) patch.path;
   pp_ne_injection pp_binding state patch.map_inj.value

src/passes/1-parser/reasonligo/Parser.mly

@@ -812,7 +812,7 @@ path :
 | projection { Path $1}
 
 update_record : 
-  "{""..."path "," sep_or_term_list(field_assignment,",") "}" {
+  "{""..."path "," sep_or_term_list(field_path_assignment,",") "}" {
     let region = cover $1 $6 in
     let ne_elements, terminator = $5 in
     let value = {
@@ -873,3 +873,21 @@ field_assignment:
       assignment = $2;
       field_expr = $3}
     in {region; value} }
+
+field_path_assignment:
+  field_name {
+    let value = {
+      field_path = ($1,[]);
+      assignment = ghost;
+      field_expr = EVar $1 }
+    in {$1 with value}
+  }
+| nsepseq(field_name,".") ":" expr {
+    let start  = nsepseq_to_region (fun x -> x.region) $1 in
+    let stop   = expr_to_region $3 in
+    let region = cover start stop in
+    let value  = {
+      field_path = $1;
+      assignment = $2;
+      field_expr = $3}
+    in {region; value} }

src/passes/2-simplify/cameligo.ml

@@ -246,7 +246,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
   | [hd] -> simpl_type_expression hd
   | lst ->
       let%bind lst = bind_map_list simpl_type_expression lst in
-      ok @@ make_t @@ T_tuple lst
+      ok @@ make_t @@ T_operator (TC_tuple lst)
 
 let rec simpl_expression :
   Raw.expr -> expr result = fun t ->
@@ -291,14 +291,23 @@ let rec simpl_expression :
     | _ -> e_accessor (e_variable (Var.of_name name)) path in 
     let updates = u.updates.value.ne_elements in
     let%bind updates' =
-      let aux (f:Raw.field_assign Raw.reg) =
+      let aux (f:Raw.field_path_assign Raw.reg) =
         let (f,_) = r_split f in
         let%bind expr = simpl_expression f.field_expr in
-        ok (f.field_name.value, expr)
+        ok ( List.map (fun (x: _ Raw.reg) -> x.value) (npseq_to_list f.field_path), expr)
       in
       bind_map_list aux @@ npseq_to_list updates 
     in
-    return @@ e_update ~loc record updates'
+    let aux ur (path, expr) = 
+      let rec aux record = function
+        | [] -> failwith "error in parsing"
+        | hd :: [] -> ok @@ e_update ~loc record hd expr
+        | hd :: tl -> 
+          let%bind expr = (aux (e_accessor ~loc record [Access_record hd]) tl) in
+          ok @@ e_update ~loc record hd expr 
+      in
+      aux ur path in
+    bind_fold_list aux record updates'
   in
 
   trace (simplifying_expr t) @@

src/passes/2-simplify/pascaligo.ml

@@ -267,7 +267,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
   | [hd] -> simpl_type_expression hd
   | lst ->
       let%bind lst = bind_list @@ List.map simpl_type_expression lst in
-      ok @@ make_t @@ T_tuple lst
+      ok @@ make_t @@ T_operator (TC_tuple lst)
 
 let simpl_projection : Raw.projection Region.reg -> _ = fun p ->
   let (p' , loc) = r_split p in
@@ -473,14 +473,23 @@ and simpl_update = fun (u:Raw.update Region.reg) ->
   | _ -> e_accessor (e_variable (Var.of_name name)) path in
   let updates = u.updates.value.ne_elements in
   let%bind updates' =
-    let aux (f:Raw.field_assign Raw.reg) =
+    let aux (f:Raw.field_path_assign Raw.reg) =
       let (f,_) = r_split f in
       let%bind expr = simpl_expression f.field_expr in
-      ok (f.field_name.value, expr)
+        ok ( List.map (fun (x: _ Raw.reg) -> x.value) (npseq_to_list f.field_path), expr)
     in
     bind_map_list aux @@ npseq_to_list updates
   in
-  ok @@ e_update ~loc record updates'
+  let aux ur (path, expr) = 
+    let rec aux record = function
+      | [] -> failwith "error in parsing"
+      | hd :: [] -> ok @@ e_update ~loc record hd expr
+      | hd :: tl -> 
+        let%bind expr = (aux (e_accessor ~loc record [Access_record hd]) tl) in
+        ok @@ e_update ~loc record hd expr 
+    in
+    aux ur path in
+  bind_fold_list aux record updates'
 
 and simpl_logic_expression (t:Raw.logic_expr) : expression result =
   let return x = ok x in
@@ -654,7 +663,7 @@ and simpl_fun_decl :
        let arguments_name = Var.of_name "arguments" in
        let%bind params = bind_map_list simpl_param lst in
        let (binder , input_type) =
-         let type_expression = T_tuple (List.map snd params) in
+         let type_expression = t_tuple (List.map snd params) in
          (arguments_name , type_expression) in
        let%bind tpl_declarations =
          let aux = fun i x ->
@@ -673,8 +682,8 @@ and simpl_fun_decl :
          let aux prec cur = cur (Some prec) in
          bind_fold_right_list aux result body in
        let expression =
-         e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in
+         e_lambda ~loc binder (Some input_type) (Some output_type) result in
-       let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in
+       let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in
        ok ((Var.of_name fun_name.value, type_annotation), expression)
      )
   )
@@ -708,7 +717,7 @@ and simpl_fun_expression :
        let arguments_name = Var.of_name "arguments" in
        let%bind params = bind_map_list simpl_param lst in
        let (binder , input_type) =
-         let type_expression = T_tuple (List.map snd params) in
+         let type_expression = t_tuple (List.map snd params) in
          (arguments_name , type_expression) in
        let%bind tpl_declarations =
          let aux = fun i x ->
@@ -727,8 +736,8 @@ and simpl_fun_expression :
          let aux prec cur = cur (Some prec) in
          bind_fold_right_list aux result body in
        let expression =
-         e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in
+         e_lambda ~loc binder (Some (input_type)) (Some output_type) result in
-       let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in
+       let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in
        ok (type_annotation, expression)
      )
   )

src/passes/3-self_ast_simplified/helpers.ml

@@ -41,13 +41,9 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
     let%bind res = bind_fold_lmap aux (ok init') m in
     ok res
   )
-  | E_update {record;updates} -> (
+  | E_update {record;update=(_,expr)} -> (
     let%bind res = self init' record in
-    let aux res (_, expr) =
+    let%bind res = fold_expression self res expr in
-      let%bind res = fold_expression self res expr in
-      ok res
-    in
-    let%bind res = bind_fold_list aux res updates in
     ok res 
   )
   | E_let_in { binder = _ ; rhs ; result } -> (
@@ -140,10 +136,10 @@ let rec map_expression : mapper -> expression -> expression result = fun f e ->
     let%bind m' = bind_map_lmap self m in
     return @@ E_record m'
   )
-  | E_update {record; updates} -> (
+  | E_update {record; update=(l,expr)} -> (
     let%bind record = self record in
-    let%bind updates = bind_map_list (fun(l,e) -> let%bind e = self e in ok (l,e)) updates in
+    let%bind expr = self expr in
-    return @@ E_update {record;updates}
+    return @@ E_update {record;update=(l,expr)}
   )
   | E_constructor (name , e) -> (
       let%bind e' = self e in

src/passes/4-typer-new/PP.ml

@@ -0,0 +1,54 @@
+open Solver
+open Format
+
+let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
+  function
+  |SC_Constructor { tv; c_tag; tv_list=_ } ->
+    let ct = match c_tag with
+      | Solver.Core.C_arrow     -> "arrow"
+      | Solver.Core.C_option    -> "option"
+      | Solver.Core.C_tuple     -> "tuple"
+      | Solver.Core.C_record    -> failwith "record"
+      | Solver.Core.C_variant   -> failwith "variant"
+      | Solver.Core.C_map       -> "map"
+      | Solver.Core.C_big_map   -> "big_map"
+      | Solver.Core.C_list      -> "list"
+      | Solver.Core.C_set       -> "set"
+      | Solver.Core.C_unit      -> "unit"
+      | Solver.Core.C_bool      -> "bool"
+      | Solver.Core.C_string    -> "string"
+      | Solver.Core.C_nat       -> "nat"
+      | Solver.Core.C_mutez     -> "mutez"
+      | Solver.Core.C_timestamp -> "timestamp"
+      | Solver.Core.C_int       -> "int"
+      | Solver.Core.C_address   -> "address"
+      | Solver.Core.C_bytes     -> "bytes"
+      | Solver.Core.C_key_hash  -> "key_hash"
+      | Solver.Core.C_key       -> "key"
+      | Solver.Core.C_signature -> "signature"
+      | Solver.Core.C_operation -> "operation"
+      | Solver.Core.C_contract  -> "contract"
+      | Solver.Core.C_chain_id  -> "chain_id"
+    in
+    fprintf ppf "CTOR %a %s()" Var.pp tv ct
+  |SC_Alias       (a, b) -> fprintf ppf "Alias %a %a" Var.pp a Var.pp b
+  |SC_Poly        _ -> fprintf ppf "Poly"
+  |SC_Typeclass   _ -> fprintf ppf "TC"
+
+let all_constraints ppf ac =
+  fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac
+
+let aliases ppf (al : unionfind) =
+  fprintf ppf "ALIASES %a" UF.print al
+
+let structured_dbs : _ -> structured_dbs -> unit = fun ppf structured_dbs ->
+  let { all_constraints = a ; aliases = b ; _ } = structured_dbs in
+  fprintf ppf "STRUCTURED_DBS\n %a\n %a" all_constraints a aliases b
+
+let already_selected : _ -> already_selected -> unit = fun ppf already_selected ->
+  let _ = already_selected in
+  fprintf ppf "ALREADY_SELECTED"
+
+let state : _ -> state -> unit = fun ppf state ->
+  let { structured_dbs=a ; already_selected=b } = state in
+  fprintf ppf "STATE %a %a" structured_dbs a already_selected b

src/passes/4-typer-new/solver.ml

@@ -34,8 +34,6 @@ module Wrap = struct
 
   let rec type_expression_to_type_value : T.type_value -> O.type_value = fun te ->
     match te.type_value' with
-    | T_tuple types ->
-      P_constant (C_tuple, List.map type_expression_to_type_value types)
     | T_sum kvmap ->
       P_constant (C_variant, T.CMap.to_list @@ T.CMap.map type_expression_to_type_value kvmap)
     | T_record kvmap ->
@@ -64,21 +62,20 @@ module Wrap = struct
       P_constant (csttag, [])
     | T_operator (type_operator) ->
       let (csttag, args) = Core.(match type_operator with
-          | TC_option o      -> (C_option, [o])
+          | TC_option o            -> (C_option, [o])
-          | TC_set s         -> (C_set, [s])
+          | TC_set s               -> (C_set, [s])
-          | TC_map (k,v)     -> (C_map, [k;v])
+          | TC_map ( k , v )       -> (C_map, [k;v])
-          | TC_big_map (k,v) -> (C_big_map, [k;v])
+          | TC_big_map ( k , v)    -> (C_big_map, [k;v])
-          | TC_list l        -> (C_list, [l])
+          | TC_list l              -> (C_list, [l])
-          | TC_contract c    -> (C_contract, [c])
+          | TC_contract c          -> (C_contract, [c])
+          | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
+          | TC_tuple lst           -> (C_tuple, lst)
       )
       in
       P_constant (csttag, List.map type_expression_to_type_value args)
 
-
   let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_value = fun te ->
     match te.type_expression' with
-    | T_tuple types ->
-      P_constant (C_tuple, List.map type_expression_to_type_value_copypasted types)
     | T_sum kvmap ->
       P_constant (C_variant, I.CMap.to_list @@ I.CMap.map type_expression_to_type_value_copypasted kvmap)
     | T_record kvmap ->
@@ -96,12 +93,14 @@ module Wrap = struct
       P_constant (csttag,[])
     | T_operator (type_name) ->
       let (csttag, args) = Core.(match type_name with
-          | TC_option o       -> (C_option , [o])
+          | TC_option o            -> (C_option , [o])
-          | TC_list l         -> (C_list   , [l])
+          | TC_list l              -> (C_list   , [l])
-          | TC_set  s         -> (C_set    , [s]) 
+          | TC_set  s              -> (C_set    , [s])
-          | TC_map  (k,v)     -> (C_map    , [k;v])
+          | TC_map  ( k , v )      -> (C_map    , [k;v])
-          | TC_big_map  (k,v) -> (C_big_map, [k;v])
+          | TC_big_map  ( k , v )  -> (C_big_map, [k;v])
-          | TC_contract c     -> (C_contract, [c])
+          | TC_contract c          -> (C_contract, [c])
+          | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
+          | TC_tuple lst           -> (C_tuple, lst)
       )
       in
       P_constant (csttag, List.map type_expression_to_type_value_copypasted args)
@@ -350,7 +349,7 @@ end
 module TypeVariable =
 struct
   type t = Core.type_variable
-  let compare a b= Var.compare a b
+  let compare a b = Var.compare a b
   let to_string = (fun s -> Format.asprintf "%a" Var.pp s)
 
 end
@@ -475,44 +474,69 @@ module UnionFindWrapper = struct
       in
       let dbs = { dbs with grouped_by_variable } in
       dbs
-  let merge_variables : type_variable -> type_variable -> structured_dbs -> structured_dbs =
+
+  let merge_constraints : type_variable -> type_variable -> structured_dbs -> structured_dbs =
     fun variable_a variable_b dbs ->
+    (* get old representant for variable_a *)
     let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in
     let dbs = { dbs with aliases } in
+    (* get old representant for variable_b *)
     let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in
     let dbs = { dbs with aliases } in
-    let default d = function None -> d | Some y -> y in
+
-    let get_constraints ab =
+    (* alias variable_a and variable_b together *)
-      TypeVariableMap.find_opt ab dbs.grouped_by_variable
+    let aliases = UF.alias variable_a variable_b dbs.aliases in
-      |> default { constructor = [] ; poly = [] ; tc = [] } in
+    let dbs = { dbs with aliases } in
-    let constraints_a = get_constraints variable_repr_a in
+
-    let constraints_b = get_constraints variable_repr_b in
+    (* Replace the two entries in grouped_by_variable by a single one *)
-    let all_constraints = {
+    (
-      constructor = constraints_a.constructor @ constraints_b.constructor ;
+      let get_constraints ab =
-      poly        = constraints_a.poly        @ constraints_b.poly        ;
+        match TypeVariableMap.find_opt ab dbs.grouped_by_variable with
-      tc          = constraints_a.tc          @ constraints_b.tc          ;
+        | Some x -> x
-    } in
+        | None -> { constructor = [] ; poly = [] ; tc = [] } in
-    let grouped_by_variable =
+      let constraints_a = get_constraints variable_repr_a in
-      TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in
+      let constraints_b = get_constraints variable_repr_b in
-    let dbs = { dbs with grouped_by_variable} in
+      let all_constraints = {
-    let grouped_by_variable =
+          constructor = constraints_a.constructor @ constraints_b.constructor ;
-      TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
+          poly        = constraints_a.poly        @ constraints_b.poly        ;
-    let dbs = { dbs with grouped_by_variable} in
+          tc          = constraints_a.tc          @ constraints_b.tc          ;
-    dbs
+        } in
+      let grouped_by_variable =
+        TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in
+      let dbs = { dbs with grouped_by_variable} in
+      let grouped_by_variable =
+        TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
+      let dbs = { dbs with grouped_by_variable} in
+      dbs
+    )
 end
 
 (* sub-sub component: constraint normalizer: remove dupes and give structure
  * right now: union-find of unification vars
  * later: better database-like organisation of knowledge *)
 
-(* Each normalizer returns a  *)
+(* Each normalizer returns an updated database (after storing the
-(* If implemented in a language with decent sets, should be 'b set not 'b list. *)
+   incoming constraint) and a list of constraints, used when the
+   normalizer rewrites the constraints e.g. into simpler ones. *)
+(* TODO: If implemented in a language with decent sets, should be 'b set not 'b list. *)
 type ('a , 'b) normalizer = structured_dbs -> 'a -> (structured_dbs * 'b list)
 
+(** Updates the dbs.all_constraints field when new constraints are
+   discovered.
+
+   This field contains a list of all the constraints, without any form of
+   grouping or sorting. *)
 let normalizer_all_constraints : (type_constraint_simpl , type_constraint_simpl) normalizer =
   fun dbs new_constraint ->
     ({ dbs with all_constraints = new_constraint :: dbs.all_constraints } , [new_constraint])
 
+(** Updates the dbs.grouped_by_variable field when new constraints are
+   discovered.
+
+    This field contains a map from type variables to lists of
+   constraints that are related to that variable (in other words, the
+   key appears in the equation).
+ *)
 let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_simpl) normalizer =
   fun dbs new_constraint ->
   let store_constraint tvars constraints =
@@ -520,16 +544,18 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si
       UnionFindWrapper.add_constraints_related_to tvar constraints dbs
     in List.fold_left aux dbs tvars
   in
-  let merge_constraints a b =
-    UnionFindWrapper.merge_variables a b dbs in
   let dbs = match new_constraint with
       SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; poly = []  ; tc = []}
     | SC_Typeclass   ({tc = _ ; args}            as c) -> store_constraint args            {constructor = []  ; poly = []  ; tc = [c]}
     | SC_Poly        ({tv; forall = _}           as c) -> store_constraint [tv]            {constructor = []  ; poly = [c] ; tc = []}
-    | SC_Alias (a , b) -> merge_constraints a b
+    | SC_Alias (a , b) -> UnionFindWrapper.merge_constraints a b dbs
   in (dbs , [new_constraint])
 
-(* Stores the first assinment ('a = ctor('b, …)) seen *)
+(** Stores the first assinment ('a = ctor('b, …)) that is encountered.
+
+    Subsequent ('a = ctor('b2, …)) with the same 'a are ignored.
+
+    TOOD: are we checking somewhere that 'b … = 'b2 … ? *)
 let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer =
   fun dbs new_constraint ->
     match new_constraint with
@@ -540,9 +566,14 @@ let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) nor
     | _ ->
       (dbs , [new_constraint])
 
+(** Evaluates a type-leval application. For now, only supports
+    immediate beta-reduction at the root of the type. *)
 let type_level_eval : type_value -> type_value * type_constraint list =
   fun tv -> Typesystem.Misc.Substitution.Pattern.eval_beta_root ~tv
 
+(** Checks that a type-level application has been fully reduced. For
+    now, only some simple cases like applications of `forall`
+    <polymorphic types are allowed. *)
 let check_applied ((reduced, _new_constraints) as x) =
   let () = match reduced with
       P_apply _ -> failwith "internal error: shouldn't happen" (* failwith "could not reduce type-level application. Arbitrary type-level applications are not supported for now." *)
@@ -552,6 +583,14 @@ let check_applied ((reduced, _new_constraints) as x) =
 (* TODO: at some point there may be uses of named type aliases (type
    foo = int; let x : foo = 42). These should be inlined. *)
 
+(** This function converts constraints from type_constraint to
+    type_constraint_simpl. The former has more possible cases, and the
+    latter uses a more minimalistic constraint language.
+
+    It does not modify the dbs, and only rewrites the constraint
+
+    TODO: update the code to show that the dbs are always copied as-is
+ *)
 let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer =
   fun dbs new_constraint ->
   let insert_fresh a b =

src/passes/4-typer-new/typer.ml

@@ -334,9 +334,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
     let%bind a' = evaluate_type e a in
     let%bind b' = evaluate_type e b in
     return (T_arrow (a', b'))
-  | T_tuple lst ->
-    let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
-    return (T_tuple lst')
   | T_sum m ->
     let aux k v prev =
       let%bind prev' = prev in
@@ -382,6 +379,13 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
         | TC_contract c ->
             let%bind c = evaluate_type e c in
             ok @@ O.TC_contract c
+        | TC_arrow ( arg , ret ) ->
+           let%bind arg' = evaluate_type e arg in
+           let%bind ret' = evaluate_type e ret in
+           ok @@ O.TC_arrow ( arg' , ret' )
+        | TC_tuple lst ->
+           let%bind lst' = bind_map_list (evaluate_type e) lst in
+           ok @@ O.TC_tuple lst'
         in
       return (T_operator (opt))
 
@@ -469,10 +473,11 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e
       return_wrapped (e_operation o) state @@ Wrap.literal (t_operation ())
     )
   | E_literal (Literal_unit) -> (
-      return_wrapped (e_unit) state @@ Wrap.literal (t_unit ())
+      return_wrapped (e_unit ()) state @@ Wrap.literal (t_unit ())
     )
   | E_skip -> (
-      failwith "TODO: missing implementation for E_skip"
+    (* E_skip just returns unit *)
+    return_wrapped (e_unit ()) state @@ Wrap.literal (t_unit ())
     )
   (* | E_literal (Literal_string s) -> (
    *     L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_expression) tv_opt) ;
@@ -516,7 +521,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e
       trace_option error @@
       Environment.get_constructor c e in
     let%bind (expr' , state') = type_expression e state expr in
-    let%bind _assert = O.assert_type_value_eq (expr'.type_annotation, c_tv) in
     let wrapped = Wrap.constructor expr'.type_annotation c_tv sum_tv in
     return_wrapped (E_constructor (c , expr')) state' wrapped
 
@@ -529,27 +533,22 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e
     let%bind (m' , state') = I.bind_fold_lmap aux (ok (I.LMap.empty , state)) m in
     let wrapped = Wrap.record (I.LMap.map get_type_annotation m') in
     return_wrapped (E_record m') state' wrapped
-  | E_update {record; updates} ->
+  | E_update {record; update=(k,expr)} ->
     let%bind (record, state) = type_expression e state record in
-    let aux (lst,state) (k, expr) =
+    let%bind (expr,state) = type_expression e state expr in
-      let%bind (expr', state) = type_expression e state expr in
-      ok ((k,expr')::lst, state)
-    in 
-    let%bind (updates, state) = bind_fold_list aux ([], state) updates in
     let wrapped = get_type_annotation record in
-    let%bind wrapped = match wrapped.type_value' with 
+    let%bind (wrapped,tv) = 
-    | T_record record ->
+      match wrapped.type_value' with 
-        let aux (k, e) =
+      | T_record record -> (
           let field_op = I.LMap.find_opt k record in
           match field_op with
+          | Some tv -> ok (record,tv)
           | None -> failwith @@ Format.asprintf "field %a is not part of record" Stage_common.PP.label k
-          | Some tv -> O.assert_type_value_eq (tv, get_type_annotation e)
+      )
-        in
+      | _ -> failwith "Update an expression which is not a record"
-        let%bind () = bind_iter_list aux updates in
-        ok (record)
-    | _ -> failwith "Update an expression which is not a record"
     in
-    return_wrapped (E_record_update (record, updates)) state (Wrap.record wrapped)
+    let%bind () = O.assert_type_value_eq (tv, get_type_annotation expr) in
+    return_wrapped (E_record_update (record, (k,expr))) state (Wrap.record wrapped)
   (* Data-structure *)
 
 (*
@@ -937,9 +936,7 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result =
 (*
 Apply type_declaration on all the node of the AST_simplified from the root p
 *)
-let type_program_returns_state (p:I.program) : (environment * Solver.state * O.program) result =
+let type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result =
-  let env = Ast_typed.Environment.full_empty in
-  let state = Solver.initial_state in
   let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
     let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in
     let ds' = match d'_opt with
@@ -954,51 +951,45 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p
   let () = ignore (env' , state') in
   ok (env', state', declarations)
 
-(* module TSMap = TMap(Solver.TypeVariable) *)
+let type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * Solver.state * 'a) -> (environment * Solver.state * 'b) Trace.result) : ('b * Solver.state) result =
-
+  let%bind (env, state, program) = type_xyz_returns_state env_state_node in
-(* let c_tag_to_string : Solver.Core.constant_tag -> string = function
- *   | Solver.Core.C_arrow     -> "arrow"
- *   | Solver.Core.C_option    -> "option"
- *   | Solver.Core.C_tuple     -> "tuple"
- *   | Solver.Core.C_record    -> failwith "record"
- *   | Solver.Core.C_variant   -> failwith "variant"
- *   | Solver.Core.C_map       -> "map"
- *   | Solver.Core.C_big_map   -> "big"
- *   | Solver.Core.C_list      -> "list"
- *   | Solver.Core.C_set       -> "set"
- *   | Solver.Core.C_unit      -> "unit"
- *   | Solver.Core.C_bool      -> "bool"
- *   | Solver.Core.C_string    -> "string"
- *   | Solver.Core.C_nat       -> "nat"
- *   | Solver.Core.C_mutez     -> "mutez"
- *   | Solver.Core.C_timestamp -> "timestamp"
- *   | Solver.Core.C_int       -> "int"
- *   | Solver.Core.C_address   -> "address"
- *   | Solver.Core.C_bytes     -> "bytes"
- *   | Solver.Core.C_key_hash  -> "key_hash"
- *   | Solver.Core.C_key       -> "key"
- *   | Solver.Core.C_signature -> "signature"
- *   | Solver.Core.C_operation -> "operation"
- *   | Solver.Core.C_contract  -> "contract"
- *   | Solver.Core.C_chain_id  -> "chain_id" *)
-
-let type_program (p : I.program) : (O.program * Solver.state) result =
-  let%bind (env, state, program) = type_program_returns_state p in
   let subst_all =
+    let aliases = state.structured_dbs.aliases in
     let assignments = state.structured_dbs.assignments in
-    let aux (v : I.type_variable) (expr : Solver.c_constructor_simpl) (p:O.program result) =
+    let substs : variable: I.type_variable -> _ = fun ~variable ->
-      let%bind p = p in
+      to_option @@
-      let Solver.{ tv ; c_tag ; tv_list } = expr in
+      let%bind root =
+        trace_option (simple_error (Format.asprintf "can't find alias root of variable %a" Var.pp variable)) @@
+          (* TODO: after upgrading UnionFind, this will be an option, not an exception. *)
+          try Some (Solver.UF.repr variable aliases) with Not_found -> None in
+      let%bind assignment =
+        trace_option (simple_error (Format.asprintf "can't find assignment for root %a" Var.pp root)) @@
+          (Solver.TypeVariableMap.find_opt root assignments) in
+      let Solver.{ tv ; c_tag ; tv_list } = assignment in
       let () = ignore tv (* I think there is an issue where the tv is stored twice (as a key and in the element itself) *) in
       let%bind (expr : O.type_value') = Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.{ type_value' = T_variable s ; simplified = None }) tv_list)) in
-      Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in
+      ok @@ expr
-    (* let p = TSMap.bind_fold_Map aux program assignments in *) (* TODO: Module magic: this does not work *)
+    in
-    let p = Solver.TypeVariableMap.fold aux assignments (ok program) in
+    let p = apply_substs ~substs program in
     p in
   let%bind program = subst_all in
   let () = ignore env in        (* TODO: shouldn't we use the `env` somewhere? *)
   ok (program, state)
 
+let type_program (p : I.program) : (O.program * Solver.state) result =
+  let empty_env = Ast_typed.Environment.full_empty in
+  let empty_state = Solver.initial_state in
+  type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state
+
+let type_expression_returns_state : (environment * Solver.state * I.expression) -> (environment * Solver.state * O.annotated_expression) Trace.result =
+  fun (env, state, e) ->
+  let%bind (e , state) = type_expression env state e in
+  ok (env, state, e)
+
+let type_expression_subst (env : environment) (state : Solver.state) ?(tv_opt : O.type_value option) (e : I.expression) : (O.annotated_expression * Solver.state) result =
+  let () = ignore tv_opt in     (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *)
+  type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_annotated_expression type_expression_returns_state
+
  (*
 TODO: Similar to type_program but use a fold_map_list and List.fold_left and add element to the left or the list which gives a better complexity
  *)
@@ -1026,9 +1017,6 @@ let type_program' : I.program -> O.program result = fun p ->
 let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
   (* TODO: or should we use t.simplified if present? *)
   let%bind t = match t.type_value' with
-  | O.T_tuple x ->
-    let%bind x' = bind_map_list untype_type_expression x in
-    ok @@ I.T_tuple x'
   | O.T_sum x ->
     let%bind x' = I.bind_map_cmap untype_type_expression x in
     ok @@ I.T_sum x'
@@ -1064,6 +1052,13 @@ let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
       | O.TC_contract c->
          let%bind c = untype_type_expression c in
          ok @@ I.TC_contract c
+      | O.TC_arrow ( arg , ret ) ->
+         let%bind arg' = untype_type_expression arg in
+         let%bind ret' = untype_type_expression ret in
+         ok @@ I.TC_arrow ( arg' , ret' )
+      | O.TC_tuple lst ->
+         let%bind lst' = bind_map_list untype_type_expression lst in
+         ok @@ I.TC_tuple lst'
       in
       ok @@ I.T_operator (type_name)
     in
@@ -1139,14 +1134,11 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
   | E_record_accessor (r, Label s) ->
     let%bind r' = untype_expression r in
     return (e_accessor r' [Access_record s])
-  | E_record_update (r, updates) ->
+  | E_record_update (r, (l,e)) ->
     let%bind r' = untype_expression r in
-    let aux (Label l,e) =
+    let%bind e = untype_expression e in 
-      let%bind e = untype_expression e in 
+    let Label l = l in
-      ok (l, e)
+    return (e_update r' l e)
-    in
-    let%bind updates = bind_map_list aux updates in
-    return (e_update r' updates)
   | E_map m ->
     let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
     return (e_map m')

src/passes/4-typer-new/typer.mli

@@ -44,6 +44,7 @@ val type_declaration : environment -> Solver.state -> I.declaration -> (environm
 (* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *)
 val evaluate_type : environment -> I.type_expression -> O.type_value result
 val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
+val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
 val type_constant : I.constant -> O.type_value list -> O.type_value option -> (O.constant * O.type_value) result
 (*
 val untype_type_value : O.type_value -> (I.type_expression) result

src/passes/4-typer-old/typer.ml

@@ -327,9 +327,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
       let%bind a' = evaluate_type e a in
       let%bind b' = evaluate_type e b in
       return (T_arrow (a', b'))
-  | T_tuple lst ->
-      let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
-      return (T_tuple lst')
   | T_sum m ->
       let aux k v prev =
         let%bind prev' = prev in
@@ -375,6 +372,13 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
         | TC_contract c ->
             let%bind c = evaluate_type e c in
             ok @@ I.TC_contract c
+        | TC_arrow ( arg , ret ) ->
+            let%bind arg' = evaluate_type e arg in
+            let%bind ret' = evaluate_type e ret in
+            ok @@ I.TC_arrow ( arg' , ret' )
+        | TC_tuple lst ->
+            let%bind lst' = bind_map_list (evaluate_type e) lst in
+            ok @@ I.TC_tuple lst'
         in
       return (T_operator (opt))
 
@@ -496,26 +500,22 @@ and type_expression' : environment -> ?tv_opt:O.type_value -> I.expression -> O.
       in
       let%bind m' = I.bind_fold_lmap aux (ok I.LMap.empty) m in
       return (E_record m') (t_record (I.LMap.map get_type_annotation m') ())
-  | E_update {record; updates} ->
+  | E_update {record; update =(l,expr)} ->
     let%bind record = type_expression' e record in
-    let aux acc (k, expr) =
+    let%bind expr' = type_expression' e expr in
-      let%bind expr' = type_expression' e expr in
-      ok ((k,expr')::acc)
-    in 
-    let%bind updates = bind_fold_list aux ([]) updates in
     let wrapped = get_type_annotation record in
-    let%bind () = match wrapped.type_value' with 
+    let%bind tv = 
-    | T_record record ->
+      match wrapped.type_value' with 
-        let aux (k, e) =
+      | T_record record -> (
-          let field_op = I.LMap.find_opt k record in
+          let field_op = I.LMap.find_opt l record in
           match field_op with
-          | None -> failwith @@ Format.asprintf "field %a is not part of record" Stage_common.PP.label k
+          | Some tv -> ok (tv)
-          | Some tv -> O.assert_type_value_eq (tv, get_type_annotation e)
+          | None -> failwith @@ Format.asprintf "field %a is not part of record %a" Stage_common.PP.label l O.PP.type_value wrapped
-        in
+      )
-        bind_iter_list aux updates
+      | _ -> failwith "Update an expression which is not a record"
-    | _ -> failwith "Update an expression which is not a record"
     in
-    return (E_record_update (record, updates)) wrapped
+    let%bind () = O.assert_type_value_eq (tv, get_type_annotation expr') in
+    return (E_record_update (record, (l,expr'))) wrapped
   (* Data-structure *)
   | E_list lst ->
       let%bind lst' = bind_map_list (type_expression' e) lst in
@@ -896,14 +896,11 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
   | E_record_accessor (r, Label s) ->
       let%bind r' = untype_expression r in
       return (e_accessor r' [Access_record s])
-  | E_record_update (r, updates) ->
+  | E_record_update (r, (l,e)) ->
     let%bind r' = untype_expression r in
-    let aux (Label l,e) =
+    let%bind e = untype_expression e in 
-      let%bind e = untype_expression e in 
+    let Label l = l in
-      ok (l, e)
+    return (e_update r' l e)
-    in
-    let%bind updates = bind_map_list aux updates in
-    return (e_update r' updates)
   | E_map m ->
       let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
       return (e_map m')

src/passes/4-typer/typer.ml

@@ -10,5 +10,5 @@ module Solver = Typer_new.Solver (* Both the old typer and the new typer use the
 type environment = Environment.t
 
 let type_program = if use_new_typer then Typer_new.type_program else Typer_old.type_program
-let type_expression = if use_new_typer then Typer_new.type_expression else Typer_old.type_expression
+let type_expression_subst = if use_new_typer then Typer_new.type_expression_subst else Typer_old.type_expression (* the old typer does not have unification variables that would need substitution, so no need to "subst" anything. *)
 let untype_expression = if use_new_typer then Typer_new.untype_expression else Typer_old.untype_expression

src/passes/4-typer/typer.mli

@@ -12,5 +12,5 @@ module Solver = Typer_new.Solver
 type environment = Environment.t
 
 val type_program : I.program -> (O.program * Solver.state) result
-val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
+val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
 val untype_expression : O.annotated_expression -> I.expression result

src/passes/6-transpiler/transpiler.ml

@@ -146,6 +146,11 @@ let rec transpile_type (t:AST.type_value) : type_value result =
   | T_operator (TC_option o) ->
       let%bind o' = transpile_type o in
       ok (T_option o')
+  | T_operator (TC_arrow (param , result)) -> (
+      let%bind param' = transpile_type param in
+      let%bind result' = transpile_type result in
+      ok (T_function (param', result'))
+    )
   (* TODO hmm *)
   | T_sum m ->
       let node = Append_tree.of_list @@ kv_list_of_cmap m in
@@ -173,7 +178,7 @@ let rec transpile_type (t:AST.type_value) : type_value result =
                         ok (Some ann, a))
                       aux node in
       ok @@ snd m'
-  | T_tuple lst ->
+  | T_operator (TC_tuple lst) ->
       let node = Append_tree.of_list lst in
       let aux a b : type_value result =
         let%bind a = a in
@@ -206,11 +211,11 @@ let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * [
     bind_fold_list aux (ty , []) lr_path in
   ok lst
 
-let record_access_to_lr : type_value -> type_value AST.label_map -> string -> (type_value * [`Left | `Right]) list result = fun ty tym ind ->
+let record_access_to_lr : type_value -> type_value AST.label_map -> label -> (type_value * [`Left | `Right]) list result = fun ty tym ind ->
   let tys = kv_list_of_lmap tym in
   let node_tv = Append_tree.of_list tys in
   let%bind path =
-    let aux (Label i , _) = i = ind in
+    let aux (Label i , _) = let Label ind = ind in i = ind in
     trace_option (corner_case ~loc:__LOC__ "record access leaf") @@
     Append_tree.exists_path aux node_tv in
   let lr_path = List.map (fun b -> if b then `Right else `Left) path in
@@ -320,7 +325,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
   | E_tuple_accessor (tpl, ind) -> (
       let%bind ty' = transpile_type tpl.type_annotation in
       let%bind ty_lst =
-        trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@
+        trace_strong (corner_case ~loc:__LOC__ "transpiler: E_tuple_accessor: not a tuple") @@
         get_t_tuple tpl.type_annotation in
       let%bind ty'_lst = bind_map_list transpile_type ty_lst in
       let%bind path =
@@ -348,7 +353,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
       trace_strong (corner_case ~loc:__LOC__ "record build") @@
       Append_tree.fold_ne (transpile_annotated_expression) aux node
     )
-  | E_record_accessor (record, Label property) ->
+  | E_record_accessor (record, property) ->
       let%bind ty' = transpile_type (get_type_annotation record) in
       let%bind ty_lmap =
         trace_strong (corner_case ~loc:__LOC__ "not a record") @@
@@ -365,23 +370,19 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
       let%bind record' = transpile_annotated_expression record in
       let expr = List.fold_left aux record' path in
       ok expr
-  | E_record_update (record, updates) -> 
+  | E_record_update (record, (l,expr)) -> 
       let%bind ty' = transpile_type (get_type_annotation record) in 
       let%bind ty_lmap =
         trace_strong (corner_case ~loc:__LOC__ "not a record") @@
         get_t_record (get_type_annotation record) in
       let%bind ty'_lmap = AST.bind_map_lmap transpile_type ty_lmap in
-      let aux (Label l, expr) =
+      let%bind path = 
-        let%bind path = 
+        trace_strong (corner_case ~loc:__LOC__ "record access") @@
-          trace_strong (corner_case ~loc:__LOC__ "record access") @@
+        record_access_to_lr ty' ty'_lmap l in
-          record_access_to_lr ty' ty'_lmap l in
+      let path' = List.map snd path in
-        let path' = List.map snd path in
+      let%bind expr' = transpile_annotated_expression expr in
-        let%bind expr' = transpile_annotated_expression expr in
-        ok (path',expr') 
-      in
-      let%bind updates = bind_map_list aux updates in
       let%bind record = transpile_annotated_expression record in
-      return @@ E_update (record, updates) 
+      return @@ E_update (record, (path',expr')) 
   | E_constant (name , lst) -> (
       let iterator_generator iterator_name =
         let lambda_to_iterator_body (f : AST.annotated_expression) (l : AST.lambda) =
@@ -509,7 +510,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
           match cur with
           | Access_tuple ind -> (
               let%bind ty_lst =
-                trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@
+                trace_strong (corner_case ~loc:__LOC__ "transpiler: E_assign: Access_tuple: not a tuple") @@
                 AST.Combinators.get_t_tuple prev in
               let%bind ty'_lst = bind_map_list transpile_type ty_lst in
               let%bind path = tuple_access_to_lr ty' ty'_lst ind in
@@ -521,7 +522,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
                 trace_strong (corner_case ~loc:__LOC__ "not a record") @@
                 AST.Combinators.get_t_record prev in
               let%bind ty'_map = bind_map_lmap transpile_type ty_map in
-              let%bind path = record_access_to_lr ty' ty'_map prop in
+              let%bind path = record_access_to_lr ty' ty'_map (Label prop) in
               let path' = List.map snd path in
             let%bind prop_in_ty_map = trace_option
                 (Errors.not_found "acessing prop in ty_map [TODO: better error message]")

src/passes/6-transpiler/untranspiler.ml

@@ -36,15 +36,6 @@ them. please report this to the developers." in
     ] in
     error ~data title content
 
-  let unknown_untranspile unknown_type value =
-    let title () = "untranspiling unknown value" in
-    let content () = Format.asprintf "can not untranspile %s" unknown_type in
-    let data = [
-      ("unknown_type" , fun () -> unknown_type) ;
-      ("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ;
-    ] in
-    error ~data title content
-
 end
 
 open Errors
@@ -196,6 +187,22 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
       )
     | TC_contract _ ->
       fail @@ bad_untranspile "contract" v
+    | TC_arrow _ -> (
+        let%bind n =
+          trace_strong (wrong_mini_c_value "lambda as string" v) @@
+          get_string v in
+        return (E_literal (Literal_string n))
+      )
+    | TC_tuple lst ->
+      let%bind node = match Append_tree.of_list lst with
+        | Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple"
+        | Full t -> ok t in
+      let%bind tpl =
+        trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@
+        extract_tuple v node in
+      let%bind tpl' = bind_list
+        @@ List.map (fun (x, y) -> untranspile x y) tpl in
+      return (E_tuple tpl')
   )
   | T_sum m ->
       let lst = kv_list_of_cmap m in
@@ -208,16 +215,6 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
         extract_constructor v node in
       let%bind sub = untranspile v tv in
       return (E_constructor (Constructor name, sub))
-  | T_tuple lst ->
-      let%bind node = match Append_tree.of_list lst with
-        | Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple"
-        | Full t -> ok t in
-      let%bind tpl =
-        trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@
-        extract_tuple v node in
-      let%bind tpl' = bind_list
-        @@ List.map (fun (x, y) -> untranspile x y) tpl in
-      return (E_tuple tpl')
   | T_record m ->
       let lst = kv_list_of_lmap m in
       let%bind node = match Append_tree.of_list lst with

src/passes/7-self_mini_c/helpers.ml

@@ -84,13 +84,9 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
       let%bind res = self init' exp in
       ok res
   )
-  | E_update (r, updates) -> (
+  | E_update (r, (_,e)) -> (
       let%bind res = self init' r in
-      let aux prev (_,e) =
+      let%bind res = self res e in
-          let%bind res = self prev e in
-          ok res
-      in
-      let%bind res = bind_fold_list aux res updates in
       ok res
   )
 
@@ -158,10 +154,10 @@ let rec map_expression : mapper -> expression -> expression result = fun f e ->
       let%bind exp' = self exp in
       return @@ E_assignment (s, lrl, exp')
   )
-  | E_update (r, updates) -> (
+  | E_update (r, (l,e)) -> (
       let%bind r = self r in
-      let%bind updates = bind_map_list (fun (p,e) -> let%bind e = self e in ok(p,e)) updates in
+      let%bind e = self e in
-      return @@ E_update(r,updates)
+      return @@ E_update(r,(l,e))
   )
 
 let map_sub_level_expression : mapper -> expression -> expression result = fun f e ->

src/passes/7-self_mini_c/self_mini_c.ml

@@ -66,8 +66,8 @@ let rec is_pure : expression -> bool = fun e ->
 
   | E_constant (c, args)
     -> is_pure_constant c && List.for_all is_pure args
-  | E_update (e, updates)
+  | E_update (r, (_,e))
-    -> is_pure e && List.for_all (fun (_,e) -> is_pure e) updates
+    -> is_pure r && is_pure e
 
   (* I'm not sure about these. Maybe can be tested better? *)
   | E_application _
@@ -111,8 +111,8 @@ let rec is_assigned : ignore_lambdas:bool -> expression_variable -> expression -
   match e.content with
   | E_assignment (x, _, e) ->
     it x || self e
-  | E_update (r, updates) ->
+  | E_update (r, (_,e)) ->
-    List.fold_left (fun prev (_,e) -> prev || self e) (self r) updates
+    self r || self e
   | E_closure { binder; body } ->
     if ignore_lambdas
     then false

src/passes/7-self_mini_c/subst.ml

@@ -94,10 +94,10 @@ let rec replace : expression -> var_name -> var_name -> expression =
     let v = replace_var v in
     let e = replace e in
     return @@ E_assignment (v, path, e)
-  | E_update (r, updates) ->
+  | E_update (r, (p,e)) ->
     let r = replace r in
-    let updates = List.map (fun (p,e)-> (p, replace e)) updates in
+    let e = replace e in
-    return @@ E_update (r,updates)
+    return @@ E_update (r, (p,e))
   | E_while (cond, body) ->
     let cond = replace cond in
     let body = replace body in
@@ -209,10 +209,10 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e
       if Var.equal s x then raise Bad_argument ;
       return @@ E_assignment (s, lrl, exp')
   )
-  | E_update (r, updates) -> (
+  | E_update (r, (p,e)) -> (
     let r' = self r in
-    let updates' = List.map (fun (p,e) -> (p, self e)) updates in
+    let e' = self e in
-    return @@ E_update(r',updates')
+    return @@ E_update(r', (p,e'))
   )
 
 let%expect_test _ =

src/passes/8-compiler/compiler_program.ml

@@ -402,32 +402,29 @@ and translate_expression (expr:expression) (env:environment) : michelson result
         i_push_unit ;
       ]
     )
-  | E_update (record, updates) -> (
+  | E_update (record, (path, expr)) -> (
     let%bind record' = translate_expression record env in
-    let insts = [
+
-      i_comment "r_update: start, move the record on top # env";
+    let record_var = Var.fresh () in
-      record';] in 
+    let env' = Environment.add (record_var, record.type_value) env in
-    let aux (init :t list) (update,expr) = 
+    let%bind expr' = translate_expression expr env' in
-      let record_var = Var.fresh () in
+    let modify_code =
-      let env' = Environment.add (record_var, record.type_value) env in
+      let aux acc step = match step with
-      let%bind expr' = translate_expression expr env' in
+        | `Left -> seq [dip i_unpair ; acc ; i_pair]
-      let modify_code =
+        | `Right -> seq [dip i_unpiar ; acc ; i_piar]
-        let aux acc step = match step with
-          | `Left -> seq [dip i_unpair ; acc ; i_pair]
-          | `Right -> seq [dip i_unpiar ; acc ; i_piar]
-        in
-        let init = dip i_drop in
-        List.fold_right' aux init update
       in
-      ok @@ init @ [
+      let init = dip i_drop in
-        expr';
+      List.fold_right' aux init path
-        i_comment "r_updates : compute rhs # rhs:env";
-        modify_code;
-        i_comment "r_update: modify code # record+rhs : env";
-        ]
     in
-    let%bind insts = bind_fold_list aux insts updates in
+    return @@ seq [
-    return @@ seq insts
+      i_comment "r_update: start # env";
+      record';
+      i_comment "r_update: move the record on top # env";
+      expr';
+      i_comment "r_updates : compute rhs # rhs:env";
+      modify_code;
+      i_comment "r_update: modify code # record+rhs : env";
+      ]
 
   )
   | E_while (expr , block) -> (

src/stages/ast_simplified/PP.ml

@@ -18,7 +18,7 @@ and type_expression ppf (te: type_expression) : unit =
   te' ppf te.type_expression'
 
 let rec expression ppf (e:expression) = match e.expression with
-  | E_literal l -> literal ppf l
+  | E_literal l -> fprintf ppf "%a" literal l
   | E_variable n -> fprintf ppf "%a" name n
   | E_application (f, arg) -> fprintf ppf "(%a)@(%a)" expression f expression arg
   | E_constructor (c, ae) -> fprintf ppf "%a(%a)" constructor c expression ae
@@ -26,11 +26,11 @@ let rec expression ppf (e:expression) = match e.expression with
   | E_tuple lst -> fprintf ppf "(%a)" (tuple_sep_d expression) lst
   | E_accessor (ae, p) -> fprintf ppf "%a.%a" expression ae access_path p
   | E_record m -> fprintf ppf "{%a}" (lrecord_sep expression (const " , ")) m
-  | E_update {record; updates} -> fprintf ppf "%a with {%a}" expression record (tuple_sep_d (fun ppf (a,b) -> fprintf ppf "%a = %a" label a expression b)) updates
+  | E_update {record; update=(path,expr)} -> fprintf ppf "%a with { %a = %a }" expression record Stage_common.PP.label path expression expr
   | E_map m -> fprintf ppf "[%a]" (list_sep_d assoc_expression) m
   | E_big_map m -> fprintf ppf "big_map[%a]" (list_sep_d assoc_expression) m
   | E_list lst -> fprintf ppf "[%a]" (list_sep_d expression) lst
-  | E_set lst -> fprintf ppf "{%a}" (list_sep_d expression) lst
+  | E_set lst  -> fprintf ppf "{%a}" (list_sep_d expression) lst
   | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" expression ds expression ind
   | E_lambda {binder;input_type;output_type;result} ->
       fprintf ppf "lambda (%a:%a) : %a return %a"

src/stages/ast_simplified/combinators.ml

@@ -36,7 +36,7 @@ let t_key_hash     : type_expression = make_t @@ T_constant (TC_key_hash)
 let t_option  o    : type_expression = make_t @@ T_operator (TC_option o)
 let t_list  t      : type_expression = make_t @@ T_operator (TC_list t)
 let t_variable n   : type_expression = make_t @@ T_variable (Var.of_name n)
-let t_tuple lst    : type_expression = make_t @@ T_tuple lst
+let t_tuple lst    : type_expression = make_t @@ T_operator (TC_tuple lst)
 let t_pair (a , b) : type_expression = t_tuple [a ; b]
 let t_record_ez lst =
   let lst = List.map (fun (k, v) -> (Label k, v)) lst in
@@ -174,9 +174,10 @@ let e_ez_record ?loc (lst : (string * expr) list) : expression =
 let e_record ?loc map =
   let lst = Map.String.to_kv_list map in
   e_ez_record ?loc lst 
-let e_update ?loc record updates = 
+
-  let updates = List.map (fun (x,y) -> (Label x, y)) updates in
+let e_update ?loc record path expr = 
-  location_wrap ?loc @@ E_update {record; updates}
+  let update = (Label path, expr) in
+  location_wrap ?loc @@ E_update {record; update}
 
 let get_e_accessor = fun t ->
   match t with
@@ -205,7 +206,7 @@ let get_e_list = fun t ->
 let get_e_tuple = fun t ->
   match t with
   | E_tuple lst -> ok lst
-  | _ -> simple_fail "not a tuple"
+  | _ -> simple_fail "ast_simplified: get_e_tuple: not a tuple"
 
 let extract_pair : expression -> (expression * expression) result = fun e ->
   match e.expression with

src/stages/ast_simplified/combinators.mli

@@ -27,8 +27,8 @@ val t_option    : type_expression -> type_expression
 *)
 val t_list      : type_expression -> type_expression
 val t_variable  : string -> type_expression
-(*
 val t_tuple     : type_expression list -> type_expression
+(*
 val t_record    : te_map -> type_expression
 *)
 val t_pair : ( type_expression * type_expression ) -> type_expression
@@ -109,7 +109,7 @@ val e_typed_set : ?loc:Location.t -> expression list -> type_expression -> expre
 
 val e_lambda : ?loc:Location.t -> expression_variable -> type_expression option -> type_expression option -> expression -> expression
 val e_record : ?loc:Location.t -> expr Map.String.t -> expression
-val e_update : ?loc:Location.t -> expression -> (string * expression) list -> expression
+val e_update : ?loc:Location.t -> expression -> string -> expression -> expression
 
 val e_ez_record : ?loc:Location.t -> ( string * expr ) list -> expression
 (*

src/stages/ast_simplified/misc.ml

@@ -1,6 +1,8 @@
 open Trace
 open Types
 
+include Stage_common.Misc
+
 module Errors = struct
   let different_literals_because_different_types name a b () =
     let title () = "literals have different types: " ^ name in
@@ -133,14 +135,14 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
       simple_fail "comparing record with other expression"
   
   | E_update ura, E_update urb ->
-    let%bind lst =
+    let _ = 
-      generic_try (simple_error "updates with different number of fields")
+      generic_try (simple_error "Updating different record") @@ 
-      (fun () -> List.combine ura.updates urb.updates) in
+      fun () -> assert_value_eq (ura.record, urb.record) in
     let aux ((Label a,expra),(Label b, exprb))=
       assert (String.equal a b);
       assert_value_eq (expra,exprb)
     in
-    let%bind _all = bind_list @@ List.map aux lst in
+    let%bind _all = aux (ura.update, urb.update) in
     ok ()
   | E_update _, _ ->
      simple_fail "comparing record update with other expression"

src/stages/ast_simplified/misc.mli

@@ -1,5 +1,8 @@
 open Trace
 open Types
+
+include module type of Stage_common.Misc
+
 (*
 
 module Errors : sig

src/stages/ast_simplified/types.ml

@@ -67,6 +67,6 @@ and expression = {
   expression : expression' ;
   location : Location.t ;
 }
-and update = {record: expr; updates: (label*expr)list}
+and update = { record: expr; update: (label *expr) }
 
 and matching_expr = (expr,unit) matching

src/stages/ast_typed/PP.ml

@@ -15,12 +15,11 @@ and type_value ppf (tv:type_value) : unit =
 
 let rec annotated_expression ppf (ae:annotated_expression) : unit =
   match ae.type_annotation.simplified with
-  | Some _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
+  | _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
-  | _ -> fprintf ppf "@[<v>%a@]" expression ae.expression
 
 and lambda ppf l =
   let ({ binder ; body } : lambda) = l in
-  fprintf ppf "lambda (%a) -> %a"
+  fprintf ppf "(lambda (%a) -> %a)"
     name binder
     annotated_expression body
 
@@ -33,14 +32,14 @@ and option_inline ppf inline =
 and expression ppf (e:expression) : unit =
   match e with
   | E_literal l -> Stage_common.PP.literal ppf l
-  | E_constant (b, lst) -> fprintf ppf "%a(%a)" constant b (list_sep_d annotated_expression) lst
+  | E_constant (b, lst) -> fprintf ppf "(e_constant %a(%a))" constant b (list_sep_d annotated_expression) lst
-  | E_constructor (c, lst) -> fprintf ppf "%a(%a)" constructor c annotated_expression lst
+  | E_constructor (c, lst) -> fprintf ppf "(e_constructor %a(%a))" constructor c annotated_expression lst
-  | E_variable a -> fprintf ppf "%a" name a
+  | E_variable a -> fprintf ppf "(e_var %a)" name a
   | E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
   | E_lambda l -> fprintf ppf "%a" lambda l
   | E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
   | E_record_accessor (ae, l) -> fprintf ppf "%a.%a" annotated_expression ae label l
-  | E_record_update (ae, ups) -> fprintf ppf "%a with record[%a]" annotated_expression ae (lmap_sep annotated_expression (const " , ")) (LMap.of_list ups)
+  | E_record_update (ae, (path,expr)) -> fprintf ppf "%a with record[%a=%a]" annotated_expression ae Stage_common.PP.label path annotated_expression expr
   | E_tuple lst -> fprintf ppf "tuple[@;  @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) lst
   | E_record m -> fprintf ppf "record[%a]" (lmap_sep annotated_expression (const " , ")) m
   | E_map m -> fprintf ppf "map[@;  @[<v>%a@]@;]" (list_sep assoc_annotated_expression (tag ",@;")) m
@@ -50,7 +49,7 @@ and expression ppf (e:expression) : unit =
   | E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
   | E_matching (ae, m) ->
       fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
-  | E_sequence (a , b) -> fprintf ppf "%a ; %a" annotated_expression a annotated_expression b
+  | E_sequence (a , b) -> fprintf ppf "(e_seq %a ; %a)" annotated_expression a annotated_expression b
   | E_loop (expr , body) -> fprintf ppf "while %a { %a }" annotated_expression expr annotated_expression body
   | E_assign (name , path , expr) ->
     fprintf ppf "%a.%a := %a"

src/stages/ast_typed/combinators.ml

@@ -48,7 +48,7 @@ let t_mutez ?s ()      : type_value = make_t (T_constant TC_mutez) s
 let t_timestamp ?s ()  : type_value = make_t (T_constant TC_timestamp) s
 let t_unit ?s ()       : type_value = make_t (T_constant TC_unit) s
 let t_option o ?s ()   : type_value = make_t (T_operator (TC_option o)) s
-let t_tuple lst ?s ()  : type_value = make_t (T_tuple lst) s
+let t_tuple lst ?s ()  : type_value = make_t (T_operator (TC_tuple lst)) s
 let t_variable t ?s () : type_value = make_t (T_variable t) s
 let t_list t ?s ()     : type_value = make_t (T_operator (TC_list t)) s
 let t_set t ?s ()      : type_value = make_t (T_operator (TC_set t)) s
@@ -147,11 +147,11 @@ let get_t_key_hash (t:type_value) : unit result = match t.type_value' with
   | _ -> fail @@ Errors.not_a_x_type "key_hash" t ()
 
 let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
-  | T_tuple lst -> ok lst
+  | T_operator (TC_tuple lst) -> ok lst
   | _ -> fail @@ Errors.not_a_x_type "tuple" t ()
 
 let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_value' with
-  | T_tuple lst ->
+  | T_operator (TC_tuple lst) ->
       let%bind () =
         trace_strong (Errors.not_a_x_type "pair (tuple with two elements)" t ()) @@
         Assert.assert_list_size lst 2 in
@@ -160,6 +160,7 @@ let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_
 
 let get_t_function (t:type_value) : (type_value * type_value) result = match t.type_value' with
   | T_arrow (a,r) -> ok (a,r)
+  | T_operator (TC_arrow (a , b)) -> ok (a , b)
   | _ -> fail @@ Errors.not_a_x_type "function" t ()
 
 let get_t_sum (t:type_value) : type_value constructor_map result = match t.type_value' with
@@ -253,11 +254,11 @@ let ez_e_record (lst : (label * ae) list) : expression =
   let map = List.fold_left aux LMap.empty lst in
   e_record map
 let e_some s : expression = E_constant (C_SOME, [s])
-let e_none   : expression = E_constant (C_NONE, [])
+let e_none () : expression = E_constant (C_NONE, [])
 
 let e_map lst : expression = E_map lst
 
-let e_unit : expression = E_literal (Literal_unit)
+let e_unit () : expression = E_literal (Literal_unit)
 let e_int n : expression = E_literal (Literal_int n)
 let e_nat n : expression = E_literal (Literal_nat n)
 let e_mutez n : expression = E_literal (Literal_mutez n)
@@ -279,7 +280,7 @@ let e_list lst : expression = E_list lst
 let e_let_in binder inline rhs result = E_let_in { binder ; rhs ; result; inline }
 let e_tuple lst : expression = E_tuple lst
 
-let e_a_unit = make_a_e e_unit (t_unit ())
+let e_a_unit = make_a_e (e_unit ()) (t_unit ())
 let e_a_int n = make_a_e (e_int n) (t_int ())
 let e_a_nat n = make_a_e (e_nat n) (t_nat ())
 let e_a_mutez n = make_a_e (e_mutez n) (t_mutez ())
@@ -289,7 +290,7 @@ let e_a_address s = make_a_e (e_address s) (t_address ())
 let e_a_pair a b = make_a_e (e_pair a b) (t_pair a.type_annotation b.type_annotation ())
 let e_a_some s = make_a_e (e_some s) (t_option s.type_annotation ())
 let e_a_lambda l in_ty out_ty = make_a_e (e_lambda l) (t_function in_ty out_ty ())
-let e_a_none t = make_a_e e_none (t_option t ())
+let e_a_none t = make_a_e (e_none ()) (t_option t ())
 let e_a_tuple lst = make_a_e (E_tuple lst) (t_tuple (List.map get_type_annotation lst) ())
 let e_a_record r = make_a_e (e_record r) (t_record (LMap.map get_type_annotation r) ())
 let e_a_application a b = make_a_e (e_application a b) (get_type_annotation b)

src/stages/ast_typed/combinators.mli

@@ -111,9 +111,9 @@ val ez_e_record : ( string * annotated_expression ) list -> expression
 
 *)
 val e_some : value -> expression
-val e_none : expression
+val e_none : unit -> expression
 val e_map : ( value * value ) list -> expression
-val e_unit : expression
+val e_unit : unit -> expression
 val e_int : int -> expression
 val e_nat : int -> expression
 val e_mutez : int -> expression

src/stages/ast_typed/misc.ml

@@ -1,5 +1,6 @@
 open Trace
 open Types
+
 include Stage_common.Misc
 
 module Errors = struct
@@ -29,6 +30,21 @@ module Errors = struct
     ] in
     error ~data title message ()
 
+  let different_operator_number_of_arguments opa opb lena lenb () =
+    let title = (thunk "different number of arguments to type constructors") in
+    assert (String.equal (type_operator_name opa) (type_operator_name opb));
+    let message () = Format.asprintf
+                       "Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the %s type constructor, but they have %d and %d arguments, respectively)"
+                       (type_operator_name opa) lena lenb in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opa) ;
+      ("b" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opb) ;
+      ("op" , fun () -> type_operator_name opa) ;
+      ("len_a" , fun () -> Format.asprintf "%d" lena) ;
+      ("len_b" , fun () -> Format.asprintf "%d" lenb) ;
+    ] in
+    error ~data title message ()
+
   let different_size_type name a b () =
     let title () = name ^ " have different sizes" in
     let message () = "Expected these two types to be the same, but they're different (both are " ^ name ^ ", but with a different number of arguments)" in
@@ -49,8 +65,6 @@ module Errors = struct
 
   let _different_size_constants = different_size_type "type constructors"
 
-  let different_size_tuples = different_size_type "tuples"
-
   let different_size_sums = different_size_type "sums"
 
   let different_size_records = different_size_type "records"
@@ -179,7 +193,7 @@ module Free_variables = struct
     | E_constructor (_ , a) -> self a
     | E_record m -> unions @@ List.map self @@ LMap.to_list m
     | E_record_accessor (a, _) -> self a
-    | E_record_update (r,ups) -> union (self r) @@ unions @@ List.map (fun (_,e) -> self e) ups
+    | E_record_update (r,(_,e)) -> union (self r) @@ self e
     | E_tuple_accessor (a, _) -> self a
     | E_list lst -> unions @@ List.map self lst
     | E_set lst -> unions @@ List.map self lst
@@ -301,13 +315,6 @@ open Errors
 
        
 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 (fun () -> (different_size_tuples a b ()))
-        @@ Assert.assert_true List.(length ta = length tb) in
-      bind_list_iter assert_type_value_eq (List.combine ta tb)
-    )
-  | T_tuple _, _ -> fail @@ different_kinds a b
   | T_constant ca, T_constant cb -> (
       trace_strong (different_constants ca cb)
       @@ Assert.assert_true (ca = cb)
@@ -321,10 +328,16 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       | TC_set la, TC_set lb -> ok @@ ([la], [lb])
       | TC_map (ka,va), TC_map (kb,vb)
       | TC_big_map (ka,va), TC_big_map (kb,vb) -> ok @@ ([ka;va] ,[kb;vb]) 
-      | _,_ -> fail @@ different_operators opa opb
+      | TC_tuple lsta, TC_tuple lstb -> ok @@ (lsta , lstb) 
+      | TC_arrow (froma , toa) , TC_arrow (fromb , tob) -> ok @@ ([froma;toa] , [fromb;tob]) 
+      | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _),
+        (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _) -> fail @@ different_operators opa opb
       in
-    trace (different_types "arguments to type operators" a b)
+      if List.length lsta <> List.length lstb then
-      @@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb)
+        fail @@ different_operator_number_of_arguments opa opb (List.length lsta) (List.length lstb)
+      else
+        trace (different_types "arguments to type operators" a b)
+        @@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb)
   )
   | T_operator _, _ -> fail @@ different_kinds a b
   | T_sum sa, T_sum sb -> (

src/stages/ast_typed/misc.mli

@@ -1,6 +1,8 @@
 open Trace
 open Types
 
+include module type of Stage_common.Misc
+
 val assert_value_eq : ( value * value ) -> unit result
 
 val assert_type_value_eq : ( type_value * type_value ) -> unit result
@@ -43,7 +45,6 @@ module Errors : sig
   val different_size_type : name -> type_value -> type_value -> unit -> error
   val different_props_in_record : string -> string -> unit -> error
   val different_size_constants : type_value -> type_value -> unit -> error
-  val different_size_tuples : type_value -> type_value -> unit -> error
   val different_size_sums : type_value -> type_value -> unit -> error
   val different_size_records : type_value -> type_value -> unit -> error
   val different_types : name -> type_value -> type_value -> unit -> error

src/stages/ast_typed/misc_smart.ml

@@ -72,14 +72,10 @@ module Captured_variables = struct
       let%bind lst' = bind_map_list self @@ LMap.to_list m in
       ok @@ unions lst'
     | E_record_accessor (a, _) -> self a
-    | E_record_update (r,ups) -> 
+    | E_record_update (r,(_,e)) -> 
       let%bind r = self r in
-      let aux (_, e) =
+      let%bind e = self e in
-        let%bind e = self e in
+      ok @@ union r e
-        ok e
-      in
-      let%bind lst = bind_map_list aux ups in
-      ok @@ union r @@ unions lst
     | E_tuple_accessor (a, _) -> self a
     | E_list lst ->
       let%bind lst' = bind_map_list self lst in

src/stages/ast_typed/types.ml

@@ -34,6 +34,12 @@ and annotated_expression = {
   location : Location.t ;
 }
 
+(* This seems to be used only for top-level declarations, and
+   represents the name of the top-level binding, and the expression
+   assigned to it. -- Suzanne.
+
+   TODO: if this is correct, then we should inline this in
+   "declaration" or at least move it close to it. *)
 and named_expression = {
   name: expression_variable ;
   annotated_expression: ae ;
@@ -41,6 +47,7 @@ and named_expression = {
 
 and ae = annotated_expression
 and type_value' = type_value type_expression'
+
 and type_value = {
   type_value' : type_value';
   simplified : S.type_expression option ; (* If we have the simplified this AST fragment comes from, it is stored here, for easier untyping. *)
@@ -77,7 +84,7 @@ and 'a expression' =
   | E_application of (('a) * ('a))
   | E_lambda of lambda
   | E_let_in of let_in
-  (* Tuple *)
+  (* Tuple, TODO: remove tuples and use records with integer keys instead *)
   | E_tuple of ('a) list
   | E_tuple_accessor of (('a) * int) (* Access n'th tuple's element *)
   (* Sum *)
@@ -85,7 +92,7 @@ and 'a expression' =
   (* Record *)
   | E_record of ('a) label_map
   | E_record_accessor of (('a) * label)
-  | E_record_update of ('a * (label* 'a) list)
+  | E_record_update of ('a * (label * 'a))
   (* Data Structures *)
   | E_map of (('a) * ('a)) list
   | E_big_map of (('a) * ('a)) list

src/stages/common/PP.ml

@@ -141,7 +141,6 @@ let lmap_sep_d x = lmap_sep x (const " , ")
 let rec type_expression' : type a . (formatter -> a -> unit) -> formatter -> a type_expression' -> unit =
   fun f ppf te ->
   match te with
-    | T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d f) lst
     | T_sum m -> fprintf ppf "sum[%a]" (cmap_sep_d f) m
     | T_record m -> fprintf ppf "record[%a]" (lmap_sep_d f ) m
     | T_arrow (a, b) -> fprintf ppf "%a -> %a" f a f b
@@ -178,6 +177,8 @@ and type_operator : type a . (formatter -> a -> unit) -> formatter -> a type_ope
     | TC_map    (k, v) -> Format.asprintf "Map (%a,%a)" f k f v
     | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v
     | TC_contract (c) -> Format.asprintf "Contract (%a)" f c
+    | TC_arrow (a , b) -> Format.asprintf "TC_Arrow (%a,%a)" f a f b
+    | TC_tuple lst -> Format.asprintf "tuple[%a]" (list_sep_d f) lst
     in
   fprintf ppf "(TO_%s)" s
 

src/stages/common/PP.mli

@@ -13,3 +13,4 @@ val type_expression' : (formatter -> 'a -> unit) -> formatter -> 'a type_express
 val type_operator    : (formatter -> 'a -> unit) -> formatter -> 'a type_operator -> unit
 val type_constant    : formatter -> type_constant -> unit
 val literal          : formatter -> literal -> unit
+val list_sep_d       : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit

src/stages/common/misc.ml

@@ -7,7 +7,9 @@ let map_type_operator f = function
   | TC_list x -> TC_list (f x)
   | TC_set x -> TC_set (f x)
   | TC_map (x , y) -> TC_map (f x , f y)
-  | TC_big_map (x , y)-> TC_big_map (f x , f y)
+  | TC_big_map (x , y) -> TC_big_map (f x , f y)
+  | TC_arrow (x , y) -> TC_arrow (f x , f y)
+  | TC_tuple lst -> TC_tuple (List.map f lst)
 
 let bind_map_type_operator f = function
     TC_contract x -> let%bind x = f x in ok @@ TC_contract x
@@ -15,7 +17,9 @@ let bind_map_type_operator f = function
   | TC_list x -> let%bind x = f x in ok @@ TC_list x
   | TC_set x -> let%bind x = f x in ok @@ TC_set x
   | TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y)
-  | TC_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y)
+  | TC_big_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y)
+  | TC_arrow (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_arrow (x , y)
+  | TC_tuple lst -> let%bind lst = bind_map_list f lst in ok @@ TC_tuple lst
 
 let type_operator_name = function
       TC_contract _ -> "TC_contract"
@@ -24,6 +28,8 @@ let type_operator_name = function
     | TC_set      _ -> "TC_set"
     | TC_map      _ -> "TC_map"
     | TC_big_map  _ -> "TC_big_map"
+    | TC_arrow    _ -> "TC_arrow"
+    | TC_tuple    _ -> "TC_tuple"
 
 let type_expression'_of_string = function
   | "TC_contract" , [x]     -> ok @@ T_operator(TC_contract x)
@@ -61,6 +67,8 @@ let string_of_type_operator = function
   | TC_set       x       -> "TC_set"      , [x]
   | TC_map       (x , y) -> "TC_map"      , [x ; y]
   | TC_big_map   (x , y) -> "TC_big_map"  , [x ; y]
+  | TC_arrow     (x , y) -> "TC_arrow"    , [x ; y]
+  | TC_tuple     lst     -> "TC_tuple"    , lst
 
 let string_of_type_constant = function
   | TC_unit      -> "TC_unit", []
@@ -81,5 +89,6 @@ let string_of_type_constant = function
 let string_of_type_expression' = function
   | T_operator o -> string_of_type_operator o
   | T_constant c -> string_of_type_constant c
-  | T_tuple _|T_sum _|T_record _|T_arrow (_, _)|T_variable _ ->
+  | T_sum _|T_record _|T_arrow (_, _)|T_variable _ ->
      failwith "not a type operator or constant"
+

src/stages/common/misc.mli

@@ -0,0 +1,9 @@
+open Types
+
+val map_type_operator : ('a -> 'b) -> 'a type_operator -> 'b type_operator
+val bind_map_type_operator : ('a -> ('b * 'c list, 'd) Pervasives.result) -> 'a type_operator -> ('b type_operator * 'c list, 'd) Pervasives.result
+val type_operator_name : 'a type_operator -> string
+val type_expression'_of_string : string * 'a list -> ('a type_expression' * 'b list, 'c) Pervasives.result
+val string_of_type_operator : 'a type_operator -> string * 'a list
+val string_of_type_constant : type_constant -> string * 'a list
+val string_of_type_expression' : 'a type_expression' -> string * 'a list

src/stages/common/types.ml

@@ -66,7 +66,6 @@ and literal =
 
 (* The ast is a tree of node, 'a is the type of the node (type_variable or {type_variable, previous_type}) *)
 type 'a type_expression' = 
-  | T_tuple of 'a list 
   | T_sum of 'a constructor_map
   | T_record of 'a label_map
   | T_arrow of 'a * 'a
@@ -96,6 +95,8 @@ and 'a type_operator =
   | TC_set of 'a
   | TC_map of 'a * 'a
   | TC_big_map of 'a * 'a
+  | TC_arrow of 'a * 'a
+  | TC_tuple of 'a list
 
 type type_base =
   | Base_unit 

src/stages/mini_c/PP.ml

@@ -99,8 +99,8 @@ and expression' ppf (e:expression') = match e with
       fprintf ppf "fold %a on %a with %a do ( %a )" expression collection expression initial Stage_common.PP.name name expression body
   | E_assignment (r , path , e) ->
       fprintf ppf "%a.%a := %a" Stage_common.PP.name r (list_sep lr (const ".")) path expression e
-  | E_update (r, updates) ->
+  | E_update (r, (path,e)) ->
-      fprintf ppf "%a with {%a}" expression r (list_sep_d (fun ppf (path, e) -> fprintf ppf "%a = %a" (list_sep lr (const ".")) path expression e)) updates
+      fprintf ppf "%a with {%a=%a}" expression r (list_sep lr (const ".")) path expression e
   | E_while (e , b) ->
       fprintf ppf "while (%a) %a" expression e expression b
 

src/stages/mini_c/misc.ml

@@ -81,7 +81,7 @@ module Free_variables = struct
     | E_sequence (x, y) -> union (self x) (self y)
     (* NB different from ast_typed... *)
     | E_assignment (v, _, e) -> unions [ var_name b v ; self e ]
-    | E_update (e, updates) -> union (self e) (unions @@ List.map (fun (_,e) -> self e) updates)
+    | E_update (r, (_,e)) -> union (self r) (self e)
     | E_while (cond , body) -> union (self cond) (self body)
 
   and var_name : bindings -> var_name -> bindings = fun b n ->

src/stages/mini_c/types.ml

@@ -73,7 +73,7 @@ and expression' =
   | E_let_in of ((var_name * type_value) * inline * expression * expression)
   | E_sequence of (expression * expression)
   | E_assignment of (expression_variable * [`Left | `Right] list * expression)
-  | E_update of (expression * ([`Left | `Right] list * expression) list)
+  | E_update of (expression * ([`Left | `Right] list * expression))
   | E_while of (expression * expression)
 
 and expression = {

src/stages/typesystem/misc.ml

@@ -3,120 +3,122 @@ open Core
 let pair_map = fun f (x , y) -> (f x , f y)
 
 module Substitution = struct
-
   module Pattern = struct
 
     open Trace
     module T = Ast_typed
     (* module TSMap = Trace.TMap(String) *)
 
-    type 'a w = 'a -> 'a result
+    type substs = variable:type_variable -> T.type_value' option (* this string is a type_name or type_variable I think *)
+    let mk_substs ~v ~expr = (v , expr)
+
+    type 'a w = substs:substs -> 'a -> 'a result
 
     let rec rec_yes = true
-    and s_environment_element_definition ~v ~expr = function
+    and s_environment_element_definition ~substs = function
       | T.ED_binder -> ok @@ T.ED_binder
       | T.ED_declaration (val_, free_variables) ->
-        let%bind val_ = s_annotated_expression ~v ~expr  val_ in
+        let%bind val_ = s_annotated_expression ~substs  val_ in
-        let%bind free_variables = bind_map_list (s_variable ~v ~expr) free_variables in
+        let%bind free_variables = bind_map_list (s_variable ~substs) free_variables in
         ok @@ T.ED_declaration (val_, free_variables)
-    and s_environment ~v ~expr : T.environment w = fun env ->
+    and s_environment : T.environment w = fun ~substs env ->
       bind_map_list (fun (variable, T.{ type_value; source_environment; definition }) ->
-          let%bind variable = s_variable ~v ~expr variable in
+          let%bind variable = s_variable ~substs variable in
-          let%bind type_value = s_type_value ~v ~expr type_value in
+          let%bind type_value = s_type_value ~substs type_value in
-          let%bind source_environment = s_full_environment ~v ~expr source_environment in
+          let%bind source_environment = s_full_environment ~substs source_environment in
-          let%bind definition = s_environment_element_definition ~v ~expr definition in
+          let%bind definition = s_environment_element_definition ~substs definition in
           ok @@ (variable, T.{ type_value; source_environment; definition })) env
-    and s_type_environment ~v ~expr : T.type_environment w = fun tenv ->
+    and s_type_environment : T.type_environment w = fun ~substs tenv ->
       bind_map_list (fun (type_variable , type_value) ->
-        let%bind type_variable = s_type_variable ~v ~expr type_variable in
+        let%bind type_variable = s_type_variable ~substs type_variable in
-        let%bind type_value = s_type_value ~v ~expr type_value in
+        let%bind type_value = s_type_value ~substs type_value in
         ok @@ (type_variable , type_value)) tenv
-    and s_small_environment ~v ~expr : T.small_environment w = fun (environment, type_environment) ->
+    and s_small_environment : T.small_environment w = fun ~substs (environment, type_environment) ->
-      let%bind environment = s_environment ~v ~expr environment in
+      let%bind environment = s_environment ~substs environment in
-      let%bind type_environment = s_type_environment ~v ~expr type_environment in
+      let%bind type_environment = s_type_environment ~substs type_environment in
       ok @@ (environment, type_environment)
-    and s_full_environment ~v ~expr : T.full_environment w = fun (a , b) ->
+    and s_full_environment : T.full_environment w = fun ~substs (a , b) ->
-      let%bind a = s_small_environment ~v ~expr a in
+      let%bind a = s_small_environment ~substs a in
-      let%bind b = bind_map_list (s_small_environment ~v ~expr) b in
+      let%bind b = bind_map_list (s_small_environment ~substs) b in
       ok (a , b)
 
-    and s_variable ~v ~expr : T.expression_variable w = fun var ->
+    and s_variable : T.expression_variable w = fun ~substs var ->
-      let () = ignore (v, expr) in
+      let () = ignore @@ substs in
       ok var
 
-    and s_type_variable ~v ~expr : T.type_variable w = fun tvar ->
+    and s_type_variable : T.type_variable w = fun ~substs tvar ->
-      let _TODO = ignore (v, expr) in
+      let _TODO = ignore @@ substs in
       Printf.printf "TODO: subst: unimplemented case s_type_variable";
       ok @@ tvar
       (* if String.equal tvar v then
        *   expr
        * else
        *   ok tvar *)
-    and s_label ~v ~expr : T.label w = fun l ->
+    and s_label : T.label w = fun ~substs l ->
-      let () = ignore (v, expr) in
+      let () = ignore @@ substs in
       ok l
     
-    and s_build_in ~v ~expr : T.constant w = fun b ->
+    and s_build_in : T.constant w = fun ~substs b ->
-      let () = ignore (v, expr) in
+      let () = ignore @@ substs in
       ok b
 
-    and s_constructor ~v ~expr : T.constructor w = fun c ->
+    and s_constructor : T.constructor w = fun ~substs c ->
-      let () = ignore (v, expr) in
+      let () = ignore @@ substs in
       ok c
 
-    and s_type_name_constant ~v ~expr : T.type_constant w = fun type_name ->
+    and s_type_name_constant : T.type_constant w = fun ~substs type_name ->
       (* TODO: we don't need to subst anything, right? *)
-      let () = ignore (v , expr) in
+      let () = ignore @@ substs in
       ok @@ type_name
 
-    and s_type_value' ~v ~expr : T.type_value' w = function
+    and s_type_value' : T.type_value' w = fun ~substs -> function
-        | T.T_tuple type_value_list ->
+        | T.T_operator (TC_tuple type_value_list) ->
-          let%bind type_value_list = bind_map_list (s_type_value ~v ~expr) type_value_list in
+          let%bind type_value_list = bind_map_list (s_type_value ~substs) type_value_list in
-          ok @@ T.T_tuple type_value_list
+          ok @@ T.T_operator (TC_tuple type_value_list)
         | T.T_sum _ -> failwith "TODO: T_sum"
         | T.T_record _ -> failwith "TODO: T_record"
-        | T.T_constant (type_name) ->
+        | T.T_constant type_name ->
-          let%bind type_name = s_type_name_constant ~v ~expr type_name in
+          let%bind type_name = s_type_name_constant ~substs type_name in
           ok @@ T.T_constant (type_name)
         | T.T_variable variable ->
-           if Var.equal variable v
+           begin
-           then ok @@ expr
+             match substs ~variable with
-           else ok @@ T.T_variable variable
+             | Some expr -> s_type_value' ~substs expr (* TODO: is it the right thing to recursively examine this? We mustn't go into an infinite loop. *)
-        | T.T_operator (type_name_and_args) ->
+             | None -> ok @@ T.T_variable variable
-          let bind_map_type_operator = Stage_common.Misc.bind_map_type_operator in (* TODO: write T.Misc.bind_map_type_operator, but it doesn't work *)
+           end
-          let%bind type_name_and_args = bind_map_type_operator (s_type_value ~v ~expr) type_name_and_args in
+        | T.T_operator type_name_and_args ->
+          let%bind type_name_and_args = T.Misc.bind_map_type_operator (s_type_value ~substs) type_name_and_args in
           ok @@ T.T_operator type_name_and_args
         | T.T_arrow _ ->
-          let _TODO = (v, expr) in
+          let _TODO = substs in
           failwith "TODO: T_function"
 
-    and s_type_expression' ~v ~expr : _ Ast_simplified.type_expression' w = fun type_expression' ->
+    and s_type_expression' : _ Ast_simplified.type_expression' w = fun ~substs -> function
-      match type_expression' with
+      | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum"
-        | Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression tuple"
+      | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record"
-        | Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum"
+      | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow"
-        | Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record"
+      | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable"
-        | Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow"
+      | Ast_simplified.T_operator op ->
-        | Ast_simplified.T_variable _ -> failwith "TODO: subst: unimplemented case s_type_expression variable"
+         let%bind op =
-        | Ast_simplified.T_operator op ->
+           Ast_simplified.Misc.bind_map_type_operator
-           let%bind op =
+             (s_type_expression ~substs)
-             Stage_common.Misc.bind_map_type_operator (* TODO: write Ast_simplified.Misc.type_operator_name *)
+             op in
-               (s_type_expression ~v ~expr)
+         (* TODO: when we have generalized operators, we might need to subst the operator name itself? *)
-               op in
+         ok @@ Ast_simplified.T_operator op
-           ok @@ Ast_simplified.T_operator op
+      | Ast_simplified.T_constant constant ->
-        | Ast_simplified.T_constant constant ->
+         ok @@ Ast_simplified.T_constant constant
-           ok @@ Ast_simplified.T_constant constant
 
-    and s_type_expression ~v ~expr : Ast_simplified.type_expression w = fun {type_expression'} ->
+    and s_type_expression : Ast_simplified.type_expression w = fun ~substs {type_expression'} ->
-      let%bind type_expression' = s_type_expression' ~v ~expr type_expression' in
+      let%bind type_expression' = s_type_expression' ~substs type_expression' in
       ok @@ Ast_simplified.{type_expression'}
 
-    and s_type_value ~v ~expr : T.type_value w = fun { type_value'; simplified } ->
+    and s_type_value : T.type_value w = fun ~substs { type_value'; simplified } ->
-      let%bind type_value' = s_type_value' ~v ~expr type_value' in
+      let%bind type_value' = s_type_value' ~substs type_value' in
-      let%bind simplified = bind_map_option (s_type_expression ~v ~expr) simplified in
+      let%bind simplified = bind_map_option (s_type_expression ~substs) simplified in
       ok @@ T.{ type_value'; simplified }
-    and s_literal ~v ~expr : T.literal w = function
+    and s_literal : T.literal w = fun ~substs -> function
       | T.Literal_unit ->
-        let () = ignore (v, expr) in
+        let () = ignore @@ substs in
         ok @@ T.Literal_unit
       | (T.Literal_bool _ as x)
       | (T.Literal_int _ as x)
@@ -132,144 +134,145 @@ module Substitution = struct
       | (T.Literal_chain_id _ as x)
       | (T.Literal_operation _ as x) ->
         ok @@ x
-    and s_matching_expr ~v ~expr : T.matching_expr w = fun _ ->
+    and s_matching_expr : T.matching_expr w = fun ~substs _ ->
-      let _TODO = v, expr in
+      let _TODO = substs in
       failwith "TODO: subst: unimplemented case s_matching"
-    and s_named_type_value ~v ~expr : T.named_type_value w = fun _ ->
+    and s_named_type_value : T.named_type_value w = fun ~substs _ ->
-      let _TODO = v, expr in
+      let _TODO = substs in
       failwith "TODO: subst: unimplemented case s_named_type_value"
-    and s_access_path  ~v ~expr : T.access_path w = fun _ ->
+    and s_access_path  : T.access_path w = fun ~substs _ ->
-      let _TODO = v, expr in
+      let _TODO = substs in
       failwith "TODO: subst: unimplemented case s_access_path"
 
-    and s_expression ~v ~expr : T.expression w = function
+    and s_expression : T.expression w = fun ~(substs : substs) -> function
       | T.E_literal         x ->
-        let%bind x = s_literal ~v ~expr x in
+        let%bind x = s_literal ~substs x in
         ok @@ T.E_literal x
       | T.E_constant        (var, vals) ->
-        let%bind var = s_build_in ~v ~expr var in
+        let%bind var = s_build_in ~substs var in
-        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
         ok @@ T.E_constant (var, vals)
       | T.E_variable        tv ->
-        let%bind tv = s_variable ~v ~expr tv in
+        let%bind tv = s_variable ~substs tv in
         ok @@ T.E_variable tv
       | T.E_application     (val1 , val2) ->
-        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val1 = s_annotated_expression ~substs val1 in
-        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        let%bind val2 = s_annotated_expression ~substs val2 in
         ok @@ T.E_application (val1 , val2)
       | T.E_lambda          { binder; body } ->
-        let%bind binder = s_variable ~v ~expr binder in
+        let%bind binder = s_variable ~substs binder in
-        let%bind body = s_annotated_expression ~v ~expr body in
+        let%bind body = s_annotated_expression ~substs body in
         ok @@ T.E_lambda { binder; body }
       | T.E_let_in          { binder; rhs; result; inline } ->
-        let%bind binder = s_variable ~v ~expr binder in
+        let%bind binder = s_variable ~substs binder in
-        let%bind rhs = s_annotated_expression ~v ~expr rhs in
+        let%bind rhs = s_annotated_expression ~substs rhs in
-        let%bind result = s_annotated_expression ~v ~expr result in
+        let%bind result = s_annotated_expression ~substs result in
         ok @@ T.E_let_in { binder; rhs; result; inline }
       | T.E_tuple           vals ->
-        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
         ok @@ T.E_tuple vals
       | T.E_tuple_accessor  (val_, i) ->
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind val_ = s_annotated_expression ~substs val_ in
         let i = i in
         ok @@ T.E_tuple_accessor (val_, i)
       | T.E_constructor     (tvar, val_) ->
-        let%bind tvar = s_constructor ~v ~expr tvar in
+        let%bind tvar = s_constructor ~substs tvar in
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind val_ = s_annotated_expression ~substs val_ in
         ok @@ T.E_constructor (tvar, val_)
       | T.E_record          aemap ->
         let _TODO = aemap in
         failwith "TODO: subst in record"
         (* let%bind aemap = TSMap.bind_map_Map (fun ~k:key ~v:val_ ->
-         *     let key = s_type_variable ~v ~expr key in
+         *     let key = s_type_variable ~substs key in
-         *     let val_ = s_annotated_expression ~v ~expr val_ in
+         *     let val_ = s_annotated_expression ~substs val_ in
          *     ok @@ (key , val_)) aemap in
          * ok @@ T.E_record aemap *)
       | T.E_record_accessor (val_, l) ->
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind val_ = s_annotated_expression ~substs val_ in
-        let%bind l = s_label ~v ~expr l in
+        let l = l in            (* Nothing to substitute, this is a label, not a type *)
         ok @@ T.E_record_accessor (val_, l)
-      | T.E_record_update (r, ups) ->
+      | T.E_record_update (r, (l, e)) ->
-        let%bind r = s_annotated_expression ~v ~expr r in
+        let%bind r = s_annotated_expression ~substs r in
-        let%bind ups = bind_map_list (fun (l,e) -> let%bind e = s_annotated_expression ~v ~expr e in ok (l,e)) ups in
+        let%bind e = s_annotated_expression ~substs e in
-        ok @@ T.E_record_update (r,ups)
+        ok @@ T.E_record_update (r, (l, e))
       | T.E_map             val_val_list ->
         let%bind val_val_list = bind_map_list (fun (val1 , val2) ->
-            let%bind val1 = s_annotated_expression ~v ~expr val1 in
+            let%bind val1 = s_annotated_expression ~substs val1 in
-            let%bind val2 = s_annotated_expression ~v ~expr val2 in
+            let%bind val2 = s_annotated_expression ~substs val2 in
             ok @@ (val1 , val2)
           ) val_val_list in
         ok @@ T.E_map val_val_list
       | T.E_big_map         val_val_list ->
         let%bind val_val_list = bind_map_list (fun (val1 , val2) ->
-            let%bind val1 = s_annotated_expression ~v ~expr val1 in
+            let%bind val1 = s_annotated_expression ~substs val1 in
-            let%bind val2 = s_annotated_expression ~v ~expr val2 in
+            let%bind val2 = s_annotated_expression ~substs val2 in
             ok @@ (val1 , val2)
           ) val_val_list in
         ok @@ T.E_big_map val_val_list
       | T.E_list            vals ->
-        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
         ok @@ T.E_list vals
       | T.E_set             vals ->
-        let%bind vals = bind_map_list (s_annotated_expression ~v ~expr) vals in
+        let%bind vals = bind_map_list (s_annotated_expression ~substs) vals in
         ok @@ T.E_set vals
       | T.E_look_up         (val1, val2) ->
-        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val1 = s_annotated_expression ~substs val1 in
-        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        let%bind val2 = s_annotated_expression ~substs val2 in
         ok @@ T.E_look_up (val1 , val2)
       | T.E_matching         (val_ , matching_expr) ->
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind val_ = s_annotated_expression ~substs val_ in
-        let%bind matching = s_matching_expr ~v ~expr matching_expr in
+        let%bind matching = s_matching_expr ~substs matching_expr in
         ok @@ T.E_matching (val_ , matching)
       | T.E_sequence        (val1, val2) ->
-        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val1 = s_annotated_expression ~substs val1 in
-        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        let%bind val2 = s_annotated_expression ~substs val2 in
         ok @@ T.E_sequence (val1 , val2)
       | T.E_loop            (val1, val2) ->
-        let%bind val1 = s_annotated_expression ~v ~expr val1 in
+        let%bind val1 = s_annotated_expression ~substs val1 in
-        let%bind val2 = s_annotated_expression ~v ~expr val2 in
+        let%bind val2 = s_annotated_expression ~substs val2 in
         ok @@ T.E_loop (val1 , val2)
       | T.E_assign          (named_tval, access_path, val_) ->
-        let%bind named_tval = s_named_type_value ~v ~expr named_tval in
+        let%bind named_tval = s_named_type_value ~substs named_tval in
-        let%bind access_path = s_access_path ~v ~expr access_path in
+        let%bind access_path = s_access_path ~substs access_path in
-        let%bind val_ = s_annotated_expression ~v ~expr val_ in
+        let%bind val_ = s_annotated_expression ~substs val_ in
         ok @@ T.E_assign (named_tval, access_path, val_)
 
-    and s_annotated_expression ~v ~expr : T.annotated_expression w = fun { expression; type_annotation; environment; location } ->
+    and s_annotated_expression : T.annotated_expression w = fun ~substs { expression; type_annotation; environment; location } ->
-      let%bind expression = s_expression ~v ~expr expression in
+      let%bind expression = s_expression ~substs expression in
-      let%bind type_annotation = s_type_value ~v ~expr type_annotation in
+      let%bind type_annotation = s_type_value ~substs type_annotation in
-      let%bind environment = s_full_environment ~v ~expr environment in
+      let%bind environment = s_full_environment ~substs environment in
       let location = location in
       ok T.{ expression; type_annotation; environment; location }
 
-    and s_named_expression ~v ~expr : T.named_expression w = fun { name; annotated_expression } ->
+    and s_named_expression : T.named_expression w = fun ~substs { name; annotated_expression } ->
-      let%bind name = s_variable ~v ~expr name in
+      let name = name in (* Nothing to substitute, this is a variable name *)
-      let%bind annotated_expression = s_annotated_expression ~v ~expr annotated_expression in
+      let%bind annotated_expression = s_annotated_expression ~substs annotated_expression in
       ok T.{ name; annotated_expression }
 
-    and s_declaration ~v ~expr : T.declaration w =
+    and s_declaration : T.declaration w = fun ~substs ->
       function
-        Ast_typed.Declaration_constant (e, i, (env1, env2)) ->
+        Ast_typed.Declaration_constant (e, inline, (env1, env2)) ->
-        let%bind e = s_named_expression ~v ~expr e in
+        let%bind e = s_named_expression ~substs e in
-        let%bind env1 = s_full_environment ~v ~expr env1 in
+        let%bind env1 = s_full_environment ~substs env1 in
-        let%bind env2 = s_full_environment ~v ~expr env2 in
+        let%bind env2 = s_full_environment ~substs env2 in
-        ok @@ Ast_typed.Declaration_constant (e, i, (env1, env2))
+        ok @@ Ast_typed.Declaration_constant (e, inline, (env1, env2))
 
-    and s_declaration_wrap ~v ~expr : T.declaration Location.wrap w = fun d ->
+    and s_declaration_wrap : T.declaration Location.wrap w = fun ~substs d ->
-      Trace.bind_map_location (s_declaration ~v ~expr) d
+      Trace.bind_map_location (s_declaration ~substs) d
 
     (* Replace the type variable ~v with ~expr everywhere within the
        program ~p. TODO: issues with scoping/shadowing. *)
-    and program ~(p : Ast_typed.program) ~(v:type_variable) ~expr : Ast_typed.program Trace.result =
+    and s_program : Ast_typed.program w = fun ~substs p ->
-      Trace.bind_map_list (s_declaration_wrap ~v ~expr) p
+      Trace.bind_map_list (s_declaration_wrap ~substs) p
 
     (*
        Computes `P[v := expr]`.
     *)
-    and type_value ~tv ~v ~expr =
+    and type_value ~tv ~substs =
-      let self tv = type_value ~tv ~v ~expr in
+      let self tv = type_value ~tv ~substs in
+      let (v, expr) = substs in
       match tv with
-      | P_variable v' when v' = v -> expr
+      | P_variable v' when Var.equal v' v -> expr
       | P_variable _ -> tv
       | P_constant (x , lst) -> (
           let lst' = List.map self lst in
@@ -280,7 +283,7 @@ module Substitution = struct
           P_apply ab'
         )
       | P_forall p -> (
-          let aux c = constraint_ ~c ~v ~expr in
+          let aux c = constraint_ ~c ~substs in
           let constraints = List.map aux p.constraints in
           if (p.binder = v) then (
             P_forall { p with constraints }
@@ -290,31 +293,33 @@ module Substitution = struct
           )
         )
 
-    and constraint_ ~c ~v ~expr =
+    and constraint_ ~c ~substs =
       match c with
       | C_equation ab -> (
-          let ab' = pair_map (fun tv -> type_value ~tv ~v ~expr) ab in
+          let ab' = pair_map (fun tv -> type_value ~tv ~substs) ab in
           C_equation ab'
         )
       | C_typeclass (tvs , tc) -> (
-          let tvs' = List.map (fun tv -> type_value ~tv ~v ~expr) tvs in
+          let tvs' = List.map (fun tv -> type_value ~tv ~substs) tvs in
-          let tc' = typeclass ~tc ~v ~expr in
+          let tc' = typeclass ~tc ~substs in
           C_typeclass (tvs' , tc')
         )
       | C_access_label (tv , l , v') -> (
-          let tv' = type_value ~tv ~v ~expr in
+          let tv' = type_value ~tv ~substs in
           C_access_label (tv' , l , v')
         )
 
-    and typeclass ~tc ~v ~expr =
+    and typeclass ~tc ~substs =
-      List.map (List.map (fun tv -> type_value ~tv ~v ~expr)) tc
+      List.map (List.map (fun tv -> type_value ~tv ~substs)) tc
+
+    let program = s_program
 
     (* Performs beta-reduction at the root of the type *)
     let eval_beta_root ~(tv : type_value) =
       match tv with
         P_apply (P_forall { binder; constraints; body }, arg) ->
-        let constraints = List.map (fun c -> constraint_ ~c ~v:binder ~expr:arg) constraints in
+        let constraints = List.map (fun c -> constraint_ ~c ~substs:(mk_substs ~v:binder ~expr:arg)) constraints in
-        (type_value ~tv:body ~v:binder ~expr:arg , constraints)
+        (type_value ~tv:body ~substs:(mk_substs ~v:binder ~expr:arg) , constraints)
       | _ -> (tv , [])
   end
 

src/test/contracts/record.ligo

@@ -64,5 +64,5 @@ end
 
 function modify_inner (const r : double_record) : double_record is
   block {
-    r := r with record inner = r.inner with record b = 2048; end; end;
+    r := r with record inner.b = 2048; end;
   } with r

src/test/contracts/record.mligo

@@ -50,4 +50,4 @@ type double_record = {
   inner : abc;
 }
 
-let modify_inner (r : double_record) : double_record = {r with inner = {r.inner with b = 2048 }}
+let modify_inner (r : double_record) : double_record = {r with inner.b = 2048 }

src/test/contracts/record.religo

@@ -50,4 +50,4 @@ type double_record = {
   inner : abc,
 };
 
-let modify_inner = (r : double_record) : double_record => {...r,inner : {...r.inner, b : 2048 } };
+let modify_inner = (r : double_record) : double_record => {...r,inner.b : 2048 };

src/test/typer_tests.ml

@@ -12,7 +12,7 @@ let int () : unit result =
   let open Typer in
   let e = Environment.full_empty in
   let state = Typer.Solver.initial_state in
-  let%bind (post , new_state) = type_expression e state pre in
+  let%bind (post , new_state) = type_expression_subst e state pre in
   let () = Typer.Solver.discard_state new_state in
   let open! Typed in
   let open Combinators in
@@ -27,7 +27,7 @@ module TestExpressions = struct
     let pre = expr in
     let open Typer in
     let open! Typed in
-    let%bind (post , new_state) = type_expression env state pre in
+    let%bind (post , new_state) = type_expression_subst env state pre in
     let () = Typer.Solver.discard_state new_state in
     let%bind () = assert_type_value_eq (post.type_annotation, test_expected_ty) in
     ok ()
@@ -37,7 +37,7 @@ module TestExpressions = struct
   module E = O
 
   let unit   () : unit result = test_expression I.(e_unit ())    O.(t_unit ())
-  let int    () : unit result = test_expression I.(e_int 32)  O.(t_int ())
+  let int    () : unit result = test_expression I.(e_int 32)     O.(t_int ())
   let bool   () : unit result = test_expression I.(e_bool true)  O.(t_bool ())
   let string () : unit result = test_expression I.(e_string "s") O.(t_string ())
   let bytes  () : unit result =

vendors/UnionFind/Partition0.ml

@@ -38,12 +38,10 @@ module Make (Item: Partition.Item) =
 
    (* Printing *)
 
-    let print (p: partition) =
+    let print ppf p =
-      let buffer = Buffer.create 80 in
       let print src dst =
-        let link =
+        Format.fprintf ppf "%s -> %s (%s)\n"
-          Printf.sprintf "%s -> %s\n"
+          (Item.to_string src) (Item.to_string dst) (Item.to_string (repr src p))
-                         (Item.to_string src) (Item.to_string dst)
+      in ItemMap.iter print p
-        in Buffer.add_string buffer link
+
-      in (ItemMap.iter print p; buffer)
   end