add key and signature types

This commit is contained in:
Lesenechal Remi 2019-11-19 15:12:58 +01:00
parent 5ab3bf85e9
commit 2fa78bd0bd
19 changed files with 70 additions and 1 deletions

View File

@ -432,6 +432,12 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e
| E_literal (Literal_string s) -> ( | E_literal (Literal_string s) -> (
return_wrapped (e_string s) state @@ Wrap.literal (t_string ()) return_wrapped (e_string s) state @@ Wrap.literal (t_string ())
) )
| E_literal (Literal_signature s) -> (
return_wrapped (e_signature s) state @@ Wrap.literal (t_signature ())
)
| E_literal (Literal_key s) -> (
return_wrapped (e_key s) state @@ Wrap.literal (t_key ())
)
| E_literal (Literal_bytes b) -> ( | E_literal (Literal_bytes b) -> (
return_wrapped (e_bytes b) state @@ Wrap.literal (t_bytes ()) return_wrapped (e_bytes b) state @@ Wrap.literal (t_bytes ())
) )
@ -1000,6 +1006,8 @@ let untype_literal (l:O.literal) : I.literal result =
| Literal_mutez n -> ok (Literal_mutez n) | Literal_mutez n -> ok (Literal_mutez n)
| Literal_int n -> ok (Literal_int n) | Literal_int n -> ok (Literal_int n)
| Literal_string s -> ok (Literal_string s) | Literal_string s -> ok (Literal_string s)
| Literal_key s -> ok (Literal_key s)
| Literal_signature s -> ok (Literal_signature s)
| Literal_bytes b -> ok (Literal_bytes b) | Literal_bytes b -> ok (Literal_bytes b)
| Literal_address s -> ok (Literal_address s) | Literal_address s -> ok (Literal_address s)
| Literal_operation s -> ok (Literal_operation s) | Literal_operation s -> ok (Literal_operation s)

View File

@ -404,6 +404,10 @@ and type_expression' : environment -> ?tv_opt:O.type_value -> I.expression -> O.
return (E_literal (Literal_unit)) (t_unit ()) return (E_literal (Literal_unit)) (t_unit ())
| E_literal (Literal_string s) -> | E_literal (Literal_string s) ->
return (E_literal (Literal_string s)) (t_string ()) return (E_literal (Literal_string s)) (t_string ())
| E_literal (Literal_key s) ->
return (E_literal (Literal_key s)) (t_key ())
| E_literal (Literal_signature s) ->
return (E_literal (Literal_signature s)) (t_signature ())
| E_literal (Literal_bytes s) -> | E_literal (Literal_bytes s) ->
return (E_literal (Literal_bytes s)) (t_bytes ()) return (E_literal (Literal_bytes s)) (t_bytes ())
| E_literal (Literal_int n) -> | E_literal (Literal_int n) ->
@ -808,6 +812,8 @@ let untype_literal (l:O.literal) : I.literal result =
| Literal_mutez n -> ok (Literal_mutez n) | Literal_mutez n -> ok (Literal_mutez n)
| Literal_int n -> ok (Literal_int n) | Literal_int n -> ok (Literal_int n)
| Literal_string s -> ok (Literal_string s) | Literal_string s -> ok (Literal_string s)
| Literal_signature s -> ok (Literal_signature s)
| Literal_key s -> ok (Literal_key s)
| Literal_bytes b -> ok (Literal_bytes b) | Literal_bytes b -> ok (Literal_bytes b)
| Literal_address s -> ok (Literal_address s) | Literal_address s -> ok (Literal_address s)
| Literal_operation s -> ok (Literal_operation s) | Literal_operation s -> ok (Literal_operation s)

View File

@ -130,6 +130,7 @@ let rec transpile_type (t:AST.type_value) : type_value result =
| T_constant (Type_name "unit", []) -> ok (T_base Base_unit) | T_constant (Type_name "unit", []) -> ok (T_base Base_unit)
| T_constant (Type_name "operation", []) -> ok (T_base Base_operation) | T_constant (Type_name "operation", []) -> ok (T_base Base_operation)
| T_constant (Type_name "signature", []) -> ok (T_base Base_signature) | T_constant (Type_name "signature", []) -> ok (T_base Base_signature)
| T_constant (Type_name "key", []) -> ok (T_base Base_key)
| T_constant (Type_name "contract", [x]) -> | T_constant (Type_name "contract", [x]) ->
let%bind x' = transpile_type x in let%bind x' = transpile_type x in
ok (T_contract x') ok (T_contract x')
@ -237,6 +238,8 @@ let rec transpile_literal : AST.literal -> value = fun l -> match l with
| Literal_bytes s -> D_bytes s | Literal_bytes s -> D_bytes s
| Literal_string s -> D_string s | Literal_string s -> D_string s
| Literal_address s -> D_string s | Literal_address s -> D_string s
| Literal_signature s -> D_string s
| Literal_key s -> D_string s
| Literal_operation op -> D_operation op | Literal_operation op -> D_operation op
| Literal_unit -> D_unit | Literal_unit -> D_unit

View File

@ -150,6 +150,12 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
bind_map_list aux lst in bind_map_list aux lst in
return (E_list lst') return (E_list lst')
) )
| T_constant (Type_name "key", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "key" v) @@
get_string v in
return (E_literal (Literal_key n))
)
| T_constant (Type_name "set", [ty]) -> ( | T_constant (Type_name "set", [ty]) -> (
let%bind lst = let%bind lst =
trace_strong (wrong_mini_c_value "set" v) @@ trace_strong (wrong_mini_c_value "set" v) @@

View File

@ -69,6 +69,7 @@ module Ty = struct
| Base_bytes -> return bytes_k | Base_bytes -> return bytes_k
| Base_operation -> fail (not_comparable "operation") | Base_operation -> fail (not_comparable "operation")
| Base_signature -> fail (not_comparable "signature") | Base_signature -> fail (not_comparable "signature")
| Base_key -> fail (not_comparable "key")
let comparable_type : type_value -> ex_comparable_ty result = fun tv -> let comparable_type : type_value -> ex_comparable_ty result = fun tv ->
match tv with match tv with
@ -98,6 +99,7 @@ module Ty = struct
| Base_bytes -> return bytes | Base_bytes -> return bytes
| Base_operation -> return operation | Base_operation -> return operation
| Base_signature -> return signature | Base_signature -> return signature
| Base_key -> return key
let rec type_ : type_value -> ex_ty result = let rec type_ : type_value -> ex_ty result =
function function
@ -180,6 +182,7 @@ let base_type : type_base -> O.michelson result =
| Base_bytes -> ok @@ O.prim T_bytes | Base_bytes -> ok @@ O.prim T_bytes
| Base_operation -> ok @@ O.prim T_operation | Base_operation -> ok @@ O.prim T_operation
| Base_signature -> ok @@ O.prim T_signature | Base_signature -> ok @@ O.prim T_signature
| Base_key -> ok @@ O.prim T_key
let rec type_ : type_value -> O.michelson result = let rec type_ : type_value -> O.michelson result =
function function

View File

@ -31,6 +31,12 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
trace_option (simple_error "too big to fit an int") @@ trace_option (simple_error "too big to fit an int") @@
Alpha_context.Script_int.to_int n in Alpha_context.Script_int.to_int n in
ok @@ D_nat n ok @@ D_nat n
| (Key_t _ ), n ->
let%bind s = match n with
| Ed25519 x -> ok @@ TP.Base58.simple_encode (TP.Ed25519.Public_key.b58check_encoding) x
| Secp256k1 x -> ok @@ TP.Base58.simple_encode (TP.Secp256k1.Public_key.b58check_encoding) x
| P256 x -> ok @@ TP.Base58.simple_encode (TP.P256.Public_key.b58check_encoding) x in
ok @@ D_string s
| (Timestamp_t _), n -> | (Timestamp_t _), n ->
let n = let n =
Z.to_int @@ Z.to_int @@

View File

@ -29,6 +29,8 @@ let literal ppf (l:literal) = match l with
| Literal_string s -> fprintf ppf "%S" s | Literal_string s -> fprintf ppf "%S" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b | Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
| Literal_address s -> fprintf ppf "@%S" s | Literal_address s -> fprintf ppf "@%S" s
| Literal_signature s -> fprintf ppf "@%S" s
| Literal_key s -> fprintf ppf "@%S" s
| Literal_operation _ -> fprintf ppf "Operation(...bytes)" | Literal_operation _ -> fprintf ppf "Operation(...bytes)"
let rec expression ppf (e:expression) = match e.expression with let rec expression ppf (e:expression) = match e.expression with

View File

@ -24,6 +24,8 @@ let t_nat : type_expression = T_constant ("nat", [])
let t_tez : type_expression = T_constant ("tez", []) let t_tez : type_expression = T_constant ("tez", [])
let t_unit : type_expression = T_constant ("unit", []) let t_unit : type_expression = T_constant ("unit", [])
let t_address : type_expression = T_constant ("address", []) let t_address : type_expression = T_constant ("address", [])
let t_signature : type_expression = T_constant ("signature", [])
let t_key : type_expression = T_constant ("key", [])
let t_option o : type_expression = T_constant ("option", [o]) let t_option o : type_expression = T_constant ("option", [o])
let t_list t : type_expression = T_constant ("list", [t]) let t_list t : type_expression = T_constant ("list", [t])
let t_variable n : type_expression = T_variable n let t_variable n : type_expression = T_variable n
@ -62,6 +64,8 @@ let e_bool ?loc b : expression = location_wrap ?loc @@ E_literal (Literal_bool
let e_string ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_string s) let e_string ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_string s)
let e_address ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_address s) let e_address ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_address s)
let e_mutez ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_mutez s) let e_mutez ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_mutez s)
let e_signature ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_signature s)
let e_key ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_key s)
let e'_bytes b : expression' result = let e'_bytes b : expression' result =
let%bind bytes = generic_try (simple_error "bad hex to bytes") (fun () -> Hex.to_bytes (`Hex b)) in let%bind bytes = generic_try (simple_error "bad hex to bytes") (fun () -> Hex.to_bytes (`Hex b)) in
ok @@ E_literal (Literal_bytes bytes) ok @@ E_literal (Literal_bytes bytes)

View File

@ -18,6 +18,8 @@ val t_nat : type_expression
val t_tez : type_expression val t_tez : type_expression
val t_unit : type_expression val t_unit : type_expression
val t_address : type_expression val t_address : type_expression
val t_key : type_expression
val t_signature : type_expression
(* (*
val t_option : type_expression -> type_expression val t_option : type_expression -> type_expression
*) *)
@ -51,6 +53,8 @@ val e_timestamp : ?loc:Location.t -> int -> expression
val e_bool : ?loc:Location.t -> bool -> expression val e_bool : ?loc:Location.t -> bool -> expression
val e_string : ?loc:Location.t -> string -> expression val e_string : ?loc:Location.t -> string -> expression
val e_address : ?loc:Location.t -> string -> expression val e_address : ?loc:Location.t -> string -> expression
val e_signature : ?loc:Location.t -> string -> expression
val e_key : ?loc:Location.t -> string -> expression
val e_mutez : ?loc:Location.t -> int -> expression val e_mutez : ?loc:Location.t -> int -> expression
val e'_bytes : string -> expression' result val e'_bytes : string -> expression' result
val e_bytes : ?loc:Location.t -> string -> expression result val e_bytes : ?loc:Location.t -> string -> expression result

View File

@ -61,6 +61,12 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
| Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
| Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b | Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b
| Literal_signature a, Literal_signature b when a = b -> ok ()
| Literal_signature _, Literal_signature _ -> fail @@ different_literals "different signature" a b
| Literal_signature _, _ -> fail @@ different_literals_because_different_types "signature vs non-signature" a b
| Literal_key a, Literal_key b when a = b -> ok ()
| Literal_key _, Literal_key _ -> fail @@ different_literals "different key" a b
| Literal_key _, _ -> fail @@ different_literals_because_different_types "key vs non-key" a b
let rec assert_value_eq (a, b: (expression * expression )) : unit result = let rec assert_value_eq (a, b: (expression * expression )) : unit result =
let error_content () = let error_content () =

View File

@ -95,6 +95,8 @@ and literal =
| Literal_bytes of bytes | Literal_bytes of bytes
| Literal_address of string | Literal_address of string
| Literal_timestamp of int | Literal_timestamp of int
| Literal_signature of string
| Literal_key of string
| Literal_operation of Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation | Literal_operation of Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation
and 'a matching = and 'a matching =

View File

@ -74,6 +74,8 @@ and literal ppf (l:literal) : unit =
| Literal_string s -> fprintf ppf "%s" s | Literal_string s -> fprintf ppf "%s" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b | Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
| Literal_address s -> fprintf ppf "@%s" s | Literal_address s -> fprintf ppf "@%s" s
| Literal_signature s -> fprintf ppf "@%s" s
| Literal_key s -> fprintf ppf "@%s" s
| Literal_operation _ -> fprintf ppf "Operation(...bytes)" | Literal_operation _ -> fprintf ppf "Operation(...bytes)"
and single_record_patch ppf ((s, ae) : string * ae) = and single_record_patch ppf ((s, ae) : string * ae) =

View File

@ -16,6 +16,7 @@ let t_string ?s () : type_value = make_t (T_constant (Type_name "string", [])) s
let t_bytes ?s () : type_value = make_t (T_constant (Type_name "bytes", [])) s let t_bytes ?s () : type_value = make_t (T_constant (Type_name "bytes", [])) s
let t_key ?s () : type_value = make_t (T_constant (Type_name "key", [])) s let t_key ?s () : type_value = make_t (T_constant (Type_name "key", [])) s
let t_key_hash ?s () : type_value = make_t (T_constant (Type_name "key_hash", [])) s let t_key_hash ?s () : type_value = make_t (T_constant (Type_name "key_hash", [])) s
let t_signature ?s () : type_value = make_t (T_constant (Type_name "signature", [])) s
let t_int ?s () : type_value = make_t (T_constant (Type_name "int", [])) s let t_int ?s () : type_value = make_t (T_constant (Type_name "int", [])) s
let t_address ?s () : type_value = make_t (T_constant (Type_name "address", [])) s let t_address ?s () : type_value = make_t (T_constant (Type_name "address", [])) s
let t_operation ?s () : type_value = make_t (T_constant (Type_name "operation", [])) s let t_operation ?s () : type_value = make_t (T_constant (Type_name "operation", [])) s
@ -238,6 +239,8 @@ let e_string s : expression = E_literal (Literal_string s)
let e_bytes s : expression = E_literal (Literal_bytes s) let e_bytes s : expression = E_literal (Literal_bytes s)
let e_timestamp s : expression = E_literal (Literal_timestamp s) let e_timestamp s : expression = E_literal (Literal_timestamp s)
let e_address s : expression = E_literal (Literal_address s) let e_address s : expression = E_literal (Literal_address s)
let e_signature s : expression = E_literal (Literal_signature s)
let e_key s : expression = E_literal (Literal_key s)
let e_operation s : expression = E_literal (Literal_operation s) let e_operation s : expression = E_literal (Literal_operation s)
let e_lambda l : expression = E_lambda l let e_lambda l : expression = E_lambda l
let e_pair a b : expression = E_tuple [a; b] let e_pair a b : expression = E_tuple [a; b]

View File

@ -19,6 +19,7 @@ val t_int : ?s:S.type_expression -> unit -> type_value
val t_nat : ?s:S.type_expression -> unit -> type_value val t_nat : ?s:S.type_expression -> unit -> type_value
val t_mutez : ?s:S.type_expression -> unit -> type_value val t_mutez : ?s:S.type_expression -> unit -> type_value
val t_address : ?s:S.type_expression -> unit -> type_value val t_address : ?s:S.type_expression -> unit -> type_value
val t_signature : ?s:S.type_expression -> unit -> type_value
val t_unit : ?s:S.type_expression -> unit -> type_value val t_unit : ?s:S.type_expression -> unit -> type_value
val t_option : type_value -> ?s:S.type_expression -> unit -> type_value val t_option : type_value -> ?s:S.type_expression -> unit -> type_value
val t_pair : type_value -> type_value -> ?s:S.type_expression -> unit -> type_value val t_pair : type_value -> type_value -> ?s:S.type_expression -> unit -> type_value
@ -118,6 +119,8 @@ val e_string : string -> expression
val e_bytes : bytes -> expression val e_bytes : bytes -> expression
val e_timestamp : int -> expression val e_timestamp : int -> expression
val e_address : string -> expression val e_address : string -> expression
val e_signature : string -> expression
val e_key : string -> expression
val e_operation : Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation -> expression val e_operation : Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation -> expression
val e_lambda : lambda -> expression val e_lambda : lambda -> expression
val e_pair : value -> value -> expression val e_pair : value -> value -> expression

View File

@ -380,6 +380,12 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_address a, Literal_address b when a = b -> ok () | Literal_address a, Literal_address b when a = b -> ok ()
| Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b | Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b
| Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
| Literal_signature a, Literal_signature b when a = b -> ok ()
| Literal_signature _, Literal_signature _ -> fail @@ different_literals "different signature" a b
| Literal_signature _, _ -> fail @@ different_literals_because_different_types "signature vs non-signature" a b
| Literal_key a, Literal_key b when a = b -> ok ()
| Literal_key _, Literal_key _ -> fail @@ different_literals "different key" a b
| Literal_key _, _ -> fail @@ different_literals_because_different_types "key vs non-key" a b
| Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
| Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b | Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b

View File

@ -126,6 +126,8 @@ and literal =
| Literal_string of string | Literal_string of string
| Literal_bytes of bytes | Literal_bytes of bytes
| Literal_address of string | Literal_address of string
| Literal_signature of string
| Literal_key of string
| Literal_operation of Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation | Literal_operation of Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation
and access = and access =

View File

@ -21,6 +21,7 @@ let type_base ppf : type_base -> _ = function
| Base_bytes -> fprintf ppf "bytes" | Base_bytes -> fprintf ppf "bytes"
| Base_operation -> fprintf ppf "operation" | Base_operation -> fprintf ppf "operation"
| Base_signature -> fprintf ppf "signature" | Base_signature -> fprintf ppf "signature"
| Base_key -> fprintf ppf "key"
let rec type_ ppf : type_value -> _ = function let rec type_ ppf : type_value -> _ = function
| T_or(a, b) -> fprintf ppf "(%a) | (%a)" annotated a annotated b | T_or(a, b) -> fprintf ppf "(%a) | (%a)" annotated a annotated b

View File

@ -5,7 +5,7 @@ type type_base =
| Base_bool | Base_bool
| Base_int | Base_nat | Base_tez | Base_int | Base_nat | Base_tez
| Base_timestamp | Base_timestamp
| Base_string | Base_bytes | Base_address | Base_string | Base_bytes | Base_address | Base_key
| Base_operation | Base_signature | Base_operation | Base_signature
type 'a annotated = string option * 'a type 'a annotated = string option * 'a

View File

@ -101,6 +101,8 @@ module Substitution = struct
| (T.Literal_string _ as x) | (T.Literal_string _ as x)
| (T.Literal_bytes _ as x) | (T.Literal_bytes _ as x)
| (T.Literal_address _ as x) | (T.Literal_address _ as x)
| (T.Literal_signature _ as x)
| (T.Literal_key _ as x)
| (T.Literal_operation _ as x) -> | (T.Literal_operation _ as x) ->
ok @@ x ok @@ x
and s_matching_expr ~v ~expr : T.matching_expr w = fun _ -> and s_matching_expr ~v ~expr : T.matching_expr w = fun _ ->