Merge branch 'dev' of gitlab.com:ligolang/ligo into rinderknecht@pprint

scripts/distribution/generic/build.sh

@@ -10,4 +10,9 @@ dockerfile="./docker/distribution/generic/build.Dockerfile"
 echo "Building LIGO for $target"
 echo "Using Dockerfile: $dockerfile"
 echo "Tagging as: $tag_build\n"
-docker build --build-arg ci_job_id="${CI_JOB_ID}" --build-arg target="$target" -t "$tag_build" -f "$dockerfile" .
+docker build \
+       --build-arg ci_job_id="${CI_JOB_ID}" \
+       --build-arg ci_commit_sha="${CI_COMMIT_SHA}" \
+       --build-arg commit_date="${COMMIT_DATE}" \
+       --build-arg target="$target" \
+       -t "$tag_build" -f "$dockerfile" .

src/bin/cli.ml

@@ -292,7 +292,7 @@ let interpret =
         let%bind mini_c_prg      = Compile.Of_typed.compile typed_prg in
         let      env             = Ast_typed.program_environment typed_prg in
         ok (mini_c_prg,state,env)
-      | None -> ok ([],Typer.Solver.initial_state,Ast_typed.Environment.full_empty) in
+      | None -> ok ([],Typer.Solver.initial_state,Environment.default) in
 
     let%bind (typed_exp,_)  = Compile.Utils.type_expression init_file syntax expression env state in
     let%bind mini_c_exp     = Compile.Of_typed.compile_expression typed_exp in
@@ -436,7 +436,7 @@ let evaluate_value =
 let compile_expression =
   let f expression syntax display_format michelson_format =
     toplevel ~display_format @@
-    let      env      = Ast_typed.Environment.full_empty in
+    let      env      = Environment.default in
     let      state    = Typer.Solver.initial_state in
     let%bind compiled_exp  = Compile.Utils.compile_expression None syntax expression env state in
     let%bind value         = Run.evaluate_expression compiled_exp.expr compiled_exp.expr_ty in

src/bin/expect_tests/michelson_converter.ml

@@ -0,0 +1,205 @@
+open Cli_expect
+
+let contract basename =
+  "../../test/contracts/" ^ basename
+let bad_contract basename =
+  "../../test/contracts/negative/" ^ basename
+
+let%expect_test _ =
+  run_ligo_bad [ "interpret" ; "--init-file="^(bad_contract "michelson_converter_no_annotation.mligo") ; "l4"] ;
+  [%expect {|
+    ligo: in file "michelson_converter_no_annotation.mligo", line 4, characters 9-39. can't retrieve type declaration order in the converted record, you need to annotate it
+
+     If you're not sure how to fix this error, you can
+     do one of the following:
+
+    * Visit our documentation: https://ligolang.org/docs/intro/introduction
+    * Ask a question on our Discord: https://discord.gg/9rhYaEt
+    * Open a gitlab issue: https://gitlab.com/ligolang/ligo/issues/new
+    * Check the changelog by running 'ligo changelog' |}] ;
+
+  run_ligo_bad [ "interpret" ; "--init-file="^(bad_contract "michelson_converter_short_record.mligo") ; "l1"] ;
+  [%expect {|
+    ligo: in file "michelson_converter_short_record.mligo", line 4, characters 9-44. converted record must have at least two elements
+
+     If you're not sure how to fix this error, you can
+     do one of the following:
+
+    * Visit our documentation: https://ligolang.org/docs/intro/introduction
+    * Ask a question on our Discord: https://discord.gg/9rhYaEt
+    * Open a gitlab issue: https://gitlab.com/ligolang/ligo/issues/new
+    * Check the changelog by running 'ligo changelog' |}]
+
+let%expect_test _ =
+  run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_pair.mligo") ; "r3"] ;
+  [%expect {|
+    ( 2 , ( +3 , "q" ) ) |}] ;
+  run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_pair.mligo") ; "r4"] ;
+  [%expect {|
+    ( 2 , ( +3 , ( "q" , true(unit) ) ) ) |}] ;
+  run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_pair.mligo") ; "l3"] ;
+  [%expect {|
+    ( ( 2 , +3 ) , "q" ) |}] ;
+  run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_pair.mligo") ; "l4"] ;
+  [%expect {|
+    ( ( ( 2 , +3 ) , "q" ) , true(unit) ) |}];
+  run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_or.mligo") ; "str3"] ;
+  [%expect {|
+    M_right(M_left(+3)) |}] ;
+  run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_or.mligo") ; "str4"] ;
+  [%expect {|
+    M_right(M_right(M_left("eq"))) |}] ;
+  run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_or.mligo") ; "stl3"] ;
+  [%expect {|
+    M_left(M_right(+3)) |}] ;
+  run_ligo_good [ "interpret" ; "--init-file="^(contract "michelson_converter_or.mligo") ; "stl4"] ;
+  [%expect {|
+    M_left(M_right("eq")) |}]
+
+let%expect_test _ =
+  run_ligo_good [ "dry-run" ; (contract "michelson_converter_pair.mligo") ; "main_r" ; "test_input_pair_r" ; "s"] ;
+  [%expect {|
+    ( LIST_EMPTY() , "eqeq" ) |}] ;
+  run_ligo_good [ "compile-contract" ; (contract "michelson_converter_pair.mligo") ; "main_r" ] ;
+  [%expect {|
+    { parameter (pair (int %one) (pair (nat %two) (pair (string %three) (bool %four)))) ;
+      storage string ;
+      code { DUP ;
+             CAR ;
+             DUP ;
+             CDR ;
+             CDR ;
+             CAR ;
+             DIG 1 ;
+             DUP ;
+             DUG 2 ;
+             CDR ;
+             CDR ;
+             CAR ;
+             CONCAT ;
+             NIL operation ;
+             PAIR ;
+             DIP { DROP 2 } } } |}];
+  run_ligo_good [ "dry-run" ; (contract "michelson_converter_pair.mligo") ; "main_l" ; "test_input_pair_l" ; "s"] ;
+  [%expect {|
+    ( LIST_EMPTY() , "eqeq" ) |}] ;
+  run_ligo_good [ "compile-contract" ; (contract "michelson_converter_pair.mligo") ; "main_l" ] ;
+  [%expect {|
+    { parameter (pair (pair (pair (int %one) (nat %two)) (string %three)) (bool %four)) ;
+      storage string ;
+      code { DUP ;
+             CAR ;
+             DUP ;
+             CAR ;
+             CDR ;
+             DIG 1 ;
+             DUP ;
+             DUG 2 ;
+             CAR ;
+             CDR ;
+             CONCAT ;
+             NIL operation ;
+             PAIR ;
+             DIP { DROP 2 } } } |}];
+  run_ligo_good [ "dry-run" ; contract "michelson_converter_or.mligo" ; "main_r" ; "vr" ; "Foo4 2"] ;
+  [%expect {|
+    ( LIST_EMPTY() , Baz4("eq") ) |}] ;
+  run_ligo_good [ "compile-contract" ; contract "michelson_converter_or.mligo" ; "main_r" ] ;
+  [%expect {|
+    { parameter (or (int %foo4) (or (nat %bar4) (or (string %baz4) (bool %boz4)))) ;
+      storage (or (or (nat %bar4) (string %baz4)) (or (bool %boz4) (int %foo4))) ;
+      code { PUSH string "eq" ;
+             LEFT bool ;
+             RIGHT nat ;
+             RIGHT int ;
+             PUSH string "eq" ;
+             RIGHT (or (int %foo4) (nat %bar4)) ;
+             LEFT bool ;
+             DIG 2 ;
+             DUP ;
+             DUG 3 ;
+             CAR ;
+             IF_LEFT
+               { DUP ; RIGHT bool ; RIGHT (or nat string) ; DIP { DROP } }
+               { DUP ;
+                 IF_LEFT
+                   { DUP ; LEFT string ; LEFT (or bool int) ; DIP { DROP } }
+                   { DUP ;
+                     IF_LEFT
+                       { DUP ; RIGHT nat ; LEFT (or bool int) ; DIP { DROP } }
+                       { DUP ; LEFT int ; RIGHT (or nat string) ; DIP { DROP } } ;
+                     DIP { DROP } } ;
+                 DIP { DROP } } ;
+             DUP ;
+             NIL operation ;
+             PAIR ;
+             DIP { DROP 4 } } } |}] ;
+  run_ligo_good [ "dry-run" ; contract "michelson_converter_or.mligo" ; "main_l" ; "vl" ; "Foo4 2"] ;
+  [%expect {|
+    ( LIST_EMPTY() , Baz4("eq") ) |}] ;
+  run_ligo_good [ "compile-contract" ; contract "michelson_converter_or.mligo" ; "main_l" ] ;
+  [%expect {|
+    { parameter (or (or (or (int %foo4) (nat %bar4)) (string %baz4)) (bool %boz4)) ;
+      storage (or (or (nat %bar4) (string %baz4)) (or (bool %boz4) (int %foo4))) ;
+      code { PUSH string "eq" ;
+             LEFT bool ;
+             RIGHT nat ;
+             RIGHT int ;
+             PUSH string "eq" ;
+             RIGHT (or (int %foo4) (nat %bar4)) ;
+             LEFT bool ;
+             DIG 2 ;
+             DUP ;
+             DUG 3 ;
+             CAR ;
+             IF_LEFT
+               { DUP ;
+                 IF_LEFT
+                   { DUP ;
+                     IF_LEFT
+                       { DUP ; RIGHT bool ; RIGHT (or nat string) ; DIP { DROP } }
+                       { DUP ; LEFT string ; LEFT (or bool int) ; DIP { DROP } } ;
+                     DIP { DROP } }
+                   { DUP ; RIGHT nat ; LEFT (or bool int) ; DIP { DROP } } ;
+                 DIP { DROP } }
+               { DUP ; LEFT int ; RIGHT (or nat string) ; DIP { DROP } } ;
+             DUP ;
+             NIL operation ;
+             PAIR ;
+             DIP { DROP 4 } } } |}]
+
+
+let%expect_test _ =
+  run_ligo_good [ "compile-contract" ; contract "michelson_comb_type_operators.mligo" ; "main_r"] ;
+  [%expect {|
+    { parameter (pair (int %foo) (pair (nat %bar) (string %baz))) ;
+      storage unit ;
+      code { UNIT ; NIL operation ; PAIR ; DIP { DROP } } } |}] ;
+
+  run_ligo_good [ "compile-contract" ; contract "michelson_comb_type_operators.mligo" ; "main_l"] ;
+  [%expect {|
+    { parameter (pair (pair (int %foo) (nat %bar)) (string %baz)) ;
+      storage unit ;
+      code { UNIT ; NIL operation ; PAIR ; DIP { DROP } } } |}]
+
+let%expect_test _ =
+  run_ligo_good [ "compile-contract" ; (contract "michelson_converter_mixed_pair_or.mligo") ; "main2" ] ;
+  [%expect {|
+    { parameter
+        (or (pair %option1 (string %bar) (nat %baz)) (pair %option2 (string %bar) (nat %baz))) ;
+      storage nat ;
+      code { DUP ;
+             CAR ;
+             IF_LEFT
+               { DUP ; LEFT (pair (string %bar) (nat %baz)) ; DIP { DROP } }
+               { DUP ; RIGHT (pair (string %bar) (nat %baz)) ; DIP { DROP } } ;
+             DUP ;
+             IF_LEFT
+               { DUP ; LEFT (pair (string %bar) (nat %baz)) ; DIP { DROP } }
+               { DUP ; RIGHT (pair (string %bar) (nat %baz)) ; DIP { DROP } } ;
+             DIP { DROP } ;
+             DUP ;
+             IF_LEFT
+               { DUP ; CDR ; NIL operation ; PAIR ; DIP { DROP } }
+               { DUP ; CDR ; NIL operation ; PAIR ; DIP { DROP } } ;
+             DIP { DROP 2 } } } |}]

src/environment/bool.ml

@@ -1,4 +1,4 @@
 open Ast_typed
 open Stage_common.Constant
 
-let environment = env_sum_type ~type_name:t_bool @@ [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None})]
+let environment = env_sum_type ~type_name:t_bool @@ [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=0});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=1})]

src/passes/10-transpiler/transpiler.ml

@@ -228,6 +228,10 @@ let transpile_constant' : AST.constant' -> constant' = function
   | C_IMPLICIT_ACCOUNT -> C_IMPLICIT_ACCOUNT
   | C_SET_DELEGATE -> C_SET_DELEGATE
   | C_CREATE_CONTRACT -> C_CREATE_CONTRACT
+  | C_CONVERT_TO_LEFT_COMB -> C_CONVERT_TO_LEFT_COMB
+  | C_CONVERT_TO_RIGHT_COMB -> C_CONVERT_TO_RIGHT_COMB
+  | C_CONVERT_FROM_LEFT_COMB -> C_CONVERT_FROM_LEFT_COMB
+  | C_CONVERT_FROM_RIGHT_COMB -> C_CONVERT_FROM_RIGHT_COMB
 
 let rec transpile_type (t:AST.type_expression) : type_value result =
   match t.type_content with

src/passes/2-concrete_to_imperative/cameligo.ml

@@ -294,29 +294,31 @@ and compile_type_expression : Raw.type_expr -> type_expression result = fun te -
   | TRecord r ->
       let (r, loc) = r_split r in
       let aux = fun (x, y) -> let%bind y = compile_type_expression y in ok (x, y) in
+      let order = fun i (x,y) -> ((x,i),y) in
       let apply (x:Raw.field_decl Raw.reg) =
         (x.value.field_name.value, x.value.field_type) in
       let%bind lst =
         bind_list
         @@ List.map aux
+        @@ List.mapi order
         @@ List.map apply
         @@ npseq_to_list r.ne_elements in
-      let m = List.fold_left (fun m (x, y) -> LMap.add (Label x) y m) LMap.empty lst in
+      let m = List.fold_left (fun m ((x,i), y) -> LMap.add (Label x) {field_type=y;field_decl_pos=i} m) LMap.empty lst in
       ok @@ make_t ~loc @@ T_record m
   | TSum s ->
       let (s,loc) = r_split s in
-      let aux (v:Raw.variant Raw.reg) =
+      let aux i (v:Raw.variant Raw.reg) =
         let args =
           match v.value.arg with
             None -> []
           | Some (_, TProd product) -> npseq_to_list product.value
           | Some (_, t_expr) -> [t_expr] in
         let%bind te = compile_list_type_expression @@ args in
-        ok (v.value.constr.value, te) in
+        ok ((v.value.constr.value,i), te) in
       let%bind lst = bind_list
-        @@ List.map aux
+        @@ List.mapi aux
         @@ npseq_to_list s in
-      let m = List.fold_left (fun m (x, y) -> CMap.add (Constructor x) y m) CMap.empty lst in
+      let m = List.fold_left (fun m ((x,i), y) -> CMap.add (Constructor x) {ctor_type=y;ctor_decl_pos=i} m) CMap.empty lst in
       ok @@ make_t ~loc @@ T_sum m
   | TString _s -> simple_fail "we don't support singleton string type"
 

src/passes/2-concrete_to_imperative/pascaligo.ml

@@ -224,29 +224,33 @@ let rec compile_type_expression (t:Raw.type_expr) : type_expression result =
         let%bind y = compile_type_expression y in
         ok (x, y)
       in
+      let order = fun i (x,y) ->
+        ((x,i),y)
+      in
       let apply =
         fun (x:Raw.field_decl Raw.reg) -> (x.value.field_name.value, x.value.field_type) in
       let%bind lst = bind_list
         @@ List.map aux
+        @@ List.mapi order
         @@ List.map apply
         @@ npseq_to_list r.ne_elements in
-      let m = List.fold_left (fun m (x, y) -> LMap.add (Label x) y m) LMap.empty lst in
+      let m = List.fold_left (fun m ((x,i), y) -> LMap.add (Label x) {field_type=y;field_decl_pos=i} m) LMap.empty lst in
       ok @@ make_t ~loc @@ T_record m
   | TSum s ->
       let (s,loc) = r_split s in
-      let aux (v:Raw.variant Raw.reg) =
+      let aux i (v:Raw.variant Raw.reg) =
         let args =
           match v.value.arg with
             None -> []
           | Some (_, TProd product) -> npseq_to_list product.value
           | Some (_, t_expr) -> [t_expr] in
         let%bind te = compile_list_type_expression @@ args in
-        ok (v.value.constr.value, te)
+        ok ((v.value.constr.value,i), te)
       in
       let%bind lst = bind_list
-        @@ List.map aux
+        @@ List.mapi aux
         @@ npseq_to_list s in
-      let m = List.fold_left (fun m (x, y) -> CMap.add (Constructor x) y m) CMap.empty lst in
+      let m = List.fold_left (fun m ((x,i), y) -> CMap.add (Constructor x) {ctor_type=y;ctor_decl_pos=i} m) CMap.empty lst in
       ok @@ make_t ~loc @@ T_sum m
   | TString _s -> simple_fail "we don't support singleton string type"
 

src/passes/3-self_ast_imperative/helpers.ml

@@ -2,6 +2,20 @@ open Ast_imperative
 open Trace
 open Stage_common.Helpers
 
+let bind_map_cmap_t f map = bind_cmap (
+  CMap.map 
+    (fun ({ctor_type;_} as ctor) -> 
+      let%bind ctor_type = f ctor_type in
+      ok {ctor with ctor_type }) 
+    map)
+
+let bind_map_lmap_t f map = bind_lmap (
+  LMap.map 
+    (fun ({field_type;_} as field) -> 
+      let%bind field_type = f field_type in
+      ok {field with field_type }) 
+    map)
+
 type 'a folder = 'a -> expression -> 'a result
 let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f init e ->
   let self = fold_expression f in 
@@ -250,10 +264,10 @@ and map_type_expression : ty_exp_mapper -> type_expression -> type_expression re
   let return type_content = ok { type_content; location=te.location } in
   match te'.type_content with
   | T_sum temap ->
-    let%bind temap' = bind_map_cmap self temap in
+    let%bind temap' = bind_map_cmap_t self temap in
     return @@ (T_sum temap')
   | T_record temap ->
-    let%bind temap' = bind_map_lmap self temap in
+    let%bind temap' = bind_map_lmap_t self temap in
     return @@ (T_record temap')
   | T_tuple telst ->
     let%bind telst' = bind_map_list self telst in

src/passes/4-imperative_to_sugar/imperative_to_sugar.ml

@@ -135,9 +135,9 @@ let rec compile_type_expression : I.type_expression -> O.type_expression result
     | I.T_sum sum -> 
       let sum = I.CMap.to_kv_list sum in
       let%bind sum = 
-        bind_map_list (fun (k,v) ->
+        bind_map_list (fun (k,({ctor_type = v; ctor_decl_pos ; _}:I.ctor_content)) ->
           let%bind v = compile_type_expression v in
-          let content : O.ctor_content = {ctor_type = v ; michelson_annotation = None} in
+          let content : O.ctor_content = {ctor_type = v ; michelson_annotation = None ; ctor_decl_pos } in
           ok @@ (k,content)
         ) sum
       in
@@ -145,9 +145,9 @@ let rec compile_type_expression : I.type_expression -> O.type_expression result
     | I.T_record record -> 
       let record = I.LMap.to_kv_list record in
       let%bind record = 
-        bind_map_list (fun (k,v) ->
+        bind_map_list (fun (k, ({field_type = v; field_decl_pos ; _}:I.field_content)) ->
           let%bind v = compile_type_expression v in
-          let content : O.field_content = {field_type = v ; michelson_annotation = None} in
+          let content : O.field_content = {field_type = v; michelson_annotation = None ; field_decl_pos} in
           ok @@ (k,content)
         ) record
       in
@@ -164,15 +164,15 @@ let rec compile_type_expression : I.type_expression -> O.type_expression result
     | I.T_operator (TC_michelson_or (l,l_ann,r,r_ann)) ->
       let%bind (l,r) = bind_map_pair compile_type_expression (l,r) in
       let sum : (O.constructor' * O.ctor_content) list = [
-        (O.Constructor "M_left" , {ctor_type = l ; michelson_annotation = Some l_ann}); 
+        (O.Constructor "M_left" , {ctor_type = l ; michelson_annotation = Some l_ann ; ctor_decl_pos = 0}); 
-        (O.Constructor "M_right", {ctor_type = r ; michelson_annotation = Some r_ann}); ]
+        (O.Constructor "M_right", {ctor_type = r ; michelson_annotation = Some r_ann ; ctor_decl_pos = 1}); ]
       in
       return @@ O.T_sum (O.CMap.of_list sum)
     | I.T_operator (TC_michelson_pair (l,l_ann,r,r_ann)) ->
       let%bind (l,r) = bind_map_pair compile_type_expression (l,r) in
       let sum : (O.label * O.field_content) list = [
-        (O.Label "0" , {field_type = l ; michelson_annotation = Some l_ann}); 
+        (O.Label "0" , {field_type = l ; michelson_annotation = Some l_ann ; field_decl_pos = 0}); 
-        (O.Label "1", {field_type = r ; michelson_annotation = Some r_ann}); ]
+        (O.Label "1", {field_type = r ; michelson_annotation = Some r_ann ; field_decl_pos = 0}); ]
       in
       return @@ O.T_record (O.LMap.of_list sum)
     | I.T_operator type_operator ->
@@ -201,6 +201,18 @@ and compile_type_operator : I.type_operator -> O.type_operator result =
       let%bind (k,v) = bind_map_pair compile_type_expression (k,v) in
       ok @@ O.TC_big_map (k,v)
     | TC_michelson_or _ | TC_michelson_pair _ -> fail @@ Errors.corner_case __LOC__
+    | TC_michelson_pair_right_comb c ->
+      let%bind c = compile_type_expression c in
+      ok @@ O.TC_michelson_pair_right_comb c
+    | TC_michelson_pair_left_comb c ->
+      let%bind c = compile_type_expression c in
+      ok @@ O.TC_michelson_pair_left_comb c
+    | TC_michelson_or_right_comb c ->
+      let%bind c = compile_type_expression c in
+      ok @@ O.TC_michelson_or_right_comb c
+    | TC_michelson_or_left_comb c ->
+      let%bind c = compile_type_expression c in
+      ok @@ O.TC_michelson_or_left_comb c
 
 let rec compile_expression : I.expression -> O.expression result =
   fun e ->
@@ -590,9 +602,9 @@ let rec uncompile_type_expression : O.type_expression -> I.type_expression resul
       let sum = I.CMap.to_kv_list sum in
       let%bind sum = 
         bind_map_list (fun (k,v) ->
-          let {ctor_type;_} : O.ctor_content = v in
+          let {ctor_type;ctor_decl_pos;_} : O.ctor_content = v in
           let%bind v = uncompile_type_expression ctor_type in
-          ok @@ (k,v)
+          ok @@ (k,({ctor_type=v; ctor_decl_pos}: I.ctor_content))
         ) sum
       in
       return @@ I.T_sum (O.CMap.of_list sum)
@@ -600,9 +612,9 @@ let rec uncompile_type_expression : O.type_expression -> I.type_expression resul
       let record = I.LMap.to_kv_list record in
       let%bind record = 
         bind_map_list (fun (k,v) ->
-          let {field_type;_} : O.field_content = v in
+          let {field_type;field_decl_pos} : O.field_content = v in
           let%bind v = uncompile_type_expression field_type in
-          ok @@ (k,v)
+          ok @@ (k,({field_type=v;field_decl_pos}:I.field_content))
         ) record
       in
       return @@ I.T_record (O.LMap.of_list record)
@@ -640,6 +652,18 @@ and uncompile_type_operator : O.type_operator -> I.type_operator result =
     | TC_big_map (k,v) ->
       let%bind (k,v) = bind_map_pair uncompile_type_expression (k,v) in
       ok @@ I.TC_big_map (k,v)
+    | TC_michelson_pair_right_comb c ->
+      let%bind c = uncompile_type_expression c in
+      ok @@ I.TC_michelson_pair_right_comb c
+    | TC_michelson_pair_left_comb c ->
+      let%bind c = uncompile_type_expression c in
+      ok @@ I.TC_michelson_pair_left_comb c
+    | TC_michelson_or_right_comb c ->
+      let%bind c = uncompile_type_expression c in
+      ok @@ I.TC_michelson_or_right_comb c
+    | TC_michelson_or_left_comb c ->
+      let%bind c = uncompile_type_expression c in
+      ok @@ I.TC_michelson_or_left_comb c
 
 let rec uncompile_expression' : O.expression -> I.expression result =
   fun e ->

src/passes/6-sugar_to_core/sugar_to_core.ml

@@ -10,9 +10,9 @@ let rec idle_type_expression : I.type_expression -> O.type_expression result =
       let sum = I.CMap.to_kv_list sum in
       let%bind sum = 
         bind_map_list (fun (k,v) ->
-          let {ctor_type ; michelson_annotation} : I.ctor_content = v in
+          let {ctor_type ; michelson_annotation ; ctor_decl_pos} : I.ctor_content = v in
           let%bind ctor_type = idle_type_expression ctor_type in
-          let v' : O.ctor_content = {ctor_type ; michelson_annotation} in
+          let v' : O.ctor_content = {ctor_type ; michelson_annotation ; ctor_decl_pos} in
           ok @@ (k,v')
         ) sum
       in
@@ -21,9 +21,9 @@ let rec idle_type_expression : I.type_expression -> O.type_expression result =
       let record = I.LMap.to_kv_list record in
       let%bind record = 
         bind_map_list (fun (k,v) ->
-          let {field_type ; michelson_annotation} : I.field_content = v in
+          let {field_type ; michelson_annotation ; field_decl_pos} : I.field_content = v in
           let%bind field_type = idle_type_expression field_type in
-          let v' : O.field_content = {field_type ; field_annotation=michelson_annotation} in
+          let v' : O.field_content = {field_type ; field_annotation=michelson_annotation ; field_decl_pos} in
           ok @@ (k,v')
         ) record
       in
@@ -31,7 +31,7 @@ let rec idle_type_expression : I.type_expression -> O.type_expression result =
     | I.T_tuple tuple ->
       let aux (i,acc) el = 
         let%bind el = idle_type_expression el in
-        ok @@ (i+1,(O.Label (string_of_int i), ({field_type=el;field_annotation=None}:O.field_content))::acc) in
+        ok @@ (i+1,(O.Label (string_of_int i), ({field_type=el;field_annotation=None;field_decl_pos=0}:O.field_content))::acc) in
       let%bind (_, lst ) = bind_fold_list aux (0,[]) tuple in
       let record = O.LMap.of_list lst in
       return @@ O.T_record record
@@ -66,6 +66,18 @@ and idle_type_operator : I.type_operator -> O.type_operator result =
     | TC_big_map (k,v) ->
       let%bind (k,v) = bind_map_pair idle_type_expression (k,v) in
       ok @@ O.TC_big_map (k,v)
+    | TC_michelson_pair_right_comb c ->
+      let%bind c = idle_type_expression c in
+      ok @@ O.TC_michelson_pair_right_comb c
+    | TC_michelson_pair_left_comb c ->
+      let%bind c = idle_type_expression c in
+      ok @@ O.TC_michelson_pair_left_comb c
+    | TC_michelson_or_right_comb c ->
+      let%bind c = idle_type_expression c in
+      ok @@ O.TC_michelson_or_right_comb c
+    | TC_michelson_or_left_comb c ->
+      let%bind c = idle_type_expression c in
+      ok @@ O.TC_michelson_or_left_comb c
 
 let rec compile_expression : I.expression -> O.expression result =
   fun e ->
@@ -238,9 +250,9 @@ let rec uncompile_type_expression : O.type_expression -> I.type_expression resul
       let sum = I.CMap.to_kv_list sum in
       let%bind sum = 
         bind_map_list (fun (k,v) ->
-          let {ctor_type;michelson_annotation} : O.ctor_content = v in
+          let {ctor_type;michelson_annotation;ctor_decl_pos} : O.ctor_content = v in
           let%bind ctor_type = uncompile_type_expression ctor_type in
-          let v' : I.ctor_content = {ctor_type;michelson_annotation} in
+          let v' : I.ctor_content = {ctor_type;michelson_annotation;ctor_decl_pos} in
           ok @@ (k,v')
         ) sum
       in
@@ -249,9 +261,9 @@ let rec uncompile_type_expression : O.type_expression -> I.type_expression resul
       let record = I.LMap.to_kv_list record in
       let%bind record = 
         bind_map_list (fun (k,v) ->
-          let {field_type;field_annotation} : O.field_content = v in
+          let {field_type;field_annotation;field_decl_pos} : O.field_content = v in
           let%bind field_type = uncompile_type_expression field_type in
-          let v' : I.field_content = {field_type;michelson_annotation=field_annotation} in
+          let v' : I.field_content = {field_type ; michelson_annotation=field_annotation ; field_decl_pos} in
           ok @@ (k,v')
         ) record
       in
@@ -288,6 +300,18 @@ and uncompile_type_operator : O.type_operator -> I.type_operator result =
       let%bind (k,v) = bind_map_pair uncompile_type_expression (k,v) in
       ok @@ I.TC_big_map (k,v)
     | TC_map_or_big_map _ -> failwith "TC_map_or_big_map shouldn't be uncompiled"
+    | TC_michelson_pair_right_comb c ->
+      let%bind c = uncompile_type_expression c in
+      ok @@ I.TC_michelson_pair_right_comb c
+    | TC_michelson_pair_left_comb c ->
+      let%bind c = uncompile_type_expression c in
+      ok @@ I.TC_michelson_pair_left_comb c
+    | TC_michelson_or_right_comb c ->
+      let%bind c = uncompile_type_expression c in
+      ok @@ I.TC_michelson_or_right_comb c
+    | TC_michelson_or_left_comb c ->
+      let%bind c = uncompile_type_expression c in
+      ok @@ I.TC_michelson_or_left_comb c
 
 let rec uncompile_expression : O.expression -> I.expression result =
   fun e ->

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

@@ -2,7 +2,7 @@ open Ast_typed
 open Format
 module UF = UnionFind.Poly2
 
-let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
+let type_constraint_ : _ -> type_constraint_simpl_ -> unit = fun ppf ->
   function
   |SC_Constructor { tv; c_tag; tv_list=_ } ->
     let ct = match c_tag with
@@ -34,6 +34,9 @@ let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf ->
   |SC_Poly        _ -> fprintf ppf "Poly"
   |SC_Typeclass   _ -> fprintf ppf "TC"
 
+let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf { reason_simpl ; c_simpl } ->
+  fprintf ppf "%a (reason: %s)" type_constraint_ c_simpl reason_simpl
+
 let all_constraints ppf ac =
   fprintf ppf "[%a]" (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint) ac
 

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

@@ -159,7 +159,7 @@ 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 dbs = match new_constraint with
+  let dbs = match new_constraint.c_simpl 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 = []}
@@ -173,7 +173,7 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si
     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
+    match new_constraint.c_simpl with
     | SC_Constructor ({tv ; c_tag = _ ; tv_list = _} as c) ->
       let assignments = Map.update tv (function None -> Some c | e -> e) dbs.assignments in
       let dbs = {dbs with assignments} in
@@ -210,28 +210,28 @@ let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer
   fun dbs new_constraint ->
   let insert_fresh a b =
     let fresh = Core.fresh_type_variable () in
-    let (dbs , cs1) = normalizer_simpl dbs (c_equation (P_variable fresh) a) in
+    let (dbs , cs1) = normalizer_simpl dbs (c_equation (P_variable fresh) a "normalizer: simpl") in
-    let (dbs , cs2) = normalizer_simpl dbs (c_equation (P_variable fresh) b) in
+    let (dbs , cs2) = normalizer_simpl dbs (c_equation (P_variable fresh) b "normalizer: simpl") in
     (dbs , cs1 @ cs2) in
   let split_constant a c_tag args =
     let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
-    let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t) (List.combine fresh_vars args) in
+    let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t "normalizer: split_constant") (List.combine fresh_vars args) in
     let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
-    (dbs , [SC_Constructor {tv=a;c_tag;tv_list=fresh_vars}] @ List.flatten recur) in
+    (dbs , [{c_simpl=SC_Constructor {tv=a;c_tag;tv_list=fresh_vars};reason_simpl="normalizer: split constant"}] @ List.flatten recur) in
-  let gather_forall a forall = (dbs , [SC_Poly { tv=a; forall }]) in
+  let gather_forall a forall = (dbs , [{c_simpl=SC_Poly { tv=a; forall };reason_simpl="normalizer: gather_forall"}]) in
-  let gather_alias a b = (dbs , [SC_Alias { a ; b }]) in
+  let gather_alias a b = (dbs , [{c_simpl=SC_Alias { a ; b };reason_simpl="normalizer: gather_alias"}]) in
   let reduce_type_app a b =
     let (reduced, new_constraints) = check_applied @@ type_level_eval b in
     let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs new_constraints in
-    let (dbs , resimpl) = normalizer_simpl dbs (c_equation a reduced) in (* Note: this calls recursively but cant't fall in the same case. *)
+    let (dbs , resimpl) = normalizer_simpl dbs (c_equation a reduced "normalizer: reduce_type_app") in (* Note: this calls recursively but cant't fall in the same case. *)
     (dbs , resimpl @ List.flatten recur) in
   let split_typeclass args tc =
     let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in
-    let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t) (List.combine fresh_vars args) in
+    let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t "normalizer: split_typeclass") (List.combine fresh_vars args) in
     let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in
-    (dbs, [SC_Typeclass { tc ; args = fresh_vars }] @ List.flatten recur) in
+    (dbs, [{c_simpl=SC_Typeclass { tc ; args = fresh_vars };reason_simpl="normalizer: split_typeclass"}] @ List.flatten recur) in
 
-  match new_constraint with
+  match new_constraint.c with
   (* break down (forall 'b, body = forall 'c, body') into ('a = forall 'b, body and 'a = forall 'c, body')) *)
   | C_equation {aval=(P_forall _ as a); bval=(P_forall _ as b)}     -> insert_fresh a b
   (* break down (forall 'b, body = c(args)) into ('a = forall 'b, body and 'a = c(args)) *)
@@ -325,7 +325,7 @@ type 'selector_output propagator = 'selector_output -> structured_dbs -> new_con
 let selector_break_ctor :  (type_constraint_simpl, output_break_ctor) selector =
   (* find two rules with the shape a = k(var …) and a = k'(var' …) *)
   fun type_constraint_simpl dbs ->
-  match type_constraint_simpl with
+  match type_constraint_simpl.c_simpl with
     SC_Constructor c ->
     (* finding other constraints related to the same type variable and
        with the same sort of constraint (constructor vs. constructor)
@@ -473,7 +473,7 @@ let propagator_break_ctor : output_break_ctor propagator =
   (* produce constraints: *)
 
   (* a.tv = b.tv *)
-  let eq1 = c_equation (P_variable a.tv) (P_variable b.tv) in
+  let eq1 = c_equation (P_variable a.tv) (P_variable b.tv) "propagator: break_ctor" in
   (* a.c_tag = b.c_tag *)
   if (compare_simple_c_constant a.c_tag b.c_tag) <> 0 then
     failwith (Format.asprintf "type error: incompatible types, not same ctor %a vs. %a (compare returns %d)" debug_pp_c_constructor_simpl a debug_pp_c_constructor_simpl b (compare_simple_c_constant a.c_tag b.c_tag))
@@ -482,7 +482,7 @@ let propagator_break_ctor : output_break_ctor propagator =
   if List.length a.tv_list <> List.length b.tv_list then
     failwith "type error: incompatible types, not same length"
   else
-    let eqs3 = List.map2 (fun aa bb -> c_equation (P_variable aa) (P_variable bb)) a.tv_list b.tv_list in
+    let eqs3 = List.map2 (fun aa bb -> c_equation (P_variable aa) (P_variable bb) "propagator: break_ctor") a.tv_list b.tv_list in
     let eqs = eq1 :: eqs3 in
     (eqs , []) (* no new assignments *)
 
@@ -531,7 +531,12 @@ and compare_type_expression = function
       | P_variable _ -> 1
       | P_constant _ -> 1
       | P_apply { tf=b1; targ=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2)
-and compare_type_constraint = function
+and compare_type_constraint = fun { c = ca ; reason = ra } { c = cb ; reason = rb } ->
+  let c = compare_type_constraint_ ca cb in
+  if c < 0 then -1
+  else if c = 0 then String.compare ra rb
+  else 1
+and compare_type_constraint_ = function
   | C_equation { aval=a1; bval=a2 } -> (function
       | C_equation { aval=b1; bval=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2
       | C_typeclass _ -> -1
@@ -569,7 +574,7 @@ let selector_specialize1 : (type_constraint_simpl, output_specialize1) selector
   (* TODO: do the same for two rules with the shape (a = forall b, d) and tc(a…) *)
   (* TODO: do the appropriate thing for two rules with the shape (a = forall b, d) and (a = forall b', d') *)
   fun type_constraint_simpl dbs ->
-  match type_constraint_simpl with
+  match type_constraint_simpl.c_simpl with
     SC_Constructor c                ->
     (* vice versa *)
     let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).poly in
@@ -599,7 +604,7 @@ let propagator_specialize1 : output_specialize1 propagator =
      The substitution is obtained by immediately applying the forall. *)
   let apply = (P_apply {tf = (P_forall a.forall); targ = P_variable fresh_existential}) in
   let (reduced, new_constraints) = check_applied @@ type_level_eval apply in
-  let eq1 = c_equation (P_variable b.tv) reduced in
+  let eq1 = c_equation (P_variable b.tv) reduced "propagator: specialize1" in
   let eqs = eq1 :: new_constraints in
   (eqs, []) (* no new assignments *)
 

src/passes/8-typer-new/todo_use_fold_generator.ml

@@ -133,3 +133,7 @@ let convert_constant' : I.constant' -> O.constant' = function
   | C_IMPLICIT_ACCOUNT -> C_IMPLICIT_ACCOUNT
   | C_SET_DELEGATE -> C_SET_DELEGATE
   | C_CREATE_CONTRACT -> C_CREATE_CONTRACT
+  | C_CONVERT_TO_LEFT_COMB -> C_CONVERT_TO_LEFT_COMB
+  | C_CONVERT_TO_RIGHT_COMB -> C_CONVERT_TO_RIGHT_COMB
+  | C_CONVERT_FROM_LEFT_COMB -> C_CONVERT_FROM_LEFT_COMB
+  | C_CONVERT_FROM_RIGHT_COMB -> C_CONVERT_FROM_RIGHT_COMB

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

@@ -133,18 +133,18 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu
   | T_sum m ->
     let aux k v prev =
       let%bind prev' = prev in
-      let {ctor_type ; michelson_annotation} : I.ctor_content = v in
+      let {ctor_type ; michelson_annotation ; ctor_decl_pos} : I.ctor_content = v in
       let%bind ctor_type = evaluate_type e ctor_type in
-      ok @@ O.CMap.add (convert_constructor' k) ({ctor_type ; michelson_annotation}:O.ctor_content) prev'
+      ok @@ O.CMap.add (convert_constructor' k) ({ctor_type ; michelson_annotation ; ctor_decl_pos}:O.ctor_content) prev'
     in
     let%bind m = I.CMap.fold aux m (ok O.CMap.empty) in
     return (T_sum m)
   | T_record m ->
     let aux k v prev =
       let%bind prev' = prev in
-      let {field_type ; field_annotation} : I.field_content = v in
+      let {field_type ; field_annotation ; field_decl_pos} : I.field_content = v in
       let%bind field_type = evaluate_type e field_type in
-      ok @@ O.LMap.add (convert_label k) ({field_type ; michelson_annotation=field_annotation}:O.field_content) prev'
+      ok @@ O.LMap.add (convert_label k) ({field_type ; michelson_annotation=field_annotation ; field_decl_pos}:O.field_content) prev'
     in
     let%bind m = I.LMap.fold aux m (ok O.LMap.empty) in
     return (T_record m)
@@ -181,6 +181,10 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu
         | TC_contract c ->
             let%bind c = evaluate_type e c in
             ok @@ O.TC_contract c
+        | TC_michelson_pair_right_comb _c | TC_michelson_pair_left_comb _c 
+        | TC_michelson_or_right_comb _c | TC_michelson_or_left_comb _c ->
+          (* not really sure what to do in the new typer, should be converted to a pair using functions defined in Helpers.Typer.Converter *)
+          simple_fail "to be implemented"
         in
       return (T_operator (opt))
 
@@ -300,7 +304,7 @@ and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression
       ok (O.LMap.add (convert_label k) expr' acc , state')
     in
     let%bind (m' , state') = Stage_common.Helpers.bind_fold_lmap aux (ok (O.LMap.empty , state)) m in
-    let wrapped = Wrap.record (O.LMap.map (fun e -> ({field_type = get_type_expression e ; michelson_annotation = None}: O.field_content)) m') in
+    let wrapped = Wrap.record (O.LMap.map (fun e -> ({field_type = get_type_expression e ; michelson_annotation = None ; field_decl_pos = 0}: O.field_content)) m') in
     return_wrapped (E_record m') state' wrapped
   | E_record_update {record; path; update} ->
     let%bind (record, state) = type_expression e state record in

src/passes/8-typer-new/untyper.ml

@@ -135,6 +135,10 @@ let unconvert_constant' : O.constant' -> I.constant' = function
   | C_IMPLICIT_ACCOUNT -> C_IMPLICIT_ACCOUNT
   | C_SET_DELEGATE -> C_SET_DELEGATE
   | C_CREATE_CONTRACT -> C_CREATE_CONTRACT
+  | C_CONVERT_TO_LEFT_COMB -> C_CONVERT_TO_LEFT_COMB
+  | C_CONVERT_TO_RIGHT_COMB -> C_CONVERT_TO_RIGHT_COMB
+  | C_CONVERT_FROM_LEFT_COMB -> C_CONVERT_FROM_LEFT_COMB
+  | C_CONVERT_FROM_RIGHT_COMB -> C_CONVERT_FROM_RIGHT_COMB
 
 let untype_type_value (t:O.type_expression) : (I.type_expression) result =
   match t.type_meta with
@@ -148,18 +152,18 @@ let rec untype_type_expression (t:O.type_expression) : (I.type_expression) resul
   (* TODO: or should we use t.core if present? *)
   let%bind t = match t.type_content with
   | O.T_sum x ->
-    let aux k ({ctor_type ; michelson_annotation} : O.ctor_content) acc =
+    let aux k ({ctor_type ; michelson_annotation ; ctor_decl_pos} : O.ctor_content) acc =
       let%bind acc = acc in
       let%bind ctor_type = untype_type_expression ctor_type in
-      let v' : I.ctor_content = {ctor_type ; michelson_annotation} in 
+      let v' : I.ctor_content = {ctor_type ; michelson_annotation ; ctor_decl_pos} in 
       ok @@ I.CMap.add (unconvert_constructor' k) v' acc in
     let%bind x' = O.CMap.fold aux x (ok I.CMap.empty) in
     ok @@ I.T_sum x'
   | O.T_record x ->
-    let aux k ({field_type ; michelson_annotation} : O.field_content) acc =
+    let aux k ({field_type ; michelson_annotation ; field_decl_pos} : O.field_content) acc =
       let%bind acc = acc in
       let%bind field_type = untype_type_expression field_type in
-      let v' = ({field_type ; field_annotation=michelson_annotation} : I.field_content) in
+      let v' = ({field_type ; field_annotation=michelson_annotation ; field_decl_pos} : I.field_content) in
       ok @@ I.LMap.add (unconvert_label k) v' acc in
     let%bind x' = O.LMap.fold aux x (ok I.LMap.empty) in
     ok @@ I.T_record x'

src/passes/8-typer-new/wrap.ml

@@ -106,6 +106,10 @@ let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_v
                                 | TC_big_map  ( k , v )  -> (C_big_map, [k;v])
                                 | TC_map_or_big_map ( k , v) -> (C_map, [k;v])
                                 | TC_contract c          -> (C_contract, [c])
+                                | TC_michelson_pair_right_comb c -> (C_record, [c])
+                                | TC_michelson_pair_left_comb c -> (C_record, [c])
+                                | TC_michelson_or_right_comb c -> (C_record, [c])
+                                | TC_michelson_or_left_comb c -> (C_record, [c])
                           )
      in
      p_constant csttag (List.map type_expression_to_type_value_copypasted args)
@@ -117,12 +121,12 @@ let failwith_ : unit -> (constraints * O.type_variable) = fun () ->
 let variable : I.expression_variable -> T.type_expression -> (constraints * T.type_variable) = fun _name expr ->
   let pattern = type_expression_to_type_value expr in
   let type_name = Core.fresh_type_variable () in
-  [C_equation { aval = P_variable type_name ; bval = pattern }] , type_name
+  [{ c = C_equation { aval = P_variable type_name ; bval = pattern } ; reason = "wrap: variable" }] , type_name
 
 let literal : T.type_expression -> (constraints * T.type_variable) = fun t ->
   let pattern = type_expression_to_type_value t in
   let type_name = Core.fresh_type_variable () in
-  [C_equation { aval = P_variable type_name ; bval = pattern }] , type_name
+  [{ c = C_equation { aval = P_variable type_name ; bval = pattern } ; reason = "wrap: literal" }] , type_name
 
 (*
   let literal_bool : unit -> (constraints * O.type_variable) = fun () ->
@@ -140,7 +144,7 @@ let tuple : T.type_expression list -> (constraints * T.type_variable) = fun tys
   let patterns = List.map type_expression_to_type_value tys in
   let pattern = p_constant C_record patterns in
   let type_name = Core.fresh_type_variable () in
-  [C_equation { aval = P_variable type_name ; bval = pattern}] , type_name
+  [{ c = C_equation { aval = P_variable type_name ; bval = pattern} ; reason = "wrap: tuple" }] , type_name
 
 (* let t_tuple         = ('label:int, 'v) … -> record ('label : 'v) … *)
 (* let t_constructor   = ('label:string, 'v) -> variant ('label : 'v) *)
@@ -169,7 +173,7 @@ end
 let access_label ~(base : T.type_expression) ~(label : O.accessor) : (constraints * T.type_variable) =
   let base' = type_expression_to_type_value base in
   let expr_type = Core.fresh_type_variable () in
-  [T.C_access_label { c_access_label_tval = base' ; accessor = label ; c_access_label_tvar = expr_type }] , expr_type
+  [{ c = C_access_label { c_access_label_tval = base' ; accessor = label ; c_access_label_tvar = expr_type } ; reason = "wrap: access_label" }] , expr_type
 
 open Ast_typed.Misc
 let constructor
@@ -180,25 +184,25 @@ let constructor
   let sum = type_expression_to_type_value sum in
   let whole_expr = Core.fresh_type_variable () in
   [
-    c_equation (P_variable whole_expr) sum ;
+    c_equation (P_variable whole_expr) sum "wrap: constructor: whole" ;
-    c_equation t_arg c_arg ;
+    c_equation t_arg c_arg "wrap: construcotr: arg" ;
   ] , whole_expr
 
 let record : T.field_content T.label_map -> (constraints * T.type_variable) = fun fields ->
   let record_type = type_expression_to_type_value (T.t_record fields ()) in
   let whole_expr = Core.fresh_type_variable () in
-  [c_equation (P_variable whole_expr) record_type] , whole_expr
+  [c_equation (P_variable whole_expr) record_type "wrap: record: whole"] , whole_expr
 
 let collection : O.constant_tag -> T.type_expression list -> (constraints * T.type_variable) =
   fun ctor element_tys ->
   let elttype = T.P_variable (Core.fresh_type_variable ()) in
   let aux elt =
     let elt' = type_expression_to_type_value elt
-    in c_equation elttype elt' in
+    in c_equation elttype elt' "wrap: collection: elt" in
   let equations = List.map aux element_tys in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation (P_variable whole_expr) (p_constant ctor [elttype]) ;
+      c_equation (P_variable whole_expr) (p_constant ctor [elttype]) "wrap: collection: whole" ;
   ] @ equations , whole_expr
 
 let list = collection T.C_list
@@ -210,15 +214,15 @@ let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_
   let v_type = T.P_variable (Core.fresh_type_variable ()) in
   let aux_k (k , _v) =
     let k' = type_expression_to_type_value k in
-    c_equation k_type k' in
+    c_equation k_type k' "wrap: map: key" in
   let aux_v (_k , v) =
     let v' = type_expression_to_type_value v in
-    c_equation v_type v' in
+    c_equation v_type v' "wrap: map: value" in
   let equations_k = List.map aux_k kv_tys in
   let equations_v = List.map aux_v kv_tys in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation (P_variable whole_expr) (p_constant C_map [k_type ; v_type]) ;
+      c_equation (P_variable whole_expr) (p_constant C_map [k_type ; v_type]) "wrap: map: whole" ;
   ] @ equations_k @ equations_v , whole_expr
 
 let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) =
@@ -227,17 +231,17 @@ let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.t
   let v_type = T.P_variable (Core.fresh_type_variable ()) in
   let aux_k (k , _v) =
     let k' = type_expression_to_type_value k in
-    c_equation k_type k' in
+    c_equation k_type k' "wrap: big_map: key" in
   let aux_v (_k , v) =
     let v' = type_expression_to_type_value v in
-    c_equation v_type v' in
+    c_equation v_type v' "wrap: big_map: value" in
   let equations_k = List.map aux_k kv_tys in
   let equations_v = List.map aux_v kv_tys in
   let whole_expr = Core.fresh_type_variable () in
   [
       (* TODO: this doesn't tag big_maps uniquely (i.e. if two
            big_map have the same type, they can be swapped. *)
-      c_equation (P_variable whole_expr) (p_constant C_big_map [k_type ; v_type]) ;
+      c_equation (P_variable whole_expr) (p_constant C_big_map [k_type ; v_type]) "wrap: big_map: whole" ;
   ] @ equations_k @ equations_v , whole_expr
 
 let application : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -246,7 +250,7 @@ let application : T.type_expression -> T.type_expression -> (constraints * T.typ
   let f'   = type_expression_to_type_value f in
   let arg' = type_expression_to_type_value arg in
   [
-      c_equation f' (p_constant C_arrow [arg' ; P_variable whole_expr]) ;
+      c_equation f' (p_constant C_arrow [arg' ; P_variable whole_expr]) "wrap: application: f" ;
   ] , whole_expr
 
 let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -256,8 +260,8 @@ let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_va
   let whole_expr = Core.fresh_type_variable () in
   let v = Core.fresh_type_variable () in
   [
-      c_equation ds' (p_constant C_map [ind' ; P_variable v]) ;
+      c_equation ds' (p_constant C_map [ind' ; P_variable v]) "wrap: look_up: map" ;
-      c_equation (P_variable whole_expr) (p_constant C_option [P_variable v]) ;
+      c_equation (P_variable whole_expr) (p_constant C_option [P_variable v]) "wrap: look_up: whole" ;
   ] , whole_expr
 
 let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -266,8 +270,8 @@ let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_v
   let b' = type_expression_to_type_value b in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation a' (p_constant C_unit []) ;
+      c_equation a' (p_constant C_unit []) "wrap: sequence: first" ;
-      c_equation b' (P_variable whole_expr) ;
+      c_equation b' (P_variable whole_expr) "wrap: sequence: second (whole)" ;
   ] , whole_expr
 
 let loop : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -276,9 +280,9 @@ let loop : T.type_expression -> T.type_expression -> (constraints * T.type_varia
   let body' = type_expression_to_type_value body in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation expr'                   (P_variable (Stage_common.Constant.t_bool)) ;
+      c_equation expr'                   (P_variable Stage_common.Constant.t_bool) "wrap: loop: expr" ;
-      c_equation body'                   (p_constant C_unit []) ;
+      c_equation body'                   (p_constant C_unit []) "wrap: loop: body" ;
-      c_equation (P_variable whole_expr) (p_constant C_unit [])
+      c_equation (P_variable whole_expr) (p_constant C_unit []) "wrap: loop: whole (unit)" ;
   ] , whole_expr
 
 let let_in : T.type_expression -> T.type_expression option -> T.type_expression -> (constraints * T.type_variable) =
@@ -287,10 +291,10 @@ let let_in : T.type_expression -> T.type_expression option -> T.type_expression
   let result'     = type_expression_to_type_value result in
   let rhs_tv_opt' = match rhs_tv_opt with
       None -> []
-    | Some annot -> [c_equation rhs' (type_expression_to_type_value annot)] in
+    | Some annot -> [c_equation rhs' (type_expression_to_type_value annot) "wrap: let_in: rhs"] in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation result' (P_variable whole_expr) ;
+      c_equation result' (P_variable whole_expr) "wrap: let_in: result (whole)" ;
   ] @ rhs_tv_opt', whole_expr
 
 let recursive : T.type_expression -> (constraints * T.type_variable) =
@@ -298,7 +302,7 @@ let recursive : T.type_expression -> (constraints * T.type_variable) =
   let fun_type = type_expression_to_type_value fun_type in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation fun_type (P_variable whole_expr) ;
+      c_equation fun_type (P_variable whole_expr) "wrap: recursive: fun_type (whole)" ;
   ], whole_expr
 
 let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -307,8 +311,8 @@ let assign : T.type_expression -> T.type_expression -> (constraints * T.type_var
   let e' = type_expression_to_type_value e in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation v'  e' ;
+      c_equation v'  e' "wrap: assign: var type must eq rhs type" ;
-      c_equation (P_variable whole_expr) (p_constant C_unit []) ;
+      c_equation (P_variable whole_expr) (p_constant C_unit []) "wrap: assign: unit (whole)" ;
   ] , whole_expr
 
 let annotation : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
@@ -317,15 +321,15 @@ let annotation : T.type_expression -> T.type_expression -> (constraints * T.type
   let annot' = type_expression_to_type_value annot in
   let whole_expr = Core.fresh_type_variable () in
   [
-      c_equation e' annot' ;
+      c_equation e' annot' "wrap: annotation: expr type must eq annot" ;
-      c_equation e' (P_variable whole_expr) ;
+      c_equation e' (P_variable whole_expr) "wrap: annotation: whole" ;
   ] , whole_expr
 
 let matching : T.type_expression list -> (constraints * T.type_variable) =
   fun es ->
   let whole_expr = Core.fresh_type_variable () in
   let type_expressions = (List.map type_expression_to_type_value es) in
-  let cs = List.map (fun e -> c_equation (P_variable whole_expr) e) type_expressions
+  let cs = List.map (fun e -> c_equation (P_variable whole_expr) e "wrap: matching: case (whole)") type_expressions
   in cs, whole_expr
 
 let fresh_binder () =
@@ -342,15 +346,16 @@ let lambda
   let unification_body = Core.fresh_type_variable () in
   let arg'  = match arg with
       None -> []
-    | Some arg -> [c_equation (P_variable unification_arg) (type_expression_to_type_value arg)] in
+    | Some arg -> [c_equation (P_variable unification_arg) (type_expression_to_type_value arg) "wrap: lambda: arg annot"] in
   let body'  = match body with
       None -> []
-    | Some body -> [c_equation (P_variable unification_body) (type_expression_to_type_value body)]
+    | Some body -> [c_equation (P_variable unification_body) (type_expression_to_type_value body) "wrap: lambda: body annot"]
   in [
-      c_equation (type_expression_to_type_value fresh) (P_variable unification_arg) ;
+      c_equation (type_expression_to_type_value fresh) (P_variable unification_arg) "wrap: lambda: arg" ;
       c_equation (P_variable whole_expr)
                  (p_constant C_arrow ([P_variable unification_arg ;
                                        P_variable unification_body]))
+                 "wrap: lambda: arrow (whole)"
      ] @ arg' @ body' , whole_expr
 
 (* This is pretty much a wrapper for an n-ary function. *)
@@ -360,5 +365,5 @@ let constant : O.type_value -> T.type_expression list -> (constraints * T.type_v
   let args'      = List.map type_expression_to_type_value args in
   let args_tuple = p_constant C_record args' in
   [
-      c_equation f (p_constant C_arrow ([args_tuple ; P_variable whole_expr]))
+      c_equation f (p_constant C_arrow ([args_tuple ; P_variable whole_expr])) "wrap: constant: as declared for built-in"
   ] , whole_expr

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

@@ -12,6 +12,22 @@ module Solver = Typer_new.Solver
 type environment = Environment.t
 
 module Errors = struct
+  let michelson_comb_no_record (loc:Location.t) () =
+    let title = (thunk "bad michelson_pair_right_comb type parameter") in
+    let message () = "michelson_pair_right_comb type operator must be used on a record type" in
+    let data = [
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ;
+    ] in
+    error ~data title message ()
+
+  let michelson_comb_no_variant (loc:Location.t) () =
+    let title = (thunk "bad michelson_or_right_comb type parameter") in
+    let message () = "michelson_or_right_comb type operator must be used on a variant type" in
+    let data = [
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ;
+    ] in
+    error ~data title message ()
+
   let unbound_type_variable (e:environment) (tv:I.type_variable) (loc:Location.t) () =
     let name = Var.to_name tv in
     let suggestion = match name with
@@ -192,7 +208,7 @@ module Errors = struct
     ] in
     error ~data title message ()
 
-  let type_error ?(msg="") ~(expected: O.type_expression) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () =
+  let _type_error ?(msg="") ~(expected: O.type_expression) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () =
     let title = (thunk "type error") in
     let message () = msg in
     let data = [
@@ -350,6 +366,10 @@ let convert_constant' : I.constant' -> O.constant' = function
   | C_IMPLICIT_ACCOUNT -> C_IMPLICIT_ACCOUNT
   | C_SET_DELEGATE -> C_SET_DELEGATE
   | C_CREATE_CONTRACT -> C_CREATE_CONTRACT
+  | C_CONVERT_TO_LEFT_COMB -> C_CONVERT_TO_LEFT_COMB
+  | C_CONVERT_TO_RIGHT_COMB -> C_CONVERT_TO_RIGHT_COMB
+  | C_CONVERT_FROM_LEFT_COMB -> C_CONVERT_FROM_LEFT_COMB
+  | C_CONVERT_FROM_RIGHT_COMB -> C_CONVERT_FROM_RIGHT_COMB
 
 let unconvert_constant' : O.constant' -> I.constant' = function
   | C_INT -> C_INT
@@ -465,6 +485,10 @@ let unconvert_constant' : O.constant' -> I.constant' = function
   | C_IMPLICIT_ACCOUNT -> C_IMPLICIT_ACCOUNT
   | C_SET_DELEGATE -> C_SET_DELEGATE
   | C_CREATE_CONTRACT -> C_CREATE_CONTRACT
+  | C_CONVERT_TO_LEFT_COMB -> C_CONVERT_TO_LEFT_COMB
+  | C_CONVERT_TO_RIGHT_COMB -> C_CONVERT_TO_RIGHT_COMB
+  | C_CONVERT_FROM_LEFT_COMB -> C_CONVERT_FROM_LEFT_COMB
+  | C_CONVERT_FROM_RIGHT_COMB -> C_CONVERT_FROM_RIGHT_COMB
 
 let rec type_program (p:I.program) : (O.program * O.typer_state) result =
   let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
@@ -495,7 +519,7 @@ and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) :
     )
 
 and type_match : (environment -> I.expression -> O.expression result) -> environment -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> O.matching_expr result =
-  fun f e t i ae loc -> match i with
+  fun f e t i _ae loc -> match i with
   | Match_option {match_none ; match_some} ->
       let%bind tv =
         trace_strong (match_error ~expected:i ~actual:t loc)
@@ -527,59 +551,32 @@ and type_match : (environment -> I.expression -> O.expression result) -> environ
       let%bind body = f e' b in
       ok (O.Match_tuple { vars ; body ; tvs})
   | Match_variant (lst,_) ->
-      let%bind variant_opt =
+      let%bind variant_cases' =
-        let aux acc ((constructor_name , _) , _) =
+        trace (match_error ~expected:i ~actual:t loc)
-          let%bind (_ , variant) =
+        @@ Ast_typed.Combinators.get_t_sum t in
-            trace_option (unbound_constructor e constructor_name loc) @@
+      let variant_cases = List.map fst @@ O.CMap.to_kv_list variant_cases' in
-            Environment.get_constructor constructor_name e in
+      let match_cases = List.map (fun x -> convert_constructor' @@ fst @@ fst x) lst in
-          let%bind acc = match acc with
+      let test_case = fun c ->
-            | None -> ok (Some variant)
+        Assert.assert_true (List.mem c match_cases)
-            | Some variant' -> (
-                trace (type_error
-                         ~msg:"in match variant"
-                         ~expected:variant
-                         ~actual:variant'
-                         ~expression:ae
-                         loc
-                      ) @@
-                Ast_typed.assert_type_expression_eq (variant , variant') >>? fun () ->
-                ok (Some variant)
-              ) in
-          ok acc in
-        trace (simple_info "in match variant") @@
-        bind_fold_list aux None lst in
-      let%bind tv =
-        trace_option (match_empty_variant i loc) @@
-        variant_opt in
-      let%bind () =
-        let%bind variant_cases' =
-          trace (match_error ~expected:i ~actual:t loc)
-          @@ Ast_typed.Combinators.get_t_sum tv in
-        let variant_cases = List.map fst @@ O.CMap.to_kv_list variant_cases' in
-        let match_cases = List.map (fun x -> convert_constructor' @@ fst @@ fst x) lst in
-        let test_case = fun c ->
-          Assert.assert_true (List.mem c match_cases)
-        in
-        let%bind () =
-          trace_strong (match_missing_case i loc) @@
-          bind_iter_list test_case variant_cases in
-        let%bind () =
-          trace_strong (match_redundant_case i loc) @@
-          Assert.assert_true List.(length variant_cases = length match_cases) in
-        ok ()
       in
+      let%bind () =
+        trace_strong (match_missing_case i loc) @@
+        bind_iter_list test_case variant_cases in
+      let%bind () =
+        trace_strong (match_redundant_case i loc) @@
+        Assert.assert_true List.(length variant_cases = length match_cases) in
       let%bind cases =
         let aux ((constructor_name , pattern) , b) =
-          let%bind (constructor , _) =
+          let%bind {ctor_type=constructor;_} =
             trace_option (unbound_constructor e constructor_name loc) @@
-            Environment.get_constructor constructor_name e in
+            O.CMap.find_opt (convert_constructor' constructor_name) variant_cases' in
           let e' = Environment.add_ez_binder pattern constructor e in
           let%bind body = f e' b in
           let constructor = convert_constructor' constructor_name in
           ok ({constructor ; pattern ; body} : O.matching_content_case)
         in
         bind_map_list aux lst in
-      ok (O.Match_variant { cases ; tv })
+      ok (O.Match_variant { cases ; tv=t })
 
 and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression result =
   let return tv' = ok (make_t ~loc:t.location tv' (Some t)) in
@@ -589,7 +586,7 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu
       let%bind type2 = evaluate_type e type2 in
       return (T_arrow {type1;type2})
   | T_sum m ->
-      let aux k ({ctor_type;michelson_annotation} : I.ctor_content) prev =
+      let aux k ({ctor_type;michelson_annotation;ctor_decl_pos} : I.ctor_content) prev =
         let%bind prev' = prev in
         let%bind ctor_type = evaluate_type e ctor_type in
         let%bind () = match Environment.get_constructor k e with
@@ -598,16 +595,16 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu
               ok ()
             else fail (redundant_constructor e k)
           | None -> ok () in
-        let v' : O.ctor_content = {ctor_type;michelson_annotation} in
+        let v' : O.ctor_content = {ctor_type;michelson_annotation;ctor_decl_pos} in
         ok @@ O.CMap.add (convert_constructor' k) v' prev'
       in
       let%bind m = I.CMap.fold aux m (ok O.CMap.empty) in
       return (T_sum m)
   | T_record m ->
-      let aux k ({field_type;field_annotation}: I.field_content) prev =
+      let aux k ({field_type;field_annotation;field_decl_pos}: I.field_content) prev =
         let%bind prev' = prev in
         let%bind field_type = evaluate_type e field_type in
-        let v' = ({field_type;michelson_annotation=field_annotation} : O.field_content) in
+        let v' = ({field_type;michelson_annotation=field_annotation;field_decl_pos} : O.field_content) in
         ok @@ O.LMap.add (convert_label k) v' prev'
       in
       let%bind m = I.LMap.fold aux m (ok O.LMap.empty) in
@@ -619,34 +616,60 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu
       ok tv
   | T_constant cst ->
       return (T_constant (convert_type_constant cst))
-  | T_operator opt ->
+  | T_operator opt -> ( match opt with
-      let%bind opt = match opt with
+    | TC_set s -> 
-        | TC_set s -> 
+        let%bind s = evaluate_type e s in 
-            let%bind s = evaluate_type e s in 
+        return @@ T_operator (O.TC_set (s))
-            ok @@ O.TC_set (s) 
+    | TC_option o -> 
-        | TC_option o -> 
+        let%bind o = evaluate_type e o in 
-            let%bind o = evaluate_type e o in 
+        return @@ T_operator (O.TC_option (o))
-            ok @@ O.TC_option (o) 
+    | TC_list l -> 
-        | TC_list l -> 
+        let%bind l = evaluate_type e l in 
-            let%bind l = evaluate_type e l in 
+        return @@ T_operator (O.TC_list (l))
-            ok @@ O.TC_list (l) 
+    | TC_map (k,v) ->
-        | TC_map (k,v) ->
+        let%bind k = evaluate_type e k in 
-            let%bind k = evaluate_type e k in 
+        let%bind v = evaluate_type e v in 
-            let%bind v = evaluate_type e v in 
+        return @@ T_operator (O.TC_map {k;v})
-            ok @@ O.TC_map {k;v}
+    | TC_big_map (k,v) ->
-        | TC_big_map (k,v) ->
+        let%bind k = evaluate_type e k in 
-            let%bind k = evaluate_type e k in 
+        let%bind v = evaluate_type e v in 
-            let%bind v = evaluate_type e v in 
+        return @@ T_operator (O.TC_big_map {k;v})
-            ok @@ O.TC_big_map {k;v}
+    | TC_map_or_big_map (k,v) ->
-        | TC_map_or_big_map (k,v) ->
+        let%bind k = evaluate_type e k in 
-            let%bind k = evaluate_type e k in 
+        let%bind v = evaluate_type e v in 
-            let%bind v = evaluate_type e v in 
+        return @@ T_operator (O.TC_map_or_big_map {k;v})
-            ok @@ O.TC_map_or_big_map {k;v}
+    | TC_contract c ->
-        | TC_contract c ->
+        let%bind c = evaluate_type e c in
-            let%bind c = evaluate_type e c in
+        return @@ T_operator (O.TC_contract c)
-            ok @@ O.TC_contract c
+    | TC_michelson_pair_right_comb c ->
-        in
+        let%bind c' = evaluate_type e c in
-      return (T_operator (opt))
+        let%bind lmap = match c'.type_content with
+          | T_record lmap when (not (Ast_typed.Helpers.is_tuple_lmap lmap)) -> ok lmap
+          | _ -> fail (michelson_comb_no_record t.location) in
+        let record = Operators.Typer.Converter.convert_pair_to_right_comb (Ast_typed.LMap.to_kv_list lmap) in
+        return @@ record
+    | TC_michelson_pair_left_comb c ->
+        let%bind c' = evaluate_type e c in
+        let%bind lmap = match c'.type_content with
+          | T_record lmap when (not (Ast_typed.Helpers.is_tuple_lmap lmap)) -> ok lmap
+          | _ -> fail (michelson_comb_no_record t.location) in
+        let record = Operators.Typer.Converter.convert_pair_to_left_comb (Ast_typed.LMap.to_kv_list lmap) in
+        return @@ record
+    | TC_michelson_or_right_comb c ->
+        let%bind c' = evaluate_type e c in
+        let%bind cmap = match c'.type_content with
+          | T_sum cmap -> ok cmap
+          | _ -> fail (michelson_comb_no_variant t.location) in
+        let pair = Operators.Typer.Converter.convert_variant_to_right_comb (Ast_typed.CMap.to_kv_list cmap) in
+        return @@ pair
+    | TC_michelson_or_left_comb c ->
+        let%bind c' = evaluate_type e c in
+        let%bind cmap = match c'.type_content with
+          | T_sum cmap -> ok cmap
+          | _ -> fail (michelson_comb_no_variant t.location) in
+        let pair = Operators.Typer.Converter.convert_variant_to_left_comb (Ast_typed.CMap.to_kv_list cmap) in
+        return @@ pair
+  )
 
 and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result
   = fun e _placeholder_for_state_of_new_typer ?tv_opt ae ->
@@ -759,7 +782,10 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
         ok (O.LMap.add (convert_label k) expr' prev)
       in
       let%bind m' = Stage_common.Helpers.bind_fold_lmap aux (ok O.LMap.empty) m in
-      let lmap = O.LMap.map (fun e -> ({field_type = get_type_expression e; michelson_annotation = None}:O.field_content)) m' in
+      (* let () = match tv_opt with
+        Some _ -> Format.printf "YES"
+       | None -> Format.printf "NO" in *)
+      let lmap = O.LMap.map (fun e -> ({field_type = get_type_expression e; michelson_annotation = None; field_decl_pos=0}:O.field_content)) m' in
       return (E_record m') (t_record lmap ())
   | E_record_update {record; path; update} ->
     let path = convert_label path in

src/passes/9-self_ast_typed/michelson_layout.ml

@@ -0,0 +1,278 @@
+open Ast_typed
+open Trace
+
+let to_sorted_kv_list_l lmap =
+  List.sort (fun (_,{field_decl_pos=a;_}) (_,{field_decl_pos=b;}) -> Int.compare a b) @@
+  LMap.to_kv_list lmap
+
+let to_sorted_kv_list_c lmap =
+  List.sort (fun (_,{ctor_decl_pos=a;_}) (_,{ctor_decl_pos=b;}) -> Int.compare a b) @@
+  CMap.to_kv_list lmap
+
+let accessor (record:expression) (path:label) (t:type_expression) =
+  { expression_content = E_record_accessor {record; path} ;
+    location = Location.generated ;
+    type_expression = t ;
+    environment = record.environment }
+
+let constructor (constructor:constructor') (element:expression) (t:type_expression) =
+  { expression_content = E_constructor { constructor ; element } ;
+    location = Location.generated ;
+    type_expression = t ;
+    environment = element.environment }
+
+let match_var (t:type_expression) =
+  { expression_content = E_variable (Var.of_name "x") ;
+    location = Location.generated ;
+    type_expression = t ;
+    environment = Environment.add_ez_binder (Var.of_name "x") t Environment.full_empty}
+
+let matching (e:expression) matchee cases =
+  { expression_content = E_matching {matchee ; cases};
+    location = Location.generated ;
+    type_expression = e.type_expression ;
+    environment = e.environment }
+
+let rec descend_types s lmap i =
+  if i > 0 then
+    let {ctor_type;_} = CMap.find (Constructor s) lmap in
+    match ctor_type.type_content with
+      | T_sum a -> ctor_type::(descend_types s a (i-1)) 
+      | _ -> []
+  else []
+
+let rec to_left_comb_record' first prev l conv_map =
+  match l with
+  | [] -> conv_map 
+  | (label_l, {field_type=t_l}) :: (label_r, {field_type=t_r})::tl when first ->
+    let exp_l = accessor prev label_l t_l in
+    let exp_r = accessor prev label_r t_r in
+    let conv_map' = LMap.add_bindings [ (Label "0" , exp_l) ; (Label "1" , exp_r) ] LMap.empty in
+    to_left_comb_record' false prev tl conv_map'
+  | (label, {field_type=t})::tl ->
+    let conv_map' = LMap.add_bindings [
+        (Label "0" , {prev with expression_content = E_record conv_map});
+        (Label "1" , accessor prev label t)]
+      LMap.empty in
+    to_left_comb_record' first prev tl conv_map'
+let to_left_comb_record = to_left_comb_record' true
+
+let rec right_comb_variant_combination' (i:int) (e:expression) (dst_lmap:ctor_content constructor_map) (src_kvl:(constructor' * ctor_content) list) : expression list =
+  let intermediary_types i =  if i = 0 then [] else e.type_expression::(descend_types "M_right" dst_lmap i) in
+  let rec comb (ctor_type,outer) l =
+    match l with
+    | [] -> constructor outer (match_var ctor_type) e.type_expression
+    | [t] -> constructor outer (match_var ctor_type) t
+    | t::tl -> constructor (Constructor "M_right") (comb (ctor_type,outer) tl) t in
+  ( match src_kvl with
+    | [] -> []
+    | (_,{ctor_type;_})::[] ->
+      let combs_t = intermediary_types (i-1) in
+      [comb (ctor_type,Constructor "M_right") combs_t]
+    | (_,{ctor_type;_})::tl ->
+      let combs_t = intermediary_types i in
+      (comb (ctor_type,Constructor "M_left") combs_t) :: right_comb_variant_combination' (i+1) e dst_lmap tl )
+let right_comb_variant_combination = right_comb_variant_combination' 0
+
+let rec left_comb_variant_combination' (i:int) (e:expression) (dst_lmap:ctor_content constructor_map) (src_kvl:(constructor' * ctor_content) list) : expression list =
+  let intermediary_types i =  if i = 0 then [] else e.type_expression::(descend_types "M_left" dst_lmap i) in
+  let rec comb (ctor_type,outer) l =
+    match l with
+    | [] -> constructor outer (match_var ctor_type) e.type_expression
+    | [t] -> constructor outer (match_var ctor_type) t
+    | t::tl -> constructor (Constructor "M_left") (comb (ctor_type,outer) tl) t in
+  ( match src_kvl with
+    | [] -> []
+    | (_,{ctor_type;_})::[] ->
+      let combs_t = intermediary_types (i-1) in
+      [comb (ctor_type,Constructor "M_left") combs_t]
+    | (_,{ctor_type;_})::tl ->
+      let combs_t = intermediary_types i in
+      (comb (ctor_type,Constructor "M_right") combs_t) :: left_comb_variant_combination' (i+1) e dst_lmap tl )
+let left_comb_variant_combination a b c = List.rev @@ left_comb_variant_combination' 0 a b (List.rev c)
+
+let rec to_right_comb_record
+    (prev:expression)
+    (l:(label * field_content) list)
+    (conv_map: expression label_map) : expression label_map =
+  match l with
+  | [] -> conv_map 
+  | [ (label_l,{field_type=tl}) ; (label_r,{field_type=tr}) ] ->
+    let exp_l = accessor prev label_l tl in
+    let exp_r = accessor prev label_r tr in
+    LMap.add_bindings [ (Label "0" , exp_l) ; (Label "1" , exp_r) ] conv_map
+  | (label,{field_type})::tl ->
+    let exp = { expression_content = E_record_accessor {record = prev ; path = label } ;
+                location = Location.generated ;
+                type_expression = field_type ;
+                environment = prev.environment } in
+    let conv_map' = LMap.add (Label "0") exp conv_map in
+    LMap.add (Label "1") ({exp with expression_content = E_record (to_right_comb_record prev tl conv_map')}) conv_map'
+
+let rec from_right_comb_record
+    (prev:expression) 
+    (src_lmap: field_content label_map)
+    (dst_kvl:(label * field_content) list)
+    (conv_map:expression label_map) : expression label_map =
+  match dst_kvl with
+  | (label , {field_type;_}) :: (_::_ as tl) ->
+    let intermediary_type = LMap.find (Label "1") src_lmap in
+    let src_lmap' = match intermediary_type.field_type.type_content with
+      | T_record a -> a
+      | _ -> src_lmap in
+    let conv_map' = LMap.add label (accessor prev (Label "0") field_type) conv_map in
+    let next = accessor prev (Label "1") intermediary_type.field_type in
+    from_right_comb_record next src_lmap' tl conv_map'
+  | [(label,_)] -> LMap.add label prev conv_map
+  | [] -> conv_map
+
+let rec from_left_comb_record
+    (prev:expression) 
+    (src_lmap: field_content label_map)
+    (dst_kvl:(label * field_content) list)
+    (conv_map:expression label_map) : expression label_map =
+  match dst_kvl with
+  | (label , {field_type;_}) :: (_::_ as tl) ->
+    let intermediary_type = LMap.find (Label "0") src_lmap in
+    let src_lmap' = match intermediary_type.field_type.type_content with
+      | T_record a -> a
+      | _ -> src_lmap in
+    let conv_map' = LMap.add label (accessor prev (Label "1") field_type) conv_map in
+    let next = accessor prev (Label "0") intermediary_type.field_type in
+    from_left_comb_record next src_lmap' tl conv_map'
+  | [(label,_)] -> LMap.add label prev conv_map
+  | [] -> conv_map
+let from_left_comb prev src_lmap dst_kvl conv_map =
+  from_left_comb_record prev src_lmap (List.rev dst_kvl) conv_map
+
+let rec from_right_comb_or (to_convert:expression) (e:expression) (matchee_t,bodies) : expression result =
+  match matchee_t , bodies with
+  | [m] , bl::br::[] ->
+    let cases = [
+      { constructor = Constructor "M_left" ;
+        pattern = Var.of_name "x";
+        body = bl } ;
+      { constructor = Constructor "M_right" ;
+        pattern = Var.of_name "x";
+        body = br } ] in
+    ok @@ matching e m (Match_variant { cases ; tv = to_convert.type_expression })
+  | m::mtl , b::btl ->
+    let%bind body = from_right_comb_or to_convert e (mtl,btl) in
+    let cases = [
+      { constructor = Constructor "M_left" ;
+        pattern = Var.of_name "x";
+        body = b } ;
+      { constructor = Constructor "M_right" ;
+        pattern = Var.of_name "x";
+        body } ] in
+    ok @@ matching e m (Match_variant { cases ; tv = to_convert.type_expression })
+  | _ -> simple_fail "corner case"
+
+let rec from_left_comb_or (to_convert:expression) (e:expression) (matchee_t,bodies) : expression result =
+  match matchee_t , bodies with
+  | [m] , bl::br::[] ->
+    let cases = [
+      { constructor = Constructor "M_right" ;
+        pattern = Var.of_name "x";
+        body = bl } ;
+      { constructor = Constructor "M_left" ;
+        pattern = Var.of_name "x";
+        body = br } ] in
+    ok @@ matching e m (Match_variant { cases ; tv = to_convert.type_expression })
+  | m::mtl , b::btl ->
+    let%bind body = from_left_comb_or to_convert e (mtl,btl) in
+    let cases = [
+      { constructor = Constructor "M_right" ;
+        pattern = Var.of_name "x";
+        body = b } ;
+      { constructor = Constructor "M_left" ;
+        pattern = Var.of_name "x";
+        body } ] in
+    ok @@ matching e m (Match_variant { cases ; tv = to_convert.type_expression })
+  | _ -> simple_fail "corner case"
+
+(**
+  converts pair/record of a given layout to record/pair to another
+  - foo = (a,(b,(c,d))) -> foo_converted = { a=foo.0 ; b=foo.1.0 ; c=foo.1.1.0 ; d=foo.1.1.1 }
+  - foo = M_left(a) -> foo_converted = match foo with M_left x -> Foo x | M_right x -> Bar x
+**)
+let peephole_expression : expression -> expression result = fun e ->
+  let return expression_content = ok { e with expression_content } in
+  match e.expression_content with
+  | E_constant {cons_name= (C_CONVERT_TO_LEFT_COMB);arguments= [ to_convert ] } -> (
+    match to_convert.type_expression.type_content with
+      | T_record src_lmap ->
+        let src_kvl = to_sorted_kv_list_l src_lmap in
+        return @@ E_record (to_left_comb_record to_convert src_kvl LMap.empty)
+      | T_sum src_cmap ->
+        let%bind dst_cmap = get_t_sum e.type_expression in
+        let src_kvl = to_sorted_kv_list_c src_cmap in
+        let bodies = left_comb_variant_combination e dst_cmap src_kvl in
+        let to_cases ((constructor,{ctor_type=_;_}),body) =
+          let pattern = (Var.of_name "x") in
+          {constructor ; pattern ; body }
+        in
+        let cases = Match_variant {
+          cases = List.map to_cases @@ (List.combine src_kvl bodies) ;
+          tv = to_convert.type_expression }
+        in
+        return @@ E_matching {matchee = to_convert ; cases}
+      | _ -> return e.expression_content
+  )
+  | E_constant {cons_name= (C_CONVERT_TO_RIGHT_COMB);arguments= [ to_convert ] } -> (
+    match to_convert.type_expression.type_content with
+      | T_record src_lmap ->
+        let src_kvl = to_sorted_kv_list_l src_lmap in
+        return @@ E_record (to_right_comb_record to_convert src_kvl LMap.empty)
+      | T_sum src_cmap ->
+        let%bind dst_cmap = get_t_sum e.type_expression in
+        let src_kvl = to_sorted_kv_list_c src_cmap in
+        let bodies = right_comb_variant_combination e dst_cmap src_kvl in
+        let to_cases ((constructor,{ctor_type=_;_}),body) =
+          let pattern = (Var.of_name "x") in
+          {constructor ; pattern ; body }
+        in
+        let cases = Match_variant {
+          cases = List.map to_cases @@ (List.combine src_kvl bodies) ;
+          tv = to_convert.type_expression }
+        in
+        return @@ E_matching {matchee = to_convert ; cases}
+      | _ -> return e.expression_content
+  )
+  | E_constant {cons_name= (C_CONVERT_FROM_RIGHT_COMB); arguments= [ to_convert ] } -> (
+    match to_convert.type_expression.type_content with
+      | T_record src_lmap ->
+        let%bind dst_lmap = get_t_record e.type_expression in
+        let dst_kvl = to_sorted_kv_list_l dst_lmap in
+        return @@ E_record (from_right_comb_record to_convert src_lmap dst_kvl LMap.empty)
+      | T_sum src_cmap ->
+        let%bind dst_lmap = get_t_sum e.type_expression in
+        let dst_kvl = to_sorted_kv_list_c dst_lmap in
+        let intermediary_types i = descend_types "M_right" src_cmap i in
+        let matchee = to_convert :: (List.map (fun t -> match_var t) @@ intermediary_types ((List.length dst_kvl)-2)) in
+        let bodies = List.map
+          (fun (ctor , {ctor_type;_}) -> constructor ctor (match_var ctor_type) e.type_expression)
+          dst_kvl in
+        let%bind match_expr = from_right_comb_or to_convert e (matchee,bodies) in
+        return match_expr.expression_content
+      | _ -> return e.expression_content
+  )
+  | E_constant {cons_name= (C_CONVERT_FROM_LEFT_COMB); arguments= [ to_convert ] } -> (
+    match to_convert.type_expression.type_content with
+      | T_record src_lmap ->
+        let%bind dst_lmap = get_t_record e.type_expression in
+        let dst_kvl = to_sorted_kv_list_l dst_lmap in
+        return @@ E_record (from_left_comb to_convert src_lmap dst_kvl LMap.empty)
+      | T_sum src_cmap ->
+        let%bind dst_lmap = get_t_sum e.type_expression in
+        let dst_kvl = to_sorted_kv_list_c dst_lmap in
+        let intermediary_types i = descend_types "M_left" src_cmap i in
+        let matchee = to_convert :: (List.map (fun t -> match_var t) @@ intermediary_types ((List.length dst_kvl)-2)) in
+        let bodies = List.map
+          (fun (ctor , {ctor_type;_}) -> constructor ctor (match_var ctor_type) e.type_expression)
+          (List.rev dst_kvl) in
+        let%bind match_expr = from_left_comb_or to_convert e (matchee,bodies) in
+        return match_expr.expression_content
+      | _ -> return e.expression_content
+  )
+  | _ as e -> return e

src/passes/9-self_ast_typed/self_ast_typed.ml

@@ -1,7 +1,8 @@
 open Trace
 
 let all_passes = [
-  Tail_recursion.peephole_expression
+  Tail_recursion.peephole_expression ;
+  Michelson_layout.peephole_expression ;
 ]
 
 let contract_passes = [

src/passes/operators/helpers.ml

@@ -133,6 +133,188 @@ module Typer = struct
       type_expression_eq (t_bool () , b) in
     ok @@ t_bool ()
 
+  module Converter = struct
+    open Ast_typed
+    open Trace
+
+    let record_checks kvl =
+      let%bind () = Assert.assert_true_err
+        (simple_error "converted record must have at least two elements")
+        (List.length kvl >=2) in
+      let all_undefined = List.for_all (fun (_,{field_decl_pos;_}) -> field_decl_pos = 0) kvl in
+      let%bind () = Assert.assert_true_err
+        (simple_error "can't retrieve type declaration order in the converted record, you need to annotate it")
+        (not all_undefined) in
+      ok ()
+
+    let variant_checks kvl =
+      let%bind () = Assert.assert_true_err
+        (simple_error "converted variant must have at least two elements")
+        (List.length kvl >=2) in
+      let all_undefined = List.for_all (fun (_,{ctor_decl_pos;_}) -> ctor_decl_pos = 0) kvl in
+      let%bind () = Assert.assert_true_err
+        (simple_error "can't retrieve type declaration order in the converted variant, you need to annotate it")
+        (not all_undefined) in
+      ok ()
+    
+    let annotate_field (field:field_content) (ann:string) : field_content =
+      {field with michelson_annotation=Some ann}
+
+    let annotate_ctor (ctor:ctor_content) (ann:string) : ctor_content =
+      {ctor with michelson_annotation=Some ann}
+
+    let comb_pair (t:type_content) : field_content =
+      let field_type = {
+        type_content = t ;
+        type_meta = None ;
+        location = Location.generated ; } in
+      {field_type ; michelson_annotation = Some "" ; field_decl_pos = 0}
+
+    let comb_ctor (t:type_content) : ctor_content =
+      let ctor_type = {
+        type_content = t ;
+        type_meta = None ;
+        location = Location.generated ; } in
+      {ctor_type ; michelson_annotation = Some "" ; ctor_decl_pos = 0}
+
+    let rec to_right_comb_pair l new_map =
+      match l with
+      | [] -> new_map
+      | [ (Label ann_l, field_content_l) ; (Label ann_r, field_content_r) ] ->
+        LMap.add_bindings [
+          (Label "0" , annotate_field field_content_l ann_l) ;
+          (Label "1" , annotate_field field_content_r ann_r) ] new_map
+      | (Label ann, field)::tl ->
+        let new_map' = LMap.add (Label "0") (annotate_field field ann) new_map in
+        LMap.add (Label "1") (comb_pair (T_record (to_right_comb_pair tl new_map'))) new_map'
+
+    let rec to_right_comb_variant l new_map =
+      match l with
+      | [] -> new_map
+      | [ (Constructor ann_l, field_content_l) ; (Constructor ann_r, field_content_r) ] ->
+        CMap.add_bindings [
+          (Constructor "M_left" , annotate_ctor field_content_l ann_l) ;
+          (Constructor "M_right" , annotate_ctor field_content_r ann_r) ] new_map
+      | (Constructor ann, field)::tl ->
+        let new_map' = CMap.add (Constructor "M_left") (annotate_ctor field ann) new_map in
+        CMap.add (Constructor "M_right") (comb_ctor (T_sum (to_right_comb_variant tl new_map'))) new_map'
+
+    let rec to_left_comb_pair' first l new_map =
+      match l with
+      | [] -> new_map
+      | (Label ann_l, field_content_l) :: (Label ann_r, field_content_r) ::tl when first ->
+        let new_map' = LMap.add_bindings [
+          (Label "0" , annotate_field field_content_l ann_l) ;
+          (Label "1" , annotate_field field_content_r ann_r) ] LMap.empty in
+        to_left_comb_pair' false tl new_map'
+      | (Label ann, field)::tl ->
+        let new_map' = LMap.add_bindings [
+          (Label "0" , comb_pair (T_record new_map)) ;
+          (Label "1" , annotate_field field ann ) ;] LMap.empty in
+        to_left_comb_pair' first tl new_map'
+    let to_left_comb_pair = to_left_comb_pair' true
+
+    let rec to_left_comb_variant' first l new_map =
+      match l with
+      | [] -> new_map
+      | (Constructor ann_l, ctor_content_l) :: (Constructor ann_r, ctor_content_r) ::tl when first ->
+        let new_map' = CMap.add_bindings [
+          (Constructor "M_left" , annotate_ctor ctor_content_l ann_l) ;
+          (Constructor "M_right" , annotate_ctor ctor_content_r ann_r) ] CMap.empty in
+        to_left_comb_variant' false tl new_map'
+      | (Constructor ann, ctor)::tl ->
+        let new_map' = CMap.add_bindings [
+          (Constructor "M_left" , comb_ctor (T_sum new_map)) ;
+          (Constructor "M_right" , annotate_ctor ctor ann ) ;] CMap.empty in
+        to_left_comb_variant' first tl new_map'
+    let to_left_comb_variant = to_left_comb_variant' true
+
+    let rec from_right_comb_pair (l:field_content label_map) (size:int) : (field_content list) result =
+      let l' = List.rev @@ LMap.to_kv_list l in
+      match l' , size with
+      | [ (_,l) ; (_,r) ] , 2 -> ok [ l ; r ]
+      | [ (_,l) ; (_,{field_type=tr;_}) ], _ ->
+        let%bind comb_lmap = get_t_record tr in
+        let%bind next = from_right_comb_pair comb_lmap (size-1) in
+        ok (l :: next)
+      | _ -> simple_fail "Could not convert michelson_pair_right_comb pair to a record"
+
+    let rec from_left_comb_pair (l:field_content label_map) (size:int) : (field_content list) result =
+      let l' = List.rev @@ LMap.to_kv_list l in
+      match l' , size with
+      | [ (_,l) ; (_,r) ] , 2 -> ok [ l ; r ]
+      | [ (_,{field_type=tl;_}) ; (_,r) ], _ ->
+        let%bind comb_lmap = get_t_record tl in
+        let%bind next = from_left_comb_pair comb_lmap (size-1) in
+        ok (List.append next [r])
+      | _ -> simple_fail "Could not convert michelson_pair_left_comb pair to a record"
+
+    let rec from_right_comb_variant (l:ctor_content constructor_map) (size:int) : (ctor_content list) result =
+      let l' = List.rev @@ CMap.to_kv_list l in
+      match l' , size with
+      | [ (_,l) ; (_,r) ] , 2 -> ok [ l ; r ]
+      | [ (_,l) ; (_,{ctor_type=tr;_}) ], _ ->
+        let%bind comb_cmap = get_t_sum tr in
+        let%bind next = from_right_comb_variant comb_cmap (size-1) in
+        ok (l :: next)
+      | _ -> simple_fail "Could not convert michelson_or right comb to a variant"
+
+    let rec from_left_comb_variant (l:ctor_content constructor_map) (size:int) : (ctor_content list) result =
+      let l' = List.rev @@ CMap.to_kv_list l in
+      match l' , size with
+      | [ (_,l) ; (_,r) ] , 2 -> ok [ l ; r ]
+      | [ (_,{ctor_type=tl;_}) ; (_,r) ], _ ->
+        let%bind comb_cmap = get_t_sum tl in
+        let%bind next = from_left_comb_variant comb_cmap (size-1) in
+        ok (List.append next [r])
+      | _ -> simple_fail "Could not convert michelson_or left comb to a record"
+
+    let convert_pair_to_right_comb l =
+      let l' = List.sort (fun (_,{field_decl_pos=a;_}) (_,{field_decl_pos=b;_}) -> Int.compare a b) l in
+      T_record (to_right_comb_pair l' LMap.empty)
+
+    let convert_pair_to_left_comb l =
+      let l' = List.sort (fun (_,{field_decl_pos=a;_}) (_,{field_decl_pos=b;_}) -> Int.compare a b) l in
+      T_record (to_left_comb_pair l' LMap.empty)
+    
+    let convert_pair_from_right_comb (src: field_content label_map) (dst: field_content label_map) : type_content result =
+      let%bind fields = from_right_comb_pair src (LMap.cardinal dst) in
+      let labels = List.map (fun (l,_) -> l) @@
+        List.sort (fun (_,{field_decl_pos=a;_}) (_,{field_decl_pos=b;_}) -> Int.compare a b ) @@
+        LMap.to_kv_list dst in
+      ok @@ (T_record (LMap.of_list @@ List.combine labels fields))
+
+    let convert_pair_from_left_comb (src: field_content label_map) (dst: field_content label_map) : type_content result =
+      let%bind fields = from_left_comb_pair src (LMap.cardinal dst) in
+      let labels = List.map (fun (l,_) -> l) @@
+        List.sort (fun (_,{field_decl_pos=a;_}) (_,{field_decl_pos=b;_}) -> Int.compare a b ) @@
+        LMap.to_kv_list dst in
+      ok @@ (T_record (LMap.of_list @@ List.combine labels fields))
+
+    let convert_variant_to_right_comb l =
+      let l' = List.sort (fun (_,{ctor_decl_pos=a;_}) (_,{ctor_decl_pos=b;_}) -> Int.compare a b) l in
+      T_sum (to_right_comb_variant l' CMap.empty)
+
+    let convert_variant_to_left_comb l =
+      let l' = List.sort (fun (_,{ctor_decl_pos=a;_}) (_,{ctor_decl_pos=b;_}) -> Int.compare a b) l in
+      T_sum (to_left_comb_variant l' CMap.empty)
+
+    let convert_variant_from_right_comb (src: ctor_content constructor_map) (dst: ctor_content constructor_map) : type_content result =
+      let%bind ctors = from_right_comb_variant src (CMap.cardinal dst) in
+      let ctors_name = List.map (fun (l,_) -> l) @@
+        List.sort (fun (_,{ctor_decl_pos=a;_}) (_,{ctor_decl_pos=b;_}) -> Int.compare a b ) @@
+        CMap.to_kv_list dst in
+      ok @@ (T_sum (CMap.of_list @@ List.combine ctors_name ctors))
+
+    let convert_variant_from_left_comb (src: ctor_content constructor_map) (dst: ctor_content constructor_map) : type_content result =
+      let%bind ctors = from_left_comb_variant src (CMap.cardinal dst) in
+      let ctors_name = List.map (fun (l,_) -> l) @@
+        List.sort (fun (_,{ctor_decl_pos=a;_}) (_,{ctor_decl_pos=b;_}) -> Int.compare a b ) @@
+        CMap.to_kv_list dst in
+      ok @@ (T_sum (CMap.of_list @@ List.combine ctors_name ctors))
+
+  end
+
 end
 
 module Compiler = struct

src/passes/operators/helpers.mli

@@ -53,6 +53,24 @@ module Typer : sig
   val comparator : string -> typer
   val boolean_operator_2 : string -> typer
 
+  module Converter : sig
+
+    open Ast_typed
+
+    val record_checks : (label * field_content) list -> unit result
+    val variant_checks : (constructor' * ctor_content) list -> unit result
+
+    val convert_pair_to_right_comb : (label * field_content) list -> type_content
+    val convert_pair_to_left_comb : (label * field_content) list -> type_content
+    val convert_pair_from_right_comb : field_content label_map -> field_content label_map -> type_content result
+    val convert_pair_from_left_comb : field_content label_map -> field_content label_map -> type_content result
+
+    val convert_variant_to_right_comb : (constructor' * ctor_content) list -> type_content
+    val convert_variant_to_left_comb : (constructor' * ctor_content) list -> type_content
+    val convert_variant_from_right_comb : ctor_content constructor_map -> ctor_content constructor_map -> type_content result
+    val convert_variant_from_left_comb : ctor_content constructor_map -> ctor_content constructor_map -> type_content result
+
+  end
 end
 
 module Compiler : sig

src/passes/operators/operators.ml

@@ -58,8 +58,11 @@ module Concrete_to_imperative = struct
     | "set"          -> Some (TC_set unit_expr)
     | "map"          -> Some (TC_map (unit_expr,unit_expr))
     | "big_map"      -> Some (TC_big_map (unit_expr,unit_expr))
-    | "michelson_or" -> Some (TC_michelson_or (unit_expr,"",unit_expr,""))
     | "contract"     -> Some (TC_contract unit_expr)
+    | "michelson_pair_right_comb" -> Some (TC_michelson_pair_right_comb unit_expr)
+    | "michelson_pair_left_comb" -> Some (TC_michelson_pair_left_comb unit_expr)
+    | "michelson_or_right_comb" -> Some (TC_michelson_or_right_comb unit_expr)
+    | "michelson_or_left_comb" -> Some (TC_michelson_or_left_comb unit_expr)
     | _              -> None
 
   let pseudo_modules = function
@@ -156,6 +159,13 @@ module Concrete_to_imperative = struct
     | "String.sub"      -> Some C_SLICE
     | "String.concat"   -> Some C_CONCAT
 
+    (* michelson pair/or type converter module *)
+
+    | "Layout.convert_to_right_comb" -> Some C_CONVERT_TO_RIGHT_COMB
+    | "Layout.convert_to_left_comb" -> Some C_CONVERT_TO_LEFT_COMB
+    | "Layout.convert_from_right_comb" -> Some C_CONVERT_FROM_RIGHT_COMB
+    | "Layout.convert_from_left_comb" -> Some C_CONVERT_FROM_LEFT_COMB
+
     | _ -> None
 
 
@@ -272,6 +282,9 @@ module Concrete_to_imperative = struct
     | "assert"          -> Some C_ASSERTION
     | "size"            -> Some C_SIZE (* Deprecated *)
     
+    | "Layout.convert_to_right_comb" -> Some C_CONVERT_TO_RIGHT_COMB
+    | "Layout.convert_to_left_comb" -> Some C_CONVERT_TO_LEFT_COMB
+
     | _ as c            -> pseudo_modules c
 
     let type_constants = type_constants
@@ -416,6 +429,8 @@ module Typer = struct
   open Helpers.Typer
   open Ast_typed
 
+  module Converter = Converter
+
   module Operators_types = struct
     open Typesystem.Shorthands
 
@@ -591,7 +606,7 @@ module Typer = struct
       | C_SELF_ADDRESS        -> ok @@ t_self_address;
       | C_IMPLICIT_ACCOUNT    -> ok @@ t_implicit_account;
       | C_SET_DELEGATE        -> ok @@ t_set_delegate ;
-      | c                     -> simple_fail @@ Format.asprintf "Typer not implemented for consant %a" Ast_typed.PP.constant c
+      | c                     -> simple_fail @@ Format.asprintf "Typer not implemented for constant %a" Ast_typed.PP.constant c
   end
 
   let none = typer_0 "NONE" @@ fun tv_opt ->
@@ -1155,6 +1170,62 @@ module Typer = struct
     let%bind () = assert_eq_1 hd elt in
     ok tl
 
+  let convert_to_right_comb = typer_1 "CONVERT_TO_RIGHT_COMB" @@ fun t ->
+    match t.type_content with
+      | T_record lmap ->
+        let kvl = LMap.to_kv_list lmap in
+        let%bind () = Converter.record_checks kvl in
+        let pair = Converter.convert_pair_to_right_comb kvl in
+        ok {t with type_content = pair}
+      | T_sum cmap ->
+        let kvl = CMap.to_kv_list cmap in
+        let%bind () = Converter.variant_checks kvl in
+        let michelson_or = Converter.convert_variant_to_right_comb kvl in
+        ok {t with type_content = michelson_or}
+      | _ -> simple_fail "converter can only be used on record or variants"
+
+  let convert_to_left_comb = typer_1 "CONVERT_TO_LEFT_COMB" @@ fun t ->
+    match t.type_content with
+      | T_record lmap ->
+        let kvl =  LMap.to_kv_list lmap in
+        let%bind () = Converter.record_checks kvl in
+        let pair = Converter.convert_pair_to_left_comb kvl in
+        ok {t with type_content = pair}
+      | T_sum cmap ->
+        let kvl = CMap.to_kv_list cmap in
+        let%bind () = Converter.variant_checks kvl in
+        let michelson_or = Converter.convert_variant_to_left_comb kvl in
+        ok {t with type_content = michelson_or}
+      | _ -> simple_fail "converter can only be used on record or variants"
+
+  let convert_from_right_comb = typer_1_opt "CONVERT_FROM_RIGHT_COMB" @@ fun t opt ->
+    match t.type_content with
+      | T_record src_lmap ->
+        let%bind dst_t = trace_option (simple_error "convert_from_right_comb must be annotated") opt in
+        let%bind dst_lmap = get_t_record dst_t in
+        let%bind record = Converter.convert_pair_from_right_comb src_lmap dst_lmap in
+        ok {t with type_content = record}
+      | T_sum src_cmap ->
+        let%bind dst_t = trace_option (simple_error "convert_from_right_comb must be annotated") opt in
+        let%bind dst_cmap = get_t_sum dst_t in
+        let%bind variant = Converter.convert_variant_from_right_comb src_cmap dst_cmap in
+        ok {t with type_content = variant}
+      | _ -> simple_fail "converter can only be used on record or variants"
+
+  let convert_from_left_comb = typer_1_opt "CONVERT_FROM_LEFT_COMB" @@ fun t opt ->
+    match t.type_content with
+      | T_record src_lmap ->
+        let%bind dst_t = trace_option (simple_error "convert_from_left_comb must be annotated") opt in
+        let%bind dst_lmap = get_t_record dst_t in
+        let%bind record = Converter.convert_pair_from_left_comb src_lmap dst_lmap in
+        ok {t with type_content = record}
+      | T_sum src_cmap ->
+        let%bind dst_t = trace_option (simple_error "convert_from_left_comb must be annotated") opt in
+        let%bind dst_cmap = get_t_sum dst_t in
+        let%bind variant = Converter.convert_variant_from_left_comb src_cmap dst_cmap in
+        ok {t with type_content = variant}
+      | _ -> simple_fail "converter can only be used on record or variants"
+  
   let constant_typers c : typer result = match c with
     | C_INT                 -> ok @@ int ;
     | C_UNIT                -> ok @@ unit ;
@@ -1247,7 +1318,11 @@ module Typer = struct
     | C_IMPLICIT_ACCOUNT    -> ok @@ implicit_account;
     | C_SET_DELEGATE        -> ok @@ set_delegate ;
     | C_CREATE_CONTRACT     -> ok @@ create_contract ;
-    | _                     -> simple_fail @@ Format.asprintf "Typer not implemented for consant %a" PP.constant c
+    | C_CONVERT_TO_RIGHT_COMB -> ok @@ convert_to_right_comb ;
+    | C_CONVERT_TO_LEFT_COMB  -> ok @@ convert_to_left_comb ;
+    | C_CONVERT_FROM_RIGHT_COMB -> ok @@ convert_from_right_comb ;
+    | C_CONVERT_FROM_LEFT_COMB  -> ok @@ convert_from_left_comb ;
+    | _                     -> simple_fail @@ Format.asprintf "Typer not implemented for constant %a" PP.constant c
 
 
 

src/passes/operators/operators.mli

@@ -171,6 +171,17 @@ module Typer : sig
   val cons : typer
   val constant_typers : constant' -> typer result
 
+  module Converter : sig
+
+    open Ast_typed
+
+    val record_checks : (label * field_content) list -> unit result
+    val convert_pair_to_right_comb : (label * field_content) list -> type_content
+    val convert_pair_to_left_comb : (label * field_content) list -> type_content
+    val convert_variant_to_right_comb : (constructor' * ctor_content) list -> type_content
+    val convert_variant_to_left_comb : (constructor'  * ctor_content) list -> type_content
+
+  end
 end
 
 module Compiler : sig

src/stages/1-ast_imperative/PP.ml

@@ -8,11 +8,17 @@ include Stage_common.PP
 let cmap_sep value sep ppf m =
   let lst = CMap.to_kv_list m in
   let lst = List.sort (fun (Constructor a,_) (Constructor b,_) -> String.compare a b) lst in
-  let new_pp ppf (k, v) = fprintf ppf "@[<h>%a -> %a@]" constructor k value v in
+  let new_pp ppf (k, ({ctor_type=v;_}:ctor_content)) = fprintf ppf "@[<h>%a -> %a@]" constructor k value v in
   fprintf ppf "%a" (list_sep new_pp sep) lst
 
 let cmap_sep_d x = cmap_sep x (tag " ,@ ")
 
+let record_sep_t value sep ppf (m : 'a label_map) =
+  let lst = LMap.to_kv_list m in
+  let lst = List.sort_uniq (fun (Label a,_) (Label b,_) -> String.compare a b) lst in
+  let new_pp ppf (k, ({field_type=v;_}:field_content)) = fprintf ppf "@[<h>%a -> %a@]" label k value v in
+  fprintf ppf "%a" (list_sep new_pp sep) lst
+
 let record_sep value sep ppf (m : 'a label_map) =
   let lst = LMap.to_kv_list m in
   let lst = List.sort_uniq (fun (Label a,_) (Label b,_) -> String.compare a b) lst in
@@ -30,7 +36,7 @@ let rec type_expression' :
   fun f ppf te ->
   match te.type_content with
   | T_sum m -> fprintf ppf "sum[%a]" (cmap_sep_d f) m
-  | T_record m -> fprintf ppf "{%a}" (record_sep f (const ";")) m
+  | T_record m -> fprintf ppf "{%a}" (record_sep_t f (const ";")) m
   | T_tuple t -> fprintf ppf "(%a)" (list_sep_d f) t
   | T_arrow a -> fprintf ppf "%a -> %a" f a.type1 f a.type2
   | T_variable tv -> type_variable ppf tv
@@ -55,6 +61,10 @@ and type_operator :
     | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v
     | TC_michelson_or (l,_, r,_) -> Format.asprintf "Michelson_or (%a,%a)" f l f r
     | TC_michelson_pair (l,_, r,_) -> Format.asprintf "Michelson_pair (%a,%a)" f l f r
+    | TC_michelson_pair_right_comb e -> Format.asprintf "michelson_pair_right_comb (%a)" f e
+    | TC_michelson_pair_left_comb e -> Format.asprintf "michelson_pair_left_comb (%a)" f e
+    | TC_michelson_or_right_comb e -> Format.asprintf "michelson_or_right_comb (%a)" f e
+    | TC_michelson_or_left_comb e -> Format.asprintf "michelson_or_left_comb (%a)" f e
     | TC_contract te  -> Format.asprintf "Contract (%a)" f te
   in
   fprintf ppf "(TO_%s)" s

src/stages/1-ast_imperative/combinators.ml

@@ -38,9 +38,9 @@ let t_option ?loc o       : type_expression = make_t ?loc @@ T_operator (TC_opti
 let t_list ?loc t         : type_expression = make_t ?loc @@ T_operator (TC_list t)
 let t_variable ?loc n     : type_expression = make_t ?loc @@ T_variable (Var.of_name n)
 let t_record_ez ?loc lst =
-  let lst = List.map (fun (k, v) -> (Label k, v)) lst in
+  let lst = List.mapi (fun i (k, v) -> (Label k, {field_type=v;field_decl_pos=i})) lst in
   let m = LMap.of_list lst in
-  make_t ?loc @@ T_record m
+  make_t ?loc @@ T_record (m:field_content label_map)
 let t_record ?loc m  : type_expression =
   let lst = Map.String.to_kv_list m in
   t_record_ez ?loc lst
@@ -49,9 +49,9 @@ let t_tuple ?loc lst    : type_expression = make_t ?loc @@ T_tuple lst
 let t_pair ?loc (a , b) : type_expression = t_tuple ?loc [a; b]
 
 let ez_t_sum ?loc (lst:(string * type_expression) list) : type_expression =
-  let aux prev (k, v) = CMap.add (Constructor k) v prev in
+  let aux (prev,i) (k, v) = (CMap.add (Constructor k) {ctor_type=v;ctor_decl_pos=i} prev, i+1) in
-  let map = List.fold_left aux CMap.empty lst in
+  let (map,_) = List.fold_left aux (CMap.empty,0) lst in
-  make_t ?loc @@ T_sum map
+  make_t ?loc @@ T_sum (map: ctor_content constructor_map)
 let t_sum ?loc m : type_expression =
   let lst = Map.String.to_kv_list m in
   ez_t_sum ?loc lst
@@ -63,6 +63,10 @@ let t_set ?loc key               : type_expression = make_t ?loc @@ T_operator (
 let t_contract ?loc contract     : type_expression = make_t ?loc @@ T_operator (TC_contract contract)
 let t_michelson_or ?loc l l_ann r r_ann : type_expression = make_t ?loc @@ T_operator (TC_michelson_or (l, l_ann, r, r_ann))
 let t_michelson_pair ?loc l l_ann r r_ann : type_expression = make_t ?loc @@ T_operator (TC_michelson_pair (l, l_ann, r, r_ann))
+let t_michelson_pair_right_comb ?loc c : type_expression = make_t ?loc @@ T_operator (TC_michelson_pair_right_comb c) 
+let t_michelson_pair_left_comb ?loc c : type_expression = make_t ?loc @@ T_operator (TC_michelson_pair_left_comb c) 
+let t_michelson_or_right_comb ?loc c : type_expression = make_t ?loc @@ T_operator (TC_michelson_or_right_comb c) 
+let t_michelson_or_left_comb ?loc c : type_expression = make_t ?loc @@ T_operator (TC_michelson_or_left_comb c) 
 
 (* TODO find a better way than using list*)
 let t_operator ?loc op lst: type_expression result =
@@ -74,6 +78,10 @@ let t_operator ?loc op lst: type_expression result =
   | TC_big_map (_,_) , [kt;vt] -> ok @@ t_big_map ?loc kt vt
   | TC_michelson_or (_,l_ann,_,r_ann) , [l;r] -> ok @@ t_michelson_or ?loc l l_ann r r_ann
   | TC_contract _    , [t] -> ok @@ t_contract t
+  | TC_michelson_pair_right_comb _ , [c] -> ok @@ t_michelson_pair_right_comb c
+  | TC_michelson_pair_left_comb _ , [c] -> ok @@ t_michelson_pair_left_comb c
+  | TC_michelson_or_right_comb _ , [c] -> ok @@ t_michelson_or_right_comb c
+  | TC_michelson_or_left_comb _ , [c] -> ok @@ t_michelson_or_left_comb c
   | _ , _ -> fail @@ bad_type_operator op
 
 let make_e ?(loc = Location.generated) expression_content =

src/stages/1-ast_imperative/types.ml

@@ -5,8 +5,8 @@ module Location = Simple_utils.Location
 include Stage_common.Types
 
 type type_content =
-  | T_sum of type_expression constructor_map
+  | T_sum of ctor_content constructor_map
-  | T_record of type_expression label_map
+  | T_record of field_content label_map
   | T_tuple  of type_expression list
   | T_arrow of arrow
   | T_variable of type_variable
@@ -15,6 +15,10 @@ type type_content =
 
 and arrow = {type1: type_expression; type2: type_expression}
 
+and field_content = {field_type : type_expression ; field_decl_pos : int} 
+
+and ctor_content = {ctor_type : type_expression ; ctor_decl_pos : int} 
+
 and michelson_prct_annotation = string
 
 and type_operator =
@@ -26,6 +30,10 @@ and type_operator =
   | TC_big_map of type_expression * type_expression
   | TC_michelson_or of type_expression * michelson_prct_annotation * type_expression * michelson_prct_annotation
   | TC_michelson_pair of type_expression * michelson_prct_annotation * type_expression * michelson_prct_annotation
+  | TC_michelson_or_right_comb of type_expression
+  | TC_michelson_or_left_comb of type_expression
+  | TC_michelson_pair_right_comb of type_expression
+  | TC_michelson_pair_left_comb of type_expression
 
 and type_expression = {type_content: type_content; location: Location.t}
 

src/stages/2-ast_sugar/PP.ml

@@ -52,6 +52,10 @@ and type_operator : (formatter -> type_expression -> unit) -> formatter -> type_
     | 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 te  -> Format.asprintf "Contract (%a)" f te
+    | TC_michelson_pair_right_comb c -> Format.asprintf "michelson_pair_right_comb (%a)" f c
+    | TC_michelson_pair_left_comb c -> Format.asprintf "michelson_pair_left_comb (%a)" f c
+    | TC_michelson_or_right_comb c -> Format.asprintf "michelson_or_right_comb (%a)" f c
+    | TC_michelson_or_left_comb c -> Format.asprintf "michelson_or_left_comb (%a)" f c
   in
   fprintf ppf "(TO_%s)" s
 

src/stages/2-ast_sugar/combinators.ml

@@ -52,8 +52,8 @@ let t_record ?loc m  : type_expression =
   t_record_ez ?loc lst
 
 let t_pair ?loc (a , b) : type_expression = t_record_ez ?loc [
-  ("0",{field_type=a;michelson_annotation=None}) ;
+  ("0",{field_type=a ; michelson_annotation=None ; field_decl_pos=0}) ;
-  ("1",{field_type=b;michelson_annotation=None})]
+  ("1",{field_type=b ; michelson_annotation=None ; field_decl_pos=0})]
 let t_tuple ?loc lst    : type_expression = t_record_ez ?loc (tuple_to_record lst)
 
 let ez_t_sum ?loc (lst:((string * ctor_content) list)) : type_expression =

src/stages/2-ast_sugar/types.ml

@@ -19,9 +19,9 @@ type type_content =
 
 and arrow = {type1: type_expression; type2: type_expression}
 
-and ctor_content = {ctor_type : type_expression ; michelson_annotation : string option}
+and ctor_content = {ctor_type : type_expression ; michelson_annotation : string option ; ctor_decl_pos : int}
 
-and field_content = {field_type : type_expression ; michelson_annotation : string option}
+and field_content = {field_type : type_expression ; michelson_annotation : string option ; field_decl_pos : int}
 
 and type_operator =
   | TC_contract of type_expression
@@ -30,6 +30,10 @@ and type_operator =
   | TC_set of type_expression
   | TC_map of type_expression * type_expression
   | TC_big_map of type_expression * type_expression
+  | TC_michelson_pair_right_comb of type_expression
+  | TC_michelson_pair_left_comb of type_expression
+  | TC_michelson_or_right_comb of type_expression
+  | TC_michelson_or_left_comb of type_expression
 
 and type_expression = {type_content: type_content; location: Location.t}
 

src/stages/4-ast_typed/PP.ml

@@ -175,6 +175,10 @@ let constant ppf : constant' -> unit = function
   | C_IMPLICIT_ACCOUNT      -> fprintf ppf "IMPLICIT_ACCOUNT"
   | C_SET_DELEGATE          -> fprintf ppf "SET_DELEGATE"
   | C_CREATE_CONTRACT       -> fprintf ppf "CREATE_CONTRACT"
+  | C_CONVERT_TO_RIGHT_COMB -> fprintf ppf "CONVERT_TO_RIGHT_COMB"
+  | C_CONVERT_TO_LEFT_COMB  -> fprintf ppf "CONVERT_TO_LEFT_COMB"
+  | C_CONVERT_FROM_RIGHT_COMB -> fprintf ppf "CONVERT_FROM_RIGHT_COMB"
+  | C_CONVERT_FROM_LEFT_COMB  -> fprintf ppf "CONVERT_FROM_LEFT_COMB"
 
 let literal ppf (l : literal) =
   match l with

src/stages/4-ast_typed/PP_generic.ml

@@ -12,6 +12,7 @@ let needs_parens              = {
     );
     type_variable             = (fun _ _ _ -> true) ;
     bool                      = (fun _ _ _ -> false) ;
+    int                       = (fun _ _ _ -> false) ;
     z                         = (fun _ _ _ -> false) ;
     string                    = (fun _ _ _ -> false) ;
     bytes                     = (fun _ _ _ -> false) ;
@@ -49,6 +50,7 @@ let op ppf = {
       | PolyInstance { poly=_; arguments=_; poly_continue } ->
          (poly_continue ())
     );
+    int                       = (fun _visitor () i               -> fprintf ppf "%i" i );
     type_variable             = (fun _visitor () type_variable   -> fprintf ppf "Var %a" Var.pp type_variable) ;
     bool                      = (fun _visitor () b               -> fprintf ppf "%s" (if b then "true" else "false")) ;
     z                         = (fun _visitor () i               -> fprintf ppf "%a" Z.pp_print i) ;

src/stages/4-ast_typed/combinators.ml

@@ -51,15 +51,19 @@ let t_list t ?loc ?s ()     : type_expression = make_t ?loc (T_operator (TC_list
 let t_set t ?loc ?s ()      : type_expression = make_t ?loc (T_operator (TC_set t)) s
 let t_contract t ?loc ?s () : type_expression = make_t ?loc (T_operator (TC_contract t)) s
 
+
 let t_record m ?loc ?s () : type_expression = make_t ?loc (T_record m) s
 let make_t_ez_record ?loc (lst:(string * type_expression) list) : type_expression =
-  let lst = List.map (fun (x,y) -> (Label x, {field_type=y;michelson_annotation=None}) ) lst in
+  let lst = List.mapi (fun i (x,y) -> (Label x, {field_type=y;michelson_annotation=None;field_decl_pos=i}) ) lst in
   let map = LMap.of_list lst in
   make_t ?loc (T_record map) None
 let ez_t_record lst ?loc ?s () : type_expression =
   let m = LMap.of_list lst in
   t_record m ?loc ?s ()
-let t_pair a b ?loc ?s ()   : type_expression = ez_t_record [(Label "0",{field_type=a;michelson_annotation=None}) ; (Label "1",{field_type=b;michelson_annotation=None})] ?loc ?s ()
+let t_pair a b ?loc ?s () : type_expression =
+  ez_t_record [
+    (Label "0",{field_type=a;michelson_annotation=None ; field_decl_pos = 0}) ;
+    (Label "1",{field_type=b;michelson_annotation=None ; field_decl_pos = 0}) ] ?loc ?s ()
 
 let t_map ?loc k v ?s () = make_t ?loc (T_operator (TC_map { k ; v })) s
 let t_big_map ?loc k v ?s () = make_t ?loc (T_operator (TC_big_map { k ; v })) s
@@ -72,7 +76,7 @@ let make_t_ez_sum ?loc ?s (lst:(constructor' * ctor_content) list) : type_expres
   make_t ?loc (T_sum map) s
 
 let t_bool ?loc ?s ()       : type_expression = make_t_ez_sum ?loc ?s
-  [(Constructor "true", {ctor_type=t_unit ();michelson_annotation=None});(Constructor "false", {ctor_type=t_unit ();michelson_annotation=None})]
+  [(Constructor "true", {ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=0});(Constructor "false", {ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=1})]
 
 let t_function param result ?loc ?s () : type_expression = make_t ?loc (T_arrow {type1=param; type2=result}) s
 let t_shallow_closure param result ?loc ?s () : type_expression = make_t ?loc (T_arrow {type1=param; type2=result}) s
@@ -183,7 +187,7 @@ let get_t_function_full (t:type_expression) : (type_expression * type_expression
     | _ -> ([],t)
   in
   let (input,output) = aux 0 t in
-  let input = List.map (fun (l,t) -> (l,{field_type = t ; michelson_annotation = None})) input in
+  let input = List.map (fun (l,t) -> (l,{field_type = t ; michelson_annotation = None ; field_decl_pos = 0})) input in
   ok @@ (t_record (LMap.of_list input) (),output) 
 
 let get_t_sum (t:type_expression) : ctor_content constructor_map result = match t.type_content with
@@ -242,6 +246,10 @@ let assert_t_list t =
   let%bind _ = get_t_list t in
   ok ()
 
+let assert_t_record t =
+  let%bind _ = get_t_record t in
+  ok ()
+
 let is_t_list = Function.compose to_bool get_t_list
 let is_t_set = Function.compose to_bool get_t_set
 let is_t_nat = Function.compose to_bool get_t_nat
@@ -324,11 +332,11 @@ let e_a_record r = make_e (e_record r) (t_record
   (LMap.map
     (fun t ->
       let field_type = get_type_expression t in
-      {field_type ; michelson_annotation=None} )
+      {field_type ; michelson_annotation=None ; field_decl_pos = 0} )
     r ) () )
 let e_a_application a b = make_e (e_application a b) (get_type_expression b)
 let e_a_variable v ty = make_e (e_variable v) ty
-let ez_e_a_record r = make_e (ez_e_record r) (ez_t_record (List.map (fun (x, y) -> x, {field_type = y.type_expression ; michelson_annotation = None}) r) ())
+let ez_e_a_record r = make_e (ez_e_record r) (ez_t_record (List.mapi (fun i (x, y) -> x, {field_type = y.type_expression ; michelson_annotation = None ; field_decl_pos = i}) r) ())
 let e_a_let_in binder expr body attributes = make_e (e_let_in binder expr body attributes) (get_type_expression body)
 
 

src/stages/4-ast_typed/combinators.mli

@@ -103,6 +103,7 @@ val assert_t_nat : type_expression -> unit result
 val assert_t_bool : type_expression -> unit result
 val assert_t_unit : type_expression -> unit result
 val assert_t_contract : type_expression -> unit result
+val assert_t_record : type_expression -> unit result
 (*
 val e_record : ae_map -> expression
 val ez_e_record : ( string * expression ) list -> expression

src/stages/4-ast_typed/dune

@@ -2,7 +2,7 @@
   (target generated_fold.ml)
   (deps ../adt_generator/generator.raku types.ml)
   (action (with-stdout-to generated_fold.ml (run perl6 ../adt_generator/generator.raku types.ml)))
-;  (mode (promote (until-clean)))
+  (mode (promote (until-clean) (only *)))
 )
 
 (library

src/stages/4-ast_typed/helpers.ml

@@ -163,7 +163,8 @@ let kv_list_of_record_or_tuple (m: _ LMap.t) =
 let remove_empty_annotation (ann : string option) : string option =
   match ann with
   | Some "" -> None
-  | _ -> ann
+  | Some ann -> Some (String.uncapitalize_ascii ann)
+  | None -> None
 
 let is_michelson_or (t: _ constructor_map) =
   CMap.cardinal t = 2 && 
@@ -174,8 +175,9 @@ let is_michelson_pair (t: _ label_map) =
   LMap.cardinal t = 2 && 
   let l = LMap.to_list t in
   List.fold_left
-    (fun prev {field_type=_;michelson_annotation} -> match michelson_annotation with
+    (fun prev {michelson_annotation;_} -> match michelson_annotation with
       | Some _ -> true
       | None -> prev)
     false 
-    l
+    l &&
+  List.for_all (fun i -> LMap.mem i t) @@ (label_range 0 (LMap.cardinal t))

src/stages/4-ast_typed/misc.ml

@@ -535,4 +535,4 @@ let p_constant (p_ctor_tag : constant_tag) (p_ctor_args : p_ctor_args) =
       p_ctor_args : p_ctor_args ;
     }
 
-let c_equation aval bval = C_equation { aval ; bval }
+let c_equation aval bval reason = { c = C_equation { aval ; bval }; reason }

src/stages/4-ast_typed/misc.mli

@@ -73,4 +73,4 @@ val get_entry : program -> string -> expression result
 val program_environment : program -> full_environment
 
 val p_constant : constant_tag -> p_ctor_args -> type_value
-val c_equation : type_value -> type_value -> type_constraint
+val c_equation : type_value -> type_value -> string -> type_constraint

src/stages/4-ast_typed/types.ml

@@ -40,11 +40,13 @@ and annot_option = string option
 and ctor_content = {
     ctor_type : type_expression;
     michelson_annotation : annot_option;
+    ctor_decl_pos : int;
 }
 
 and field_content = {
     field_type : type_expression;
     michelson_annotation : annot_option;
+    field_decl_pos : int;
 }
 
 and type_map_args = {
@@ -254,6 +256,10 @@ and constant' =
   | C_IMPLICIT_ACCOUNT
   | C_SET_DELEGATE
   | C_CREATE_CONTRACT
+  | C_CONVERT_TO_LEFT_COMB
+  | C_CONVERT_TO_RIGHT_COMB
+  | C_CONVERT_FROM_LEFT_COMB
+  | C_CONVERT_FROM_RIGHT_COMB
 
 and declaration_loc = declaration location_wrap
 
@@ -504,8 +510,11 @@ and c_access_label = {
     c_access_label_tvar : type_variable ;
   }
 
-(*What i was saying just before *)
+and type_constraint = {
-and type_constraint =
+  reason : string ;
+  c : type_constraint_ ;
+}
+and type_constraint_ =
   (* | C_assignment of (type_variable * type_pattern) *)
   | C_equation of c_equation (* TVA = TVB *)
   | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *)
@@ -564,7 +573,11 @@ and c_poly_simpl = {
   tv     : type_variable ;
   forall : p_forall      ;
 }
-and type_constraint_simpl =
+and type_constraint_simpl = {
+    reason_simpl : string ;
+    c_simpl : type_constraint_simpl_ ;
+  }
+and type_constraint_simpl_ =
   | SC_Constructor of c_constructor_simpl             (* α = ctor(β, …) *)
   | SC_Alias       of c_alias                         (* α = β *)
   | SC_Poly        of c_poly_simpl                    (* α = forall β, δ where δ can be a more complex type *)

src/stages/5-mini_c/PP.ml

@@ -248,6 +248,10 @@ and constant ppf : constant' -> unit = function
   | C_IMPLICIT_ACCOUNT      -> fprintf ppf "IMPLICIT_ACCOUNT"
   | C_SET_DELEGATE          -> fprintf ppf "SET_DELEGATE"
   | C_CREATE_CONTRACT       -> fprintf ppf "CREATE_CONTRACT"
+  | C_CONVERT_TO_RIGHT_COMB -> fprintf ppf "CONVERT_TO_RIGHT_COMB"
+  | C_CONVERT_TO_LEFT_COMB  -> fprintf ppf "CONVERT_TO_LEFT_COMB"
+  | C_CONVERT_FROM_RIGHT_COMB -> fprintf ppf "CONVERT_FROM_RIGHT_COMB"
+  | C_CONVERT_FROM_LEFT_COMB  -> fprintf ppf "CONVERT_FROM_LEFT_COMB"
 
 let%expect_test _ =
   Format.printf "%a" value (D_bytes (Bytes.of_string "foo")) ;

src/stages/common/PP.ml

@@ -125,6 +125,10 @@ let constant ppf : constant' -> unit = function
   | C_IMPLICIT_ACCOUNT      -> fprintf ppf "IMPLICIT_ACCOUNT"
   | C_SET_DELEGATE          -> fprintf ppf "SET_DELEGATE"
   | C_CREATE_CONTRACT       -> fprintf ppf "CREATE_CONTRACT"
+  | C_CONVERT_TO_RIGHT_COMB -> fprintf ppf "CONVERT_TO_RIGHT_COMB"
+  | C_CONVERT_TO_LEFT_COMB  -> fprintf ppf "CONVERT_TO_LEFT_COMB"
+  | C_CONVERT_FROM_RIGHT_COMB -> fprintf ppf "CONVERT_FROM_RIGHT_COMB"
+  | C_CONVERT_FROM_LEFT_COMB  -> fprintf ppf "CONVERT_FROM_LEFT_COMB"
 
 let literal ppf (l : literal) =
   match l with
@@ -250,6 +254,10 @@ module Ast_PP_type (PARAMETER : AST_PARAMETER_TYPE) = struct
       | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v
       | TC_map_or_big_map (k, v) -> Format.asprintf "Map Or Big Map (%a,%a)" f k f v
       | TC_contract te  -> Format.asprintf "Contract (%a)" f te
+      | TC_michelson_pair_right_comb c -> Format.asprintf "michelson_pair_right_comb (%a)" f c
+      | TC_michelson_pair_left_comb c -> Format.asprintf "michelson_pair_left_comb (%a)" f c
+      | TC_michelson_or_right_comb c -> Format.asprintf "michelson_or_right_comb (%a)" f c
+      | TC_michelson_or_left_comb c -> Format.asprintf "michelson_or_left_comb (%a)" f c
     in
     fprintf ppf "(type_operator: %s)" s
 end

src/stages/common/types.ml

@@ -47,9 +47,9 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
 
   and arrow = {type1: type_expression; type2: type_expression}
   
-  and ctor_content = {ctor_type : type_expression ; michelson_annotation : string option}
+  and ctor_content = {ctor_type : type_expression ; michelson_annotation : string option ; ctor_decl_pos : int}
 
-  and field_content = {field_type : type_expression ; field_annotation : string option}
+  and field_content = {field_type : type_expression ; field_annotation : string option ; field_decl_pos : int}
 
   and type_operator =
     | TC_contract of type_expression
@@ -59,6 +59,10 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | TC_map of type_expression * type_expression
     | TC_big_map of type_expression * type_expression
     | TC_map_or_big_map of type_expression * type_expression
+    | TC_michelson_pair_right_comb of type_expression
+    | TC_michelson_pair_left_comb of type_expression
+    | TC_michelson_or_right_comb of type_expression
+    | TC_michelson_or_left_comb of type_expression
 
 
   and type_expression = {type_content: type_content; location: Location.t; type_meta: type_meta}
@@ -72,6 +76,10 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | TC_map (x , y) -> TC_map (f x , f y)
     | TC_big_map (x , y)-> TC_big_map (f x , f y)
     | TC_map_or_big_map (x , y)-> TC_map_or_big_map (f x , f y)
+    | TC_michelson_pair_right_comb c -> TC_michelson_pair_right_comb (f c)
+    | TC_michelson_pair_left_comb c -> TC_michelson_pair_left_comb (f c)
+    | TC_michelson_or_right_comb c -> TC_michelson_or_right_comb (f c)
+    | TC_michelson_or_left_comb c -> TC_michelson_or_left_comb (f c)
 
   let bind_map_type_operator f = function
       TC_contract x -> let%bind x = f x in ok @@ TC_contract x
@@ -81,6 +89,10 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | 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_map_or_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_map_or_big_map (x , y)
+    | TC_michelson_pair_right_comb c -> let%bind c = f c in ok @@ TC_michelson_pair_right_comb c
+    | TC_michelson_pair_left_comb c -> let%bind c = f c in ok @@ TC_michelson_pair_left_comb c
+    | TC_michelson_or_right_comb c -> let%bind c = f c in ok @@ TC_michelson_or_right_comb c
+    | TC_michelson_or_left_comb c -> let%bind c = f c in ok @@ TC_michelson_or_left_comb c
 
   let type_operator_name = function
         TC_contract _ -> "TC_contract"
@@ -90,6 +102,10 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
       | TC_map      _ -> "TC_map"
       | TC_big_map  _ -> "TC_big_map"
       | TC_map_or_big_map _ -> "TC_map_or_big_map"
+      | TC_michelson_pair_right_comb _ -> "TC_michelson_pair_right_comb" 
+      | TC_michelson_pair_left_comb _ -> "TC_michelson_pair_left_comb" 
+      | TC_michelson_or_right_comb _ -> "TC_michelson_or_right_comb" 
+      | TC_michelson_or_left_comb _ -> "TC_michelson_or_left_comb" 
 
   let type_expression'_of_string = function
     | "TC_contract" , [x]     -> ok @@ T_operator(TC_contract x)
@@ -127,6 +143,10 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
     | TC_map            (x , y) -> "TC_map"          , [x ; y]
     | TC_big_map        (x , y) -> "TC_big_map"      , [x ; y]
     | TC_map_or_big_map (x , y) -> "TC_map_or_big_map"  , [x ; y]
+    | TC_michelson_pair_right_comb c -> "TC_michelson_pair_right_comb" , [c]
+    | TC_michelson_pair_left_comb c -> "TC_michelson_pair_left_comb" , [c]
+    | TC_michelson_or_right_comb c -> "TC_michelson_or_right_comb" , [c]
+    | TC_michelson_or_left_comb c -> "TC_michelson_or_left_comb" , [c]
 
   let string_of_type_constant = function
     | TC_unit      -> "TC_unit", []
@@ -294,3 +314,7 @@ and constant' =
   | C_IMPLICIT_ACCOUNT
   | C_SET_DELEGATE
   | C_CREATE_CONTRACT
+  | C_CONVERT_TO_LEFT_COMB
+  | C_CONVERT_TO_RIGHT_COMB
+  | C_CONVERT_FROM_LEFT_COMB
+  | C_CONVERT_FROM_RIGHT_COMB

src/stages/typesystem/misc.ml

@@ -245,7 +245,10 @@ module Substitution = struct
           )
         )
 
-    and constraint_ ~c ~substs =
+    and constraint_ ~c:{c;reason} ~substs =
+      {c = constraint__ ~c ~substs;reason}
+
+    and constraint__ ~c ~substs =
       match c with
       | C_equation { aval; bval } -> (
         let aux tv = type_value ~tv ~substs in

src/stages/typesystem/shorthands.ml

@@ -3,7 +3,7 @@ open Core
 open Ast_typed.Misc
 
 let tc type_vars allowed_list : type_constraint =
-  C_typeclass {tc_args = type_vars ; typeclass = allowed_list}
+  { c = C_typeclass {tc_args = type_vars ; typeclass = allowed_list} ; reason = "shorthands: typeclass" }
 
 let forall binder f =
   let () = ignore binder in

src/test/adt_generator/.gitignore

@@ -0,0 +1 @@
+/generated_fold.ml

src/test/adt_generator/dune

@@ -2,7 +2,7 @@
   (target generated_fold.ml)
   (deps ../../../src/stages/adt_generator/generator.raku amodule.ml)
   (action (with-stdout-to generated_fold.ml (run perl6 ../../../src/stages/adt_generator/generator.raku amodule.ml)))
-;  (mode (promote (until-clean)))
+  (mode (promote (until-clean) (only *)))
 )
 
 (executable

src/test/contracts/michelson_comb_type_operators.mligo

@@ -0,0 +1,10 @@
+type t3 = { foo : int ; bar : nat ;  baz : string}
+
+type param_r = t3 michelson_pair_right_comb
+type param_l = t3 michelson_pair_left_comb
+
+let main_r (action, store : param_r * unit) : (operation list * unit) =
+ ([] : operation list),  unit
+
+let main_l (action, store : param_l * unit) : (operation list * unit) =
+ ([] : operation list),  unit

src/test/contracts/michelson_converter_mixed_pair_or.mligo

@@ -0,0 +1,34 @@
+
+type foo = {
+  bar : string;
+  baz : nat;
+}
+
+type foo_michelson = foo michelson_pair_right_comb
+
+type union1 =
+| Choice1 of foo
+| Choice2 of foo
+
+type union1_aux =
+| Option1 of foo_michelson
+| Option2 of foo_michelson
+
+type union1_michelson = union1_aux michelson_or_right_comb
+
+let union1_from_michelson (m : union1_michelson) : union1 =
+ let aux : union1_aux = Layout.convert_from_right_comb m in
+ match aux with
+ | Option1 fm ->
+  let f : foo = Layout.convert_from_right_comb fm in
+  Choice1 f
+| Option2 fm ->
+  let f : foo = Layout.convert_from_right_comb fm in
+  Choice2 f
+
+let main2 (pm, s : union1_michelson * nat) =
+  let p = union1_from_michelson pm in
+  match p with
+  | Choice1 f -> ([] : operation list), f.baz
+  | Choice2 f -> ([] : operation list), f.baz
+

src/test/contracts/michelson_converter_or.mligo

@@ -0,0 +1,43 @@
+type st4 =
+  | Foo4 of int
+  | Bar4 of nat
+  | Baz4 of string
+  | Boz4 of bool
+
+type st3 =
+  | Foo3 of int
+  | Bar3 of nat
+  | Baz3 of string
+
+(*convert from*)
+
+type tr3 = (string,"baz4",bool,"boz4")michelson_or
+type tr2 = (nat,"bar4",tr3,"") michelson_or
+type tr1 = (int,"foo4",tr2,"")michelson_or
+let vr : tr1 = M_right (M_right (M_left "eq":tr3):tr2)
+
+type tl3 = (int,"foo4",nat,"bar4")michelson_or
+type tl2 = (tl3,"",string,"baz4") michelson_or
+type tl1 = (tl2,"",bool,"boz4")michelson_or
+let vl : tl1 = M_left (M_right "eq":tl2)
+
+type param_r = st4 michelson_or_right_comb
+let main_r (p, s : param_r * st4) : (operation list * st4) =
+  let r4 : st4 = Layout.convert_from_right_comb p in
+  ([] : operation list), r4
+
+type param_l = st4 michelson_or_left_comb
+let main_l (p, s : param_l * st4) : (operation list * st4) =
+  let r4 : st4 = Layout.convert_from_left_comb p in
+  ([] : operation list), r4
+
+(** convert_to **)
+
+let vst3 = Bar3 3n
+let vst4 = Baz4 "eq"
+
+let str3 = Layout.convert_to_right_comb (vst3:st3)
+let str4 = Layout.convert_to_right_comb (vst4:st4)
+
+let stl3 = Layout.convert_to_left_comb (vst3:st3)
+let stl4 = Layout.convert_to_left_comb (vst4:st4)

src/test/contracts/michelson_converter_pair.mligo

@@ -0,0 +1,29 @@
+type t3 = { foo : int ; bar : nat ;  baz : string}
+type t4 = { one: int ; two : nat ; three : string ; four : bool}
+
+(*convert from*)
+
+let s = "eq"
+let test_input_pair_r = (1,(2n,(s,true)))
+let test_input_pair_l = (((1,2n), s), true)
+
+type param_r = t4 michelson_pair_right_comb
+let main_r (p, s : param_r * string) : (operation list * string) =
+  let r4 : t4 = Layout.convert_from_right_comb p in
+  ([] : operation list),  r4.three ^ p.1.1.0
+
+type param_l = t4 michelson_pair_left_comb
+let main_l (p, s : param_l * string) : (operation list * string) =
+  let r4 : t4 = Layout.convert_from_left_comb p in
+  ([] : operation list),  r4.three ^ p.0.1
+
+(*convert to*)
+
+let v3 = { foo = 2 ; bar = 3n ; baz = "q" }
+let v4 = { one = 2 ; two = 3n ; three = "q" ; four = true }
+
+let r3 = Layout.convert_to_right_comb (v3:t3)
+let r4 = Layout.convert_to_right_comb (v4:t4)
+
+let l3 = Layout.convert_to_left_comb (v3:t3)
+let l4 = Layout.convert_to_left_comb (v4:t4)

src/test/contracts/negative/michelson_converter_no_annotation.mligo

@@ -0,0 +1,4 @@
+type t4 = { one: int ; two : nat ; three : string ; four : bool}
+let v4 = { one = 2 ; two = 3n ; three = "q" ; four = true }
+
+let l4 = Layout.convert_to_left_comb v4

src/test/contracts/negative/michelson_converter_short_record.mligo

@@ -0,0 +1,4 @@
+type t1 = { foo : int }
+let v1 = { foo = 2 }
+
+let l1 = Layout.convert_to_left_comb (v1:t1)

src/test/typer_tests.ml

@@ -56,8 +56,8 @@ module TestExpressions = struct
 
   let constructor () : unit result =
     let variant_foo_bar : (Typed.constructor' * Typed.ctor_content) list = [
-        (Typed.Constructor "foo", {ctor_type = Typed.t_int () ; michelson_annotation = None});
+        (Typed.Constructor "foo", {ctor_type = Typed.t_int () ; michelson_annotation = None ; ctor_decl_pos = 0});
-        (Typed.Constructor "bar", {ctor_type = Typed.t_string () ; michelson_annotation = None}) ]
+        (Typed.Constructor "bar", {ctor_type = Typed.t_string () ; michelson_annotation = None ; ctor_decl_pos = 1}) ]
     in test_expression
       ~env:(E.env_sum_type variant_foo_bar)
       I.(e_constructor "foo" (e_int (Z.of_int 32)))

vendors/ligo-utils/simple-utils/trace.ml

@@ -752,6 +752,10 @@ module Assert = struct
      true -> ok ()
   | false -> simple_fail msg
 
+  let assert_true_err err = function
+    | true -> ok ()
+    | false -> fail err
+
   let assert_equal ?msg expected actual =
     assert_true ?msg (expected = actual)
 

vendors/ligo-utils/simple-utils/x_map.ml

@@ -6,6 +6,7 @@ module type S = sig
   val of_list : (key * 'a) list -> 'a t
   val to_list : 'a t -> 'a list
   val to_kv_list : 'a t -> (key * 'a) list
+  val add_bindings : (key * 'a) list -> 'a t -> 'a t
 end
 
 module Make(Ord : Map.OrderedType) : S with type key = Ord.t = struct
@@ -22,6 +23,10 @@ module Make(Ord : Map.OrderedType) : S with type key = Ord.t = struct
   let to_kv_list (t: 'a t) : (key * 'a) list =
     let aux k v prev = (k, v) :: prev in
     fold aux t []
+  
+  let add_bindings (kvl:(key * 'a) list) (m:'a t) =
+    let aux prev (k, v) = add k v prev in
+    List.fold_left aux m kvl
 end
 
 module String = Make(String)