diff --git a/src/passes/1-parser/ligodity/LexToken.mli b/src/passes/1-parser/ligodity/LexToken.mli
index a30c41714..ea4f0a6ad 100644
--- a/src/passes/1-parser/ligodity/LexToken.mli
+++ b/src/passes/1-parser/ligodity/LexToken.mli
@@ -31,50 +31,50 @@ type lexeme = string
 type t =
   (* Symbols *)
 
-  ARROW of Region.t   (* "->" *)
-| CONS of Region.t     (* "::" *)
-| CAT of Region.t      (* "^"  *)
-  (*| APPEND   (* "@"  *)*)
+  ARROW of Region.t  (* "->" *)
+| CONS  of Region.t  (* "::" *)
+| CAT   of Region.t  (* "^"  *)
+(*| APPEND   (* "@"  *)*)
 
   (* Arithmetics *)
 
 | MINUS of Region.t    (* "-" *)
-| PLUS of Region.t     (* "+" *)
+| PLUS  of Region.t    (* "+" *)
 | SLASH of Region.t    (* "/" *)
-| TIMES of Region.t   (* "*" *)
+| TIMES of Region.t    (* "*" *)
 
   (* Compounds *)
 
-| LPAR of Region.t    (* "(" *)
-| RPAR of Region.t   (* ")" *)
-| LBRACKET of Region.t (* "[" *)
-| RBRACKET of Region.t (* "]" *)
-| LBRACE of Region.t  (* "{" *)
-| RBRACE of Region.t  (* "}" *)
+| LPAR     of Region.t  (* "(" *)
+| RPAR     of Region.t  (* ")" *)
+| LBRACKET of Region.t  (* "[" *)
+| RBRACKET of Region.t  (* "]" *)
+| LBRACE   of Region.t  (* "{" *)
+| RBRACE   of Region.t  (* "}" *)
 
   (* Separators *)
 
-| COMMA of Region.t   (* "," *)
-| SEMI  of Region.t   (* ";" *)
-| VBAR of Region.t    (* "|" *)
-| COLON of Region.t   (* ":" *)
-| DOT of Region.t     (* "." *)
+| COMMA of Region.t  (* "," *)
+| SEMI  of Region.t  (* ";" *)
+| VBAR  of Region.t  (* "|" *)
+| COLON of Region.t  (* ":" *)
+| DOT   of Region.t  (* "." *)
 
   (* Wildcard *)
 
-| WILD of Region.t    (* "_" *)
+| WILD of Region.t  (* "_" *)
 
   (* Comparisons *)
 
 | EQ of Region.t      (* "="  *)
-| NE of Region.t       (* "<>" *)
-| LT of Region.t       (* "<"  *)
-| GT of Region.t    (* ">"  *)
+| NE of Region.t      (* "<>" *)
+| LT of Region.t      (* "<"  *)
+| GT of Region.t      (* ">"  *)
 | LE of Region.t      (* "=<" *)
-| GE of Region.t       (* ">=" *)
+| GE of Region.t      (* ">=" *)
 
-| BOOL_OR of Region.t (* "||" *)
-| BOOL_AND of Region.t(* "&&" *)
+| BOOL_OR  of Region.t (* "||" *)
+| BOOL_AND of Region.t (* "&&" *)
 
   (* Identifiers, labels, numbers and strings *)
 
@@ -90,24 +90,24 @@ type t =
 
 (*| And*)
 | Begin of Region.t
-| Else of Region.t
-| End of Region.t
+| Else  of Region.t
+| End   of Region.t
 | False of Region.t
-| Fun of Region.t
-| If of Region.t
-| In of Region.t
-| Let of Region.t
+| Fun   of Region.t
+| If    of Region.t
+| In    of Region.t
+| Let   of Region.t
 | Match of Region.t
-| Mod of Region.t
-| Not of Region.t
-| Of of Region.t
-| Or of Region.t
-| Then of Region.t
-| True of Region.t
-| Type of Region.t
-| With of Region.t
+| Mod   of Region.t
+| Not   of Region.t
+| Of    of Region.t
+| Or    of Region.t
+| Then  of Region.t
+| True  of Region.t
+| Type  of Region.t
+| With  of Region.t
 
-  (* Liquidity specific *)
+  (* Liquidity-specific *)
 
 | LetEntry of Region.t
 | MatchNat of Region.t
@@ -137,23 +137,20 @@ val to_region : token -> Region.t
 
 (* Injections *)
 
-type int_err =
-  Non_canonical_zero
-
+type   int_err = Non_canonical_zero
 type ident_err = Reserved_name
+type   nat_err = Invalid_natural
+               | Non_canonical_zero_nat
+type   sym_err = Invalid_symbol
 
-type invalid_natural = 
-  | Invalid_natural
-  | Non_canonical_zero_nat
-
-val mk_string : lexeme -> Region.t -> token
-val mk_bytes  : lexeme -> Region.t -> token
 val mk_int    : lexeme -> Region.t -> (token,   int_err) result
-val mk_nat    : lexeme -> Region.t -> (token,   invalid_natural) result
+val mk_nat    : lexeme -> Region.t -> (token,   nat_err) result
 val mk_mtz    : lexeme -> Region.t -> (token,   int_err) result
 val mk_ident  : lexeme -> Region.t -> (token, ident_err) result
+val mk_sym    : lexeme -> Region.t -> (token,   sym_err) result
+val mk_string : lexeme -> Region.t -> token
+val mk_bytes  : lexeme -> Region.t -> token
 val mk_constr : lexeme -> Region.t -> token
-val mk_sym    : lexeme -> Region.t -> token
 val eof       : Region.t -> token
 
 (* Predicates *)
diff --git a/src/passes/1-parser/ligodity/LexToken.mll b/src/passes/1-parser/ligodity/LexToken.mll
index 74c32cd1a..2c437d15c 100644
--- a/src/passes/1-parser/ligodity/LexToken.mll
+++ b/src/passes/1-parser/ligodity/LexToken.mll
@@ -13,50 +13,50 @@ module SSet   = Utils.String.Set
 type t =
   (* Symbols *)
 
-  ARROW of Region.t     (* "->" *)
-| CONS of Region.t      (* "::" *)
-| CAT of Region.t       (* "^"  *)
-  (*| APPEND   (* "@"  *)*)
+  ARROW of Region.t  (* "->" *)
+| CONS  of Region.t  (* "::" *)
+| CAT   of Region.t  (* "^"  *)
+(*| APPEND   (* "@"  *)*)
 
   (* Arithmetics *)
 
-| MINUS of Region.t     (* "-" *)
-| PLUS of Region.t      (* "+" *)
-| SLASH of Region.t     (* "/" *)
-| TIMES of Region.t     (* "*" *)
+| MINUS of Region.t    (* "-" *)
+| PLUS  of Region.t    (* "+" *)
+| SLASH of Region.t    (* "/" *)
+| TIMES of Region.t    (* "*" *)
 
   (* Compounds *)
 
-| LPAR of Region.t      (* "(" *)
-| RPAR of Region.t      (* ")" *)
+| LPAR     of Region.t  (* "(" *)
+| RPAR     of Region.t  (* ")" *)
 | LBRACKET of Region.t  (* "[" *)
 | RBRACKET of Region.t  (* "]" *)
-| LBRACE of Region.t    (* "{" *)
-| RBRACE of Region.t    (* "}" *)
+| LBRACE   of Region.t  (* "{" *)
+| RBRACE   of Region.t  (* "}" *)
 
   (* Separators *)
 
-| COMMA of Region.t     (* "," *)
-| SEMI  of Region.t     (* ";" *)
-| VBAR of Region.t      (* "|" *)
-| COLON of Region.t     (* ":" *)
-| DOT of Region.t       (* "." *)
+| COMMA of Region.t  (* "," *)
+| SEMI  of Region.t  (* ";" *)
+| VBAR  of Region.t  (* "|" *)
+| COLON of Region.t  (* ":" *)
+| DOT   of Region.t  (* "." *)
 
   (* Wildcard *)
 
-| WILD of Region.t      (* "_" *)
+| WILD of Region.t  (* "_" *)
 
   (* Comparisons *)
 
-| EQ of Region.t        (* "="  *)
-| NE of Region.t        (* "<>" *)
-| LT of Region.t        (* "<"  *)
-| GT of Region.t        (* ">"  *)
-| LE of Region.t        (* "=<" *)
-| GE of Region.t        (* ">=" *)
+| EQ of Region.t      (* "="  *)
+| NE of Region.t      (* "<>" *)
+| LT of Region.t      (* "<"  *)
+| GT of Region.t      (* ">"  *)
+| LE of Region.t      (* "=<" *)
+| GE of Region.t      (* ">=" *)
 
-| BOOL_OR of Region.t   (* "||" *)
-| BOOL_AND of Region.t  (* "&&" *)
+| BOOL_OR  of Region.t (* "||" *)
+| BOOL_AND of Region.t (* "&&" *)
 
   (* Identifiers, labels, numbers and strings *)
 
@@ -72,24 +72,24 @@ type t =
 
 (*| And*)
 | Begin of Region.t
-| Else of Region.t
-| End of Region.t
+| Else  of Region.t
+| End   of Region.t
 | False of Region.t
-| Fun of Region.t
-| If of Region.t
-| In of Region.t
-| Let of Region.t
+| Fun   of Region.t
+| If    of Region.t
+| In    of Region.t
+| Let   of Region.t
 | Match of Region.t
-| Mod of Region.t
-| Not of Region.t
-| Of of Region.t
-| Or of Region.t
-| Then of Region.t
-| True of Region.t
-| Type of Region.t
-| With of Region.t
+| Mod   of Region.t
+| Not   of Region.t
+| Of    of Region.t
+| Or    of Region.t
+| Then  of Region.t
+| True  of Region.t
+| Type  of Region.t
+| With  of Region.t
 
-  (* Liquidity specific *)
+  (* Liquidity-specific *)
 
 | LetEntry of Region.t
 | MatchNat of Region.t
@@ -99,7 +99,7 @@ type t =
 | Struct
 *)
 
-(* Virtual tokens *)
+  (* Virtual tokens *)
 
 | EOF of Region.t (* End of file *)
 
@@ -200,8 +200,8 @@ let to_lexeme = function
   | BOOL_AND _ -> "&&"
   | Ident id -> id.Region.value
   | Constr id -> id.Region.value
-  | Int i 
-  | Nat i 
+  | Int i
+  | Nat i
   | Mtz i -> fst i.Region.value
   | Str s -> s.Region.value
   | Bytes b -> fst b.Region.value
@@ -264,7 +264,7 @@ let keywords = [
 
 let reserved =
   let open SSet in
-  empty 
+  empty
     |> add "and"
     |> add "as"
     |> add "asr"
@@ -284,7 +284,7 @@ let reserved =
     |> add "lazy"
     |> add "lor"
     |> add "lsl"
-    |> add "lsr"    
+    |> add "lsr"
     |> add "lxor"
     |> add "method"
     |> add "module"
@@ -306,7 +306,7 @@ let reserved =
 
 let constructors = [
   (fun reg -> False reg);
-  (fun reg -> True  reg);  
+  (fun reg -> True  reg);
 ]
 
 let add map (key, value) = SMap.add key value map
@@ -379,15 +379,14 @@ let mk_int lexeme region =
   then Error Non_canonical_zero
   else Ok (Int Region.{region; value = lexeme, z})
 
-type invalid_natural = 
-  | Invalid_natural
-  | Non_canonical_zero_nat
-
+type nat_err =
+  Invalid_natural
+| Non_canonical_zero_nat
 
 let mk_nat lexeme region =
-  match (String.index_opt lexeme 'p') with  
+  match (String.index_opt lexeme 'p') with
   | None -> Error Invalid_natural
-  | Some _ -> (  
+  | Some _ -> (
     let z =
       Str.(global_replace (regexp "_") "" lexeme) |>
       Str.(global_replace (regexp "p") "") |>
@@ -408,35 +407,41 @@ let mk_mtz lexeme region =
 
 let eof region = EOF region
 
+type sym_err = Invalid_symbol
+
 let mk_sym lexeme region =
   match lexeme with
-    "->"   ->   ARROW     region
-  | "::"   ->   CONS      region
-  | "^"   ->    CAT       region
-  | "-"   ->    MINUS     region
-  | "+"   ->    PLUS      region
-  | "/"   ->    SLASH     region
-  | "*"   ->    TIMES     region
-  | "["   ->    LBRACKET  region
-  | "]"   ->    RBRACKET  region
-  | "{"   ->    LBRACE    region
-  | "}"  ->     RBRACE    region
-  | ","  ->     COMMA     region
-  | ";"   ->    SEMI      region
-  | "|"   ->    VBAR      region
-  | ":"   ->    COLON     region
-  | "."  ->     DOT       region
-  | "_"   ->    WILD      region
-  | "="  ->     EQ        region
-  | "<>" ->     NE        region
-  | "<"   ->    LT        region
-  | ">"   ->    GT        region
-  | "=<"   ->   LE        region
-  | ">="   ->   GE        region
-  | "||"   ->   BOOL_OR   region
-  | "&&"   ->   BOOL_AND  region
-  | "("    ->   LPAR      region
-  | ")"    ->   RPAR      region
+  (* Lexemes in common with all concrete syntaxes *)
+    ";"   -> Ok (SEMI     region)
+  | ","   -> Ok (COMMA    region)
+  | "("   -> Ok (LPAR     region)
+  | ")"   -> Ok (RPAR     region)
+  | "["   -> Ok (LBRACKET region)
+  | "]"   -> Ok (RBRACKET region)
+  | "{"   -> Ok (LBRACE   region)
+  | "}"   -> Ok (RBRACE   region)
+  | "="   -> Ok (EQ       region)
+  | ":"   -> Ok (COLON    region)
+  | "|"   -> Ok (VBAR     region)
+  | "->"  -> Ok (ARROW    region)
+  | "."   -> Ok (DOT      region)
+  | "_"   -> Ok (WILD     region)
+  | "^"   -> Ok (CAT      region)
+  | "+"   -> Ok (PLUS     region)
+  | "-"   -> Ok (MINUS    region)
+  | "*"   -> Ok (TIMES    region)
+  | "/"   -> Ok (SLASH    region)
+  | "<"   -> Ok (LT       region)
+  | "<="  -> Ok (LE       region)
+  | ">"   -> Ok (GT       region)
+  | ">="  -> Ok (GE       region)
+
+
+  | "<>"  -> Ok (NE        region)
+  | "::"  -> Ok (CONS      region)
+  | "||"  -> Ok (BOOL_OR   region)
+  | "&&"  -> Ok (BOOL_AND  region)
+
   |  a  ->   failwith ("Not understood token: " ^ a)
 
 (* Identifiers *)
@@ -533,4 +538,4 @@ let is_sym = function
 let is_eof = function EOF _ -> true | _ -> false
 
 (* END TRAILER *)
-}
\ No newline at end of file
+}
diff --git a/src/passes/1-parser/pascaligo/AST.ml b/src/passes/1-parser/pascaligo/AST.ml
index 44c6c0734..537901bab 100644
--- a/src/passes/1-parser/pascaligo/AST.ml
+++ b/src/passes/1-parser/pascaligo/AST.ml
@@ -63,7 +63,6 @@ type kwd_not        = Region.t
 type kwd_of         = Region.t
 type kwd_or         = Region.t
 type kwd_patch      = Region.t
-type kwd_procedure  = Region.t
 type kwd_record     = Region.t
 type kwd_remove     = Region.t
 type kwd_set        = Region.t
@@ -161,9 +160,9 @@ type t = {
 and ast = t
 
 and declaration =
-  TypeDecl   of type_decl reg
-| ConstDecl  of const_decl reg
-| LambdaDecl of lambda_decl
+  TypeDecl  of type_decl reg
+| ConstDecl of const_decl reg
+| FunDecl   of fun_decl reg
 
 and const_decl = {
   kwd_const  : kwd_const;
@@ -188,7 +187,7 @@ and type_decl = {
 and type_expr =
   TProd   of cartesian
 | TSum    of (variant reg, vbar) nsepseq reg
-| TRecord of record_type
+| TRecord of field_decl reg injection reg
 | TApp    of (type_name * type_tuple) reg
 | TFun    of (type_expr * arrow * type_expr) reg
 | TPar    of type_expr par reg
@@ -198,11 +197,9 @@ and cartesian = (type_expr, times) nsepseq reg
 
 and variant = {
   constr : constr;
-  args   : (kwd_of * cartesian) option
+  args   : (kwd_of * type_expr) option
 }
 
-and record_type = field_decl reg injection reg
-
 and field_decl = {
   field_name : field_name;
   colon      : colon;
@@ -213,10 +210,6 @@ and type_tuple = (type_expr, comma) nsepseq par reg
 
 (* Function and procedure declarations *)
 
-and lambda_decl =
-  FunDecl   of fun_decl   reg
-| ProcDecl  of proc_decl  reg
-
 and fun_decl = {
   kwd_function : kwd_function;
   name         : variable;
@@ -231,16 +224,6 @@ and fun_decl = {
   terminator   : semi option
 }
 
-and proc_decl = {
-  kwd_procedure : kwd_procedure;
-  name          : variable;
-  param         : parameters;
-  kwd_is        : kwd_is;
-  local_decls   : local_decl list;
-  block         : block reg;
-  terminator    : semi option
-}
-
 and parameters = (param_decl, semi) nsepseq par reg
 
 and param_decl =
@@ -284,7 +267,6 @@ and statement =
 
 and local_decl =
   LocalFun  of fun_decl reg
-| LocalProc of proc_decl reg
 | LocalData of data_decl
 
 and data_decl =
@@ -425,10 +407,8 @@ and for_loop =
 and for_int = {
   kwd_for : kwd_for;
   assign  : var_assign reg;
-  down    : kwd_down option;
   kwd_to  : kwd_to;
   bound   : expr;
-  step    : (kwd_step * expr) option;
   block   : block reg
 }
 
@@ -439,14 +419,22 @@ and var_assign = {
 }
 
 and for_collect = {
-  kwd_for : kwd_for;
-  var     : variable;
-  bind_to : (arrow * variable) option;
-  kwd_in  : kwd_in;
-  expr    : expr;
-  block   : block reg
+  kwd_for    : kwd_for;
+  var        : variable;
+  bind_to    : (arrow * variable) option;
+  colon      : colon;
+  elt_type   : type_expr;
+  kwd_in     : kwd_in;
+  collection : collection;
+  expr       : expr;
+  block      : block reg
 }
 
+and collection =
+  Map  of kwd_map
+| Set  of kwd_set
+| List of kwd_list
+
 (* Expressions *)
 
 and expr =
@@ -577,16 +565,13 @@ and selection =
   FieldName of field_name
 | Component of (Lexer.lexeme * Z.t) reg
 
-and tuple_expr =
-  TupleInj of tuple_injection
-
-and tuple_injection = (expr, comma) nsepseq par reg
+and tuple_expr = (expr, comma) nsepseq par reg
 
 and none_expr = c_None
 
 and fun_call = (fun_name * arguments) reg
 
-and arguments = tuple_injection
+and arguments = tuple_expr
 
 (* Patterns *)
 
@@ -596,6 +581,7 @@ and pattern =
 | PVar    of Lexer.lexeme reg
 | PWild   of wild
 | PInt    of (Lexer.lexeme * Z.t) reg
+| PNat    of (Lexer.lexeme * Z.t) reg
 | PBytes  of (Lexer.lexeme * Hex.t) reg
 | PString of Lexer.lexeme reg
 | PUnit   of c_Unit
@@ -645,8 +631,7 @@ let rec expr_to_region = function
 | ECase  {region;_}
 | EPar   {region; _} -> region
 
-and tuple_expr_to_region = function
-  TupleInj {region; _} -> region
+and tuple_expr_to_region {region; _} = region
 
 and map_expr_to_region = function
   MapLookUp {region; _}
@@ -733,6 +718,7 @@ let pattern_to_region = function
 | PVar        {region; _}
 | PWild        region
 | PInt        {region; _}
+| PNat        {region; _}
 | PBytes      {region; _}
 | PString     {region; _}
 | PUnit        region
@@ -748,7 +734,6 @@ let pattern_to_region = function
 
 let local_decl_to_region = function
   LocalFun             {region; _}
-| LocalProc            {region; _}
 | LocalData LocalConst {region; _}
 | LocalData LocalVar   {region; _} -> region
 
diff --git a/src/passes/1-parser/pascaligo/AST.mli b/src/passes/1-parser/pascaligo/AST.mli
index 1deedf566..8bda1d76e 100644
--- a/src/passes/1-parser/pascaligo/AST.mli
+++ b/src/passes/1-parser/pascaligo/AST.mli
@@ -47,7 +47,6 @@ type kwd_not        = Region.t
 type kwd_of         = Region.t
 type kwd_or         = Region.t
 type kwd_patch      = Region.t
-type kwd_procedure  = Region.t
 type kwd_record     = Region.t
 type kwd_remove     = Region.t
 type kwd_set        = Region.t
@@ -135,7 +134,7 @@ type 'a braces = {
   rbrace : rbrace
 }
 
-(** The Abstract Syntax Tree 
+(** The Abstract Syntax Tree
 
 The AST mirrors the contents of Parser.mly, which defines a tree of parsing
 productions that are used to make a syntax tree from a given program input.
@@ -152,9 +151,9 @@ type t = {
 and ast = t
 
 and declaration =
-  TypeDecl   of type_decl reg
-| ConstDecl  of const_decl reg
-| LambdaDecl of lambda_decl
+  TypeDecl  of type_decl reg
+| ConstDecl of const_decl reg
+| FunDecl   of fun_decl reg
 
 and const_decl = {
   kwd_const  : kwd_const;
@@ -179,7 +178,7 @@ and type_decl = {
 and type_expr =
   TProd   of cartesian
 | TSum    of (variant reg, vbar) nsepseq reg
-| TRecord of record_type
+| TRecord of field_decl reg injection reg
 | TApp    of (type_name * type_tuple) reg
 | TFun    of (type_expr * arrow * type_expr) reg
 | TPar    of type_expr par reg
@@ -189,11 +188,9 @@ and cartesian = (type_expr, times) nsepseq reg
 
 and variant = {
   constr : constr;
-  args   : (kwd_of * cartesian) option
+  args   : (kwd_of * type_expr) option
 }
 
-and record_type = field_decl reg injection reg
-
 and field_decl = {
   field_name : field_name;
   colon      : colon;
@@ -202,11 +199,7 @@ and field_decl = {
 
 and type_tuple = (type_expr, comma) nsepseq par reg
 
-(* Function and procedure declarations *)
-
-and lambda_decl =
-  FunDecl   of fun_decl   reg
-| ProcDecl  of proc_decl  reg
+(* Function declarations *)
 
 and fun_decl = {
   kwd_function : kwd_function;
@@ -222,16 +215,6 @@ and fun_decl = {
   terminator   : semi option
 }
 
-and proc_decl = {
-  kwd_procedure : kwd_procedure;
-  name          : variable;
-  param         : parameters;
-  kwd_is        : kwd_is;
-  local_decls   : local_decl list;
-  block         : block reg;
-  terminator    : semi option
-}
-
 and parameters = (param_decl, semi) nsepseq par reg
 
 and param_decl =
@@ -275,7 +258,6 @@ and statement =
 
 and local_decl =
   LocalFun  of fun_decl reg
-| LocalProc of proc_decl reg
 | LocalData of data_decl
 
 and data_decl =
@@ -416,10 +398,8 @@ and for_loop =
 and for_int = {
   kwd_for : kwd_for;
   assign  : var_assign reg;
-  down    : kwd_down option;
   kwd_to  : kwd_to;
   bound   : expr;
-  step    : (kwd_step * expr) option;
   block   : block reg
 }
 
@@ -430,18 +410,26 @@ and var_assign = {
 }
 
 and for_collect = {
-  kwd_for : kwd_for;
-  var     : variable;
-  bind_to : (arrow * variable) option;
-  kwd_in  : kwd_in;
-  expr    : expr;
-  block   : block reg
+  kwd_for    : kwd_for;
+  var        : variable;
+  bind_to    : (arrow * variable) option;
+  colon      : colon;
+  elt_type   : type_expr;
+  kwd_in     : kwd_in;
+  collection : collection;
+  expr       : expr;
+  block      : block reg
 }
 
+and collection =
+  Map  of kwd_map
+| Set  of kwd_set
+| List of kwd_list
+
 (* Expressions *)
 
 and expr =
-| ECase   of expr case reg
+  ECase   of expr case reg
 | EAnnot  of annot_expr reg
 | ELogic  of logic_expr
 | EArith  of arith_expr
@@ -568,16 +556,13 @@ and selection =
   FieldName of field_name
 | Component of (Lexer.lexeme * Z.t) reg
 
-and tuple_expr =
-  TupleInj of tuple_injection
-
-and tuple_injection = (expr, comma) nsepseq par reg
+and tuple_expr = (expr, comma) nsepseq par reg
 
 and none_expr = c_None
 
 and fun_call = (fun_name * arguments) reg
 
-and arguments = tuple_injection
+and arguments = tuple_expr
 
 (* Patterns *)
 
@@ -587,6 +572,7 @@ and pattern =
 | PVar    of Lexer.lexeme reg
 | PWild   of wild
 | PInt    of (Lexer.lexeme * Z.t) reg
+| PNat    of (Lexer.lexeme * Z.t) reg
 | PBytes  of (Lexer.lexeme * Hex.t) reg
 | PString of Lexer.lexeme reg
 | PUnit   of c_Unit
diff --git a/src/passes/1-parser/pascaligo/Doc/pascaligo.md b/src/passes/1-parser/pascaligo/Doc/pascaligo.md
index e9802ebab..8680138a8 100644
--- a/src/passes/1-parser/pascaligo/Doc/pascaligo.md
+++ b/src/passes/1-parser/pascaligo/Doc/pascaligo.md
@@ -327,20 +327,20 @@ expression, typically performing a side effect.
 There are three kinds of native numerical types in PascaLIGO: `int`,
 `nat` and `tez`.
 
-    * The first is the type of signed integers, e.g., `-4`, `0` or
+* The first is the type of signed integers, e.g., `-4`, `0` or
 `13`. Note that the value zero has a canonical form, `0`, and no
 other, for example `00` is invalid. Also, for the sake of convenience,
 underscores are allowed in the literals, like `1_000_000`.
 
-    * The second numerical type is the type of the natural numbers,
-e.g., `0n` or `13n`. Note that the `nat` literals must be annotated
-with the suffix `n`, which distinguishes them from `int` literals. The
-same convenient use of underscores as with integer literals is allowed
-too and the canonical form of zero is `0n`.
+* The second numerical type is the type of the natural numbers, e.g.,
+`0n` or `13n`. Note that the `nat` literals must be annotated with the
+suffix `n`, which distinguishes them from `int` literals. The same
+convenient use of underscores as with integer literals is allowed too
+and the canonical form of zero is `0n`.
 
-    * The last kind of native numerical type is `tez`, which is a unit
-of measure of the amounts (fees, accounts). Beware: the literals of
-the type `tez` are annotated with the suffix `mtz`, which stands for
+* The last kind of native numerical type is `tez`, which is a unit of
+measure of the amounts (fees, accounts). Beware: the literals of the
+type `tez` are annotated with the suffix `mtz`, which stands for
 millionth of Tez, for instance, `0mtz` or `1200000mtz`. The same handy
 use of underscores as in natural literals help in the writing, like
 `1_200_000mtz`.
@@ -533,14 +533,13 @@ in terse style (see section "Predefined types and values/Lists").
 
 Given a tuple `t` with _n_ components, the `i`th component is
 
-    t.(i)
+    t.i
 
-where `t.(0)` is the first component. For example, given the
-declaration
+where `t.0` is the first component. For example, given the declaration
 
     const t : int * string = (4, "four")
 
-the expression `t.(1)` has the value `"four"`.
+the expression `t.1` has the value `"four"`.
 
 #### Records
 
diff --git a/src/passes/1-parser/pascaligo/LexToken.mli b/src/passes/1-parser/pascaligo/LexToken.mli
index ea1f2123e..1f94e166f 100644
--- a/src/passes/1-parser/pascaligo/LexToken.mli
+++ b/src/passes/1-parser/pascaligo/LexToken.mli
@@ -53,13 +53,13 @@ type t =
 | VBAR     of Region.t  (* "|"   *)
 | ARROW    of Region.t  (* "->"  *)
 | ASS      of Region.t  (* ":="  *)
-| EQUAL    of Region.t  (* "="   *)
+| EQ       of Region.t  (* "="   *)
 | COLON    of Region.t  (* ":"   *)
 | LT       of Region.t  (* "<"   *)
-| LEQ      of Region.t  (* "<="  *)
+| LE       of Region.t  (* "<="  *)
 | GT       of Region.t  (* ">"   *)
-| GEQ      of Region.t  (* ">="  *)
-| NEQ      of Region.t  (* "=/=" *)
+| GE       of Region.t  (* ">="  *)
+| NE       of Region.t  (* "=/=" *)
 | PLUS     of Region.t  (* "+"   *)
 | MINUS    of Region.t  (* "-"   *)
 | SLASH    of Region.t  (* "/"   *)
@@ -137,23 +137,20 @@ val to_region : token -> Region.t
 
 (* Injections *)
 
-type int_err =
-  Non_canonical_zero
-
+type   int_err = Non_canonical_zero
 type ident_err = Reserved_name
+type   nat_err = Invalid_natural
+               | Non_canonical_zero_nat
+type   sym_err = Invalid_symbol
 
-type invalid_natural =
-  | Invalid_natural
-  | Non_canonical_zero_nat
-
-val mk_string : lexeme -> Region.t -> token
-val mk_bytes  : lexeme -> Region.t -> token
 val mk_int    : lexeme -> Region.t -> (token,   int_err) result
-val mk_nat    : lexeme -> Region.t -> (token,   invalid_natural) result
+val mk_nat    : lexeme -> Region.t -> (token,   nat_err) result
 val mk_mtz    : lexeme -> Region.t -> (token,   int_err) result
 val mk_ident  : lexeme -> Region.t -> (token, ident_err) result
+val mk_sym    : lexeme -> Region.t -> (token,   sym_err) result
+val mk_string : lexeme -> Region.t -> token
+val mk_bytes  : lexeme -> Region.t -> token
 val mk_constr : lexeme -> Region.t -> token
-val mk_sym    : lexeme -> Region.t -> token
 val eof       : Region.t -> token
 
 (* Predicates *)
diff --git a/src/passes/1-parser/pascaligo/LexToken.mll b/src/passes/1-parser/pascaligo/LexToken.mll
index b92ae7edd..c27abbb12 100644
--- a/src/passes/1-parser/pascaligo/LexToken.mll
+++ b/src/passes/1-parser/pascaligo/LexToken.mll
@@ -51,13 +51,13 @@ type t =
 | VBAR     of Region.t
 | ARROW    of Region.t
 | ASS      of Region.t
-| EQUAL    of Region.t
+| EQ       of Region.t
 | COLON    of Region.t
 | LT       of Region.t
-| LEQ      of Region.t
+| LE       of Region.t
 | GT       of Region.t
-| GEQ      of Region.t
-| NEQ      of Region.t
+| GE       of Region.t
+| NE       of Region.t
 | PLUS     of Region.t
 | MINUS    of Region.t
 | SLASH    of Region.t
@@ -183,13 +183,13 @@ let proj_token = function
 | VBAR     region -> region, "VBAR"
 | ARROW    region -> region, "ARROW"
 | ASS      region -> region, "ASS"
-| EQUAL    region -> region, "EQUAL"
+| EQ       region -> region, "EQ"
 | COLON    region -> region, "COLON"
 | LT       region -> region, "LT"
-| LEQ      region -> region, "LEQ"
+| LE       region -> region, "LE"
 | GT       region -> region, "GT"
-| GEQ      region -> region, "GEQ"
-| NEQ      region -> region, "NEQ"
+| GE       region -> region, "GE"
+| NE       region -> region, "NE"
 | PLUS     region -> region, "PLUS"
 | MINUS    region -> region, "MINUS"
 | SLASH    region -> region, "SLASH"
@@ -276,13 +276,13 @@ let to_lexeme = function
 | VBAR     _ -> "|"
 | ARROW    _ -> "->"
 | ASS      _ -> ":="
-| EQUAL    _ -> "="
+| EQ       _ -> "="
 | COLON    _ -> ":"
 | LT       _ -> "<"
-| LEQ      _ -> "<="
+| LE       _ -> "<="
 | GT       _ -> ">"
-| GEQ      _ -> ">="
-| NEQ      _ -> "=/="
+| GE       _ -> ">="
+| NE       _ -> "=/="
 | PLUS     _ -> "+"
 | MINUS    _ -> "-"
 | SLASH    _ -> "/"
@@ -480,9 +480,9 @@ let mk_int lexeme region =
   then Error Non_canonical_zero
   else Ok (Int Region.{region; value = lexeme, z})
 
-type invalid_natural =
-  | Invalid_natural
-  | Non_canonical_zero_nat
+type nat_err =
+  Invalid_natural
+| Non_canonical_zero_nat
 
 let mk_nat lexeme region =
   match (String.index_opt lexeme 'n') with
@@ -508,35 +508,42 @@ let mk_mtz lexeme region =
 
 let eof region = EOF region
 
+type sym_err = Invalid_symbol
+
 let mk_sym lexeme region =
   match lexeme with
-    ";"   -> SEMI     region
-  | ","   -> COMMA    region
-  | "("   -> LPAR     region
-  | ")"   -> RPAR     region
-  | "{"   -> LBRACE   region
-  | "}"   -> RBRACE   region
-  | "["   -> LBRACKET region
-  | "]"   -> RBRACKET region
-  | "#"   -> CONS     region
-  | "|"   -> VBAR     region
-  | "->"  -> ARROW    region
-  | ":="  -> ASS      region
-  | "="   -> EQUAL    region
-  | ":"   -> COLON    region
-  | "<"   -> LT       region
-  | "<="  -> LEQ      region
-  | ">"   -> GT       region
-  | ">="  -> GEQ      region
-  | "=/=" -> NEQ      region
-  | "+"   -> PLUS     region
-  | "-"   -> MINUS    region
-  | "/"   -> SLASH    region
-  | "*"   -> TIMES    region
-  | "."   -> DOT      region
-  | "_"   -> WILD     region
-  | "^"   -> CAT      region
-  |     _ -> assert false
+  (* Lexemes in common with all concrete syntaxes *)
+    ";"   -> Ok (SEMI     region)
+  | ","   -> Ok (COMMA    region)
+  | "("   -> Ok (LPAR     region)
+  | ")"   -> Ok (RPAR     region)
+  | "["   -> Ok (LBRACKET region)
+  | "]"   -> Ok (RBRACKET region)
+  | "{"   -> Ok (LBRACE   region)
+  | "}"   -> Ok (RBRACE   region)
+  | "="   -> Ok (EQ       region)
+  | ":"   -> Ok (COLON    region)
+  | "|"   -> Ok (VBAR     region)
+  | "->"  -> Ok (ARROW    region)
+  | "."   -> Ok (DOT      region)
+  | "_"   -> Ok (WILD     region)
+  | "^"   -> Ok (CAT      region)
+  | "+"   -> Ok (PLUS     region)
+  | "-"   -> Ok (MINUS    region)
+  | "*"   -> Ok (TIMES    region)
+  | "/"   -> Ok (SLASH    region)
+  | "<"   -> Ok (LT       region)
+  | "<="  -> Ok (LE      region)
+  | ">"   -> Ok (GT       region)
+  | ">="  -> Ok (GE      region)
+
+  (* Lexemes specific to PascaLIGO *)
+  | "=/=" -> Ok (NE       region)
+  | "#"   -> Ok (CONS     region)
+  | ":="  -> Ok (ASS      region)
+
+  (* Invalid lexemes *)
+  |     _ -> Error Invalid_symbol
 
 (* Identifiers *)
 
@@ -632,13 +639,13 @@ let is_sym = function
 | VBAR     _
 | ARROW    _
 | ASS      _
-| EQUAL    _
+| EQ       _
 | COLON    _
 | LT       _
-| LEQ      _
+| LE       _
 | GT       _
-| GEQ      _
-| NEQ      _
+| GE       _
+| NE       _
 | PLUS     _
 | MINUS    _
 | SLASH    _
diff --git a/src/passes/1-parser/pascaligo/ParToken.mly b/src/passes/1-parser/pascaligo/ParToken.mly
index 49f77b8d3..c236def9e 100644
--- a/src/passes/1-parser/pascaligo/ParToken.mly
+++ b/src/passes/1-parser/pascaligo/ParToken.mly
@@ -27,13 +27,13 @@
 %token <Region.t> VBAR        (* "|"   *)
 %token <Region.t> ARROW       (* "->"  *)
 %token <Region.t> ASS         (* ":="  *)
-%token <Region.t> EQUAL       (* "="   *)
+%token <Region.t> EQ          (* "="   *)
 %token <Region.t> COLON       (* ":"   *)
 %token <Region.t> LT          (* "<"   *)
-%token <Region.t> LEQ         (* "<="  *)
+%token <Region.t> LE          (* "<="  *)
 %token <Region.t> GT          (* ">"   *)
-%token <Region.t> GEQ         (* ">="  *)
-%token <Region.t> NEQ         (* "=/=" *)
+%token <Region.t> GE          (* ">="  *)
+%token <Region.t> NE          (* "=/=" *)
 %token <Region.t> PLUS        (* "+"   *)
 %token <Region.t> MINUS       (* "-"   *)
 %token <Region.t> SLASH       (* "/"   *)
@@ -51,7 +51,6 @@
 %token <Region.t> Case        (* "case"       *)
 %token <Region.t> Const       (* "const"      *)
 %token <Region.t> Contains    (* "contains"   *)
-%token <Region.t> Down        (* "down"       *)
 %token <Region.t> Else        (* "else"       *)
 %token <Region.t> End         (* "end"        *)
 %token <Region.t> For         (* "for"        *)
@@ -68,12 +67,10 @@
 %token <Region.t> Of          (* "of"         *)
 %token <Region.t> Or          (* "or"         *)
 %token <Region.t> Patch       (* "patch"      *)
-%token <Region.t> Procedure   (* "procedure"  *)
 %token <Region.t> Record      (* "record"     *)
 %token <Region.t> Remove      (* "remove"     *)
 %token <Region.t> Set         (* "set"        *)
 %token <Region.t> Skip        (* "skip"       *)
-%token <Region.t> Step        (* "step"       *)
 %token <Region.t> Then        (* "then"       *)
 %token <Region.t> To          (* "to"         *)
 %token <Region.t> Type        (* "type"       *)
diff --git a/src/passes/1-parser/pascaligo/Parser.mly b/src/passes/1-parser/pascaligo/Parser.mly
index 55729ed77..dfb401942 100644
--- a/src/passes/1-parser/pascaligo/Parser.mly
+++ b/src/passes/1-parser/pascaligo/Parser.mly
@@ -114,9 +114,9 @@ contract:
   }
 
 declaration:
-  type_decl   {    TypeDecl $1 }
-| const_decl  {   ConstDecl $1 }
-| lambda_decl {  LambdaDecl $1 }
+  type_decl  {   TypeDecl $1 }
+| const_decl {  ConstDecl $1 }
+| fun_decl   {    FunDecl $1 }
 
 (* Type declarations *)
 
@@ -137,23 +137,27 @@ type_decl:
   }
 
 type_expr:
-  cartesian   {   TProd $1 }
-| sum_type    {    TSum $1 }
+  sum_type    {    TSum $1 }
 | record_type { TRecord $1 }
+| cartesian   {         $1 }
 
 cartesian:
-  nsepseq(function_type,TIMES) {
-    let region = nsepseq_to_region type_expr_to_region $1
-    in {region; value=$1}}
+  function_type TIMES nsepseq(function_type,TIMES) {
+    let value  = Utils.nsepseq_cons $1 $2 $3 in
+    let region = nsepseq_to_region type_expr_to_region value
+    in TProd {region; value}
+  }
+| function_type { ($1 : type_expr) }
 
 function_type:
   core_type {
     $1
   }
 | core_type ARROW function_type {
-    let region = cover (type_expr_to_region $1)
-                       (type_expr_to_region $3)
-    in TFun {region; value = ($1, $2, $3)} }
+    let start  = type_expr_to_region $1
+    and stop   = type_expr_to_region $3 in
+    let region = cover start stop in
+    TFun {region; value = $1,$2,$3} }
 
 core_type:
   type_name {
@@ -200,7 +204,7 @@ sum_type:
 
 variant:
   Constr Of cartesian {
-    let region = cover $1.region $3.region
+    let region = cover $1.region (type_expr_to_region $3)
     and value = {constr = $1; args = Some ($2, $3)}
     in {region; value}
   }
@@ -235,11 +239,7 @@ field_decl:
     and value  = {field_name = $1; colon = $2; field_type = $3}
     in {region; value} }
 
-(* Function and procedure declarations *)
-
-lambda_decl:
-  fun_decl   {   FunDecl $1 }
-| proc_decl  {  ProcDecl $1 }
+(* Function declarations *)
 
 fun_decl:
   Function fun_name parameters COLON type_expr Is
@@ -265,26 +265,6 @@ fun_decl:
       terminator   = $11}
     in {region; value}}
 
-proc_decl:
-  Procedure fun_name parameters Is
-    seq(local_decl)
-    block option(SEMI)
-    {
-     let stop =
-       match $7 with
-         Some region -> region
-       |        None -> $6.region in
-     let region = cover $1 stop
-     and value = {
-       kwd_procedure = $1;
-       name          = $2;
-       param         = $3;
-       kwd_is        = $4;
-       local_decls   = $5;
-       block         = $6;
-       terminator    = $7}
-     in {region; value}}
-
 parameters:
   par(nsepseq(param_decl,SEMI)) { $1 }
 
@@ -310,7 +290,7 @@ param_decl:
     in ParamConst {region; value}}
 
 param_type:
-  cartesian { TProd $1 }
+  cartesian { $1 }
 
 block:
   Begin sep_or_term_list(statement,SEMI) End {
@@ -342,7 +322,7 @@ open_data_decl:
 | open_var_decl   { LocalVar   $1 }
 
 open_const_decl:
-  Const unqualified_decl(EQUAL) {
+  Const unqualified_decl(EQ) {
     let name, colon, const_type, equal, init, stop = $2 in
     let region = cover $1 stop
     and value = {
@@ -371,7 +351,6 @@ open_var_decl:
 
 local_decl:
   fun_decl  { LocalFun  $1 }
-| proc_decl { LocalProc $1 }
 | data_decl { LocalData $1 }
 
 data_decl:
@@ -616,38 +595,42 @@ while_loop:
     in While {region; value}}
 
 for_loop:
-  For var_assign Down? To expr option(step_clause) block {
-    let region = cover $1 $7.region in
+  For var_assign To expr block {
+    let region = cover $1 $5.region in
     let value = {
       kwd_for = $1;
       assign  = $2;
-      down    = $3;
-      kwd_to  = $4;
-      bound   = $5;
-      step    = $6;
-      block   = $7}
+      kwd_to  = $3;
+      bound   = $4;
+      block   = $5}
     in For (ForInt {region; value})
   }
-| For var option(arrow_clause) In expr block {
-    let region = cover $1 $6.region in
+| For var option(arrow_clause) COLON type_expr
+  In collection expr block {
+    let region = cover $1 $9.region in
     let value = {
-      kwd_for = $1;
-      var     = $2;
-      bind_to = $3;
-      kwd_in  = $4;
-      expr    = $5;
-      block   = $6}
+      kwd_for    = $1;
+      var        = $2;
+      bind_to    = $3;
+      colon      = $4;
+      elt_type   = $5;
+      kwd_in     = $6;
+      collection = $7;
+      expr       = $8;
+      block      = $9}
     in For (ForCollect {region; value})}
 
+collection:
+  Map  { Map  $1 }
+| Set  { Set  $1 }
+| List { List $1 }
+
 var_assign:
   var ASS expr {
     let region = cover $1.region (expr_to_region $3)
     and value  = {name = $1; assign = $2; expr = $3}
     in {region; value}}
 
-step_clause:
-  Step expr { $1,$2 }
-
 arrow_clause:
   ARROW var { $1,$2 }
 
@@ -701,7 +684,7 @@ comp_expr:
     and value  = {arg1 = $1; op = $2; arg2 = $3}
     in ELogic (CompExpr (Lt {region; value}))
   }
-| comp_expr LEQ cat_expr {
+| comp_expr LE cat_expr {
     let start  = expr_to_region $1
     and stop   = expr_to_region $3 in
     let region = cover start stop
@@ -715,21 +698,21 @@ comp_expr:
     and value  = {arg1 = $1; op = $2; arg2 = $3}
     in ELogic (CompExpr (Gt {region; value}))
   }
-| comp_expr GEQ cat_expr {
+| comp_expr GE cat_expr {
     let start  = expr_to_region $1
     and stop   = expr_to_region $3 in
     let region = cover start stop
     and value  = {arg1 = $1; op = $2; arg2 = $3}
     in ELogic (CompExpr (Geq {region; value}))
   }
-| comp_expr EQUAL cat_expr {
+| comp_expr EQ cat_expr {
     let start  = expr_to_region $1
     and stop   = expr_to_region $3 in
     let region = cover start stop
     and value  = {arg1 = $1; op = $2; arg2 = $3}
     in ELogic (CompExpr (Equal {region; value}))
   }
-| comp_expr NEQ cat_expr {
+| comp_expr NE cat_expr {
     let start  = expr_to_region $1
     and stop   = expr_to_region $3 in
     let region = cover start stop
@@ -826,6 +809,7 @@ core_expr:
 | C_Unit           { EUnit $1                     }
 | annot_expr       { EAnnot $1                    }
 | tuple_expr       { ETuple $1                    }
+| par(expr)        { EPar $1                      }
 | list_expr        { EList $1                     }
 | C_None           { EConstr (NoneExpr $1)        }
 | fun_call         { ECall $1                     }
@@ -906,7 +890,7 @@ record_expr:
    in {region; value} }
 
 field_assignment:
-  field_name EQUAL expr {
+  field_name EQ expr {
     let region = cover $1.region (expr_to_region $3)
     and value = {
       field_name = $1;
@@ -920,13 +904,14 @@ fun_call:
     in {region; value = $1,$2}}
 
 tuple_expr:
-  tuple_inj { TupleInj $1 }
+  par(tuple_comp) { $1 }
 
-tuple_inj:
-  par(nsepseq(expr,COMMA)) { $1 }
+tuple_comp:
+  expr COMMA nsepseq(expr,COMMA) {
+    Utils.nsepseq_cons $1 $2 $3}
 
 arguments:
-  tuple_inj { $1 }
+  par(nsepseq(expr,COMMA)) { $1 }
 
 list_expr:
   injection(List,expr) { List $1 }
@@ -935,14 +920,18 @@ list_expr:
 (* Patterns *)
 
 pattern:
-  nsepseq(core_pattern,CONS) {
-    let region = nsepseq_to_region pattern_to_region $1
-    in PCons {region; value=$1}}
+  core_pattern CONS nsepseq(core_pattern,CONS) {
+    let value = Utils.nsepseq_cons $1 $2 $3 in
+    let region = nsepseq_to_region pattern_to_region value
+    in PCons {region; value}}
+| core_pattern { $1 }
 
 core_pattern:
   var                      {    PVar $1 }
 | WILD                     {   PWild $1 }
 | Int                      {    PInt $1 }
+| Nat                      {    PNat $1 }
+| Bytes                    {  PBytes $1 }
 | String                   { PString $1 }
 | C_Unit                   {   PUnit $1 }
 | C_False                  {  PFalse $1 }
diff --git a/src/passes/1-parser/pascaligo/ParserLog.ml b/src/passes/1-parser/pascaligo/ParserLog.ml
index 6cf9ccc3e..be363e4b2 100644
--- a/src/passes/1-parser/pascaligo/ParserLog.ml
+++ b/src/passes/1-parser/pascaligo/ParserLog.ml
@@ -62,6 +62,11 @@ let print_int buffer {region; value = lexeme, abstract} =
                (Z.to_string abstract)
   in Buffer.add_string buffer line
 
+let print_nat buffer {region; value = lexeme, abstract} =
+  let line = sprintf "%s: Nat (\"%s\", %s)\n"
+               (compact region) lexeme
+               (Z.to_string abstract)
+  in Buffer.add_string buffer line
 
 (* Main printing function *)
 
@@ -71,9 +76,9 @@ let rec print_tokens buffer ast =
   print_token buffer eof "EOF"
 
 and print_decl buffer = function
-  TypeDecl   decl -> print_type_decl   buffer decl
-| ConstDecl  decl -> print_const_decl  buffer decl
-| LambdaDecl decl -> print_lambda_decl buffer decl
+  TypeDecl  decl -> print_type_decl  buffer decl
+| ConstDecl decl -> print_const_decl buffer decl
+| FunDecl   decl -> print_fun_decl   buffer decl
 
 and print_const_decl buffer {value; _} =
   let {kwd_const; name; colon; const_type;
@@ -107,14 +112,14 @@ and print_type_expr buffer = function
 and print_cartesian buffer {value; _} =
   print_nsepseq buffer "*" print_type_expr value
 
-and print_variant buffer {value; _} =
+and print_variant buffer ({value; _}: variant reg) =
   let {constr; args} = value in
   print_constr buffer constr;
   match args with
     None -> ()
-  | Some (kwd_of, product) ->
+  | Some (kwd_of, t_expr) ->
       print_token     buffer kwd_of "of";
-      print_cartesian buffer product
+      print_type_expr buffer t_expr
 
 and print_sum_type buffer {value; _} =
   print_nsepseq buffer "|" print_variant value
@@ -151,10 +156,6 @@ and print_type_tuple buffer {value; _} =
   print_nsepseq buffer "," print_type_expr inside;
   print_token buffer rpar ")"
 
-and print_lambda_decl buffer = function
-  FunDecl     fun_decl -> print_fun_decl   buffer fun_decl
-| ProcDecl   proc_decl -> print_proc_decl  buffer proc_decl
-
 and print_fun_decl buffer {value; _} =
   let {kwd_function; name; param; colon;
        ret_type; kwd_is; local_decls;
@@ -171,17 +172,6 @@ and print_fun_decl buffer {value; _} =
   print_expr        buffer return;
   print_terminator  buffer terminator
 
-and print_proc_decl buffer {value; _} =
-  let {kwd_procedure; name; param; kwd_is;
-       local_decls; block; terminator} = value in
-  print_token       buffer kwd_procedure "procedure";
-  print_var         buffer name;
-  print_parameters  buffer param;
-  print_token       buffer kwd_is "is";
-  print_local_decls buffer local_decls;
-  print_block       buffer block;
-  print_terminator  buffer terminator
-
 and print_parameters buffer {value; _} =
   let {lpar; inside; rpar} = value in
   print_token buffer lpar "(";
@@ -229,7 +219,6 @@ and print_local_decls buffer sequence =
 
 and print_local_decl buffer = function
   LocalFun  decl -> print_fun_decl  buffer decl
-| LocalProc decl -> print_proc_decl buffer decl
 | LocalData decl -> print_data_decl buffer decl
 
 and print_data_decl buffer = function
@@ -342,14 +331,11 @@ and print_for_loop buffer = function
 | ForCollect for_collect -> print_for_collect buffer for_collect
 
 and print_for_int buffer ({value; _} : for_int reg) =
-  let {kwd_for; assign; down; kwd_to;
-       bound; step; block} = value in
+  let {kwd_for; assign; kwd_to; bound; block} = value in
   print_token      buffer kwd_for "for";
   print_var_assign buffer assign;
-  print_down       buffer down;
   print_token      buffer kwd_to "to";
   print_expr       buffer bound;
-  print_step       buffer step;
   print_block      buffer block
 
 and print_var_assign buffer {value; _} =
@@ -358,24 +344,26 @@ and print_var_assign buffer {value; _} =
   print_token buffer assign ":=";
   print_expr  buffer expr
 
-and print_down buffer = function
-  Some kwd_down -> print_token buffer kwd_down "down"
-| None          -> ()
-
-and print_step buffer = function
-  Some (kwd_step, expr) ->
-    print_token buffer kwd_step "step";
-    print_expr  buffer expr
-| None -> ()
-
 and print_for_collect buffer ({value; _} : for_collect reg) =
-  let {kwd_for; var; bind_to; kwd_in; expr; block} = value in
-  print_token   buffer kwd_for "for";
-  print_var     buffer var;
-  print_bind_to buffer bind_to;
-  print_token   buffer kwd_in "in";
-  print_expr    buffer expr;
-  print_block   buffer block
+  let {kwd_for; var; bind_to; colon; elt_type;
+       kwd_in; collection; expr; block} = value in
+  print_token      buffer kwd_for "for";
+  print_var        buffer var;
+  print_bind_to    buffer bind_to;
+  print_token      buffer colon ":";
+  print_type_expr  buffer elt_type;
+  print_token      buffer kwd_in "in";
+  print_collection buffer collection;
+  print_expr       buffer expr;
+  print_block      buffer block
+
+and print_collection buffer = function
+  Map kwd_map ->
+    print_token buffer kwd_map "map"
+| Set kwd_set ->
+    print_token buffer kwd_set "set"
+| List kwd_list ->
+    print_token buffer kwd_list "list"
 
 and print_bind_to buffer = function
   Some (arrow, variable) ->
@@ -632,10 +620,7 @@ and print_binding buffer {value; _} =
   print_token buffer arrow "->";
   print_expr  buffer image
 
-and print_tuple_expr buffer = function
-  TupleInj inj -> print_tuple_inj buffer inj
-
-and print_tuple_inj buffer {value; _} =
+and print_tuple_expr buffer {value; _} =
   let {lpar; inside; rpar} = value in
   print_token   buffer lpar "(";
   print_nsepseq buffer "," print_expr inside;
@@ -647,20 +632,20 @@ and print_none_expr buffer value = print_token buffer value "None"
 
 and print_fun_call buffer {value; _} =
   let fun_name, arguments = value in
-  print_var       buffer fun_name;
-  print_tuple_inj buffer arguments
+  print_var        buffer fun_name;
+  print_tuple_expr buffer arguments
 
 and print_constr_app buffer {value; _} =
   let constr, arguments = value in
   print_constr buffer constr;
   match arguments with
     None -> ()
-  | Some args -> print_tuple_inj buffer args
+  | Some args -> print_tuple_expr buffer args
 
 and print_some_app buffer {value; _} =
   let c_Some, arguments = value in
-  print_token     buffer c_Some "Some";
-  print_tuple_inj buffer arguments
+  print_token      buffer c_Some "Some";
+  print_tuple_expr buffer arguments
 
 and print_par_expr buffer {value; _} =
   let {lpar; inside; rpar} = value in
@@ -673,6 +658,7 @@ and print_pattern buffer = function
 | PVar var         -> print_var buffer var
 | PWild wild       -> print_token buffer wild "_"
 | PInt i           -> print_int buffer i
+| PNat n           -> print_nat buffer n
 | PBytes b         -> print_bytes buffer b
 | PString s        -> print_string buffer s
 | PUnit region     -> print_token buffer region "Unit"
@@ -740,3 +726,711 @@ let tokens_to_string      = to_string print_tokens
 let path_to_string        = to_string print_path
 let pattern_to_string     = to_string print_pattern
 let instruction_to_string = to_string print_instruction
+
+(* Pretty-printing the AST *)
+
+let mk_pad len rank pc =
+  pc ^ (if rank = len-1 then "`-- " else "|-- "),
+  pc ^ (if rank = len-1 then "    " else "|   ")
+
+let pp_ident buffer ~pad:(pd,_) name =
+  let node = sprintf "%s%s\n" pd name
+  in Buffer.add_string buffer node
+
+let pp_string buffer = pp_ident buffer
+
+let pp_node buffer = pp_ident buffer
+
+let rec pp_ast buffer ~pad:(_,pc as pad) {decl; _} =
+  let apply len rank =
+    let pad = mk_pad len rank pc in
+    pp_declaration buffer ~pad in
+  let decls = Utils.nseq_to_list decl in
+  pp_node buffer ~pad "<ast>";
+  List.iteri (List.length decls |> apply) decls
+
+and pp_declaration buffer ~pad:(_,pc as pad) = function
+  TypeDecl {value; _} ->
+    pp_node buffer ~pad "TypeDecl";
+    pp_ident buffer ~pad:(mk_pad 2 0 pc) value.name.value;
+    pp_type_expr buffer ~pad:(mk_pad 2 1 pc) value.type_expr
+| ConstDecl {value; _} ->
+    pp_node buffer ~pad "ConstDecl";
+    pp_const_decl buffer ~pad:(mk_pad 1 0 pc) value
+| FunDecl {value; _} ->
+    pp_node buffer ~pad "FunDecl";
+    pp_fun_decl buffer ~pad:(mk_pad 1 0 pc) value
+
+and pp_const_decl buffer ~pad:(_,pc) decl =
+  pp_ident buffer ~pad:(mk_pad 3 0 pc) decl.name.value;
+  pp_type_expr buffer ~pad:(mk_pad 3 1 pc) decl.const_type;
+  pp_expr buffer ~pad:(mk_pad 3 2 pc) decl.init
+
+and pp_type_expr buffer ~pad:(_,pc as pad) = function
+  TProd cartesian ->
+    pp_node buffer ~pad "TProd";
+    pp_cartesian buffer ~pad cartesian
+| TAlias {value; _} ->
+    pp_node buffer ~pad "TAlias";
+    pp_ident buffer ~pad:(mk_pad 1 0 pc) value
+| TPar {value; _} ->
+    pp_node buffer ~pad "TPar";
+    pp_type_expr buffer ~pad:(mk_pad 1 0 pc) value.inside
+| TApp {value=name,tuple; _} ->
+    pp_node buffer ~pad "TApp";
+    pp_ident buffer ~pad:(mk_pad 1 0 pc) name.value;
+    pp_type_tuple buffer ~pad:(mk_pad 2 1 pc) tuple
+| TFun {value; _} ->
+    pp_node buffer ~pad "TFun";
+    let apply len rank =
+      let pad = mk_pad len rank pc in
+      pp_type_expr buffer ~pad in
+    let domain, _, range = value in
+    List.iteri (apply 2) [domain; range]
+| TSum {value; _} ->
+    pp_node buffer ~pad "TSum";
+    let apply len rank variant =
+      let pad = mk_pad len rank pc in
+      pp_variant buffer ~pad variant.value in
+    let variants = Utils.nsepseq_to_list value in
+    List.iteri (List.length variants |> apply) variants
+| TRecord {value; _} ->
+    pp_node buffer ~pad "TRecord";
+    let apply len rank field_decl =
+      pp_field_decl buffer ~pad:(mk_pad len rank pc)
+                    field_decl.value in
+    let fields = Utils.sepseq_to_list value.elements in
+    List.iteri (List.length fields |> apply) fields
+
+and pp_cartesian buffer ~pad:(_,pc) {value; _} =
+  let apply len rank =
+    pp_type_expr buffer ~pad:(mk_pad len rank pc) in
+  let components = Utils.nsepseq_to_list value
+  in List.iteri (List.length components |> apply) components
+
+and pp_variant buffer ~pad:(_,pc as pad) {constr; args} =
+  pp_node buffer ~pad constr.value;
+  match args with
+          None -> ()
+  | Some (_,c) ->
+      pp_type_expr buffer ~pad:(mk_pad 1 0 pc) c
+
+and pp_field_decl buffer ~pad:(_,pc as pad) decl =
+  pp_node buffer ~pad decl.field_name.value;
+  pp_type_expr buffer ~pad:(mk_pad 1 0 pc) decl.field_type
+
+and pp_type_tuple buffer ~pad:(_,pc) {value; _} =
+  let components = Utils.nsepseq_to_list value.inside in
+  let apply len rank =
+    pp_type_expr buffer ~pad:(mk_pad len rank pc)
+  in List.iteri (List.length components |> apply) components
+
+and pp_fun_decl buffer ~pad:(_,pc) decl =
+  let () =
+    let pad = mk_pad 6 0 pc in
+    pp_ident buffer ~pad decl.name.value in
+  let () =
+    let pad = mk_pad 6 1 pc in
+    pp_node buffer ~pad "<parameters>";
+    pp_parameters buffer ~pad decl.param in
+  let () =
+    let _, pc as pad = mk_pad 6 2 pc in
+    pp_node buffer ~pad "<return type>";
+    pp_type_expr buffer ~pad:(mk_pad 1 0 pc) decl.ret_type in
+  let () =
+    let pad = mk_pad 6 3 pc in
+    pp_node buffer ~pad "<local declarations>";
+    pp_local_decls buffer ~pad decl.local_decls in
+  let () =
+    let pad = mk_pad 6 4 pc in
+    pp_node buffer ~pad "<block>";
+    let statements = decl.block.value.statements in
+    pp_statements buffer ~pad statements in
+  let () =
+    let _, pc as pad = mk_pad 6 5 pc in
+    pp_node buffer ~pad "<return>";
+    pp_expr buffer ~pad:(mk_pad 1 0 pc) decl.return
+  in ()
+
+and pp_parameters buffer ~pad:(_,pc) {value; _} =
+  let params = Utils.nsepseq_to_list value.inside in
+  let arity  = List.length params in
+  let apply len rank =
+    pp_param_decl buffer ~pad:(mk_pad len rank pc)
+  in List.iteri (apply arity) params
+
+and pp_param_decl buffer ~pad:(_,pc as pad) = function
+  ParamConst {value; _} ->
+    pp_node buffer ~pad "ParamConst";
+    pp_ident buffer ~pad:(mk_pad 2 0 pc) value.var.value;
+    pp_type_expr buffer ~pad:(mk_pad 2 1 pc) value.param_type
+| ParamVar {value; _} ->
+    pp_node buffer ~pad "ParamVar";
+    pp_ident buffer ~pad:(mk_pad 2 0 pc) value.var.value;
+    pp_type_expr buffer ~pad:(mk_pad 2 1 pc) value.param_type
+
+and pp_statements buffer ~pad:(_,pc) statements =
+  let statements = Utils.nsepseq_to_list statements in
+  let length     = List.length statements in
+  let apply len rank =
+    pp_statement buffer ~pad:(mk_pad len rank pc)
+  in List.iteri (apply length) statements
+
+and pp_statement buffer ~pad:(_,pc as pad) = function
+  Instr instr ->
+    pp_node buffer ~pad "Instr";
+    pp_instruction buffer ~pad:(mk_pad 1 0 pc) instr
+| Data data_decl ->
+    pp_node buffer ~pad "Data";
+    pp_data_decl buffer ~pad:(mk_pad 1 0 pc) data_decl
+
+and pp_instruction buffer ~pad:(_,pc as pad) = function
+  Single single_instr ->
+    pp_node buffer ~pad "Single";
+    pp_single_instr buffer ~pad:(mk_pad 1 0 pc) single_instr
+| Block {value; _} ->
+    pp_node buffer ~pad "Block";
+    pp_statements buffer ~pad value.statements
+
+and pp_single_instr buffer ~pad:(_,pc as pad) = function
+  Cond {value; _} ->
+    pp_node buffer ~pad "Cond";
+    pp_conditional buffer ~pad value
+| CaseInstr {value; _} ->
+    pp_node buffer ~pad "CaseInstr";
+    pp_case pp_instruction buffer ~pad value
+| Assign {value; _} ->
+    pp_node buffer ~pad "Assign";
+    pp_assignment buffer ~pad value
+| Loop loop ->
+    pp_node buffer ~pad "Loop";
+    pp_loop buffer ~pad:(mk_pad 1 0 pc) loop
+| ProcCall {value; _} ->
+    pp_node buffer ~pad "ProcCall";
+    pp_fun_call buffer ~pad value
+| Skip _ ->
+    pp_node buffer ~pad "Skip"
+| RecordPatch {value; _} ->
+    pp_node buffer ~pad "RecordPatch";
+    pp_record_patch buffer ~pad value
+| MapPatch {value; _} ->
+    pp_node buffer ~pad "MapPatch";
+    pp_map_patch buffer ~pad value
+| SetPatch {value; _} ->
+    pp_node buffer ~pad "SetPatch";
+    pp_set_patch buffer ~pad value
+| MapRemove {value; _} ->
+    pp_node buffer ~pad "MapRemove";
+    pp_map_remove buffer ~pad value
+| SetRemove {value; _} ->
+    pp_node buffer ~pad "SetRemove";
+    pp_set_remove buffer ~pad value
+
+and pp_conditional buffer ~pad:(_,pc) cond =
+  let () =
+    let _, pc as pad = mk_pad 3 0 pc in
+    pp_node buffer ~pad "<condition>";
+    pp_expr buffer ~pad:(mk_pad 1 0 pc) cond.test in
+  let () =
+    let _, pc as pad = mk_pad 3 1 pc in
+    pp_node buffer ~pad "<true>";
+    pp_if_clause buffer ~pad:(mk_pad 1 0 pc) cond.ifso in
+  let () =
+    let _, pc as pad = mk_pad 3 2 pc in
+    pp_node buffer ~pad "<false>";
+    pp_if_clause buffer ~pad:(mk_pad 1 0 pc) cond.ifnot
+  in ()
+
+and pp_if_clause buffer ~pad:(_,pc as pad) = function
+  ClauseInstr instr ->
+    pp_node buffer ~pad "ClauseInstr";
+    pp_instruction buffer ~pad:(mk_pad 1 0 pc) instr
+| ClauseBlock {value; _} ->
+    pp_node buffer ~pad "ClauseBlock";
+    let statements, _ = value.inside in
+    pp_statements buffer ~pad statements
+
+and pp_case :
+  'a.(Buffer.t -> pad:(string*string) -> 'a -> unit)
+  -> Buffer.t -> pad:(string*string) -> 'a case -> unit =
+  fun printer buffer ~pad:(_,pc) case ->
+    let clauses = Utils.nsepseq_to_list case.cases.value in
+    let clauses = List.map (fun {value; _} -> value) clauses in
+    let length  = List.length clauses + 1 in
+    let apply len rank =
+      pp_case_clause printer buffer ~pad:(mk_pad len (rank+1) pc)
+    in pp_expr buffer ~pad:(mk_pad length 0 pc) case.expr;
+    List.iteri (apply length) clauses
+
+and pp_case_clause :
+  'a.(Buffer.t -> pad:(string*string) -> 'a -> unit)
+  -> Buffer.t -> pad:(string*string) -> 'a case_clause -> unit =
+  fun printer buffer ~pad:(_,pc as pad) clause ->
+    pp_node buffer ~pad "<clause>";
+    pp_pattern buffer ~pad:(mk_pad 2 0 pc) clause.pattern;
+    printer buffer ~pad:(mk_pad 2 1 pc) clause.rhs
+
+and pp_pattern buffer ~pad:(_,pc as pad) = function
+  PNone _ ->
+    pp_node buffer ~pad "PNone"
+| PSome {value=_,{value=par; _}; _} ->
+    pp_node buffer ~pad "PSome";
+    pp_pattern buffer ~pad:(mk_pad 1 0 pc) par.inside
+| PWild _ ->
+    pp_node buffer ~pad "PWild"
+| PConstr {value; _} ->
+    pp_node buffer ~pad "PConstr";
+    pp_constr_pattern buffer ~pad:(mk_pad 1 0 pc) value
+| PCons {value; _} ->
+    let patterns = Utils.nsepseq_to_list value in
+    let length   = List.length patterns in
+    let apply len rank =
+      pp_pattern buffer ~pad:(mk_pad len rank pc) in
+    pp_node buffer ~pad "PCons";
+    List.iteri (apply length) patterns
+| PVar {value; _} ->
+    pp_node buffer ~pad "PVar";
+    pp_ident buffer ~pad:(mk_pad 1 0 pc) value
+| PInt {value; _} ->
+    pp_node buffer ~pad "PInt";
+    pp_int buffer ~pad value
+| PNat {value; _} ->
+    pp_node buffer ~pad "PNat";
+    pp_int buffer ~pad value
+| PBytes {value; _} ->
+    pp_node buffer ~pad "PBytes";
+    pp_bytes buffer ~pad value
+| PString {value; _} ->
+    pp_node buffer ~pad "PString";
+    pp_ident buffer ~pad:(mk_pad 1 0 pc) value
+| PUnit _ ->
+    pp_node buffer ~pad "PUnit"
+| PFalse _ ->
+    pp_node buffer ~pad "PFalse"
+| PTrue _ ->
+    pp_node buffer ~pad "PTrue"
+| PList plist ->
+    pp_node buffer ~pad "PList";
+    pp_plist buffer ~pad:(mk_pad 1 0 pc) plist
+| PTuple {value; _} ->
+    pp_node buffer ~pad "PTuple";
+    pp_tuple_pattern buffer ~pad:(mk_pad 1 0 pc) value
+
+and pp_bytes buffer ~pad:(_,pc) (lexeme, hex) =
+  pp_string buffer ~pad:(mk_pad 2 0 pc) lexeme;
+  pp_string buffer ~pad:(mk_pad 2 1 pc) (Hex.to_string hex)
+
+and pp_int buffer ~pad:(_,pc) (lexeme, z) =
+  pp_string buffer ~pad:(mk_pad 2 0 pc) lexeme;
+  pp_string buffer ~pad:(mk_pad 2 1 pc) (Z.to_string z)
+
+and pp_constr_pattern buffer ~pad = function
+  {value; _}, None ->
+    pp_ident buffer ~pad value
+| {value=id; _}, Some {value=ptuple; _} ->
+    pp_ident buffer ~pad id;
+    pp_tuple_pattern buffer ~pad ptuple
+
+and pp_plist buffer ~pad:(_,pc as pad) = function
+  Sugar {value; _} ->
+    pp_node buffer ~pad "Sugar";
+    pp_injection pp_pattern buffer ~pad:(mk_pad 1 0 pc) value
+| PNil _ ->
+    pp_node buffer ~pad "PNil"
+| Raw {value; _} ->
+    pp_node buffer ~pad "Raw";
+    pp_raw buffer ~pad:(mk_pad 1 0 pc) value.inside
+
+and pp_raw buffer ~pad:(_,pc) (head, _, tail) =
+  pp_pattern buffer ~pad:(mk_pad 2 0 pc) head;
+  pp_pattern buffer ~pad:(mk_pad 2 1 pc) tail
+
+and pp_injection :
+  'a.(Buffer.t -> pad:(string*string) -> 'a -> unit)
+  -> Buffer.t -> pad:(string*string) -> 'a injection -> unit =
+  fun printer buffer ~pad:(_,pc) inj ->
+  let elements = Utils.sepseq_to_list inj.elements in
+  let length   = List.length elements in
+  let apply len rank = printer buffer ~pad:(mk_pad len rank pc)
+  in List.iteri (apply length) elements
+
+and pp_tuple_pattern buffer ~pad:(_,pc) tuple =
+  let patterns = Utils.nsepseq_to_list tuple.inside in
+  let length   = List.length patterns in
+  let apply len rank =
+    pp_pattern buffer ~pad:(mk_pad len rank pc)
+  in List.iteri (apply length) patterns
+
+and pp_assignment buffer ~pad:(_,pc) asgn =
+  pp_lhs buffer ~pad:(mk_pad 2 0 pc) asgn.lhs;
+  pp_expr buffer ~pad:(mk_pad 2 1 pc) asgn.rhs
+
+and pp_lhs buffer ~pad:(_,pc as pad) = function
+  Path path ->
+    pp_node buffer ~pad "Path";
+    pp_path buffer ~pad:(mk_pad 1 0 pc) path
+| MapPath {value; _} ->
+    pp_node buffer ~pad "MapPath";
+    pp_map_lookup buffer ~pad value
+
+and pp_path buffer ~pad:(_,pc as pad) = function
+  Name {value; _} ->
+    pp_node buffer ~pad "Name";
+    pp_ident buffer ~pad:(mk_pad 1 0 pc) value
+| Path {value; _} ->
+    pp_node buffer ~pad "Path";
+    pp_projection buffer ~pad value
+
+and pp_projection buffer ~pad:(_,pc) proj =
+  let selections = Utils.nsepseq_to_list proj.field_path in
+  let len = List.length selections in
+  let apply len rank =
+    pp_selection buffer ~pad:(mk_pad len rank pc) in
+  pp_ident buffer ~pad:(mk_pad (1+len) 0 pc) proj.struct_name.value;
+  List.iteri (apply len) selections
+
+and pp_selection buffer ~pad:(_,pc as pad) = function
+  FieldName {value; _} ->
+    pp_node buffer ~pad "FieldName";
+    pp_ident buffer ~pad:(mk_pad 1 0 pc) value
+| Component {value; _} ->
+    pp_node buffer ~pad "Component";
+    pp_int buffer ~pad value
+
+and pp_map_lookup buffer ~pad:(_,pc) lookup =
+  pp_path buffer ~pad:(mk_pad 2 0 pc) lookup.path;
+  pp_expr buffer ~pad:(mk_pad 2 1 pc) lookup.index.value.inside
+
+and pp_loop buffer ~pad:(_,pc as pad) = function
+  While {value; _} ->
+    pp_node buffer ~pad "<while>";
+    let () =
+      let _, pc as pad = mk_pad 2 0 pc in
+      pp_node buffer ~pad "<condition>";
+      pp_expr buffer ~pad:(mk_pad 1 0 pc) value.cond in
+    let () =
+      let pad = mk_pad 2 1 pc in
+      let statements = value.block.value.statements in
+      pp_node buffer ~pad "<statements>";
+      pp_statements buffer ~pad statements
+    in ()
+| For for_loop ->
+    pp_node buffer ~pad "<for>";
+    pp_for_loop buffer ~pad:(mk_pad 1 0 pc) for_loop
+
+and pp_for_loop buffer ~pad = function
+  ForInt {value; _} ->
+    pp_node buffer ~pad "ForInt";
+    pp_for_int buffer ~pad value
+| ForCollect {value; _} ->
+    pp_node buffer ~pad "ForCollect";
+    pp_for_collect buffer ~pad value
+
+and pp_for_int buffer ~pad:(_,pc) for_int =
+  let () =
+    let pad = mk_pad 3 0 pc in
+    pp_node buffer ~pad "<init>";
+    pp_var_assign buffer ~pad for_int.assign.value in
+  let () =
+    let _, pc as pad = mk_pad 3 1 pc in
+    pp_node buffer ~pad "<bound>";
+    pp_expr buffer ~pad:(mk_pad 1 0 pc) for_int.bound in
+  let () =
+    let pad = mk_pad 3 2 pc in
+    let statements = for_int.block.value.statements in
+    pp_node buffer ~pad "<statements>";
+    pp_statements buffer ~pad statements
+  in ()
+
+and pp_var_assign buffer ~pad:(_,pc) asgn =
+  let pad = mk_pad 2 0 pc in
+  pp_ident buffer ~pad asgn.name.value;
+  let pad = mk_pad 2 1 pc in
+  pp_expr buffer ~pad asgn.expr
+
+and pp_for_collect buffer ~pad:(_,pc) collect =
+  let () =
+    let pad = mk_pad 4 0 pc in
+    match collect.bind_to with
+      None ->
+        pp_ident buffer ~pad collect.var.value
+    | Some (_, var) ->
+        pp_var_binding buffer ~pad (collect.var, var) in
+  let () =
+    let _, pc  as pad = mk_pad 4 1 pc in
+    pp_node buffer ~pad "<element type>";
+    pp_type_expr buffer ~pad:(mk_pad 1 0 pc) collect.elt_type in
+  let () =
+    let _, pc  as pad = mk_pad 4 2 pc in
+    pp_node buffer ~pad "<collection>";
+    pp_collection buffer ~pad:(mk_pad 2 0 pc) collect.collection;
+    pp_expr buffer ~pad:(mk_pad 1 0 pc) collect.expr in
+  let () =
+      let pad = mk_pad 4 3 pc in
+      let statements = collect.block.value.statements in
+      pp_node buffer ~pad "<statements>";
+      pp_statements buffer ~pad statements
+  in ()
+
+and pp_collection buffer ~pad = function
+  Map  _ -> pp_string buffer ~pad "map"
+| Set  _ -> pp_string buffer ~pad "set"
+| List _ -> pp_string buffer ~pad "list"
+
+and pp_var_binding buffer ~pad:(_,pc as pad) (source, image) =
+  pp_node buffer ~pad "<binding>";
+  pp_ident buffer ~pad:(mk_pad 2 0 pc) source.value;
+  pp_ident buffer ~pad:(mk_pad 2 1 pc) image.value
+
+and pp_fun_call buffer ~pad:(_,pc) (name, args) =
+  let args = Utils.nsepseq_to_list args.value.inside in
+  let arity = List.length args in
+  let apply len rank =
+    pp_expr buffer ~pad:(mk_pad len rank pc)
+  in pp_ident buffer ~pad:(mk_pad (1+arity) 0 pc) name.value;
+    List.iteri (apply arity) args
+
+and pp_record_patch buffer ~pad:(_,pc as pad) patch =
+  pp_path buffer ~pad:(mk_pad 2 0 pc) patch.path;
+  pp_injection pp_field_assign buffer
+    ~pad patch.record_inj.value
+
+and pp_field_assign buffer ~pad:(_,pc as pad) {value; _} =
+  pp_node buffer ~pad "<field assignment>";
+  pp_ident buffer ~pad:(mk_pad 2 0 pc) value.field_name.value;
+  pp_expr  buffer ~pad:(mk_pad 2 1 pc) value.field_expr
+
+and pp_map_patch buffer ~pad:(_,pc as pad) patch =
+  pp_path buffer ~pad:(mk_pad 2 0 pc) patch.path;
+  pp_injection pp_binding buffer
+    ~pad patch.map_inj.value
+
+and pp_binding buffer ~pad:(_,pc as pad) {value; _} =
+  let source, image = value.source, value.image in
+  pp_node buffer ~pad "<binding>";
+  pp_expr buffer ~pad:(mk_pad 2 0 pc) source;
+  pp_expr buffer ~pad:(mk_pad 2 1 pc) image
+
+and pp_set_patch buffer ~pad:(_,pc as pad) patch =
+  pp_path buffer ~pad:(mk_pad 2 0 pc) patch.path;
+  pp_injection pp_expr buffer ~pad patch.set_inj.value
+
+and pp_map_remove buffer ~pad:(_,pc) rem =
+  pp_expr buffer ~pad:(mk_pad 2 0 pc) rem.key;
+  pp_path buffer ~pad:(mk_pad 2 1 pc) rem.map
+
+and pp_set_remove buffer ~pad:(_,pc) rem =
+  pp_expr buffer ~pad:(mk_pad 2 0 pc) rem.element;
+  pp_path buffer ~pad:(mk_pad 2 1 pc) rem.set
+
+and pp_local_decls buffer ~pad:(_,pc) decls =
+  let apply len rank =
+    pp_local_decl buffer ~pad:(mk_pad len rank pc)
+  in List.iteri (List.length decls |> apply) decls
+
+and pp_local_decl buffer ~pad:(_,pc as pad) = function
+  LocalFun {value; _} ->
+    pp_node buffer ~pad "LocalFun";
+    pp_fun_decl buffer ~pad:(mk_pad 1 0 pc) value
+| LocalData data ->
+    pp_node buffer ~pad "LocalData";
+    pp_data_decl buffer ~pad:(mk_pad 1 0 pc) data
+
+and pp_data_decl buffer ~pad = function
+  LocalConst {value; _} ->
+    pp_node buffer ~pad "LocalConst";
+    pp_const_decl buffer ~pad value
+| LocalVar {value; _} ->
+    pp_node buffer ~pad "LocalVar";
+    pp_var_decl buffer ~pad value
+
+and pp_var_decl buffer ~pad:(_,pc) decl =
+  pp_ident     buffer ~pad:(mk_pad 3 0 pc) decl.name.value;
+  pp_type_expr buffer ~pad:(mk_pad 3 1 pc) decl.var_type;
+  pp_expr      buffer ~pad:(mk_pad 3 2 pc) decl.init
+
+and pp_expr buffer ~pad:(_,pc as pad) = function
+  ECase {value; _} ->
+    pp_node buffer ~pad "ECase";
+    pp_case pp_expr buffer ~pad value
+| EAnnot {value; _} ->
+    pp_node buffer ~pad "EAnnot";
+    pp_annotated buffer ~pad value
+| ELogic e_logic ->
+    pp_node buffer ~pad "ELogic";
+    pp_e_logic buffer ~pad:(mk_pad 1 0 pc) e_logic
+| EArith e_arith ->
+    pp_node buffer ~pad "EArith";
+    pp_arith_expr buffer ~pad:(mk_pad 1 0 pc) e_arith
+| EString e_string ->
+    pp_node buffer ~pad "EString";
+    pp_string_expr buffer ~pad:(mk_pad 1 0 pc) e_string
+| EList e_list ->
+    pp_node buffer ~pad "EList";
+    pp_list_expr buffer ~pad:(mk_pad 1 0 pc) e_list
+| ESet e_set ->
+    pp_node buffer ~pad "ESet";
+    pp_set_expr buffer ~pad:(mk_pad 1 0 pc) e_set
+| EConstr e_constr ->
+    pp_node buffer ~pad "EConstr";
+    pp_constr_expr buffer ~pad:(mk_pad 1 0 pc) e_constr
+| ERecord {value; _} ->
+    pp_node buffer ~pad "ERecord";
+    pp_injection pp_field_assign buffer ~pad value
+| EProj {value; _} ->
+    pp_node buffer ~pad "EProj";
+    pp_projection buffer ~pad value
+| EMap e_map ->
+    pp_node buffer ~pad "EMap";
+    pp_map_expr buffer ~pad:(mk_pad 1 0 pc) e_map
+| EVar {value; _} ->
+    pp_node buffer ~pad "EVar";
+    pp_ident buffer ~pad:(mk_pad 1 0 pc) value
+| ECall {value; _} ->
+    pp_node buffer ~pad "ECall";
+    pp_fun_call buffer ~pad value
+| EBytes {value; _} ->
+    pp_node buffer ~pad "EBytes";
+    pp_bytes buffer ~pad value
+| EUnit _ ->
+    pp_node buffer ~pad "EUnit"
+| ETuple e_tuple ->
+    pp_node buffer ~pad "ETuple";
+    pp_tuple_expr buffer ~pad e_tuple
+| EPar {value; _} ->
+    pp_node buffer ~pad "EPar";
+    pp_expr buffer ~pad:(mk_pad 1 0 pc) value.inside
+
+and pp_list_expr buffer ~pad:(_,pc as pad) = function
+  Cons {value; _} ->
+    pp_node buffer ~pad "Cons";
+    pp_expr buffer ~pad:(mk_pad 2 0 pc) value.arg1;
+    pp_expr buffer ~pad:(mk_pad 2 1 pc) value.arg2
+| List {value; _} ->
+    pp_node buffer ~pad "List";
+    pp_injection pp_expr buffer ~pad value
+| Nil _ ->
+    pp_node buffer ~pad "Nil"
+
+and pp_arith_expr buffer ~pad:(_,pc as pad) = function
+  Add {value; _} ->
+    pp_bin_op "Add" buffer ~pad value
+| Sub {value; _} ->
+    pp_bin_op "Sub" buffer ~pad value
+| Mult {value; _} ->
+    pp_bin_op "Mult" buffer ~pad value
+| Div {value; _} ->
+    pp_bin_op "Div" buffer ~pad value
+| Mod {value; _} ->
+    pp_bin_op "Mod" buffer ~pad value
+| Neg {value; _} ->
+    pp_node buffer ~pad "Neg";
+    pp_expr buffer ~pad:(mk_pad 1 0 pc) value.arg;
+| Int {value; _} ->
+    pp_node buffer ~pad "Int";
+    pp_int  buffer ~pad value
+| Nat {value; _} ->
+    pp_node buffer ~pad "Nat";
+    pp_int  buffer ~pad value
+| Mtz {value; _} ->
+    pp_node buffer ~pad "Mtz";
+    pp_int  buffer ~pad value
+
+and pp_set_expr buffer ~pad:(_,pc as pad) = function
+  SetInj {value; _} ->
+    pp_node buffer ~pad "SetInj";
+    pp_injection pp_expr buffer ~pad value
+| SetMem {value; _} ->
+    pp_node buffer ~pad "SetMem";
+    pp_expr buffer ~pad:(mk_pad 2 0 pc) value.set;
+    pp_expr buffer ~pad:(mk_pad 2 1 pc) value.element
+
+and pp_e_logic buffer ~pad = function
+  BoolExpr e ->
+    pp_node buffer ~pad "BoolExpr";
+    pp_bool_expr buffer ~pad e
+| CompExpr e ->
+    pp_node buffer ~pad "CompExpr";
+    pp_comp_expr buffer ~pad e
+
+and pp_bool_expr buffer ~pad:(_,pc as pad) = function
+  Or {value; _} ->
+    pp_bin_op "Or" buffer ~pad value
+| And {value; _} ->
+    pp_bin_op "And" buffer ~pad value
+| Not {value; _} ->
+    let _, pc as pad = mk_pad 1 0 pc in
+    pp_node buffer ~pad "Not";
+    pp_expr buffer ~pad:(mk_pad 1 0 pc) value.arg
+| False _ ->
+    pp_node buffer ~pad:(mk_pad 1 0 pc) "False"
+| True _ ->
+    pp_node buffer ~pad:(mk_pad 1 0 pc) "True"
+
+and pp_comp_expr buffer ~pad = function
+  Lt {value; _} ->
+    pp_bin_op "Lt" buffer ~pad value
+| Leq {value; _} ->
+    pp_bin_op "Leq" buffer ~pad value
+| Gt {value; _} ->
+    pp_bin_op "Gt" buffer ~pad value
+| Geq {value; _} ->
+    pp_bin_op "Geq" buffer ~pad value
+| Equal {value; _} ->
+    pp_bin_op "Equal" buffer ~pad value
+| Neq {value; _} ->
+    pp_bin_op "Neq" buffer ~pad value
+
+and pp_constr_expr buffer ~pad:(_, pc as pad) = function
+  SomeApp {value=some_region,args; _} ->
+    let constr = {value="Some"; region=some_region} in
+    let app = constr, Some args in
+    pp_node buffer ~pad "SomeApp";
+    pp_constr_app buffer ~pad app
+| NoneExpr _ ->
+    pp_node buffer ~pad "NoneExpr"
+| ConstrApp {value; _} ->
+    pp_node buffer ~pad "ConstrApp";
+    pp_constr_app buffer ~pad:(mk_pad 1 0 pc) value
+
+and pp_constr_app buffer ~pad (constr, args_opt) =
+  pp_ident buffer ~pad constr.value;
+  match args_opt with
+         None -> ()
+  | Some args -> pp_tuple_expr buffer ~pad args
+
+and pp_map_expr buffer ~pad = function
+  MapLookUp {value; _} ->
+    pp_node buffer ~pad "MapLookUp";
+    pp_map_lookup buffer ~pad value
+| MapInj {value; _} ->
+    pp_node buffer ~pad "MapInj";
+    pp_injection pp_binding buffer ~pad value
+
+and pp_tuple_expr buffer ~pad:(_,pc) {value; _} =
+  let exprs  = Utils.nsepseq_to_list value.inside in
+  let length = List.length exprs in
+  let apply len rank =
+    pp_expr buffer ~pad:(mk_pad len rank pc)
+  in List.iteri (apply length) exprs
+
+and pp_string_expr buffer ~pad:(_,pc as pad) = function
+  Cat {value; _} ->
+    pp_node buffer ~pad "Cat";
+    pp_expr buffer ~pad:(mk_pad 2 0 pc) value.arg1;
+    pp_expr buffer ~pad:(mk_pad 2 1 pc) value.arg2;
+| String {value; _} ->
+    pp_node buffer ~pad "String";
+    pp_string buffer ~pad:(mk_pad 1 0 pc) value
+
+and pp_annotated buffer ~pad:(_,pc) (expr, t_expr) =
+  pp_expr buffer ~pad:(mk_pad 2 0 pc) expr;
+  pp_type_expr buffer ~pad:(mk_pad 2 1 pc) t_expr
+
+and pp_bin_op node buffer ~pad:(_,pc) op =
+  pp_node buffer ~pad:(mk_pad 1 0 pc) node;
+  let _, pc = mk_pad 1 0 pc in
+  (pp_expr buffer ~pad:(mk_pad 2 0 pc) op.arg1;
+   pp_expr buffer ~pad:(mk_pad 2 1 pc) op.arg2)
+
+let pp_ast buffer = pp_ast buffer ~pad:("","")
diff --git a/src/passes/1-parser/pascaligo/ParserLog.mli b/src/passes/1-parser/pascaligo/ParserLog.mli
index ad0c3f4f3..bf53dc3e2 100644
--- a/src/passes/1-parser/pascaligo/ParserLog.mli
+++ b/src/passes/1-parser/pascaligo/ParserLog.mli
@@ -12,3 +12,5 @@ val tokens_to_string      : AST.t -> string
 val path_to_string        : AST.path -> string
 val pattern_to_string     : AST.pattern -> string
 val instruction_to_string : AST.instruction -> string
+
+val pp_ast : Buffer.t -> AST.t -> unit
diff --git a/src/passes/1-parser/pascaligo/ParserMain.ml b/src/passes/1-parser/pascaligo/ParserMain.ml
index 70d8a8542..5fa99ab76 100644
--- a/src/passes/1-parser/pascaligo/ParserMain.ml
+++ b/src/passes/1-parser/pascaligo/ParserMain.ml
@@ -103,6 +103,14 @@ let () =
   try
     let ast = Parser.contract tokeniser buffer in
     if Utils.String.Set.mem "ast" options.verbose
+    then let buffer = Buffer.create 131 in
+         begin
+           ParserLog.offsets := options.offsets;
+           ParserLog.mode    := options.mode;
+           ParserLog.pp_ast buffer ast;
+           Buffer.output_buffer stdout buffer
+         end
+    else if Utils.String.Set.mem "ast-tokens" options.verbose
     then let buffer = Buffer.create 131 in
          begin
            ParserLog.offsets := options.offsets;
diff --git a/src/passes/1-parser/shared/EvalOpt.ml b/src/passes/1-parser/shared/EvalOpt.ml
index 44bb9adc8..a4508ab30 100644
--- a/src/passes/1-parser/shared/EvalOpt.ml
+++ b/src/passes/1-parser/shared/EvalOpt.ml
@@ -39,7 +39,7 @@ let help language extension () =
   print "  -q, --quiet            No output, except errors (default)";
   print "      --columns          Columns for source locations";
   print "      --bytes            Bytes for source locations";
-  print "      --verbose=<stages> cmdline, cpp, ast (colon-separated)";
+  print "      --verbose=<stages> cmdline, cpp, ast-tokens, ast (colon-separated)";
   print "      --version          Commit hash on stdout";
   print "  -h, --help             This help";
   exit 0
diff --git a/src/passes/1-parser/shared/Lexer.mli b/src/passes/1-parser/shared/Lexer.mli
index 7d4cbb810..8f56ac87e 100644
--- a/src/passes/1-parser/shared/Lexer.mli
+++ b/src/passes/1-parser/shared/Lexer.mli
@@ -60,22 +60,22 @@ module type TOKEN =
 
     (* Errors *)
 
-    type   int_err       = Non_canonical_zero
-    type ident_err       = Reserved_name
-    type invalid_natural = 
-      | Invalid_natural
-      | Non_canonical_zero_nat
+    type   int_err = Non_canonical_zero
+    type ident_err = Reserved_name
+    type   nat_err = Invalid_natural
+                   | Non_canonical_zero_nat
+    type   sym_err = Invalid_symbol
 
     (* Injections *)
 
-    val mk_string : lexeme -> Region.t -> token
-    val mk_bytes  : lexeme -> Region.t -> token
     val mk_int    : lexeme -> Region.t -> (token,   int_err) result
-    val mk_nat    : lexeme -> Region.t -> (token,   invalid_natural) result
+    val mk_nat    : lexeme -> Region.t -> (token,   nat_err) result
     val mk_mtz    : lexeme -> Region.t -> (token,   int_err) result
     val mk_ident  : lexeme -> Region.t -> (token, ident_err) result
+    val mk_sym    : lexeme -> Region.t -> (token,   sym_err) result
+    val mk_string : lexeme -> Region.t -> token
+    val mk_bytes  : lexeme -> Region.t -> token
     val mk_constr : lexeme -> Region.t -> token
-    val mk_sym    : lexeme -> Region.t -> token
     val eof       : Region.t -> token
 
     (* Predicates *)
diff --git a/src/passes/1-parser/shared/Lexer.mll b/src/passes/1-parser/shared/Lexer.mll
index f2172595f..012d8b6b6 100644
--- a/src/passes/1-parser/shared/Lexer.mll
+++ b/src/passes/1-parser/shared/Lexer.mll
@@ -101,22 +101,22 @@ module type TOKEN =
 
     (* Errors *)
 
-    type   int_err       = Non_canonical_zero
-    type ident_err       = Reserved_name
-    type invalid_natural =
-      | Invalid_natural
-      | Non_canonical_zero_nat
+    type   int_err = Non_canonical_zero
+    type ident_err = Reserved_name
+    type   nat_err = Invalid_natural
+                   | Non_canonical_zero_nat
+    type   sym_err = Invalid_symbol
 
     (* Injections *)
 
-    val mk_string : lexeme -> Region.t -> token
-    val mk_bytes  : lexeme -> Region.t -> token
     val mk_int    : lexeme -> Region.t -> (token,   int_err) result
-    val mk_nat    : lexeme -> Region.t -> (token,   invalid_natural) result
+    val mk_nat    : lexeme -> Region.t -> (token,   nat_err) result
     val mk_mtz    : lexeme -> Region.t -> (token,   int_err) result
     val mk_ident  : lexeme -> Region.t -> (token, ident_err) result
+    val mk_sym    : lexeme -> Region.t -> (token,   sym_err) result
+    val mk_string : lexeme -> Region.t -> token
+    val mk_bytes  : lexeme -> Region.t -> token
     val mk_constr : lexeme -> Region.t -> token
-    val mk_sym    : lexeme -> Region.t -> token
     val eof       : Region.t -> token
 
     (* Predicates *)
@@ -343,6 +343,7 @@ module Make (Token: TOKEN) : (S with module Token = Token) =
     type Error.t += Broken_string
     type Error.t += Invalid_character_in_string
     type Error.t += Reserved_name
+    type Error.t += Invalid_symbol
     type Error.t += Invalid_natural
 
     let error_to_string = function
@@ -386,6 +387,9 @@ module Make (Token: TOKEN) : (S with module Token = Token) =
     | Reserved_name ->
         "Reserved named.\n\
          Hint: Change the name.\n"
+    | Invalid_symbol ->
+        "Invalid symbol.\n\
+         Hint: Check the LIGO syntax you use.\n"
     | Invalid_natural ->
         "Invalid natural."
     | _ -> assert false
@@ -487,8 +491,10 @@ module Make (Token: TOKEN) : (S with module Token = Token) =
       in Token.mk_constr lexeme region, state
 
     let mk_sym state buffer =
-      let region, lexeme, state = sync state buffer
-      in Token.mk_sym lexeme region, state
+      let region, lexeme, state = sync state buffer in
+      match Token.mk_sym lexeme region with
+        Ok token -> token, state
+      | Error Token.Invalid_symbol -> fail region Invalid_symbol
 
     let mk_eof state buffer =
       let region, _, state = sync state buffer
@@ -518,12 +524,17 @@ let byte_seq   = byte | byte (byte | '_')* byte
 let bytes      = "0x" (byte_seq? as seq)
 let esc        = "\\n" | "\\\"" | "\\\\" | "\\b"
                | "\\r" | "\\t" | "\\x" byte
-let symbol     = ';' | ',' | '(' | ')'| '[' | ']' | '{' | '}'
-               | '#' | '|' | "->" | ":=" | '=' | ':'
-               | '<' | "<=" | '>' | ">=" | "=/=" | "<>"
-               | '+' | '-' | '*' | '/' | '.' | '_' | '^'
-               | "::" | "||" | "&&"
-let string     = [^'"' '\\' '\n']*  (* For strings of #include *)
+let pascaligo_sym = "=/=" | '#' | ":="
+let cameligo_sym = "<>" | "::" | "||" | "&&"
+
+let symbol =
+  ';' | ',' | '(' | ')'| '[' | ']' | '{' | '}'
+| '=' | ':' | '|' | "->" | '.' | '_' | '^'
+| '+' | '-' | '*' | '/'
+| '<' | "<=" | '>' | ">="
+| pascaligo_sym | cameligo_sym
+
+let string = [^'"' '\\' '\n']*  (* For strings of #include *)
 
 (* RULES *)
 
diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml
index 40b508e9b..919976d1f 100644
--- a/src/passes/2-simplify/pascaligo.ml
+++ b/src/passes/2-simplify/pascaligo.ml
@@ -35,26 +35,6 @@ module Errors = struct
     ] in
     error ~data title message
 
-  let unsupported_proc_decl decl =
-    let title () = "procedure declarations" in
-    let message () =
-      Format.asprintf "procedures are not supported yet" in
-    let data = [
-      ("declaration",
-       fun () -> Format.asprintf "%a" Location.pp_lift @@ decl.Region.region)
-    ] in
-    error ~data title message
-
-  let unsupported_local_proc region =
-    let title () = "local procedure declarations" in
-    let message () =
-      Format.asprintf "local procedures are not supported yet" in
-    let data = [
-      ("declaration",
-       fun () -> Format.asprintf "%a" Location.pp_lift @@ region)
-    ] in
-    error ~data title message
-
   let corner_case ~loc message =
     let title () = "corner case" in
     let content () = "We don't have a good error message for this case. \
@@ -88,16 +68,6 @@ module Errors = struct
     ] in
     error ~data title message
 
-  let unsupported_proc_calls call =
-    let title () = "procedure calls" in
-    let message () =
-      Format.asprintf "procedure calls are not supported yet" in
-    let data = [
-      ("call_loc",
-       fun () -> Format.asprintf "%a" Location.pp_lift @@ call.Region.region)
-    ] in
-    error ~data title message
-
   let unsupported_for_loops region =
     let title () = "bounded iterators" in
     let message () =
@@ -273,10 +243,11 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
         let args =
           match v.value.args with
             None -> []
-          | Some (_, product) ->
-              npseq_to_list product.value in
-        let%bind te = simpl_list_type_expression
-          @@ args in
+          | Some (_, t_expr) ->
+              match t_expr with
+                TProd product -> npseq_to_list product.value
+              | _ -> [t_expr] in
+        let%bind te = simpl_list_type_expression @@ args in
         ok (v.value.constr.value, te)
       in
       let%bind lst = bind_list
@@ -345,8 +316,7 @@ let rec simpl_expression (t:Raw.expr) : expr result =
     let (x' , loc) = r_split x in
     return @@ e_literal ~loc (Literal_bytes (Bytes.of_string @@ fst x'))
   | ETuple tpl ->
-      let (Raw.TupleInj tpl') = tpl in
-      let (tpl' , loc) = r_split tpl' in
+      let (tpl' , loc) = r_split tpl in
       simpl_tuple_expression ~loc @@ npseq_to_list tpl'.inside
   | ERecord r ->
       let%bind fields = bind_list
@@ -550,8 +520,7 @@ and simpl_local_declaration : Raw.local_decl -> _ result = fun t ->
       let (f , loc) = r_split f in
       let%bind (name , e) = simpl_fun_declaration ~loc f in
       return_let_in ~loc name e
-  | LocalProc d ->
-      fail @@ unsupported_local_proc d.Region.region
+
 and simpl_data_declaration : Raw.data_decl -> _ result = fun t ->
   match t with
   | LocalVar x ->
@@ -659,13 +628,11 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result =
         ok @@ Declaration_constant (name.value , type_annotation , expression)
       in
       bind_map_location simpl_const_decl (Location.lift_region x)
-  | LambdaDecl (FunDecl x) -> (
+  | FunDecl x -> (
       let (x , loc) = r_split x in
       let%bind ((name , ty_opt) , expr) = simpl_fun_declaration ~loc x in
       ok @@ Location.wrap ~loc (Declaration_constant (name , ty_opt , expr))
     )
-  | LambdaDecl (ProcDecl decl) ->
-      fail @@ unsupported_proc_decl decl
 
 and simpl_statement : Raw.statement -> (_ -> expression result) result =
   fun s ->
@@ -728,7 +695,7 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
               | Name name -> ok (name.value , e_variable name.value, [])
               | Path p ->
                 let (name,p') = simpl_path v'.path in
-                let%bind accessor = simpl_projection p in 
+                let%bind accessor = simpl_projection p in
                 ok @@ (name , accessor , p')
             in
             let%bind key_expr = simpl_expression v'.index.value.inside in
@@ -882,7 +849,7 @@ and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -
         | [] -> ok x'
         | _ -> ok t
       )
-    | _ -> fail @@ corner_case ~loc:__LOC__ "unexpected pattern" in
+    | pattern -> ok pattern in
   let get_constr (t: Raw.pattern) =
     match t with
     | PConstr v -> (
diff --git a/src/passes/2-simplify/pascaligo.mli b/src/passes/2-simplify/pascaligo.mli
index c04edcf72..f0e63026a 100644
--- a/src/passes/2-simplify/pascaligo.mli
+++ b/src/passes/2-simplify/pascaligo.mli
@@ -6,21 +6,17 @@ open Ast_simplified
 module Raw = Parser.Pascaligo.AST
 module SMap = Map.String
 
-module Errors : sig
-
-  val bad_bytes : Location.t -> string -> unit -> error
-
-  val unsupported_arith_op : Raw.expr -> unit -> error
-
-  val unsupported_proc_calls : 'a Raw.reg -> unit -> error
-
-end
+module Errors :
+  sig
+    val bad_bytes : Location.t -> string -> unit -> error
+    val unsupported_arith_op : Raw.expr -> unit -> error
+  end
 
 
-(** Convert a concrete PascaLIGO expression AST to the simplified expression AST 
+(** Convert a concrete PascaLIGO expression AST to the simplified expression AST
     used by the compiler. *)
 val simpl_expression : Raw.expr -> expr result
 
-(** Convert a concrete PascaLIGO program AST to the simplified program AST used 
+(** Convert a concrete PascaLIGO program AST to the simplified program AST used
     by the compiler. *)
 val simpl_program : Raw.ast -> program result