pipeline ok

src/ligo/ast_simplified.ml

@@ -100,6 +100,8 @@ and matching =
 
 let ae expression = {expression ; type_annotation = None}
 
+let annotated_expression expression type_annotation = {expression ; type_annotation}
+
 open Ligo_helpers.Trace
 
 module PP = struct

src/ligo/ast_typed.ml

@@ -1,3 +1,5 @@
+module S = Ast_simplified
+
 module SMap = Ligo_helpers.X_map.String
 
 let list_of_smap (s:'a SMap.t) : (string * 'a) list =
@@ -30,13 +32,18 @@ and ae = annotated_expression
 and tv_map = type_value type_name_map
 and ae_map = annotated_expression name_map
 
-and type_value =
+and type_value' =
   | Type_tuple of tv list
   | Type_sum of tv_map
   | Type_record of tv_map
   | Type_constant of type_name * tv list
   | Type_function of tv * tv
 
+and type_value = {
+  type_value : type_value' ;
+  simplified : S.type_expression option ;
+}
+
 and expression =
   (* Base *)
   | Literal of literal
@@ -91,23 +98,29 @@ and matching =
       match_none : b ;
       match_some : name * b ;
     }
-  | Match_tuple of (name * b) list
+  | Match_tuple of name list * b
+
+let type_value type_value simplified = { type_value ; simplified }
+let annotated_expression expression type_annotation = { expression ; type_annotation }
 
 module PP = struct
   open Format
   open Ligo_helpers.PP
 
-  let rec type_value ppf (tv:type_value) : unit =
+  let rec type_value' ppf (tv':type_value') : unit =
-    match tv with
+    match tv' with
     | Type_tuple lst -> fprintf ppf "tuple[%a]" (list_sep type_value) lst
     | Type_sum m -> fprintf ppf "sum[%a]" (smap_sep type_value) m
     | Type_record m -> fprintf ppf "record[%a]" (smap_sep type_value) m
     | Type_function (a, b) -> fprintf ppf "%a -> %a" type_value a type_value b
     | Type_constant (c, []) -> fprintf ppf "%s" c
     | Type_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep type_value) n
+
+  and type_value ppf (tv:type_value) : unit =
+    type_value' ppf tv.type_value
 end
 
-open Ligo_helpers.Trace
+open! Ligo_helpers.Trace
 
 module Errors = struct
   let different_kinds a b =
@@ -132,22 +145,22 @@ module Errors = struct
 end
 open Errors
 
-let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab with
+let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value, b.type_value) with
-  | Type_tuple a as ta, (Type_tuple b as tb) -> (
+  | Type_tuple ta, Type_tuple tb -> (
       let%bind _ =
-        trace_strong (different_size_tuples ta tb)
+        trace_strong (different_size_tuples a b)
-        @@ Assert.assert_true List.(length a = length b) in
+        @@ Assert.assert_true List.(length ta = length tb) in
-      bind_list_iter type_value_eq (List.combine a b)
+      bind_list_iter assert_type_value_eq (List.combine ta tb)
     )
-  | Type_constant (a, a') as ca, (Type_constant (b, b') as cb) -> (
+  | Type_constant (ca, lsta), Type_constant (cb, lstb) -> (
       let%bind _ =
-        trace_strong (different_size_constants ca cb)
+        trace_strong (different_size_constants a b)
-        @@ Assert.assert_true List.(length a' = length b') in
+        @@ Assert.assert_true List.(length lsta = length lstb) in
       let%bind _ =
-        trace_strong (different_constants a b)
+        trace_strong (different_constants ca cb)
         @@ Assert.assert_true (a = b) in
       trace (simple_error "constant sub-expression")
-      @@ bind_list_iter type_value_eq (List.combine a' b')
+      @@ bind_list_iter assert_type_value_eq (List.combine lsta lstb)
     )
   | Type_sum a, Type_sum b -> (
       let a' = list_of_smap a in
@@ -156,7 +169,7 @@ let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab w
         let%bind _ =
           Assert.assert_true ~msg:"different keys in sum types"
           @@ (ka = kb) in
-        type_value_eq (va, vb)
+        assert_type_value_eq (va, vb)
       in
       trace (simple_error "sum type")
       @@ bind_list_iter aux (List.combine a' b')
@@ -169,13 +182,18 @@ let rec type_value_eq (ab: (type_value * type_value)) : unit result = match ab w
         let%bind _ =
           Assert.assert_true ~msg:"different keys in record types"
           @@ (ka = kb) in
-        type_value_eq (va, vb)
+        assert_type_value_eq (va, vb)
       in
       trace (simple_error "record type")
       @@ bind_list_iter aux (List.combine a' b')
 
     )
-  | a, b -> fail @@ different_kinds a b
+  | _ -> fail @@ different_kinds a b
+
+(* No information about what made it fail *)
+let type_value_eq ab = match assert_type_value_eq ab with
+  | Ok _ -> true
+  | _ -> false
 
 let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
   match a, b with
@@ -183,38 +201,68 @@ let merge_annotation (a:type_value option) (b:type_value option) : type_value re
   | Some a, None -> ok a
   | None, Some b -> ok b
   | Some a, Some b ->
-      let%bind _ = type_value_eq (a, b) in
+      let%bind _ = assert_type_value_eq (a, b) in
-      ok a
+      match a.simplified, b.simplified with
+      | _, None -> ok a
+      | None, Some _ -> ok b
+      | _ -> simple_fail "both have simplified ASTs"
 
-let t_bool : type_value = Type_constant ("bool", [])
+let t_bool s : type_value = type_value (Type_constant ("bool", [])) s
-let t_string : type_value = Type_constant ("string", [])
+let simplify_t_bool s = t_bool (Some s)
-let t_bytes : type_value = Type_constant ("bytes", [])
+let make_t_bool = t_bool None
-let t_int : type_value = Type_constant ("int", [])
+
-let t_unit : type_value = Type_constant ("unit", [])
+let t_string s : type_value = type_value (Type_constant ("string", [])) s
+let simplify_t_string s = t_string (Some s)
+let make_t_string = t_string None
+
+let t_bytes s : type_value = type_value (Type_constant ("bytes", [])) s
+let simplify_t_bytes s = t_bytes (Some s)
+let make_t_bytes = t_bytes None
+
+let t_int s : type_value = type_value (Type_constant ("int", [])) s
+let simplify_t_int s = t_int (Some s)
+let make_t_int = t_int None
+
+let t_unit s : type_value = type_value (Type_constant ("unit", [])) s
+let simplify_t_unit s = t_unit (Some s)
+let make_t_unit = t_unit None
+
+let t_tuple lst s : type_value = type_value (Type_tuple lst) s
+let simplify_t_tuple lst s = t_tuple lst (Some s)
+let make_t_tuple lst = t_tuple lst None
+
+let t_record m s : type_value = type_value (Type_record m) s
+let make_t_record m = t_record m None
+
+let t_sum m s : type_value = type_value (Type_sum m) s
+let make_t_sum m = t_sum m None
+
+let t_function (param, result) s : type_value = type_value (Type_function (param, result)) s
+let make_t_function f = t_function f None
 
 let get_annotation (x:annotated_expression) = x.type_annotation
 
-let get_t_bool : type_value -> unit result = function
+let get_t_bool (t:type_value) : unit result = match t.type_value with
   | Type_constant ("bool", []) -> ok ()
   | _ -> simple_fail "not a bool"
 
-let get_t_option : type_value -> type_value result = function
+let get_t_option (t:type_value) : type_value result = match t.type_value with
   | Type_constant ("option", [o]) -> ok o
   | _ -> simple_fail "not a option"
 
-let get_t_list : type_value -> type_value result = function
+let get_t_list (t:type_value) : type_value result = match t.type_value with
   | Type_constant ("list", [o]) -> ok o
   | _ -> simple_fail "not a list"
 
-let get_t_tuple : type_value -> type_value list result = function
+let get_t_tuple (t:type_value) : type_value list result = match t.type_value with
   | Type_tuple lst -> ok lst
   | _ -> simple_fail "not a tuple"
 
-let get_t_sum : type_value -> type_value SMap.t result = function
+let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value with
   | Type_sum m -> ok m
   | _ -> simple_fail "not a sum"
 
-let get_t_record : type_value -> type_value SMap.t result = function
+let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value with
   | Type_record m -> ok m
   | _ -> simple_fail "not a record"
 

src/ligo/ligo-helpers/trace.ml

@@ -58,6 +58,14 @@ let rec bind_list = function
       ok @@ hd :: tl
     )
 
+let bind_smap (s:_ X_map.String.t) =
+  let open X_map.String in
+  let aux k v prev =
+    prev >>? fun prev' ->
+    v >>? fun v' ->
+    ok @@ add k v' prev' in
+  fold aux s (ok empty)
+
 let bind_fold_list f init lst =
   let aux x y =
     x >>? fun x ->
@@ -155,16 +163,18 @@ let pp_to_string pp () x =
 let errors_to_string = pp_to_string errors_pp
 
 module Assert = struct
-  let assert_true ?msg = function
+  let assert_true ?(msg="not true") = function
     | true -> ok ()
-    | false -> simple_fail @@ Option.unopt ~default:"not true" msg
+    | false -> simple_fail msg
 
-  let assert_equal_int ?msg a b =
+  let assert_equal_int ?(msg="not equal int") a b =
-    let msg = Option.unopt ~default:"not equal int" msg in
     assert_true ~msg (a = b)
 
-  let assert_list_size ~msg lst n =
+  let assert_list_size ?(msg="lst doesn't have the right size") lst n =
-    assert_true ~msg (List.length lst = n)
+    assert_true ~msg List.(length lst = n)
+
+  let assert_list_same_size ?(msg="lists don't have same size") a b =
+    assert_true ~msg List.(length a = length b)
 
   let assert_list_size_2 ~msg = function
     | [a;b] -> ok (a, b)

src/ligo/ligo.ml

@@ -75,12 +75,16 @@ let type_ (p:AST_Simplified.program) : AST_Typed.program result = Typer.type_pro
 let type_expression ?(env:Typer.Environment.t = Typer.Environment.empty)
     (e:AST_Simplified.annotated_expression) : AST_Typed.annotated_expression result =
   Typer.type_annotated_expression env e
-let untype_expression (e:AST_Typed.annotated_expression) : AST_Simplified.annotated_expression = Typer.untype_annotated_expression e
+let untype_expression (e:AST_Typed.annotated_expression) : AST_Simplified.annotated_expression result = Typer.untype_annotated_expression e
 
 let transpile (p:AST_Typed.program) : Mini_c.program result = Transpiler.translate_program p
 let transpile_expression ?(env:Mini_c.Environment.t = Mini_c.Environment.empty)
     (e:AST_Typed.annotated_expression) : Mini_c.expression result = Transpiler.translate_annotated_expression env e
 let transpile_value ?(env:Mini_c.Environment.t = Mini_c.Environment.empty)
-    (e:AST_Typed.annotated_expression) : Mini_c.expression result =
+    (e:AST_Typed.annotated_expression) : Mini_c.value result =
   let%bind e = Transpiler.translate_annotated_expression env e in
   Mini_c.expression_to_value e
+
+let untranspile_value (v : Mini_c.value) (e:AST_Typed.type_value) : AST_Typed.annotated_expression result =
+  Transpiler.untranspile v e
+

src/ligo/mini_c.ml

@@ -360,59 +360,6 @@ module Translate_type = struct
 
 end
 
-module Math = struct
-
-  let lt_power_of_two n =
-    let rec aux prev n =
-      let cur = prev * 2 in
-      if cur >= n
-      then prev
-      else aux cur n
-    in
-    if n > 0
-    then ok (aux 1 n)
-    else fail @@ error "lt_power_of_two" (string_of_int n)
-
-  let ge_power_of_two n =
-    let rec aux c n =
-      if c >= n
-      then c
-      else aux (c * 2) n
-    in
-    if n > 0
-    then ok (aux 1 n)
-    else fail @@ error "ge_power_of_two" (string_of_int n)
-
-  let rec exp x n =
-    if n = 0
-    then 1
-    else
-      let exp' = exp (x * x) (n / 2) in
-      let m = if n mod 2 = 0 then 1 else x in
-      m * exp'
-
-  let exp2 = exp 2
-
-  let log2_c n =
-    let rec aux acc n =
-      if n = 1
-      then acc
-      else aux (acc + 1) (n / 2)
-    in
-    if n < 1 then raise @@ Failure ("log_2") ;
-    let n' = aux 0 n in
-    if exp2 n' = n then n' else n' + 1
-
-  let int_to_bools n l =
-    let rec aux acc n = function
-      | 0 -> acc
-      | s -> aux ((n mod 2 = 0) :: acc) (n / 2) (s - 1)
-    in
-    List.rev @@ aux [] n l
-
-end
-
-
 module Environment = struct
   open Tezos_utils.Micheline
 
@@ -1020,27 +967,43 @@ module Run = struct
 end
 
 
-(* module Combinators = struct
+module Combinators = struct
- *
+
- *   let var x : expression' = Var x
+  let get_bool (v:value) = match v with
- *   let apply a b : expression' = Apply(a, b)
+    | `Bool b -> ok b
- *
+    | _ -> simple_fail "not a bool"
- *   let t_int : type_value = `Base Int
+
- *   let type_int x : expression = x, `Base Int
+  let get_int (v:value) = match v with
- *   let type_f_int x : expression = x,`Function (`Base Int, `Base Int)
+    | `Int n -> ok n
- *   let type_closure_int t x : expression = x, `Deep_closure (t, `Base Int, `Base Int)
+    | _ -> simple_fail "not an int"
- *   let int n = type_int @@ Literal(`Int n)
+
- *   let neg_int x = type_int @@ Predicate("NEG", [x])
+  let get_string (v:value) = match v with
- *   let add_int x y = type_int @@ Predicate("ADD_INT", [x ; y])
+    | `String s -> ok s
- *   let var_int x = type_int @@ var x
+    | _ -> simple_fail "not a string"
- *   let apply_int a b = type_int @@ apply a b
+
- *
+  let get_bytes (v:value) = match v with
- *   let assign_variable v expr = Assignment (Variable (v, expr))
+    | `Bytes b -> ok b
- *   let assign_function v anon = Assignment (Variable (v, anon))
+    | _ -> simple_fail "not a bytes"
- *   let function_int body binder result = {
+
- *     input = `Base Int ;
+  let get_unit (v:value) = match v with
- *     output = `Base Int ;
+    | `Unit -> ok ()
- *     body ; binder ; result ;
+    | _ -> simple_fail "not a bool"
- *   }
+
- *
+  let get_pair (v:value) = match v with
- * end *)
+    | `Pair (a, b) -> ok (a, b)
+    | _ -> simple_fail "not a pair"
+
+  let get_left (v:value) = match v with
+    | `Left b -> ok b
+    | _ -> simple_fail "not a left"
+
+  let get_right (v:value) = match v with
+    | `Right b -> ok b
+    | _ -> simple_fail "not a right"
+
+  let get_or (v:value) = match v with
+    | `Left b -> ok (false, b)
+    | `Right b -> ok (true, b)
+    | _ -> simple_fail "not a left/right"
+
+end

src/ligo/transpiler.ml

@@ -5,9 +5,12 @@ module AST = Ast_typed
 
 let list_of_map m = List.rev @@ Ligo_helpers.X_map.String.fold (fun _ v prev -> v :: prev) m []
 let kv_list_of_map m = List.rev @@ Ligo_helpers.X_map.String.fold (fun k v prev -> (k, v) :: prev) m []
+let map_of_kv_list lst =
+  let open AST.SMap in
+  List.fold_left (fun prev (k, v) -> add k v prev) empty lst
 
 let rec translate_type (t:AST.type_value) : type_value result =
-  match t with
+  match t.type_value with
   | Type_constant ("bool", []) -> ok (`Base Bool)
   | Type_constant ("int", []) -> ok (`Base Int)
   | Type_constant ("string", []) -> ok (`Base String)
@@ -81,7 +84,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
           if k = m then (
             let%bind _ =
               trace (simple_error "constructor parameter doesn't have expected type (shouldn't happen here)")
-              @@ AST.type_value_eq (tv, param.type_annotation) in
+              @@ AST.assert_type_value_eq (tv, param.type_annotation) in
             ok (Some (param'_expr), param'_tv)
           ) else (
             let%bind tv = translate_type tv in
@@ -213,3 +216,98 @@ let translate_program (lst:AST.program) : program result =
   in
   let%bind (statements, _) = List.fold_left aux (ok ([], Environment.empty)) lst in
   ok statements
+
+open Combinators
+
+let rec exp x n =
+  if n = 0
+  then 1
+  else
+    let exp' = exp (x * x) (n / 2) in
+    let m = if n mod 2 = 0 then 1 else x in
+    m * exp'
+
+let exp2 = exp 2
+
+let extract_constructor (v : value) (tree : _ Append_tree.t') : (string * value * AST.type_value) result =
+  let open Append_tree in
+  let rec aux tv : (string * value * AST.type_value) result=
+    match tv with
+    | Leaf (k, t), v -> ok (k, v, t)
+    | Node {a}, `Left v -> aux (a, v)
+    | Node {b}, `Right v -> aux (b, v)
+    | _ -> simple_fail "bad constructor path"
+  in
+  let%bind (s, v, t) = aux (tree, v) in
+  ok (s, v, t)
+
+let extract_tuple (v : value) (tree : AST.type_value Append_tree.t') : ((value * AST.type_value) list) result =
+  let open Append_tree in
+  let rec aux tv : ((value * AST.type_value) list) result =
+    match tv with
+    | Leaf t, v -> ok @@ [v, t]
+    | Node {a;b}, `Pair (va, vb) ->
+        let%bind a' = aux (a, va) in
+        let%bind b' = aux (b, vb) in
+        ok (a' @ b')
+    | _ -> simple_fail "bad tuple path"
+  in
+  aux (tree, v)
+
+let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result =
+  let open Append_tree in
+  let rec aux tv : ((string * (value * AST.type_value)) list) result =
+    match tv with
+    | Leaf (s, t), v -> ok @@ [s, (v, t)]
+    | Node {a;b}, `Pair (va, vb) ->
+        let%bind a' = aux (a, va) in
+        let%bind b' = aux (b, vb) in
+        ok (a' @ b')
+    | _ -> simple_fail "bad record path"
+  in
+  aux (tree, v)
+
+
+let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression result =
+  let open! AST in
+  let return e = ok AST.(annotated_expression e t) in
+  match t.type_value with
+  | Type_constant ("bool", []) ->
+      let%bind b = get_bool v in
+      return (Literal (Bool b))
+  | Type_constant ("int", []) ->
+      let%bind n = get_int v in
+      return (Literal (Int n))
+  | Type_constant ("string", []) ->
+      let%bind n = get_string v in
+      return (Literal (String n))
+  | Type_constant _ ->
+      simple_fail "unknown type_constant"
+  | Type_sum m ->
+      let lst = kv_list_of_map m in
+      let%bind node = match Append_tree.of_list lst with
+        | Empty -> simple_fail "empty sum type"
+        | Full t -> ok t
+      in
+      let%bind (name, v, tv) = extract_constructor v node in
+      let%bind sub = untranspile v tv in
+      return (Constructor (name, sub))
+  | Type_tuple lst ->
+      let%bind node = match Append_tree.of_list lst with
+        | Empty -> simple_fail "empty tuple"
+        | Full t -> ok t in
+      let%bind tpl = extract_tuple v node in
+      let%bind tpl' = bind_list
+        @@ List.map (fun (x, y) -> untranspile x y) tpl in
+      return (Tuple tpl')
+  | Type_record m ->
+      let lst = kv_list_of_map m in
+      let%bind node = match Append_tree.of_list lst with
+        | Empty -> simple_fail "empty tuple"
+        | Full t -> ok t in
+      let%bind lst = extract_record v node in
+      let%bind lst = bind_list
+        @@ List.map (fun (x, (y, z)) -> let%bind yz = untranspile y z in ok (x, yz)) lst in
+      let m' = map_of_kv_list lst in
+      return (Record m')
+  | Type_function _ -> simple_fail "no untranspilation for functions yet"

src/ligo/typer.ml

@@ -22,10 +22,11 @@ module Environment = struct
   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)
+      | (_, (O.{type_value=(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 =
@@ -101,7 +102,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
   | Loop (cond, body) ->
       let%bind cond = type_annotated_expression e cond in
       let%bind _ =
-        O.type_value_eq (cond.type_annotation, (O.Type_constant ("bool", []))) in
+        O.assert_type_value_eq (cond.type_annotation, O.make_t_bool) in
       let%bind body = type_block e body in
       ok (e, O.Loop (cond, body))
   | Assignment {name;annotated_expression} -> (
@@ -115,12 +116,12 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
           let%bind annotated_expression = type_annotated_expression e annotated_expression in
           let e' = Environment.add e name annotated_expression.type_annotation in
           let%bind _ =
-            O.type_value_eq (annotated_expression.type_annotation, prev) in
+            O.assert_type_value_eq (annotated_expression.type_annotation, prev) in
           ok (e', O.Assignment {name;annotated_expression})
       | Some _, Some prev ->
           let%bind annotated_expression = type_annotated_expression e annotated_expression in
           let%bind _assert = trace (simple_error "Annotation doesn't match environment")
-            @@ O.type_value_eq (annotated_expression.type_annotation, prev) in
+            @@ O.assert_type_value_eq (annotated_expression.type_annotation, prev) in
           let e' = Environment.add e name annotated_expression.type_annotation in
           ok (e', O.Assignment {name;annotated_expression})
     )
@@ -158,23 +159,28 @@ and type_match (e:environment) (t:O.type_value) : I.matching -> O.matching resul
       let%bind b' = type_block e' b in
       ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')})
   | Match_tuple (lst, b) ->
-      let%bind lst =
+      let%bind t_tuple =
         trace_strong (simple_error "Matching tuple on not-a-tuple")
-        get_tuple
+        @@ O.get_t_tuple t in
-      let aux (x, y) =
+      let%bind _ =
-        let%bind y = type_block e y in
+        trace_strong (simple_error "Matching tuple of different size")
-        ok (x, y) in
+        @@ Assert.assert_list_same_size t_tuple lst in
-      let%bind lst' = bind_list @@ List.map aux lst in
+      let lst' = List.combine lst t_tuple in
-      ok (O.Match_tuple lst')
+      let aux prev (name, tv) = Environment.add prev name tv in
+      let e' = List.fold_left aux e lst' in
+      let%bind b' = type_block e' b in
+      ok (O.Match_tuple (lst, b'))
 
-and evaluate_type (e:environment) : I.type_expression -> O.type_value result = function
+and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
+  let return tv' = ok O.(type_value tv' (Some t)) in
+  match t with
   | Type_function (a, b) ->
       let%bind a' = evaluate_type e a in
       let%bind b' = evaluate_type e b in
-      ok (O.Type_function (a', b'))
+      return (Type_function (a', b'))
   | Type_tuple lst ->
       let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
-      ok (O.Type_tuple lst')
+      return (Type_tuple lst')
   | Type_sum m ->
       let aux k v prev =
         let%bind prev' = prev in
@@ -182,7 +188,7 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f
         ok @@ SMap.add k v' prev'
       in
       let%bind m = SMap.fold aux m (ok SMap.empty) in
-      ok (O.Type_sum m)
+      return (Type_sum m)
   | Type_record m ->
       let aux k v prev =
         let%bind prev' = prev in
@@ -190,7 +196,7 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f
         ok @@ SMap.add k v' prev'
       in
       let%bind m = SMap.fold aux m (ok SMap.empty) in
-      ok (O.Type_record m)
+      return (Type_record m)
   | Type_variable name ->
       let%bind tv =
         trace_option (unbound_type_variable e name)
@@ -198,13 +204,13 @@ and evaluate_type (e:environment) : I.type_expression -> O.type_value result = f
       ok tv
   | Type_constant (cst, lst) ->
       let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
-      ok (O.Type_constant(cst, lst'))
+      return (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
+  let check tv = O.(merge_annotation tv_opt (Some tv)) in
   match ae.expression with
   (* Basic *)
   | Variable name ->
@@ -214,25 +220,25 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
       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
+      let%bind type_annotation = check O.make_t_bool in
       ok O.{expression = Literal (Bool b) ; type_annotation }
   | Literal Unit ->
-      let%bind type_annotation = check O.t_unit in
+      let%bind type_annotation = check O.make_t_unit in
       ok O.{expression = Literal (Unit) ; type_annotation }
   | Literal (String s) ->
-      let%bind type_annotation = check O.t_string in
+      let%bind type_annotation = check O.make_t_string in
       ok O.{expression = Literal (String s) ; type_annotation }
   | Literal (Bytes s) ->
-      let%bind type_annotation = check O.t_bytes in
+      let%bind type_annotation = check O.make_t_bytes in
       ok O.{expression = Literal (Bytes s) ; type_annotation }
   | Literal (Number n) ->
-      let%bind type_annotation = check O.t_int in
+      let%bind type_annotation = check O.make_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
+      let%bind type_annotation = check (O.make_t_tuple tv_lst) in
       ok O.{expression = Tuple lst' ; type_annotation }
   | Tuple_accessor (tpl, ind) ->
       let%bind tpl' = type_annotated_expression e tpl in
@@ -248,7 +254,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
         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 _assert = O.assert_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 *)
@@ -259,7 +265,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
         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
+      let%bind type_annotation = check @@ O.make_t_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
@@ -281,7 +287,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
       let e' = Environment.add e binder input_type in
       let%bind result = type_annotated_expression e' result in
       let%bind body = type_block e' body in
-      let%bind type_annotation = check O.(Type_function (input_type, output_type)) in
+      let%bind type_annotation = check @@ O.make_t_function (input_type, output_type) in
       ok O.{expression = Lambda {binder;input_type;output_type;result;body} ; type_annotation}
   | Constant (name, lst) ->
       let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
@@ -292,9 +298,9 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
   | Application (f, arg) ->
       let%bind f = type_annotated_expression e f in
       let%bind arg = type_annotated_expression e arg in
-      let%bind type_annotation = match f.type_annotation with
+      let%bind type_annotation = match f.type_annotation.type_value with
         | Type_function (param, result) ->
-            let%bind _ = O.type_value_eq (param, arg.type_annotation) in
+            let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
             ok result
         | _ -> simple_fail "applying to not-a-function"
       in
@@ -304,8 +310,108 @@ and type_constant (name:string) (lst:O.type_value list) : (string * O.type_value
   (* Constant poorman's polymorphism *)
   let open O in
   match (name, lst) with
-  | "ADD", [a ; b] when a = t_int && b = t_int -> ok ("ADD_INT", t_int)
+  | "ADD", [a ; b] when type_value_eq (a, make_t_int) && type_value_eq (b, make_t_int) -> ok ("ADD_INT", make_t_int)
-  | "ADD", [a ; b] when a = t_string && b = t_string -> ok ("CONCAT", t_string)
+  | "ADD", [a ; b] when type_value_eq (a, make_t_string) && type_value_eq (b, make_t_string) -> ok ("CONCAT", make_t_string)
   | "ADD", [_ ; _] -> simple_fail "bad types to add"
   | "ADD", _ -> simple_fail "bad number of params to add"
   | name, _ -> fail @@ unrecognized_constant name
+
+let untype_type_value (t:O.type_value) : (I.type_expression) result =
+  match t.simplified with
+  | Some s -> ok s
+  | _ -> simple_fail "trying to untype generated type"
+
+let untype_literal (l:O.literal) : I.literal result =
+  let open I in
+  match l with
+  | Unit -> ok Unit
+  | Bool b -> ok (Bool b)
+  | Nat n -> ok (Number n)
+  | Int n -> ok (Number n)
+  | String s -> ok (String s)
+  | Bytes b -> ok (Bytes b)
+
+let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_expression) result =
+  let open I in
+  let annotation = e.type_annotation.simplified in
+  let return e = ok @@ annotated_expression e annotation in
+  match e.expression with
+  | Literal l ->
+      let%bind l = untype_literal l in
+      return (Literal l)
+  | Constant (n, lst) ->
+      let%bind lst' = bind_list
+        @@ List.map untype_annotated_expression lst in
+      return (Constant (n, lst'))
+  | Variable n ->
+      return (Variable n)
+  | Application (f, arg) ->
+      let%bind f' = untype_annotated_expression f in
+      let%bind arg' = untype_annotated_expression arg in
+      return (Application (f', arg'))
+  | Lambda {binder;input_type;output_type;body;result} ->
+      let%bind input_type = untype_type_value input_type in
+      let%bind output_type = untype_type_value output_type in
+      let%bind result = untype_annotated_expression result in
+      let%bind body = untype_block body in
+      return (Lambda {binder;input_type;output_type;body;result})
+  | Tuple lst ->
+      let%bind lst' = bind_list
+        @@ List.map untype_annotated_expression lst in
+      return (Tuple lst')
+  | Tuple_accessor (tpl, ind)  ->
+      let%bind tpl' = untype_annotated_expression tpl in
+      return (Tuple_accessor (tpl', ind))
+  | Constructor (n, p) ->
+      let%bind p' = untype_annotated_expression p in
+      return (Constructor (n, p'))
+  | Record r ->
+      let%bind r' = bind_smap
+        @@ SMap.map untype_annotated_expression r in
+      return (Record r')
+  | Record_accessor (r, s) ->
+      let%bind r' = untype_annotated_expression r in
+      return (Record_accessor (r', s))
+
+and untype_block (b:O.block) : (I.block) result =
+  bind_list @@ List.map untype_instruction b
+
+and untype_instruction (i:O.instruction) : (I.instruction) result =
+  let open I in
+  match i with
+  | Skip -> ok Skip
+  | Fail e ->
+      let%bind e' = untype_annotated_expression e in
+      ok (Fail e')
+  | Loop (e, b) ->
+      let%bind e' = untype_annotated_expression e in
+      let%bind b' = untype_block b in
+      ok @@ Loop (e', b')
+  | Assignment a ->
+      let%bind annotated_expression = untype_annotated_expression a.annotated_expression in
+      ok @@ Assignment {name = a.name ; annotated_expression}
+  | Matching (e, m) ->
+      let%bind e' = untype_annotated_expression e in
+      let%bind m' = untype_matching m in
+      ok @@ Matching (e', m')
+
+and untype_matching (m:O.matching) : (I.matching) result =
+  let open I in
+  match m with
+  | Match_bool {match_true ; match_false} ->
+      let%bind match_true = untype_block match_true in
+      let%bind match_false = untype_block match_false in
+      ok @@ Match_bool {match_true ; match_false}
+  | Match_tuple (lst, b) ->
+      let%bind b = untype_block b in
+      ok @@ Match_tuple (lst, b)
+  | Match_option {match_none ; match_some = (v, some)} ->
+      let%bind match_none = untype_block match_none in
+      let%bind some = untype_block some in
+      let match_some = v, some in
+      ok @@ Match_option {match_none ; match_some}
+  | Match_list {match_nil ; match_cons = (hd, tl, cons)} ->
+      let%bind match_nil = untype_block match_nil in
+      let%bind cons = untype_block cons in
+      let match_cons = hd, tl, cons in
+      ok @@ Match_list {match_nil ; match_cons}