typer: bugfix: tuple is now a built-in type constructor

This commit is contained in:
Suzanne Dupéron 2019-12-06 18:32:00 +01:00 committed by Suzanne Dupéron
parent 30dac09494
commit 0f420eaaf5
18 changed files with 72 additions and 70 deletions

View File

@ -41,7 +41,7 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_3.mligo" ; "main" ] ;
[%expect {|
ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"tuple[int , string , bool]","b":"tuple[int , string]"}
ligo: in file "error_typer_3.mligo", line 3, characters 34-53. different number of arguments to type constructors: Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the TC_tuple type constructor, but they have 3 and 2 arguments, respectively) {"a":"(TO_tuple[int , string , bool])","b":"(TO_tuple[int , string])","op":"TC_tuple","len_a":"3","len_b":"2"}
If you're not sure how to fix this error, you can

View File

@ -14,11 +14,11 @@ let assert_equal_contract_type : check_type -> string -> Ast_typed.program -> As
match entry_point.type_annotation.type_value' with
| T_arrow (args,_) -> (
match args.type_value' with
| T_tuple [param_exp;storage_exp] -> (
| T_operator (TC_tuple [param_exp;storage_exp]) -> (
match c with
| Check_parameter -> assert_type_value_eq (param_exp, param.type_annotation)
| Check_storage -> assert_type_value_eq (storage_exp, param.type_annotation)
)
| _ -> dummy_fail
)
| _ -> dummy_fail )
| _ -> dummy_fail )

View File

@ -242,7 +242,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
| [hd] -> simpl_type_expression hd
| lst ->
let%bind lst = bind_map_list simpl_type_expression lst in
ok @@ make_t @@ T_tuple lst
ok @@ make_t @@ T_operator (TC_tuple lst)
let rec simpl_expression :
Raw.expr -> expr result = fun t ->

View File

@ -266,7 +266,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
| [hd] -> simpl_type_expression hd
| lst ->
let%bind lst = bind_list @@ List.map simpl_type_expression lst in
ok @@ make_t @@ T_tuple lst
ok @@ make_t @@ T_operator (TC_tuple lst)
let simpl_projection : Raw.projection Region.reg -> _ = fun p ->
let (p' , loc) = r_split p in
@ -636,7 +636,7 @@ and simpl_fun_decl :
let arguments_name = Var.of_name "arguments" in
let%bind params = bind_map_list simpl_param lst in
let (binder , input_type) =
let type_expression = T_tuple (List.map snd params) in
let type_expression = t_tuple (List.map snd params) in
(arguments_name , type_expression) in
let%bind tpl_declarations =
let aux = fun i x ->
@ -657,8 +657,8 @@ and simpl_fun_decl :
let aux prec cur = cur (Some prec) in
bind_fold_right_list aux result body in
let expression =
e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in
let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in
e_lambda ~loc binder (Some input_type) (Some output_type) result in
let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in
ok ((Var.of_name fun_name.value, type_annotation), expression)
)
)
@ -694,7 +694,7 @@ and simpl_fun_expression :
let arguments_name = Var.of_name "arguments" in
let%bind params = bind_map_list simpl_param lst in
let (binder , input_type) =
let type_expression = T_tuple (List.map snd params) in
let type_expression = t_tuple (List.map snd params) in
(arguments_name , type_expression) in
let%bind tpl_declarations =
let aux = fun i x ->
@ -715,8 +715,8 @@ and simpl_fun_expression :
let aux prec cur = cur (Some prec) in
bind_fold_right_list aux result body in
let expression =
e_lambda ~loc binder (Some (make_t @@ input_type)) (Some output_type) result in
let type_annotation = Some (make_t @@ T_arrow (make_t input_type, output_type)) in
e_lambda ~loc binder (Some (input_type)) (Some output_type) result in
let type_annotation = Some (make_t @@ T_arrow (input_type, output_type)) in
ok (type_annotation, expression)
)
)

View File

@ -34,8 +34,6 @@ module Wrap = struct
let rec type_expression_to_type_value : T.type_value -> O.type_value = fun te ->
match te.type_value' with
| T_tuple types ->
P_constant (C_tuple, List.map type_expression_to_type_value types)
| T_sum kvmap ->
P_constant (C_variant, T.CMap.to_list @@ T.CMap.map type_expression_to_type_value kvmap)
| T_record kvmap ->
@ -71,15 +69,13 @@ module Wrap = struct
| TC_list l -> (C_list, [l])
| TC_contract c -> (C_contract, [c])
| TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
| TC_tuple lst -> (C_tuple, lst)
)
in
P_constant (csttag, List.map type_expression_to_type_value args)
let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_value = fun te ->
match te.type_expression' with
| T_tuple types ->
P_constant (C_tuple, List.map type_expression_to_type_value_copypasted types)
| T_sum kvmap ->
P_constant (C_variant, I.CMap.to_list @@ I.CMap.map type_expression_to_type_value_copypasted kvmap)
| T_record kvmap ->
@ -104,6 +100,7 @@ module Wrap = struct
| TC_big_map ( k , v ) -> (C_big_map, [k;v])
| TC_contract c -> (C_contract, [c])
| TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ])
| TC_tuple lst -> (C_tuple, lst)
)
in
P_constant (csttag, List.map type_expression_to_type_value_copypasted args)

View File

@ -334,9 +334,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let%bind a' = evaluate_type e a in
let%bind b' = evaluate_type e b in
return (T_arrow (a', b'))
| T_tuple lst ->
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
return (T_tuple lst')
| T_sum m ->
let aux k v prev =
let%bind prev' = prev in
@ -386,6 +383,9 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let%bind arg' = evaluate_type e arg in
let%bind ret' = evaluate_type e ret in
ok @@ O.TC_arrow ( arg' , ret' )
| TC_tuple lst ->
let%bind lst' = bind_map_list (evaluate_type e) lst in
ok @@ O.TC_tuple lst'
in
return (T_operator (opt))
@ -1022,9 +1022,6 @@ let type_program' : I.program -> O.program result = fun p ->
let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
(* TODO: or should we use t.simplified if present? *)
let%bind t = match t.type_value' with
| O.T_tuple x ->
let%bind x' = bind_map_list untype_type_expression x in
ok @@ I.T_tuple x'
| O.T_sum x ->
let%bind x' = I.bind_map_cmap untype_type_expression x in
ok @@ I.T_sum x'
@ -1064,6 +1061,9 @@ let rec untype_type_expression (t:O.type_value) : (I.type_expression) result =
let%bind arg' = untype_type_expression arg in
let%bind ret' = untype_type_expression ret in
ok @@ I.TC_arrow ( arg' , ret' )
| O.TC_tuple lst ->
let%bind lst' = bind_map_list untype_type_expression lst in
ok @@ I.TC_tuple lst'
in
ok @@ I.T_operator (type_name)
in

View File

@ -327,9 +327,6 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let%bind a' = evaluate_type e a in
let%bind b' = evaluate_type e b in
return (T_arrow (a', b'))
| T_tuple lst ->
let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in
return (T_tuple lst')
| T_sum m ->
let aux k v prev =
let%bind prev' = prev in
@ -379,6 +376,9 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
let%bind arg' = evaluate_type e arg in
let%bind ret' = evaluate_type e ret in
ok @@ I.TC_arrow ( arg' , ret' )
| TC_tuple lst ->
let%bind lst' = bind_map_list (evaluate_type e) lst in
ok @@ I.TC_tuple lst'
in
return (T_operator (opt))

View File

@ -173,7 +173,7 @@ let rec transpile_type (t:AST.type_value) : type_value result =
ok (Some ann, a))
aux node in
ok @@ snd m'
| T_tuple lst ->
| T_operator (TC_tuple lst) ->
let node = Append_tree.of_list lst in
let aux a b : type_value result =
let%bind a = a in

View File

@ -36,15 +36,6 @@ them. please report this to the developers." in
] in
error ~data title content
let unknown_untranspile unknown_type value =
let title () = "untranspiling unknown value" in
let content () = Format.asprintf "can not untranspile %s" unknown_type in
let data = [
("unknown_type" , fun () -> unknown_type) ;
("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ;
] in
error ~data title content
end
open Errors
@ -202,6 +193,16 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
get_string v in
return (E_literal (Literal_string n))
)
| TC_tuple lst ->
let%bind node = match Append_tree.of_list lst with
| Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple"
| Full t -> ok t in
let%bind tpl =
trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@
extract_tuple v node in
let%bind tpl' = bind_list
@@ List.map (fun (x, y) -> untranspile x y) tpl in
return (E_tuple tpl')
)
| T_sum m ->
let lst = kv_list_of_cmap m in
@ -214,16 +215,6 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
extract_constructor v node in
let%bind sub = untranspile v tv in
return (E_constructor (Constructor name, sub))
| T_tuple lst ->
let%bind node = match Append_tree.of_list lst with
| Empty -> fail @@ corner_case ~loc:__LOC__ "empty tuple"
| Full t -> ok t in
let%bind tpl =
trace_strong (corner_case ~loc:__LOC__ "tuple extract") @@
extract_tuple v node in
let%bind tpl' = bind_list
@@ List.map (fun (x, y) -> untranspile x y) tpl in
return (E_tuple tpl')
| T_record m ->
let lst = kv_list_of_lmap m in
let%bind node = match Append_tree.of_list lst with

View File

@ -36,7 +36,7 @@ let t_key_hash : type_expression = make_t @@ T_constant (TC_key_hash)
let t_option o : type_expression = make_t @@ T_operator (TC_option o)
let t_list t : type_expression = make_t @@ T_operator (TC_list t)
let t_variable n : type_expression = make_t @@ T_variable (Var.of_name n)
let t_tuple lst : type_expression = make_t @@ T_tuple lst
let t_tuple lst : type_expression = make_t @@ T_operator (TC_tuple lst)
let t_pair (a , b) : type_expression = t_tuple [a ; b]
let t_record_ez lst =
let lst = List.map (fun (k, v) -> (Label k, v)) lst in

View File

@ -27,8 +27,8 @@ val t_option : type_expression -> type_expression
*)
val t_list : type_expression -> type_expression
val t_variable : string -> type_expression
(*
val t_tuple : type_expression list -> type_expression
(*
val t_record : te_map -> type_expression
*)
val t_pair : ( type_expression * type_expression ) -> type_expression

View File

@ -48,7 +48,7 @@ let t_mutez ?s () : type_value = make_t (T_constant TC_mutez) s
let t_timestamp ?s () : type_value = make_t (T_constant TC_timestamp) s
let t_unit ?s () : type_value = make_t (T_constant TC_unit) s
let t_option o ?s () : type_value = make_t (T_operator (TC_option o)) s
let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s
let t_tuple lst ?s () : type_value = make_t (T_operator (TC_tuple lst)) s
let t_variable t ?s () : type_value = make_t (T_variable t) s
let t_list t ?s () : type_value = make_t (T_operator (TC_list t)) s
let t_set t ?s () : type_value = make_t (T_operator (TC_set t)) s
@ -147,11 +147,11 @@ let get_t_key_hash (t:type_value) : unit result = match t.type_value' with
| _ -> fail @@ Errors.not_a_x_type "key_hash" t ()
let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
| T_tuple lst -> ok lst
| T_operator (TC_tuple lst) -> ok lst
| _ -> fail @@ Errors.not_a_x_type "tuple" t ()
let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_value' with
| T_tuple lst ->
| T_operator (TC_tuple lst) ->
let%bind () =
trace_strong (Errors.not_a_x_type "pair (tuple with two elements)" t ()) @@
Assert.assert_list_size lst 2 in

View File

@ -29,6 +29,21 @@ module Errors = struct
] in
error ~data title message ()
let different_operator_number_of_arguments opa opb lena lenb () =
let title = (thunk "different number of arguments to type constructors") in
assert (String.equal (type_operator_name opa) (type_operator_name opb));
let message () = Format.asprintf
"Expected these two n-ary type constructors to be the same, but they have different numbers of arguments (both use the %s type constructor, but they have %d and %d arguments, respectively)"
(type_operator_name opa) lena lenb in
let data = [
("a" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opa) ;
("b" , fun () -> Format.asprintf "%a" (Stage_common.PP.type_operator PP.type_value) opb) ;
("op" , fun () -> type_operator_name opa) ;
("len_a" , fun () -> Format.asprintf "%d" lena) ;
("len_b" , fun () -> Format.asprintf "%d" lenb) ;
] in
error ~data title message ()
let different_size_type name a b () =
let title () = name ^ " have different sizes" in
let message () = "Expected these two types to be the same, but they're different (both are " ^ name ^ ", but with a different number of arguments)" in
@ -49,8 +64,6 @@ module Errors = struct
let _different_size_constants = different_size_type "type constructors"
let different_size_tuples = different_size_type "tuples"
let different_size_sums = different_size_type "sums"
let different_size_records = different_size_type "records"
@ -301,13 +314,6 @@ open Errors
let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with
| T_tuple ta, T_tuple tb -> (
let%bind _ =
trace_strong (fun () -> (different_size_tuples a b ()))
@@ Assert.assert_true List.(length ta = length tb) in
bind_list_iter assert_type_value_eq (List.combine ta tb)
)
| T_tuple _, _ -> fail @@ different_kinds a b
| T_constant ca, T_constant cb -> (
trace_strong (different_constants ca cb)
@@ Assert.assert_true (ca = cb)
@ -321,10 +327,16 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
| TC_set la, TC_set lb -> ok @@ ([la], [lb])
| TC_map (ka,va), TC_map (kb,vb)
| TC_big_map (ka,va), TC_big_map (kb,vb) -> ok @@ ([ka;va] ,[kb;vb])
| _,_ -> fail @@ different_operators opa opb
| TC_tuple lsta, TC_tuple lstb -> ok @@ (lsta , lstb)
| TC_arrow (froma , toa) , TC_arrow (fromb , tob) -> ok @@ ([froma;toa] , [fromb;tob])
| (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _),
(TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_tuple _ | TC_arrow _) -> fail @@ different_operators opa opb
in
trace (different_types "arguments to type operators" a b)
@@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb)
if List.length lsta <> List.length lstb then
fail @@ different_operator_number_of_arguments opa opb (List.length lsta) (List.length lstb)
else
trace (different_types "arguments to type operators" a b)
@@ bind_list_iter (fun (a,b) -> assert_type_value_eq (a,b) )(List.combine lsta lstb)
)
| T_operator _, _ -> fail @@ different_kinds a b
| T_sum sa, T_sum sb -> (

View File

@ -43,7 +43,6 @@ module Errors : sig
val different_size_type : name -> type_value -> type_value -> unit -> error
val different_props_in_record : string -> string -> unit -> error
val different_size_constants : type_value -> type_value -> unit -> error
val different_size_tuples : type_value -> type_value -> unit -> error
val different_size_sums : type_value -> type_value -> unit -> error
val different_size_records : type_value -> type_value -> unit -> error
val different_types : name -> type_value -> type_value -> unit -> error

View File

@ -141,7 +141,6 @@ let lmap_sep_d x = lmap_sep x (const " , ")
let rec type_expression' : type a . (formatter -> a -> unit) -> formatter -> a type_expression' -> unit =
fun f ppf te ->
match te with
| T_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d f) lst
| T_sum m -> fprintf ppf "sum[%a]" (cmap_sep_d f) m
| T_record m -> fprintf ppf "record[%a]" (lmap_sep_d f ) m
| T_arrow (a, b) -> fprintf ppf "%a -> %a" f a f b
@ -179,6 +178,7 @@ and type_operator : type a . (formatter -> a -> unit) -> formatter -> a type_ope
| TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v
| TC_contract (c) -> Format.asprintf "Contract (%a)" f c
| TC_arrow (a , b) -> Format.asprintf "TC_Arrow (%a,%a)" f a f b
| TC_tuple lst -> Format.asprintf "tuple[%a]" (list_sep_d f) lst
in
fprintf ppf "(TO_%s)" s

View File

@ -9,6 +9,7 @@ let map_type_operator f = function
| TC_map (x , y) -> TC_map (f x , f y)
| TC_big_map (x , y) -> TC_big_map (f x , f y)
| TC_arrow (x , y) -> TC_arrow (f x , f y)
| TC_tuple lst -> TC_tuple (List.map f lst)
let bind_map_type_operator f = function
TC_contract x -> let%bind x = f x in ok @@ TC_contract x
@ -18,6 +19,7 @@ let bind_map_type_operator f = function
| TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y)
| TC_big_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y)
| TC_arrow (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_arrow (x , y)
| TC_tuple lst -> let%bind lst = bind_map_list f lst in ok @@ TC_tuple lst
let type_operator_name = function
TC_contract _ -> "TC_contract"
@ -27,6 +29,7 @@ let type_operator_name = function
| TC_map _ -> "TC_map"
| TC_big_map _ -> "TC_big_map"
| TC_arrow _ -> "TC_arrow"
| TC_tuple _ -> "TC_tuple"
let type_expression'_of_string = function
| "TC_contract" , [x] -> ok @@ T_operator(TC_contract x)
@ -65,6 +68,7 @@ let string_of_type_operator = function
| TC_map (x , y) -> "TC_map" , [x ; y]
| TC_big_map (x , y) -> "TC_big_map" , [x ; y]
| TC_arrow (x , y) -> "TC_arrow" , [x ; y]
| TC_tuple lst -> "TC_tuple" , lst
let string_of_type_constant = function
| TC_unit -> "TC_unit", []
@ -85,5 +89,5 @@ let string_of_type_constant = function
let string_of_type_expression' = function
| T_operator o -> string_of_type_operator o
| T_constant c -> string_of_type_constant c
| T_tuple _|T_sum _|T_record _|T_arrow (_, _)|T_variable _ ->
| T_sum _|T_record _|T_arrow (_, _)|T_variable _ ->
failwith "not a type operator or constant"

View File

@ -66,7 +66,6 @@ and literal =
(* The ast is a tree of node, 'a is the type of the node (type_variable or {type_variable, previous_type}) *)
type 'a type_expression' =
| T_tuple of 'a list
| T_sum of 'a constructor_map
| T_record of 'a label_map
| T_arrow of 'a * 'a
@ -97,6 +96,7 @@ and 'a type_operator =
| TC_map of 'a * 'a
| TC_big_map of 'a * 'a
| TC_arrow of 'a * 'a
| TC_tuple of 'a list
type type_base =
| Base_unit

View File

@ -72,9 +72,9 @@ module Substitution = struct
ok @@ type_name
and s_type_value' : T.type_value' w = fun ~substs -> function
| T.T_tuple type_value_list ->
| T.T_operator (TC_tuple type_value_list) ->
let%bind type_value_list = bind_map_list (s_type_value ~substs) type_value_list in
ok @@ T.T_tuple type_value_list
ok @@ T.T_operator (TC_tuple type_value_list)
| T.T_sum _ -> failwith "TODO: T_sum"
| T.T_record _ -> failwith "TODO: T_record"
| T.T_constant type_name ->
@ -95,7 +95,6 @@ module Substitution = struct
failwith "TODO: T_function"
and s_type_expression' : _ Ast_simplified.type_expression' w = fun ~substs -> function
| Ast_simplified.T_tuple _ -> failwith "TODO: subst: unimplemented case s_type_expression tuple"
| Ast_simplified.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum"
| Ast_simplified.T_record _ -> failwith "TODO: subst: unimplemented case s_type_expression record"
| Ast_simplified.T_arrow (_, _) -> failwith "TODO: subst: unimplemented case s_type_expression arrow"
@ -274,7 +273,7 @@ module Substitution = struct
let self tv = type_value ~tv ~substs in
let (v, expr) = substs in
match tv with
| P_variable v' when String.equal v' v -> expr
| P_variable v' when Var.equal v' v -> expr
| P_variable _ -> tv
| P_constant (x , lst) -> (
let lst' = List.map self lst in