diff --git a/AST2.ml b/AST2.ml
index e0a8d9ffd..2b255f53b 100644
--- a/AST2.ml
+++ b/AST2.ml
@@ -2,98 +2,99 @@
 
 exception TODO of string
 
+module I = AST
+
 open Region
 
-module In = AST
+module SMap = Map.Make(String)
 
-module SMap = Utils.String.Map
+module O = struct
+  type type_name = string
+  type var_name = string
 
-module Out =
-  struct
-    type type_name = string
-    type variable  = string
+  type pattern =
+    PVar    of var_name
+  | PWild
+  | PInt    of Z.t
+  | PBytes  of MBytes.t
+  | PString of string
+  | PUnit
+  | PFalse
+  | PTrue
+  | PNone
+  | PSome   of pattern
+  | PCons   of pattern * pattern
+  | PNull
+  | PTuple  of pattern list
 
-    type ast = {
-      types        : type_decl list;
-      storage      : typed_var;
-      operations   : typed_var;
-      declarations : decl list;
-      prev         : In.t;
+  type type_expr =
+    Prod     of type_expr list
+  | Sum      of (type_name * type_expr) list
+  | Record   of (type_name * type_expr) list
+  | TypeApp  of type_name * (type_expr list)
+  | Function of { args: type_expr list; ret: type_expr }
+  | Ref      of type_expr
+  | Unit
+  | Int
+  | TODO
+
+  type typed_var = { name:var_name; ty:type_expr }
+
+  type type_decl = { name:string; ty:type_expr }
+
+  type expr =
+    App      of { operator: operator; arguments: expr list }
+  | Var of var_name
+  | Constant of constant
+  | Lambda   of lambda
+
+  and decl = { name:var_name; ty:type_expr; value: expr }
+
+  and lambda = {
+      parameters:   type_expr SMap.t;
+      declarations: decl list;
+      instructions: instr list;
+      result:       expr;
     }
 
-   and typed_var = {name: variable; ty: type_expr}
-   and type_decl = {name: variable; ty: type_expr}
+  and operator =
+    Or | And | Lt | Leq | Gt | Geq | Equal | Neq | Cat | Cons | Add | Sub | Mult | Div | Mod
+    | Neg | Not
+    | Tuple | Set | List
+    | MapLookup
+    | Function of string
 
-   and decl = {name: variable; ty: type_expr; value: expr}
+  and constant =
+    Unit | Int of Z.t | String of string | Bytes of MBytes.t | False | True
+    | Null of type_expr | EmptySet of type_expr | CNone of type_expr
 
-   and type_expr =
-     Prod     of type_expr list
-   | Sum      of (type_name * type_expr) list
-   | Record   of (type_name * type_expr) list
-   | TypeApp  of type_name * type_expr list
-   | Function of {args: type_expr list; ret: type_expr}
-   | Ref      of type_expr
-   | Unit
-   | Int
-   | TODO
+  and instr =
+    Assignment    of { name: var_name; value: expr }
+  | While         of { condition: expr; body: instr list }
+  | ForCollection of { list: expr; key: var_name; value: var_name option; body: instr list }
+  | If            of { condition: expr; ifso: instr list; ifnot: instr list }
+  | Match         of { expr: expr; cases: (pattern * instr list) list }
+  | DropUnit      of expr       (* expr returns unit, drop the result. *)
+  | Fail          of { expr: expr }
 
-   and expr =
-     App      of {operator: operator; arguments: expr list}
-   | Variable of variable
-   | Constant of constant
-   | Lambda   of lambda
+  type ast = {
+      types           : type_decl list;
+      storage_decl    : typed_var;
+      operations_decl : typed_var;
+      declarations    : decl list;
+    }
+end
 
-   and lambda = {
-     parameters   : type_expr SMap.t;
-     declarations : decl list;
-     instructions : instr list;
-     result       : expr
-   }
-
-   and operator = Add | Sub | Lt | Gt | Function of string
-
-   and constant =
-     Unit
-   | Int of Z.t
-
-   and instr =
-     Assignment    of { name: variable; value: expr }
-   | While         of { condition: expr; body: instr list }
-   | ForCollection of { list: expr; key: variable;
-                        value: variable option;
-                        body: instr list }
-   | If            of { condition: expr; ifso: instr list; ifnot: instr list }
-   | Match         of { expr: expr; cases: (pattern * instr list) list }
-   | DropUnit      of expr       (* expr returns unit, drop the result. *)
-   | Fail          of { expr: expr }
-   | Null
-
-   and pattern =
-     PVar    of variable
-   | PWild
-   | PInt    of Z.t
-   | PBytes  of MBytes.t
-   | PString of string
-   | PUnit
-   | PFalse
-   | PTrue
-   | PNone
-   | PSome   of pattern
-   | Cons    of pattern * pattern
-   | PTuple  of pattern list
-  end
-
-let map f l = List.(rev_map f l |> rev)
-
-(* TODO: check that List.to_seq, SMap.of_seq are not broken
+(* open Sanity: *)
+let (|>) v f = f v       (* pipe f to v *)
+let (@@) f v = f v       (* apply f on v *)
+let (@.) f g x = f (g x) (* compose *)
+let map f l = List.rev (List.rev_map f l)
+(* TODO: check that List.to_seq, List.append and SMap.of_seq are not broken
    (i.e. check that they are tail-recursive) *)
-
 let append_map f l = map f l |>  List.flatten
-
-let append l = List.(rev l |> rev_append)
-
-let list_to_map l = l |> List.to_seq |> SMap.of_seq  (* Why lazy ? *)
-
+let append l1 l2 = List.append l1 l2
+let list_to_map l = l |> List.to_seq |> SMap.of_seq
 let fold_map f a l =
   let f (acc, l) elem =
     let acc', elem' = f acc elem
@@ -111,165 +112,230 @@ let s_sepseq : ('a,'sep) Utils.sepseq -> 'a list =
     None         -> []
   | Some nsepseq -> s_nsepseq nsepseq
 
-let s_name ({value=name; region}: string reg) =
-  ignore region; name
+let s_name {value=name; region} : O.var_name =
+  let () = ignore (region) in
+  name
 
-let rec s_cartesian {value=sequence; region} : Out.type_expr =
-  let () = ignore region in
+let rec s_cartesian {value=sequence; region} : O.type_expr =
+  let () = ignore (region) in
   Prod (map s_type_expr (s_nsepseq sequence))
 
-and s_sum_type {value=sequence; region} : Out.type_expr =
-  let () = ignore region in
-  let _todo = sequence in
-(*  Sum (map s_type_expr (s_nsepseq sequence)) *)
-  TODO
+and s_sum_type {value=sequence; region} : O.type_expr =
+  let () = ignore (region) in
+  Sum (map s_variant (s_nsepseq sequence))
 
-and s_record_type {value=(kwd_record, field_decls, kwd_end); region} : Out.type_expr =
+and s_variant {value=(constr, kwd_of, cartesian); region} =
+  let () = ignore (kwd_of,region) in
+  (s_name constr, s_cartesian cartesian)
+
+and s_record_type {value=(kwd_record, field_decls, kwd_end); region} : O.type_expr =
   let () = ignore (kwd_record,region,kwd_end) in
-  let _todo = (* s_field_decls *) field_decls in
-  TODO
+  Record (map s_field_decl (s_nsepseq field_decls))
 
-and s_type_app {value=node; region} : Out.type_expr =
-  let () = ignore region in
-  let _todo = node in
-  TODO
-  (* let type_name, type_tuple = node in *)
-  (* s_var        type_name; *)
-  (* s_type_tuple type_tuple *)
+and s_field_decl {value=(var, colon, type_expr); region} =
+  let () = ignore (colon,region) in
+  (s_name var, s_type_expr type_expr)
 
-and s_par_type {value=node; region} : Out.type_expr =
-  let () = ignore region in
-  let _todo = node in
-  TODO
+and s_type_app {value=(type_name,type_tuple); region} : O.type_expr =
+  let () = ignore (region) in
+  TypeApp (s_name type_name, s_type_tuple type_tuple)
 
-and s_var {region; value=lexeme} : Out.type_expr =
-  let () = ignore region in
-  let _todo = lexeme in
-  TODO
+and s_type_tuple ({value=(lpar, sequence, rpar); region} : (I.type_name, I.comma) Utils.nsepseq I.par) : O.type_expr list =
+  let () = ignore (lpar,rpar,region) in
+  (* TODO: the grammar should allow any type expr, not just type_name in the tuple elements *)
+  map s_type_expr (map (fun a -> I.TAlias a) (s_nsepseq sequence))
 
-(*  let lpar, type_expr, rpar = node in
-  s_token     lpar "(";
-  s_type_expr type_expr;
-  s_token     rpar ")"*)
+and s_par_type {value=(lpar, type_expr, rpar); region} : O.type_expr =
+  let () = ignore (lpar,rpar,region) in
+  s_type_expr type_expr
 
-and s_type_expr : In.type_expr -> Out.type_expr = function
+and s_type_alias name : O.type_expr =
+  let () = ignore () in
+  TypeApp (s_name name, [])
+
+and s_type_expr : I.type_expr -> O.type_expr = function
   Prod    cartesian   -> s_cartesian   cartesian
 | Sum     sum_type    -> s_sum_type    sum_type
 | Record  record_type -> s_record_type record_type
 | TypeApp type_app    -> s_type_app    type_app
 | ParType par_type    -> s_par_type    par_type
-| TAlias  type_alias  -> s_var         type_alias
+| TAlias  type_alias  -> s_type_alias  type_alias
 
 
-let s_type_decl In.{value={kwd_type;name;kwd_is;type_expr;terminator}; region} : Out.type_decl =
+let s_type_decl I.{value={kwd_type;name;kwd_is;type_expr;terminator}; region} : O.type_decl =
   let () = ignore (kwd_type,kwd_is,terminator,region) in
-  Out.{ name = s_name name; ty = s_type_expr type_expr }
+  O.{ name = s_name name; ty = s_type_expr type_expr }
 
-let s_storage_decl In.{value={kwd_storage; store_type; terminator}; region} : Out.typed_var =
-  let () = ignore (kwd_storage,terminator,region) in
-  Out.{ name = "storage"; ty = s_type_expr store_type }
+let s_storage_decl I.{value={kwd_storage; name; colon; store_type; terminator}; region} : O.typed_var =
+  let () = ignore (kwd_storage,colon,terminator,region) in
+  O.{ name = s_name name; ty = s_type_expr store_type }
 
-let s_operations_decl In.{value={kwd_operations;op_type;terminator}; region} : Out.typed_var =
-  let () = ignore (kwd_operations,terminator,region) in
-  Out.{ name = "operations"; ty = s_type_expr op_type }
+let s_operations_decl I.{value={kwd_operations;name;colon;op_type;terminator}; region} : O.typed_var =
+  let () = ignore (kwd_operations,colon,terminator,region) in
+  O.{ name = s_name name; ty = s_type_expr op_type }
 
-let s_expr : In.expr -> Out.expr = function
-  | _ -> raise (TODO "simplify expressions")
+let s_empty_list {value=(l, (lbracket, rbracket, colon, type_expr), r); region} : O.expr =
+  let () = ignore (l, lbracket, rbracket, colon, r, region) in
+  Constant (Null (s_type_expr type_expr))
 
-let s_case : In.case -> Out.pattern * (Out.instr list) = function
+let s_empty_set {value=(l, (lbrace, rbrace, colon, type_expr), r); region} : O.expr =
+  let () = ignore (l, lbrace, rbrace, colon, r, region) in
+  Constant (EmptySet (s_type_expr type_expr))
+
+let s_none {value=(l, (c_None, colon, type_expr), r); region} : O.expr =
+  let () = ignore (l, c_None, colon, r, region) in
+  Constant (CNone (s_type_expr type_expr))
+
+let rec bin l operator r = O.App { operator; arguments = [s_expr l; s_expr r] }
+and     una operator v = O.App { operator; arguments = [s_expr v] }
+and s_expr : I.expr -> O.expr =
+  function
+    Or        {value=(l, bool_or, r);     region} -> let () = ignore (region, bool_or) in bin l Or    r
+  | And       {value=(l, bool_and, r);    region} -> let () = ignore (region,bool_and) in bin l And   r
+  | Lt        {value=(l, lt, r);          region} -> let () = ignore (region,      lt) in bin l Lt    r
+  | Leq       {value=(l, leq, r);         region} -> let () = ignore (region,     leq) in bin l Leq   r
+  | Gt        {value=(l, gt, r);          region} -> let () = ignore (region,      gt) in bin l Gt    r
+  | Geq       {value=(l, geq, r);         region} -> let () = ignore (region,     geq) in bin l Geq   r
+  | Equal     {value=(l, equal, r);       region} -> let () = ignore (region,   equal) in bin l Equal r
+  | Neq       {value=(l, neq, r);         region} -> let () = ignore (region,     neq) in bin l Neq   r
+  | Cat       {value=(l, cat, r);         region} -> let () = ignore (region,     cat) in bin l Cat   r
+  | Cons      {value=(l, cons, r);        region} -> let () = ignore (region,    cons) in bin l Cons  r
+  | Add       {value=(l, plus, r);        region} -> let () = ignore (region,    plus) in bin l Add   r
+  | Sub       {value=(l, minus, r);       region} -> let () = ignore (region,   minus) in bin l Sub   r
+  | Mult      {value=(l, times, r);       region} -> let () = ignore (region,   times) in bin l Mult  r
+  | Div       {value=(l, slash, r);       region} -> let () = ignore (region,   slash) in bin l Div   r
+  | Mod       {value=(l, kwd_mod, r);     region} -> let () = ignore (region, kwd_mod) in bin l Mod   r
+  | Neg       {value=(minus, expr);       region} -> let () = ignore (region,   minus) in una Neg expr
+  | Not       {value=(kwd_not, expr);     region} -> let () = ignore (region, kwd_not) in una Not expr
+  | Int       {value=(lexeme, z);         region} -> let () = ignore (region,  lexeme) in Constant (Int z)
+  | Var       {value=lexeme;              region} -> let () = ignore (region)          in Var lexeme
+  | String    {value=s;                   region} -> let () = ignore (region)          in Constant (String s)
+  | Bytes     {value=(lexeme, mbytes);    region} -> let () = ignore (region,  lexeme) in Constant (Bytes mbytes)
+  | False     c_False                             -> let () = ignore (c_False)         in Constant (False)
+  | True      c_True                              -> let () = ignore (c_True)          in Constant (True)
+  | Unit      c_Unit                              -> let () = ignore (c_Unit)          in Constant (Unit)
+  | Tuple     {value=(l,tuple,r);         region} -> let () = ignore (l,r,region)      in App { operator = Tuple; arguments = map s_expr (s_nsepseq tuple)}
+  | List      list                                -> s_list list
+  | EmptyList empty_list                          -> s_empty_list empty_list
+  | Set       set                                 -> s_set set
+  | EmptySet  empty_set                           -> s_empty_set empty_set
+  | NoneExpr  none_expr                           -> s_none none_expr
+  | FunCall   fun_call                            -> s_fun_call fun_call
+  | ConstrApp constr_app                          -> s_constr_app constr_app
+  | SomeApp   some_app                            -> s_some_app some_app
+  | MapLookUp map_lookup                          -> s_map_lookup map_lookup
+  | ParExpr   {value=(lpar,expr,rpar);    region} -> let () = ignore (lpar,rpar,region) in s_expr expr
+
+and s_map_lookup I.{value = {map_name; selector; index}; region} : O.expr =
+  let {value = lbracket, index_expr, rbracket; region=region2} = index in
+  let () = ignore (selector, lbracket, rbracket, region2, region) in
+  App { operator = MapLookup; arguments = [Var (s_name map_name); s_expr index_expr] }
+
+and s_some_app {value=(c_Some, {value=(l,arguments,r); region=region2}); region} : O.expr =
+  let () = ignore (c_Some,l,r,region2,region) in
+  match s_nsepseq arguments with
+    [] -> Constant Unit
+  | [a] -> s_expr a
+  | l -> App { operator = Tuple; arguments = map s_expr l }
+
+and s_list {value=(l, list, r); region} : O.expr =
+  let () = ignore (l, r, region) in
+  App { operator = List; arguments = map s_expr (s_nsepseq list) }
+
+and s_set {value=(l, set, r); region} : O.expr =
+  let () = ignore (l, r, region) in
+  App { operator = Set; arguments = map s_expr (s_nsepseq set) }
+
+and s_case : I.case -> O.pattern * (O.instr list) = function
   | _ -> raise (TODO "simplify pattern matching cases")
 
-let s_const_decl In.{value; region} : Out.decl =
-  let In.{kwd_const; name; colon;
-          const_type; equal; init; terminator} = value in
+and s_const_decl I.{value={kwd_const;name;colon;const_type;equal;init;terminator}; region} : O.decl =
   let () = ignore (kwd_const,colon,equal,terminator,region) in
-  Out.{name  = s_name name;
-       ty    = s_type_expr const_type;
-       value = s_expr init}
+  O.{ name = s_name name; ty = s_type_expr const_type; value = s_expr init }
 
-let s_param_const {value=(kwd_const,variable,colon,type_expr); region} : string * Out.type_expr =
+and s_param_const {value=(kwd_const,variable,colon,type_expr); region} : string * O.type_expr =
   let () = ignore (kwd_const,colon,region) in
   s_name variable, s_type_expr type_expr
 
-let s_param_var {value=(kwd_var,variable,colon,type_expr); region} : string * Out.type_expr =
+and s_param_var {value=(kwd_var,variable,colon,type_expr); region} : string * O.type_expr =
   let () = ignore (kwd_var,colon,region) in
   s_name variable, s_type_expr type_expr
 
-let s_param_decl : In.param_decl -> string * Out.type_expr = function
+and s_param_decl : I.param_decl -> string * O.type_expr = function
     ParamConst p ->  s_param_const p
   | ParamVar p ->    s_param_var p
 
-let s_parameters ({value=(lpar,param_decl,rpar);region} : In.parameters) : (string * Out.type_expr) list =
+and s_parameters ({value=(lpar,param_decl,rpar);region} : I.parameters) : (string * O.type_expr) list =
   let () = ignore (lpar,rpar,region) in
   let l = (s_nsepseq param_decl) in
   map s_param_decl l
 
-let rec s_var_decl {value; region} : Out.decl =
-  let In.{kwd_var; name; colon;
-          var_type; ass; init; terminator} = value in
-  let () = ignore (kwd_var, colon, ass, terminator, region) in
-  Out.{name  = s_name name;
-       ty    = s_type_expr var_type;
-       value = s_expr init}
+and s_var_decl I.{value={kwd_var;name;colon;var_type;ass;init;terminator}; region} : O.decl =
+  let () = ignore (kwd_var,colon,ass,terminator,region) in
+  O.{
+      name = s_name name;
+      ty = s_type_expr var_type;
+      value = s_expr init
+  }
 
-and s_local_decl : In.local_decl -> Out.decl = function
+and s_local_decl : I.local_decl -> O.decl = function
   LocalLam   decl -> s_lambda_decl decl
 | LocalConst decl -> s_const_decl  decl
 | LocalVar   decl -> s_var_decl    decl
 
-and s_instructions ({value=sequence; region} : In.instructions) : Out.instr list =
-  let () = ignore region in
+and s_instructions ({value=sequence; region} : I.instructions) : O.instr list =
+  let () = ignore (region) in
   append_map s_instruction (s_nsepseq sequence)
 
-and s_instruction : In.instruction -> Out.instr list = function
+and s_instruction : I.instruction -> O.instr list = function
   Single instr -> s_single_instr instr
 |  Block block -> (s_block block)
 
-and s_conditional In.{kwd_if;test;kwd_then;ifso;kwd_else;ifnot} : Out.instr =
+and s_conditional I.{kwd_if;test;kwd_then;ifso;kwd_else;ifnot} : O.instr =
   let () = ignore (kwd_if,kwd_then,kwd_else) in
   If { condition = s_expr test; ifso = s_instruction ifso; ifnot = s_instruction ifnot }
 
-and s_match_instr In.{kwd_match;expr;kwd_with;lead_vbar;cases;kwd_end} : Out.instr =
+and s_match_instr I.{kwd_match;expr;kwd_with;lead_vbar;cases;kwd_end} : O.instr =
   let {value=cases;region} = cases in
   let () = ignore (kwd_match,kwd_with,lead_vbar,kwd_end,region) in
   Match { expr = s_expr expr; cases = map s_case (s_nsepseq cases) }
 
-and s_ass_instr {value=(variable,ass,expr); region} : Out.instr =
+and s_ass_instr {value=(variable,ass,expr); region} : O.instr =
   let () = ignore (ass,region) in
   Assignment { name = s_name variable; value = s_expr expr }
 
-and s_while_loop {value=(kwd_while, expr, block); region} : Out.instr list =
+and s_while_loop {value=(kwd_while, expr, block); region} : O.instr list =
   let () = ignore (kwd_while,region) in
   [While {condition = s_expr expr; body = s_block block}]
 
-and s_for_loop : In.for_loop -> Out.instr list = function
+and s_for_loop : I.for_loop -> O.instr list = function
   ForInt     for_int     -> s_for_int     for_int
 | ForCollect for_collect -> s_for_collect for_collect
 
-and s_for_int ({value={kwd_for;ass;down;kwd_to;bound;step;block}; region} : In.for_int reg) : Out.instr list =
+and s_for_int ({value={kwd_for;ass;down;kwd_to;bound;step;block}; region} : I.for_int reg) : O.instr list =
   let {value=(variable,ass_kwd,expr);region = ass_region} = ass in
   let () = ignore (kwd_for,ass_region,ass_kwd,kwd_to,region) in
   let name = s_name variable in
-  let condition, operator = match down with Some kwd_down -> ignore kwd_down; Out.Gt, Out.Sub
-                                          | None          ->                  Out.Lt, Out.Add in
+  let condition, operator = match down with Some kwd_down -> ignore kwd_down; O.Gt, O.Sub
+                                          | None          ->                  O.Lt, O.Add in
   let step = s_step step
   in [
       Assignment { name; value = s_expr expr };
       (* TODO: lift the declaration of the variable *)
       While {
           condition = App { operator = condition;
-                            arguments = [Variable name; s_expr bound] };
-          body = List.append (s_block block)
-                        [Out.Assignment { name;
+                            arguments = [Var name; s_expr bound] };
+          body = append (s_block block)
+                        [O.Assignment { name;
                                         value = App { operator;
-                                                      arguments = [Variable name; step]}}]
+                                                      arguments = [Var name; step]}}]
         }
     ]
 
-and s_for_collect ({value={kwd_for;var;bind_to;kwd_in;expr;block}; _} : In.for_collect reg) : Out.instr list =
+and s_for_collect ({value={kwd_for;var;bind_to;kwd_in;expr;block}; _} : I.for_collect reg) : O.instr list =
   let () = ignore (kwd_for,kwd_in) in
   [
-    Out.ForCollection {
+    O.ForCollection {
         list = s_expr expr;
         key = s_name var;
         value = s_bind_to bind_to;
@@ -277,31 +343,38 @@ and s_for_collect ({value={kwd_for;var;bind_to;kwd_in;expr;block}; _} : In.for_c
       }
   ]
 
-and s_step : (In.kwd_step * In.expr) option -> Out.expr = function
+and s_step : (I.kwd_step * I.expr) option -> O.expr = function
   Some (kwd_step, expr) -> let () = ignore (kwd_step) in s_expr expr
-| None -> Constant (Int Z.one)
+| None -> Constant (Int (Z.of_int 1))
 
-and s_bind_to : (In.arrow * In.variable) option -> Out.variable option = function
-    Some (arrow, variable) ->
-    let () = ignore arrow in Some (s_name variable)
-| None -> None
+and s_bind_to : (I.arrow * I.variable) option -> O.var_name option = function
+    Some (arrow, variable) -> let () = ignore (arrow) in Some (s_name variable)
+  | None -> None
 
-and s_loop : In.loop -> Out.instr list = function
+and s_loop : I.loop -> O.instr list = function
     While while_loop -> s_while_loop while_loop
   | For     for_loop -> s_for_loop for_loop
 
-and s_fun_call {value=(fun_name, arguments); region} : Out.expr =
-  let () = ignore region in
+and s_fun_call {value=(fun_name, arguments); region} : O.expr =
+  let () = ignore (region) in
   App { operator = Function (s_name fun_name); arguments = s_arguments arguments }
 
+and s_constr_app {value=(constr, arguments); region} : O.expr =
+  let () = ignore (region) in
+  App { operator = Function (s_name constr); arguments = s_arguments arguments }
+
 and s_arguments {value=(lpar, sequence, rpar); region} =
-  let () = ignore (lpar, rpar, region) in
+  let () = ignore (lpar,rpar,region) in
   map s_expr (s_nsepseq sequence);
 
-and s_fail ((kwd_fail, expr) : (In.kwd_fail * In.expr)) : Out.instr =
-  ignore kwd_fail; Fail {expr = s_expr expr}
+and s_fail ((kwd_fail, expr) : (I.kwd_fail * I.expr)) : O.instr =
+  let () = ignore (kwd_fail) in
+  Fail { expr = s_expr expr }
 
-and s_single_instr : In.single_instr -> Out.instr list = function
+
+
+
+and s_single_instr : I.single_instr -> O.instr list = function
   Cond     {value; _} -> [s_conditional value]
 | Match    {value; _} -> [s_match_instr value]
 | Ass      instr      -> [s_ass_instr instr]
@@ -311,13 +384,13 @@ and s_single_instr : In.single_instr -> Out.instr list = function
                          []
 | Fail     {value; _} -> [s_fail value]
 
-and s_block In.{value={opening;instr;terminator;close}; _} : Out.instr list =
+and s_block I.{value={opening;instr;terminator;close}; _} : O.instr list =
   let () = ignore (opening,terminator,close) in
   s_instructions instr
 
-and s_fun_decl In.{value={kwd_function;name;param;colon;ret_type;kwd_is;local_decls;block;kwd_with;return;terminator}; region} : Out.decl =
+and s_fun_decl I.{value={kwd_function;name;param;colon;ret_type;kwd_is;local_decls;block;kwd_with;return;terminator}; region} : O.decl =
   let () = ignore (kwd_function,colon,kwd_is,kwd_with,terminator,region) in
-  Out.{
+  O.{
       name = s_name name;
       ty = Function { args = map snd (s_parameters param); ret = s_type_expr ret_type };
       value = Lambda {
@@ -328,50 +401,70 @@ and s_fun_decl In.{value={kwd_function;name;param;colon;ret_type;kwd_is;local_de
                 }
   }
 
-and s_proc_decl In.{value={kwd_procedure;name;param;kwd_is;local_decls;block;terminator}; region} =
+and s_proc_decl I.{value={kwd_procedure;name;param;kwd_is;local_decls;block;terminator}; region} =
   let () = ignore (kwd_procedure,kwd_is,terminator,region) in
-  Out.{
+  O.{
       name = s_name name;
       ty = Function { args = map snd (s_parameters param); ret = Unit };
       value = Lambda {
                   parameters   = s_parameters param |> list_to_map;
                   declarations = map s_local_decl local_decls;
                   instructions = s_block block;
-                  result       = Out.Constant Out.Unit
+                  result       = O.Constant O.Unit
                 }
   }
 
-and s_lambda_decl : In.lambda_decl -> Out.decl = function
-  FunDecl   fun_decl -> s_fun_decl fun_decl
-| ProcDecl proc_decl -> s_proc_decl proc_decl
-| EntryDecl entry_decl -> failwith "TODO"
-
-let s_main_block (block: In.block reg) : Out.decl =
-  Out.{
-      name = "main";
-      ty = Function { args = []; ret = Unit };
+and s_entry_decl I.{value={kwd_entrypoint;name;param;kwd_is;local_decls;block;terminator}; region} =
+  let () = ignore (kwd_entrypoint,kwd_is,terminator,region) in
+  O.{
+      name = s_name name;
+      ty = Function { args = map snd (s_parameters param); ret = Unit };
       value = Lambda {
-                  parameters   = SMap.empty;
-                  declarations = [];
+                  parameters   = s_parameters param |> list_to_map;
+                  declarations = map s_local_decl local_decls;
                   instructions = s_block block;
-                  result       = Out.Constant Out.Unit
+                  result       = O.Constant O.Unit
                 }
   }
 
-let s_ast (ast : In.ast) : Out.ast =
-  let In.{types;constants;storage;operations;lambdas;block;eof} = ast in
-  let () = ignore (eof) in
-  Out.{
-      types        = map s_type_decl types;
-      storage      = s_storage_decl storage;
-      operations   = s_operations_decl operations;
-      declarations = List.flatten [(map s_const_decl  constants);
-                                   (map s_lambda_decl lambdas);
-                                   [s_main_block block]];
-      prev         = ast
+and s_lambda_decl : I.lambda_decl -> O.decl = function
+  FunDecl     fun_decl -> s_fun_decl fun_decl
+| EntryDecl entry_decl -> s_entry_decl entry_decl
+| ProcDecl   proc_decl -> s_proc_decl proc_decl
+
+type tmp_ast = {
+    types           : O.type_decl list;
+    storage_decl    : O.typed_var option;
+    operations_decl : O.typed_var option;
+    declarations    : O.decl list;
   }
 
 
+let s_declaration (ast : tmp_ast) : I.declaration -> tmp_ast = function
+    TypeDecl    t -> { ast with types           = (s_type_decl    t) :: ast.types }
+  | ConstDecl   c -> { ast with declarations    = (s_const_decl   c) :: ast.declarations }
+  | StorageDecl s -> { ast with storage_decl    = Some (s_storage_decl    s) }
+  | OpDecl      o -> { ast with operations_decl = Some (s_operations_decl o) }
+  | LambdaDecl  l -> { ast with declarations    = (s_lambda_decl  l) :: ast.declarations }
+
+let s_ast (ast : I.ast) : O.ast =
+  let I.{decl=(decl1,decls);eof} = ast in
+  let () = ignore (eof) in
+  let {types; storage_decl; operations_decl; declarations} =
+    List.fold_left s_declaration
+                   { types = [];
+                     storage_decl = None;
+                     operations_decl = None;
+                     declarations = [] }
+                   ( decl1 :: decls ) in
+  let storage_decl = match storage_decl with
+      Some x -> x
+    | None -> failwith "Missing storage declaration" in
+  let operations_decl = match operations_decl with
+      Some x -> x
+    | None -> failwith "Missing storage declaration"
+  in {types; storage_decl; operations_decl; declarations}
+
 
 
 
@@ -399,30 +492,6 @@ let s_ast (ast : In.ast) : Out.ast =
 (*          (compact region) lexeme *)
 (*          (Z.to_string abstract) *)
 
-(* and s_cartesian {value=sequence; _} = *)
-(*   s_nsepseq "*" s_type_expr sequence *)
-
-(* and s_variant {value=node; _} = *)
-(*   let constr, kwd_of, cartesian = node in *)
-(*   s_constr    constr; *)
-(*   s_token     kwd_of "of"; *)
-(*   s_cartesian cartesian *)
-
-(* and s_field_decls sequence = *)
-(*   s_nsepseq ";" s_field_decl sequence *)
-
-(* and s_field_decl {value=node; _} = *)
-(*   let var, colon, type_expr = node in *)
-(*   s_var       var; *)
-(*   s_token     colon ":"; *)
-(*   s_type_expr type_expr *)
-
-(* and s_type_tuple {value=node; _} = *)
-(*   let lpar, sequence, rpar = node in *)
-(*   s_token lpar "("; *)
-(*   s_nsepseq "," s_var sequence; *)
-(*   s_token rpar ")" *)
-
 
 (* and s_parameters {value=node; _} = *)
 (*   let lpar, sequence, rpar = node in *)
@@ -545,13 +614,6 @@ let s_ast (ast : In.ast) : Out.ast =
 (*   s_token c_Some "Some"; *)
 (*   s_tuple arguments *)
 
-(* and s_map_lookup {value=node; _} = *)
-(*   let {value = lbracket, expr, rbracket; _} = node.index in *)
-(*   s_var   node.map_name; *)
-(*   s_token node.selector "."; *)
-(*   s_token lbracket "["; *)
-(*   s_expr  expr; *)
-(*   s_token rbracket "]" *)
 
 (* and s_par_expr {value=node; _} = *)
 (*   let lpar, expr, rpar = node in *)
diff --git a/ParserMain.ml b/ParserMain.ml
index 9b2f79064..d6bff2efc 100644
--- a/ParserMain.ml
+++ b/ParserMain.ml
@@ -97,3 +97,15 @@ let () =
       let () = close_all () in
       print_error ~offsets EvalOpt.mode error
   | Sys_error msg -> Utils.highlight msg
+
+(* Temporary: force dune to build AST2.ml *)
+let () =
+  let open AST2 in
+  let _ = s_ast in
+  ()
+
+(* Temporary: force dune to build AST2.ml *)
+let () =
+  let open Typecheck2 in
+  let _ = temporary_force_dune in
+  ()
diff --git a/Typecheck2.ml b/Typecheck2.ml
new file mode 100644
index 000000000..7f1b5866c
--- /dev/null
+++ b/Typecheck2.ml
@@ -0,0 +1,104 @@
+[@@@warning "-30"]
+
+module SMap = Map.Make(String)
+
+module O = struct
+  type asttodo = [`TODO] (* occurrences of asttodo will point to some part of the original parser AST *)
+
+  type type_name = string
+  type var_name = { name: string; orig: asttodo }
+
+  type pattern =
+    PVar    of var_name
+  | PWild
+  | PInt    of Z.t
+  | PBytes  of MBytes.t
+  | PString of string
+  | PUnit
+  | PFalse
+  | PTrue
+  | PNone
+  | PSome   of pattern
+  | PCons   of pattern * pattern
+  | PNull
+  | PTuple  of pattern list
+
+  type type_constructor =
+  | Option
+  | List
+  | Set
+  | Map
+
+  type type_expr_case =
+    Prod     of type_expr_case list
+  | Sum      of (type_name * type_expr_case) list
+  | Record   of (type_name * type_expr_case) list
+  | TypeApp  of type_constructor * (type_expr_case list)
+  | Function of { args: type_expr_case list; ret: type_expr_case }
+  | Ref      of type_expr_case
+  | TC       of type_constructor
+  | String
+  | Int
+  | Unit
+  | Bool
+
+
+  type type_expr = { type_expr: type_expr_case; name: string option; orig: AST.type_expr }
+
+  type typed_var = { name:var_name; ty:type_expr; orig: asttodo }
+
+  type type_decl = { name:string; ty:type_expr; orig: asttodo }
+
+  type expr_case =
+    App      of { operator: operator; arguments: expr list }
+  | Var      of typed_var
+  | Constant of constant
+  | Lambda   of lambda
+
+  and expr = { expr: expr_case; ty:type_expr; orig: asttodo }
+
+  and decl = { var: typed_var; value: expr; orig: asttodo }
+
+  and lambda = {
+      parameters:   typed_var SMap.t;
+      declarations: decl list;
+      instructions: instr list;
+      result:       expr;
+    }
+
+  and operator_case =
+    Function of string
+  | Or | And | Lt | Leq | Gt | Geq | Equal | Neq | Cat | Cons | Add | Sub | Mult | Div | Mod
+  | Neg | Not
+  | Tuple | Set | List
+  | MapLookup
+
+  and operator = { operator: operator_case; ty:type_expr; orig: asttodo }
+
+  and constant =
+    Unit
+  | Int of Z.t | String of string | Bytes of MBytes.t
+  | False | True
+  | Null
+  | EmptySet
+  | CNone
+
+  and instr =
+    Assignment    of { name: var_name; value: expr; orig: asttodo }
+  | While         of { condition: expr; body: instr list; orig: asttodo }
+  | ForCollection of { list: expr; key: var_name; value: var_name option; body: instr list; orig: asttodo }
+  | If            of { condition: expr; ifso: instr list; ifnot: instr list; orig: asttodo }
+  | Match         of { expr: expr; cases: (pattern * instr list) list; orig: asttodo }
+  | DropUnit      of { expr: expr; orig: asttodo } (* expr returns unit, drop the result. Similar to OCaml's ";". *)
+  | Fail          of { expr: expr; orig: asttodo }
+
+  type ast = {
+      types           : type_decl list;
+      storage_decl    : typed_var;
+      operations_decl : typed_var;
+      declarations    : decl list;
+      orig: AST.t
+    }
+end
+
+let temporary_force_dune = 123
diff --git a/Typecheck2.mli b/Typecheck2.mli
new file mode 100644
index 000000000..7f1b5866c
--- /dev/null
+++ b/Typecheck2.mli
@@ -0,0 +1,104 @@
+[@@@warning "-30"]
+
+module SMap = Map.Make(String)
+
+module O = struct
+  type asttodo = [`TODO] (* occurrences of asttodo will point to some part of the original parser AST *)
+
+  type type_name = string
+  type var_name = { name: string; orig: asttodo }
+
+  type pattern =
+    PVar    of var_name
+  | PWild
+  | PInt    of Z.t
+  | PBytes  of MBytes.t
+  | PString of string
+  | PUnit
+  | PFalse
+  | PTrue
+  | PNone
+  | PSome   of pattern
+  | PCons   of pattern * pattern
+  | PNull
+  | PTuple  of pattern list
+
+  type type_constructor =
+  | Option
+  | List
+  | Set
+  | Map
+
+  type type_expr_case =
+    Prod     of type_expr_case list
+  | Sum      of (type_name * type_expr_case) list
+  | Record   of (type_name * type_expr_case) list
+  | TypeApp  of type_constructor * (type_expr_case list)
+  | Function of { args: type_expr_case list; ret: type_expr_case }
+  | Ref      of type_expr_case
+  | TC       of type_constructor
+  | String
+  | Int
+  | Unit
+  | Bool
+
+
+  type type_expr = { type_expr: type_expr_case; name: string option; orig: AST.type_expr }
+
+  type typed_var = { name:var_name; ty:type_expr; orig: asttodo }
+
+  type type_decl = { name:string; ty:type_expr; orig: asttodo }
+
+  type expr_case =
+    App      of { operator: operator; arguments: expr list }
+  | Var      of typed_var
+  | Constant of constant
+  | Lambda   of lambda
+
+  and expr = { expr: expr_case; ty:type_expr; orig: asttodo }
+
+  and decl = { var: typed_var; value: expr; orig: asttodo }
+
+  and lambda = {
+      parameters:   typed_var SMap.t;
+      declarations: decl list;
+      instructions: instr list;
+      result:       expr;
+    }
+
+  and operator_case =
+    Function of string
+  | Or | And | Lt | Leq | Gt | Geq | Equal | Neq | Cat | Cons | Add | Sub | Mult | Div | Mod
+  | Neg | Not
+  | Tuple | Set | List
+  | MapLookup
+
+  and operator = { operator: operator_case; ty:type_expr; orig: asttodo }
+
+  and constant =
+    Unit
+  | Int of Z.t | String of string | Bytes of MBytes.t
+  | False | True
+  | Null
+  | EmptySet
+  | CNone
+
+  and instr =
+    Assignment    of { name: var_name; value: expr; orig: asttodo }
+  | While         of { condition: expr; body: instr list; orig: asttodo }
+  | ForCollection of { list: expr; key: var_name; value: var_name option; body: instr list; orig: asttodo }
+  | If            of { condition: expr; ifso: instr list; ifnot: instr list; orig: asttodo }
+  | Match         of { expr: expr; cases: (pattern * instr list) list; orig: asttodo }
+  | DropUnit      of { expr: expr; orig: asttodo } (* expr returns unit, drop the result. Similar to OCaml's ";". *)
+  | Fail          of { expr: expr; orig: asttodo }
+
+  type ast = {
+      types           : type_decl list;
+      storage_decl    : typed_var;
+      operations_decl : typed_var;
+      declarations    : decl list;
+      orig: AST.t
+    }
+end
+
+let temporary_force_dune = 123