diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml
index b121ccd66..ab1747ffd 100644
--- a/src/ligo/ast_simplified.ml
+++ b/src/ligo/ast_simplified.ml
@@ -31,7 +31,7 @@ and named_type_expression = {
 and te = type_expression
 and ae = annotated_expression
 and te_map = type_expression type_name_map
-and e_map = expression name_map
+and ae_map = annotated_expression name_map
 
 and type_expression =
   | Type_tuple of te list
@@ -41,17 +41,25 @@ and type_expression =
   | Type_constant of type_name * te list
 
 and expression =
+  (* Base *)
   | Literal of literal
   | Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *)
   | Variable of name
-  | Tuple of ae list
-  | Constructor of name * ae list (* For user defined constructors *)
   | Lambda of {
       binder: name ;
       input_type: type_expression ;
       output_type: type_expression ;
+      result: ae ;
       body: block ;
     }
+  (* Tuple *)
+  | Tuple of ae list
+  | Tuple_accessor of ae * int (* Access n'th tuple's element *)
+  (* Sum *)
+  | Constructor of name * ae (* For user defined constructors *)
+  (* Record *)
+  | Record of ae_map
+  | Record_accessor of ae * string
 
 and literal =
   | Bool of bool
@@ -64,7 +72,7 @@ and b = block
 
 and instruction =
   | Assignment of named_expression
-  | Matching of matching
+  | Matching of ae * matching
   | Loop of ae * b
   | Skip
   | Fail of ae
diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml
index 2a22d710f..3ad88684f 100644
--- a/src/ligo/ast_typed.ml
+++ b/src/ligo/ast_typed.ml
@@ -28,7 +28,7 @@ and named_expression = {
 and tv = type_value
 and ae = annotated_expression
 and tv_map = type_value type_name_map
-and e_map = expression name_map
+and ae_map = annotated_expression name_map
 
 and type_value =
   | Type_tuple of tv list
@@ -37,21 +37,31 @@ and type_value =
   | Type_constant of type_name * tv list
 
 and expression =
+  (* Base *)
   | Literal of literal
   | Constant of name * ae list (* For language constants, like (Cons hd tl) or (plus i j) *)
   | Variable of name
-  | Tuple of ae list
-  | Constructor of name * ae list (* For user defined constructors *)
   | Lambda of {
       binder: name ;
-      input_type: type_value ;
-      output_type: type_value ;
+      input_type: tv ;
+      output_type: tv ;
+      result: ae ;
       body: block ;
     }
+  (* Tuple *)
+  | Tuple of ae list
+  | Tuple_accessor of ae * int (* Access n'th tuple's element *)
+  (* Sum *)
+  | Constructor of name * ae (* For user defined constructors *)
+  (* Record *)
+  | Record of ae_map
+  | Record_accessor of ae * string
+
 
 and literal =
   | Bool of bool
-  | Number of int
+  | Int of int
+  | Nat of int
   | String of string
   | Bytes of bytes
 
@@ -60,7 +70,7 @@ and b = block
 
 and instruction =
   | Assignment of named_expression
-  | Matching of matching
+  | Matching of ae * matching
   | Loop of ae * b
   | Skip
   | Fail of ae
@@ -127,11 +137,29 @@ let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab w
     )
   | _ -> simple_fail "Different kinds of types"
 
-let merge_annotation (a:type_value option) (b:type_value option) : type_value option result =
+let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
   match a, b with
-  | None, None -> ok None
-  | Some a, None -> ok (Some a)
-  | None, Some b -> ok (Some b)
+  | None, None -> simple_fail "no annotation"
+  | Some a, None -> ok a
+  | None, Some b -> ok b
   | Some a, Some b ->
       let%bind _ = type_value_eq (a, b) in
-      ok (Some a)
+      ok a
+
+let t_bool : type_value = Type_constant ("bool", [])
+let t_string : type_value = Type_constant ("string", [])
+let t_int : type_value = Type_constant ("int", [])
+
+let get_annotation (x:annotated_expression) = x.type_annotation
+
+let get_t_tuple : type_value -> type_value list result = function
+  | Type_tuple lst -> ok lst
+  | _ -> simple_fail "not a tuple"
+
+let get_t_sum : type_value -> type_value SMap.t result = function
+  | Type_sum m -> ok m
+  | _ -> simple_fail "not a sum"
+
+let get_t_record : type_value -> type_value SMap.t result = function
+  | Type_record m -> ok m
+  | _ -> simple_fail "not a record"
diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml
index ad1b17036..33345f98c 100644
--- a/src/ligo/mini_c.ml
+++ b/src/ligo/mini_c.ml
@@ -1225,6 +1225,82 @@ module Run = struct
 
 end
 
+module Translate_new_AST = struct
+
+  module AST = Ast_typed
+
+  let list_of_map m = List.rev @@ Ligo_helpers.X_map.String.fold (fun _ v prev -> v :: prev) m []
+
+  let rec translate_type (t:AST.type_value) : type_value result =
+    match t with
+    | Type_constant ("bool", []) -> ok (`Base Bool)
+    | Type_constant ("int", []) -> ok (`Base Int)
+    | Type_constant ("string", []) -> ok (`Base String)
+    | Type_sum m ->
+        let node = Append_tree.of_list @@ list_of_map m in
+        let aux a b : type_value result =
+          let%bind a = a in
+          let%bind b = b in
+          ok (`Or (a, b))
+        in
+        Append_tree.fold_ne translate_type aux node
+    | Type_record m ->
+        let node = Append_tree.of_list @@ list_of_map m in
+        let aux a b : type_value result =
+          let%bind a = a in
+          let%bind b = b in
+          ok (`Pair (a, b))
+        in
+        Append_tree.fold_ne translate_type aux node
+    | Type_tuple lst ->
+        let node = Append_tree.of_list lst in
+        let aux a b : type_value result =
+          let%bind a = a in
+          let%bind b = b in
+          ok (`Pair (a, b))
+        in
+        Append_tree.fold_ne translate_type aux node
+    | _ -> simple_fail "todo"
+
+  let rec translate_block (b:AST.block) : block result =
+    bind_list @@ List.map translate_instruction b
+
+  and translate_instruction (i:AST.instruction) : statement result =
+    match i with
+    | Assignment {name;annotated_expression} ->
+        let%bind expression = translate_annotated_expression annotated_expression in
+        ok @@ Assignment (Variable (name, expression))
+    | Matching (expr, Match_bool {match_true ; match_false}) ->
+        let%bind expr' = translate_annotated_expression expr in
+        let%bind true_branch = translate_block match_true in
+        let%bind false_branch = translate_block match_false in
+        ok @@ Cond (expr', true_branch, false_branch)
+    | Loop (expr, body) ->
+        let%bind expr' = translate_annotated_expression expr in
+        let%bind body' = translate_block body in
+        ok @@ While (expr', body')
+    | _ -> simple_fail "todo"
+
+  and translate_annotated_expression (ae:AST.annotated_expression) : expression result =
+    let%bind tv = translate_type ae.type_annotation in
+    match ae.expression with
+    | Literal (Bool b) -> ok (Literal (`Bool b), tv)
+    | Literal (Number n) -> ok (Literal (`Int n), tv)
+    | Literal (String s) -> ok (Literal (`String s), tv)
+    | Variable name -> ok (Var name, tv)
+    | _ -> simple_fail "todo"
+
+
+  let translate_declaration (d:AST.declaration) : toplevel_statement result =
+    match d with
+    | Constant_declaration {name;annotated_expression} ->
+        let%bind expression = translate_annotated_expression annotated_expression in
+        ok @@ Variable (name, expression)
+
+  let translate_program (lst:AST.program) : program result =
+    bind_list @@ List.map translate_declaration lst
+end
+
 module Combinators = struct
 
   let var x : expression' = Var x
diff --git a/src/ligo/type_ast.ml b/src/ligo/type_ast.ml
index 82f4bd471..97b7ced20 100644
--- a/src/ligo/type_ast.ml
+++ b/src/ligo/type_ast.ml
@@ -6,20 +6,36 @@ module O = Ast_typed
 module SMap = O.SMap
 
 module Environment = struct
-  type t = unit
-  let empty : t = ()
+  type ele = O.type_value
 
-  let get (():t) (_s:string) : O.type_value option = None
-  let add (():t) (_s:string) (_tv:O.type_value) : t = ()
-  let get_type (():t) (_s:string) : O.type_value option = None
-  let add_type (():t) (_s:string) (_tv:O.type_value) : t = ()
+  type t = {
+    environment: (string * ele) list ;
+    type_environment: (string * ele) list ;
+  }
+  let empty : t = {
+    environment = [] ;
+    type_environment = [] ;
+  }
+
+  let get (e:t) (s:string) : ele option =
+    List.assoc_opt s e.environment
+  let get_constructor (e:t) (s:string) : (ele * ele) option =
+    let rec aux = function
+      | [] -> None
+      | (_, ((O.Type_sum m) as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv)
+      | _ :: tl -> aux tl
+    in
+    aux e.environment
+  let add (e:t) (s:string) (tv:ele) : t =
+    {e with environment = (s, tv) :: e.environment}
+  let get_type (e:t) (s:string) : ele option =
+    List.assoc_opt s e.type_environment
+  let add_type (e:t) (s:string) (tv:ele) : t =
+    {e with type_environment = (s, tv) :: e.type_environment}
 end
 
 type environment = Environment.t
 
-type environment = unit
-let empty : environment = ()
-
 let rec type_program (p:I.program) : O.program result =
   let aux (e, acc:(environment * O.declaration list)) (d:I.declaration) =
     let%bind (e', d') = type_declaration e d in
@@ -27,12 +43,18 @@ let rec type_program (p:I.program) : O.program result =
     | None -> ok (e', acc)
     | Some d' -> ok (e', d' :: acc)
   in
-  let%bind (_, lst) = bind_fold_list aux (empty, []) p in
+  let%bind (_, lst) = bind_fold_list aux (Environment.empty, []) p in
   ok @@ List.rev lst
 
-and type_declaration _env : I.declaration -> (environment * O.declaration option) result = function
-  | Type_declaration _ -> simple_fail ""
-  | Constant_declaration _ -> simple_fail ""
+and type_declaration env : I.declaration -> (environment * O.declaration option) result = function
+  | Type_declaration {type_name;type_expression} ->
+      let%bind tv = evaluate_type env type_expression in
+      let env' = Environment.add_type env type_name tv in
+      ok (env', None)
+  | Constant_declaration {name;annotated_expression} ->
+      let%bind ae' = type_annotated_expression env annotated_expression in
+      let env' = Environment.add env name ae'.type_annotation in
+      ok (env', Some (O.Constant_declaration {name;annotated_expression=ae'}))
 
 and type_block (e:environment) (b:I.block) : O.block result =
   let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) =
@@ -73,9 +95,10 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
           let e' = Environment.add e name annotated_expression.type_annotation in
           ok (e', O.Assignment {name;annotated_expression})
     )
-  | Matching m ->
+  | Matching (ex, m) ->
       let%bind m' = type_match e m in
-      ok (e, O.Matching m')
+      let%bind ex' = type_annotated_expression e ex in
+      ok (e, O.Matching (ex', m'))
 
 and type_match (e:environment) : I.matching -> O.matching result = function
   | Match_bool {match_true ; match_false} ->
@@ -129,10 +152,66 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f
       ok (O.Type_constant(cst, lst'))
 
 and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.annotated_expression result =
+  let%bind tv_opt = match ae.type_annotation with
+    | None -> ok None
+    | Some s -> let%bind r = evaluate_type e s in ok (Some r) in
+  let check tv = O.merge_annotation (Some tv) tv_opt in
   match ae.expression with
+  (* Basic *)
   | Variable name ->
       let%bind tv' =
         trace_option (simple_error "var not in env")
         @@ Environment.get e name in
-      ok O.{expression = Variable name ; type_annotation = tv'}
+      let%bind type_annotation = check tv' in
+      ok O.{expression = Variable name ; type_annotation}
+  | Literal (Bool b) ->
+      let%bind type_annotation = check O.t_bool in
+      ok O.{expression = Literal (Bool b) ; type_annotation }
+  | Literal (String s) ->
+      let%bind type_annotation = check O.t_string in
+      ok O.{expression = Literal (String s) ; type_annotation }
+  | Literal (Number n) ->
+      let%bind type_annotation = check O.t_int in
+      ok O.{expression = Literal (Int n) ; type_annotation }
+  (* Tuple *)
+  | Tuple lst ->
+      let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
+      let tv_lst = List.map O.get_annotation lst' in
+      let%bind type_annotation = check (O.Type_tuple tv_lst) in
+      ok O.{expression = Tuple lst' ; type_annotation }
+  | Tuple_accessor (tpl, ind) ->
+      let%bind tpl' = type_annotated_expression e tpl in
+      let%bind tpl_tv = O.get_t_tuple tpl'.type_annotation in
+      let%bind tv =
+        generic_try (simple_error "bad tuple index")
+        @@ (fun () -> List.nth tpl_tv ind) in
+      let%bind type_annotation = check tv in
+      ok O.{expression = O.Tuple_accessor (tpl', ind) ; type_annotation}
+  (* Sum *)
+  | Constructor (c, expr) ->
+      let%bind (c_tv, sum_tv) =
+        trace_option (simple_error "no such constructor")
+        @@ Environment.get_constructor e c in
+      let%bind expr' = type_annotated_expression e expr in
+      let%bind _assert = O.type_value_eq (expr'.type_annotation, c_tv) in
+      let%bind type_annotation = check sum_tv in
+      ok O.{expression = O.Constructor(c, expr') ; type_annotation }
+  (* Record *)
+  | Record m ->
+      let aux k expr prev =
+        let%bind prev' = prev in
+        let%bind expr' = type_annotated_expression e expr in
+        ok (SMap.add k expr' prev')
+      in
+      let%bind m' = SMap.fold aux m (ok SMap.empty) in
+      let%bind type_annotation = check @@ O.Type_record (SMap.map O.get_annotation m') in
+      ok O.{expression = O.Record m' ; type_annotation }
+  | Record_accessor (r, ind) ->
+      let%bind r' = type_annotated_expression e r in
+      let%bind r_tv = O.get_t_record r'.type_annotation in
+      let%bind tv =
+        generic_try (simple_error "bad record index")
+        @@ (fun () -> SMap.find ind r_tv) in
+      let%bind type_annotation = check tv in
+      ok O.{expression = O.Record_accessor (r', ind) ; type_annotation }
   | _ -> simple_fail "default"