Michelson: new (nop) opcodes CAST and RENAME

Removes RENAME macro

docs/whitedoc/michelson.rst

@@ -1918,6 +1918,20 @@ type on top.
    EMPTY_MAP :t 'key 'val
    :: 'S -> (map :t 'key 'val) : 'S
 
+
+A no-op instruction ``CAST`` ensures the top of the stack has the
+specified type, and change its type if it is compatible. In particular,
+this allows to change or remove type names explicitly.
+
+::
+
+   CAST 'b
+   :: 'a : 'S   ->   'b : 'S
+      iff  'a = 'b
+
+   > CAST t / a : S  =>  a : S
+
+
 Variable Annotations
 ~~~~~~~~~~~~~~~~~~~~
 
@@ -2010,6 +2024,8 @@ The instructions which accept at most one variable annotation are:
    STEPS_TO_QUOTA
    SOURCE
    SELF
+   CAST
+   RENAME
 
 The instructions which accept at most two variable annotations are:
 
@@ -2034,6 +2050,17 @@ annotations will see only their top-most stack type elements annotated.
    :: key_hash : option key_hash : bool : tez : 'S
       ->  @op operation : address : 'S
 
+A no-op instruction ``RENAME`` allows to rename variables in the stack
+or to erase variable annotations in the stack.
+
+::
+
+   RENAME @new
+   :: @old 'a ; 'S -> @new 'a : 'S
+
+   RENAME
+   :: @old 'a ; 'S -> 'a : 'S
+
 
 Field and Constructor Annotations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

src/bin_client/test/contracts/unpair_macro.tz

@@ -2,6 +2,7 @@ parameter (unit :param_unit);
 storage (unit :u1);
 code { DROP ;
        UNIT :u4 @4; UNIT :u3 @3; UNIT :u2 @2; UNIT :u1 @1;
+       CAST unit ; CAST (unit :u1);
        PAIR; UNPAIR @x1 @x2;
        PPAIPAIR @p1 %x1 %x2 %x3 %x4; UNPPAIPAIR @uno @due @tre @quattro;
        PAPAPAIR @p2 %x1 %x2 %x3 %x4; UNPAPAPAIR @un @deux @trois @quatre;

src/proto_alpha/lib_protocol/src/alpha_context.mli

@@ -248,6 +248,8 @@ module Script : sig
     | I_ADDRESS
     | I_CONTRACT
     | I_ISNAT
+    | I_CAST
+    | I_RENAME
     | T_bool
     | T_contract
     | T_int

src/proto_alpha/lib_protocol/src/michelson_v1_primitives.ml

@@ -97,6 +97,8 @@ type prim =
   | I_ADDRESS
   | I_CONTRACT
   | I_ISNAT
+  | I_CAST
+  | I_RENAME
   | T_bool
   | T_contract
   | T_int
@@ -222,6 +224,8 @@ let string_of_prim = function
   | I_ADDRESS -> "ADDRESS"
   | I_CONTRACT -> "CONTRACT"
   | I_ISNAT -> "ISNAT"
+  | I_CAST -> "CAST"
+  | I_RENAME -> "RENAME"
   | T_bool -> "bool"
   | T_contract -> "contract"
   | T_int -> "int"
@@ -328,6 +332,8 @@ let prim_of_string = function
   | "ADDRESS" -> ok I_ADDRESS
   | "CONTRACT" -> ok I_CONTRACT
   | "ISNAT" -> ok I_ISNAT
+  | "CAST" -> ok I_CAST
+  | "RENAME" -> ok I_RENAME
   | "bool" -> ok T_bool
   | "contract" -> ok T_contract
   | "int" -> ok T_int
@@ -479,6 +485,8 @@ let prim_encoding =
     ("ADDRESS", I_ADDRESS) ;
     ("CONTRACT", I_CONTRACT) ;
     ("ISNAT", I_ISNAT) ;
+    ("CAST", I_CAST) ;
+    ("RENAME", I_RENAME) ;
     ("bool", T_bool) ;
     ("contract", T_contract) ;
     ("int", T_int) ;

src/proto_alpha/lib_protocol/src/michelson_v1_primitives.mli

@@ -95,6 +95,8 @@ type prim =
   | I_ADDRESS
   | I_CONTRACT
   | I_ISNAT
+  | I_CAST
+  | I_RENAME
   | T_bool
   | T_contract
   | T_int

src/proto_alpha/lib_protocol/src/script_ir_translator.ml

@@ -307,7 +307,9 @@ let namespace = function
   | I_LOOP_LEFT
   | I_ADDRESS
   | I_CONTRACT
-  | I_ISNAT -> Instr_namespace
+  | I_ISNAT
+  | I_CAST
+  | I_RENAME -> Instr_namespace
   | T_bool
   | T_contract
   | T_int
@@ -2214,6 +2216,19 @@ and parse_instr
         parse_var_annot loc annot >>=? fun annot ->
         typed ctxt loc Ge
           (Item_t (Bool_t None, rest, annot))
+    (* annotations *)
+    | Prim (loc, I_CAST, [ cast_t ], annot),
+      Item_t (t, stack, item_annot) ->
+        parse_var_annot loc annot ~default:item_annot >>=? fun annot ->
+        (Lwt.return (parse_ty ~allow_big_map:true ~allow_operation:true cast_t))
+        >>=? fun (Ex_ty cast_t) ->
+        Lwt.return @@ ty_eq cast_t t >>=? fun Eq ->
+        Lwt.return @@ merge_types loc cast_t t >>=? fun _ ->
+        typed ctxt loc Nop (Item_t (cast_t, stack, annot))
+    | Prim (loc, I_RENAME, [], annot),
+      Item_t (t, stack, _) ->
+        parse_var_annot loc annot >>=? fun annot -> (* can erase annot *)
+        typed ctxt loc Nop (Item_t (t, stack, annot))
     (* protocol *)
     | Prim (loc, I_ADDRESS, [], annot),
       Item_t (Contract_t _, rest, contract_annot) ->