Merge branch 'dev' into rinderknecht@pprint_comments

.gitlab-ci.yml

@@ -85,9 +85,11 @@ xrefcheck:
 .webide-e2e:
   extends: .nix
   only:
-    - merge_requests
-    - dev
-    - /^.*-run-dev$/
+    # Disabled for now unless the branch name contains webide, because a test in this job fails randomly
+    - /.*webide.*/
+    #- merge_requests
+    #- dev
+    #- /^.*-run-dev$/
   script:
     - nix-build nix -A ligo-editor.e2e
 

debug.cmd

@@ -0,0 +1 @@
+(echo '['; sed -ne '/###############################START_OF_JSON/,/###############################END_OF_JSON/{/^###############################.*_OF_JSON/d;p}' < '/home/suzanne/00ligopam/ligo/_build/default/src/test/_build/_tests/'*'/Integration (End to End).001.output'; echo '"end of json"]') > /tmp/js.json

src/bin/cli.ml

@@ -139,7 +139,7 @@ let optimize =
 
 module Helpers   = Ligo.Compile.Helpers
 module Compile   = Ligo.Compile
-module Uncompile = Ligo.Uncompile
+module Decompile = Ligo.Decompile
 module Run = Ligo.Run.Of_michelson
 
 let compile_file =
@@ -285,7 +285,7 @@ let compile_parameter =
 
 let interpret =
   let f expression init_file syntax amount balance sender source predecessor_timestamp display_format =
-    return_result ~display_format (Uncompile.Formatter.expression_format) @@
+    return_result ~display_format (Decompile.Formatter.expression_format) @@
       let%bind (decl_list,state,env) = match init_file with
         | Some init_file ->
           let%bind typed_prg,state = Compile.Utils.type_file init_file syntax Env in
@@ -299,7 +299,7 @@ let interpret =
       let%bind compiled_exp   = Compile.Of_mini_c.aggregate_and_compile_expression decl_list mini_c_exp in
       let%bind options        = Run.make_dry_run_options {predecessor_timestamp ; amount ; balance ; sender ; source } in
       let%bind runres         = Run.run_expression ~options compiled_exp.expr compiled_exp.expr_ty in
-      Uncompile.uncompile_expression typed_exp.type_expression runres
+      Decompile.Of_michelson.decompile_expression typed_exp.type_expression runres
   in
   let term =
     Term.(const f $ expression "EXPRESSION" 0 $ init_file $ syntax $ amount $ balance $ sender $ source $ predecessor_timestamp $ display_format ) in
@@ -345,7 +345,7 @@ let compile_storage =
 
 let dry_run =
   let f source_file entry_point storage input amount balance sender source predecessor_timestamp syntax display_format =
-    return_result ~display_format (Uncompile.Formatter.expression_format) @@
+    return_result ~display_format (Decompile.Formatter.expression_format) @@
       let%bind typed_prg,state = Compile.Utils.type_file source_file syntax (Contract entry_point) in
       let      env             = Ast_typed.program_environment Environment.default typed_prg in
       let%bind mini_c_prg      = Compile.Of_typed.compile typed_prg in
@@ -359,7 +359,7 @@ let dry_run =
 
       let%bind options           = Run.make_dry_run_options {predecessor_timestamp ; amount ; balance ; sender ; source } in
       let%bind runres  = Run.run_contract ~options michelson_prg.expr michelson_prg.expr_ty args_michelson in
-      Uncompile.uncompile_typed_program_entry_function_result typed_prg entry_point runres
+      Decompile.Of_michelson.decompile_typed_program_entry_function_result typed_prg entry_point runres
     in
   let term =
     Term.(const f $ source_file 0 $ entry_point 1 $ expression "PARAMETER" 2 $ expression "STORAGE" 3 $ amount $ balance $ sender $ source $ predecessor_timestamp $ syntax $ display_format) in
@@ -369,7 +369,7 @@ let dry_run =
 
 let run_function =
   let f source_file entry_point parameter amount balance sender source predecessor_timestamp syntax display_format =
-    return_result ~display_format (Uncompile.Formatter.expression_format) @@
+    return_result ~display_format (Decompile.Formatter.expression_format) @@
       let%bind typed_prg,state = Compile.Utils.type_file source_file syntax Env in
       let      env             = Ast_typed.program_environment Environment.default typed_prg in
       let%bind mini_c_prg      = Compile.Of_typed.compile typed_prg in
@@ -386,7 +386,7 @@ let run_function =
       let%bind michelson        = Compile.Of_mini_c.aggregate_and_compile_expression mini_c_prg compiled_applied in
       let%bind options          = Run.make_dry_run_options {predecessor_timestamp ; amount ; balance ; sender ; source } in
       let%bind runres           = Run.run_expression ~options michelson.expr michelson.expr_ty in
-      Uncompile.uncompile_typed_program_entry_function_result typed_prg entry_point runres
+      Decompile.Of_michelson.decompile_typed_program_entry_function_result typed_prg entry_point runres
     in
   let term =
     Term.(const f $ source_file 0 $ entry_point 1 $ expression "PARAMETER" 2 $ amount $ balance $ sender $ source $ predecessor_timestamp $ syntax $ display_format) in
@@ -396,14 +396,14 @@ let run_function =
 
 let evaluate_value =
   let f source_file entry_point amount balance sender source predecessor_timestamp syntax display_format =
-    return_result ~display_format Uncompile.Formatter.expression_format @@
+    return_result ~display_format Decompile.Formatter.expression_format @@
       let%bind typed_prg,_ = Compile.Utils.type_file source_file syntax Env in
       let%bind mini_c      = Compile.Of_typed.compile typed_prg in
       let%bind (exp,_)     = trace_option Main_errors.entrypoint_not_found @@ Mini_c.get_entry mini_c entry_point in
       let%bind compiled    = Compile.Of_mini_c.aggregate_and_compile_expression mini_c exp in
       let%bind options     = Run.make_dry_run_options {predecessor_timestamp ; amount ; balance ; sender ; source } in
       let%bind runres      = Run.run_expression ~options compiled.expr compiled.expr_ty in
-      Uncompile.uncompile_typed_program_entry_expression_result typed_prg entry_point runres
+      Decompile.Of_michelson.decompile_typed_program_entry_expression_result typed_prg entry_point runres
     in
   let term =
     Term.(const f $ source_file 0 $ entry_point 1 $ amount $ balance $ sender $ source $ predecessor_timestamp $ syntax $ display_format) in
@@ -449,6 +449,41 @@ let list_declarations =
   let doc = "Subcommand: List all the top-level declarations." in
   (Term.ret term , Term.info ~doc cmdname)
 
+let transpile_contract =
+  let f source_file new_syntax syntax display_format =
+    return_result ~display_format (Parser.Formatter.ppx_format) @@
+      let%bind core       = Compile.Utils.to_core source_file syntax in
+      let%bind sugar      = Decompile.Of_core.decompile core in
+      let%bind imperative = Decompile.Of_sugar.decompile sugar in
+      let%bind buffer     = Decompile.Of_imperative.decompile imperative (Syntax_name new_syntax) in
+      ok @@ buffer
+  in
+  let term =
+    Term.(const f $ source_file 0 $ req_syntax 1 $ syntax $ display_format) in
+  let cmdname = "transpile-contract" in
+  let doc = "Subcommand: Transpile a contract to another syntax." in
+  (Term.ret term , Term.info ~doc cmdname)
+
+let transpile_expression =
+  let f expression new_syntax syntax display_format =
+    return_result ~display_format (Parser.Formatter.ppx_format) @@
+      let%bind v_syntax   = Helpers.syntax_to_variant (Syntax_name syntax) None in
+      let%bind n_syntax   = Decompile.Helpers.syntax_to_variant (Syntax_name new_syntax) None in
+      let%bind imperative = Compile.Of_source.compile_expression v_syntax expression in
+      let%bind sugar      = Compile.Of_imperative.compile_expression imperative in
+      let%bind core       = Compile.Of_sugar.compile_expression sugar in
+      let%bind sugar      = Decompile.Of_core.decompile_expression core in
+      let%bind imperative = Decompile.Of_sugar.decompile_expression sugar in
+      let%bind buffer     = Decompile.Of_imperative.decompile_expression imperative n_syntax in
+      ok @@ buffer
+  in
+  let term =
+    Term.(const f $ expression "" 1  $ req_syntax 2 $ req_syntax 0 $ display_format) in
+  let cmdname = "transpile-expression" in
+  let doc = "Subcommand: Transpile an expression to another syntax." in
+  (Term.ret term , Term.info ~doc cmdname)
+
+
 let run ?argv () =
   Term.eval_choice ?argv main [
     temp_ligo_interpreter ;
@@ -457,6 +492,8 @@ let run ?argv () =
     compile_parameter ;
     compile_storage ;
     compile_expression ;
+    transpile_contract ;
+    transpile_expression ;
     interpret ;
     dry_run ;
     run_function ;

src/bin/expect_tests/help_tests.ml

@@ -87,6 +87,12 @@ let%expect_test _ =
            run-function
                Subcommand: Run a function with the given parameter.
 
+           transpile-contract
+               Subcommand: Transpile a contract to another syntax.
+
+           transpile-expression
+               Subcommand: Transpile an expression to another syntax.
+
     OPTIONS
            --help[=FMT] (default=auto)
                Show this help in format FMT. The value FMT must be one of `auto',
@@ -181,6 +187,12 @@ let%expect_test _ =
            run-function
                Subcommand: Run a function with the given parameter.
 
+           transpile-contract
+               Subcommand: Transpile a contract to another syntax.
+
+           transpile-expression
+               Subcommand: Transpile an expression to another syntax.
+
     OPTIONS
            --help[=FMT] (default=auto)
                Show this help in format FMT. The value FMT must be one of `auto',

src/main/compile/helpers.ml

@@ -18,97 +18,97 @@ let syntax_to_variant (Syntax_name syntax) source =
   | _ -> fail (invalid_syntax syntax) 
 
 
-let parsify_pascaligo source =
+let parse_and_abstract_pascaligo source =
   let%bind raw = trace parser_tracer @@
     Parser.Pascaligo.parse_file source in
   let%bind imperative = trace cit_pascaligo_tracer @@
     Tree_abstraction.Pascaligo.compile_program raw
   in ok imperative
 
-let parsify_expression_pascaligo source =
+let parse_and_abstract_expression_pascaligo source =
   let%bind raw = trace parser_tracer @@
     Parser.Pascaligo.parse_expression source in
   let%bind imperative = trace cit_pascaligo_tracer @@
     Tree_abstraction.Pascaligo.compile_expression raw
   in ok imperative
 
-let parsify_cameligo source =
+let parse_and_abstract_cameligo source =
   let%bind raw = trace parser_tracer @@
     Parser.Cameligo.parse_file source in
   let%bind imperative = trace cit_cameligo_tracer @@
     Tree_abstraction.Cameligo.compile_program raw
   in ok imperative
 
-let parsify_expression_cameligo source =
+let parse_and_abstract_expression_cameligo source =
   let%bind raw = trace parser_tracer @@
     Parser.Cameligo.parse_expression source in
   let%bind imperative = trace cit_cameligo_tracer @@
     Tree_abstraction.Cameligo.compile_expression raw
   in ok imperative
 
-let parsify_reasonligo source =
+let parse_and_abstract_reasonligo source =
   let%bind raw = trace parser_tracer @@
     Parser.Reasonligo.parse_file source in
   let%bind imperative = trace cit_cameligo_tracer @@
     Tree_abstraction.Cameligo.compile_program raw
   in ok imperative
 
-let parsify_expression_reasonligo source =
+let parse_and_abstract_expression_reasonligo source =
   let%bind raw = trace parser_tracer @@
     Parser.Reasonligo.parse_expression source in
   let%bind imperative = trace cit_cameligo_tracer @@
     Tree_abstraction.Cameligo.compile_expression raw
   in ok imperative
 
-let parsify syntax source : (Ast_imperative.program, _) Trace.result =
-  let%bind parsify =
+let parse_and_abstract syntax source : (Ast_imperative.program, _) Trace.result =
+  let%bind parse_and_abstract =
     match syntax with
-      PascaLIGO  -> ok parsify_pascaligo
-    | CameLIGO   -> ok parsify_cameligo
-    | ReasonLIGO -> ok parsify_reasonligo in
-  let%bind parsified = parsify source in
+      PascaLIGO  -> ok parse_and_abstract_pascaligo
+    | CameLIGO   -> ok parse_and_abstract_cameligo
+    | ReasonLIGO -> ok parse_and_abstract_reasonligo in
+  let%bind parsified = parse_and_abstract source in
   let%bind applied = trace self_ast_imperative_tracer @@
     Self_ast_imperative.all_program parsified in
   ok applied
 
-let parsify_expression syntax source =
-  let%bind parsify = match syntax with
-    PascaLIGO  -> ok parsify_expression_pascaligo
-  | CameLIGO   -> ok parsify_expression_cameligo
-  | ReasonLIGO -> ok parsify_expression_reasonligo in
-  let%bind parsified = parsify source in
+let parse_and_abstract_expression syntax source =
+  let%bind parse_and_abstract = match syntax with
+    PascaLIGO  -> ok parse_and_abstract_expression_pascaligo
+  | CameLIGO   -> ok parse_and_abstract_expression_cameligo
+  | ReasonLIGO -> ok parse_and_abstract_expression_reasonligo in
+  let%bind parsified = parse_and_abstract source in
   let%bind applied = trace self_ast_imperative_tracer @@
     Self_ast_imperative.all_expression parsified
   in ok applied
 
-let parsify_string_reasonligo source =
+let parse_and_abstract_string_reasonligo source =
   let%bind raw = trace parser_tracer @@
     Parser.Reasonligo.parse_string source in
   let%bind imperative = trace cit_cameligo_tracer @@
     Tree_abstraction.Cameligo.compile_program raw
   in ok imperative
 
-let parsify_string_pascaligo source =
+let parse_and_abstract_string_pascaligo source =
   let%bind raw = trace parser_tracer @@
     Parser.Pascaligo.parse_string source in
   let%bind imperative = trace cit_pascaligo_tracer @@
     Tree_abstraction.Pascaligo.compile_program raw
   in ok imperative
 
-let parsify_string_cameligo source =
+let parse_and_abstract_string_cameligo source =
   let%bind raw = trace parser_tracer @@
     Parser.Cameligo.parse_string source in
   let%bind imperative = trace cit_cameligo_tracer @@
     Tree_abstraction.Cameligo.compile_program raw
   in ok imperative
 
-let parsify_string syntax source =
-  let%bind parsify =
+let parse_and_abstract_string syntax source =
+  let%bind parse_and_abstract =
     match syntax with
-      PascaLIGO  -> ok parsify_string_pascaligo
-    | CameLIGO   -> ok parsify_string_cameligo
-    | ReasonLIGO -> ok parsify_string_reasonligo in
-  let%bind parsified = parsify source in
+      PascaLIGO  -> ok parse_and_abstract_string_pascaligo
+    | CameLIGO   -> ok parse_and_abstract_string_cameligo
+    | ReasonLIGO -> ok parse_and_abstract_string_reasonligo in
+  let%bind parsified = parse_and_abstract source in
   let%bind applied = trace self_ast_imperative_tracer @@
     Self_ast_imperative.all_program parsified
   in ok applied

src/main/compile/of_core.ml

@@ -18,17 +18,18 @@ let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * Ty
 let compile_expression ?(env = Ast_typed.Environment.empty) ~(state : Typesystem.Solver_types.typer_state) (e : Ast_core.expression)
     : (Ast_typed.expression * Typesystem.Solver_types.typer_state , _) result =
   let%bind (ae_typed,state) = trace typer_tracer @@ Typer.type_expression_subst env state e in
-  let () = Typer.Solver.discard_state state in
   let%bind ae_typed' = trace self_ast_typed_tracer @@ Self_ast_typed.all_expression ae_typed in
   ok @@ (ae_typed',state)
 
 let apply (entry_point : string) (param : Ast_core.expression) : (Ast_core.expression , _) result =
   let name = Var.of_name entry_point in
   let entry_point_var : Ast_core.expression =
-    { expression_content = Ast_core.E_variable name ;
+    { content  = Ast_core.E_variable name ;
+      sugar    = None ;
       location = Virtual "generated entry-point variable" } in
   let applied : Ast_core.expression = 
-    { expression_content = Ast_core.E_application {lamb=entry_point_var; args=param} ;
+    { content  = Ast_core.E_application {lamb=entry_point_var; args=param} ;
+      sugar    = None ;
       location = Virtual "generated application" } in
   ok applied
 

src/main/compile/of_imperative.ml

@@ -3,10 +3,6 @@ open Trace
 open Ast_imperative
 open Purification
 
-type form = 
-  | Contract of string
-  | Env
-
 let compile (program : program) : (Ast_sugar.program, _) result =
   trace purification_tracer @@ compile_program program
 

src/main/compile/of_source.ml

@@ -3,16 +3,16 @@ open Helpers
 
 let compile (source_filename:string) syntax : (Ast_imperative.program , _) result =
   let%bind syntax = syntax_to_variant syntax (Some source_filename) in
-  let%bind abstract = parsify syntax source_filename in
+  let%bind abstract = parse_and_abstract syntax source_filename in
   ok abstract
 
 let compile_string (source:string) syntax : (Ast_imperative.program , _) result =
-  let%bind abstract = parsify_string syntax source in
+  let%bind abstract = parse_and_abstract_string syntax source in
   ok abstract
 
 let compile_expression : v_syntax -> string -> (Ast_imperative.expression , _) result =
     fun syntax exp ->
-  parsify_expression syntax exp
+  parse_and_abstract_expression syntax exp
 
 let compile_contract_input : string -> string -> v_syntax -> (Ast_imperative.expression , _) result =
     fun storage parameter syntax ->

src/main/compile/of_sugar.ml

@@ -3,10 +3,6 @@ open Ast_sugar
 open Desugaring
 open Main_errors
 
-type form = 
-  | Contract of string
-  | Env
-
 let compile (program : program) : (Ast_core.program , _) result =
   trace desugaring_tracer @@ compile_program program
 

src/main/decompile/dune

@@ -1,17 +1,30 @@
 (library
-  (name uncompile)
-  (public_name ligo.uncompile)
+  (name decompile)
+  (public_name ligo.decompile)
   (libraries
+    main_errors
     simple-utils
+    tezos-utils
+    parser
+    tree_abstraction
+    ast_imperative
+    self_ast_imperative
     purification
+    ast_sugar
+    self_ast_sugar
     desugaring
+    ast_core
+    self_ast_core
     typer_new
     typer
     ast_typed
+    self_ast_typed
+    interpreter
     spilling
     mini_c
+    self_mini_c
     stacking
-    main_errors
+    self_michelson
   )
   (preprocess
     (pps ppx_let bisect_ppx --conditional)

src/main/decompile/helpers.ml

@@ -0,0 +1,78 @@
+open Trace
+open Main_errors
+
+type s_syntax = Syntax_name of string
+type v_syntax = PascaLIGO | CameLIGO | ReasonLIGO
+
+let syntax_to_variant (Syntax_name syntax) source =
+  match syntax, source with
+    "auto", Some sf ->
+      (match Filename.extension sf with
+         ".ligo" | ".pligo" -> ok PascaLIGO
+       | ".mligo"           -> ok CameLIGO
+       | ".religo"          -> ok ReasonLIGO
+       | ext                -> fail (syntax_auto_detection ext))
+  | ("pascaligo" | "PascaLIGO"),   _ -> ok PascaLIGO
+  | ("cameligo" | "CameLIGO"),     _ -> ok CameLIGO
+  | ("reasonligo" | "ReasonLIGO"), _ -> ok ReasonLIGO
+  | _ -> fail (invalid_syntax syntax) 
+
+let specialise_and_print_pascaligo program =
+  let%bind cst = trace cit_pascaligo_tracer @@
+    Tree_abstraction.Pascaligo.decompile_program program in
+  let%bind source = trace pretty_tracer @@
+    Parser.Pascaligo.pretty_print cst
+  in ok source
+
+let specialise_and_print_expression_pascaligo expression =
+  let%bind cst = trace cit_pascaligo_tracer @@
+    Tree_abstraction.Pascaligo.decompile_expression expression in
+  let%bind source = trace pretty_tracer @@
+    Parser.Pascaligo.pretty_print_expression cst
+  in ok source
+
+let specialise_and_print_cameligo program =
+  let%bind cst = trace cit_cameligo_tracer @@
+    Tree_abstraction.Cameligo.decompile_program program in
+  let%bind source = trace pretty_tracer @@
+    Parser.Cameligo.pretty_print cst
+  in ok source
+
+let specialise_and_print_expression_cameligo expression =
+  let%bind cst = trace cit_cameligo_tracer @@
+    Tree_abstraction.Cameligo.decompile_expression expression in
+  let%bind source = trace pretty_tracer @@
+    Parser.Cameligo.pretty_print_expression cst
+  in ok source
+
+let specialise_and_print_reasonligo program =
+  let%bind cst = trace cit_cameligo_tracer @@
+    Tree_abstraction.Cameligo.decompile_program program in
+  let%bind source = trace pretty_tracer @@
+    Parser.Reasonligo.pretty_print cst
+  in ok source
+
+let specialise_and_print_expression_reasonligo expression =
+  let%bind cst = trace cit_cameligo_tracer @@
+    Tree_abstraction.Cameligo.decompile_expression expression in
+  let%bind source = trace pretty_tracer @@
+    Parser.Reasonligo.pretty_print_expression cst
+  in ok source
+
+
+let specialise_and_print syntax source : (Buffer.t, _) Trace.result =
+  let%bind specialise_and_print =
+    match syntax with
+      PascaLIGO  -> ok specialise_and_print_pascaligo
+    | CameLIGO   -> ok specialise_and_print_cameligo
+    | ReasonLIGO -> ok specialise_and_print_reasonligo in
+  let%bind source = specialise_and_print source in
+  ok source
+
+let specialise_and_print_expression syntax source =
+  let%bind specialise_and_print = match syntax with
+    PascaLIGO  -> ok specialise_and_print_expression_pascaligo
+  | CameLIGO   -> ok specialise_and_print_expression_cameligo
+  | ReasonLIGO -> ok specialise_and_print_expression_reasonligo in
+  let%bind source = specialise_and_print source in
+  ok source

src/main/decompile/of_core.ml

@@ -0,0 +1,10 @@
+open Trace
+open Ast_core
+open Desugaring
+open Main_errors
+
+let decompile (program : program) : (Ast_sugar.program , _) result =
+  trace sugaring_tracer @@ decompile_program program
+
+let decompile_expression (e : expression) : (Ast_sugar.expression , _) result =
+  trace sugaring_tracer @@ decompile_expression e

src/main/decompile/of_imperative.ml

@@ -0,0 +1,10 @@
+open Trace
+open Ast_imperative
+open Helpers
+
+let decompile (program : program) syntax : (_ , _) result =
+  let%bind syntax = syntax_to_variant syntax None in
+  specialise_and_print syntax program
+
+let decompile_expression (e : expression) syntax : (_ , _) result =
+  specialise_and_print_expression syntax e

src/main/decompile/of_michelson.ml

@@ -5,7 +5,7 @@ open Trace
 open Simple_utils.Runned_result
 
 type ret_type = Function | Expression
-let uncompile_value func_or_expr program entry ex_ty_value =
+let decompile_value func_or_expr program entry ex_ty_value =
   let%bind output_type =
     let%bind entry_expression = trace_option entrypoint_not_found @@ Ast_typed.get_entry program entry in
     match func_or_expr with
@@ -14,30 +14,30 @@ let uncompile_value func_or_expr program entry ex_ty_value =
     | Function ->
       let%bind (_,output_type) = trace_option entrypoint_not_a_function @@ Ast_typed.get_t_function entry_expression.type_expression in
       ok output_type in
-  let%bind mini_c = trace uncompile_michelson @@ Stacking.Decompiler.decompile_value ex_ty_value in
-  let%bind typed =  trace uncompile_mini_c    @@ Spilling.decompile mini_c output_type in
-  let%bind core  =  trace uncompile_typed     @@ Typer.untype_expression typed in
+  let%bind mini_c = trace decompile_michelson @@ Stacking.Decompiler.decompile_value ex_ty_value in
+  let%bind typed =  trace decompile_mini_c    @@ Spilling.decompile mini_c output_type in
+  let%bind core  =  trace decompile_typed     @@ Typer.untype_expression typed in
   ok @@ core
 
-let uncompile_typed_program_entry_expression_result program entry runned_result =
+let decompile_typed_program_entry_expression_result program entry runned_result =
   match runned_result with
   | Fail s -> ok (Fail s)
   | Success ex_ty_value ->
-    let%bind uncompiled_value = uncompile_value Expression program entry ex_ty_value in
-    ok (Success uncompiled_value)
+    let%bind decompiled_value = decompile_value Expression program entry ex_ty_value in
+    ok (Success decompiled_value)
 
-let uncompile_typed_program_entry_function_result program entry runned_result =
+let decompile_typed_program_entry_function_result program entry runned_result =
   match runned_result with
   | Fail s -> ok (Fail s)
   | Success ex_ty_value ->
-    let%bind uncompiled_value = uncompile_value Function program entry ex_ty_value in
-    ok (Success uncompiled_value)
+    let%bind decompiled_value = decompile_value Function program entry ex_ty_value in
+    ok (Success decompiled_value)
 
-let uncompile_expression type_value runned_result =
+let decompile_expression type_value runned_result =
   match runned_result with
   | Fail s -> ok (Fail s)
   | Success ex_ty_value ->
-    let%bind mini_c = trace uncompile_michelson @@ Stacking.Decompiler.decompile_value ex_ty_value in
-    let%bind typed = trace uncompile_mini_c @@ Spilling.decompile mini_c type_value in
-    let%bind uncompiled_value = trace uncompile_typed @@ Typer.untype_expression typed in
-    ok (Success uncompiled_value)
+    let%bind mini_c = trace decompile_michelson @@ Stacking.Decompiler.decompile_value ex_ty_value in
+    let%bind typed = trace decompile_mini_c @@ Spilling.decompile mini_c type_value in
+    let%bind decompiled_value = trace decompile_typed @@ Typer.untype_expression typed in
+    ok (Success decompiled_value)

src/main/decompile/of_sugar.ml

@@ -0,0 +1,10 @@
+open Trace
+open Ast_sugar
+open Purification
+open Main_errors
+
+let decompile (program : program) : (Ast_imperative.program , _) result =
+  trace depurification_tracer @@ decompile_program program
+
+let decompile_expression (e : expression) : (Ast_imperative.expression , _) result =
+  trace depurification_tracer @@ decompile_expression e

src/main/dune

@@ -4,7 +4,7 @@
   (libraries
     run
     compile
-    uncompile
+    decompile
     main_errors
   )
   (preprocess

src/main/main.ml

@@ -1,5 +1,5 @@
 module Run = Run
 module Compile   = Compile
-module Uncompile = Uncompile
+module Decompile = Decompile
 module Display = Display
 module Formatter = Main_errors.Formatter

src/main/main_errors/formatter.ml

@@ -121,9 +121,12 @@ let rec error_ppformat' : display_format:string display_format ->
     | `Main_michelson_execution_error _ -> Format.fprintf f "@[<hv>Error of execution@]"
 
     | `Main_parser e -> Parser.Errors.error_ppformat ~display_format f e
+    | `Main_pretty _e -> () (*no error in this pass*)
     | `Main_self_ast_imperative e -> Self_ast_imperative.Errors.error_ppformat ~display_format f e 
     | `Main_purification e -> Purification.Errors.error_ppformat ~display_format f e
+    | `Main_depurification _e -> () (*no error in this pass*)
     | `Main_desugaring _e -> () (*no error in this pass*)
+    | `Main_sugaring _e -> () (*no error in this pass*)
     | `Main_cit_pascaligo e -> Tree_abstraction.Pascaligo.Errors.error_ppformat ~display_format f e
     | `Main_cit_cameligo e -> Tree_abstraction.Cameligo.Errors.error_ppformat ~display_format f e
     | `Main_typer e -> Typer.Errors.error_ppformat ~display_format f e
@@ -133,9 +136,9 @@ let rec error_ppformat' : display_format:string display_format ->
     | `Main_spilling e -> Spilling.Errors.error_ppformat ~display_format f  e
     | `Main_stacking e -> Stacking.Errors.error_ppformat ~display_format f e
 
-    | `Main_uncompile_michelson e -> Stacking.Errors.error_ppformat ~display_format f  e
-    | `Main_uncompile_mini_c e -> Spilling.Errors.error_ppformat ~display_format f  e
-    | `Main_uncompile_typed e -> Typer.Errors.error_ppformat ~display_format f  e
+    | `Main_decompile_michelson e -> Stacking.Errors.error_ppformat ~display_format f  e
+    | `Main_decompile_mini_c e -> Spilling.Errors.error_ppformat ~display_format f  e
+    | `Main_decompile_typed e -> Typer.Errors.error_ppformat ~display_format f  e
   )
   
 let error_ppformat : display_format:string display_format ->
@@ -272,9 +275,12 @@ let rec error_jsonformat : Types.all -> J.t = fun a ->
   | `Main_entrypoint_not_found -> json_error ~stage:"top-level glue" ~content:(`String "Missing entrypoint")
 
   | `Main_parser e -> Parser.Errors.error_jsonformat e
+  | `Main_pretty _ -> `Null (*no error in this pass*)
   | `Main_self_ast_imperative e -> Self_ast_imperative.Errors.error_jsonformat e
   | `Main_purification e -> Purification.Errors.error_jsonformat e
+  | `Main_depurification _ -> `Null (*no error in this pass*)
   | `Main_desugaring _ -> `Null (*no error in this pass*)
+  | `Main_sugaring _ -> `Null (*no error in this pass*)
   | `Main_cit_pascaligo e -> Tree_abstraction.Pascaligo.Errors.error_jsonformat e
   | `Main_cit_cameligo e -> Tree_abstraction.Cameligo.Errors.error_jsonformat e
   | `Main_typer e -> Typer.Errors.error_jsonformat e
@@ -284,9 +290,9 @@ let rec error_jsonformat : Types.all -> J.t = fun a ->
   | `Main_self_mini_c e -> Self_mini_c.Errors.error_jsonformat e
   | `Main_stacking e -> Stacking.Errors.error_jsonformat e
   
-  | `Main_uncompile_michelson e -> Stacking.Errors.error_jsonformat e
-  | `Main_uncompile_mini_c e -> Spilling.Errors.error_jsonformat e
-  | `Main_uncompile_typed e -> Typer.Errors.error_jsonformat e
+  | `Main_decompile_michelson e -> Stacking.Errors.error_jsonformat e
+  | `Main_decompile_mini_c e -> Spilling.Errors.error_jsonformat e
+  | `Main_decompile_typed e -> Typer.Errors.error_jsonformat e
 
 let error_format : _ Display.format = {
   pp = error_ppformat;

src/main/main_errors/main_errors.ml

@@ -5,11 +5,14 @@ type all = Types.all
 (* passes tracers *)
 
 let parser_tracer (e:Parser.Errors.parser_error) : all = `Main_parser e
+let pretty_tracer (e:Parser.Errors.parser_error) : all = `Main_pretty e
 let cit_cameligo_tracer (e:Tree_abstraction.Cameligo.Errors.abs_error) : all = `Main_cit_cameligo e
 let cit_pascaligo_tracer (e:Tree_abstraction.Pascaligo.Errors.abs_error) : all = `Main_cit_pascaligo e
 let self_ast_imperative_tracer (e:Self_ast_imperative.Errors.self_ast_imperative_error) : all = `Main_self_ast_imperative e
 let purification_tracer (e:Purification.Errors.purification_error) : all = `Main_purification e
+let depurification_tracer (e:Purification.Errors.purification_error) : all = `Main_depurification e
 let desugaring_tracer (e:Desugaring.Errors.desugaring_error) : all = `Main_desugaring e
+let sugaring_tracer (e:Desugaring.Errors.desugaring_error) : all = `Main_sugaring e
 let typer_tracer (e:Typer.Errors.typer_error) : all = `Main_typer e
 let self_ast_typed_tracer (e:Self_ast_typed.Errors.self_ast_typed_error) : all = `Main_self_ast_typed e
 let self_mini_c_tracer (e:Self_mini_c.Errors.self_mini_c_error) : all = `Main_self_mini_c e
@@ -17,9 +20,9 @@ let spilling_tracer (e:Spilling.Errors.spilling_error) : all = `Main_spilling e
 let stacking_tracer (e:Stacking.Errors.stacking_error) : all = `Main_stacking e
 let interpret_tracer (e:Interpreter.interpreter_error) : all = `Main_interpreter e
 
-let uncompile_mini_c : Spilling.Errors.spilling_error -> all = fun e -> `Main_uncompile_mini_c e
-let uncompile_typed : Typer.Errors.typer_error -> all = fun e -> `Main_uncompile_typed e
-let uncompile_michelson : Stacking.Errors.stacking_error -> all = fun e -> `Main_uncompile_michelson e
+let decompile_mini_c : Spilling.Errors.spilling_error -> all = fun e -> `Main_decompile_mini_c e
+let decompile_typed : Typer.Errors.typer_error -> all = fun e -> `Main_decompile_typed e
+let decompile_michelson : Stacking.Errors.stacking_error -> all = fun e -> `Main_decompile_michelson e
 
 (* top-level glue (in between passes) *)
 

src/main/main_errors/types.ml

@@ -21,9 +21,12 @@ type all =
  | `Main_michelson_execution_error of Proto_alpha_utils.Trace.tezos_alpha_error list
 
  | `Main_parser of Parser.Errors.parser_error
+ | `Main_pretty of Parser.Errors.parser_error
  | `Main_self_ast_imperative of Self_ast_imperative.Errors.self_ast_imperative_error
  | `Main_purification   of Purification.Errors.purification_error
+ | `Main_depurification of Purification.Errors.purification_error
  | `Main_desugaring of Desugaring.Errors.desugaring_error
+ | `Main_sugaring   of Desugaring.Errors.desugaring_error
  | `Main_cit_pascaligo of Tree_abstraction.Pascaligo.Errors.abs_error
  | `Main_cit_cameligo of Tree_abstraction.Cameligo.Errors.abs_error
  | `Main_typer of Typer.Errors.typer_error
@@ -33,9 +36,9 @@ type all =
  | `Main_spilling of Spilling.Errors.spilling_error
  | `Main_stacking of Stacking.Errors.stacking_error
 
- | `Main_uncompile_michelson of Stacking.Errors.stacking_error
- | `Main_uncompile_mini_c of Spilling.Errors.spilling_error
- | `Main_uncompile_typed of Typer.Errors.typer_error
+ | `Main_decompile_michelson of Stacking.Errors.stacking_error
+ | `Main_decompile_mini_c of Spilling.Errors.spilling_error
+ | `Main_decompile_typed of Typer.Errors.typer_error
  | `Main_entrypoint_not_a_function
  | `Main_entrypoint_not_found
  | `Main_invalid_amount of string

src/passes/01-parsing/cameligo.ml

@@ -146,11 +146,24 @@ let preprocess source = apply (fun () -> Unit.preprocess source)
 
 (* Pretty-print a file (after parsing it). *)
 
-let pretty_print source =
-  match parse_file source with
-    Stdlib.Error _ as e -> e
-  | Ok ast ->
-      let doc    = Pretty.print (fst ast) in
+let pretty_print cst =
+  let doc    = Pretty.print cst in
+  let buffer = Buffer.create 131 in
+  let width  =
+    match Terminal_size.get_columns () with
+      None -> 60
+    | Some c -> c in
+  let () = PPrint.ToBuffer.pretty 1.0 width buffer doc
+  in Trace.ok buffer
+
+let pretty_print_from_source source =
+  match parse_file source with
+    Stdlib.Error _ as e -> e
+  | Ok cst ->
+    pretty_print @@ fst cst
+
+let pretty_print_expression cst =
+  let doc    = Pretty.pp_expr cst in
   let buffer = Buffer.create 131 in
   let width  =
     match Terminal_size.get_columns () with

src/passes/01-parsing/cameligo.mli

@@ -22,4 +22,9 @@ val parse_expression : string -> (CST.expr , Errors.parser_error) result
 val preprocess : string -> (Buffer.t , Errors.parser_error) result
 
 (** Pretty-print a given CameLIGO file (after parsing it). *)
-val pretty_print : string -> (Buffer.t, Errors.parser_error) result
+val pretty_print_from_source : string -> (Buffer.t, Errors.parser_error) result
+
+(** Take a CameLIGO cst and pretty_print it *)
+val pretty_print : CST.t -> (Buffer.t, _) result
+
+val pretty_print_expression : CST.expr -> (Buffer.t, _) result

src/passes/01-parsing/cameligo/Parser.mly

@@ -93,7 +93,7 @@ tuple(item):
 
 list__(item):
   "[" sep_or_term_list(item,";")? "]" {
-    let compound = Brackets ($1,$3)
+    let compound = Some (Brackets ($1,$3))
     and region = cover $1 $3 in
     let elements, terminator =
       match $2 with
@@ -194,7 +194,7 @@ record_type:
     let () = Utils.nsepseq_to_list ne_elements
              |> Scoping.check_fields in
     let region = cover $1 $3
-    and value  = {compound = Braces ($1,$3); ne_elements; terminator}
+    and value  = {compound = Some (Braces ($1,$3)); ne_elements; terminator}
     in TRecord {region; value} }
 
 field_decl:
@@ -300,7 +300,7 @@ record_pattern:
   "{" sep_or_term_list(field_pattern,";") "}" {
     let ne_elements, terminator = $2 in
     let region = cover $1 $3 in
-    let value  = {compound = Braces ($1,$3); ne_elements; terminator}
+    let value  = {compound = Some (Braces ($1,$3)); ne_elements; terminator}
     in {region; value} }
 
 field_pattern:
@@ -377,22 +377,18 @@ if_then_else(right_expr):
                   test     = $2;
                   kwd_then = $3;
                   ifso     = $4;
-                  kwd_else = $5;
-                  ifnot    = $6}
+                  ifnot    = Some($5,$6)}
     in ECond {region; value} }
 
 if_then(right_expr):
   "if" expr "then" right_expr {
-    let the_unit = ghost, ghost in
-    let ifnot    = EUnit (wrap_ghost the_unit) in
     let stop     = expr_to_region $4 in
     let region   = cover $1 stop in
     let value    = {kwd_if   = $1;
                     test     = $2;
                     kwd_then = $3;
                     ifso     = $4;
-                    kwd_else = ghost;
-                    ifnot}
+                    ifnot    = None}
     in ECond {region; value} }
 
 base_if_then_else__open(x):
@@ -630,7 +626,7 @@ record_expr:
   "{" sep_or_term_list(field_assignment,";") "}" {
     let ne_elements, terminator = $2 in
     let region = cover $1 $3 in
-    let value  = {compound = Braces ($1,$3);
+    let value  = {compound = Some (Braces ($1,$3));
                   ne_elements;
                   terminator}
     in {region; value} }
@@ -643,7 +639,7 @@ update_record:
       lbrace   = $1;
       record   = $2;
       kwd_with = $3;
-      updates  = {value = {compound = Braces (ghost, ghost);
+      updates  = {value = {compound = None;
                            ne_elements;
                            terminator};
                   region = cover $3 $5};
@@ -671,7 +667,7 @@ path :
 sequence:
   "begin" series? "end" {
     let region   = cover $1 $3
-    and compound = BeginEnd ($1,$3) in
+    and compound = Some (BeginEnd ($1,$3)) in
     let elements = $2 in
     let value    = {compound; elements; terminator=None}
     in {region; value} }
@@ -691,7 +687,7 @@ let_in_sequence:
     let seq       = $6 in
     let stop      = nsepseq_to_region expr_to_region seq in
     let region    = cover $1 stop in
-    let compound  = BeginEnd (Region.ghost, Region.ghost) in
+    let compound  = None in
     let elements  = Some seq in
     let value     = {compound; elements; terminator=None} in
     let body      = ESeq {region; value} in

src/passes/01-parsing/cameligo/Pretty.ml

@@ -5,6 +5,7 @@ open CST
 module Region = Simple_utils.Region
 open! Region
 open! PPrint
+module Option = Simple_utils.Option
 
 let pp_par printer {value; _} =
   string "(" ^^ nest 1 (printer value.inside ^^ string ")")
@@ -173,13 +174,15 @@ and pp_clause {value; _} =
     pp_pattern pattern ^^ prefix 4 1 (string " ->") (pp_expr rhs)
 
 and pp_cond_expr {value; _} =
-  let {test; ifso; kwd_else; ifnot; _} = value in
+  let {test; ifso; ifnot; _} = value in
   let test = string "if " ^^ group (nest 3 (pp_expr test))
   and ifso = string "then" ^^ group (nest 2 (break 1 ^^ pp_expr ifso))
-  and ifnot = string "else" ^^ group (nest 2 (break 1 ^^ pp_expr ifnot))
-  in if   kwd_else#is_ghost
-     then test ^/^ ifso
-     else test ^/^ ifso ^/^ ifnot
+  in match ifnot with
+    Some (_,ifnot) ->
+    let ifnot = string "else" ^^ group (nest 2 (break 1 ^^ pp_expr ifnot)) in
+    test ^/^ ifso ^/^ ifnot
+  | None ->
+    test ^/^ ifso
 
 and pp_annot_expr {value; _} =
   let expr, _, type_expr = value.inside in
@@ -243,18 +246,15 @@ and pp_injection :
     let sep = string ";" ^^ break 1 in
     let elements = Utils.sepseq_to_list elements in
     let elements = separate_map sep printer elements in
-    match pp_compound compound with
+    match Option.map pp_compound compound with
       None -> elements
     | Some (opening, closing) ->
         string opening ^^ nest 1 elements ^^ string closing
 
 and pp_compound = function
-  BeginEnd (start, _) ->
-    if start#is_ghost then None else Some ("begin","end")
-| Braces (start, _) ->
-    if start#is_ghost then None else Some ("{","}")
-| Brackets (start, _) ->
-    if start#is_ghost then None else Some ("[","]")
+  BeginEnd (_, _) -> ("begin","end")
+| Braces (_, _)   -> ("{","}")
+| Brackets (_, _) -> ("[","]")
 
 and pp_constr_expr = function
   ENone      _ -> string "None"
@@ -282,7 +282,7 @@ and pp_ne_injection :
   fun printer {value; _} ->
     let {compound; ne_elements; _} = value in
     let elements = pp_nsepseq ";" printer ne_elements in
-    match pp_compound compound with
+    match Option.map pp_compound compound with
       None -> elements
     | Some (opening, closing) ->
         string opening ^^ nest 1 elements ^^ string closing
@@ -356,8 +356,8 @@ and pp_let_in {value; _} =
     | Some _ -> "let rec " in
   let binding = pp_let_binding binding
   and attr    = pp_attributes attributes
-  in string let_str ^^ binding ^^ attr
-     ^^ hardline ^^ group (string "in " ^^ nest 3 (pp_expr body))
+  in string let_str ^^ binding ^^ attr ^^ string " in"
+     ^^ hardline ^^ group (pp_expr body)
 
 and pp_fun {value; _} =
   let {binders; lhs_type; body; _} = value in
@@ -375,7 +375,7 @@ and pp_seq {value; _} =
   let sep = string ";" ^^ hardline in
   let elements = Utils.sepseq_to_list elements in
   let elements = separate_map sep pp_expr elements in
-  match pp_compound compound with
+  match Option.map pp_compound compound with
     None -> elements
   | Some (opening, closing) ->
      string opening
@@ -406,7 +406,7 @@ and pp_variants {value; _} =
   let head = pp_variant head in
   let head = if tail = [] then head else ifflat head (blank 2 ^^ head) in
   let rest = List.map snd tail in
-  let app variant = break 1 ^^ string "| " ^^ pp_variant variant
+  let app variant = group (break 1 ^^ string "| " ^^ pp_variant variant)
   in head ^^ concat_map app rest
 
 and pp_variant {value; _} =

src/passes/01-parsing/pascaligo.ml

@@ -8,6 +8,7 @@ module Scoping  = Parser_pascaligo.Scoping
 module Region   = Simple_utils.Region
 module ParErr   = Parser_pascaligo.ParErr
 module SSet     = Set.Make (String)
+module Pretty   = Parser_pascaligo.Pretty
 
 (* Mock IOs TODO: Fill them with CLI options *)
 
@@ -156,3 +157,23 @@ let parse_expression source = apply (fun () -> Unit.expr_in_string source)
 (* Preprocessing a contract in a file *)
 
 let preprocess source = apply (fun () -> Unit.preprocess source)
+
+let pretty_print cst =
+  let doc    = Pretty.print cst in
+  let buffer = Buffer.create 131 in
+  let width  =
+    match Terminal_size.get_columns () with
+      None -> 60
+    | Some c -> c in
+  let () = PPrint.ToBuffer.pretty 1.0 width buffer doc
+  in Trace.ok buffer
+
+let pretty_print_expression cst =
+  let doc    = Pretty.pp_expr cst in
+  let buffer = Buffer.create 131 in
+  let width  =
+    match Terminal_size.get_columns () with
+      None -> 60
+    | Some c -> c in
+  let () = PPrint.ToBuffer.pretty 1.0 width buffer doc
+  in Trace.ok buffer

src/passes/01-parsing/pascaligo.mli

@@ -21,3 +21,8 @@ val parse_expression : string -> (CST.expr, parser_error) result
 
 (** Preprocess a given PascaLIGO file and preprocess it. *)
 val preprocess : string -> (Buffer.t, parser_error) result
+
+(** Take a PascaLIGO cst and pretty_print it *)
+val pretty_print : CST.t -> (Buffer.t, _) result
+
+val pretty_print_expression : CST.expr -> (Buffer.t, _) result

src/passes/01-parsing/pascaligo/Parser.mly

@@ -259,25 +259,7 @@ fun_expr:
 (* Function declarations *)
 
 open_fun_decl:
-  ioption ("recursive") "function" fun_name parameters type_annot? "is"
-  block "with" expr {
-    Scoping.check_reserved_name $3;
-    let stop   = expr_to_region $9 in
-    let region = cover $2 stop
-    and value  = {kwd_recursive= $1;
-                  kwd_function = $2;
-                  fun_name     = $3;
-                  param        = $4;
-                  ret_type     = $5;
-                  kwd_is       = $6;
-                  block_with   = Some ($7, $8);
-                  return       = $9;
-                  terminator   = None;
-                  attributes   = None}
-    in {region; value}
-  }
-| ioption ("recursive") "function" fun_name parameters type_annot? "is"
-  expr {
+  ioption("recursive") "function" fun_name parameters type_annot? "is" expr {
     Scoping.check_reserved_name $3;
     let stop   = expr_to_region $7 in
     let region = cover $2 stop
@@ -287,11 +269,11 @@ open_fun_decl:
                   param        = $4;
                   ret_type     = $5;
                   kwd_is       = $6;
-                  block_with   = None;
                   return       = $7;
                   terminator   = None;
                   attributes   = None}
-    in {region; value} }
+    in {region; value}
+  }
 
 fun_decl:
   open_fun_decl ";"? {
@@ -593,7 +575,7 @@ case_clause(rhs):
 
 assignment:
   lhs ":=" rhs {
-    let stop   = rhs_to_region $3 in
+    let stop   = expr_to_region $3 in
     let region = cover (lhs_to_region $1) stop
     and value  = {lhs = $1; assign = $2; rhs = $3}
     in {region; value} }
@@ -662,6 +644,15 @@ expr:
 | cond_expr  { $1                        }
 | disj_expr  { $1                        }
 | fun_expr   { EFun $1                   }
+| block_with { EBlock $1                 }
+
+block_with:
+  block "with" expr {
+    let start  = $2
+    and stop   = expr_to_region $3 in
+    let region = cover start stop in
+    let value  = {block=$1; kwd_with=$2; expr=$3}
+    in {region; value} }
 
 cond_expr:
   "if" expr "then" expr ";"? "else" expr {

src/passes/01-parsing/pascaligo/Pretty.ml

@@ -85,7 +85,7 @@ and pp_variants {value; _} =
   let head = if tail = [] then head
              else ifflat head (string "  " ^^ head) in
   let rest = List.map snd tail in
-  let app variant = break 1 ^^ string "| " ^^ pp_variant variant
+  let app variant = group (break 1 ^^ string "| " ^^ pp_variant variant)
   in head ^^ concat_map app rest
 
 and pp_variant {value; _} =
@@ -144,7 +144,7 @@ and pp_fun_expr {value; _} =
 
 and pp_fun_decl {value; _} =
   let {kwd_recursive; fun_name; param; ret_type;
-       block_with; return; attributes; _} = value in
+       return; attributes; _} = value in
   let start =
     match kwd_recursive with
         None -> string "function"
@@ -160,10 +160,9 @@ and pp_fun_decl {value; _} =
                        ^^ string " is"))
   and body =
     let expr = pp_expr return in
-    match block_with with
-            None -> group (nest 2 (break 1 ^^ expr))
-    | Some (b,_) -> hardline ^^ pp_block b ^^ string " with"
-                   ^^ group (nest 4 (break 1 ^^ expr))
+    match return with
+      EBlock _ -> group (break 1 ^^ expr)
+    | _ -> group (nest 2 (break 1 ^^ expr))
   and attr =
     match attributes with
       None -> empty
@@ -406,6 +405,14 @@ and pp_expr = function
 | EPar        e -> pp_par pp_expr e
 | EFun        e -> pp_fun_expr e
 | ECodeInj    e -> pp_code_inj e
+| EBlock      e -> pp_block_with e
+
+and pp_block_with {value; _} =
+  let {block; kwd_with; expr} = value in
+  let expr = value.expr in
+  let expr = pp_expr expr in
+  group (pp_block block ^^ string " with"
+         ^^ group (nest 4 (break 1 ^^ expr)))
 
 and pp_annot_expr {value; _} =
   let expr, _, type_expr = value.inside in

src/passes/01-parsing/reasonligo.ml

@@ -147,12 +147,25 @@ let parse_expression source = apply (fun () -> Unit.expr_in_string source)
 let preprocess source = apply (fun () -> Unit.preprocess source)
 
 (* Pretty-print a file (after parsing it). *)
-
-let pretty_print source =
-  match parse_file source with
-    Stdlib.Error _ as e -> e
-  | Ok ast ->
-      let doc    = Pretty.print (fst ast) in
+let pretty_print cst =
+  let doc    = Pretty.print cst in
+  let buffer = Buffer.create 131 in
+  let width  =
+    match Terminal_size.get_columns () with
+      None -> 60
+    | Some c -> c in
+  let () = PPrint.ToBuffer.pretty 1.0 width buffer doc
+  in Trace.ok buffer
+
+let pretty_print_from_source source =
+  match parse_file source with
+    Stdlib.Error _ as e -> e
+  | Ok cst ->
+    pretty_print @@ fst cst
+
+
+let pretty_print_expression cst =
+  let doc    = Pretty.pp_expr cst in
   let buffer = Buffer.create 131 in
   let width  =
     match Terminal_size.get_columns () with

src/passes/01-parsing/reasonligo.mli

@@ -21,5 +21,10 @@ val parse_expression : string -> (CST.expr , Errors.parser_error) result
 (** Preprocess a given ReasonLIGO file and preprocess it. *)
 val preprocess : string -> (Buffer.t , Errors.parser_error) result
 
-(** Pretty-print a given CameLIGO file (after parsing it). *)
-val pretty_print : string -> (Buffer.t , Errors.parser_error) result
+(** Pretty-print a given ReasonLIGO file (after parsing it). *)
+val pretty_print_from_source : string -> (Buffer.t , Errors.parser_error) result
+
+(** Take a ReasonLIGO cst and pretty_print it *)
+val pretty_print : CST.t -> (Buffer.t, _) result
+
+val pretty_print_expression : CST.expr -> (Buffer.t, _) result

src/passes/01-parsing/reasonligo/Parser.mly

@@ -131,7 +131,7 @@ tuple(item):
 
 list__(item):
   "[" sep_or_term_list(item,";")? "]" {
-    let compound = Brackets ($1,$3)
+    let compound = Some (Brackets ($1,$3))
     and region = cover $1 $3 in
     let elements, terminator =
       match $2 with
@@ -224,7 +224,7 @@ record_type:
     let () = Utils.nsepseq_to_list ne_elements
              |> Scoping.check_fields in
     let region = cover $1 $3
-    and value  = {compound = Braces ($1,$3); ne_elements; terminator}
+    and value  = {compound = Some(Braces ($1,$3)); ne_elements; terminator}
     in TRecord {region; value} }
 
 type_expr_field:
@@ -362,7 +362,7 @@ record_pattern:
   "{" sep_or_term_list(field_pattern,",") "}" {
     let ne_elements, terminator = $2 in
     let region = cover $1 $3 in
-    let value  = {compound = Braces ($1,$3);
+    let value  = {compound = Some (Braces ($1,$3));
                   ne_elements;
                   terminator}
     in {region; value} }
@@ -592,15 +592,12 @@ parenthesized_expr:
 
 if_then(right_expr):
   "if" parenthesized_expr "{" closed_if ";"? "}" {
-    let the_unit = ghost, ghost in
-    let ifnot    = EUnit {region=ghost; value=the_unit} in
     let region   = cover $1 $6 in
     let value    = {kwd_if   = $1;
                     test     = $2;
                     kwd_then = $3;
                     ifso     = $4;
-                    kwd_else = ghost;
-                    ifnot}
+                    ifnot    = None}
     in ECond {region; value} }
 
 if_then_else(right_expr):
@@ -611,8 +608,7 @@ if_then_else(right_expr):
                   test     = $2;
                   kwd_then = $3;
                   ifso     = $4;
-                  kwd_else = $6;
-                  ifnot    = $9}
+                  ifnot    = Some ($6,$9)}
     in ECond {region; value} }
 
 base_if_then_else__open(x):
@@ -825,7 +821,7 @@ list_or_spread:
     let elts, terminator = $4 in
     let elts = Utils.nsepseq_cons $2 $3 elts in
     let value = {
-      compound = Brackets ($1,$5);
+      compound = Some (Brackets ($1,$5));
       elements = Some elts;
       terminator}
     and region = cover $1 $5 in
@@ -837,7 +833,7 @@ list_or_spread:
     in EList (ECons {region; value})
   }
 | "[" expr? "]" {
-    let compound = Brackets ($1,$3)
+    let compound = Some (Brackets ($1,$3))
     and elements =
       match $2 with
         None -> None
@@ -913,7 +909,7 @@ update_record:
       lbrace   = $1;
       record   = $3;
       kwd_with = $4;
-      updates  = {value = {compound = Braces (ghost, ghost);
+      updates  = {value = {compound = None;
                            ne_elements;
                            terminator};
                   region = cover $4 $6};
@@ -949,7 +945,7 @@ exprs:
       in
       let sequence = ESeq {
         value = {
-          compound   = BeginEnd (ghost, ghost);
+          compound   = None; 
           elements   = Some val_;
           terminator = snd c};
         region = sequence_region
@@ -982,7 +978,7 @@ more_field_assignments:
 sequence:
   "{" exprs "}" {
     let elts, _region = $2 in
-    let compound = Braces ($1, $3) in
+    let compound = Some (Braces ($1, $3)) in
     let value    = {compound;
                     elements = Some elts;
                     terminator = None} in
@@ -991,7 +987,7 @@ sequence:
 
 record:
   "{" field_assignment more_field_assignments? "}" {
-    let compound = Braces ($1,$4) in
+    let compound = Some (Braces ($1,$4)) in
     let region   = cover $1 $4 in
 
     match $3 with
@@ -1010,7 +1006,7 @@ record:
     let field_name = {$2 with value} in
     let comma, elts = $3 in
     let ne_elements = Utils.nsepseq_cons field_name comma elts in
-    let compound = Braces ($1,$4) in
+    let compound = Some (Braces ($1,$4)) in
     let region   = cover $1 $4 in
     {value = {compound; ne_elements; terminator = None}; region} }
 

src/passes/01-parsing/reasonligo/Pretty.ml

@@ -5,6 +5,7 @@ open CST
 module Region = Simple_utils.Region
 open! Region
 open! PPrint
+module Option = Simple_utils.Option
 
 let rec print ast =
   let app decl = group (pp_declaration decl) in
@@ -179,13 +180,13 @@ and pp_clause {value; _} =
   prefix 4 1 (pp_pattern pattern ^^ string " =>") (pp_expr rhs)
 
 and pp_cond_expr {value; _} =
-  let {test; ifso; kwd_else; ifnot; _} = value in
+  let {test; ifso; ifnot; _} = value in
   let if_then =
     string "if" ^^ string " (" ^^ pp_expr test ^^ string ")" ^^ string " {" ^^ break 0
     ^^ group (nest 2 (break 2 ^^ pp_expr ifso)) ^^ hardline ^^ string "}" in
-  if kwd_else#is_ghost then
-    if_then
-  else
+  match ifnot with
+    None -> if_then
+  | Some (_,ifnot) ->
     if_then
     ^^ string " else" ^^ string " {" ^^ break 0 ^^ group (nest 2 (break 2 ^^ pp_expr ifnot)) ^^ hardline ^^ string "}"
 
@@ -252,18 +253,15 @@ and pp_injection :
     let sep = (string ",") ^^ break 1 in
     let elements = Utils.sepseq_to_list elements in
     let elements = separate_map sep printer elements in
-    match pp_compound compound with
+    match Option.map pp_compound compound with
       None -> elements
     | Some (opening, closing) ->
         string opening ^^ nest 1 elements ^^ string closing
 
 and pp_compound = function
-  BeginEnd (start, _) ->
-    if start#is_ghost then None else Some ("begin","end")
-| Braces (start, _) ->
-    if start#is_ghost then None else Some ("{","}")
-| Brackets (start, _) ->
-    if start#is_ghost then None else Some ("[","]")
+  BeginEnd (_, _) -> ("begin","end")
+| Braces   (_, _) -> ("{","}")
+| Brackets (_, _) -> ("[","]")
 
 and pp_constr_expr = function
   ENone      _ -> string "None"
@@ -291,7 +289,7 @@ and pp_ne_injection :
   fun printer {value; _} ->
     let {compound; ne_elements; _} = value in
     let elements = pp_nsepseq "," printer ne_elements in
-    match pp_compound compound with
+    match Option.map pp_compound compound with
       None -> elements
     | Some (opening, closing) ->
         string opening ^^ nest 2 (break 0 ^^ elements) ^^ break 1 ^^ string closing
@@ -387,7 +385,7 @@ and pp_seq {value; _} =
   let sep = string ";" ^^ hardline in
   let elements = Utils.sepseq_to_list elements in
   let elements = separate_map sep pp_expr elements in
-  match pp_compound compound with
+  match Option.map pp_compound compound with
     None -> elements
   | Some (opening, closing) ->
      string opening

src/passes/03-tree_abstraction/cameligo/cameligo.ml

@@ -2,7 +2,11 @@ module CST = Cst.Cameligo
 module AST = Ast_imperative
 
 module Compiler   = Compiler
+module Decompiler = Decompiler
 module Errors = Errors
 
 let compile_program    = Compiler.compile_program
 let compile_expression = Compiler.compile_expression
+
+let decompile_program    = Decompiler.decompile_program
+let decompile_expression = Decompiler.decompile_expression

src/passes/03-tree_abstraction/cameligo/cameligo.mli

@@ -8,5 +8,7 @@ module Errors = Errors
 
 
 val compile_expression : CST.expr -> (AST.expr, Errors.abs_error) result
-
 val compile_program : CST.ast -> (AST.program, Errors.abs_error) result
+
+val decompile_expression : AST.expr -> (CST.expr, _) result
+val decompile_program    : AST.program -> (CST.ast, _) result

src/passes/03-tree_abstraction/cameligo/compiler.ml

@@ -11,6 +11,7 @@ module Option = Simple_utils.Option
 
 open Combinators
 
+let (<@) f g x = f (g x)
 let nseq_to_list (hd, tl) = hd :: tl
 let npseq_to_list (hd, tl) = hd :: (List.map snd tl)
 let npseq_to_nelist (hd, tl) = hd, (List.map snd tl)
@@ -247,7 +248,7 @@ in trace (abstracting_expr_tracer t) @@
       let%bind ty_opt =
         bind_map_option (fun (re,te) -> let%bind te = compile_type_expression te in ok(Location.lift re,te)) lhs_type in
       let%bind rhs = compile_expression let_rhs in
-      let rhs_b = Var.fresh ~name: "rhs" () in
+      let rhs_b = Var.fresh ~name:"rhs" () in
       let rhs',rhs_b_expr =
         match ty_opt with
           None -> rhs, e_variable ~loc rhs_b
@@ -491,7 +492,8 @@ in trace (abstracting_expr_tracer t) @@
       let (c , loc) = r_split c in
       let%bind expr = compile_expression c.test in
       let%bind match_true = compile_expression c.ifso in
-      let%bind match_false = compile_expression c.ifnot in
+      let%bind match_false = bind_map_option (compile_expression <@ snd) c.ifnot in
+      let match_false = Option.unopt ~default:(e_unit ()) match_false in
       return @@ e_cond ~loc expr match_true match_false
   | ECodeInj ci ->
      let ci, loc   = r_split ci in
@@ -541,7 +543,7 @@ and compile_fun lamb' : (expr , abs_error) result =
     let aux ((var : Raw.variable) , ty_opt) =
       match var.value , ty_opt with
       | "storage" , None ->
-        ok (var , t_variable ~loc @@ Var.fresh ~name:"storage" ())
+        ok (var , t_variable_ez ~loc "storage")
       | _ , None ->
           fail @@ untyped_fun_param var
       | _ , Some ty -> (

src/passes/03-tree_abstraction/cameligo/decompiler.ml

@@ -0,0 +1,504 @@
+module AST = Ast_imperative
+module CST = Cst.Cameligo
+module Predefined = Predefined.Tree_abstraction.Cameligo
+
+open Trace
+
+(* General tools *)
+let (<@) f g x = f (g x)
+
+(* Utils *)
+let rg = Region.ghost
+let wrap : type a. a -> a CST.reg = fun value -> {value;region=rg}
+let list_to_sepseq lst =
+  match lst with
+    [] -> None
+  |  hd :: lst ->
+      let aux e = (rg, e) in
+      Some (hd, List.map aux lst)
+let list_to_nsepseq lst =
+  match list_to_sepseq lst with
+    Some s -> ok @@ s
+  | None   -> failwith "List is empty"
+
+let nelist_to_npseq (hd, lst) = (hd, List.map (fun e -> (rg, e)) lst)
+let npseq_cons hd lst = hd,(rg, fst lst)::(snd lst)
+
+let par a = CST.{lpar=rg;inside=a;rpar=rg}
+let inject compound a = CST.{compound;elements=a;terminator=Some(rg)}
+let ne_inject compound a = CST.{compound;ne_elements=a;terminator=Some(rg)}
+let prefix_colon a = (rg, a)
+let braces = Some (CST.Braces (rg,rg))
+let brackets = Some (CST.Brackets (rg,rg))
+let beginEnd = Some (CST.BeginEnd (rg,rg))
+
+(* Decompiler *)
+
+let decompile_variable : type a. a Var.t -> CST.variable = fun var ->
+  let var = Format.asprintf "%a" Var.pp var in
+  if String.contains var '#' then
+    let var = String.split_on_char '#' var in
+    wrap @@ "gen__" ^ (String.concat "" var)
+  else
+    if String.length var > 4 && String.equal "gen__" @@ String.sub var 0 5 then
+      wrap @@ "user__" ^ var
+    else
+      wrap @@ var
+
+let rec decompile_type_expr : AST.type_expression -> _ result = fun te ->
+  let return te = ok @@ te in
+  match te.type_content with
+    T_sum sum ->
+    let sum = AST.CMap.to_kv_list sum in
+    let aux (AST.Constructor c, AST.{ctor_type;_}) =
+      let constr = wrap c in
+      let%bind arg = decompile_type_expr ctor_type in
+      let arg = Some (rg, arg) in
+      let variant : CST.variant = {constr;arg} in
+      ok @@ wrap variant
+    in
+    let%bind sum = bind_map_list aux sum in
+    let%bind sum = list_to_nsepseq sum in
+    return @@ CST.TSum (wrap sum)
+  | T_record record ->
+    let record = AST.LMap.to_kv_list record in
+    let aux (AST.Label c, AST.{field_type;_}) =
+      let field_name = wrap c in
+      let colon = rg in
+      let%bind field_type = decompile_type_expr field_type in
+      let variant : CST.field_decl = {field_name;colon;field_type} in
+      ok @@ wrap variant
+    in
+    let%bind record = bind_map_list aux record in
+    let%bind record = list_to_nsepseq record in
+    return @@ CST.TRecord (wrap @@ ne_inject (braces) record)
+  | T_tuple tuple ->
+    let%bind tuple = bind_map_list decompile_type_expr tuple in
+    let%bind tuple = list_to_nsepseq @@ tuple in
+    return @@ CST.TProd (wrap tuple)
+  | T_arrow {type1;type2} ->
+    let%bind type1 = decompile_type_expr type1 in
+    let%bind type2 = decompile_type_expr type2 in
+    let arrow = (type1, rg, type2) in
+    return @@ CST.TFun (wrap arrow)
+  | T_variable var ->
+    let var = decompile_variable var in
+    return @@ CST.TVar (var)
+  | T_constant const ->
+    let const = Predefined.type_constant_to_string const in
+    return @@ CST.TVar (wrap const)
+  | T_operator (operator, lst) ->
+    let operator = wrap @@ Predefined.type_operator_to_string operator in
+    let%bind lst = bind_map_list decompile_type_expr lst in
+    let%bind lst = list_to_nsepseq lst in
+    let lst : _ CST.par = {lpar=rg;inside=lst;rpar=rg} in
+    return @@ CST.TApp (wrap (operator,wrap lst))
+  | T_annoted _annot ->
+    failwith "let's work on it later"
+
+let get_e_variable : AST.expression -> _ result = fun expr ->
+  match expr.expression_content with
+    E_variable var -> ok @@ var
+  | _ -> failwith @@
+    Format.asprintf "%a should be a variable expression"
+    AST.PP.expression expr
+
+let get_e_tuple : AST.expression -> _ result = fun expr ->
+  match expr.expression_content with
+    E_tuple tuple -> ok @@ tuple
+  | E_variable _
+  | E_literal _
+  | E_constant _
+  | E_lambda _ -> ok @@ [expr]
+  | _ -> failwith @@
+    Format.asprintf "%a should be a tuple expression"
+    AST.PP.expression expr
+
+let pattern_type var ty_opt =
+  let var = CST.PVar (decompile_variable var) in
+  match ty_opt with
+    Some s ->
+      let%bind type_expr = decompile_type_expr s in
+      ok @@ CST.PTyped (wrap @@ CST.{pattern=var;colon=rg;type_expr})
+  | None -> ok @@ var
+
+let rec decompile_expression : AST.expression -> _ result = fun expr ->
+  let return_expr expr = ok @@ expr in
+  let return_expr_with_par expr = return_expr @@ CST.EPar (wrap @@ par @@ expr) in
+  match expr.expression_content with
+    E_variable name ->
+    let var = decompile_variable name in
+    return_expr @@ CST.EVar (var)
+  | E_constant {cons_name; arguments} ->
+    let expr = CST.EVar (wrap @@ Predefined.constant_to_string cons_name) in
+    (match arguments with
+      [] -> return_expr @@ expr
+    | _ ->
+      let%bind arguments = map List.Ne.of_list @@
+        map (List.map (fun x -> CST.EPar (wrap @@ par @@ x))) @@
+        bind_map_list decompile_expression arguments in
+      let const = wrap (expr, arguments) in
+      return_expr_with_par @@ CST.ECall const
+    )
+  | E_literal literal ->
+    (match literal with
+        Literal_unit  ->  return_expr @@ CST.EUnit (wrap (rg,rg))
+      | Literal_int i ->  return_expr @@ CST.EArith (Int (wrap ("",i)))
+      | Literal_nat n ->  return_expr @@ CST.EArith (Nat (wrap ("",n)))
+      | Literal_timestamp time ->
+        let time = Tezos_utils.Time.Protocol.to_notation @@
+          Tezos_utils.Time.Protocol.of_seconds @@ Z.to_int64 time in
+          (* TODO combinators for CSTs. *)
+        let%bind ty = decompile_type_expr @@ AST.t_timestamp () in
+        let time = CST.EString (String (wrap time)) in
+        return_expr @@ CST.EAnnot (wrap @@ par (time, rg, ty))
+      | Literal_mutez mtez -> return_expr @@ CST.EArith (Mutez (wrap ("",mtez)))
+      | Literal_string (Standard str) -> return_expr @@ CST.EString (String   (wrap str))
+      | Literal_string (Verbatim ver) -> return_expr @@ CST.EString (Verbatim (wrap ver))
+      | Literal_bytes b ->
+        let b = Hex.of_bytes b in
+        let s = Hex.to_string b in
+        return_expr @@ CST.EBytes (wrap (s,b))
+      | Literal_address addr ->
+        let addr = CST.EString (String (wrap addr)) in
+        let%bind ty = decompile_type_expr @@ AST.t_address () in
+        return_expr @@ CST.EAnnot (wrap @@ par (addr,rg,ty))
+      | Literal_signature sign ->
+        let sign = CST.EString (String (wrap sign)) in
+        let%bind ty = decompile_type_expr @@ AST.t_signature () in
+        return_expr @@ CST.EAnnot (wrap @@ par (sign,rg,ty))
+      | Literal_key k ->
+        let k = CST.EString (String (wrap k)) in
+        let%bind ty = decompile_type_expr @@ AST.t_key () in
+        return_expr @@ CST.EAnnot (wrap @@ par (k,rg,ty))
+      | Literal_key_hash kh ->
+        let kh = CST.EString (String (wrap kh)) in
+        let%bind ty = decompile_type_expr @@ AST.t_key_hash () in
+        return_expr @@ CST.EAnnot (wrap @@ par (kh,rg,ty))
+      | Literal_chain_id _
+      | Literal_void
+      | Literal_operation _ ->
+        failwith "chain_id, void, operation are not created currently ?"
+    )
+  | E_application {lamb;args} ->
+    let%bind lamb = decompile_expression lamb in
+    let%bind args = map List.Ne.of_list @@
+      bind (bind_map_list decompile_expression) @@
+      get_e_tuple args
+    in
+    return_expr @@ CST.ECall (wrap (lamb,args))
+  | E_lambda lambda ->
+    let%bind (binders,_lhs_type,_block_with,body) = decompile_lambda lambda in
+    let fun_expr : CST.fun_expr = {kwd_fun=rg;binders;lhs_type=None;arrow=rg;body} in
+    return_expr_with_par @@ CST.EFun (wrap @@ fun_expr)
+  | E_recursive _ ->
+    failwith "corner case : annonymous recursive function"
+  | E_let_in {let_binder;rhs;let_result;inline} ->
+    let var = CST.PVar (decompile_variable @@ fst let_binder) in
+    let binders = (var,[]) in
+    let%bind lhs_type = bind_map_option (bind_compose (ok <@ prefix_colon) decompile_type_expr) @@ snd let_binder in
+    let%bind let_rhs = decompile_expression rhs in
+    let binding : CST.let_binding = {binders;lhs_type;eq=rg;let_rhs} in
+    let%bind body = decompile_expression let_result in
+    let attributes = decompile_attributes inline in
+    let lin : CST.let_in = {kwd_let=rg;kwd_rec=None;binding;kwd_in=rg;body;attributes} in
+    return_expr @@ CST.ELetIn (wrap lin)
+  | E_raw_code {language; code} ->
+    let language = wrap @@ wrap @@ language in
+    let%bind code = decompile_expression code in
+    let ci : CST.code_inj = {language;code;rbracket=rg} in
+    return_expr @@ CST.ECodeInj (wrap ci)
+  | E_constructor {constructor;element} ->
+    let Constructor constr = constructor in
+    let constr = wrap constr in
+    let%bind element = decompile_expression element in
+    return_expr_with_par @@ CST.EConstr (EConstrApp (wrap (constr, Some element)))
+  | E_matching {matchee; cases} ->
+    let%bind expr  = decompile_expression matchee in
+    let%bind cases = decompile_matching_cases cases in
+    let cases : _ CST.case = {kwd_match=rg;expr;kwd_with=rg;lead_vbar=None;cases} in
+    return_expr @@ CST.ECase (wrap cases)
+  | E_record record  ->
+    let record = AST.LMap.to_kv_list record in
+    let aux (AST.Label str, expr) =
+      let field_name = wrap str in
+      let%bind field_expr = decompile_expression expr in
+      let field : CST.field_assign = {field_name;assignment=rg;field_expr} in
+      ok @@ wrap field
+    in
+    let%bind record = bind_map_list aux record in
+    let%bind record = list_to_nsepseq record in
+    let record = ne_inject braces record in
+    (* why is the record not empty ? *)
+    return_expr @@ CST.ERecord (wrap record)
+  | E_accessor {record; path} ->
+    (match List.rev path with
+      Access_map e :: [] ->
+      let%bind map = decompile_expression record in
+      let%bind e = decompile_expression e in
+      let arg = e,[map] in
+      return_expr @@ CST.ECall( wrap (CST.EVar (wrap "Map.find_opt"), arg))
+    | Access_map e :: lst ->
+      let path = List.rev lst in
+      let%bind field_path = bind list_to_nsepseq @@ bind_map_list decompile_to_selection path in
+      let%bind struct_name = map (decompile_variable) @@ get_e_variable record in
+      let proj : CST.projection = {struct_name;selector=rg;field_path} in
+      let%bind e = decompile_expression e in
+      let arg = e,[CST.EProj (wrap proj)] in
+      return_expr @@ CST.ECall( wrap (CST.EVar (wrap "Map.find_opt"), arg))
+    | _ ->
+      let%bind field_path = bind list_to_nsepseq @@ bind_map_list decompile_to_selection path in
+       let%bind struct_name = map (decompile_variable) @@ get_e_variable record in
+      let proj : CST.projection = {struct_name;selector=rg;field_path} in
+      return_expr @@ CST.EProj (wrap proj)
+    )
+  (* Update on multiple field of the same record. may be removed by adding sugar *)
+  | E_update {record={expression_content=E_update _;_} as record;path;update} ->
+    let%bind record = decompile_expression record in
+    let%bind (record,updates) = match record with
+      CST.EUpdate {value;_} -> ok @@ (value.record,value.updates)
+    | _ -> failwith @@ Format.asprintf "Inpossible case %a" AST.PP.expression expr
+    in
+    let%bind var,path = match path with
+      Access_record var::path -> ok @@ (var,path)
+    | _ -> failwith "Impossible case %a"
+    in
+    let%bind field_path = decompile_to_path (Var.of_name var) path in
+    let%bind field_expr = decompile_expression update in
+    let field_assign : CST.field_path_assignment = {field_path;assignment=rg;field_expr} in
+    let updates = updates.value.ne_elements in
+    let updates = wrap @@ ne_inject braces @@ npseq_cons (wrap @@ field_assign) updates in
+    let update : CST.update = {lbrace=rg;record;kwd_with=rg;updates;rbrace=rg} in
+    return_expr @@ CST.EUpdate (wrap @@ update)
+  | E_update {record; path; update} ->
+    let%bind record = map (decompile_variable) @@ get_e_variable record in
+    let%bind field_expr = decompile_expression update in
+    let (struct_name,field_path) = List.Ne.of_list path in
+    (match field_path with
+      [] ->
+      (match struct_name with
+        Access_record name ->
+        let record : CST.path = Name record in
+        let field_path = CST.Name (wrap name) in
+        let update : CST.field_path_assignment = {field_path;assignment=rg;field_expr} in
+        let updates = wrap @@ ne_inject braces @@ (wrap update,[]) in
+        let update : CST.update = {lbrace=rg;record;kwd_with=rg;updates;rbrace=rg} in
+        return_expr @@ CST.EUpdate (wrap update)
+      | Access_tuple i ->
+        let record : CST.path = Name record in
+        let field_path = CST.Name (wrap @@ Z.to_string i) in
+        let update : CST.field_path_assignment = {field_path;assignment=rg;field_expr} in
+        let updates = wrap @@ ne_inject braces @@ (wrap update,[]) in
+        let update : CST.update = {lbrace=rg;record;kwd_with=rg;updates;rbrace=rg} in
+        return_expr @@ CST.EUpdate (wrap update)
+      | Access_map e ->
+        let%bind e = decompile_expression e in
+        let arg = field_expr,[e; CST.EVar record] in
+        return_expr @@ CST.ECall (wrap (CST.EVar (wrap "Map.add"), arg))
+      )
+    | _ ->
+      let%bind struct_name = match struct_name with
+          Access_record name -> ok @@ wrap name
+        | Access_tuple i -> ok @@ wrap @@ Z.to_string i
+        | Access_map _ -> failwith @@ Format.asprintf "invalid map update %a" AST.PP.expression expr
+      in
+      (match List.rev field_path with
+        Access_map e :: lst ->
+        let field_path = List.rev lst in
+        let%bind field_path = bind_map_list decompile_to_selection field_path in
+        let%bind field_path = list_to_nsepseq field_path in
+        let field_path : CST.projection = {struct_name; selector=rg;field_path} in
+        let field_path = CST.EProj (wrap @@ field_path) in
+        let%bind e = decompile_expression e in
+        let arg = field_expr, [e; field_path] in
+        return_expr @@ CST.ECall (wrap (CST.EVar (wrap "Map.add"),arg))
+      | _ ->
+        let%bind field_path = bind_map_list decompile_to_selection field_path in
+        let%bind field_path = list_to_nsepseq field_path in
+        let field_path : CST.projection = {struct_name; selector=rg;field_path} in
+        let field_path = CST.Path (wrap @@ field_path) in
+        let record : CST.path = Name record in
+        let update : CST.field_path_assignment = {field_path;assignment=rg;field_expr} in
+        let updates = wrap @@ ne_inject braces @@ (wrap update,[]) in
+        let update : CST.update = {lbrace=rg;record;kwd_with=rg;updates;rbrace=rg} in
+        return_expr @@ CST.EUpdate (wrap update)
+      )
+    )
+  | E_ascription {anno_expr;type_annotation} ->
+    let%bind expr = decompile_expression anno_expr in
+    let%bind ty   = decompile_type_expr type_annotation in
+    return_expr @@ CST.EAnnot (wrap @@ par (expr,rg,ty))
+  | E_cond {condition;then_clause;else_clause} ->
+    let%bind test  = decompile_expression condition in
+    let%bind ifso  = decompile_expression then_clause in
+    let%bind ifnot = decompile_expression else_clause in
+    let ifnot = Some(rg,ifnot) in
+    let cond : CST.cond_expr = {kwd_if=rg;test;kwd_then=rg;ifso;ifnot} in
+    return_expr @@ CST.ECond (wrap cond)
+  | E_sequence {expr1;expr2} ->
+    let%bind expr1 = decompile_expression expr1 in
+    let%bind expr2 = decompile_expression expr2 in
+    return_expr @@ CST.ESeq (wrap @@ inject beginEnd @@ list_to_sepseq [expr1; expr2])
+  | E_tuple tuple ->
+    let%bind tuple = bind_map_list decompile_expression tuple in
+    let%bind tuple = list_to_nsepseq tuple in
+    return_expr @@ CST.ETuple (wrap @@ tuple)
+  | E_map map ->
+    let%bind map = bind_map_list (bind_map_pair decompile_expression) map in
+    let aux (k,v) = CST.ETuple (wrap (k,[(rg,v)])) in
+    let map = List.map aux map in
+    (match map with
+      [] -> return_expr @@ CST.EVar (wrap "Big_map.empty")
+    | _  ->
+      let var = CST.EVar (wrap "Map.literal") in
+      return_expr @@ CST.ECall (wrap @@ (var, List.Ne.of_list @@ map))
+    )
+  | E_big_map big_map ->
+    let%bind big_map = bind_map_list (bind_map_pair decompile_expression) big_map in
+    let aux (k,v) = CST.ETuple (wrap (k,[(rg,v)])) in
+    let big_map = List.map aux big_map in
+    (match big_map with
+      [] -> return_expr @@ CST.EVar (wrap "Big_map.empty")
+    | _  ->
+      let var = CST.EVar (wrap "Big_map.literal") in
+      return_expr @@ CST.ECall (wrap @@ (var, List.Ne.of_list @@ big_map))
+    )
+  | E_list lst ->
+    let%bind lst = bind_map_list decompile_expression lst in
+    let lst = list_to_sepseq lst in
+    return_expr @@ CST.EList (EListComp (wrap @@ inject brackets @@ lst))
+  | E_set set ->
+    let%bind set = bind_map_list decompile_expression set in
+    let set = List.Ne.of_list @@ set in
+    let var = CST.EVar (wrap "Set.literal") in
+    return_expr @@ CST.ECall (wrap @@ (var,set))
+    (* We should avoid to generate skip instruction*)
+  | E_skip -> return_expr @@ CST.EUnit (wrap (rg,rg))
+  | E_assign _
+  | E_for _
+  | E_for_each _
+  | E_while _ ->
+    failwith @@ Format.asprintf "Decompiling a imperative construct to CameLIGO %a"
+    AST.PP.expression expr
+
+and decompile_to_path : AST.expression_variable -> AST.access list -> (CST.path, _) result = fun var access ->
+  let struct_name = decompile_variable var in
+  match access with
+    [] -> ok @@ CST.Name struct_name
+  | lst ->
+    let%bind field_path = bind list_to_nsepseq @@ bind_map_list decompile_to_selection lst in
+    let path : CST.projection = {struct_name;selector=rg;field_path} in
+    ok @@ (CST.Path (wrap @@ path) : CST.path)
+
+and decompile_to_selection : AST.access -> (CST.selection, _) result = fun access ->
+  match access with
+    Access_tuple index -> ok @@ CST.Component (wrap @@ ("",index))
+  | Access_record str  -> ok @@ CST.FieldName (wrap str)
+  | Access_map _ ->
+    failwith @@ Format.asprintf
+    "Can't decompile access_map to selection"
+
+and decompile_lambda : AST.lambda -> _ = fun {binder;input_type;output_type;result} ->
+    let%bind param_decl = pattern_type binder input_type in
+    let param = (param_decl, []) in
+    let%bind ret_type = bind_map_option (bind_compose (ok <@ prefix_colon) decompile_type_expr) output_type in
+    let%bind return = decompile_expression result in
+    ok @@ (param,ret_type,None,return)
+
+and decompile_attributes = function
+    true -> [wrap "inline"]
+  | false -> []
+
+and decompile_matching_cases : AST.matching_expr -> ((CST.expr CST.case_clause Region.reg, Region.t) Simple_utils.Utils.nsepseq Region.reg,_) result =
+fun m ->
+  let%bind cases = match m with
+    Match_variable (var, ty_opt, expr) ->
+    let%bind pattern = pattern_type var ty_opt in
+    let%bind rhs = decompile_expression expr in
+    let case : _ CST.case_clause = {pattern; arrow=rg; rhs}in
+    ok @@ [wrap case]
+  | Match_tuple (lst, ty_opt, expr) ->
+    let%bind tuple = match ty_opt with
+      Some ty_lst ->
+      let aux (var, ty) =
+        let pattern = CST.PVar (decompile_variable var) in
+        let%bind type_expr = decompile_type_expr ty in
+        ok @@ CST.PTyped (wrap @@ CST.{pattern;colon=rg;type_expr})
+      in
+      bind list_to_nsepseq @@ bind_map_list aux @@ List.combine lst ty_lst
+    | None ->
+      let aux var = CST.PVar (decompile_variable var) in
+      list_to_nsepseq @@ List.map aux lst
+    in
+    let pattern : CST.pattern = PTuple (wrap @@ tuple) in
+    let%bind rhs = decompile_expression expr in
+    let case : _ CST.case_clause = {pattern; arrow=rg; rhs}in
+    ok @@ [wrap case]
+  | Match_record _ -> failwith "match_record not availiable yet"
+  | Match_option {match_none;match_some}->
+    let%bind rhs = decompile_expression match_none in
+    let none_case : _ CST.case_clause = {pattern=PConstr (PNone rg);arrow=rg; rhs} in
+    let%bind rhs = decompile_expression @@ snd match_some in
+    let var = CST.PVar (decompile_variable @@ fst match_some)in
+    let some_case : _ CST.case_clause = {pattern=PConstr (PSomeApp (wrap (rg,var)));arrow=rg; rhs} in
+    ok @@ [wrap some_case;wrap none_case]
+  | Match_list {match_nil; match_cons} ->
+    let (hd,tl,expr) = match_cons in
+    let hd = CST.PVar (decompile_variable hd) in
+    let tl = CST.PVar (decompile_variable tl) in
+    let cons = (hd,rg,tl) in
+    let%bind rhs = decompile_expression @@ expr in
+    let cons_case : _ CST.case_clause = {pattern=PList (PCons (wrap cons));arrow=rg; rhs} in
+    let%bind rhs = decompile_expression @@ match_nil in
+    let nil_case : _ CST.case_clause = {pattern=PList (PListComp (wrap @@ inject brackets None));arrow=rg; rhs} in
+    ok @@ [wrap cons_case; wrap nil_case]
+  | Match_variant lst ->
+    let aux ((c,v),e) =
+      let AST.Constructor c = c in
+      let constr = wrap @@ c in
+      let var : CST.pattern = PVar (decompile_variable v) in
+      let tuple = var in
+      let pattern : CST.pattern = PConstr (PConstrApp (wrap (constr, Some tuple))) in
+      let%bind rhs = decompile_expression e in
+      let case : _ CST.case_clause = {pattern;arrow=rg;rhs} in
+      ok @@ wrap case
+    in
+    bind_map_list aux lst
+  in
+  map wrap @@ list_to_nsepseq cases
+let decompile_declaration : AST.declaration Location.wrap -> (CST.declaration, _) result = fun decl ->
+  let decl = Location.unwrap decl in
+  let wrap value = ({value;region=Region.ghost} : _ Region.reg) in
+  match decl with
+    Declaration_type (name, te) ->
+    let name = decompile_variable name in
+    let%bind type_expr = decompile_type_expr te in
+    ok @@ CST.TypeDecl (wrap (CST.{kwd_type=rg; name; eq=rg; type_expr}))
+  | Declaration_constant (var, ty_opt, inline, expr) ->
+    let attributes : CST.attributes = decompile_attributes inline in
+    let var = CST.PVar (decompile_variable var) in
+    let binders = (var,[]) in
+    match expr.expression_content with
+      E_lambda lambda ->
+      let%bind lhs_type = bind_map_option (bind_compose (ok <@ prefix_colon) decompile_type_expr) ty_opt in
+      let%bind let_rhs = decompile_expression @@ AST.make_e @@ AST.E_lambda lambda in
+      let let_binding : CST.let_binding = {binders;lhs_type;eq=rg;let_rhs} in
+      let let_decl : CST.let_decl = wrap (rg,None,let_binding,attributes) in
+      ok @@ CST.Let let_decl
+    | E_recursive {lambda; _} ->
+      let%bind lhs_type = bind_map_option (bind_compose (ok <@ prefix_colon) decompile_type_expr) ty_opt in
+      let%bind let_rhs = decompile_expression @@ AST.make_e @@ AST.E_lambda lambda in
+      let let_binding : CST.let_binding = {binders;lhs_type;eq=rg;let_rhs} in
+      let let_decl : CST.let_decl = wrap (rg,Some rg,let_binding,attributes) in
+      ok @@ CST.Let (let_decl)
+    | _ ->
+      let%bind lhs_type = bind_map_option (bind_compose (ok <@ prefix_colon) decompile_type_expr) ty_opt in
+      let%bind let_rhs = decompile_expression expr in
+      let let_binding : CST.let_binding = {binders;lhs_type;eq=rg;let_rhs} in
+      let let_decl : CST.let_decl = wrap (rg,None,let_binding,attributes) in
+      ok @@ CST.Let let_decl
+
+let decompile_program : AST.program -> (CST.ast, _) result = fun prg ->
+  let%bind decl = bind_map_list decompile_declaration prg in
+  let decl = List.Ne.of_list decl in
+  ok @@ ({decl;eof=rg}: CST.ast)

src/passes/03-tree_abstraction/pascaligo/compiler.ml

@@ -418,6 +418,11 @@ let rec compile_expression : CST.expr -> (AST.expr , abs_error) result = fun e -
     let (language, _) = r_split language in
     let%bind code = compile_expression ci.code in
     return @@ e_raw_code ~loc language code
+  | EBlock be ->
+    let be, _ = r_split be in
+    let%bind next = compile_expression be.expr in
+    compile_block ~next be.block
+
 
 and compile_matching_expr : type a.(a -> _ result) -> a CST.case_clause CST.reg List.Ne.t -> _ =
 fun compiler cases ->
@@ -497,11 +502,11 @@ fun compiler cases ->
     return @@ AST.Match_variant (List.combine constrs lst)
   | (p, _), _ -> fail @@ unsupported_pattern_type p
 
-let compile_attribute_declaration = function
+and compile_attribute_declaration = function
   None   -> return false
 | Some _ -> return true
 
-let compile_parameters (params : CST.parameters) =
+and compile_parameters (params : CST.parameters) =
   let compile_param_decl (param : CST.param_decl) =
     match param with
       ParamConst pc ->
@@ -519,10 +524,10 @@ let compile_parameters (params : CST.parameters) =
   let params = npseq_to_list params.inside in
   bind_map_list compile_param_decl params
 
-let rec compile_instruction : ?next: AST.expression -> CST.instruction -> _ result  = fun ?next instruction ->
+and compile_instruction : ?next: AST.expression -> CST.instruction -> _ result  = fun ?next instruction ->
   let return expr = match next with 
-    Some e -> return @@ e_sequence expr e
-  | None -> return expr
+    Some e -> ok @@ e_sequence expr e
+  | None -> ok @@ expr 
   in
   let compile_tuple_expression (tuple_expr : CST.tuple_expr) =
     let (lst, loc) = r_split tuple_expr in
@@ -733,16 +738,13 @@ and compile_block : ?next:AST.expression -> CST.block CST.reg -> _ result = fun
     Some block -> return block
   | None -> fail @@ block_start_with_attribute block
 
-and compile_fun_decl ({kwd_recursive; fun_name; param; ret_type; block_with; return=r; attributes}: CST.fun_decl) =
+and compile_fun_decl ({kwd_recursive; fun_name; param; ret_type; return=r; attributes}: CST.fun_decl) =
   let%bind attr = compile_attribute_declaration attributes in
   let (fun_name, loc) = r_split fun_name in
   let%bind ret_type = bind_map_option (compile_type_expression <@ snd) ret_type in
   let%bind param = compile_parameters param in
-  let%bind r     = compile_expression r in
+  let%bind result    = compile_expression r in
   let (param, param_type) = List.split param in
-  let%bind body = Option.unopt ~default:(return r) @@
-    Option.map (compile_block ~next:r <@ fst) block_with
-  in
   (* This handle the parameter case *)
   let (lambda,fun_type) = (match param_type with
     ty::[] ->
@@ -750,18 +752,18 @@ and compile_fun_decl ({kwd_recursive; fun_name; param; ret_type; block_with; ret
       binder = (Var.of_name @@ List.hd param);
       input_type  = ty ;
       output_type = ret_type ;
-      result = body;
+      result;
     } in
     lambda,Option.map (fun (a,b) -> t_function a b)@@ Option.bind_pair (ty,ret_type)
   | lst ->
     let lst = Option.bind_list lst in
     let input_type = Option.map t_tuple lst in
-    let binder = Var.fresh ~name:"parameter" () in
+    let binder = Var.fresh ~name:"parameters" () in
     let lambda : AST.lambda = {
       binder;
       input_type = input_type;
       output_type = ret_type;
-      result = e_matching_tuple_ez (e_variable binder) param lst body;
+      result = e_matching_tuple_ez (e_variable binder) param lst result;
     } in
     lambda,Option.map (fun (a,b) -> t_function a b)@@ Option.bind_pair (input_type,ret_type)
   )

src/passes/03-tree_abstraction/pascaligo/decompiler.ml

@@ -0,0 +1,660 @@
+module AST = Ast_imperative
+module CST = Cst.Pascaligo
+module Predefined = Predefined.Tree_abstraction.Pascaligo
+
+open Trace
+
+(* General tools *)
+let (<@) f g x = f (g x)
+
+(* Utils *)
+let rg = Region.ghost
+let wrap : type a. a -> a CST.reg = fun value -> {value;region=rg}
+let list_to_sepseq lst =
+  match lst with
+    [] -> None
+  |  hd :: lst ->
+      let aux e = (rg, e) in
+      Some (hd, List.map aux lst)
+let list_to_nsepseq lst =
+  match list_to_sepseq lst with
+    Some s -> ok @@ s
+  | None   -> failwith "List is not a non_empty list"
+let nelist_to_npseq (hd, lst) = (hd, List.map (fun e -> (rg, e)) lst)
+let npseq_cons hd lst = hd,(rg, fst lst)::(snd lst)
+
+let par a = CST.{lpar=rg;inside=a;rpar=rg}
+let braces a = CST.{lbrace=rg;inside=a;rbrace=rg}
+let brackets a = CST.{lbracket=rg;inside=a;rbracket=rg}
+let inject kind a = CST.{kind;enclosing=Brackets (rg,rg);elements=a;terminator=Some(rg)}
+let ne_inject kind a = CST.{kind;enclosing=Brackets (rg,rg);ne_elements=a;terminator=Some(rg)}
+let prefix_colon a = (rg, a)
+let suffix_with a = (a, rg)
+let to_block a = CST.{enclosing=Block (rg,rg,rg);statements=a;terminator=Some rg}
+let empty_block = to_block (CST.Instr (CST.Skip rg),[])
+
+(* Decompiler *)
+
+let decompile_variable : type a. a Var.t -> CST.variable = fun var ->
+  let var = Format.asprintf "%a" Var.pp var in
+  if String.contains var '#' then
+    let var = String.split_on_char '#' var in
+    wrap @@ "gen__" ^ (String.concat "" var)
+  else
+    if String.length var > 4 && String.equal "gen__" @@ String.sub var 0 5 then
+      wrap @@ "user__" ^ var
+    else
+      wrap @@ var
+
+let rec decompile_type_expr : AST.type_expression -> _ result = fun te ->
+  let return te = ok @@ te in
+  match te.type_content with
+    T_sum sum ->
+    let sum = AST.CMap.to_kv_list sum in
+    let aux (AST.Constructor c, AST.{ctor_type;_}) =
+      let constr = wrap c in
+      let%bind arg = decompile_type_expr ctor_type in
+      let arg = Some (rg, arg) in
+      let variant : CST.variant = {constr;arg} in
+      ok @@ wrap variant
+    in
+    let%bind sum = bind_map_list aux sum in
+    let%bind sum = list_to_nsepseq sum in
+    return @@ CST.TSum (wrap sum)
+  | T_record record ->
+    let record = AST.LMap.to_kv_list record in
+    let aux (AST.Label c, AST.{field_type;_}) =
+      let field_name = wrap c in
+      let colon = rg in
+      let%bind field_type = decompile_type_expr field_type in
+      let variant : CST.field_decl = {field_name;colon;field_type} in
+      ok @@ wrap variant
+    in
+    let%bind record = bind_map_list aux record in
+    let%bind record = list_to_nsepseq record in
+    return @@ CST.TRecord (wrap @@ ne_inject (NEInjRecord rg) record)
+  | T_tuple tuple ->
+    let%bind tuple = bind_map_list decompile_type_expr tuple in
+    let%bind tuple = list_to_nsepseq @@ tuple in
+    return @@ CST.TProd (wrap tuple)
+  | T_arrow {type1;type2} ->
+    let%bind type1 = decompile_type_expr type1 in
+    let%bind type2 = decompile_type_expr type2 in
+    let arrow = (type1, rg, type2) in
+    return @@ CST.TFun (wrap arrow)
+  | T_variable var ->
+    let var = decompile_variable var in
+    return @@ CST.TVar (var)
+  | T_constant const ->
+    let const = Predefined.type_constant_to_string const in
+    return @@ CST.TVar (wrap const)
+  | T_operator (operator, lst) ->
+    let operator = wrap @@ Predefined.type_operator_to_string operator in
+    let%bind lst = bind_map_list decompile_type_expr lst in
+    let%bind lst = list_to_nsepseq lst in
+    let lst : _ CST.par = {lpar=rg;inside=lst;rpar=rg} in
+    return @@ CST.TApp (wrap (operator,wrap lst))
+  | T_annoted _annot ->
+    failwith "let's work on it later"
+
+let get_e_variable : AST.expression -> _ result = fun expr ->
+  match expr.expression_content with
+    E_variable var -> ok @@ var
+  | _ -> failwith @@
+    Format.asprintf "%a should be a variable expression"
+    AST.PP.expression expr
+
+let rec get_e_accessor : AST.expression -> _ result = fun expr ->
+  match expr.expression_content with
+    E_variable var -> ok @@ (var, [])
+  | E_accessor {record;path} ->
+    let%bind (var, lst) = get_e_accessor record in
+    ok @@ (var, lst @ path)
+  | _ -> failwith @@
+    Format.asprintf "%a should be a variable expression"
+    AST.PP.expression expr
+
+let get_e_tuple : AST.expression -> _ result = fun expr ->
+  match expr.expression_content with
+    E_tuple tuple -> ok @@ tuple
+  | E_variable _
+  | E_literal _
+  | E_constant _
+  | E_lambda _ -> ok @@ [expr]
+  | _ -> failwith @@
+    Format.asprintf "%a should be a tuple expression"
+    AST.PP.expression expr
+type eos =
+| Expression
+| Statements
+
+type state = Cst_pascaligo.ParserLog.state
+
+let statements_of_expression : CST.expr -> CST.statement List.Ne.t option = fun stat ->
+  match stat with
+  | CST.ECall call -> Some (CST.Instr (CST.ProcCall call), [])
+  | _ -> None
+
+let rec decompile_expression : AST.expression -> _ result = fun e ->
+  let%bind (block,expr) = decompile_to_block e in
+  match expr with
+    Some expr ->
+    ( match block with
+      Some block ->
+        let block = wrap @@ block in
+        ok @@ CST.EBlock (wrap @@ CST.{block;kwd_with=rg;expr})
+    | None -> ok @@ expr
+    )
+  | None ->
+    failwith @@ Format.asprintf
+      "An expression was expected, but this was decompile to statements. \n
+      Expr : %a
+      Loc : %a"
+      AST.PP.expression e
+      Location.pp e.location
+
+and decompile_statements : AST.expression -> _ result = fun expr ->
+  let%bind (stat,_) = decompile_eos Statements expr in
+  match stat with
+    Some stat -> ok @@ stat
+  | None ->
+      failwith @@ Format.asprintf
+        "Statements was expected, but this was decompile to expression. \n
+        Expr : %a
+        Loc : %a"
+        AST.PP.expression expr
+        Location.pp expr.location
+
+and decompile_to_block : AST.expression -> _ result = fun expr ->
+  let to_block a = CST.{enclosing=Block (rg,rg,rg);statements=a;terminator=Some rg} in
+  let%bind (stats,next) = decompile_eos Expression expr in
+  let block = Option.map (to_block <@ nelist_to_npseq) stats in
+  ok @@ (block, next)
+
+and decompile_to_tuple_expr : AST.expression list -> (CST.tuple_expr,_) result = fun expr ->
+  let%bind tuple_expr = bind_map_list decompile_expression expr in
+  let%bind tuple_expr = list_to_nsepseq tuple_expr in
+  let tuple_expr : CST.tuple_expr = wrap @@ par @@  tuple_expr in
+  ok @@ tuple_expr
+
+and decompile_eos : eos -> AST.expression -> ((CST.statement List.Ne.t option)* (CST.expr option), _) result = fun output expr ->
+  let return (a,b) = ok @@ (a,b) in
+  let return_expr expr = return @@ (None, Some expr) in
+  let return_expr_with_par expr = return_expr @@ CST.EPar (wrap @@ par @@ expr) in
+  let return_stat stat = return @@ (Some stat, None) in
+  let return_stat_ez stat = return_stat @@ (stat, []) in
+  let return_inst inst = return_stat_ez @@ CST.Instr inst in
+  match expr.expression_content with
+    E_variable name ->
+    let var = decompile_variable name in
+    return_expr @@ CST.EVar (var)
+  | E_constant {cons_name; arguments} ->
+    let expr = CST.EVar (wrap @@ Predefined.constant_to_string cons_name) in
+    (match arguments with
+      [] -> return_expr @@ expr
+    | _ ->
+      let%bind arguments = decompile_to_tuple_expr arguments in
+      let const : CST.fun_call = wrap (expr, arguments) in
+      (match output with
+        Expression -> return_expr (CST.ECall const)
+      | Statements -> return_inst (CST.ProcCall const)
+      )
+    )
+  | E_literal literal ->
+    (match literal with
+        Literal_unit  ->  return_expr @@ CST.EUnit rg
+      | Literal_int i ->  return_expr @@ CST.EArith (Int (wrap ("",i)))
+      | Literal_nat n ->  return_expr @@ CST.EArith (Nat (wrap ("",n)))
+      | Literal_timestamp time ->
+        let time = Tezos_utils.Time.Protocol.to_notation @@
+          Tezos_utils.Time.Protocol.of_seconds @@ Z.to_int64 time in
+          (* TODO combinators for CSTs. *)
+        let%bind ty = decompile_type_expr @@ AST.t_timestamp () in
+        let time = CST.EString (String (wrap time)) in
+        return_expr @@ CST.EAnnot (wrap @@ par (time, rg, ty))
+      | Literal_mutez mtez -> return_expr @@ CST.EArith (Mutez (wrap ("",mtez)))
+      | Literal_string (Standard str) -> return_expr @@ CST.EString (String   (wrap str))
+      | Literal_string (Verbatim ver) -> return_expr @@ CST.EString (Verbatim (wrap ver))
+      | Literal_bytes b ->
+        let b = Hex.of_bytes b in
+        let s = Hex.to_string b in
+        return_expr @@ CST.EBytes (wrap (s,b))
+      | Literal_address addr ->
+        let addr = CST.EString (String (wrap addr)) in
+        let%bind ty = decompile_type_expr @@ AST.t_address () in
+        return_expr @@ CST.EAnnot (wrap @@ par (addr,rg,ty))
+      | Literal_signature sign ->
+        let sign = CST.EString (String (wrap sign)) in
+        let%bind ty = decompile_type_expr @@ AST.t_signature () in
+        return_expr @@ CST.EAnnot (wrap @@ par (sign,rg,ty))
+      | Literal_key k ->
+        let k = CST.EString (String (wrap k)) in
+        let%bind ty = decompile_type_expr @@ AST.t_key () in
+        return_expr @@ CST.EAnnot (wrap @@ par (k,rg,ty))
+      | Literal_key_hash kh ->
+        let kh = CST.EString (String (wrap kh)) in
+        let%bind ty = decompile_type_expr @@ AST.t_key_hash () in
+        return_expr @@ CST.EAnnot (wrap @@ par (kh,rg,ty))
+      | Literal_chain_id _
+      | Literal_void
+      | Literal_operation _ ->
+        failwith "chain_id, void, operation are not created currently ?"
+    )
+  | E_application {lamb;args} ->
+    let%bind lamb = decompile_expression lamb in
+    let%bind args = bind decompile_to_tuple_expr @@ get_e_tuple args in
+    (match output with
+      Expression ->
+      return_expr @@ CST.ECall (wrap (lamb,args))
+    | Statements ->
+      return_inst @@ CST.ProcCall (wrap (lamb,args))
+    )
+  | E_lambda lambda ->
+    let%bind (param,ret_type,return) = decompile_lambda lambda in
+    let fun_expr : CST.fun_expr = {kwd_function=rg;param;ret_type;kwd_is=rg;return} in
+    return_expr_with_par @@ CST.EFun (wrap @@ fun_expr)
+  | E_recursive _ ->
+    failwith "corner case : annonymous recursive function"
+  | E_let_in {let_binder;rhs={expression_content=E_update {record={expression_content=E_variable var;_};path;update};_};let_result;inline=_} when Var.equal (fst let_binder) var ->
+    let%bind lhs = (match List.rev path with
+      Access_map e :: path ->
+      let%bind path  = decompile_to_path var @@ List.rev path in
+      let%bind index = map (wrap <@ brackets) @@ decompile_expression e in
+      let mlu : CST.map_lookup = {path; index} in
+      ok @@ CST.MapPath (wrap @@ mlu)
+    | _ ->
+      let%bind path  = decompile_to_path var @@ path in
+      ok @@ (CST.Path (path) : CST.lhs)
+    )
+    in
+    let%bind rhs = decompile_expression update in
+    let assign : CST.assignment = {lhs;assign=rg;rhs} in
+    let assign = CST.Instr (CST.Assign (wrap @@ assign)) in
+    let%bind (stat,expr) = decompile_eos output let_result in
+    let stat = (match stat with
+      Some (stat) -> Some (List.Ne.cons assign stat)
+    | None -> Some (assign,[])
+    )
+    in
+    return @@ (stat,expr)
+  | E_let_in {let_binder;rhs;let_result;inline} ->
+    let%bind lin = decompile_to_data_decl let_binder rhs inline in
+    let%bind (lst, expr) = decompile_eos Expression let_result in
+    let lst = match lst with
+      Some lst -> List.Ne.cons (CST.Data lin) lst
+    | None -> (CST.Data lin, [])
+    in
+    return @@ (Some lst, expr)
+  | E_raw_code {language; code} ->
+    let language = wrap @@ wrap @@ language in
+    let%bind code = decompile_expression code in
+    let ci : CST.code_inj = {language;code;rbracket=rg} in
+    return_expr @@ CST.ECodeInj (wrap ci)
+  | E_constructor {constructor;element} ->
+    let Constructor constr = constructor in
+    let constr = wrap constr in
+    let%bind element = bind decompile_to_tuple_expr @@ get_e_tuple element in
+    return_expr_with_par @@ CST.EConstr (ConstrApp (wrap (constr, Some element)))
+  | E_matching {matchee; cases} ->
+    let%bind expr  = decompile_expression matchee in
+    (match output with
+      Expression ->
+      let%bind cases = decompile_matching_expr decompile_expression cases in
+      let cases : _ CST.case = {kwd_case=rg;expr;kwd_of=rg;enclosing=End rg;lead_vbar=None;cases} in
+      return_expr @@ CST.ECase (wrap cases)
+    | Statements ->
+      let%bind cases = decompile_matching_expr decompile_if_clause cases in
+      let cases : _ CST.case = {kwd_case=rg;expr;kwd_of=rg;enclosing=End rg;lead_vbar=None;cases} in
+      return_inst @@ CST.CaseInstr (wrap cases)
+    )
+  | E_record record  ->
+    let record = AST.LMap.to_kv_list record in
+    let aux (AST.Label str, expr) =
+      let field_name = wrap str in
+      let%bind field_expr = decompile_expression expr in
+      let field : CST.field_assignment = {field_name;assignment=rg;field_expr} in
+      ok @@ wrap field
+    in
+    let%bind record = bind_map_list aux record in
+    let%bind record = list_to_nsepseq record in
+    let record = ne_inject (NEInjRecord rg) record in
+    (* why is the record not empty ? *)
+    return_expr @@ CST.ERecord (wrap record)
+  | E_accessor {record; path} ->
+    (match List.rev path with
+      Access_map e :: [] ->
+      let%bind (var,lst) = get_e_accessor @@ record in
+      let%bind path = decompile_to_path var lst in
+      let%bind e = decompile_expression e in
+      let index = wrap @@ brackets @@ e in
+      let mlu : CST.map_lookup = {path;index} in
+      return_expr @@ CST.EMap(MapLookUp (wrap @@ mlu))
+    | Access_map e :: lst ->
+      let path = List.rev lst in
+      let%bind field_path = bind list_to_nsepseq @@ bind_map_list decompile_to_selection path in
+      let%bind struct_name = map (decompile_variable) @@ get_e_variable record in
+      let proj : CST.projection = {struct_name;selector=rg;field_path} in
+      let path : CST.path = CST.Path (wrap proj) in
+      let%bind e = decompile_expression e in
+      let index = wrap @@ brackets @@ e in
+      let mlu : CST.map_lookup = {path;index} in
+      return_expr @@ CST.EMap(MapLookUp (wrap @@ mlu))
+    | _ ->
+      let%bind field_path = bind list_to_nsepseq @@ bind_map_list decompile_to_selection path in
+       let%bind struct_name = map (decompile_variable) @@ get_e_variable record in
+      let proj : CST.projection = {struct_name;selector=rg;field_path} in
+      return_expr @@ CST.EProj (wrap proj)
+    )
+  (* Update on multiple field of the same record. may be removed by adding sugar *)
+  | E_update {record={expression_content=E_update _;_} as record;path;update} ->
+    let%bind record = decompile_expression record in
+    let%bind (record,updates) = match record with
+      CST.EUpdate {value;_} -> ok @@ (value.record,value.updates)
+    | _ -> failwith @@ Format.asprintf "Inpossible case %a" AST.PP.expression expr
+    in
+    let%bind var,path = match path with
+      Access_record var::path -> ok @@ (var,path)
+    | _ -> failwith "Impossible case %a"
+    in
+    let%bind field_path = decompile_to_path (Var.of_name var) path in
+    let%bind field_expr = decompile_expression update in
+    let field_assign : CST.field_path_assignment = {field_path;assignment=rg;field_expr} in
+    let updates = updates.value.ne_elements in
+    let updates = wrap @@ ne_inject (NEInjRecord rg) @@ npseq_cons (wrap @@ field_assign) updates in
+    let update : CST.update = {record;kwd_with=rg;updates} in
+    return_expr @@ CST.EUpdate (wrap @@ update)
+  | E_update {record; path; update} ->
+    let%bind record = map (decompile_variable) @@ get_e_variable record in
+    let%bind field_expr = decompile_expression update in
+    let (struct_name,field_path) = List.Ne.of_list path in
+    (match field_path with
+      [] ->
+      (match struct_name with
+        Access_record name ->
+        let record : CST.path = Name record in
+        let field_path = CST.Name (wrap name) in
+        let update : CST.field_path_assignment = {field_path;assignment=rg;field_expr} in
+        let updates = wrap @@ ne_inject (NEInjRecord rg) @@ (wrap update,[]) in
+        let update : CST.update = {record;kwd_with=rg;updates;} in
+        return_expr @@ CST.EUpdate (wrap update)
+      | Access_tuple _ -> failwith @@ Format.asprintf "invalid tuple update %a" AST.PP.expression expr
+      | Access_map e ->
+        let%bind e = decompile_expression e in
+        let arg : CST.tuple_expr = wrap @@ par @@ nelist_to_npseq (field_expr,[e; CST.EVar record]) in
+        return_expr @@ CST.ECall (wrap (CST.EVar (wrap "Map.add"), arg))
+      )
+    | _ ->
+      let%bind struct_name = match struct_name with
+          Access_record name -> ok @@ wrap name
+        | Access_tuple _ -> failwith @@ Format.asprintf "invalid tuple update %a" AST.PP.expression expr
+        | Access_map _ -> failwith @@ Format.asprintf "invalid map update %a" AST.PP.expression expr
+      in
+      (match List.rev field_path with
+        Access_map e :: lst ->
+        let field_path = List.rev lst in
+        let%bind field_path = bind_map_list decompile_to_selection field_path in
+        let%bind field_path = list_to_nsepseq field_path in
+        let field_path : CST.projection = {struct_name; selector=rg;field_path} in
+        let field_path = CST.EProj (wrap @@ field_path) in
+        let%bind e = decompile_expression e in
+        let arg = wrap @@ par @@ nelist_to_npseq (field_expr, [e; field_path]) in
+        return_expr @@ CST.ECall (wrap (CST.EVar (wrap "Map.add"),arg))
+      | _ ->
+        let%bind field_path = bind_map_list decompile_to_selection field_path in
+        let%bind field_path = list_to_nsepseq field_path in
+        let field_path : CST.projection = {struct_name; selector=rg;field_path} in
+        let field_path : CST.path = CST.Path (wrap @@ field_path) in
+        let record : CST.path = Name record in
+        let update : CST.field_path_assignment = {field_path;assignment=rg;field_expr} in
+        let updates = wrap @@ ne_inject (NEInjRecord rg) @@ (wrap update,[]) in
+        let update : CST.update = {record;kwd_with=rg;updates;} in
+        return_expr @@ CST.EUpdate (wrap update)
+      )
+    )
+  | E_ascription {anno_expr;type_annotation} ->
+    let%bind expr = decompile_expression anno_expr in
+    let%bind ty   = decompile_type_expr type_annotation in
+    return_expr @@ CST.EAnnot (wrap @@ par (expr,rg,ty))
+  | E_cond {condition;then_clause;else_clause} ->
+    let%bind test  = decompile_expression condition in
+    (match output with
+      Expression ->
+      let%bind ifso = decompile_expression then_clause in
+      let%bind ifnot = decompile_expression else_clause in
+      let cond : CST.cond_expr = {kwd_if=rg;test;kwd_then=rg;ifso;terminator=Some rg;kwd_else=rg;ifnot} in
+      return_expr @@ CST.ECond (wrap cond)
+    | Statements ->
+      let%bind ifso  = decompile_if_clause then_clause in
+      let%bind ifnot = decompile_if_clause else_clause in
+      let cond : CST.conditional = {kwd_if=rg;test;kwd_then=rg;ifso;terminator=Some rg; kwd_else=rg;ifnot} in
+      return_inst @@ CST.Cond (wrap cond)
+    )
+  | E_sequence {expr1;expr2} ->
+    let%bind expr1 = decompile_statements expr1 in
+    let%bind (expr2,next) = decompile_eos Statements expr2 in
+    let expr1 = Option.unopt ~default:expr1 @@ Option.map (List.Ne.append expr1) expr2 in
+    return @@ (Some expr1, next)
+  | E_skip -> return_inst @@ CST.Skip rg
+  | E_tuple tuple ->
+    let%bind tuple = bind_map_list decompile_expression tuple in
+    let%bind tuple = list_to_nsepseq tuple in
+    return_expr @@ CST.ETuple (wrap @@ par tuple)
+  | E_map map ->
+    let%bind map = bind_map_list (bind_map_pair decompile_expression) map in
+    let aux (k,v) =
+      let binding : CST.binding = {source=k;arrow=rg;image=v} in
+      wrap @@ binding
+    in
+    let map = list_to_sepseq @@ List.map aux map in
+    return_expr @@ CST.EMap (MapInj (wrap @@ inject (InjMap rg) @@ map))
+  | E_big_map big_map ->
+    let%bind big_map = bind_map_list (bind_map_pair decompile_expression) big_map in
+    let aux (k,v) =
+      let binding : CST.binding = {source=k;arrow=rg;image=v} in
+      wrap @@ binding
+    in
+    let big_map = list_to_sepseq @@ List.map aux big_map in
+    return_expr @@ CST.EMap (BigMapInj (wrap @@ inject (InjBigMap rg) @@ big_map))
+  | E_list lst ->
+    let%bind lst = bind_map_list decompile_expression lst in
+    let lst = list_to_sepseq lst in
+    return_expr @@ CST.EList (EListComp (wrap @@ inject (InjList rg) @@ lst))
+  | E_set set ->
+    let%bind set = bind_map_list decompile_expression set in
+    let set = list_to_sepseq set in
+    return_expr @@ CST.ESet (SetInj (wrap @@ inject (InjSet rg) @@ set))
+  | E_assign {variable;access_path;expression} ->
+    let%bind lhs = decompile_to_lhs variable access_path in
+    let%bind rhs = decompile_expression expression in
+    let assign : CST.assignment = {lhs;assign=rg;rhs} in
+    return_inst @@ Assign (wrap assign)
+  | E_for {binder;start;final;increment;body} ->
+    let binder     = decompile_variable binder in
+    let%bind init  = decompile_expression start in
+    let%bind bound = decompile_expression final in
+    let%bind step  = decompile_expression increment in
+    let step       = Some (rg, step) in
+    let%bind (block,_next) = decompile_to_block body in
+    let block = wrap @@ Option.unopt ~default:(empty_block) block in
+    let fl : CST.for_int = {kwd_for=rg;binder;assign=rg;init;kwd_to=rg;bound;step;block} in
+    return_inst @@ CST.Loop (For (ForInt (wrap fl)))
+  | E_for_each {binder;collection;collection_type;body} ->
+    let var = decompile_variable @@ fst binder in
+    let bind_to = Option.map (fun x -> (rg,decompile_variable x)) @@ snd binder in
+    let%bind expr = decompile_expression collection in
+    let collection = match collection_type with
+      Map -> CST.Map rg | Set -> Set rg | List -> List rg in
+    let%bind (block,_next) = decompile_to_block body in
+    let block = wrap @@ Option.unopt ~default:(empty_block) block in
+    let fc : CST.for_collect = {kwd_for=rg;var;bind_to;kwd_in=rg;collection;expr;block} in
+    return_inst @@ CST.Loop (For (ForCollect (wrap fc)))
+  | E_while {condition;body} ->
+    let%bind cond  = decompile_expression condition in
+    let%bind (block,_next) = decompile_to_block body in
+    let block = wrap @@ Option.unopt ~default:(empty_block) block in
+    let loop : CST.while_loop = {kwd_while=rg;cond;block} in
+    return_inst @@ CST.Loop (While (wrap loop))
+
+and decompile_if_clause : AST.expression -> (CST.if_clause, _) result = fun e ->
+  let%bind clause = decompile_statements e in
+  match clause with
+    CST.Instr instr,[] ->
+    ok @@ CST.ClauseInstr instr
+  | _ ->
+    let clause = nelist_to_npseq clause, Some rg in
+    ok @@ CST.ClauseBlock (ShortBlock (wrap @@ braces @@ clause))
+
+and decompile_to_data_decl : (AST.expression_variable * AST.type_expression option) -> AST.expression -> bool -> (CST.data_decl, _) result = fun (name,ty_opt) expr inline ->
+  let name = decompile_variable name in
+  let%bind const_type = bind_map_option (bind_compose (ok <@ prefix_colon) decompile_type_expr) ty_opt in
+  let attributes : CST.attr_decl option = match inline with
+    true -> Some (wrap @@ ne_inject (NEInjAttr rg) @@ (wrap @@ "inline",[]))
+  | false -> None
+  in
+  let fun_name = name in
+  match expr.expression_content with
+    E_lambda lambda ->
+    let%bind (param,ret_type,return) = decompile_lambda lambda in
+    let fun_decl : CST.fun_decl = {kwd_recursive=None;kwd_function=rg;fun_name;param;ret_type;kwd_is=rg;return;terminator=Some rg;attributes} in
+    ok @@ CST.LocalFun (wrap fun_decl)
+  | E_recursive {lambda; _} ->
+    let%bind (param,ret_type,return) = decompile_lambda lambda in
+    let fun_decl : CST.fun_decl = {kwd_recursive=Some rg;kwd_function=rg;fun_name;param;ret_type;kwd_is=rg;return;terminator=Some rg;attributes} in
+    ok @@ CST.LocalFun (wrap fun_decl)
+  | _ ->
+    let%bind init = decompile_expression expr in
+    let const_decl : CST.const_decl = {kwd_const=rg;name;const_type;equal=rg;init;terminator=Some rg; attributes} in
+    let data_decl  : CST.data_decl  =  LocalConst (wrap const_decl) in
+    ok @@ data_decl
+
+and decompile_to_lhs : AST.expression_variable -> AST.access list -> (CST.lhs, _) result = fun var access ->
+  match List.rev access with
+    [] -> ok @@ (CST.Path (Name (decompile_variable var)) : CST.lhs)
+  | hd :: tl ->
+    match hd with
+    | AST.Access_map e ->
+      let%bind path = decompile_to_path var @@ List.rev tl in
+      let%bind index = map (wrap <@ brackets) @@ decompile_expression e in
+      let mlu: CST.map_lookup = {path;index} in
+      ok @@ CST.MapPath (wrap @@ mlu)
+    | _ ->
+      let%bind path = decompile_to_path var @@ access in
+      ok @@ (CST.Path (path) : CST.lhs)
+
+and decompile_to_path : AST.expression_variable -> AST.access list -> (CST.path, _) result = fun var access ->
+  let struct_name = decompile_variable var in
+  match access with
+    [] -> ok @@ CST.Name struct_name
+  | lst ->
+    let%bind field_path = bind list_to_nsepseq @@ bind_map_list decompile_to_selection lst in
+    let path : CST.projection = {struct_name;selector=rg;field_path} in
+    ok @@ (CST.Path (wrap @@ path) : CST.path)
+
+and decompile_to_selection : AST.access -> (CST.selection, _) result = fun access ->
+  match access with
+    Access_tuple index -> ok @@ CST.Component (wrap @@ ("",index))
+  | Access_record str  -> ok @@ CST.FieldName (wrap str)
+  | Access_map _ ->
+    failwith @@ Format.asprintf
+    "Can't decompile access_map to selection"
+
+and decompile_lambda : AST.lambda -> _ = fun {binder;input_type;output_type;result} ->
+    let var = decompile_variable binder in
+    let%bind param_type = bind_map_option (bind_compose (ok <@ prefix_colon) decompile_type_expr) input_type in
+    let param_const : CST.param_const = {kwd_const=rg;var;param_type} in
+    let param_decl : CST.param_decl = ParamConst (wrap param_const) in
+    let param = nelist_to_npseq (param_decl, []) in
+    let param : CST.parameters = wrap @@ par param in
+    let%bind ret_type = bind_map_option (bind_compose (ok <@ prefix_colon) decompile_type_expr) output_type in
+    let%bind return = decompile_expression result in
+    ok @@ (param,ret_type,return)
+
+and decompile_matching_expr : type a.(AST.expr ->(a,_) result) -> AST.matching_expr -> ((a CST.case_clause Region.reg, Region.t) Simple_utils.Utils.nsepseq Region.reg,_) result =
+fun f m ->
+  let%bind cases = match m with
+    Match_variable (var, _ty_opt, expr) ->
+    let pattern : CST.pattern = PVar (decompile_variable var) in
+    let%bind rhs = f expr in
+    let case : _ CST.case_clause = {pattern; arrow=rg; rhs}in
+    ok @@ [wrap case]
+  | Match_tuple (lst, _ty_opt, expr) ->
+    let aux var = CST.PVar (decompile_variable var) in
+    let%bind tuple = list_to_nsepseq @@ List.map aux lst in
+    let pattern : CST.pattern = PTuple (wrap @@ par @@ tuple) in
+    let%bind rhs = f expr in
+    let case : _ CST.case_clause = {pattern; arrow=rg; rhs}in
+    ok @@ [wrap case]
+  | Match_record _ -> failwith "match_record not availiable yet"
+  | Match_option {match_none;match_some}->
+    let%bind rhs = f match_none in
+    let none_case : _ CST.case_clause = {pattern=PConstr (PNone rg);arrow=rg; rhs} in
+    let%bind rhs = f @@ snd match_some in
+    let var = wrap @@ par @@ CST.PVar (decompile_variable @@ fst match_some)in
+    let some_case : _ CST.case_clause = {pattern=PConstr (PSomeApp (wrap (rg,var)));arrow=rg; rhs} in
+    ok @@ [wrap some_case;wrap none_case]
+  | Match_list {match_nil; match_cons} ->
+    let (hd,tl,expr) = match_cons in
+    let hd = CST.PVar (decompile_variable hd) in
+    let tl = CST.PVar (decompile_variable tl) in
+    let cons = (hd,[rg,tl]) in
+    let%bind rhs = f @@ expr in
+    let cons_case : _ CST.case_clause = {pattern=PList (PCons (wrap cons));arrow=rg; rhs} in
+    let%bind rhs = f @@ match_nil in
+    let nil_case : _ CST.case_clause = {pattern=PList (PNil rg);arrow=rg; rhs} in
+    ok @@ [wrap cons_case; wrap nil_case]
+  | Match_variant lst ->
+    let aux ((c,v),e) =
+      let AST.Constructor c = c in
+      let constr = wrap @@ c in
+      let var : CST.pattern = PVar (decompile_variable v) in
+      let tuple = wrap @@ par @@ (var,[]) in
+      let pattern : CST.pattern = PConstr (PConstrApp (wrap (constr, Some tuple))) in
+      let%bind rhs = f e in
+      let case : _ CST.case_clause = {pattern;arrow=rg;rhs} in
+      ok @@ wrap case
+    in
+    bind_map_list aux lst
+  in
+  map wrap @@ list_to_nsepseq cases
+let decompile_declaration : AST.declaration Location.wrap -> (CST.declaration, _) result = fun decl ->
+  let decl = Location.unwrap decl in
+  let wrap value = ({value;region=Region.ghost} : _ Region.reg) in
+  match decl with
+    Declaration_type (name, te) ->
+    let kwd_type = Region.ghost
+    and name = decompile_variable name
+    and kwd_is = Region.ghost in
+    let%bind type_expr = decompile_type_expr te in
+    let terminator = Some Region.ghost in
+    ok @@ CST.TypeDecl (wrap (CST.{kwd_type; name; kwd_is; type_expr; terminator}))
+  | Declaration_constant (var, ty_opt, inline, expr) ->
+    let attributes = match inline with
+      true ->
+        let attr = wrap "inline" in
+        let ne_inj : _ CST.ne_injection =
+          {kind=NEInjAttr rg;enclosing=End rg;ne_elements=(attr, []);terminator=Some rg} in
+        let attr_decl = wrap ne_inj in
+        Some attr_decl
+    | false -> None
+    in
+    let name = decompile_variable var in
+    let fun_name = name in
+    match expr.expression_content with
+      E_lambda lambda ->
+      let%bind (param,ret_type,return) = decompile_lambda lambda in
+      let fun_decl : CST.fun_decl = {kwd_recursive=None;kwd_function=rg;fun_name;param;ret_type;kwd_is=rg;return;terminator=Some rg;attributes} in
+      ok @@ CST.FunDecl (wrap fun_decl)
+    | E_recursive {lambda; _} ->
+      let%bind (param,ret_type,return) = decompile_lambda lambda in
+      let fun_decl : CST.fun_decl = {kwd_recursive=Some rg;kwd_function=rg;fun_name;param;ret_type;kwd_is=rg;return;terminator=Some rg;attributes} in
+      ok @@ CST.FunDecl (wrap fun_decl)
+    | _ ->
+      let%bind const_type = bind_map_option (bind_compose (ok <@ prefix_colon) decompile_type_expr) ty_opt in
+      let%bind init = decompile_expression expr in
+      let const_decl : CST.const_decl = {kwd_const=rg;name;const_type;equal=rg;init;terminator=Some rg; attributes} in
+      ok @@ CST.ConstDecl (wrap const_decl)
+
+let decompile_program : AST.program -> (CST.ast, _) result = fun prg ->
+  let%bind decl = bind_map_list decompile_declaration prg in
+  let decl = List.Ne.of_list decl in
+  ok @@ ({decl;eof=rg}: CST.ast)

src/passes/03-tree_abstraction/pascaligo/pascaligo.ml

@@ -2,7 +2,11 @@ module CST = Cst.Pascaligo
 module AST = Ast_imperative
 
 module Compiler   = Compiler
+module Decompiler = Decompiler
 module Errors = Errors
 
 let compile_program      = Compiler.compile_program
 let compile_expression   = Compiler.compile_expression
+
+let decompile_program    = Decompiler.decompile_program
+let decompile_expression = Decompiler.decompile_expression

src/passes/03-tree_abstraction/pascaligo/pascaligo.mli

@@ -6,10 +6,14 @@ module Errors = Errors
 
 open Trace
 
-(** Convert a concrete PascaLIGO expression AST to the imperative
+(** Convert a concrete PascaLIGO expression CST to the imperative
     expression AST used by the compiler. *)
-val compile_expression : CST.expr -> (AST.expr , Errors.abs_error) result
+val compile_expression : CST.expr -> (AST.expr, Errors.abs_error) result
 
-(** Convert a concrete PascaLIGO program AST to the miperative program
+(** Convert a concrete PascaLIGO program CST to the miperative program
     AST used by the compiler. *)
 val compile_program : CST.ast -> (AST.program, Errors.abs_error) result
+
+val decompile_expression : AST.expr -> (CST.expr, _) result
+
+val decompile_program : AST.program -> (CST.ast, _) result

src/passes/05-purification/compiler.ml

@@ -252,7 +252,7 @@ and compile_expression' : I.expression -> (O.expression option -> O.expression,
       let%bind condition    = compile_expression condition in
       let%bind then_clause' = compile_expression then_clause in
       let%bind else_clause' = compile_expression else_clause in
-      let env = Var.fresh () in
+      let env = Var.fresh ~name:"env" () in
       let%bind ((_,free_vars_true), then_clause) = repair_mutable_variable_in_matching then_clause' [] env in
       let%bind ((_,free_vars_false), else_clause) = repair_mutable_variable_in_matching else_clause' [] env in
       let then_clause  = add_to_end then_clause (O.e_variable env) in
@@ -283,7 +283,9 @@ and compile_expression' : I.expression -> (O.expression option -> O.expression,
     | I.E_assign {variable; access_path; expression} ->
       let%bind access_path = compile_path access_path in
       let%bind expression = compile_expression expression in
-      let rhs = O.e_update ~loc (O.e_variable ~loc variable) access_path expression in
+      let rhs = match access_path with
+        [] -> expression
+      | _  -> O.e_update ~loc (O.e_variable ~loc variable) access_path expression in
       ok @@ fun expr -> (match expr with 
        | None -> O.e_let_in ~loc (variable,None) true false rhs (O.e_skip ())
        | Some e -> O.e_let_in ~loc (variable, None) true false rhs e
@@ -328,7 +330,7 @@ and compile_matching : I.matching -> Location.t -> (O.expression option -> O.exp
       let%bind match_none' = compile_expression match_none in
       let (n,expr) = match_some in
       let%bind expr' = compile_expression expr in
-      let env = Var.fresh () in
+      let env = Var.fresh ~name:"env" () in
       let%bind ((_,free_vars_none), match_none) = repair_mutable_variable_in_matching match_none' [] env in
       let%bind ((_,free_vars_some), expr) = repair_mutable_variable_in_matching expr' [n] env in
       let match_none = add_to_end match_none (O.e_variable env) in
@@ -348,7 +350,7 @@ and compile_matching : I.matching -> Location.t -> (O.expression option -> O.exp
       let%bind match_nil' = compile_expression match_nil in
       let (hd,tl,expr) = match_cons in
       let%bind expr' = compile_expression expr in
-      let env = Var.fresh () in
+      let env = Var.fresh ~name:"name" () in
       let%bind ((_,free_vars_nil), match_nil) = repair_mutable_variable_in_matching match_nil' [] env in
       let%bind ((_,free_vars_cons), expr) = repair_mutable_variable_in_matching expr' [hd;tl] env in
       let match_nil = add_to_end match_nil (O.e_variable env) in
@@ -365,7 +367,7 @@ and compile_matching : I.matching -> Location.t -> (O.expression option -> O.exp
       else
         return @@ O.e_matching ~loc matchee @@ O.Match_list {match_nil=match_nil'; match_cons=(hd,tl,expr')}
     | I.Match_variant lst ->
-      let env = Var.fresh () in
+      let env = Var.fresh ~name:"env" () in
       let aux fv ((c,n),expr) =
         let%bind expr = compile_expression expr in
         let%bind ((_,free_vars), case_clause) = repair_mutable_variable_in_matching expr [n] env in
@@ -401,8 +403,8 @@ and compile_matching : I.matching -> Location.t -> (O.expression option -> O.exp
       return @@ O.e_matching ~loc matchee @@ O.Match_variable (lst,ty_opt,expr)
  
 and compile_while I.{condition;body} =
-  let env_rec = Var.fresh () in
-  let binder  = Var.fresh () in
+  let env_rec = Var.fresh ~name:"env_rec" () in
+  let binder  = Var.fresh ~name:"binder"  () in
 
   let%bind cond = compile_expression condition in
   let ctrl = 
@@ -436,7 +438,7 @@ and compile_while I.{condition;body} =
 
 
 and compile_for I.{binder;start;final;increment;body} =
-  let env_rec = Var.fresh () in
+  let env_rec = Var.fresh ~name:"env_rec" () in
   (*Make the cond and the step *)
   let cond = I.e_annotation (I.e_constant C_LE [I.e_variable binder ; final]) (I.t_bool ()) in
   let%bind cond = compile_expression cond in
@@ -481,8 +483,8 @@ and compile_for I.{binder;start;final;increment;body} =
   ok @@ restore_mutable_variable return_expr captured_name_list env_rec 
 
 and compile_for_each I.{binder;collection;collection_type; body} =
-  let env_rec = Var.fresh () in
-  let args = Var.fresh () in
+  let env_rec = Var.fresh ~name:"env_rec" () in
+  let args    = Var.fresh ~name:"args" () in
 
   let%bind element_names = ok @@ match snd binder with
     | Some v -> [fst binder;v]

src/passes/07-desugaring/compiler.ml

@@ -6,7 +6,7 @@ open Errors
 
 let rec compile_type_expression : I.type_expression -> (O.type_expression , desugaring_error) result =
   fun te ->
-  let return tc = ok @@ O.make_t ~loc:te.location tc in
+  let return tc = ok @@ O.make_t ~loc:te.location ~sugar:te tc in
   match te.type_content with
     | I.T_sum sum -> 
       let sum = I.CMap.to_kv_list sum in
@@ -48,9 +48,9 @@ let rec compile_type_expression : I.type_expression -> (O.type_expression , desu
       return @@ T_operator (type_operator, lst)
 
 let rec compile_expression : I.expression -> (O.expression , desugaring_error) result =
-  fun e ->
-  let return expr = ok @@ O.make_e ~loc:e.location expr in
-  match e.expression_content with
+  fun sugar ->
+  let return expr = ok @@ O.make_e ~loc:sugar.location ~sugar expr in
+  match sugar.expression_content with
     | I.E_literal literal   -> return @@ O.E_literal literal
     | I.E_constant {cons_name;arguments} -> 
       let%bind arguments = bind_map_list compile_expression arguments in
@@ -81,7 +81,7 @@ let rec compile_expression : I.expression -> (O.expression , desugaring_error) r
       return @@ O.E_constructor {constructor;element}
     | I.E_matching {matchee; cases} ->
       let%bind matchee = compile_expression matchee in
-      compile_matching e.location matchee cases
+      compile_matching sugar matchee cases
     | I.E_record record ->
       let record = I.LMap.to_kv_list record in
       let%bind record = 
@@ -93,33 +93,33 @@ let rec compile_expression : I.expression -> (O.expression , desugaring_error) r
       return @@ O.E_record (O.LMap.of_list record)
     | I.E_accessor {record;path} ->
       let%bind record = compile_expression record in
-      let accessor ?loc e a =
+      let accessor ?loc expr a =
         match a with 
-          I.Access_tuple  i -> ok @@ O.e_record_accessor ?loc e (Label (Z.to_string i))
-        | I.Access_record a -> ok @@ O.e_record_accessor ?loc e (Label a)
+          I.Access_tuple  i -> ok @@ O.e_record_accessor ?loc expr (Label (Z.to_string i))
+        | I.Access_record a -> ok @@ O.e_record_accessor ?loc expr (Label a)
         | I.Access_map k -> 
           let%bind k = compile_expression k in
-          ok @@ O.e_constant ?loc C_MAP_FIND_OPT [k;e]
+          ok @@ O.e_constant ?loc C_MAP_FIND_OPT [k;expr]
       in
       bind_fold_list accessor record path
     | I.E_update {record;path;update} ->
       let%bind record = compile_expression record in
       let%bind update = compile_expression update in
-      let accessor ?loc e a =
+      let accessor ?loc expr a =
         match a with 
-          I.Access_tuple  i -> ok @@ O.e_record_accessor ?loc e (Label (Z.to_string i))
-        | I.Access_record a -> ok @@ O.e_record_accessor ?loc e (Label a)
+          I.Access_tuple  i -> ok @@ O.e_record_accessor ?loc expr (Label (Z.to_string i))
+        | I.Access_record a -> ok @@ O.e_record_accessor ?loc expr (Label a)
         | I.Access_map k -> 
           let%bind k = compile_expression k in
-          ok @@ O.e_constant ?loc C_MAP_FIND_OPT [k;e]
+          ok @@ O.e_constant ?loc C_MAP_FIND_OPT [k;expr]
       in
-      let updator ?loc (s:O.expression) a e =
+      let updator ?loc (s:O.expression) a expr =
         match a with
-          I.Access_tuple  i -> ok @@ O.e_record_update ?loc s (Label (Z.to_string i)) e
-        | I.Access_record a -> ok @@ O.e_record_update ?loc s (Label a) e
+          I.Access_tuple  i -> ok @@ O.e_record_update ?loc s (Label (Z.to_string i)) expr
+        | I.Access_record a -> ok @@ O.e_record_update ?loc s (Label a) expr
         | I.Access_map k ->
           let%bind k = compile_expression k in
-          ok @@ O.e_constant ?loc C_MAP_ADD [k;e;s]
+          ok @@ O.e_constant ?loc C_MAP_ADD [k;expr;s]
       in
       let aux (s, e : O.expression * _) lst =
         let%bind s' = accessor ~loc:s.location s lst in
@@ -176,7 +176,7 @@ let rec compile_expression : I.expression -> (O.expression , desugaring_error) r
       let%bind expr1 = compile_expression expr1 in
       let%bind expr2 = compile_expression expr2 in
       return @@ O.E_let_in {let_binder=(Var.of_name "_", Some (O.t_unit ())); rhs=expr1;let_result=expr2; inline=false}
-    | I.E_skip -> ok @@ O.e_unit ~loc:e.location ()
+    | I.E_skip -> ok @@ O.e_unit ~loc:sugar.location ~sugar ()
     | I.E_tuple t ->
       let aux (i,acc) el = 
         let%bind el = compile_expression el in
@@ -191,19 +191,20 @@ and compile_lambda : I.lambda -> (O.lambda , desugaring_error) result =
     let%bind output_type = bind_map_option compile_type_expression output_type in
     let%bind result = compile_expression result in
     ok @@ O.{binder;input_type;output_type;result}
-and compile_matching : Location.t -> O.expression -> I.matching_expr -> (O.expression, desugaring_error) result =
-  fun loc e m -> 
+and compile_matching : I.expression -> O.expression -> I.matching_expr -> (O.expression, desugaring_error) result =
+  fun sugar e m -> 
+  let loc = sugar.location in
   match m with 
     | I.Match_list {match_nil;match_cons} ->
       let%bind match_nil = compile_expression match_nil in
       let (hd,tl,expr) = match_cons in
       let%bind expr = compile_expression expr in
-      ok @@ O.e_matching ~loc e @@ O.Match_list {match_nil; match_cons=(hd,tl,expr)}
+      ok @@ O.e_matching ~loc ~sugar e @@ O.Match_list {match_nil; match_cons=(hd,tl,expr)}
     | I.Match_option {match_none;match_some} ->
       let%bind match_none = compile_expression match_none in
       let (n,expr) = match_some in
       let%bind expr = compile_expression expr in
-      ok @@ O.e_matching ~loc e @@ O.Match_option {match_none; match_some=(n,expr)}
+      ok @@ O.e_matching ~loc ~sugar e @@ O.Match_option {match_none; match_some=(n,expr)}
     | I.Match_variant lst ->
       let%bind lst = bind_map_list (
         fun ((c,n),expr) ->
@@ -211,7 +212,7 @@ and compile_matching : Location.t -> O.expression -> I.matching_expr -> (O.expre
           ok @@ ((c,n),expr)
       ) lst 
       in
-      ok @@ O.e_matching ~loc e @@ O.Match_variant lst
+      ok @@ O.e_matching ~loc ~sugar e @@ O.Match_variant lst
     | I.Match_record (fields,field_types, expr) ->
       let combine fields field_types =
         match field_types with
@@ -221,7 +222,7 @@ and compile_matching : Location.t -> O.expression -> I.matching_expr -> (O.expre
       let%bind next   = compile_expression expr in
       let%bind field_types = bind_map_option (bind_map_list compile_type_expression) field_types in
       let aux ((index,expr) : int * _ ) ((field,name): (O.label * (O.expression_variable * O.type_expression option))) =
-        let f = fun expr' -> O.e_let_in name false (O.e_record_accessor e field) expr' in
+        let f = fun expr' -> O.e_let_in ~sugar name false (O.e_record_accessor ~sugar e field) expr' in
         (index+1, fun expr' -> expr (f expr'))
       in
       let (_,header) = List.fold_left aux (0, fun e -> e) @@
@@ -238,7 +239,7 @@ and compile_matching : Location.t -> O.expression -> I.matching_expr -> (O.expre
       let%bind next   = compile_expression expr in
       let%bind field_types = bind_map_option (bind_map_list compile_type_expression) field_types in
       let aux ((index,expr) : int * _ ) (field: O.expression_variable * O.type_expression option) =
-        let f = fun expr' -> O.e_let_in field false (O.e_record_accessor e (Label (string_of_int index))) expr' in
+        let f = fun expr' -> O.e_let_in ~sugar field false (O.e_record_accessor ~sugar e (Label (string_of_int index))) expr' in
         (index+1, fun expr' -> expr (f expr'))
       in
       let (_,header) = List.fold_left aux (0, fun e -> e) @@
@@ -248,7 +249,7 @@ and compile_matching : Location.t -> O.expression -> I.matching_expr -> (O.expre
     | I.Match_variable (a, ty_opt, expr) ->
       let%bind ty_opt = bind_map_option compile_type_expression ty_opt in
       let%bind expr = compile_expression expr in
-      ok @@ O.e_let_in (a,ty_opt) false e expr
+      ok @@ O.e_let_in ~sugar (a,ty_opt) false e expr
  
 let compile_declaration : I.declaration Location.wrap -> _ =
   fun {wrap_content=declaration;location} ->
@@ -257,7 +258,7 @@ let compile_declaration : I.declaration Location.wrap -> _ =
   | I.Declaration_constant (n, te_opt, inline, expr) ->
     let%bind expr = compile_expression expr in
     let%bind te_opt = bind_map_option compile_type_expression te_opt in
-    return @@ O.Declaration_constant (n, te_opt, inline, expr)
+    return @@ O.Declaration_constant (n, te_opt, {inline}, expr)
   | I.Declaration_type (n, te) ->
     let%bind te = compile_type_expression te in
     return @@ O.Declaration_type (n,te)

src/passes/07-desugaring/decompiler.ml

@@ -7,7 +7,10 @@ open Errors
 let rec decompile_type_expression : O.type_expression -> (I.type_expression, desugaring_error) result =
   fun te ->
   let return te = ok @@ I.make_t te in
-  match te.type_content with
+  match te.sugar with 
+    Some te -> ok @@ te
+  | None ->
+    match te.content with
       | O.T_sum sum -> 
         let sum = I.CMap.to_kv_list sum in
         let%bind sum = 
@@ -43,7 +46,10 @@ let rec decompile_type_expression : O.type_expression -> (I.type_expression, des
 let rec decompile_expression : O.expression -> (I.expression, desugaring_error) result =
   fun e ->
   let return expr = ok @@ I.make_e ~loc:e.location expr in
-  match e.expression_content with 
+  match e.sugar with
+    Some e -> ok @@ e
+  | None -> 
+    match e.content with 
       O.E_literal lit -> return @@ I.E_literal lit
     | O.E_constant {cons_name;arguments} -> 
       let%bind arguments = bind_map_list decompile_expression arguments in
@@ -134,7 +140,7 @@ and decompile_matching : O.matching_expr -> (I.matching_expr, desugaring_error)
 let decompile_declaration : O.declaration Location.wrap -> _ result = fun {wrap_content=declaration;location} ->
   let return decl = ok @@ Location.wrap ~loc:location decl in
   match declaration with 
-  | O.Declaration_constant (n, te_opt, inline, expr) ->
+  | O.Declaration_constant (n, te_opt, {inline}, expr) ->
     let%bind expr = decompile_expression expr in
     let%bind te_opt = bind_map_option decompile_type_expression te_opt in
     return @@ I.Declaration_constant (n, te_opt, inline, expr)

src/passes/08-self_ast_core/helpers.ml

@@ -3,7 +3,6 @@ open Trace
 open Stage_common.Helpers
 
 include Stage_common.PP
-include Stage_common.Types.Ast_generic_type(Ast_core_parameter)
 
 let bind_map_cmap f map = bind_cmap (
   CMap.map 
@@ -23,7 +22,7 @@ type ('a,'err) folder = 'a -> expression -> ('a, 'err) result
 let rec fold_expression : ('a, 'err) folder -> 'a -> expression -> ('a,'err) result = fun f init e ->
   let self = fold_expression f in 
   let%bind init' = f init e in
-  match e.expression_content with
+  match e.content with
   | E_literal _ | E_variable _ | E_raw_code _ -> ok init'
   | E_constant {arguments=lst} -> (
     let%bind res = bind_fold_list self init' lst in
@@ -98,8 +97,8 @@ type 'err abs_mapper =
 let rec map_expression : 'err exp_mapper -> expression -> (expression , 'err) result = fun f e ->
   let self = map_expression f in
   let%bind e' = f e in
-  let return expression_content = ok { e' with expression_content } in
-  match e'.expression_content with
+  let return content = ok { e' with content } in
+  match e'.content with
   | E_ascription ascr -> (
       let%bind e' = self ascr.anno_expr in
       return @@ E_ascription {ascr with anno_expr=e'}
@@ -151,11 +150,11 @@ let rec map_expression : 'err exp_mapper -> expression -> (expression , 'err) re
   | E_literal _ | E_variable _ | E_raw_code _ as e' -> return e'
 
 and map_type_expression : 'err ty_exp_mapper -> type_expression -> (type_expression , 'err) result =
-    fun f ({type_content ; location ; type_meta} as te) ->
+    fun f ({content ; sugar; location } as te) ->
   let self = map_type_expression f in
   let%bind te' = f te in
-  let return type_content = ok { type_content; location ; type_meta } in
-  match type_content with
+  let return content = ok @@ ({ content; sugar; location}: type_expression) in
+  match content with
   | T_sum temap ->
     let%bind temap' = bind_map_cmap self temap in
     return @@ (T_sum temap')
@@ -212,8 +211,8 @@ let rec fold_map_expression : ('a , 'err) fold_mapper -> 'a -> expression -> ('a
   let%bind (continue, init',e') = f a e in
   if (not continue) then ok(init',e')
   else
-  let return expression_content = { e' with expression_content } in
-  match e'.expression_content with
+  let return content = { e' with content } in
+  match e'.content with
   | E_ascription ascr -> (
       let%bind (res,e') = self init' ascr.anno_expr in
       ok (res, return @@ E_ascription {ascr with anno_expr=e'})

src/passes/09-typing/08-typer-common/errors.ml

@@ -1,6 +1,7 @@
 open Trace
 open Simple_utils.Display
 
+
 let stage = "typer"
 
 type typer_error = [
@@ -69,7 +70,28 @@ type typer_error = [
   | `Typer_constant_decl_tracer of Ast_core.expression_variable * Ast_core.expr * Ast_typed.type_expression option * typer_error
   | `Typer_match_variant_tracer of Ast_core.matching_expr * typer_error
   | `Typer_unrecognized_type_operator of Ast_core.type_expression
-  |`Typer_expected_ascription of Ast_core.expression
+  | `Typer_expected_ascription of Ast_core.expression
+  | `Typer_different_kinds of Ast_typed.type_expression * Ast_typed.type_expression
+  | `Typer_different_constants of Ast_typed.type_constant * Ast_typed.type_constant
+  | `Typer_different_operators of Ast_typed.type_operator * Ast_typed.type_operator
+  | `Typer_operator_number_of_arguments of Ast_typed.type_operator * Ast_typed.type_operator * int * int
+  | `Typer_different_record_props of
+    Ast_typed.type_expression * Ast_typed.type_expression * Ast_typed.te_lmap * Ast_typed.te_lmap * string * string
+  | `Typer_different_kind_record_tuple of
+    Ast_typed.type_expression * Ast_typed.type_expression * Ast_typed.te_lmap * Ast_typed.te_lmap
+  | `Typer_different_size_records_tuples of
+    Ast_typed.type_expression * Ast_typed.type_expression * Ast_typed.te_lmap * Ast_typed.te_lmap
+  | `Typer_different_size_sums of
+    Ast_typed.type_expression * Ast_typed.type_expression
+  | `Typer_different_types of string * Ast_typed.type_expression * Ast_typed.type_expression * typer_error
+  | `Typer_different_literals of string * Ast_typed.literal * Ast_typed.literal
+  | `Typer_different_values of string * Ast_typed.expression * Ast_typed.expression
+  | `Typer_different_literals_because_different_types of string * Ast_typed.literal * Ast_typed.literal
+  | `Typer_different_values_because_different_types of string * Ast_typed.expression * Ast_typed.expression
+  | `Typer_uncomparable_literals of string * Ast_typed.literal * Ast_typed.literal
+  | `Typer_uncomparable_values of string * Ast_typed.expression * Ast_typed.expression
+  | `Typer_missing_key_in_record_value of string
+  | `Typer_compare_tracer of typer_error
 ]
 
 let michelson_comb_no_record (loc:Location.t) = `Typer_michelson_comb_no_record loc
@@ -150,6 +172,23 @@ let constant_declaration_tracer (name: Ast_core.expression_variable) (ae:Ast_cor
   `Typer_constant_decl_tracer (name,ae,expected,err)
 let in_match_variant_tracer (ae:Ast_core.matching_expr) (err:typer_error) =
   `Typer_match_variant_tracer (ae,err)
+let different_kinds a b = `Typer_different_kinds (a,b)
+let different_constants a b = `Typer_different_constants (a,b)
+let different_operators a b = `Typer_different_operators (a,b)
+let different_operator_number_of_arguments opa opb lena lenb = `Typer_operator_number_of_arguments (opa, opb, lena, lenb)
+let different_props_in_record a b ra rb ka kb = `Typer_different_record_props (a,b,ra,rb,ka,kb)
+let different_kind_record_tuple a b ra rb = `Typer_different_kind_record_tuple (a,b,ra,rb)
+let different_size_records_tuples a b ra rb = `Typer_different_size_records_tuples (a,b,ra,rb)
+let different_size_sums a b = `Typer_different_size_sums (a,b)
+let different_types name a b err = `Typer_different_types (name,a,b,err)
+let different_literals name a b = `Typer_different_literals (name,a,b)
+let different_values name a b = `Typer_different_values (name,a,b)
+let different_literals_because_different_types name a b = `Typer_different_literals_because_different_types (name,a,b)
+let different_values_because_different_types name a b = `Typer_different_values_because_different_types (name,a,b)
+let error_uncomparable_literals name a b = `Typer_uncomparable_literals (name,a,b)
+let error_uncomparable_values name a b = `Typer_uncomparable_values (name,a,b)
+let missing_key_in_record_value k = `Typer_missing_key_in_record_value k
+let compare_tracer err = `Typer_compare_tracer err
 
 let rec error_ppformat : display_format:string display_format ->
   Format.formatter -> typer_error -> unit =
@@ -470,6 +509,75 @@ let rec error_ppformat : display_format:string display_format ->
         "@[<hv>%a@ expected ascription but got %a@]"
         Location.pp t.location
         Ast_core.PP.expression t
+    | `Typer_different_kinds (a,b) ->
+      Format.fprintf f
+        "@[<hv> different kinds %a@ %a@]"
+        Ast_typed.PP.type_expression a
+        Ast_typed.PP.type_expression b
+    | `Typer_different_constants (a,b) ->
+      Format.fprintf f
+        "@[<hv> different type constructors.@ \
+        Expected these two constant type constructors to be the same, but they're different@ %a@ %a@]"
+        Ast_typed.PP.type_constant a
+        Ast_typed.PP.type_constant b
+    | `Typer_different_operators (a,b) ->
+      Format.fprintf f
+        "@[<hv> different type constructors.@ \
+        Expected these two n-ary type constructors to be the same, but they're different@ %a@ %a@]"
+        (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) a
+        (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) b
+    | `Typer_operator_number_of_arguments (opa, _opb, lena, lenb) ->
+      Format.fprintf f
+        "@[<hv> different number of arguments to type constructors.@ \
+        Expected these two n-ary type constructors to be the same, but they have different number\
+        of arguments (both use the %s type constructor, but they have %d and %d arguments, respectively)@]"
+        (Ast_typed.Helpers.type_operator_name opa) lena lenb
+    | `Typer_different_record_props (_a,_b,ra,rb,_ka,_kb) ->
+      let names = if Ast_typed.Helpers.is_tuple_lmap ra &&Ast_typed.Helpers.is_tuple_lmap rb
+        then "tuples" else "records" in
+      Format.fprintf f
+        "@[<hv> different keys in %s@]"
+        names
+    | `Typer_different_kind_record_tuple (_a,_b,ra,rb) ->
+      let name_a = if Ast_typed.Helpers.is_tuple_lmap ra then "tuple" else "record" in
+      let name_b = if Ast_typed.Helpers.is_tuple_lmap rb then "tuple" else "record" in
+      Format.fprintf f
+        "@[<hv> different keys.@ Expected these two types to be the same, but they're different (one is a %s\ 
+        and the other is a %s)@]"
+        name_a name_b
+    | `Typer_different_size_records_tuples (_a,_b,ra,rb) ->
+      let n = if Ast_typed.Helpers.is_tuple_lmap ra && Ast_typed.Helpers.is_tuple_lmap rb
+        then "tuples" else "records" in
+      Format.fprintf f 
+        "@[<hv> %s have different sizes.@ Expected these two types to be the same, but they're \
+        different (both are %s, but with a different number of arguments)@]"
+        n n
+    | `Typer_different_size_sums (_a,_b) ->
+      Format.fprintf f 
+        "@[<hv> sum types have different sizes.@ Expected these two types to be the same, but they're \
+        different"
+    | `Typer_different_types (name,_a,_b,err) ->
+      Format.fprintf f
+      "@[<hv> %s are different.\ 
+      Expected these two types to be the same, but they're different.@ %a@]"
+      name
+      (error_ppformat ~display_format) err
+    | `Typer_different_literals (name,_a,_b) ->
+      Format.fprintf f "@[<hv> %s are different@]" name
+    | `Typer_different_values (name,_a,_b) ->
+      Format.fprintf f "@[<hv> %s are different@]" name
+    | `Typer_different_literals_because_different_types (name,_a,_b) ->
+      Format.fprintf f "@[<hv> Literals have different types: %s@]" name
+    | `Typer_different_values_because_different_types (name,_a,_b) ->
+      Format.fprintf f "@[<hv> Values have different types: %s@]" name
+    | `Typer_uncomparable_literals (name,_a,_b) ->
+      Format.fprintf f "@[<hv> %s are not comparable @]" name
+    | `Typer_uncomparable_values (name,_a,_b) ->
+      Format.fprintf f "@[<hv> %s are not comparable @]" name
+    | `Typer_missing_key_in_record_value k ->
+      Format.fprintf f "@[<hv> missing %s in one of the record @]" k
+    | `Typer_compare_tracer err ->
+      error_ppformat ~display_format f err 
   )
 
 let rec error_jsonformat : typer_error -> J.t = fun a ->
@@ -1151,3 +1259,189 @@ let rec error_jsonformat : typer_error -> J.t = fun a ->
       ("value", value) ;
     ] in
     json_error ~stage ~content
+  | `Typer_different_kinds (a,b) ->
+    let message = `String "different kinds" in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_constants (a,b) ->
+    let message = `String "different type constructors.\
+      Expected these two constant type constructors to be the same, but they're different" in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_constant a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_constant b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_operators (a,b) ->
+    let message = `String "different type constructors.\
+      Expected these two n-ary type constructors to be the same, but they're different" in
+    let a = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) a) in
+    let b = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_operator_number_of_arguments (opa, opb, lena, lenb) ->
+    let message = `String "different number of arguments to type constructors.\ 
+      Expected these two n-ary type constructors to be the same, but they have different number\ 
+      of arguments" in
+    let a = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) opa) in
+    let b = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) opb) in
+    let op = `String (Ast_typed.Helpers.type_operator_name opa) in
+    let len_a = `Int lena in
+    let len_b = `Int lenb in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+      ("op", op) ;
+      ("len_a", len_a) ;
+      ("len_b", len_b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_record_props (a,b,ra,rb,ka,kb) ->
+    let names = if Ast_typed.Helpers.is_tuple_lmap ra &&Ast_typed.Helpers.is_tuple_lmap rb
+      then "tuples" else "records" in
+    let message = `String ("different keys in " ^ names) in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+      ("ka", `String ka) ;
+      ("kb", `String kb) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_kind_record_tuple (a,b,ra,rb) ->
+    let name_a = if Ast_typed.Helpers.is_tuple_lmap ra then "tuple" else "record" in
+    let name_b = if Ast_typed.Helpers.is_tuple_lmap rb then "tuple" else "record" in
+    let message = `String ("different keys. Expected these two types to be the same, but they're different (one is a "
+      ^ name_a ^ " and the other is a " ^ name_b ^ ")") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_size_records_tuples (a,b,ra,rb) ->
+    let n = if Ast_typed.Helpers.is_tuple_lmap ra && Ast_typed.Helpers.is_tuple_lmap rb
+       then "tuples" else "records" in
+    let message = `String (n^ " have different sizes. Expected these two types to be the same, but they're \
+      different (both are " ^ n ^ ", but with a different number of arguments)") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_size_sums (a,b) ->
+    let message = `String (" sum types have different sizes. Expected these two types to be the same, but they're \
+      different") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_types (name,a,b,err) ->
+    let message = `String (name ^" are different.\ 
+      Expected these two types to be the same, but they're different") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+      ("children", error_jsonformat err)
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_literals (name,a,b) ->
+    let message = `String (name ^ " are different") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.literal a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.literal b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_values (name,a,b) ->
+    let message = `String (name ^ " are different") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_literals_because_different_types (name,a,b) ->
+    let message = `String ("literals have different types: " ^ name) in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.literal a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.literal b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_values_because_different_types (name,a,b) ->
+    let message = `String ("values have different types: " ^ name) in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_uncomparable_literals (name,a,b) ->
+    let message = `String (name ^ " are not comparable") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.literal a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.literal b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_uncomparable_values (name,a,b) ->
+    let message = `String (name ^ " are not comparable") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_missing_key_in_record_value k ->
+    let message = `String "missing keys in one of the records" in
+    let content = `Assoc [
+      ("message", message) ;
+      ("missing_key", `String k) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_compare_tracer err ->
+    let content = `Assoc [
+      ("message", `String "not equal") ;
+      ("children", error_jsonformat err)
+    ] in
+    json_error ~stage ~content

src/passes/09-typing/08-typer-new/compare_types.ml

@@ -0,0 +1,165 @@
+open Ast_typed
+open Trace
+open Typer_common.Errors
+
+let rec assert_type_expression_eq (a, b: (type_expression * type_expression)) : (unit, typer_error) result = match (a.type_content, b.type_content) with
+  | T_constant ca, T_constant cb -> (
+      Assert.assert_true (different_constants ca cb) (ca = cb)
+    )
+  | T_constant _, _ -> fail @@ different_kinds a b
+  | T_operator opa, T_operator opb -> (
+    let%bind (lsta, lstb) = match (opa, opb) with
+      | TC_option la, TC_option lb
+      | TC_list la, TC_list lb
+      | TC_contract la, TC_contract lb
+      | TC_set la, TC_set lb -> ok @@ ([la], [lb])
+      | (TC_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb})
+      | (TC_big_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_big_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb})
+        -> ok @@ ([ka;va] ,[kb;vb]) 
+      | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ ),
+        (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ )
+        -> fail @@ different_operators opa opb
+      in
+      if List.length lsta <> List.length lstb then
+        fail @@ different_operator_number_of_arguments opa opb (List.length lsta) (List.length lstb)
+      else
+        trace (different_types "arguments to type operators" a b)
+        @@ bind_list_iter (fun (a,b) -> assert_type_expression_eq (a,b) )(List.combine lsta lstb)
+  )
+  | T_operator _, _ -> fail @@ different_kinds a b
+  | T_sum sa, T_sum sb -> (
+      let sa' = CMap.to_kv_list sa in
+      let sb' = CMap.to_kv_list sb in
+      let aux ((ka, {ctor_type=va;_}), (kb, {ctor_type=vb;_})) =
+        let%bind _ =
+          Assert.assert_true (corner_case "different keys in sum types")
+          @@ (ka = kb) in
+        assert_type_expression_eq (va, vb)
+      in
+      let%bind _ =
+        Assert.assert_list_same_size (different_size_sums a b)
+        sa' sb'
+      in
+      trace (different_types "sum type" a b) @@
+      bind_list_iter aux (List.combine sa' sb')
+    )
+  | T_sum _, _ -> fail @@ different_kinds a b
+  | T_record ra, T_record rb
+       when Helpers.is_tuple_lmap ra <> Helpers.is_tuple_lmap rb -> (
+    fail @@ different_kind_record_tuple a b ra rb
+  )
+  | T_record ra, T_record rb -> (
+      let sort_lmap r' = List.sort (fun (Label a,_) (Label b,_) -> String.compare a b) r' in
+      let ra' = sort_lmap @@ LMap.to_kv_list ra in
+      let rb' = sort_lmap @@ LMap.to_kv_list rb in
+      let aux ((ka, {field_type=va;_}), (kb, {field_type=vb;_})) =
+        let%bind _ =
+          trace (different_types "records" a b) @@
+          let Label ka = ka in
+          let Label kb = kb in
+          Assert.assert_true (different_props_in_record a b ra rb ka kb) (ka = kb) in
+        assert_type_expression_eq (va, vb)
+      in
+      let%bind _ =
+        Assert.assert_list_same_size (different_size_records_tuples a b ra rb) ra' rb' in
+      trace (different_types "record type" a b)
+      @@ bind_list_iter aux (List.combine ra' rb')
+
+    )
+  | T_record _, _ -> fail @@ different_kinds a b
+  | T_arrow {type1;type2}, T_arrow {type1=type1';type2=type2'} ->
+      let%bind _ = assert_type_expression_eq (type1, type1') in
+      let%bind _ = assert_type_expression_eq (type2, type2') in
+      ok ()
+  | T_arrow _, _ -> fail @@ different_kinds a b
+  | T_variable x, T_variable y -> let _ = (x = y) in failwith "TODO : we must check that the two types were bound at the same location (even if they have the same name), i.e. use something like De Bruijn indices or a propper graph encoding"
+  | T_variable _, _ -> fail @@ different_kinds a b
+
+(* No information about what made it fail *)
+let type_expression_eq ab = Trace.to_bool @@ assert_type_expression_eq ab
+
+let assert_literal_eq (a, b : literal * literal) : (unit, typer_error) result =
+  match (a, b) with
+  | Literal_int a, Literal_int b when a = b -> ok ()
+  | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
+  | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b
+  | Literal_nat a, Literal_nat b when a = b -> ok ()
+  | Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
+  | Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
+  | Literal_timestamp a, Literal_timestamp b when a = b -> ok ()
+  | Literal_timestamp _, Literal_timestamp _ -> fail @@ different_literals "different timestamps" a b
+  | Literal_timestamp _, _ -> fail @@ different_literals_because_different_types "timestamp vs non-timestamp" a b
+  | Literal_mutez a, Literal_mutez b when a = b -> ok ()
+  | Literal_mutez _, Literal_mutez _ -> fail @@ different_literals "different tezs" a b
+  | Literal_mutez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
+  | Literal_string a, Literal_string b when a = b -> ok ()
+  | Literal_string _, Literal_string _ -> fail @@ different_literals "different strings" a b
+  | Literal_string _, _ -> fail @@ different_literals_because_different_types "string vs non-string" a b
+  | Literal_bytes a, Literal_bytes b when a = b -> ok ()
+  | Literal_bytes _, Literal_bytes _ -> fail @@ different_literals "different bytes" a b
+  | Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b
+  | Literal_void, Literal_void -> ok ()
+  | Literal_void, _ -> fail @@ different_literals_because_different_types "void vs non-void" a b
+  | Literal_unit, Literal_unit -> ok ()
+  | Literal_unit, _ -> fail @@ different_literals_because_different_types "unit vs non-unit" a b
+  | Literal_address a, Literal_address b when a = b -> ok ()
+  | Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b
+  | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
+  | Literal_signature a, Literal_signature b when a = b -> ok ()
+  | Literal_signature _, Literal_signature _ -> fail @@ different_literals "different signature" a b
+  | Literal_signature _, _ -> fail @@ different_literals_because_different_types "signature vs non-signature" a b
+  | Literal_key a, Literal_key b when a = b -> ok ()
+  | Literal_key _, Literal_key _ -> fail @@ different_literals "different key" a b
+  | Literal_key _, _ -> fail @@ different_literals_because_different_types "key vs non-key" a b
+  | Literal_key_hash a, Literal_key_hash b when a = b -> ok ()
+  | Literal_key_hash _, Literal_key_hash _ -> fail @@ different_literals "different key_hash" a b
+  | Literal_key_hash _, _ -> fail @@ different_literals_because_different_types "key_hash vs non-key_hash" a b
+  | Literal_chain_id a, Literal_chain_id b when a = b -> ok ()
+  | Literal_chain_id _, Literal_chain_id _ -> fail @@ different_literals "different chain_id" a b
+  | Literal_chain_id _, _ -> fail @@ different_literals_because_different_types "chain_id vs non-chain_id" a b
+  | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
+  | Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b
+
+
+let rec assert_value_eq (a, b: (expression*expression)) : (unit, typer_error) result =
+  trace compare_tracer @@
+  match (a.expression_content, b.expression_content) with
+  | E_literal a, E_literal b ->
+      assert_literal_eq (a, b)
+  | E_constant {cons_name=ca;arguments=lsta}, E_constant {cons_name=cb;arguments=lstb} when ca = cb -> (
+      let%bind lst =
+        generic_try (corner_case "constants with different number of elements")
+          (fun () -> List.combine lsta lstb) in
+      let%bind _all = bind_list @@ List.map assert_value_eq lst in
+      ok ()
+    )
+  | E_constant _, E_constant _ ->
+      fail @@ different_values "constants" a b
+  | E_constant _, _ ->
+      fail @@ (corner_case "comparing constant with other stuff")
+
+  | E_constructor {constructor=ca;element=a}, E_constructor {constructor=cb;element=b} when ca = cb -> (
+      let%bind _eq = assert_value_eq (a, b) in
+      ok ()
+    )
+  | E_constructor _, E_constructor _ ->
+      fail @@ different_values "constructors" a b
+  | E_constructor _, _ ->
+      fail @@ different_values_because_different_types "constructor vs. non-constructor" a b
+  | E_record sma, E_record smb -> (
+      let aux (Label k) a b =
+        match a, b with
+        | Some a, Some b -> Some (assert_value_eq (a, b))
+        | _              -> Some (fail @@ missing_key_in_record_value k)
+      in
+      let%bind _all = Helpers.bind_lmap @@ LMap.merge aux sma smb in
+      ok ()
+    )
+  | E_record _, _ ->
+      fail @@ (different_values_because_different_types "record vs. non-record" a b)
+
+  | (E_literal _, _) | (E_variable _, _) | (E_application _, _)
+  | (E_lambda _, _) | (E_let_in _, _) | (E_raw_code _, _) | (E_recursive _, _)
+  | (E_record_accessor _, _) | (E_record_update _,_)
+  | (E_matching _, _)
+  -> fail @@ error_uncomparable_values "can't compare sequences nor loops" a b

src/passes/09-typing/08-typer-new/heuristic_break_ctor.ml

@@ -36,6 +36,9 @@ let propagator : output_break_ctor propagator =
 
   (* a.tv = b.tv *)
   let eq1 = c_equation { tsrc = "solver: propagator: break_ctor a" ; t = P_variable a.tv} { tsrc = "solver: propagator: break_ctor b" ; t = P_variable b.tv} "propagator: break_ctor" in
+  let () = if Ast_typed.Debug.debug_new_typer then
+           let p = Ast_typed.PP_generic.c_constructor_simpl in
+           Format.printf "\npropagator_break_ctor\na = %a\nb = %a\n%!" p a p b in
   (* a.c_tag = b.c_tag *)
   if (Solver_should_be_generated.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)"
@@ -51,4 +54,11 @@ let propagator : output_break_ctor propagator =
     let eqs = eq1 :: eqs3 in
     (eqs , []) (* no new assignments *)
 
-let heuristic = Propagator_heuristic { selector ; propagator ; comparator = Solver_should_be_generated.compare_output_break_ctor }
+let heuristic =
+  Propagator_heuristic
+    {
+      selector ;
+      propagator ;
+      printer = Ast_typed.PP_generic.output_break_ctor ; (* TODO: use an accessor that can get the printer for PP_generic or PP_json alike *)
+      comparator = Solver_should_be_generated.compare_output_break_ctor
+    }

src/passes/09-typing/08-typer-new/heuristic_specialize1.ml

@@ -48,8 +48,16 @@ let propagator : output_specialize1 propagator =
       t = P_apply { tf   = { tsrc = "solver: propagator: specialize1 tf"   ; t = P_forall a.forall            };
                     targ = { tsrc = "solver: propagator: specialize1 targ" ; t = P_variable fresh_existential }} } in
   let (reduced, new_constraints) = Typelang.check_applied @@ Typelang.type_level_eval apply in
+  (if Ast_typed.Debug.debug_new_typer then Format.printf "apply = %a\nb = %a\nreduced = %a\nnew_constraints = [\n%a\n]\n" Ast_typed.PP_generic.type_value apply Ast_typed.PP_generic.c_constructor_simpl b Ast_typed.PP_generic.type_value reduced (PP_helpers.list_sep Ast_typed.PP_generic.type_constraint (fun ppf () -> Format.fprintf ppf " ;\n")) new_constraints);
   let eq1 = c_equation { tsrc = "solver: propagator: specialize1 eq1" ; t = P_variable b.tv } reduced "propagator: specialize1" in
   let eqs = eq1 :: new_constraints in
   (eqs, []) (* no new assignments *)
 
-let heuristic = Propagator_heuristic { selector ; propagator ; comparator = Solver_should_be_generated.compare_output_specialize1 }
+let heuristic =
+  Propagator_heuristic
+    {
+      selector ;
+      propagator ;
+      printer = Ast_typed.PP_generic.output_specialize1 ;
+      comparator = Solver_should_be_generated.compare_output_specialize1
+    }

src/passes/09-typing/08-typer-new/normalizer.ml

@@ -114,7 +114,7 @@ let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer
   | C_equation {aval=({ tsrc = _ ; t = P_apply _ } as a); bval=(_ as b)}               -> reduce_type_app b a
   (* break down (TC(args)) into (TC('a, …) and ('a = arg) …) *)
   | C_typeclass { tc_args; typeclass }                              -> split_typeclass tc_args typeclass
-  | C_access_label { c_access_label_tval; accessor; c_access_label_tvar } -> let _todo = ignore (c_access_label_tval, accessor, c_access_label_tvar) in failwith "TODO" (* tv, label, result *)
+  | C_access_label { c_access_label_tval; accessor; c_access_label_tvar } -> let _todo = ignore (c_access_label_tval, accessor, c_access_label_tvar) in failwith "TODO C_access_label" (* tv, label, result *)
 
 let normalizers : type_constraint -> structured_dbs -> (structured_dbs , 'modified_constraint) state_list_monad =
   fun new_constraint dbs ->

src/passes/09-typing/08-typer-new/solver.ml

@@ -13,8 +13,8 @@ let propagator_heuristics =
     Heuristic_specialize1.heuristic ;
   ]
 
-let init_propagator_heuristic (Propagator_heuristic { selector ; propagator ; comparator }) =
-  Propagator_state { selector ; propagator ; already_selected = Set.create ~cmp:comparator }
+let init_propagator_heuristic (Propagator_heuristic { selector ; propagator ; printer ; comparator }) =
+  Propagator_state { selector ; propagator ; printer ; already_selected = Set.create ~cmp:comparator }
 
 let initial_state : typer_state = {
     structured_dbs =
@@ -45,16 +45,25 @@ let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_
      (* Call the propagation rule *)
      let (new_constraints , new_assignments) = List.split @@ List.map (propagator dbs) selected_outputs in
      (* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *)
+let () =
+  (if Ast_typed.Debug.debug_new_typer && false then
+   let s str = (fun ppf () -> Format.fprintf ppf str) in
+   Format.printf "propagator produced\nnew_constraints = %a\nnew_assignments = %a\n"
+     (PP_helpers.list_sep (PP_helpers.list_sep Ast_typed.PP_generic.type_constraint (s "\n")) (s "\n"))
+     new_constraints
+     (PP_helpers.list_sep (PP_helpers.list_sep Ast_typed.PP_generic.c_constructor_simpl (s "\n")) (s "\n"))
+     new_assignments)
+in
      (already_selected , List.flatten new_constraints , List.flatten new_assignments)
   | WasNotSelected ->
      (already_selected, [] , [])
 
-let select_and_propagate_one new_constraint (new_states , new_constraints , dbs) (Propagator_state { selector; propagator; already_selected }) =
+let select_and_propagate_one new_constraint (new_states , new_constraints , dbs) (Propagator_state { selector; propagator; printer ; already_selected }) =
   let sel_propag = (select_and_propagate selector propagator) in
   let (already_selected , new_constraints', new_assignments) = sel_propag already_selected new_constraint dbs in
   let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> Map.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in
   let dbs = { dbs with assignments } in
-  Propagator_state { selector; propagator; already_selected } :: new_states, new_constraints' @ new_constraints, dbs
+  Propagator_state { selector; propagator; printer ; already_selected } :: new_states, new_constraints' @ new_constraints, dbs
 
 (* Takes a constraint, applies all selector+propagator pairs to it.
    Keeps track of which constraints have already been selected. *)

src/passes/09-typing/08-typer-new/typer.ml

@@ -14,8 +14,7 @@ module Map = RedBlackTrees.PolyMap
 open Todo_use_fold_generator
 
 let assert_type_expression_eq ((tv',tv):O.type_expression * O.type_expression) : (unit,typer_error) result = 
-  trace_option (assert_equal tv' tv) @@
-    O.assert_type_expression_eq (tv' , tv)
+  Compare_types.assert_type_expression_eq (tv' , tv)
 
 (*
   Extract pairs of (name,type) in the declaration and add it to the environment
@@ -25,7 +24,7 @@ let rec type_declaration env state : I.declaration -> (environment * O'.typer_st
     let%bind tv = evaluate_type env type_expression in
     let env' = Environment.add_type (type_name) tv env in
     ok (env', state , None)
-  | Declaration_constant (binder , tv_opt , inline, expression) -> (
+  | Declaration_constant (binder , tv_opt , attr, expression) -> (
     (*
       Determine the type of the expression and add it to the environment
     *)
@@ -34,7 +33,7 @@ let rec type_declaration env state : I.declaration -> (environment * O'.typer_st
         trace (constant_declaration_tracer binder expression tv'_opt) @@
         type_expression env state expression in
       let post_env = Environment.add_ez_declaration binder expr env in
-      ok (post_env, state' , Some (O.Declaration_constant { binder ; expr ; inline} ))
+      ok (post_env, state' , Some (O.Declaration_constant { binder ; expr ; inline=attr.inline} ))
     )
 
 and type_match : environment -> O'.typer_state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * O'.typer_state, typer_error) result =
@@ -67,8 +66,8 @@ and type_match : environment -> O'.typer_state -> O.type_expression -> I.matchin
           let%bind acc = match acc with
             | None -> ok (Some variant)
             | Some variant' ->
-                let%bind () = trace_option (not_matching variant variant') @@
-                  Ast_typed.assert_type_expression_eq (variant , variant') in
+                let%bind () =
+                  assert_type_expression_eq (variant , variant') in
                 ok (Some variant)
             in
           ok acc in
@@ -112,7 +111,7 @@ and type_match : environment -> O'.typer_state -> O.type_expression -> I.matchin
 *)
 and evaluate_type (e:environment) (t:I.type_expression) : (O.type_expression, typer_error) result =
   let return tv' = ok (make_t ~loc:t.location tv' (Some t)) in
-  match t.type_content with
+  match t.content with
   | T_arrow {type1;type2} ->
     let%bind type1 = evaluate_type e type1 in
     let%bind type2 = evaluate_type e type2 in
@@ -211,7 +210,7 @@ and type_expression : environment -> O'.typer_state -> ?tv_opt:O.type_expression
     ok @@ (expr' , new_state) in
   let return_wrapped expr state (constraints , expr_type) = return expr state constraints expr_type in
   trace (expression_tracer ae) @@
-  match ae.expression_content with
+  match ae.content with
 
   (* TODO: this file should take care only of the order in which program fragments
      are translated by Wrap.xyz
@@ -440,19 +439,36 @@ let type_program_returns_state ((env, state, p) : environment * O'.typer_state *
   let declarations = List.rev declarations in (* Common hack to have O(1) append: prepend and then reverse *)
   ok (env', state', declarations)
 
+let print_env_state_node (node_printer : Format.formatter -> 'a -> unit) ((env,state,node) : environment * O'.typer_state * 'a) =
+  ignore node; (* TODO *)
+  Printf.printf "%s" @@
+    Format.asprintf "{ \"ENV\": %a,\n\"STATE\": %a,\n\"NODE\": %a\n},\n"
+      Ast_typed.PP_json.environment env
+      Typesystem.Solver_types.json_typer_state state
+      node_printer node
+
 let type_and_subst_xyz
-  (env_state_node : environment * O'.typer_state * 'a) (apply_substs : ('b, Typer_common.Errors.typer_error) Typesystem.Misc.Substitution.Pattern.w)
-  (type_xyz_returns_state : (environment * O'.typer_state * 'a) -> (environment * O'.typer_state * 'b, typer_error) Trace.result) : ('b * O'.typer_state, typer_error) result =
+      (in_printer : Format.formatter -> 'a -> unit)
+      (out_printer : Format.formatter -> 'b -> unit)
+      (env_state_node : environment * O'.typer_state * 'a)
+      (apply_substs : ('b , Typer_common.Errors.typer_error) Typesystem.Misc.Substitution.Pattern.w)
+      (type_xyz_returns_state : (environment * O'.typer_state * 'a) -> (environment * O'.typer_state * 'b , typer_error) Trace.result)
+    : ('b * O'.typer_state , typer_error) result =
+  let () = (if Ast_typed.Debug.json_new_typer then Printf.printf "%!\n###############################START_OF_JSON\n[%!") in
+  let () = (if Ast_typed.Debug.debug_new_typer then Printf.printf "\nTODO AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA Print env_state_node here.\n\n") in
+  let () = (if Ast_typed.Debug.debug_new_typer || Ast_typed.Debug.json_new_typer then print_env_state_node in_printer env_state_node) in
   let%bind (env, state, node) = type_xyz_returns_state env_state_node in
   let subst_all =
     let aliases = state.structured_dbs.aliases in
     let assignments = state.structured_dbs.assignments in
     let substs : variable: I.type_variable -> _ = fun ~variable ->
       to_option @@
+      let () = (if Ast_typed.Debug.debug_new_typer then Printf.fprintf stderr "%s" @@ Format.asprintf "TRY   %a\n" Var.pp variable) in
       let%bind root =
         trace_option (corner_case (Format.asprintf "can't find alias root of variable %a" Var.pp variable)) @@
           (* TODO: after upgrading UnionFind, this will be an option, not an exception. *)
           try Some (Solver.UF.repr variable aliases) with Not_found -> None in
+      let () = (if Ast_typed.Debug.debug_new_typer then Printf.fprintf stderr "%s" @@ Format.asprintf "TRYR  %a (%a)\n" Var.pp variable Var.pp root) in
       let%bind assignment =
         trace_option (corner_case (Format.asprintf "can't find assignment for root %a" Var.pp root)) @@
           (Map.find_opt root assignments) in
@@ -460,18 +476,22 @@ let type_and_subst_xyz
       let () = ignore tv (* I think there is an issue where the tv is stored twice (as a key and in the element itself) *) in
       let%bind (expr : O.type_content) = trace_option (corner_case "wrong constant tag") @@
         Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.t_variable s ()) tv_list)) in
+      let () = (if Ast_typed.Debug.debug_new_typer then Printf.fprintf stderr "%s" @@ Format.asprintf "SUBST %a (%a is %a)\n" Var.pp variable Var.pp root Ast_typed.PP_generic.type_content expr) in
       ok @@ expr
     in
     let p = apply_substs ~substs node in
     p in
   let%bind node = subst_all in
+  let () = (if Ast_typed.Debug.debug_new_typer then Printf.printf "\nTODO AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA Print env,state,node here again.\n\n") in
+  let () = (if Ast_typed.Debug.debug_new_typer || Ast_typed.Debug.json_new_typer then print_env_state_node out_printer (env, state, node)) in
+  let () = (if Ast_typed.Debug.json_new_typer then Printf.printf "%!\"end of JSON\"],\n###############################END_OF_JSON\n%!") in
   let () = ignore env in        (* TODO: shouldn't we use the `env` somewhere? *)
   ok (node, state)
 
 let type_program (p : I.program) : (O.program * O'.typer_state, typer_error) result =
   let empty_env = DEnv.default in
   let empty_state = Solver.initial_state in
-  type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state
+  type_and_subst_xyz (fun ppf _v -> Format.fprintf ppf "\"no JSON yet for I.PP.program\"") Ast_typed.PP_json.program (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state
 
 let type_expression_returns_state : (environment * O'.typer_state * I.expression) -> (environment * O'.typer_state * O.expression, typer_error) result =
   fun (env, state, e) ->
@@ -480,7 +500,7 @@ let type_expression_returns_state : (environment * O'.typer_state * I.expression
 
 let type_expression_subst (env : environment) (state : O'.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O'.typer_state , typer_error) result =
   let () = ignore tv_opt in     (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *)
-  type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state
+  type_and_subst_xyz (fun ppf _v -> Format.fprintf ppf "\"no JSON yet for I.PP.expression\"") Ast_typed.PP_json.expression (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state
 
 let untype_type_expression  = Untyper.untype_type_expression
 let untype_expression       = Untyper.untype_expression
@@ -493,7 +513,7 @@ and [@warning "-32"] type_expression : environment -> O'.typer_state -> ?tv_opt:
 and [@warning "-32"] type_lambda e state lam = type_lambda e state lam
 and [@warning "-32"] type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression, typer_error) result = type_constant name lst tv_opt
 let [@warning "-32"] type_program_returns_state ((env, state, p) : environment * O'.typer_state * I.program) : (environment * O'.typer_state * O.program, typer_error) result = type_program_returns_state (env, state, p)
-let [@warning "-32"] type_and_subst_xyz (env_state_node : environment * O'.typer_state * 'a) (apply_substs : ('b,typer_error) Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O'.typer_state * 'a) -> (environment * O'.typer_state * 'b, typer_error) result) : ('b * O'.typer_state, typer_error) result = type_and_subst_xyz env_state_node apply_substs type_xyz_returns_state
+let [@warning "-32"] type_and_subst_xyz (in_printer : (Format.formatter -> 'a -> unit)) (out_printer : (Format.formatter -> 'b -> unit)) (env_state_node : environment * O'.typer_state * 'a) (apply_substs : ('b,typer_error) Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O'.typer_state * 'a) -> (environment * O'.typer_state * 'b, typer_error) result) : ('b * O'.typer_state, typer_error) result = type_and_subst_xyz in_printer out_printer env_state_node apply_substs type_xyz_returns_state
 let [@warning "-32"] type_program (p : I.program) : (O.program * O'.typer_state, typer_error) result = type_program p
 let [@warning "-32"] type_expression_returns_state : (environment * O'.typer_state * I.expression) -> (environment * O'.typer_state * O.expression, typer_error) Trace.result = type_expression_returns_state
 let [@warning "-32"] type_expression_subst (env : environment) (state : O'.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O'.typer_state, typer_error) result = type_expression_subst env state ?tv_opt e

src/passes/09-typing/08-typer-new/wrap.ml

@@ -62,7 +62,7 @@ let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun
      p_constant csttag (List.map type_expression_to_type_value args)
 
 let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_value = fun te ->
-  match te.type_content with
+  match te.content with
   | T_sum kvmap ->
      let () = failwith "fixme: don't use to_list, it drops the variant keys, rows have a differnt kind than argument lists for now!" in
      let tlist = List.map (fun ({ctor_type;_}:I.ctor_content) -> ctor_type) (I.CMap.to_list kvmap) in

src/passes/09-typing/08-typer-old/typer.ml

@@ -290,13 +290,13 @@ and type_declaration env (_placeholder_for_state_of_new_typer : O'.typer_state)
       let%bind tv = evaluate_type env type_expr in
       let env' = Environment.add_type (type_binder) tv env in
       ok (env', (Solver.placeholder_for_state_of_new_typer ()) , (O.Declaration_type { type_binder ; type_expr = tv } ))
-  | Declaration_constant (binder , tv_opt , inline, expression) -> (
+  | Declaration_constant (binder , tv_opt , attr, expression) -> (
       let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
       let%bind expr =
         trace (constant_declaration_error_tracer binder expression tv'_opt) @@
         type_expression' ?tv_opt:tv'_opt env expression in
       let post_env = Environment.add_ez_declaration binder expr env in
-      ok (post_env, (Solver.placeholder_for_state_of_new_typer ()) , (O.Declaration_constant { binder ; expr ; inline}))
+      ok (post_env, (Solver.placeholder_for_state_of_new_typer ()) , (O.Declaration_constant { binder ; expr ; inline=attr.inline}))
     )
 
 and type_match : (environment -> I.expression -> (O.expression , typer_error) result) -> environment -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr, typer_error) result =
@@ -349,7 +349,7 @@ and type_match : (environment -> I.expression -> (O.expression , typer_error) re
 
 and evaluate_type (e:environment) (t:I.type_expression) : (O.type_expression, typer_error) result =
   let return tv' = ok (make_t ~loc:t.location tv' (Some t)) in
-  match t.type_content with
+  match t.content with
   | T_arrow {type1;type2} ->
       let%bind type1 = evaluate_type e type1 in
       let%bind type2 = evaluate_type e type2 in
@@ -456,7 +456,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
     let location = ae.location in
     ok @@ make_e ~location expr tv in
   trace (expression_tracer ae) @@
-  match ae.expression_content with
+  match ae.content with
   (* Basic *)
   | E_variable name ->
       let%bind tv' =
@@ -561,7 +561,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
    return (E_lambda lambda ) lambda_type
   | E_constant {cons_name=( C_LIST_FOLD | C_MAP_FOLD | C_SET_FOLD) as opname ;
                 arguments=[
-                    ( { expression_content = (I.E_lambda { binder = lname ;
+                    ( { content = (I.E_lambda { binder = lname ;
                                                    input_type = None ; 
                                                    output_type = None ; 
                                                    result }) ;
@@ -589,7 +589,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
       return (E_constant {cons_name=opname';arguments=lst'}) tv
   | E_constant {cons_name=C_FOLD_WHILE as opname;
                 arguments = [
-                    ( { expression_content = (I.E_lambda { binder = lname ;
+                    ( { content = (I.E_lambda { binder = lname ;
                                                    input_type = None ; 
                                                    output_type = None ; 
                                                    result }) ;
@@ -701,7 +701,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
     return (E_let_in {let_binder; rhs; let_result; inline}) let_result.type_expression
   | E_raw_code {language;code} ->
     let%bind (code,type_expression) = trace_option (expected_ascription code) @@
-      I.get_e_ascription code.expression_content in
+      I.get_e_ascription code.content in
     let%bind code = type_expression' e code in
     let%bind type_expression = evaluate_type e type_expression in
     let code = {code with type_expression} in
@@ -740,9 +740,9 @@ and type_lambda e {
           match input_type with
           | Some ty -> ok ty
           | None -> (
-              match result.expression_content with
+              match result.content with
               | I.E_let_in li -> (
-                  match li.rhs.expression_content with
+                  match li.rhs.content with
                   | I.E_variable name when name = (binder) -> (
                       match snd li.let_binder with
                       | Some ty -> ok ty
@@ -849,7 +849,7 @@ let rec untype_expression (e:O.expression) : (I.expression , typer_error) result
   | E_recursive {fun_name;fun_type; lambda} ->
       let%bind fun_type = untype_type_expression fun_type in
       let%bind unty_expr= untype_expression_content ty @@ E_lambda lambda in
-      let lambda = match unty_expr.expression_content with I.E_lambda l -> l | _ -> failwith "impossible case" in
+      let lambda = match unty_expr.content with I.E_lambda l -> l | _ -> failwith "impossible case" in
       return @@ e_recursive fun_name fun_type lambda
 
 and untype_matching : (O.expression -> (I.expression , typer_error) result) -> O.matching_expr -> (I.matching_expr , typer_error) result = fun f m ->

src/passes/10-self_ast_typed/helpers.ml

@@ -256,7 +256,7 @@ type contract_type = {
 let fetch_contract_type : string -> program -> (contract_type, self_ast_typed_error) result = fun main_fname program ->
   let aux declt = match Location.unwrap declt with
     | Declaration_constant ({ binder ; expr=_ ; inline=_ } as p) ->
-       if String.equal (Var.to_name binder) main_fname
+       if Var.equal binder @@ Var.of_name main_fname
        then Some p
        else None
     | Declaration_type _ -> None

src/passes/predefined/predefined.ml

@@ -47,6 +47,23 @@ module Tree_abstraction = struct
     | "timestamp" -> Some TC_timestamp
     | _           -> None
 
+  let type_constant_to_string tc = 
+    match tc with
+      TC_chain_id  -> "chain_id"  
+    | TC_unit      -> "unit"      
+    | TC_string    -> "string"    
+    | TC_bytes     -> "bytes"     
+    | TC_nat       -> "nat"       
+    | TC_int       -> "int"       
+    | TC_mutez     -> "tez"       
+    | TC_operation -> "operation" 
+    | TC_address   -> "address"   
+    | TC_key       -> "key"       
+    | TC_key_hash  -> "key_hash"  
+    | TC_signature -> "signature" 
+    | TC_timestamp -> "timestamp" 
+    | TC_void      -> "void"
+
   let type_operators s =
     match s with
       "list"                      -> Some (TC_list)
@@ -61,6 +78,23 @@ module Tree_abstraction = struct
     | "michelson_or_left_comb"    -> Some (TC_michelson_or_left_comb)
     | _                           -> None
 
+  let type_operator_to_string s =
+    match s with
+      TC_list -> "list"                      
+    | TC_option -> "option"                    
+    | TC_set -> "set"                       
+    | TC_map -> "map"                       
+    | TC_big_map -> "big_map"                   
+    | TC_contract -> "contract"                  
+    | TC_michelson_pair -> "michelson_pair"
+    | TC_michelson_or -> "michelson_or"
+    | TC_michelson_pair_right_comb -> "michelson_pair_right_comb" 
+    | TC_michelson_pair_left_comb -> "michelson_pair_left_comb"  
+    | TC_michelson_or_right_comb -> "michelson_or_right_comb"   
+    | TC_michelson_or_left_comb -> "michelson_or_left_comb"    
+    | TC_map_or_big_map -> "map_or_big_map"
+    
+
   let pseudo_modules = function
     | "Tezos.chain_id"           -> Some C_CHAIN_ID
     | "Tezos.balance"            -> Some C_BALANCE
@@ -165,6 +199,113 @@ module Tree_abstraction = struct
     | _ -> None
 
 
+  let pseudo_module_to_string = function
+    | C_CHAIN_ID                -> "Tezos.chain_id"
+    | C_BALANCE                 -> "Tezos.balance"
+    | C_NOW                     -> "Tezos.now"
+    | C_AMOUNT                  -> "Tezos.amount"
+    | C_SENDER                  -> "Tezos.sender"
+    | C_ADDRESS                 -> "Tezos.address"
+    | C_SELF                    -> "Tezos.self"
+    | C_SELF_ADDRESS            -> "Tezos.self_address"
+    | C_IMPLICIT_ACCOUNT        -> "Tezos.implicit_account"
+    | C_SOURCE                  -> "Tezos.source"
+    | C_FAILWITH                -> "Tezos.failwith"
+    | C_CREATE_CONTRACT         -> "Tezos.create_contract"
+    | C_CALL                    -> "Tezos.transaction"
+    | C_SET_DELEGATE            -> "Tezos.set_delegate"
+    | C_CONTRACT_OPT            -> "Tezos.get_contract_opt"
+    | C_CONTRACT_ENTRYPOINT_OPT -> "Tezos.get_entrypoint_opt"
+    | C_CONTRACT                -> "Tezos.get_contract"
+    | C_CONTRACT_ENTRYPOINT     -> "Tezos.get_entrypoint"
+
+    (* Crypto module *)
+
+    | C_CHECK_SIGNATURE -> "Crypto.check"
+    | C_HASH_KEY        -> "Crypto.hash_key"
+    | C_BLAKE2b         -> "Crypto.blake2b"
+    | C_SHA256          -> "Crypto.sha256"
+    | C_SHA512          -> "Crypto.sha512"
+    
+    (* Bytes module *)
+
+    | C_BYTES_PACK   -> "Bytes.pack"
+    | C_BYTES_UNPACK -> "Bytes.unpack"
+    | C_SIZE         -> "Bytes.length"
+    | C_CONCAT       -> "Bytes.concat"
+    | C_SLICE        -> "Bytes.sub"
+
+    (* List module *)   
+
+  (*  | C_SIZE      -> "List.size" *)
+    | C_LIST_ITER -> "List.iter"
+    | C_LIST_MAP  -> "List.map"
+    | C_LIST_FOLD -> "List.fold"
+
+    (* Set module *)   
+
+    | C_SET_EMPTY   -> "Set.empty"
+    | C_SET_LITERAL -> "Set.literal"
+   (* | C_SIZE        -> "Set.cardinal"*)
+    | C_SET_MEM     -> "Set.mem"
+    | C_SET_ADD     -> "Set.add"
+    | C_SET_REMOVE  -> "Set.remove"
+    | C_SET_ITER    -> "Set.iter"
+    | C_SET_FOLD    -> "Set.fold"
+
+    (* Map module *)   
+
+    | C_MAP_FIND_OPT -> "Map.find_opt"
+    | C_MAP_UPDATE   -> "Map.update"
+    | C_MAP_ITER     -> "Map.iter"
+    | C_MAP_MAP      -> "Map.map"
+    | C_MAP_FOLD     -> "Map.fold"
+    | C_MAP_MEM      -> "Map.mem"
+  (*  | C_SIZE         -> "Map.size" *)
+    | C_MAP_ADD      -> "Map.add"
+    | C_MAP_REMOVE   -> "Map.remove"
+    | C_MAP_EMPTY    -> "Map.empty"
+    | C_MAP_LITERAL  -> "Map.literal"
+    
+    (* Big_map module *)   
+    
+    | C_MAP_FIND        -> "Big_map.find"
+  (*  | C_MAP_FIND_OPT    -> "Big_map.find_opt"
+    | C_MAP_UPDATE      -> "Big_map.update" *)
+    | C_BIG_MAP_LITERAL -> "Big_map.literal"
+    | C_BIG_MAP_EMPTY   -> "Big_map.empty"
+  (*  | C_MAP_MEM         -> "Big_map.mem"
+    | C_MAP_REMOVE      -> "Big_map.remove"
+    | C_MAP_ADD         -> "Big_map.add" *)
+
+    (* Bitwise module *)
+
+    | C_OR  -> "Bitwise.or"
+    | C_AND -> "Bitwise.and"
+    | C_XOR -> "Bitwise.xor"
+    | C_LSL -> "Bitwise.shift_left"
+    | C_LSR -> "Bitwise.shift_right"
+
+    (* String module *)
+
+  (*  | C_SIZE   -> "String.length" (* will never trigger, rename size *)
+    | C_SLICE  -> "String.sub"
+    | C_CONCAT -> "String.concat" *)
+
+    (* michelson pair/or type converter module *)
+
+    | C_CONVERT_TO_RIGHT_COMB   -> "Layout.convert_to_right_comb"
+    | C_CONVERT_TO_LEFT_COMB    -> "Layout.convert_to_left_comb"
+    | C_CONVERT_FROM_RIGHT_COMB -> "Layout.convert_from_right_comb"
+    | C_CONVERT_FROM_LEFT_COMB  -> "Layout.convert_from_left_comb"
+
+    (* Not parsed *)
+    | C_SOME -> "Some"
+    | C_NONE -> "None"
+
+    | _ as c -> failwith @@ Format.asprintf "Constant not handled : %a" Stage_common.PP.constant c 
+
+
   module Pascaligo = struct
     let constants = function
     (* Tezos module (ex-Michelson) *)
@@ -283,8 +424,46 @@ module Tree_abstraction = struct
 
     | _ as c            -> pseudo_modules c
 
+    let constant_to_string = function
+    (* Tezos module (ex-Michelson) *)
+    | C_FAILWITH -> "failwith"
+
+    | C_IS_NAT -> "is_nat"
+    | C_INT    -> "int"
+    | C_ABS    -> "abs"
+    | C_EDIV   -> "ediv"
+    | C_UNIT   -> "unit"
+
+    | C_NEG  -> "NEG"
+    | C_ADD  -> "ADD"
+    | C_SUB  -> "SUB"
+    | C_MUL  -> "TIMES"
+    | C_DIV  -> "DIV"
+    | C_MOD  -> "MOD"
+    | C_EQ   -> "EQ"
+    | C_NOT  -> "NOT"
+    | C_AND  -> "AND"
+    | C_OR   -> "OR"
+    | C_GT   -> "GT"
+    | C_GE   -> "GE"
+    | C_LT   -> "LT"
+    | C_LE   -> "LE"
+    | C_CONS -> "CONS"
+    | C_NEQ  -> "NEQ"
+
+    (*->  Others *)
+
+    | C_ASSERTION -> "assert"
+    
+    | C_CONVERT_TO_RIGHT_COMB -> "Layout.convert_to_right_comb"
+    | C_CONVERT_TO_LEFT_COMB  -> "Layout.convert_to_left_comb"
+
+    | _ as c            -> pseudo_module_to_string c
+
     let type_constants = type_constants
     let type_operators = type_operators
+    let type_constant_to_string = type_constant_to_string
+    let type_operator_to_string = type_operator_to_string
   end
 
   module Cameligo = struct
@@ -370,8 +549,43 @@ module Tree_abstraction = struct
 
     | _ as c -> pseudo_modules c
 
+    let constant_to_string = function
+    (* Tezos (ex-Michelson, ex-Current, ex-Operation) *)
+    | C_FAILWITH -> "failwith"
+    
+    | C_IS_NAT -> "is_nat"
+    | C_INT    -> "int"
+    | C_ABS    -> "abs"
+    | C_EDIV   -> "ediv"
+    | C_UNIT   -> "unit"
+
+    | C_NEG  -> "NEG"
+    | C_ADD  -> "ADD"
+    | C_SUB  -> "SUB"
+    | C_MUL  -> "TIMES"
+    | C_DIV  -> "DIV"
+    | C_MOD  -> "MOD"
+    | C_EQ   -> "EQ"
+    | C_NOT  -> "NOT"
+    | C_AND  -> "AND"
+    | C_OR   -> "OR"
+    | C_GT   -> "GT"
+    | C_GE   -> "GE"
+    | C_LT   -> "LT"
+    | C_LE   -> "LE"
+    | C_CONS -> "CONS"
+    | C_NEQ  -> "NEQ"
+
+    (* Others *)
+
+    | C_ASSERTION -> "assert"
+
+    | _ as c -> pseudo_module_to_string c
+
     let type_constants = type_constants
     let type_operators = type_operators
+    let type_constant_to_string = type_constant_to_string
+    let type_operator_to_string = type_operator_to_string
   end
 end
 

src/passes/predefined/predefined.mli

@@ -6,12 +6,18 @@ module Tree_abstraction : sig
     val constants      : string -> constant' option
     val type_constants : string -> type_constant option
     val type_operators : string -> type_operator option
+    val constant_to_string      : constant'     -> string
+    val type_constant_to_string : type_constant -> string
+    val type_operator_to_string : type_operator -> string
   end
 
   module Cameligo : sig
     val constants  : string -> constant' option
     val type_constants : string -> type_constant option
     val type_operators : string -> type_operator option
+    val constant_to_string      : constant'     -> string
+    val type_constant_to_string : type_constant -> string
+    val type_operator_to_string : type_operator -> string
   end
 
 end

src/stages/1-cst/cameligo/CST.ml

@@ -256,13 +256,13 @@ and expr =
 and annot_expr = expr * colon * type_expr
 
 and 'a injection = {
-  compound   : compound;
+  compound   : compound option;
   elements   : ('a, semi) sepseq;
   terminator : semi option
 }
 
 and 'a ne_injection = {
-  compound    : compound;
+  compound    : compound option;
   ne_elements : ('a, semi) nsepseq;
   terminator  : semi option
 }
@@ -400,8 +400,7 @@ and cond_expr = {
   test     : expr;
   kwd_then : kwd_then;
   ifso     : expr;
-  kwd_else : kwd_else;
-  ifnot    : expr
+  ifnot    : (kwd_else * expr) option;
 }
 
 (* Code injection.  Note how the field [language] wraps a region in

src/stages/1-cst/cameligo/ParserLog.ml

@@ -63,6 +63,11 @@ let print_sepseq :
         None -> ()
   | Some seq -> print_nsepseq state sep print seq
 
+let print_option : state -> (state -> 'a -> unit ) -> 'a option -> unit =
+  fun state print -> function
+    None -> ()
+  | Some opt -> print state opt
+
 let print_csv state print {value; _} =
   print_nsepseq state "," print value
 
@@ -74,7 +79,7 @@ let print_token state region lexeme =
 let print_var state {region; value} =
   let line =
     sprintf "%s: Ident %s\n"
-            (compact state region) value
+            (compact state region)value
   in Buffer.add_string state#buffer line
 
 let print_constr state {region; value} =
@@ -244,14 +249,18 @@ and print_ne_injection :
     print_close_compound state compound
 
 and print_open_compound state = function
+  None -> ()
+| Some compound -> match compound with
     BeginEnd (kwd_begin,_) -> print_token state kwd_begin "begin"
-| Braces   (lbrace,_)    -> print_token state lbrace    "{"
-| Brackets (lbracket,_)  -> print_token state lbracket  "["
+  | Braces   (lbrace,_)    -> print_token state lbrace    "{"
+  | Brackets (lbracket,_)  -> print_token state lbracket  "["
 
 and print_close_compound state = function
+  None -> ()
+| Some compound -> match compound with
     BeginEnd (_,kwd_end)  -> print_token state kwd_end  "end"
-| Braces   (_,rbrace)   -> print_token state rbrace   "}"
-| Brackets (_,rbracket) -> print_token state rbracket "]"
+  | Braces   (_,rbrace)   -> print_token state rbrace   "}"
+  | Brackets (_,rbracket) -> print_token state rbracket "]"
 
 and print_terminator state = function
   Some semi -> print_token state semi ";"
@@ -584,14 +593,17 @@ and print_fun_expr state {value; _} =
 
 and print_conditional state {value; _} =
   let {kwd_if; test; kwd_then;
-       ifso; kwd_else; ifnot} = value in
+       ifso; ifnot} = value in
   print_token state ghost "(";
   print_token state kwd_if "if";
   print_expr  state test;
   print_token state kwd_then "then";
   print_expr  state ifso;
+  print_option state 
+    (fun state (kwd_else,ifnot) -> 
       print_token state kwd_else "else";
       print_expr state ifnot;
+    ) ifnot;
   print_token state ghost ")"
 
 (* Conversion to string *)
@@ -1114,10 +1126,12 @@ and pp_cond_expr state (cond: cond_expr) =
     let state = state#pad 3 1 in
     pp_node state "<true>";
     pp_expr (state#pad 1 0) cond.ifso in
-  let () =
+  let () = match cond.ifnot with
+    Some (_, ifnot) ->
     let state = state#pad 3 2 in
     pp_node state "<false>";
-    pp_expr (state#pad 1 0) cond.ifnot
+    pp_expr (state#pad 1 0) ifnot
+  | None -> ()
   in ()
 
 and pp_case :

src/stages/1-cst/pascaligo/CST.ml

@@ -224,12 +224,17 @@ and fun_decl = {
   param         : parameters;
   ret_type      : (colon * type_expr) option;
   kwd_is        : kwd_is;
-  block_with    : (block reg * kwd_with) option;
   return        : expr;
   terminator    : semi option;
   attributes    : attr_decl option
 }
 
+and block_with = {
+  block    : block reg;
+  kwd_with : kwd_with;
+  expr     : expr
+}
+
 and parameters = (param_decl, semi) nsepseq par reg
 
 and param_decl =
@@ -387,15 +392,13 @@ and 'a case_clause = {
 and assignment = {
   lhs    : lhs;
   assign : assign;
-  rhs    : rhs
+  rhs    : expr;
 }
 
 and lhs =
   Path    of path
 | MapPath of map_lookup reg
 
-and rhs = expr
-
 and loop =
   While of while_loop reg
 | For   of for_loop
@@ -470,6 +473,7 @@ and expr =
 | EPar     of expr par reg
 | EFun     of fun_expr reg
 | ECodeInj of code_inj reg
+| EBlock   of block_with reg
 
 and annot_expr = expr * colon * type_expr
 
@@ -696,7 +700,8 @@ let rec expr_to_region = function
 | ECond    {region; _}
 | EPar     {region; _}
 | EFun     {region; _}
-| ECodeInj {region; _} -> region
+| ECodeInj {region; _}
+| EBlock   {region; _} -> region
 
 and tuple_expr_to_region {region; _} = region
 
@@ -814,8 +819,6 @@ let lhs_to_region : lhs -> Region.t = function
   Path path -> path_to_region path
 | MapPath {region; _} -> region
 
-let rhs_to_region = expr_to_region
-
 let selection_to_region = function
   FieldName {region; _}
 | Component {region; _} -> region

src/stages/1-cst/pascaligo/ParserLog.ml

@@ -218,18 +218,13 @@ and print_type_tuple state {value; _} =
 
 and print_fun_decl state {value; _} =
   let {kwd_function; fun_name; param;
-       ret_type; kwd_is; block_with;
+       ret_type; kwd_is;
        return; terminator; _} = value in
   print_token      state kwd_function "function";
   print_var        state fun_name;
   print_parameters state param;
   print_option     state print_type_annot ret_type;
   print_token      state kwd_is "is";
-  (match block_with with
-    None -> ()
-  | Some (block, kwd_with) ->
-     print_block state block;
-     print_token state kwd_with "with");
   print_expr state return;
   print_terminator state terminator;
 
@@ -252,6 +247,12 @@ and print_code_inj state {value; _} =
   print_expr   state code;
   print_token  state rbracket "]"
 
+and print_block_expr state {value; _} =
+  let {block;kwd_with;expr} = value in
+  print_block state block;
+  print_token state kwd_with "with";
+  print_expr  state expr;
+
 and print_parameters state {value; _} =
   let {lpar; inside; rpar} = value in
   print_token   state lpar "(";
@@ -475,6 +476,7 @@ and print_expr state = function
 | EPar     e -> print_par_expr state e
 | EFun     e -> print_fun_expr state e
 | ECodeInj e -> print_code_inj state e
+| EBlock   e -> print_block_expr state e
 
 and print_annot_expr state node =
   let {inside; _} : annot_expr par = node in
@@ -919,8 +921,7 @@ and pp_attr_decl state = pp_ne_injection pp_string state
 and pp_fun_decl state decl =
   let kwd_recursive = if decl.kwd_recursive = None then 0 else 1 in
   let ret_type = if decl.ret_type = None then 0 else 1 in
-  let block_with = if decl.block_with = None then 0 else 1 in
-  let arity = kwd_recursive + ret_type + block_with + 3 in
+  let arity = kwd_recursive + ret_type + 3 in
   let index = 0 in
   let index =
     match decl.kwd_recursive with
@@ -945,15 +946,6 @@ and pp_fun_decl state decl =
        pp_node state "<return type>";
        pp_type_expr (state#pad 1 0) t_expr;
        index+1 in
-  let index =
-    match decl.block_with with
-      None -> index
-    | Some (block,_) ->
-        let statements = block.value.statements in
-        let state = state#pad arity index in
-        pp_node state "<body>";
-        pp_statements state statements;
-        index+1 in
   let () =
     let state = state#pad arity index in
     pp_node state "<return>";
@@ -1051,15 +1043,27 @@ and pp_fun_expr state (expr: fun_expr) =
     pp_expr (state#pad 1 0) expr.return
   in ()
 
-and pp_code_inj state rc =
+and pp_code_inj state node =
   let () =
     let state = state#pad 2 0 in
     pp_node state "<language>";
-    pp_string (state#pad 1 0) rc.language.value in
+    pp_string (state#pad 1 0) node.language.value in
   let () =
     let state = state#pad 2 1 in
     pp_node state "<code>";
-    pp_expr (state#pad 1 0) rc.code
+    pp_expr (state#pad 1 0) node.code
+  in ()
+
+and pp_block_expr state node =
+  let {block; expr; _} : block_with = node in
+  let () =
+    let state = state#pad 2 0 in
+    pp_node state "<block>";
+    pp_statements state block.value.statements in
+  let () =
+    let state = state#pad 2 1 in
+    pp_node state "<expr>";
+    pp_expr (state#pad 1 0) expr
   in ()
 
 and pp_parameters state {value; _} =
@@ -1548,6 +1552,9 @@ and pp_expr state = function
 | ECodeInj {value; region} ->
     pp_loc_node state "ECodeInj" region;
     pp_code_inj state value;
+| EBlock {value; region} ->
+    pp_loc_node state "EBlock" region;
+    pp_block_expr state value;
 
 and pp_list_expr state = function
   ECons {value; region} ->

src/stages/1-cst/pascaligo/ParserLog.mli

@@ -19,6 +19,7 @@ val print_path        : state -> CST.path -> unit
 val print_pattern     : state -> CST.pattern -> unit
 val print_instruction : state -> CST.instruction -> unit
 val print_expr        : state -> CST.expr -> unit
+val print_statements  : state -> CST.statements -> unit
 
 (** {1 Printing tokens from the CST in a string} *)
 

src/stages/2-ast_imperative/PP.ml

@@ -71,7 +71,7 @@ let rec expression ppf (e : expression) =
 and expression_content ppf (ec : expression_content) =
   match ec with
   | E_literal l ->
-      literal ppf l
+      fprintf ppf "%a" literal l
   | E_variable n ->
       fprintf ppf "%a" expression_variable n
   | E_application {lamb;args} ->

src/stages/4-ast_core/PP.ml

@@ -2,16 +2,96 @@
 open Types
 open Format
 open PP_helpers
-
+module Helpers = Stage_common.Helpers
 include Stage_common.PP
-include Ast_PP_type(Ast_core_parameter)
+
+
+  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, {ctor_type;_}) = fprintf ppf "@[<h>%a -> %a@]" constructor k value ctor_type in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+  let cmap_sep_d x = cmap_sep x (tag " ,@ ")
+
+  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
+    let new_pp ppf (k, {field_type;_}) = fprintf ppf "@[<h>%a -> %a@]" label k value field_type in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+
+  let tuple_sep value sep ppf m =
+    assert (Helpers.is_tuple_lmap m);
+    let lst = Helpers.tuple_of_record m in
+    let new_pp ppf (_, {field_type;_}) = fprintf ppf "%a" value field_type in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+
+  let record_sep_expr 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, v) = fprintf ppf "@[<h>%a -> %a@]" label k value v in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+
+  let tuple_sep_expr value sep ppf m =
+    assert (Helpers.is_tuple_lmap m);
+    let lst = Helpers.tuple_of_record m in
+    let new_pp ppf (_,v) = fprintf ppf "%a" value v in
+    fprintf ppf "%a" (list_sep new_pp sep) lst
+
+(* Prints records which only contain the consecutive fields
+  0..(cardinal-1) as tuples *)
+let tuple_or_record_sep_t value format_record sep_record format_tuple sep_tuple ppf m =
+  if Helpers.is_tuple_lmap m then
+    fprintf ppf format_tuple (tuple_sep value (tag sep_tuple)) m
+  else
+    fprintf ppf format_record (record_sep value (tag sep_record)) m
+
+let tuple_or_record_sep_expr value format_record sep_record format_tuple sep_tuple ppf m =
+  if Helpers.is_tuple_lmap m then
+    fprintf ppf format_tuple (tuple_sep_expr value (tag sep_tuple)) m
+  else
+    fprintf ppf format_record (record_sep_expr value (tag sep_record)) m
+
+let tuple_or_record_sep_expr value = tuple_or_record_sep_expr value "@[<hv 7>record[%a]@]" " ,@ " "@[<hv 2>( %a )@]" " ,@ "
+let tuple_or_record_sep_type value = tuple_or_record_sep_t value "@[<hv 7>record[%a]@]" " ,@ " "@[<hv 2>( %a )@]" " *@ "
+
+let rec type_content : formatter -> type_expression -> unit =
+  fun ppf te ->
+  match te.content with
+  | T_sum m -> fprintf ppf "@[<hv 4>sum[%a]@]" (cmap_sep_d type_expression) m
+  | T_record m -> fprintf ppf "%a" (tuple_or_record_sep_type type_expression) m
+  | T_arrow a -> fprintf ppf "%a -> %a" type_expression a.type1 type_expression a.type2
+  | T_variable tv -> type_variable ppf tv
+  | T_constant tc -> type_constant ppf tc
+  | T_operator to_ -> type_operator type_expression ppf to_
+
+and type_expression ppf (te : type_expression) : unit =
+  fprintf ppf "%a" type_content te
+
+and type_operator : (formatter -> type_expression -> unit) -> formatter -> type_operator * type_expression list -> unit =
+  fun f ppf to_ ->
+  let s = match to_ with
+    TC_option                    , lst -> Format.asprintf "option(%a)"                     (list_sep_d f) lst
+  | TC_list                      , lst -> Format.asprintf "list(%a)"                       (list_sep_d f) lst
+  | TC_set                       , lst -> Format.asprintf "set(%a)"                        (list_sep_d f) lst
+  | TC_map                       , lst -> Format.asprintf "Map (%a)"                       (list_sep_d f) lst
+  | TC_big_map                   , lst -> Format.asprintf "Big Map (%a)"                   (list_sep_d f) lst
+  | TC_map_or_big_map            , lst -> Format.asprintf "Map Or Big Map (%a)"            (list_sep_d f) lst
+  | TC_contract                  , lst -> Format.asprintf "Contract (%a)"                  (list_sep_d f) lst
+  | TC_michelson_pair            , lst -> Format.asprintf "michelson_pair (%a)"            (list_sep_d f) lst                            
+  | TC_michelson_or              , lst -> Format.asprintf "michelson_or (%a)"              (list_sep_d f) lst
+  | TC_michelson_pair_right_comb , lst -> Format.asprintf "michelson_pair_right_comb (%a)" (list_sep_d f) lst
+  | TC_michelson_pair_left_comb  , lst -> Format.asprintf "michelson_pair_left_comb (%a)"  (list_sep_d f) lst
+  | TC_michelson_or_right_comb   , lst -> Format.asprintf "michelson_or_right_comb (%a)"   (list_sep_d f) lst
+  | TC_michelson_or_left_comb    , lst -> Format.asprintf "michelson_or_left_comb (%a)"    (list_sep_d f) lst
+  in
+  fprintf ppf "(type_operator: %s)" s
 
 let expression_variable ppf (ev : expression_variable) : unit =
   fprintf ppf "%a" Var.pp ev
 
 
 let rec expression ppf (e : expression) =
-  expression_content ppf e.expression_content
+  expression_content ppf e.content
 and expression_content ppf (ec : expression_content) =
   match ec with
   | E_literal l ->
@@ -109,10 +189,10 @@ let declaration ppf (d : declaration) =
   match d with
   | Declaration_type (type_name, te) ->
       fprintf ppf "@[<2>type %a =@ %a@]" type_variable type_name type_expression te
-  | Declaration_constant (name, ty_opt, i, expr) ->
+  | Declaration_constant (name, ty_opt, attr, expr) ->
       fprintf ppf "@[<2>const %a =@ %a%a@]" option_type_name (name, ty_opt) expression
         expr
-        option_inline i
+        option_inline attr.inline
 
 let program ppf (p : program) =
   fprintf ppf "@[<v>%a@]"

src/stages/4-ast_core/combinators.ml

@@ -3,109 +3,108 @@ module Option = Simple_utils.Option
 
 module SMap = Map.String
 
-let make_t ?(loc = Location.generated) type_content = {type_content; location=loc; type_meta = ()}
+let make_t ?(loc = Location.generated) ?sugar content = ({content; sugar; location=loc}: type_expression)
 
 let tuple_to_record lst =
   let aux (i,acc) el = (i+1,(string_of_int i, el)::acc) in
   let (_, lst ) = List.fold_left aux (0,[]) lst in
   lst
 
-let t_bool ?loc ()        : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool)
-let t_string ?loc ()      : type_expression = make_t ?loc @@ T_constant (TC_string)
-let t_bytes ?loc ()       : type_expression = make_t ?loc @@ T_constant (TC_bytes)
-let t_int ?loc ()         : type_expression = make_t ?loc @@ T_constant (TC_int)
-let t_operation ?loc ()   : type_expression = make_t ?loc @@ T_constant (TC_operation)
-let t_nat ?loc ()         : type_expression = make_t ?loc @@ T_constant (TC_nat)
-let t_tez ?loc ()         : type_expression = make_t ?loc @@ T_constant (TC_mutez)
-let t_unit ?loc ()        : type_expression = make_t ?loc @@ T_constant (TC_unit)
-let t_address ?loc ()     : type_expression = make_t ?loc @@ T_constant (TC_address)
-let t_signature ?loc ()   : type_expression = make_t ?loc @@ T_constant (TC_signature)
-let t_key ?loc ()         : type_expression = make_t ?loc @@ T_constant (TC_key)
-let t_key_hash ?loc ()    : type_expression = make_t ?loc @@ T_constant (TC_key_hash)
-let t_timestamp ?loc ()   : type_expression = make_t ?loc @@ T_constant (TC_timestamp)
-let t_option ?loc o       : type_expression = make_t ?loc @@ T_operator (TC_option, [o])
-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 t_bool      ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_variable (Stage_common.Constant.t_bool)
+let t_string    ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_string)
+let t_bytes     ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_bytes)
+let t_int       ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_int)
+let t_operation ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_operation)
+let t_nat       ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_nat)
+let t_tez       ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_mutez)
+let t_unit      ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_unit)
+let t_address   ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_address)
+let t_signature ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_signature)
+let t_key       ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_key)
+let t_key_hash  ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_key_hash)
+let t_timestamp ?loc ?sugar () : type_expression = make_t ?loc ?sugar @@ T_constant (TC_timestamp)
+let t_option    ?loc ?sugar o  : type_expression = make_t ?loc ?sugar @@ T_operator (TC_option, [o])
+let t_list      ?loc ?sugar t  : type_expression = make_t ?loc ?sugar @@ T_operator (TC_list, [t])
+let t_variable  ?loc ?sugar n  : type_expression = make_t ?loc ?sugar @@ T_variable (Var.of_name n)
+let t_record_ez ?loc ?sugar lst =
   let lst = List.map (fun (k, v) -> (Label k, v)) lst in
   let m = LMap.of_list lst in
-  make_t ?loc @@ T_record m
-let t_record ?loc m  : type_expression =
+  make_t ?loc ?sugar @@ T_record m
+let t_record ?loc ?sugar m  : type_expression =
   let lst = Map.String.to_kv_list m in
-  t_record_ez ?loc lst
+  t_record_ez ?loc ?sugar lst
 
-let t_pair ?loc (a , b) : type_expression = t_record_ez ?loc [("0",a) ; ("1",b)]
-let t_tuple ?loc lst    : type_expression = t_record_ez ?loc (tuple_to_record lst)
+let t_pair  ?loc ?sugar (a , b) : type_expression = t_record_ez ?loc ?sugar [("0",a) ; ("1",b)]
+let t_tuple ?loc ?sugar lst     : type_expression = t_record_ez ?loc ?sugar (tuple_to_record lst)
 
-let ez_t_sum ?loc (lst:(string * ctor_content) list) : type_expression =
+let ez_t_sum ?loc ?sugar (lst:(string * ctor_content) list) : type_expression =
   let aux prev (k, v) = CMap.add (Constructor k) v prev in
   let map = List.fold_left aux CMap.empty lst in
-  make_t ?loc @@ T_sum map
-let t_sum ?loc m : type_expression =
+  make_t ?loc ?sugar @@ T_sum map
+let t_sum ?loc ?sugar m : type_expression =
   let lst = Map.String.to_kv_list m in
-  ez_t_sum ?loc lst
+  ez_t_sum ?loc ?sugar lst
 
-let t_function ?loc type1 type2  : type_expression = make_t ?loc @@ T_arrow {type1; type2}
+let t_function ?loc ?sugar type1 type2  : type_expression = make_t ?loc ?sugar @@ T_arrow {type1; type2}
+let t_operator ?loc ?sugar op lst       : type_expression = make_t ?loc ?sugar @@ T_operator (op, lst)
+let t_map      ?loc ?sugar key value    : type_expression = make_t ?loc ?sugar @@ T_operator (TC_map, [key; value])
+let t_big_map  ?loc ?sugar key value    : type_expression = make_t ?loc ?sugar @@ T_operator (TC_big_map, [key; value])
+let t_set      ?loc ?sugar key          : type_expression = make_t ?loc ?sugar @@ T_operator (TC_set, [key])
+let t_contract ?loc ?sugar contract     : type_expression = make_t ?loc ?sugar @@ T_operator (TC_contract, [contract])
 
-let t_operator ?loc op lst       : type_expression = make_t ?loc @@ T_operator (op, lst)
-let t_map ?loc key value         : type_expression = make_t ?loc @@ T_operator (TC_map, [key; value])
-let t_big_map ?loc key value     : type_expression = make_t ?loc @@ T_operator (TC_big_map, [key; value])
-let t_set ?loc key               : type_expression = make_t ?loc @@ T_operator (TC_set, [key])
-let t_contract ?loc contract     : type_expression = make_t ?loc @@ T_operator (TC_contract, [contract])
+let make_e ?(loc = Location.generated) ?sugar content = {content; sugar; location=loc }
 
-let make_e ?(loc = Location.generated) expression_content = { expression_content; location=loc }
-
-let e_var ?loc (n: string) : expression = make_e ?loc @@ E_variable (Var.of_name n)
-let e_literal ?loc l : expression = make_e ?loc @@ E_literal l
-let e_unit ?loc () : expression = make_e ?loc @@ E_literal (Literal_unit)
-let e_int ?loc n : expression = make_e ?loc @@ E_literal (Literal_int n)
-let e_nat ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n)
-let e_timestamp ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n)
-let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s)
-let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s)
-let e_mutez ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s)
-let e_signature ?loc s : expression = make_e ?loc @@ E_literal (Literal_signature s)
-let e_key ?loc s : expression = make_e ?loc @@ E_literal (Literal_key s)
-let e_key_hash ?loc s : expression = make_e ?loc @@ E_literal (Literal_key_hash s)
-let e_chain_id ?loc s : expression = make_e ?loc @@ E_literal (Literal_chain_id s)
+let e_var       ?loc ?sugar n  : expression = make_e ?loc ?sugar @@ E_variable (Var.of_name n)
+let e_literal   ?loc ?sugar l  : expression = make_e ?loc ?sugar @@ E_literal l
+let e_unit      ?loc ?sugar () : expression = make_e ?loc ?sugar @@ E_literal (Literal_unit)
+let e_int       ?loc ?sugar n  : expression = make_e ?loc ?sugar @@ E_literal (Literal_int n)
+let e_nat       ?loc ?sugar n  : expression = make_e ?loc ?sugar @@ E_literal (Literal_nat n)
+let e_timestamp ?loc ?sugar n  : expression = make_e ?loc ?sugar @@ E_literal (Literal_timestamp n)
+let e_string    ?loc ?sugar s  : expression = make_e ?loc ?sugar @@ E_literal (Literal_string s)
+let e_address   ?loc ?sugar s  : expression = make_e ?loc ?sugar @@ E_literal (Literal_address s)
+let e_mutez     ?loc ?sugar s  : expression = make_e ?loc ?sugar @@ E_literal (Literal_mutez s)
+let e_signature ?loc ?sugar s  : expression = make_e ?loc ?sugar @@ E_literal (Literal_signature s)
+let e_key       ?loc ?sugar s  : expression = make_e ?loc ?sugar @@ E_literal (Literal_key s)
+let e_key_hash  ?loc ?sugar s  : expression = make_e ?loc ?sugar @@ E_literal (Literal_key_hash s)
+let e_chain_id  ?loc ?sugar s  : expression = make_e ?loc ?sugar @@ E_literal (Literal_chain_id s)
 let e'_bytes b : expression_content =
   let bytes = Hex.to_bytes (`Hex b) in
   E_literal (Literal_bytes bytes)
-let e_bytes_hex ?loc b : expression =
+let e_bytes_hex ?loc ?sugar b : expression =
   let e' = e'_bytes b in
-  make_e ?loc e'
-let e_bytes_raw ?loc (b: bytes) : expression =
-  make_e ?loc @@ E_literal (Literal_bytes b)
-let e_bytes_string ?loc (s: string) : expression =
-  make_e ?loc @@ E_literal (Literal_bytes (Hex.to_bytes (Hex.of_string s)))
-let e_some ?loc s  : expression = make_e ?loc @@ E_constant {cons_name = C_SOME; arguments = [s]}
-let e_none ?loc () : expression = make_e ?loc @@ E_constant {cons_name = C_NONE; arguments = []}
-let e_string_cat ?loc sl sr : expression = make_e ?loc @@ E_constant {cons_name = C_CONCAT; arguments = [sl ; sr ]}
-let e_map_add ?loc k v old  : expression = make_e ?loc @@ E_constant {cons_name = C_MAP_ADD; arguments = [k ; v ; old]}
+  make_e ?loc ?sugar e'
+let e_bytes_raw ?loc ?sugar (b: bytes) : expression =
+  make_e ?loc ?sugar @@ E_literal (Literal_bytes b)
+let e_bytes_string ?loc ?sugar (s: string) : expression =
+  make_e ?loc ?sugar @@ E_literal (Literal_bytes (Hex.to_bytes (Hex.of_string s)))
+let e_some       ?loc ?sugar s        : expression = make_e ?loc ?sugar @@ E_constant {cons_name = C_SOME; arguments = [s]}
+let e_none       ?loc ?sugar ()       : expression = make_e ?loc ?sugar @@ E_constant {cons_name = C_NONE; arguments = []}
+let e_string_cat ?loc ?sugar sl sr    : expression = make_e ?loc ?sugar @@ E_constant {cons_name = C_CONCAT; arguments = [sl ; sr ]}
+let e_map_add    ?loc ?sugar k v old  : expression = make_e ?loc ?sugar @@ E_constant {cons_name = C_MAP_ADD; arguments = [k ; v ; old]}
 
-let e_constant ?loc name lst = make_e ?loc @@ E_constant {cons_name=name ; arguments = lst}
-let e_variable ?loc v = make_e ?loc @@ E_variable v
-let e_application ?loc a b = make_e ?loc @@ E_application {lamb=a ; args=b}
-let e_lambda ?loc binder input_type output_type result =  make_e ?loc @@ E_lambda {binder; input_type; output_type; result ;  }
-let e_recursive ?loc fun_name fun_type lambda = make_e ?loc @@ E_recursive {fun_name; fun_type; lambda}
-let e_let_in ?loc (binder, ascr) inline rhs let_result = make_e ?loc @@ E_let_in { let_binder = (binder,ascr) ; rhs ; let_result; inline }
-let e_raw_code ?loc language code = make_e ?loc @@ E_raw_code {language; code}
+let e_constant    ?loc ?sugar name lst                             = make_e ?loc ?sugar @@ E_constant {cons_name=name ; arguments = lst}
+let e_variable    ?loc ?sugar v                                    = make_e ?loc ?sugar @@ E_variable v
+let e_application ?loc ?sugar a b                                  = make_e ?loc ?sugar @@ E_application {lamb=a ; args=b}
+let e_lambda      ?loc ?sugar binder input_type output_type result = make_e ?loc ?sugar @@ E_lambda {binder; input_type; output_type; result ;  }
+let e_recursive   ?loc ?sugar fun_name fun_type lambda             = make_e ?loc ?sugar @@ E_recursive {fun_name; fun_type; lambda}
+let e_let_in      ?loc ?sugar (binder, ascr) inline rhs let_result = make_e ?loc ?sugar @@ E_let_in { let_binder = (binder,ascr) ; rhs ; let_result; inline }
+let e_raw_code    ?loc ?sugar language code                        = make_e ?loc ?sugar @@ E_raw_code {language; code}
 
-let e_constructor ?loc s a : expression = make_e ?loc @@ E_constructor { constructor = Constructor s; element = a}
-let e_matching ?loc a b : expression = make_e ?loc @@ E_matching {matchee=a;cases=b}
+let e_constructor ?loc ?sugar s a : expression = make_e ?loc ?sugar @@ E_constructor { constructor = Constructor s; element = a}
+let e_matching    ?loc ?sugar a b : expression = make_e ?loc ?sugar @@ E_matching {matchee=a;cases=b}
 
-let e_record ?loc map = make_e ?loc @@ E_record map
-let e_record_accessor ?loc a b = make_e ?loc @@ E_record_accessor {record = a; path = b}
-let e_record_update ?loc record path update = make_e ?loc @@ E_record_update {record; path; update}
+let e_record          ?loc ?sugar map = make_e ?loc ?sugar @@ E_record map
+let e_record_accessor ?loc ?sugar a b = make_e ?loc ?sugar @@ E_record_accessor {record = a; path = b}
+let e_record_update   ?loc ?sugar record path update = make_e ?loc ?sugar @@ E_record_update {record; path; update}
 
-let e_annotation ?loc anno_expr ty = make_e ?loc @@ E_ascription {anno_expr; type_annotation = ty}
+let e_annotation ?loc ?sugar anno_expr ty = make_e ?loc ?sugar @@ E_ascription {anno_expr; type_annotation = ty}
 
-let e_bool ?loc   b : expression = e_constructor ?loc (string_of_bool b) (e_unit ())
+let e_bool ?loc ?sugar b : expression = e_constructor ?loc ?sugar (string_of_bool b) (e_unit ())
 
-let make_option_typed ?loc e t_opt =
+let make_option_typed ?loc ?sugar e t_opt =
   match t_opt with
   | None -> e
-  | Some t -> e_annotation ?loc e t
+  | Some t -> e_annotation ?loc ?sugar e t
 
 let e_typed_none ?loc t_opt =
   let type_annotation = t_option t_opt in
@@ -139,7 +138,7 @@ let get_e_list = fun t ->
   let rec aux t = 
     match t with
       E_constant {cons_name=C_CONS;arguments=[key;lst]} -> 
-        let lst = aux lst.expression_content in
+        let lst = aux lst.content in
         (Some key)::(lst)
     | E_constant {cons_name=C_LIST_EMPTY;arguments=[]} ->
         []
@@ -161,7 +160,7 @@ let get_e_ascription = fun a ->
 
 (* Same as get_e_pair *)
 let extract_pair : expression -> (expression * expression) option = fun e ->
-  match e.expression_content with
+  match e.content with
   | E_record r -> ( 
   let lst = LMap.to_kv_list r in
     match lst with 
@@ -173,13 +172,13 @@ let extract_pair : expression -> (expression * expression) option = fun e ->
   | _ -> None
 
 let extract_record : expression -> (label * expression) list option = fun e ->
-  match e.expression_content with
+  match e.content with
   | E_record lst -> Some (LMap.to_kv_list lst)
   | _ -> None
 
 let extract_map : expression -> (expression * expression) list option = fun e ->
   let rec aux e =
-    match e.expression_content with
+    match e.content with
       E_constant {cons_name=C_UPDATE|C_MAP_ADD; arguments=[k;v;map]} -> 
         let map = aux map in
         (Some (k,v))::map 

src/stages/4-ast_core/combinators.mli

@@ -1,86 +1,86 @@
 open Types
 
-val make_t      : ?loc:Location.t -> type_content -> type_expression
-val t_bool      : ?loc:Location.t -> unit -> type_expression
-val t_string    : ?loc:Location.t -> unit -> type_expression
-val t_bytes     : ?loc:Location.t -> unit -> type_expression
-val t_int       : ?loc:Location.t -> unit -> type_expression
-val t_operation : ?loc:Location.t -> unit -> type_expression
-val t_nat       : ?loc:Location.t -> unit -> type_expression
-val t_tez       : ?loc:Location.t -> unit -> type_expression
-val t_unit      : ?loc:Location.t -> unit -> type_expression
-val t_address   : ?loc:Location.t -> unit -> type_expression
-val t_key       : ?loc:Location.t -> unit -> type_expression
-val t_key_hash  : ?loc:Location.t -> unit -> type_expression
-val t_timestamp : ?loc:Location.t -> unit -> type_expression
-val t_signature : ?loc:Location.t -> unit -> type_expression
+val make_t      : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> type_content -> type_expression
+val t_bool      : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_string    : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_bytes     : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_int       : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_operation : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_nat       : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_tez       : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_unit      : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_address   : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_key       : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_key_hash  : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_timestamp : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
+val t_signature : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> unit -> type_expression
 (*
 val t_option    : type_expression -> type_expression
 *)
-val t_list      : ?loc:Location.t -> type_expression -> type_expression
-val t_variable  : ?loc:Location.t -> string -> type_expression
+val t_list      : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> type_expression -> type_expression
+val t_variable  : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> string -> type_expression
 (*
 val t_record    : te_map -> type_expression
 *)
-val t_pair   : ?loc:Location.t -> ( field_content * field_content ) -> type_expression
-val t_tuple  : ?loc:Location.t -> field_content list -> type_expression
+val t_pair   : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> ( field_content * field_content ) -> type_expression
+val t_tuple  : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> field_content list -> type_expression
 
-val t_record    : ?loc:Location.t -> field_content Map.String.t -> type_expression
-val t_record_ez : ?loc:Location.t -> (string * field_content) list -> type_expression
+val t_record    : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> field_content Map.String.t -> type_expression
+val t_record_ez : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> (string * field_content) list -> type_expression
 
-val t_sum    : ?loc:Location.t -> Types.ctor_content Map.String.t -> type_expression
-val ez_t_sum : ?loc:Location.t -> ( string * Types.ctor_content ) list -> type_expression
+val t_sum    : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> Types.ctor_content Map.String.t -> type_expression
+val ez_t_sum : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> ( string * Types.ctor_content ) list -> type_expression
 
-val t_function : ?loc:Location.t -> type_expression -> type_expression -> type_expression
+val t_function : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> type_expression -> type_expression -> type_expression
 
-val t_operator : ?loc:Location.t -> type_operator -> type_expression list -> type_expression
-val t_map : ?loc:Location.t -> type_expression -> type_expression -> type_expression
-val t_big_map : ?loc:Location.t -> type_expression -> type_expression -> type_expression
-val t_contract : ?loc:Location.t -> type_expression -> type_expression
-val t_set      : ?loc:Location.t -> type_expression -> type_expression
+val t_operator : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> type_operator -> type_expression list -> type_expression
+val t_map : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> type_expression -> type_expression -> type_expression
+val t_big_map : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> type_expression -> type_expression -> type_expression
+val t_contract : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> type_expression -> type_expression
+val t_set      : ?loc:Location.t -> ?sugar:Ast_sugar.type_expression -> type_expression -> type_expression
 
-val make_e : ?loc:Location.t -> expression_content -> expression
-val e_var : ?loc:Location.t -> string -> expression
-val e_literal : ?loc:Location.t -> literal -> expression
-val e_unit : ?loc:Location.t -> unit -> expression
-val e_int : ?loc:Location.t -> Z.t -> expression 
-val e_nat : ?loc:Location.t -> Z.t -> expression
-val e_timestamp : ?loc:Location.t -> Z.t -> expression
-val e_bool : ?loc:Location.t -> bool -> expression
-val e_string : ?loc:Location.t -> ligo_string -> expression
-val e_address : ?loc:Location.t -> string -> expression 
-val e_signature : ?loc:Location.t -> string -> expression 
-val e_key : ?loc:Location.t -> string -> expression 
-val e_key_hash : ?loc:Location.t -> string -> expression 
-val e_chain_id : ?loc:Location.t -> string -> expression 
-val e_mutez : ?loc:Location.t -> Z.t -> expression
+val make_e         : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression_content -> expression
+val e_var          : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression
+val e_literal      : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> literal -> expression
+val e_unit         : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> unit -> expression
+val e_int          : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> Z.t -> expression 
+val e_nat          : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> Z.t -> expression
+val e_timestamp    : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> Z.t -> expression
+val e_bool         : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> bool -> expression
+val e_string       : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> ligo_string -> expression
+val e_address      : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression 
+val e_signature    : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression 
+val e_key          : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression 
+val e_key_hash     : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression 
+val e_chain_id     : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression 
+val e_mutez        : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> Z.t -> expression
 val e'_bytes       : string -> expression_content
-val e_bytes_hex : ?loc:Location.t -> string -> expression
-val e_bytes_raw : ?loc:Location.t -> bytes -> expression
-val e_bytes_string : ?loc:Location.t -> string -> expression
+val e_bytes_hex    : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression
+val e_bytes_raw    : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> bytes -> expression
+val e_bytes_string : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression
 
-val e_some : ?loc:Location.t -> expression -> expression
-val e_none : ?loc:Location.t -> unit -> expression
-val e_string_cat : ?loc:Location.t -> expression -> expression -> expression
-val e_map_add : ?loc:Location.t -> expression -> expression ->  expression -> expression
-val e_constructor : ?loc:Location.t -> string -> expression -> expression
-val e_matching : ?loc:Location.t -> expression -> matching_expr -> expression
-val e_record_accessor : ?loc:Location.t -> expression -> label -> expression
-val e_variable : ?loc:Location.t -> expression_variable -> expression
-val e_let_in : ?loc:Location.t -> ( expression_variable * type_expression option ) -> bool -> expression -> expression -> expression
-val e_raw_code : ?loc:Location.t -> string -> expression -> expression
-val e_annotation : ?loc:Location.t -> expression -> type_expression -> expression
-val e_application : ?loc:Location.t -> expression -> expression -> expression
-val e_constant : ?loc:Location.t -> constant' -> expression list -> expression
+val e_some            : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression -> expression
+val e_none            : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> unit -> expression
+val e_string_cat      : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression -> expression -> expression
+val e_map_add         : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression -> expression ->  expression -> expression
+val e_constructor     : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression -> expression
+val e_matching        : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression -> matching_expr -> expression
+val e_record_accessor : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression -> label -> expression
+val e_variable        : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression_variable -> expression
+val e_let_in          : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> ( expression_variable * type_expression option ) -> bool -> expression -> expression -> expression
+val e_raw_code        : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> string -> expression -> expression
+val e_annotation      : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression -> type_expression -> expression
+val e_application     : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression -> expression -> expression
+val e_constant        : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> constant' -> expression list -> expression
 
-val make_option_typed : ?loc:Location.t -> expression -> type_expression option -> expression
+val make_option_typed : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression -> type_expression option -> expression
 
 val e_typed_none      : ?loc:Location.t -> type_expression -> expression
 
-val e_lambda : ?loc:Location.t -> expression_variable -> type_expression option -> type_expression option -> expression -> expression
-val e_recursive : ?loc:Location.t -> expression_variable -> type_expression -> lambda -> expression
-val e_record : ?loc:Location.t -> expr label_map-> expression
-val e_record_update : ?loc:Location.t -> expression -> label -> expression -> expression
+val e_lambda        : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression_variable -> type_expression option -> type_expression option -> expression -> expression
+val e_recursive     : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression_variable -> type_expression -> lambda -> expression
+val e_record        : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expr label_map-> expression
+val e_record_update : ?loc:Location.t -> ?sugar:Ast_sugar.expression -> expression -> label -> expression -> expression
 
 val assert_e_record_accessor : expression_content -> unit option
 

src/stages/4-ast_core/dune

@@ -5,6 +5,7 @@
     simple-utils
     tezos-utils
     stage_common
+    ast_sugar
   )
   (preprocess
     (pps ppx_let bisect_ppx --conditional)

src/stages/4-ast_core/misc.ml

@@ -97,7 +97,7 @@ let assert_literal_eq (a, b : literal * literal) : unit option =
   | Literal_chain_id _, _ -> None
 
 let rec assert_value_eq (a, b: (expression * expression )) : unit option =
-  match (a.expression_content , b.expression_content) with
+  match (a.content , b.content) with
   | E_literal a , E_literal b ->
     assert_literal_eq (a, b)
   | E_constant (ca) , E_constant (cb) when ca.cons_name = cb.cons_name -> (

src/stages/4-ast_core/types.ml

@@ -2,15 +2,11 @@
 
 module Location = Simple_utils.Location
 
-module Ast_core_parameter = struct
-  type type_meta = unit
-end
-
 include Stage_common.Types
 
-include Ast_generic_type (Ast_core_parameter)
-
-type inline = bool 
+type attribute = {
+  inline: bool
+} 
 type program = declaration Location.wrap list
 and declaration =
   | Declaration_type of (type_variable * type_expression)
@@ -20,10 +16,35 @@ and declaration =
    *   an optional type annotation
    *   a boolean indicating whether it should be inlined
    *   an expression *)
-  | Declaration_constant of (expression_variable * type_expression option * inline * expression)
+  | Declaration_constant of (expression_variable * type_expression option * attribute * expression)
 
 (* | Macro_declaration of macro_declaration *)
-and expression = {expression_content: expression_content; location: Location.t}
+
+
+and type_content =
+  | T_sum of ctor_content constructor_map
+  | T_record of field_content label_map
+  | T_arrow of arrow
+  | T_variable of type_variable
+  | T_constant of type_constant
+  | T_operator of (type_operator * type_expression list)
+
+and arrow = {type1: type_expression; type2: type_expression}
+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 ; field_decl_pos : int}
+
+and type_expression = {
+  content  : type_content; 
+  sugar    : Ast_sugar.type_expression option;
+  location : Location.t;
+  }
+
+
+and expression = {
+  content  : expression_content; 
+  sugar    : Ast_sugar.expression option;
+  location : Location.t
+  }
 
 and expression_content =
   (* Base *)

src/stages/5-ast_typed/PP_generic.ml

@@ -42,10 +42,10 @@ module M = struct
   let op ppf : (no_state, unit) fold_config = {
       generic = (fun NoState info ->
         match info.node_instance.instance_kind with
-        | RecordInstance { fields } ->
+        | RecordInstance { field_instances } ->
            let aux ppf (fld : ('xi , 'xo) Adt_info.ctor_or_field_instance) =
              fprintf ppf "%s = %a" fld.cf.name (fun _ppf -> fld.cf_continue) NoState in
-           fprintf ppf "{@,@[<hv 2> %a @]@,}" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) fields
+           fprintf ppf "{@,@[<hv 2> %a @]@,}" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) field_instances
         | VariantInstance { constructor ; _ } ->
            if constructor.cf_new_fold needs_parens NoState
            then fprintf ppf "%s (%a)" constructor.cf.name (fun _ppf -> constructor.cf_continue) NoState

src/stages/5-ast_typed/PP_json.ml

@@ -10,12 +10,12 @@ module M = struct
   let to_json : (no_state, json) fold_config = {
       generic = (fun NoState info ->
         match info.node_instance.instance_kind with
-        | RecordInstance { fields } ->
-          let fields' = List.fold_left
+        | RecordInstance { field_instances } ->
+          let field_instances' = List.fold_left
             (fun acc (fld : ('xi, json) Adt_info.ctor_or_field_instance) -> (fld.cf.name, fld.cf_continue NoState)::acc)
-            [] fields 
+            [] field_instances 
           in
-          `Assoc fields'
+          `Assoc field_instances'
         | VariantInstance { constructor ; _ } ->
           `List [ `String constructor.cf.name ; constructor.cf_continue NoState ]
         | PolyInstance { poly=_; arguments=_; poly_continue } ->
@@ -76,13 +76,23 @@ module M = struct
         `Assoc ["typeVariableMap",  `List lst'] );
     }
 
-  let print : ((no_state, json) fold_config -> no_state -> 'a -> json) -> 'a -> json = fun fold v ->
+  let to_json : ((no_state, json) fold_config -> no_state -> 'a -> json) -> 'a -> json = fun fold v ->
     fold to_json NoState v
+  
+  let print : ((no_state, json) fold_config -> no_state -> 'a -> json) -> formatter -> 'a -> unit  = fun fold ppf v ->
+    fprintf ppf "%a" Yojson.Basic.pp (to_json fold v)
 end
 
+module Yojson = Fold.Folds(struct
+  type in_state = M.no_state ;;
+  type out_state = json ;;
+  type 'a t = 'a -> json ;;
+  let f = M.to_json ;;
+end)
+
 include Fold.Folds(struct
   type in_state = M.no_state ;;
   type out_state = json ;;
-  type 'a t = 'a -> json ;;
+  type 'a t = formatter -> 'a -> unit ;;
   let f = M.print ;;
 end)

src/stages/5-ast_typed/ast_typed.ml

@@ -17,5 +17,6 @@ module Helpers = Helpers
 include Types
 include Misc
 include Combinators
+module Debug = Stage_common.Debug
 
 let program_environment env program = fst (Compute_environment.program env program)

src/stages/5-ast_typed/compare_generic.ml

@@ -36,10 +36,10 @@ module M = struct
   let op : (no_state, t) fold_config = {
       generic = (fun NoState info ->
         match info.node_instance.instance_kind with
-        | RecordInstance { fields } ->
+        | RecordInstance { field_instances } ->
            let aux (fld : ('xi, 'xo) Adt_info.ctor_or_field_instance) =
              ( fld.cf.name , fun () -> fld.cf_continue NoState ) in
-           Record ("name_of_the_record", List.map aux fields)
+           Record ("name_of_the_record", List.map aux field_instances)
         | VariantInstance { constructor ; _ } ->
            VariantConstructor ("name_of_the_variant", constructor.cf.name, fun () -> constructor.cf_continue NoState)
         | PolyInstance { poly=_; arguments=_; poly_continue } ->

src/stages/5-ast_typed/formatter.ml

@@ -4,7 +4,7 @@ let program_ppformat ~display_format f (typed,_) =
   match display_format with
   | Human_readable | Dev -> PP.program f typed
 
-let program_jsonformat (typed,_) : json = PP_json.program typed
+let program_jsonformat (typed,_) : json = PP_json.Yojson.program typed
 
 let program_format : 'a format = {
   pp = program_ppformat;

src/stages/5-ast_typed/types_utils.ml

@@ -127,3 +127,33 @@ let fold_map__poly_set : type a state new_a err . new_a extra_info__comparable -
     ok (state , PolySet.add new_elt s) in
   let%bind (state , m) = PolySet.fold_inc aux s ~init:(ok (state, PolySet.create ~cmp:new_compare)) in
   ok (state , m)
+
+
+(* This takes a fold_map__xxx function and turns it into a make__xxx
+   function.
+   It just swaps the error monad with the option monad, and uses unit
+   as the type for the state and for "errors". *)
+let fold_map_to_make fold_map = fun f v ->
+  match fold_map (fun () x -> match f x with Some x' -> ok ((), x') | None -> Pervasives.Error ()) () v with
+    Pervasives.Ok (((), v'), _) -> Some v'
+  | Pervasives.Error () -> None
+
+(* This can't be done automatically, because the auto-generated
+   comparison functions make use of the fold, the fold supplies to
+   users some "make" functions, and there's no deterministic way to
+   extract the comparison functions (or other typeclass-like
+   functions).
+
+   Instead of writing the following functions, we could just write the
+   get_typeclass_compare functions for poly_unionfind and poly_set,
+   but the resulting code wouldn't be much clearer. *)
+let make__constructor_map f v = fold_map_to_make fold_map__constructor_map f v
+let make__label_map f v = fold_map_to_make fold_map__label_map f v
+let make__list f v = fold_map_to_make fold_map__list f v
+let make__location_wrap f v = fold_map_to_make fold_map__location_wrap f v
+let make__list_ne f v = fold_map_to_make fold_map__list_ne f v
+let make__option f v = fold_map_to_make fold_map__option f v
+let make__poly_unionfind f v = fold_map_to_make (fold_map__poly_unionfind { compare = failwith "TODO" (*UnionFind.Poly2.get_compare v*) }) f v
+let make__PolyMap f v = fold_map_to_make fold_map__PolyMap f v
+let make__typeVariableMap f v = fold_map_to_make fold_map__typeVariableMap f v
+let make__poly_set f v = fold_map_to_make (fold_map__poly_set { compare = failwith "TODO" (*PolySet.get_compare v*) }) f v

src/stages/adt_generator/common.ml

@@ -1,3 +1,7 @@
 type ('a,'err) monad = ('a,'err) Simple_utils.Trace.result;;
 let (>>?) v f = Simple_utils.Trace.bind f v;;
 let return v = Simple_utils.Trace.ok v;;
+
+let sorted_bindings m =
+  List.sort (fun (a , _) (b , _) -> String.compare a b)
+  @@ RedBlackTrees.PolyMap.bindings m

src/stages/adt_generator/dune

@@ -3,5 +3,6 @@
   (public_name ligo.adt_generator)
   (libraries
     simple-utils
+    RedBlackTrees
   )
 )

src/stages/adt_generator/generator.raku

@@ -94,6 +94,12 @@ $*OUT = open $folder_filename, :w;
     for $statements -> $statement { say "$statement" }
     say "open $moduleName;;";
 
+    say "  (* must be provided by one of the open or include statements: *)";
+    say "  module CheckFolderInputSignature = struct";
+    for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant}).map({$_<kind>}).unique -> $poly
+    { say "    let make__$poly : type a b . (a -> b option) -> a $poly -> b $poly option = make__$poly;;"; }
+    say "  end";
+
     say "";
     say "  include Adt_generator.Generic.BlahBluh";
     say "  type ('in_state, 'out_state , 'adt_info_node_instance_info) _fold_config = \{";
@@ -107,9 +113,25 @@ $*OUT = open $folder_filename, :w;
     { say "      $poly : 'a . ('in_state , 'out_state , 'adt_info_node_instance_info) _fold_config -> ('in_state -> 'a -> 'out_state) -> 'in_state -> 'a $poly -> 'out_state;"; }
     say '    };;';
 
+    say "";
+    say "  type whatever =";
+    say "  | NoArgument (* supplied to make constructors with no arguments *)";
+    # look for builtins, filtering out the "implicit unit-like fake argument of emtpy constructors" (represented by '')
+    for $adts.map({ $_<ctorsOrFields> })[*;*].grep({$_<isBuiltin> && $_<type> ne ''}).map({$_<type>}).unique -> $builtin
+    { say "  | Whatever_{tc $builtin} of $builtin"; }
+    for $adts.list -> $t
+    { say "  | Whatever_{tc $t<name>} of $t<name>" }
+
+    say "  type make_poly =";
+    # look for built-in polymorphic types
+    for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant}).map({$_<kind>}).unique -> $poly
+    { say "  | Make_{tc $poly} of (whatever $poly -> whatever option)"; }
+
     say "";
     say "  module Adt_info = Adt_generator.Generic.Adt_info (struct";
     say "    type nonrec ('in_state , 'out_state , 'adt_info_node_instance_info) fold_config = ('in_state , 'out_state , 'adt_info_node_instance_info) _fold_config;;";
+    say "    type nonrec whatever = whatever;;";
+    say "    type nonrec make_poly = make_poly;;";
     say "  end);;";
     say "  include Adt_info;;";
     say "  type ('in_state, 'out_state) fold_config = ('in_state , 'out_state , ('in_state , 'out_state) Adt_info.node_instance_info) _fold_config;;";
@@ -127,14 +149,31 @@ $*OUT = open $folder_filename, :w;
     for $adts.list -> $t
     { for $t<ctorsOrFields>.list -> $c
       { say "  (* info for field or ctor $t<name>.$c<name> *)";
+        if ($t<kind> eq $variant) {
+	    say "  let info__$t<name>__$c<name> : Adt_info.constructor_type = \{";
+	    say "      ctor = \{";
+	    say "        name = \"$c<name>\";";
+	    say "        is_builtin = {$c<isBuiltin> ?? 'true' !! 'false'};";
+	    say "        type_ = \"$c<type>\";";
+	    say "      \};";
+	    if ($c<type> eq '') {
+		# this constructor has no arguments.
+		say "      make_ctor = (function NoArgument -> Some (Whatever_{tc $t<name>} $c<name>) | _ -> None);";
+	    } else {
+		say "      make_ctor = (function Whatever_{tc $c<type>} v -> Some (Whatever_{tc $t<name>} ($c<name> v)) | _ -> None);";
+	    }
+	    say '    };;';
+        } else {
 	    say "  let info__$t<name>__$c<name> : Adt_info.ctor_or_field = \{";
 	    say "        name = \"$c<name>\";";
 	    say "        is_builtin = {$c<isBuiltin> ?? 'true' !! 'false'};";
 	    say "        type_ = \"$c<type>\";";
 	    say '    };;';
+	}
         # say "";
         say "  let continue_info__$t<name>__$c<name> : type in_qstate out_qstate . the_folds -> (in_qstate , out_qstate) fold_config -> {$c<type> || 'unit'} -> (in_qstate, out_qstate) Adt_info.ctor_or_field_instance = fun the_folds visitor x -> \{";
-        say "        cf = info__$t<name>__$c<name>;";
+        my $dotctor = ($t<kind> eq $variant) ?? ".ctor" !! ""; # TODO: give the full constructor info with its "make" function instead of extracting the .ctor part.
+        say "        cf = info__$t<name>__$c<name>$dotctor;";
         say "        cf_continue = (fun state -> the_folds.fold__$t<name>__$c<name> the_folds visitor state x);";
         say "        cf_new_fold = (fun visitor state -> the_folds.fold__$t<name>__$c<name> the_folds visitor state x);";
         say '      };;';
@@ -142,16 +181,40 @@ $*OUT = open $folder_filename, :w;
       }
       say "  (* info for node $t<name> *)";
       say "  let info__$t<name> : Adt_info.node = \{";
-      my $kind = do given $t<kind> {
-          when $record { "Record" }
-          when $variant { "Variant" }
-          default { "Poly \"$_\"" }
-      };
-      say "      kind = $kind;";
-      say "      declaration_name = \"$t<name>\";";
-      print "      ctors_or_fields = [ ";
+      print "      kind = ";
+      do given $t<kind> {
+          when $record {
+	      say "RecordType \{";
+	      say "        fields = [";
+	      for $t<ctorsOrFields>.list -> $f {
+		  say "          info__$t<name>__$f<name>;";
+	      }
+	      say "        ];";
+	      say "        make_record = (fun r -> match Adt_generator.Common.sorted_bindings r with";
+	      say "        | [";
+	      for $t<ctorsOrFields>.list.sort({$_<name>}) -> $f {
+		  say "          (\"$f<name>\" , Whatever_{tc $f<type>} $f<name>) ;";
+	      }	    
+	      say "          ] -> Some (Whatever_{tc $t<name>} \{";
+	      for $t<ctorsOrFields>.list -> $f { say "          $f<name> ;"; }
+	      say "        \})";
+	      say "        | _ -> None)";
+	      say "      \};"; }
+          when $variant {
+	      say "VariantType \{";
+	      print "        constructors = [ ";
 	      for $t<ctorsOrFields>.list -> $c { print "info__$t<name>__$c<name> ; "; }
 	      say "];";
+	      say "      \};"; }
+          default {
+	      say "PolyType \{";
+	      say "        poly_name = \"$_\";";
+	      print "        make_poly = Make_{tc $_} (fun p -> match make__$_ ";
+	      for $t<ctorsOrFields>.list -> $a { print "(function Whatever_{tc $a<type>} v -> Some v | _ -> None)"; }
+	      say " p with Some p -> Some (Whatever_{tc $t<name>} p) | None -> None);";
+	      say "      \};"; }
+      };
+      say "      declaration_name = \"$t<name>\";";
       say '    };;';
       # say "";
       # TODO: factor out some of the common bits here.
@@ -161,9 +224,9 @@ $*OUT = open $folder_filename, :w;
       do given $t<kind> {
           when $record {
               say '      instance_kind = RecordInstance {';
-              print "      fields = [ ";
+              print "          field_instances = [ ";
               for $t<ctorsOrFields>.list -> $c { print "continue_info__$t<name>__$c<name> the_folds visitor x.$c<name> ; "; }
-              say "      ];";
+              say "];";
               say '        };';
           }
           when $variant {
@@ -174,7 +237,7 @@ $*OUT = open $folder_filename, :w;
               for $t<ctorsOrFields>.list -> $c { say "               | $c<name> { $c<type> ?? 'v ' !! '' }-> continue_info__$t<name>__$c<name> the_folds visitor { $c<type> ?? 'v' !! '()' }"; }
               say "              );";
               print "            variant = [ ";
-              for $t<ctorsOrFields>.list -> $c { print "info__$t<name>__$c<name> ; "; }
+              for $t<ctorsOrFields>.list -> $c { print "info__$t<name>__$c<name>.ctor ; "; } # TODO: give the full constructor info with its "make" function.
               say "];";
               say '          };';
           }
@@ -183,9 +246,7 @@ $*OUT = open $folder_filename, :w;
               say '        PolyInstance {';
               say "            poly = \"$_\";";
               print "            arguments = [";
-              # TODO: sort by c<name> (currently we only have one-argument
-              # polymorphic types so it happens to work but should be fixed.
-              for $t<ctorsOrFields>.list -> $c { print "\"$c<type>\""; }
+              for $t<ctorsOrFields>.list.sort({$_<name>}) -> $c { print "\"$c<type>\""; }
               say "];";
               print "            poly_continue = (fun state -> visitor.$_ visitor (";
               print $t<ctorsOrFields>
@@ -201,10 +262,11 @@ $*OUT = open $folder_filename, :w;
 
     say "";
     say "  (* info for adt $moduleName *)";
-    print "  let whole_adt_info : unit -> Adt_info.adt = fun () -> [ ";
+    say "  let whole_adt_info : unit -> Adt_info.adt = fun () ->";
+    print "  match RedBlackTrees.PolyMap.from_list ~cmp:String.compare [ ";
     for $adts.list -> $t
-    { print "info__$t<name> ; "; }
-    say "];;";
+    { print "\"$t<name>\" , info__$t<name> ; "; }
+    say "] with Some x -> x | None -> failwith \"Internal error: duplicate nodes in ADT info\";;";
 
     # fold functions
     say "";
@@ -300,7 +362,7 @@ $*OUT = open $mapper_filename, :w;
     }
 
     say "";
-    for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant && $typeclasses{$_<kind>}}).unique(:as({$_<ctorsOrFields>, $_<kind>})) -> $t
+    for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant && $typeclasses{$_<kind>}}).unique(:as({$_<ctorsOrFields>, $_<kind>}), :with(&[eqv])) -> $t
     { my $ty = $t<ctorsOrFields>[0]<type>;
       my $typeclass = $typeclasses{$t<kind>};
       say "  val extra_info__{$ty}__$typeclass : $ty extra_info__$typeclass;;"; }
@@ -311,7 +373,7 @@ $*OUT = open $mapper_filename, :w;
     say "  module O : OSig = $oModuleName";
     say "";
     say "  (* must be provided by one of the open or include statements: *)";
-    say "  module CheckInputSignature = struct";
+    say "  module CheckMapperInputSignature = struct";
     for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant}).map({$_<kind>}).unique -> $poly
     { say "    let fold_map__$poly : type a new_a state err .{ $typeclasses{$poly} ?? " new_a extra_info__{$typeclasses{$poly}} ->" !! "" } (state -> a -> (state * new_a, err) monad) -> state -> a $poly -> (state * new_a $poly , err) monad = fold_map__$poly;;"; }
     say "  end";
@@ -500,7 +562,7 @@ $*OUT = open $combinators_filename, :w;
     }
 
     say "";
-    for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant && $typeclasses{$_<kind>}}).unique(:as({$_<ctorsOrFields>, $_<kind>})) -> $t
+    for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant && $typeclasses{$_<kind>}}).unique(:as({$_<ctorsOrFields>, $_<kind>}), :with(&[eqv])) -> $t
     { my $ty = $t<ctorsOrFields>[0]<type>;
       my $typeclass = $typeclasses{$t<kind>};
       say "let extra_info__{$ty}__$typeclass : $ty extra_info__$typeclass = {tc $typeclass}.$ty;;";

src/stages/adt_generator/generic.ml

@@ -10,14 +10,35 @@ module BlahBluh = struct
   type 'state generic_continue_fold = ('state generic_continue_fold_node) StringMap.t;;
 end
 
-module Adt_info (M : sig type ('in_state , 'out_state , 'adt_info_node_instance_info) fold_config end) = struct
+module Adt_info (M : sig type ('in_state , 'out_state , 'adt_info_node_instance_info) fold_config;; type whatever;; type make_poly;; end) = struct
   type kind =
-  | Record
-  | Variant
-  | Poly of string
+  | RecordType of record_type
+  | VariantType of variant_type
+  | PolyType of poly_type
 
-  type ('in_state , 'out_state) record_instance = {
-    fields : ('in_state , 'out_state) ctor_or_field_instance list;
+  and ctor_or_field =
+    {
+      name : string;
+      is_builtin : bool;
+      type_ : string;
+    }
+
+  and record_type = {
+    fields : ctor_or_field list;
+    make_record : (string , M.whatever) RedBlackTrees.PolyMap.t -> M.whatever option
+  }
+
+  and ('in_state , 'out_state) record_instance = {
+    field_instances : ('in_state , 'out_state) ctor_or_field_instance list;
+  }
+
+  and variant_type = {
+    constructors : constructor_type list;
+  }
+
+  and constructor_type = {
+    ctor : ctor_or_field;
+    make_ctor : M.whatever -> M.whatever option;
   }
 
   and ('in_state , 'out_state) constructor_instance = {
@@ -25,6 +46,11 @@ module Adt_info (M : sig type ('in_state , 'out_state , 'adt_info_node_instance_
     variant : ctor_or_field list
   }
 
+  and poly_type = {
+    poly_name : string;
+    make_poly : M.make_poly;
+  }
+
   and ('in_state , 'out_state) poly_instance = {
     poly : string;
     arguments : string list;
@@ -41,13 +67,6 @@ module Adt_info (M : sig type ('in_state , 'out_state , 'adt_info_node_instance_
     instance_kind : ('in_state , 'out_state) kind_instance;
   }
 
-  and ctor_or_field =
-    {
-      name : string;
-      is_builtin : bool;
-      type_ : string;
-    }
-
   and ('in_state , 'out_state) ctor_or_field_instance =
     {
       cf : ctor_or_field;
@@ -59,11 +78,10 @@ module Adt_info (M : sig type ('in_state , 'out_state , 'adt_info_node_instance_
     {
       kind : kind;
       declaration_name : string;
-      ctors_or_fields : ctor_or_field list;
     }
 
   (* TODO: rename things a bit in this file. *)
-  and adt = node list
+  and adt = (string, node) RedBlackTrees.PolyMap.t
   and ('in_state , 'out_state) node_instance_info = {
     adt           : adt ;
     node_instance : ('in_state , 'out_state) instance ;

src/stages/common/ast_common.ml

@@ -3,3 +3,4 @@ include Types
 module Types = Types
 module PP = PP
 module Helpers = Helpers
+module Debug = Debug

src/stages/common/debug.ml

@@ -0,0 +1,2 @@
+let debug_new_typer = false
+let json_new_typer = false

src/stages/common/types.ml

@@ -52,7 +52,6 @@ end
 module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct
   open PARAMETER
 
-  type michelson_annotation = string
 
   type type_content =
     | T_sum of ctor_content constructor_map

src/stages/ligo_interpreter/PP.ml

@@ -34,7 +34,7 @@ let rec pp_value : value -> string = function
 let pp_env : env -> unit = fun env ->
   let () = Format.printf "{ #elements : %i\n" @@ Env.cardinal env in
   let () = Env.iter (fun var v ->
-    Format.printf "\t%s -> %s\n" (Var.to_name var) (pp_value v))
+    Format.printf "\t%a -> %s\n" Var.pp var (pp_value v))
   env in
   let () = Format.printf "\n}\n" in
   ()

src/stages/typesystem/core.ml

@@ -27,8 +27,10 @@ type type_variable = Ast_typed.type_variable
 type type_expression = Ast_typed.type_expression
 
 (* generate a new type variable and gave it an id *)
-let fresh_type_variable : ?name:string -> unit -> type_variable =
-    Var.fresh
+let fresh_type_variable : ?name:string -> unit -> type_variable = fun ?name () ->
+  let fresh_name = Var.fresh ?name () in
+  let () = (if Ast_typed.Debug.debug_new_typer && false then Printf.printf "Generated variable %s\n%!%s\n%!" (Var.debug fresh_name) (Printexc.get_backtrace ())) in
+  fresh_name
 
 let type_expression'_of_simple_c_constant : constant_tag * type_expression list -> Ast_typed.type_content option = fun (c, l) ->
   match c, l with

src/stages/typesystem/misc.ml

@@ -96,9 +96,9 @@ module Substitution = struct
       | Ast_core.T_constant constant ->
          ok @@ Ast_core.T_constant constant
 
-    and s_abstr_type_expression : (Ast_core.type_expression,_) w = fun ~substs {type_content;location;type_meta} ->
-      let%bind type_content = s_abstr_type_content ~substs type_content in
-      ok @@ Ast_core.{type_content;location;type_meta}
+    and s_abstr_type_expression : (Ast_core.type_expression,_) w = fun ~substs {content;sugar;location} ->
+      let%bind content = s_abstr_type_content ~substs content in
+      ok @@ (Ast_core.{content;sugar;location} : Ast_core.type_expression)
 
     and s_type_expression : (T.type_expression,_) w = fun ~substs { type_content; location; type_meta } ->
       let%bind type_content = s_type_content ~substs type_content in

src/stages/typesystem/solver_types.ml

@@ -15,12 +15,14 @@ type ('old_constraint_type , 'selector_output ) propagator_heuristic = {
   selector          : ('old_constraint_type, 'selector_output) selector ;
   (* constraint propagation: (buch of constraints) → (new constraints * assignments) *)
   propagator        : 'selector_output propagator ;
+  printer           : Format.formatter -> 'selector_output -> unit ;
   comparator        : 'selector_output -> 'selector_output -> int ;
 }
 
 type ('old_constraint_type , 'selector_output ) propagator_state = {
   selector          : ('old_constraint_type, 'selector_output) selector ;
   propagator        : 'selector_output propagator ;
+  printer           : Format.formatter -> 'selector_output -> unit ;
   already_selected  : 'selector_output Set.t;
 }
 
@@ -37,6 +39,38 @@ type typer_state = {
   already_selected_and_propagators : ex_propagator_state list ;
 }
 
+open Format
+open PP_helpers
+
+let pp_already_selected = fun printer ppf set ->
+  let lst = (RedBlackTrees.PolySet.elements set) in
+    Format.fprintf ppf "Set [@,@[<hv 2> %a @]@,]" (list_sep printer (fun ppf () -> fprintf ppf " ;@ ")) lst
+
+let pp_ex_propagator_state = fun ppf (Propagator_state { selector ; propagator ; printer ; already_selected }) ->
+  ignore ( selector, propagator );
+  Format.fprintf ppf "{ selector = (* OCaml function *); propagator = (* OCaml function *); already_selected = %a }"
+  (pp_already_selected printer) already_selected
+
+let pp_typer_state = fun ppf ({ structured_dbs; already_selected_and_propagators } : typer_state) ->
+  Format.fprintf ppf "{ structured_dbs = %a ; already_selected_and_propagators = [ %a ] }"
+    Ast_typed.PP_generic.structured_dbs structured_dbs
+    (list_sep pp_ex_propagator_state (fun ppf () -> fprintf ppf " ;@ ")) already_selected_and_propagators
+
+
+let json_already_selected = fun printer ppf set ->
+  let lst = (RedBlackTrees.PolySet.elements set) in
+    Format.fprintf ppf "[ \"Set\" %a ]" (list_sep printer (fun ppf () -> fprintf ppf " , ")) lst
+
+let json_ex_propagator_state = fun ppf (Propagator_state { selector; propagator; printer ; already_selected }) ->
+  ignore (selector,propagator);
+  Format.fprintf ppf "{ \"selector\": \"OCaml function\"; \"propagator\": \"OCaml function\"; \"already_selected\": %a }"
+  (json_already_selected printer) already_selected
+
+let json_typer_state = fun ppf ({ structured_dbs; already_selected_and_propagators } : typer_state) ->
+  Format.fprintf ppf "{ \"structured_dbs\": %a ; \"already_selected_and_propagators\": [ %a ] }"
+    Ast_typed.PP_json.structured_dbs structured_dbs
+    (list_sep json_ex_propagator_state (fun ppf () -> fprintf ppf " , ")) already_selected_and_propagators
+
 (* state+list monad *)
 type ('state, 'elt) state_list_monad = { state: 'state ; list : 'elt list }
 let lift_state_list_monad ~state ~list = { state ; list }

src/test/adt_generator/amodule_utils.ml

@@ -12,3 +12,10 @@ let fold_map__option continue state v =
   match v with
     Some x -> continue state x
   | None -> ok None
+
+let make__list f l =
+  List.fold_right
+    (fun elt acc -> match acc, f elt with
+         Some acc, Some x -> Some (x :: acc)
+       | _ -> None)
+    l (Some [])

src/test/adt_generator/use_a_fold.ml

@@ -61,14 +61,13 @@ let _noi : (int, _) fold_map_config__Amodule = no_op (* (fun _ -> ()) *)
 let _nob : (bool, _) fold_map_config__Amodule = no_op (* (fun _ -> ()) *)
 
 type no_state = NoState
-let () =
-  let some_root : root = A [ { a1 = X (A [ { a1 = X (B [ 1 ; 2 ; 3 ]) ; a2 = W () } ]) ; a2 = Z (W ()) } ] in
+let to_string some_root =
   let op : ('i, 'o) Generated_fold.fold_config = {
     generic = (fun NoState info ->
         match info.node_instance.instance_kind with
-        | RecordInstance { fields } ->
-           false, "{ " ^ String.concat " ; " (List.map (fun (fld : ('xi , 'xo) Adt_info.ctor_or_field_instance) -> fld.cf.name ^ " = " ^ snd (fld.cf_continue NoState)) fields) ^ " }"
-        | VariantInstance { constructor={ cf = { name; is_builtin=_; type_=_ }; cf_continue; cf_new_fold=_ }; variant=_ } ->
+        | RecordInstance { field_instances } ->
+          false, "{ " ^ String.concat " ; " (List.map (fun (fld : ('xi , 'xo) Adt_info.ctor_or_field_instance) -> fld.cf.name ^ " = " ^ snd (fld.cf_continue NoState)) field_instances) ^ " }"
+        | VariantInstance { constructor={ cf = { name; is_builtin=_; type_=_; }; cf_continue; cf_new_fold=_ }; variant=_ } ->
           (match cf_continue NoState with
            | true,  arg -> true, name ^ " (" ^ arg ^ ")"
            | false, arg -> true, name ^ " "  ^ arg)
@@ -87,8 +86,50 @@ let () =
      * ); *)
   } in
   let (_ , state) = Generated_fold.fold__root op NoState some_root in
+  state
+
+let () =
+  let some_root : root = A [ { a1 = X (A [ { a1 = X (B [ 1 ; 2 ; 3 ]) ; a2 = W () } ]) ; a2 = Z (W ()) } ] in
   let expected = "A [ { a1 = X (A [ { a1 = X (B [ 1 ; 2 ; 3 ]) ; a2 = W () } ]) ; a2 = Z (W ()) } ]" in
+  let state = to_string some_root in
   if String.equal state expected; then
     ()
   else
     failwith (Printf.sprintf "Test failed: expected\n  %s\n but got\n  %s" expected state)
+
+(* Test generic creation of nodes *)
+let () =
+  let i = whole_adt_info () in
+  let dynamic =
+    match RedBlackTrees.PolyMap.find_opt "rootB" i with
+    | Some { kind = PolyType { poly_name = _; make_poly }; declaration_name = _ } ->
+      (match make_poly with
+         Make_List mk ->
+         match mk [ Whatever_Int 42 ; Whatever_Int 43 ] with
+           Some l ->
+           (match RedBlackTrees.PolyMap.find_opt "root" i with
+              Some { kind = VariantType { constructors }; declaration_name = _ } ->
+              (* TODO: use a PolyMap.t *)
+              let { ctor = _ ; make_ctor } = List.find (fun { ctor = { name; is_builtin = _; type_ = _ }; make_ctor = _ } -> String.equal name "B") constructors in
+              let _ =
+                (match l with
+                 | Whatever_RootB _ -> () | _ -> failwith "whoops")
+              in
+              (match make_ctor l with (* Wrap the int list with the B constructor *)
+                 Some b -> b
+               | None -> failwith "Couldn't create instance of the B constructor, did you supply the right argument type?")
+            | Some { kind = _ ; _ } -> failwith "unexpected node info for root: wrong kind !!!"
+            | None -> failwith "can't find node info for root !!!")
+         | None -> failwith "Couldn't create list, did you supply the wrong element type?"
+         (* | _ -> failwith "unexpected maker function for rootB: expected rootB to be a list !!!" *)
+      )
+    | Some { kind = _ ; _ } -> failwith "unexpected node info for rootB: wrong kind !!!"
+    | None -> failwith "can't find node info for rootB !!!"
+  in
+  (match dynamic with
+     Whatever_Root root ->
+     (match root with
+        B [ 42 ; 43 ] -> () (* Victory, we created the expected value *)
+      | _ -> failwith ("Incorrect value " ^ to_string root))
+   | _ -> failwith "Incorrect result type: expected a dynamically-typed root, but got something else")
+

src/test/coase_tests.ml

@@ -221,10 +221,10 @@ let sell () =
     in
     let make_expecter : int -> Ast_core.expression -> (unit,_) result = fun n result ->
       let%bind (ops , storage) = trace_option (test_internal __LOC__) @@
-        Ast_core.get_e_pair result.expression_content in
+        Ast_core.get_e_pair result.content in
       let%bind () =
         let%bind lst = trace_option (test_internal __LOC__) @@
-          Ast_core.get_e_list ops.expression_content in
+          Ast_core.get_e_list ops.content in
           Assert.assert_list_size (test_internal __LOC__) lst 1 in
       let expected_storage =
         let cards = List.hds @@ cards_ez first_owner n in

src/test/contracts/expected/FA1.2.ligo.expected

@@ -31,10 +31,8 @@ type getBalance is
 type getTotalSupply is record [callback : contract (nat)]
 
 type action is
-    Transfer of transfer
-  | Approve of approve
-  | GetAllowance of getAllowance
-  | GetBalance of getBalance
+    Transfer of transfer | Approve of approve
+  | GetAllowance of getAllowance | GetBalance of getBalance
   | GetTotalSupply of getTotalSupply
 
 function transfer (const p : transfer; const s : storage)

src/test/contracts/expected/FA1.2.mligo.expected

@@ -24,10 +24,8 @@ type getBalance = {owner : address; callback : nat contract}
 type getTotalSupply = {callback : nat contract}
 
 type action =
-  Transfer of transfer
-| Approve of approve
-| GetAllowance of getAllowance
-| GetBalance of getBalance
+  Transfer of transfer | Approve of approve
+| GetAllowance of getAllowance | GetBalance of getBalance
 | GetTotalSupply of getTotalSupply
 
 let transfer (p, s : transfer * storage)
@@ -42,19 +40,19 @@ let transfer (p, s : transfer * storage)
                 s.allowances
         with
           Some value -> value
-        | None -> 0n
-      in if (authorized_value < p.value)
+        | None -> 0n in
+      if (authorized_value < p.value)
       then (failwith "Not Enough Allowance" : allowances)
       else
         Big_map.update
           (Tezos.sender, p.address_from)
           (Some (abs (authorized_value - p.value)))
-             s.allowances
-  in let sender_balance =
+          s.allowances in
+  let sender_balance =
     match Big_map.find_opt p.address_from s.tokens with
       Some value -> value
-       | None -> 0n
-     in if (sender_balance < p.value)
+    | None -> 0n in
+  if (sender_balance < p.value)
   then
     (failwith "Not Enough Balance"
      : operation list * storage)
@@ -63,21 +61,19 @@ let transfer (p, s : transfer * storage)
       Big_map.update
         p.address_from
         (Some (abs (sender_balance - p.value)))
-              s.tokens
-          in let receiver_balance =
-               match Big_map.find_opt p.address_to s.tokens
-               with
+        s.tokens in
+    let receiver_balance =
+      match Big_map.find_opt p.address_to s.tokens with
         Some value -> value
-               | None -> 0n
-             in let new_tokens =
+      | None -> 0n in
+    let new_tokens =
       Big_map.update
         p.address_to
         (Some (receiver_balance + p.value))
-                    new_tokens
-                in ([] : operation list),
+        new_tokens in
+    ([] : operation list),
     {s with
-                     tokens = new_tokens;
-                     allowances = new_allowances}
+      tokens = new_tokens; allowances = new_allowances}
 
 let approve (p, s : approve * storage)
 : operation list * storage =
@@ -87,8 +83,8 @@ let approve (p, s : approve * storage)
             s.allowances
     with
       Some value -> value
-    | None -> 0n
-  in if previous_value > 0n && p.value > 0n
+    | None -> 0n in
+  if previous_value > 0n && p.value > 0n
   then
     (failwith "Unsafe Allowance Change"
      : operation list * storage)
@@ -97,8 +93,8 @@ let approve (p, s : approve * storage)
       Big_map.update
         (p.spender, Tezos.sender)
         (Some (p.value))
-           s.allowances
-       in ([] : operation list),
+        s.allowances in
+    ([] : operation list),
     {s with
       allowances = new_allowances}
 
@@ -108,24 +104,24 @@ let getAllowance (p, s : getAllowance * storage)
     match Big_map.find_opt (p.owner, p.spender) s.allowances
     with
       Some value -> value
-    | None -> 0n
-  in let op = Tezos.transaction value 0mutez p.callback
-     in ([op], s)
+    | None -> 0n in
+  let op = Tezos.transaction value 0mutez p.callback in
+  ([op], s)
 
 let getBalance (p, s : getBalance * storage)
 : operation list * storage =
   let value =
     match Big_map.find_opt p.owner s.tokens with
       Some value -> value
-    | None -> 0n
-  in let op = Tezos.transaction value 0mutez p.callback
-     in ([op], s)
+    | None -> 0n in
+  let op = Tezos.transaction value 0mutez p.callback in
+  ([op], s)
 
 let getTotalSupply (p, s : getTotalSupply * storage)
 : operation list * storage =
-  let total = s.total_amount
-  in let op = Tezos.transaction total 0mutez p.callback
-     in ([op], s)
+  let total = s.total_amount in
+  let op = Tezos.transaction total 0mutez p.callback in
+  ([op], s)
 
 let main (a, s : action * storage) =
   match a with

src/test/contracts/expected/address.mligo.expected

@@ -1,3 +1,3 @@
 let main (p : key_hash) =
-  let c : unit contract = Tezos.implicit_account p
-  in Tezos.address c
+  let c : unit contract = Tezos.implicit_account p in
+  Tezos.address c

src/test/contracts/expected/amount_lambda.mligo.expected

@@ -1,6 +1,6 @@
 let f1 (x : unit) : unit -> tez =
-  let amt : tez = Current.amount
-  in fun (x : unit) -> amt
+  let amt : tez = Current.amount in
+  fun (x : unit) -> amt
 
 let f2 (x : unit) : unit -> tez =
   fun (x : unit) -> Current.amount

src/test/contracts/expected/assert.mligo.expected

@@ -1,3 +1,3 @@
 let main (p, s : bool * unit) =
-  let u : unit = assert p
-  in ([] : operation list), s
+  let u : unit = assert p in
+  ([] : operation list), s

src/test/contracts/expected/attributes.mligo.expected

@@ -1,8 +1,8 @@
 let x = 1 [@@inline]
 
 let foo (a : int) : int =
-  (let test = 2 + a [@@inline]
-   in test) [@@inline]
+  (let test = 2 + a [@@inline] in
+   test) [@@inline]
 
 let y = 1 [@@inline][@@other]
 
@@ -10,5 +10,5 @@ let bar (b : int) : int =
   let test = fun (z : int) -> 2 + b + z
     [@@inline]
     [@@foo]
-    [@@bar]
-  in test b
+    [@@bar] in
+  test b

src/test/contracts/expected/big_map.mligo.expected

@@ -18,5 +18,5 @@ let map1 : foo = Big_map.literal [(23, 0); (42, 0)]
 let map1 : foo = Big_map.literal [(23, 0); (42, 0)]
 
 let mutimaps (m : foo) (n : foo) : foo =
-  let bar : foo = Big_map.update 42 (Some 0) m
-  in Big_map.update 42 (get bar) n
+  let bar : foo = Big_map.update 42 (Some 0) m in
+  Big_map.update 42 (get bar) n

src/test/contracts/expected/bytes_unpack.mligo.expected

@@ -1,11 +1,11 @@
 let id_string (p : string) : string option =
-  let packed : bytes = Bytes.pack p
-  in (Bytes.unpack packed : string option)
+  let packed : bytes = Bytes.pack p in
+  (Bytes.unpack packed : string option)
 
 let id_int (p : int) : int option =
-  let packed : bytes = Bytes.pack p
-  in (Bytes.unpack packed : int option)
+  let packed : bytes = Bytes.pack p in
+  (Bytes.unpack packed : int option)
 
 let id_address (p : address) : address option =
-  let packed : bytes = Bytes.pack p
-  in (Bytes.unpack packed : address option)
+  let packed : bytes = Bytes.pack p in
+  (Bytes.unpack packed : address option)

src/test/contracts/expected/closure.mligo.expected

@@ -1,5 +1,5 @@
 let test (k : int) : int =
-  let j : int = k + 5
-  in let close : int -> int = fun (i : int) -> i + j
-     in let j : int = 20
-        in close 20
+  let j : int = k + 5 in
+  let close : int -> int = fun (i : int) -> i + j in
+  let j : int = 20 in
+  close 20