Michelson: different types of annotations

src/bin_client/test/contracts/and.tz

@@ -1,3 +1,3 @@
-parameter (pair (bool @first) (bool @second));
+parameter (pair :param %first %second bool bool);
 storage (option bool);
-code { CAR @param; DUP; CAR @first; DIP{CDR @second}; AND; SOME; NIL operation; PAIR };
+code { CAR; UNPAIR; AND @and; SOME @prev; NIL operation; PAIR };

src/lib_micheline/micheline.ml

@@ -7,10 +7,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+type annot = string list
+
 type ('l, 'p) node =
   | Int of 'l * Z.t
   | String of 'l * string
-  | Prim of 'l * 'p * ('l, 'p) node list * string list
+  | Prim of 'l * 'p * ('l, 'p) node list * annot
   | Seq of 'l * ('l, 'p) node list
 
 type canonical_location = int
@@ -41,7 +43,6 @@ let annotations = function
   | Seq (_, _) -> []
   | Prim (_, _, _, annots) -> annots
 
-
 let root (Canonical expr) = expr
 
 let strip_locations root =

src/lib_micheline/micheline.mli

@@ -7,13 +7,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
+type annot = string list
+
 (** The abstract syntax tree of Micheline expressions. The first
     parameter is used to conatin locations, but can also embed custom
     data. The second parameter is the type of primitive names. *)
 type ('l, 'p) node =
   | Int of 'l * Z.t
   | String of 'l * string
-  | Prim of 'l * 'p * ('l, 'p) node list * string list
+  | Prim of 'l * 'p * ('l, 'p) node list * annot
   | Seq of 'l * ('l, 'p) node list
 
 (** Encoding for expressions, as their {!canonical} encoding.

src/lib_micheline/micheline_printer.ml

@@ -36,6 +36,9 @@ let print_string ppf text =
     text ;
   Format.fprintf ppf "\""
 
+let print_annotations =
+  Format.pp_print_list ~pp_sep:Format.pp_print_space Format.pp_print_string
+
 let preformat root =
   let preformat_loc = function
     | { comment = None } ->
@@ -81,7 +84,8 @@ let rec print_expr_unwrapped ppf = function
   | Prim ((ml, s, { comment }), name, args, annot) ->
       let name = match annot with
         | [] -> name
-        | annots -> Format.asprintf "%s @[<h>%a@]" name (Format.pp_print_list Format.pp_print_string) annots in
+        | annots ->
+            Format.asprintf "%s @[<h>%a@]" name print_annotations annots in
       if not ml && s < 80 then begin
         if args = [] then
           Format.fprintf ppf "%s" name

src/lib_protocol_environment/sigs/v1/micheline.mli

@@ -7,10 +7,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+type annot = string list
+
 type ('l, 'p) node =
   | Int of 'l * Z.t
   | String of 'l * string
-  | Prim of 'l * 'p * ('l, 'p) node list * string list
+  | Prim of 'l * 'p * ('l, 'p) node list * annot
   | Seq of 'l * ('l, 'p) node list
 
 type 'p canonical

src/proto_alpha/lib_client/michelson_v1_emacs.ml

@@ -33,6 +33,14 @@ let print_expr ppf expr =
   let root = root (Michelson_v1_primitives.strings_of_prims expr) in
   Format.fprintf ppf "@[<h>%a@]" print_expr root
 
+let print_var_annots ppf =
+  List.iter (Format.fprintf ppf "%s ")
+
+let print_annot_expr ppf (expr, annot) =
+  Format.fprintf ppf "(%a%a)"
+    print_var_annots annot
+    print_expr expr
+
 open Micheline_parser
 open Script_tc_errors
 
@@ -49,7 +57,7 @@ let print_type_map ppf (parsed, type_map) =
         List.iter (print_expr_types ppf) items
   and print_stack ppf items =
     Format.fprintf ppf "(%a)"
-      (Format.pp_print_list ~pp_sep:Format.pp_print_space print_expr)
+      (Format.pp_print_list ~pp_sep:Format.pp_print_space print_annot_expr)
       items
   and print_item ppf loc = try
       let { start = { point = s } ; stop = { point = e } }, locs =

src/proto_alpha/lib_client/michelson_v1_error_reporter.ml

@@ -16,11 +16,14 @@ open Script_ir_translator
 open Script_interpreter
 open Michelson_v1_printer
 
-let print_ty (type t) ppf (annot, (ty : t ty)) =
+let print_ty (type t) ppf (ty : t ty) =
-  unparse_ty annot ty
+  unparse_ty ty
   |> Micheline.strip_locations
   |> Michelson_v1_printer.print_expr_unwrapped ppf
 
+let print_var_annot ppf annot =
+  List.iter (Format.fprintf ppf "@ %s") (unparse_var_annot annot)
+
 let print_stack_ty (type t) ?(depth = max_int) ppf (s : t stack_ty) =
   let rec loop
     : type t. int -> Format.formatter -> t stack_ty -> unit
@@ -29,11 +32,14 @@ let print_stack_ty (type t) ?(depth = max_int) ppf (s : t stack_ty) =
       | _ when depth <= 0 ->
           Format.fprintf ppf "..."
       | Item_t (last, Empty_t, annot) ->
-          Format.fprintf ppf "%a"
+          Format.fprintf ppf "%a%a"
-            print_ty (annot, last)
+            print_ty last
+            print_var_annot annot
       | Item_t (last, rest, annot) ->
-          Format.fprintf ppf "%a :@ %a"
+          Format.fprintf ppf "%a%a@ :@ %a"
-            print_ty (annot, last) (loop (depth - 1)) rest in
+            print_ty last
+            print_var_annot annot
+            (loop (depth - 1)) rest in
   match s with
   | Empty_t ->
       Format.fprintf ppf "[]"
@@ -148,7 +154,7 @@ let report_errors ~details ~show_source ?parsed ppf errs =
              | Some s -> Format.fprintf ppf "%s " s)
           name
           print_source (parsed, hilights)
-          print_ty ([], ty) ;
+          print_ty ty ;
         if rest <> [] then Format.fprintf ppf "@," ;
         print_trace (parsed_locations parsed) rest
     | Alpha_environment.Ecoproto_error (Ill_formed_type (_, expr, loc)) :: rest ->
@@ -325,21 +331,21 @@ let report_errors ~details ~show_source ?parsed ppf errs =
                  @[<hov 2>and@ %a.@]@]"
                 print_loc loc
                 (Michelson_v1_primitives.string_of_prim name)
-                print_ty ([], tya)
+                print_ty tya
-                print_ty ([], tyb)
+                print_ty tyb
           | Undefined_unop (loc, name, ty) ->
               Format.fprintf ppf
                 "@[<hov 0>@[<hov 2>%aoperator %s is undefined on@ %a@]@]"
                 print_loc loc
                 (Michelson_v1_primitives.string_of_prim name)
-                print_ty ([], ty)
+                print_ty ty
           | Bad_return (loc, got, exp) ->
               Format.fprintf ppf
                 "@[<v 2>%awrong stack type at end of body:@,\
                  - @[<v 0>expected return stack type:@ %a,@]@,\
                  - @[<v 0>actual stack type:@ %a.@]@]"
                 print_loc loc
-                (fun ppf -> print_stack_ty ppf) (Item_t (exp, Empty_t, []))
+                (fun ppf -> print_stack_ty ppf) (Item_t (exp, Empty_t, None))
                 (fun ppf -> print_stack_ty ppf) got
           | Bad_stack (loc, name, depth, sty) ->
               Format.fprintf ppf
@@ -358,18 +364,18 @@ let report_errors ~details ~show_source ?parsed ppf errs =
           | Inconsistent_annotations (annot1, annot2) ->
               Format.fprintf ppf
                 "@[<v 2>The two annotations do not match:@,\
-                 - @[<v>%a@]@,\
+                 - @[<v>%s@]@,\
-                 - @[<v>%a@]@]"
+                 - @[<v>%s@]@]"
-                (Format.pp_print_list Format.pp_print_string) annot1
+                annot1
-                (Format.pp_print_list Format.pp_print_string) annot2
+                annot2
           | Inconsistent_type_annotations (loc, ty1, ty2) ->
               Format.fprintf ppf
                 "@[<v 2>%athe two types contain incompatible annotations:@,\
                  - @[<hov>%a@]@,\
                  - @[<hov>%a@]@]"
                 print_loc loc
-                print_ty ([], ty1)
+                print_ty ty1
-                print_ty ([], ty2)
+                print_ty ty2
           | Unexpected_annotation loc ->
               Format.fprintf ppf
                 "@[<v 2>%aunexpected annotation."
@@ -396,7 +402,7 @@ let report_errors ~details ~show_source ?parsed ppf errs =
                  @[<hov 2>is invalid for type@ %a.@]@]"
                 print_loc loc
                 print_expr got
-                print_ty ([], exp)
+                print_ty exp
           | Invalid_contract (loc, contract) ->
               Format.fprintf ppf
                 "%ainvalid contract %a."
@@ -405,13 +411,13 @@ let report_errors ~details ~show_source ?parsed ppf errs =
               Format.fprintf ppf "%acomparable type expected."
                 print_loc loc ;
               Format.fprintf ppf "@[<hov 0>@[<hov 2>Type@ %a@]@ is not comparable.@]"
-                print_ty ([], ty)
+                print_ty ty
           | Inconsistent_types (tya, tyb) ->
               Format.fprintf ppf
                 "@[<hov 0>@[<hov 2>Type@ %a@]@ \
                  @[<hov 2>is not compatible with type@ %a.@]@]"
-                print_ty ([], tya)
+                print_ty tya
-                print_ty ([], tyb)
+                print_ty tyb
           | Reject loc ->
               Format.fprintf ppf "%ascript reached FAIL instruction"
                 print_loc loc

src/proto_alpha/lib_client/michelson_v1_macros.ml

@@ -274,7 +274,7 @@ let expand_paaiair original =
 
 let expand_unpaaiair original =
   match original with
-  | Prim (loc, str, args, []) ->
+  | Prim (loc, str, args, annot) ->
       let len = String.length str in
       if len >= 6
       && String.sub str 0 3 = "UNP"
@@ -282,35 +282,40 @@ let expand_unpaaiair original =
       && check_letters str 3 (len - 2)
            (function 'A' | 'I' -> true | _ -> false) then
         try
-          let rec parse i acc =
+          let rec parse i remaining_annots acc =
             if i = 2 then
               match acc with
               | [ Seq _ as acc ] -> acc
               | _ -> Seq (loc, List.rev acc)
             else if String.get str i = 'I'
                  && String.get str (i - 1) = 'A' then
-              parse (i - 2)
+              let car_annot, cdr_annot, remaining_annots =
+                match remaining_annots with
+                | [] -> [], [], []
+                | a :: b :: r when i = 4 -> [ a ], [ b ], r
+                | a :: r -> [ a ], [], r in
+              parse (i - 2) remaining_annots
                 (Seq (loc, [ Prim (loc, "DUP", [], []) ;
-                             Prim (loc, "CAR", [], []) ;
+                             Prim (loc, "CAR", [], car_annot) ;
                              Prim (loc, "DIP",
                                    [ Seq (loc,
-                                          [ Prim (loc, "CDR", [], []) ]) ], []) ])
+                                          [ Prim (loc, "CDR", [], cdr_annot) ]) ], []) ])
                  :: acc)
             else if String.get str i = 'A' then
               match acc with
               | [] ->
                   raise_notrace Not_a_pair
               | (Seq _ as acc) :: accs ->
-                  parse (i - 1)
+                  parse (i - 1) remaining_annots
                     (Prim (loc, "DIP", [ acc ], []) :: accs)
               | acc :: accs ->
-                  parse (i - 1)
+                  parse (i - 1) remaining_annots
                     (Prim (loc, "DIP",
                            [ Seq (loc, [ acc ]) ],
                            []) :: accs)
             else
               raise_notrace Not_a_pair in
-          let expanded = parse (len - 2) [] in
+          let expanded = parse (len - 2) annot [] in
           begin match args with
             | [] -> ok ()
             | _ :: _ -> error (Invalid_arity (str, List.length args, 0))

src/proto_alpha/lib_client/michelson_v1_printer.ml

@@ -26,13 +26,21 @@ let print_expr_unwrapped ppf expr =
   |> Micheline.inject_locations (fun _ -> anon)
   |> print_expr_unwrapped ppf
 
+let print_var_annots ppf =
+  List.iter (Format.fprintf ppf "%s ")
+
+let print_annot_expr_unwrapped ppf (expr, annot) =
+  Format.fprintf ppf "%a%a"
+    print_var_annots annot
+    print_expr_unwrapped expr
+
 let print_stack ppf = function
   | [] -> Format.fprintf ppf "[]"
   | more ->
       Format.fprintf ppf "@[<hov 0>[ %a ]@]"
         (Format.pp_print_list
            ~pp_sep: (fun ppf () -> Format.fprintf ppf "@ : ")
-           print_expr_unwrapped)
+           print_annot_expr_unwrapped)
         more
 
 let inject_types type_map parsed =

src/proto_alpha/lib_protocol/src/alpha_context.mli

@@ -272,6 +272,8 @@ module Script : sig
 
   type location = Micheline.canonical_location
 
+  type annot = Micheline.annot
+
   type expr = prim Micheline.canonical
 
   type lazy_expr = expr Data_encoding.lazy_t

src/proto_alpha/lib_protocol/src/script_interpreter.ml

@@ -527,22 +527,22 @@ let rec interp
         | Nop, stack ->
             logged_return (stack, ctxt)
         (* comparison *)
-        | Compare Bool_key, Item (a, Item (b, rest)) ->
+        | Compare (Bool_key _), Item (a, Item (b, rest)) ->
             consume_gaz_comparison descr Compare.Bool.compare Interp_costs.compare_bool a b rest
-        | Compare String_key, Item (a, Item (b, rest)) ->
+        | Compare (String_key _), Item (a, Item (b, rest)) ->
             consume_gaz_comparison descr Compare.String.compare Interp_costs.compare_string a b rest
-        | Compare Mutez_key, Item (a, Item (b, rest)) ->
+        | Compare (Mutez_key _), Item (a, Item (b, rest)) ->
             consume_gaz_comparison descr Tez.compare Interp_costs.compare_tez a b rest
-        | Compare Int_key, Item (a, Item (b, rest)) ->
+        | Compare (Int_key _), Item (a, Item (b, rest)) ->
             consume_gaz_comparison descr Script_int.compare Interp_costs.compare_int a b rest
-        | Compare Nat_key, Item (a, Item (b, rest)) ->
+        | Compare (Nat_key _), Item (a, Item (b, rest)) ->
             consume_gaz_comparison descr Script_int.compare Interp_costs.compare_nat a b rest
-        | Compare Key_hash_key, Item (a, Item (b, rest)) ->
+        | Compare (Key_hash_key _), Item (a, Item (b, rest)) ->
             consume_gaz_comparison descr Signature.Public_key_hash.compare
               Interp_costs.compare_key_hash a b rest
-        | Compare Timestamp_key, Item (a, Item (b, rest)) ->
+        | Compare (Timestamp_key _), Item (a, Item (b, rest)) ->
             consume_gaz_comparison descr Script_timestamp.compare Interp_costs.compare_timestamp a b rest
-        | Compare Address_key, Item (a, Item (b, rest)) ->
+        | Compare (Address_key _), Item (a, Item (b, rest)) ->
             consume_gaz_comparison descr Contract.compare Interp_costs.compare_address a b rest
         (* comparators *)
         | Eq, Item (cmpres, rest) ->
@@ -623,7 +623,7 @@ let rec interp
         | Implicit_account, Item (key, rest) ->
             Lwt.return (Gas.consume ctxt Interp_costs.implicit_account) >>=? fun ctxt ->
             let contract = Contract.implicit_contract key in
-            logged_return (Item ((Unit_t, contract), rest), ctxt)
+            logged_return (Item ((Unit_t None, contract), rest), ctxt)
         | Create_contract (storage_type, param_type, Lam (_, code)),
           Item (manager, Item
                   (delegate, Item
@@ -634,8 +634,8 @@ let rec interp
             Lwt.return (Gas.consume ctxt Interp_costs.create_contract) >>=? fun ctxt ->
             let code =
               Micheline.strip_locations
-                (Seq (0, [ Prim (0, K_parameter, [ unparse_ty [] param_type ], []) ;
+                (Seq (0, [ Prim (0, K_parameter, [ unparse_ty param_type ], []) ;
-                           Prim (0, K_storage, [ unparse_ty [] storage_type ], []) ;
+                           Prim (0, K_storage, [ unparse_ty storage_type ], []) ;
                            Prim (0, K_code, [ Micheline.root code ], []) ])) in
             unparse_data ctxt Optimized storage_type init >>=? fun (storage, ctxt) ->
             let storage = Micheline.strip_locations storage in

src/proto_alpha/lib_protocol/src/script_ir_translator.mli

@@ -19,6 +19,9 @@ type ex_script = Ex_script : ('a, 'b) Script_typed_ir.script -> ex_script
 
 type unparsing_mode = Optimized | Readable
 
+type type_logger =
+  int -> (Script.expr * Script.annot) list -> (Script.expr * Script.annot)  list -> unit
+
 (* ---- Sets and Maps -------------------------------------------------------*)
 
 val empty_set : 'a Script_typed_ir.comparable_ty -> 'a Script_typed_ir.set
@@ -58,20 +61,19 @@ val ty_eq :
   ('ta Script_typed_ir.ty, 'tb Script_typed_ir.ty) eq tzresult
 
 val parse_data :
-  ?type_logger: (int -> Script.expr list -> Script.expr list -> unit) ->
+  ?type_logger: type_logger ->
   context ->
   'a Script_typed_ir.ty -> Script.node -> ('a * context) tzresult Lwt.t
 val unparse_data :
-  context -> unparsing_mode ->
+  context -> unparsing_mode -> 'a Script_typed_ir.ty -> 'a ->
-  'a Script_typed_ir.ty -> 'a -> (Script.node * context) tzresult Lwt.t
+  (Script.node * context) tzresult Lwt.t
+val unparse_var_annot : Script_typed_ir.var_annot option -> string list
 
 val parse_ty :
   allow_big_map: bool ->
   allow_operation: bool ->
-  Script.node ->
+  Script.node -> ex_ty tzresult
-  (ex_ty * Script_typed_ir.annot) tzresult
+val unparse_ty : 'a Script_typed_ir.ty -> Script.node
-val unparse_ty :
-  string list -> 'a Script_typed_ir.ty -> Script.node
 
 val parse_toplevel
   : Script.expr -> (Script.node * Script.node * Script.node) tzresult
@@ -80,11 +82,11 @@ val typecheck_code :
   context -> Script.expr -> (type_map * context) tzresult Lwt.t
 
 val typecheck_data :
-  ?type_logger: (int -> Script.expr list -> Script.expr list -> unit) ->
+  ?type_logger: type_logger ->
   context -> Script.expr * Script.expr -> context tzresult Lwt.t
 
 val parse_script :
-  ?type_logger: (int -> Script.expr list -> Script.expr list -> unit) ->
+  ?type_logger: type_logger ->
   context -> Script.t -> (ex_script * context) tzresult Lwt.t
 val unparse_script :
   context -> unparsing_mode ->

src/proto_alpha/lib_protocol/src/script_repr.ml

@@ -11,6 +11,8 @@ type location = Micheline.canonical_location
 
 let location_encoding = Micheline.canonical_location_encoding
 
+type annot = Micheline.annot
+
 type expr = Michelson_v1_primitives.prim Micheline.canonical
 
 type lazy_expr = expr Data_encoding.lazy_t

src/proto_alpha/lib_protocol/src/script_repr.mli

@@ -9,6 +9,8 @@
 
 type location = Micheline.canonical_location
 
+type annot = Micheline.annot
+
 type expr = Michelson_v1_primitives.prim Micheline.canonical
 
 type error += Lazy_script_decode (* `Permanent *)

src/proto_alpha/lib_protocol/src/script_tc_errors.ml

@@ -17,7 +17,7 @@ open Script_typed_ir
 (* Auxiliary types for error documentation *)
 type namespace = Type_namespace | Constant_namespace | Instr_namespace | Keyword_namespace
 type kind = Int_kind | String_kind | Prim_kind | Seq_kind
-type type_map = (int * (Script.expr list * Script.expr list)) list
+type type_map = (int * ((Script.expr * Script.annot) list * (Script.expr * Script.annot) list)) list
 
 (* Structure errors *)
 type error += Invalid_arity of Script.location * prim * int * int
@@ -39,8 +39,10 @@ type error += Unmatched_branches : Script.location * _ stack_ty * _ stack_ty ->
 type error += Self_in_lambda of Script.location
 type error += Bad_stack_length
 type error += Bad_stack_item of int
-type error += Inconsistent_annotations of string list * string list
+type error += Inconsistent_annotations of string * string
 type error += Inconsistent_type_annotations : Script.location * _ ty * _ ty -> error
+type error += Invalid_type_annotation : Script.location * annot list -> error
+type error += Invalid_var_annotation : Script.location * annot list -> error
 type error += Unexpected_annotation of Script.location
 type error += Invalid_map_body : Script.location * _ stack_ty -> error
 type error += Invalid_map_block_fail of Script.location

src/proto_alpha/lib_protocol/src/script_tc_errors_registration.ml

@@ -17,21 +17,22 @@ open Script_ir_translator
 (* Helpers for encoding *)
 let type_map_enc =
   let open Data_encoding in
+  let stack_enc = list (tup2 Script.expr_encoding (list string)) in
   list
     (conv
        (fun (loc, (bef, aft)) -> (loc, bef, aft))
        (fun (loc, bef, aft) -> (loc, (bef, aft)))
        (obj3
           (req "location" Script.location_encoding)
-          (req "stackBefore" (list Script.expr_encoding))
+          (req "stackBefore" stack_enc)
-          (req "stackAfter" (list Script.expr_encoding))))
+          (req "stackAfter" stack_enc)))
 
 let ex_ty_enc =
   Data_encoding.conv
-    (fun (Ex_ty ty) -> strip_locations (unparse_ty [] ty))
+    (fun (Ex_ty ty) -> strip_locations (unparse_ty ty))
     (fun expr ->
        match parse_ty ~allow_big_map:true ~allow_operation:true (root expr) with
-       | Ok (Ex_ty ty, _) -> Ex_ty ty
+       | Ok ty -> ty
        | _ -> assert false)
     Script.expr_encoding
 
@@ -63,6 +64,8 @@ let () =
                   "string", String_kind ;
                   "primitiveApplication", Prim_kind ;
                   "sequence", Seq_kind ] in
+  let var_annot_enc =
+    conv (function `Var_annot x -> x)  (function x -> `Var_annot x) string in
   let ex_stack_ty_enc =
     let rec unfold = function
       | Ex_stack_ty (Item_t (ty, rest, annot)) ->
@@ -73,7 +76,7 @@ let () =
           let Ex_stack_ty rest = fold rest in
           Ex_stack_ty (Item_t (ty, rest, annot))
       | [] -> Ex_stack_ty Empty_t in
-    conv unfold fold (list (tup2 ex_ty_enc (list string))) in
+    conv unfold fold (list (tup2 ex_ty_enc (option var_annot_enc))) in
   (* -- Structure errors ---------------------- *)
   (* Invalid arity *)
   register_error_kind
@@ -327,8 +330,8 @@ let () =
     ~title:"Annotations inconsistent between branches"
     ~description:"The annotations on two types could not be merged"
     (obj2
-       (req "annot1" (list string))
+       (req "annot1" string)
-       (req "annot2" (list string)))
+       (req "annot2" string))
     (function Inconsistent_annotations (annot1, annot2) -> Some (annot1, annot2)
             | _ -> None)
     (fun (annot1, annot2) -> Inconsistent_annotations (annot1, annot2)) ;

src/proto_alpha/lib_protocol/src/script_typed_ir.ml

@@ -13,15 +13,35 @@ open Script_int
 
 (* ---- Auxiliary types -----------------------------------------------------*)
 
+type var_annot = [ `Var_annot of string ]
+type type_annot = [ `Type_annot of string ]
+type field_annot = [ `Field_annot of string ]
+
+type annot = [ var_annot | type_annot | field_annot ]
+
+(* type 'ty comparable_ty_desc =
+ *   | Int_key : (z num) comparable_ty_desc
+ *   | Nat_key : (n num) comparable_ty_desc
+ *   | String_key : string comparable_ty_desc
+ *   | Mutez_key : Tez.t comparable_ty_desc
+ *   | Bool_key : bool comparable_ty_desc
+ *   | Key_hash_key : public_key_hash comparable_ty_desc
+ *   | Timestamp_key : Script_timestamp.t comparable_ty_desc
+ *   | Address_key : Contract.t comparable_ty_desc
+ *
+ * type 'ty comparable_ty =
+ *   { comp_ty_desc : 'ty comparable_ty_desc ; comp_ty_name : type_annot option } *)
+
 type 'ty comparable_ty =
-  | Int_key : (z num) comparable_ty
+  | Int_key : type_annot option -> (z num) comparable_ty
-  | Nat_key : (n num) comparable_ty
+  | Nat_key : type_annot option -> (n num) comparable_ty
-  | String_key : string comparable_ty
+  | String_key : type_annot option -> string comparable_ty
-  | Mutez_key : Tez.t comparable_ty
+  | Mutez_key : type_annot option -> Tez.t comparable_ty
-  | Bool_key : bool comparable_ty
+  | Bool_key : type_annot option -> bool comparable_ty
-  | Key_hash_key : public_key_hash comparable_ty
+  | Key_hash_key : type_annot option -> public_key_hash comparable_ty
-  | Timestamp_key : Script_timestamp.t comparable_ty
+  | Timestamp_key : type_annot option -> Script_timestamp.t comparable_ty
-  | Address_key : Contract.t comparable_ty
+  | Address_key : type_annot option -> Contract.t comparable_ty
+
 
 module type Boxed_set = sig
   type elt
@@ -42,8 +62,6 @@ end
 
 type ('key, 'value) map = (module Boxed_map with type key = 'key and type value = 'value)
 
-type annot = string list
-
 type ('arg, 'storage) script =
   { code : (('arg, 'storage) pair, (packed_internal_operation list, 'storage) pair) lambda ;
     arg_type : 'arg ty ;
@@ -62,31 +80,56 @@ and ('arg, 'ret) lambda =
 and 'arg typed_contract =
   'arg ty * Contract.t
 
+(* and 'ty ty_desc =
+ *   | Unit_t : unit ty_desc
+ *   | Int_t : z num ty_desc
+ *   | Nat_t : n num ty_desc
+ *   | Signature_t : signature ty_desc
+ *   | String_t : string ty_desc
+ *   | Mutez_t : Tez.t ty_desc
+ *   | Key_hash_t : public_key_hash ty_desc
+ *   | Key_t : public_key ty_desc
+ *   | Timestamp_t : Script_timestamp.t ty_desc
+ *   | Address_t : Contract.t ty_desc
+ *   | Bool_t : bool ty_desc
+ *   | Pair_t : ('a ty * field_annot option) * ('b ty * field_annot option) -> ('a, 'b) pair ty_desc
+ *   | Union_t : ('a ty * field_annot option) * ('b ty * field_annot option) -> ('a, 'b) union ty_desc
+ *   | Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty_desc
+ *   | Option_t : ('v ty * field_annot option) * field_annot option -> 'v option ty_desc
+ *   | List_t : 'v ty -> 'v list ty_desc
+ *   | Set_t : 'v comparable_ty -> 'v set ty_desc
+ *   | Map_t : 'k comparable_ty * 'v ty -> ('k, 'v) map ty_desc
+ *   | Big_map_t : 'k comparable_ty * 'v ty -> ('k, 'v) big_map ty_desc
+ *   | Contract_t : 'arg ty -> 'arg typed_contract ty_desc
+ *   | Operation_t : internal_operation ty_desc
+ *
+ * and 'ty ty = { ty_desc : 'ty ty_desc ; ty_name : type_annot option } *)
+
 and 'ty ty =
-  | Unit_t : unit ty
+  | Unit_t : type_annot option -> unit ty
-  | Int_t : z num ty
+  | Int_t : type_annot option -> z num ty
-  | Nat_t : n num ty
+  | Nat_t : type_annot option -> n num ty
-  | Signature_t : signature ty
+  | Signature_t : type_annot option -> signature ty
-  | String_t : string ty
+  | String_t : type_annot option -> string ty
-  | Mutez_t : Tez.t ty
+  | Mutez_t : type_annot option -> Tez.t ty
-  | Key_hash_t : public_key_hash ty
+  | Key_hash_t : type_annot option -> public_key_hash ty
-  | Key_t : public_key ty
+  | Key_t : type_annot option -> public_key ty
-  | Timestamp_t : Script_timestamp.t ty
+  | Timestamp_t : type_annot option -> Script_timestamp.t ty
-  | Address_t : Contract.t ty
+  | Address_t : type_annot option -> Contract.t ty
-  | Bool_t : bool ty
+  | Bool_t : type_annot option -> bool ty
-  | Pair_t : ('a ty * annot) * ('b ty * annot) -> ('a, 'b) pair ty
+  | Pair_t :  ('a ty * field_annot option) * ('b ty * field_annot option) * type_annot option -> ('a, 'b) pair ty
-  | Union_t : ('a ty * annot) * ('b ty * annot) -> ('a, 'b) union ty
+  | Union_t : ('a ty * field_annot option) * ('b ty * field_annot option) * type_annot option  -> ('a, 'b) union ty
-  | Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty
+  | Lambda_t : 'arg ty * 'ret ty * type_annot option  -> ('arg, 'ret) lambda ty
-  | Option_t : 'v ty -> 'v option ty
+  | Option_t : ('v ty * field_annot option) * field_annot option * type_annot option  -> 'v option ty
-  | List_t : 'v ty -> 'v list ty
+  | List_t : 'v ty * type_annot option -> 'v list ty
-  | Set_t : 'v comparable_ty -> 'v set ty
+  | Set_t : 'v comparable_ty * type_annot option -> 'v set ty
-  | Map_t : 'k comparable_ty * 'v ty -> ('k, 'v) map ty
+  | Map_t : 'k comparable_ty * 'v ty * type_annot option -> ('k, 'v) map ty
-  | Big_map_t : 'k comparable_ty * 'v ty -> ('k, 'v) big_map ty
+  | Big_map_t : 'k comparable_ty * 'v ty * type_annot option -> ('k, 'v) big_map ty
-  | Contract_t : 'arg ty -> 'arg typed_contract ty
+  | Contract_t : 'arg ty * type_annot option -> 'arg typed_contract ty
-  | Operation_t : packed_internal_operation ty
+  | Operation_t : type_annot option -> packed_internal_operation ty
 
 and 'ty stack_ty =
-  | Item_t : 'ty ty * 'rest stack_ty * annot -> ('ty * 'rest) stack_ty
+  | Item_t : 'ty ty * 'rest stack_ty * var_annot option -> ('ty * 'rest) stack_ty
   | Empty_t : end_of_stack stack_ty
 
 and ('key, 'value) big_map = { diff : ('key, 'value option) map ;