diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index f854940..b9d88e3 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -16,10 +16,6 @@ , infer/2 , unfold_types_in_type/2 , unfold_types_in_type/3 - %% TODO: Newly added - , get_named_argument_constraint_name/1 - , get_named_argument_constraint_args/1 - , get_named_argument_constraint_type/1 ]). %% Newly exported @@ -27,6 +23,11 @@ , freshen_type/2 , freshen_type_sig/2 , infer_const/2 + , app_t/3 + , unify/4 + , create_freshen_tvars/0 + , destroy_freshen_tvars/0 + , freshen/1 ]). -export_type([ utype/0 , typesig/0 @@ -54,57 +55,6 @@ element(1, T) =:= con orelse element(1, T) =:= qcon). --type why_record() :: aeso_syntax:field(aeso_syntax:expr()) - | {var_args, aeso_syntax:ann(), aeso_syntax:expr()} - | {proj, aeso_syntax:ann(), aeso_syntax:expr(), aeso_syntax:id()}. - --record(named_argument_constraint, - {args :: named_args_t(), - name :: aeso_syntax:id(), - type :: utype()}). - --record(dependent_type_constraint, - { named_args_t :: named_args_t() - , named_args :: [aeso_syntax:arg_expr()] - , general_type :: utype() - , specialized_type :: utype() - , context :: term() }). - --type named_argument_constraint() :: #named_argument_constraint{} | #dependent_type_constraint{}. - --record(field_constraint, - { record_t :: utype() - , field :: aeso_syntax:id() - , field_t :: utype() - , kind :: project | create | update %% Projection constraints can match contract - , context :: why_record() }). %% types, but field constraints only record types. - -%% Constraint checking that 'record_t' has precisely 'fields'. --record(record_create_constraint, - { record_t :: utype() - , fields :: [aeso_syntax:id()] - , context :: why_record() }). - --record(is_contract_constraint, - { contract_t :: utype(), - context :: {contract_literal, aeso_syntax:expr()} | - {address_to_contract, aeso_syntax:ann()} | - {bytecode_hash, aeso_syntax:ann()} | - {var_args, aeso_syntax:ann(), aeso_syntax:expr()}, - force_def = false :: boolean() - }). - --type field_constraint() :: #field_constraint{} | #record_create_constraint{} | #is_contract_constraint{}. - --type byte_constraint() :: {is_bytes, utype()} - | {add_bytes, aeso_syntax:ann(), concat | split, utype(), utype(), utype()}. - --type aens_resolve_constraint() :: {aens_resolve_type, utype()}. --type oracle_type_constraint() :: {oracle_type, aeso_syntax:ann(), utype()}. - --type constraint() :: named_argument_constraint() | field_constraint() | byte_constraint() - | aens_resolve_constraint() | oracle_type_constraint(). - -type type() :: aeso_syntax:type(). -type name() :: string(). -type typesig() :: {type_sig, aeso_syntax:ann(), type_constraints(), [aeso_syntax:named_arg_t()], [type()], type()}. @@ -165,11 +115,9 @@ get_option(A, B) -> aeso_tc_options:get_option(A, B). when_option(A, B) -> aeso_tc_options:when_option(A, B). when_warning(A, B) -> aeso_tc_options:when_warning(A, B). -%% -- New functions ---------------------------------------------------------- +%% ------- -get_named_argument_constraint_name(#named_argument_constraint{name = Name}) -> Name. -get_named_argument_constraint_args(#named_argument_constraint{args = Args}) -> Args. -get_named_argument_constraint_type(#named_argument_constraint{type = Type}) -> Type. +ensure_first_order(A, B) -> aeso_tc_type_utils:ensure_first_order(A, B). %% -- The rest --------------------------------------------------------------- @@ -893,11 +841,11 @@ register_implementation(Id, Sig) -> end. infer_nonrec(Env, LetFun) -> - create_constraints(), + aeso_tc_constraints:create_constraints(), NewLetFun = {{_, Sig}, _} = infer_letfun(Env, LetFun), check_special_funs(Env, NewLetFun), register_implementation(get_letfun_id(LetFun), Sig), - solve_then_destroy_and_report_unsolved_constraints(Env), + aeso_tc_constraints:solve_then_destroy_and_report_unsolved_constraints(Env), Result = {TypeSig, _} = aeso_tc_type_utils:instantiate(NewLetFun), print_typesig(TypeSig), Result. @@ -915,7 +863,7 @@ check_special_funs(Env, {{"init", Type}, _}) -> check_special_funs(_, _) -> ok. infer_letrec(Env, Defs) -> - create_constraints(), + aeso_tc_constraints:create_constraints(), Funs = lists:map(fun({letfun, _, {id, Ann, Name}, _, _, _}) -> {Name, fresh_uvar(Ann)}; ({fun_clauses, _, {id, Ann, Name}, _, _}) -> {Name, fresh_uvar(Ann)} end, Defs), @@ -927,12 +875,12 @@ infer_letrec(Env, Defs) -> Got = proplists:get_value(Name, Funs), Expect = aeso_tc_type_utils:typesig_to_fun_t(TypeSig), unify(Env, Got, Expect, {check_typesig, Name, Got, Expect}), - solve_constraints(Env), + aeso_tc_constraints:solve_constraints(Env), ?PRINT_TYPES("Checked ~s : ~s\n", [Name, pp(aeso_tc_type_utils:dereference_deep(Got))]), Res end || LF <- Defs ], - solve_then_destroy_and_report_unsolved_constraints(Env), + aeso_tc_constraints:solve_then_destroy_and_report_unsolved_constraints(Env), TypeSigs = aeso_tc_type_utils:instantiate([Sig || {Sig, _} <- Inferred]), NewDefs = aeso_tc_type_utils:instantiate([D || {_, D} <- Inferred]), [print_typesig(S) || S <- TypeSigs], @@ -1022,22 +970,6 @@ ensure_first_order_entrypoint({letfun, Ann, Id = {id, _, Name}, Args, Ret, _}) - %% rather than being returned. ok. -ensure_first_order(Type, Err) -> - is_first_order(Type) orelse type_error(Err). - -is_first_order({fun_t, _, _, _, _}) -> false; -is_first_order(Ts) when is_list(Ts) -> lists:all(fun is_first_order/1, Ts); -is_first_order(Tup) when is_tuple(Tup) -> is_first_order(tuple_to_list(Tup)); -is_first_order(_) -> true. - -ensure_monomorphic(Type, Err) -> - is_monomorphic(Type) orelse type_error(Err). - -is_monomorphic({tvar, _, _}) -> false; -is_monomorphic(Ts) when is_list(Ts) -> lists:all(fun is_monomorphic/1, Ts); -is_monomorphic(Tup) when is_tuple(Tup) -> is_monomorphic(tuple_to_list(Tup)); -is_monomorphic(_) -> true. - check_state_init(Env) -> Top = aeso_tc_env:namespace(Env), StateType = aeso_tc_env:lookup_type(Env, {id, [{origin, system}], "state"}), @@ -1117,8 +1049,7 @@ infer_expr(_Env, Body={oracle_query_id, As, _}) -> {typed, As, Body, {app_t, As, {id, As, "oracle_query"}, [Q, R]}}; infer_expr(_Env, Body={contract_pubkey, As, _}) -> Con = fresh_uvar(As), - add_constraint([#is_contract_constraint{ contract_t = Con, - context = {contract_literal, Body} }]), + aeso_tc_constraints:add_is_contract_constraint(Con, {contract_literal, Body}), {typed, As, Body, Con}; infer_expr(_Env, Body={id, As, "_"}) -> {typed, As, Body, fresh_uvar(As)}; @@ -1214,17 +1145,17 @@ infer_expr(Env, {app, Ann, Fun, Args0} = App) -> ResultType = fresh_uvar(Ann), unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, GeneralResultType}, When), when_warning(warn_negative_spend, fun() -> warn_potential_negative_spend(Ann, NewFun1, NewArgs) end), - [ add_constraint({aens_resolve_type, GeneralResultType}) + [ aeso_tc_constraints:add_aens_resolve_constraint(GeneralResultType) || element(3, FunName) =:= ["AENS", "resolve"] ], - [ add_constraint({oracle_type, Ann, OType}) + [ aeso_tc_constraints:add_oracle_type_constraint(Ann, OType) || OType <- [get_oracle_type(FunName, ArgTypes, GeneralResultType)], OType =/= false ], - add_constraint( - #dependent_type_constraint{ named_args_t = NamedArgsVar, - named_args = NamedArgs1, - general_type = GeneralResultType, - specialized_type = ResultType, - context = {check_return, App} }), + aeso_tc_constraints:add_dependent_type_constraint( + NamedArgsVar, + NamedArgs1, + GeneralResultType, + ResultType, + {check_return, App}), {typed, Ann, {app, Ann, NewFun1, NamedArgs1 ++ NewArgs}, aeso_tc_type_utils:dereference(ResultType)} end; infer_expr(Env, {'if', Attrs, Cond, Then, Else}) -> @@ -1244,19 +1175,13 @@ infer_expr(Env, {record, Attrs, Fields}) -> NewFields = [{field, A, FieldName, infer_expr(Env, Expr)} || {field, A, FieldName, Expr} <- Fields], RecordType1 = unfold_types_in_type(Env, RecordType), - add_constraint([ #record_create_constraint{ - record_t = RecordType1, - fields = [ FieldName || {field, _, [{proj, _, FieldName}], _} <- Fields ], - context = Attrs } || not aeso_tc_env:in_pattern(Env) ] ++ - [begin - [{proj, _, FieldName}] = LV, - #field_constraint{ - record_t = RecordType1, - field = FieldName, - field_t = T, - kind = create, - context = Fld} - end || {Fld, {field, _, LV, {typed, _, _, T}}} <- lists:zip(Fields, NewFields)]), + [ aeso_tc_constraints:add_record_create_constraint( + RecordType1, + [ FieldName || {field, _, [{proj, _, FieldName}], _} <- Fields ], + Attrs) + || not aeso_tc_env:in_pattern(Env) ], + [ aeso_tc_constraints:add_field_constraint(RecordType1, FieldName, T, create, Fld) + || {Fld, {field, _, [{proj, _, FieldName}], {typed, _, _, T}}} <- lists:zip(Fields, NewFields) ], {typed, Attrs, {record, Attrs, NewFields}, RecordType}; infer_expr(Env, {record, Attrs, Record, Update}) -> NewRecord = {typed, _, _, RecordType} = infer_expr(Env, Record), @@ -1265,12 +1190,12 @@ infer_expr(Env, {record, Attrs, Record, Update}) -> infer_expr(Env, {proj, Attrs, Record, FieldName}) -> NewRecord = {typed, _, _, RecordType} = infer_expr(Env, Record), FieldType = fresh_uvar(Attrs), - add_constraint([#field_constraint{ - record_t = unfold_types_in_type(Env, RecordType), - field = FieldName, - field_t = FieldType, - kind = project, - context = {proj, Attrs, Record, FieldName} }]), + aeso_tc_constraints:add_field_constraint( + unfold_types_in_type(Env, RecordType), + FieldName, + FieldType, + project, + {proj, Attrs, Record, FieldName}), {typed, Attrs, {proj, Attrs, NewRecord, FieldName}, FieldType}; %% Maps infer_expr(Env, {map_get, Attrs, Map, Key}) -> %% map lookup @@ -1445,18 +1370,13 @@ check_contract_construction(Env, ForceDef, ContractT, Fun, NamedArgsT, ArgTypes, InitT = fresh_uvar(Ann), unify(Env, InitT, {fun_t, Ann, NamedArgsT, ArgTypes, fresh_uvar(Ann)}, {checking_init_args, Ann, ContractT, ArgTypes}), unify(Env, RetT, ContractT, {return_contract, Fun, ContractT}), - add_constraint( - [ #field_constraint{ - record_t = unfold_types_in_type(Env, ContractT), - field = {id, Ann, ?CONSTRUCTOR_MOCK_NAME}, - field_t = InitT, - kind = project, - context = {var_args, Ann, Fun} } - , #is_contract_constraint{ contract_t = ContractT, - context = {var_args, Ann, Fun}, - force_def = ForceDef - } - ]), + aeso_tc_constraints:add_field_constraint( + unfold_types_in_type(Env, ContractT), + {id, Ann, ?CONSTRUCTOR_MOCK_NAME}, + InitT, + project, + {var_args, Ann, Fun}), + aeso_tc_constraints:add_is_contract_constraint(ContractT, {var_args, Ann, Fun}, ForceDef), ok. split_args(Args0) -> @@ -1467,11 +1387,7 @@ split_args(Args0) -> infer_named_arg(Env, NamedArgs, {named_arg, Ann, Id, E}) -> CheckedExpr = {typed, _, _, ArgType} = infer_expr(Env, E), check_stateful_named_arg(Env, Id, E), - add_constraint( - #named_argument_constraint{ - args = NamedArgs, - name = Id, - type = ArgType }), + aeso_tc_constraints:add_named_argument_constraint(NamedArgs, Id, ArgType), {named_arg, Ann, Id, CheckedExpr}. check_map_update(Env, {field, Ann, [{map_get, Ann1, Key}], Val}, KeyType, ValType) -> @@ -1505,12 +1421,12 @@ check_record_update(Env, RecordType, Fld) -> FunType = {fun_t, Ann1, [], [FldType], FldType}, {field_upd, Ann, LV, check_expr(Env, Fun, FunType)} end, - add_constraint([#field_constraint{ - record_t = unfold_types_in_type(Env, RecordType), - field = FieldName, - field_t = FldType, - kind = update, - context = Fld }]), + aeso_tc_constraints:add_field_constraint( + unfold_types_in_type(Env, RecordType), + FieldName, + FldType, + update, + Fld), Fld1. infer_op(Env, As, Op, Args, InferOp) -> @@ -1579,9 +1495,9 @@ infer_const(Env, {letval, Ann, TypedId = {typed, _, Id = {id, _, _}, Type}, Expr {letval, Ann, TypedId, NewExpr}; infer_const(Env, {letval, Ann, Id = {id, AnnId, _}, Expr}) -> check_valid_const_expr(Expr) orelse type_error({invalid_const_expr, Id}), - create_constraints(), + aeso_tc_constraints:create_constraints(), NewExpr = {typed, _, _, Type} = infer_expr(aeso_tc_env:set_current_const(Id, Env), Expr), - solve_then_destroy_and_report_unsolved_constraints(Env), + aeso_tc_constraints:solve_then_destroy_and_report_unsolved_constraints(Env), IdType = setelement(2, Type, AnnId), NewId = {typed, aeso_syntax:get_ann(Id), Id, IdType}, aeso_tc_type_utils:instantiate({letval, Ann, NewId, NewExpr}). @@ -1656,129 +1572,6 @@ free_vars(L) when is_list(L) -> [V || Elem <- L, V <- free_vars(Elem)]. -%% -- Constraints -- - -create_constraints() -> - aeso_tc_ets_manager:ets_new(constraints, [ordered_set]). - --spec add_constraint(constraint() | [constraint()]) -> true. -add_constraint(Constraint) -> - aeso_tc_ets_manager:ets_insert_ordered(constraints, Constraint). - -get_constraints() -> - aeso_tc_ets_manager:ets_tab2list_ordered(constraints). - -destroy_constraints() -> - aeso_tc_ets_manager:ets_delete(constraints). - --spec solve_constraints(env()) -> ok. -solve_constraints(Env) -> - %% First look for record fields that appear in only one type definition - IsAmbiguous = - fun(#field_constraint{ - record_t = RecordType, - field = Field={id, _Attrs, FieldName}, - field_t = FieldType, - kind = Kind, - context = When }) -> - Arity = aeso_tc_type_utils:fun_arity(aeso_tc_type_utils:dereference_deep(FieldType)), - FieldInfos = case Arity of - none -> aeso_tc_env:lookup_record_field(Env, FieldName, Kind); - _ -> aeso_tc_env:lookup_record_field_arity(Env, FieldName, Arity, Kind) - end, - case FieldInfos of - [] -> - type_error({undefined_field, Field}), - false; - [Fld] -> - FldType = aeso_tc_env:field_info_field_t(Fld), - RecType = aeso_tc_env:field_info_record_t(Fld), - create_freshen_tvars(), - FreshFldType = freshen(FldType), - FreshRecType = freshen(RecType), - destroy_freshen_tvars(), - unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}), - unify(Env, FreshRecType, RecordType, {record_constraint, FreshRecType, RecordType, When}), - false; - _ -> - %% ambiguity--need cleverer strategy - true - end; - (_) -> true - end, - AmbiguousConstraints = lists:filter(IsAmbiguous, get_constraints()), - - % The two passes on AmbiguousConstraints are needed - solve_ambiguous_constraints(Env, AmbiguousConstraints ++ AmbiguousConstraints). - --spec solve_ambiguous_constraints(env(), [constraint()]) -> ok. -solve_ambiguous_constraints(Env, Constraints) -> - Unknown = solve_known_record_types(Env, Constraints), - if Unknown == [] -> ok; - length(Unknown) < length(Constraints) -> - %% progress! Keep trying. - solve_ambiguous_constraints(Env, Unknown); - true -> - case solve_unknown_record_types(Env, Unknown) of - true -> %% Progress! - solve_ambiguous_constraints(Env, Unknown); - _ -> ok %% No progress. Report errors later. - end - end. - -solve_then_destroy_and_report_unsolved_constraints(Env) -> - solve_constraints(Env), - destroy_and_report_unsolved_constraints(Env). - -destroy_and_report_unsolved_constraints(Env) -> - {FieldCs, OtherCs} = - lists:partition(fun(#field_constraint{}) -> true; (_) -> false end, - get_constraints()), - {CreateCs, OtherCs1} = - lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end, - OtherCs), - {ContractCs, OtherCs2} = - lists:partition(fun(#is_contract_constraint{}) -> true; (_) -> false end, OtherCs1), - {NamedArgCs, OtherCs3} = - lists:partition(fun(#dependent_type_constraint{}) -> true; - (#named_argument_constraint{}) -> true; - (_) -> false - end, OtherCs2), - {BytesCs, OtherCs4} = - lists:partition(fun({is_bytes, _}) -> true; - ({add_bytes, _, _, _, _, _}) -> true; - (_) -> false - end, OtherCs3), - {AensResolveCs, OtherCs5} = - lists:partition(fun({aens_resolve_type, _}) -> true; - (_) -> false - end, OtherCs4), - {OracleTypeCs, []} = - lists:partition(fun({oracle_type, _, _}) -> true; - (_) -> false - end, OtherCs5), - - Unsolved = [ S || S <- [ solve_constraint(Env, aeso_tc_type_utils:dereference_deep(C)) || C <- NamedArgCs ], - S == unsolved ], - [ type_error({unsolved_named_argument_constraint, C}) || C <- Unsolved ], - - Unknown = solve_known_record_types(Env, FieldCs), - if Unknown == [] -> ok; - true -> - case solve_unknown_record_types(Env, Unknown) of - true -> ok; - Errors -> [ type_error(Err) || Err <- Errors ] - end - end, - - check_record_create_constraints(Env, CreateCs), - check_is_contract_constraints(Env, ContractCs), - check_bytes_constraints(Env, BytesCs), - check_aens_resolve_constraints(Env, AensResolveCs), - check_oracle_type_constraints(Env, OracleTypeCs), - - destroy_constraints(). - get_oracle_type({qid, _, ["Oracle", "register"]}, _ , OType) -> OType; get_oracle_type({qid, _, ["Oracle", "query"]}, [OType| _], _ ) -> OType; get_oracle_type({qid, _, ["Oracle", "get_question"]}, [OType| _], _ ) -> OType; @@ -1788,276 +1581,6 @@ get_oracle_type({qid, _, ["Oracle", "check_query"]}, [OType| _], _ ) -> OTyp get_oracle_type({qid, _, ["Oracle", "respond"]}, [OType| _], _ ) -> OType; get_oracle_type(_Fun, _Args, _Ret) -> false. -%% -- Named argument constraints -- - -%% If false, a type error has been emitted, so it's safe to drop the constraint. --spec check_named_argument_constraint(env(), named_argument_constraint()) -> true | false | unsolved. -check_named_argument_constraint(_Env, #named_argument_constraint{ args = {uvar, _, _} }) -> - unsolved; -check_named_argument_constraint(Env, - C = #named_argument_constraint{ args = Args, - name = Id = {id, _, Name}, - type = Type }) -> - case [ T || {named_arg_t, _, {id, _, Name1}, T, _} <- Args, Name1 == Name ] of - [] -> - type_error({bad_named_argument, Args, Id}), - false; - [T] -> unify(Env, T, Type, {check_named_arg_constraint, C}), true - end; -check_named_argument_constraint(Env, - #dependent_type_constraint{ named_args_t = NamedArgsT0, - named_args = NamedArgs, - general_type = GenType, - specialized_type = SpecType, - context = {check_return, App} }) -> - NamedArgsT = aeso_tc_type_utils:dereference(NamedArgsT0), - case aeso_tc_type_utils:dereference(NamedArgsT0) of - [_ | _] = NamedArgsT -> - GetVal = fun(Name, Default) -> - hd([ Val || {named_arg, _, {id, _, N}, Val} <- NamedArgs, N == Name] ++ - [ Default ]) - end, - ArgEnv = maps:from_list([ {Name, GetVal(Name, Default)} - || {named_arg_t, _, {id, _, Name}, _, Default} <- NamedArgsT ]), - GenType1 = specialize_dependent_type(ArgEnv, GenType), - unify(Env, GenType1, SpecType, {check_expr, App, GenType1, SpecType}), - true; - _ -> unify(Env, GenType, SpecType, {check_expr, App, GenType, SpecType}), true - end. - -specialize_dependent_type(Env, Type) -> - case aeso_tc_type_utils:dereference(Type) of - {if_t, _, {id, _, Arg}, Then, Else} -> - Val = maps:get(Arg, Env), - case Val of - {typed, _, {bool, _, true}, _} -> Then; - {typed, _, {bool, _, false}, _} -> Else; - _ -> - type_error({named_argument_must_be_literal_bool, Arg, Val}), - fresh_uvar(aeso_syntax:get_ann(Val)) - end; - _ -> Type %% Currently no deep dependent types - end. - -%% -- Bytes constraints -- - -solve_constraint(_Env, #field_constraint{record_t = {uvar, _, _}}) -> - not_solved; -solve_constraint(Env, C = #field_constraint{record_t = RecType, - field = FieldName, - field_t = FieldType, - context = When}) -> - RecId = record_type_name(RecType), - Attrs = aeso_syntax:get_ann(RecId), - case aeso_tc_env:lookup_type(Env, RecId) of - {_, {_Ann, {Formals, {What, Fields}}}} when What =:= record_t; What =:= contract_t -> - FieldTypes = [{Name, Type} || {field_t, _, {id, _, Name}, Type} <- Fields], - {id, _, FieldString} = FieldName, - case proplists:get_value(FieldString, FieldTypes) of - undefined -> - type_error({missing_field, FieldName, RecId}), - not_solved; - FldType -> - create_freshen_tvars(), - FreshFldType = freshen(FldType), - FreshRecType = freshen(app_t(Attrs, RecId, Formals)), - destroy_freshen_tvars(), - unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}), - unify(Env, FreshRecType, RecType, {record_constraint, FreshRecType, RecType, When}), - C - end; - _ -> - type_error({not_a_record_type, aeso_tc_type_utils:instantiate(RecType), When}), - not_solved - end; -solve_constraint(Env, C = #dependent_type_constraint{}) -> - check_named_argument_constraint(Env, C); -solve_constraint(Env, C = #named_argument_constraint{}) -> - check_named_argument_constraint(Env, C); -solve_constraint(_Env, {is_bytes, _}) -> ok; -solve_constraint(Env, {add_bytes, Ann, _, A0, B0, C0}) -> - A = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(A0)), - B = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(B0)), - C = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(C0)), - case {A, B, C} of - {{bytes_t, _, M}, {bytes_t, _, N}, _} -> unify(Env, {bytes_t, Ann, M + N}, C, {at, Ann}); - {{bytes_t, _, M}, _, {bytes_t, _, R}} when R >= M -> unify(Env, {bytes_t, Ann, R - M}, B, {at, Ann}); - {_, {bytes_t, _, N}, {bytes_t, _, R}} when R >= N -> unify(Env, {bytes_t, Ann, R - N}, A, {at, Ann}); - _ -> ok - end; -solve_constraint(_, _) -> ok. - -check_bytes_constraints(Env, Constraints) -> - InAddConstraint = [ T || {add_bytes, _, _, A, B, C} <- Constraints, - T <- [A, B, C], - element(1, T) /= bytes_t ], - %% Skip is_bytes constraints for types that occur in add_bytes constraints - %% (no need to generate error messages for both is_bytes and add_bytes). - Skip = fun({is_bytes, T}) -> lists:member(T, InAddConstraint); - (_) -> false end, - [ check_bytes_constraint(Env, C) || C <- Constraints, not Skip(C) ]. - -check_bytes_constraint(Env, {is_bytes, Type}) -> - Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)), - case Type1 of - {bytes_t, _, _} -> ok; - _ -> - type_error({unknown_byte_length, Type}) - end; -check_bytes_constraint(Env, {add_bytes, Ann, Fun, A0, B0, C0}) -> - A = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(A0)), - B = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(B0)), - C = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(C0)), - case {A, B, C} of - {{bytes_t, _, _M}, {bytes_t, _, _N}, {bytes_t, _, _R}} -> - ok; %% If all are solved we checked M + N == R in solve_constraint. - _ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C}) - end. - -check_aens_resolve_constraints(_Env, []) -> - ok; -check_aens_resolve_constraints(Env, [{aens_resolve_type, Type} | Rest]) -> - Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)), - {app_t, _, {id, _, "option"}, [Type2]} = Type1, - case Type2 of - {id, _, "string"} -> ok; - {id, _, "address"} -> ok; - {con, _, _} -> ok; - {app_t, _, {id, _, "oracle"}, [_, _]} -> ok; - {app_t, _, {id, _, "oracle_query"}, [_, _]} -> ok; - _ -> type_error({invalid_aens_resolve_type, aeso_syntax:get_ann(Type), Type2}) - end, - check_aens_resolve_constraints(Env, Rest). - -check_oracle_type_constraints(_Env, []) -> - ok; -check_oracle_type_constraints(Env, [{oracle_type, Ann, OType} | Rest]) -> - Type = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(OType)), - {app_t, _, {id, _, "oracle"}, [QType, RType]} = Type, - ensure_monomorphic(QType, {invalid_oracle_type, polymorphic, query, Ann, Type}), - ensure_monomorphic(RType, {invalid_oracle_type, polymorphic, response, Ann, Type}), - ensure_first_order(QType, {invalid_oracle_type, higher_order, query, Ann, Type}), - ensure_first_order(RType, {invalid_oracle_type, higher_order, response, Ann, Type}), - check_oracle_type_constraints(Env, Rest). - -%% -- Field constraints -- - -check_record_create_constraints(_, []) -> ok; -check_record_create_constraints(Env, [C | Cs]) -> - #record_create_constraint{ - record_t = Type, - fields = Fields, - context = When } = C, - Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)), - try aeso_tc_env:lookup_type(Env, record_type_name(Type1)) of - {_QId, {_Ann, {_Args, {record_t, RecFields}}}} -> - ActualNames = [ Fld || {field_t, _, {id, _, Fld}, _} <- RecFields ], - GivenNames = [ Fld || {id, _, Fld} <- Fields ], - case ActualNames -- GivenNames of %% We know already that we don't have too many fields - [] -> ok; - Missing -> type_error({missing_fields, When, Type1, Missing}) - end; - _ -> %% We can get here if there are other type errors. - ok - catch _:_ -> %% Might be unsolved, we get a different error in that case - ok - end, - check_record_create_constraints(Env, Cs). - -is_contract_defined(C) -> - aeso_tc_ets_manager:ets_lookup(defined_contracts, qname(C)) =/= []. - -check_is_contract_constraints(_Env, []) -> ok; -check_is_contract_constraints(Env, [C | Cs]) -> - #is_contract_constraint{ contract_t = Type, context = Cxt, force_def = ForceDef } = C, - Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)), - TypeName = record_type_name(Type1), - case aeso_tc_env:lookup_type(Env, TypeName) of - {_, {_Ann, {[], {contract_t, _}}}} -> - case not ForceDef orelse is_contract_defined(TypeName) of - true -> ok; - false -> type_error({contract_lacks_definition, Type1, Cxt}) - end; - _ -> type_error({not_a_contract_type, Type1, Cxt}) - end, - check_is_contract_constraints(Env, Cs). - --spec solve_unknown_record_types(env(), [field_constraint()]) -> true | [tuple()]. -solve_unknown_record_types(Env, Unknown) -> - UVars = lists:usort([UVar || #field_constraint{record_t = UVar = {uvar, _, _}} <- Unknown]), - Solutions = [solve_for_uvar(Env, UVar, [{Kind, When, Field} - || #field_constraint{record_t = U, field = Field, kind = Kind, context = When} <- Unknown, - U == UVar]) - || UVar <- UVars], - case lists:member(true, Solutions) of - true -> true; - false -> Solutions - end. - -%% This will solve all kinds of constraints but will only return the -%% unsolved field constraints --spec solve_known_record_types(env(), [constraint()]) -> [field_constraint()]. -solve_known_record_types(Env, Constraints) -> - DerefConstraints = lists:map(fun(C = #field_constraint{record_t = RecordType}) -> - C#field_constraint{record_t = aeso_tc_type_utils:dereference(RecordType)}; - (C) -> aeso_tc_type_utils:dereference_deep(C) - end, Constraints), - SolvedConstraints = lists:map(fun(C) -> solve_constraint(Env, aeso_tc_type_utils:dereference_deep(C)) end, DerefConstraints), - Unsolved = DerefConstraints--SolvedConstraints, - lists:filter(fun(#field_constraint{}) -> true; (_) -> false end, Unsolved). - -record_type_name({app_t, _Attrs, RecId, _Args}) when ?is_type_id(RecId) -> - RecId; -record_type_name(RecId) when ?is_type_id(RecId) -> - RecId; -record_type_name(_Other) -> - %% io:format("~p is not a record type\n", [Other]), - {id, [{origin, system}], "not_a_record_type"}. - -solve_for_uvar(Env, UVar = {uvar, Attrs, _}, Fields0) -> - Fields = [{Kind, Fld} || {Kind, _, Fld} <- Fields0], - [{_, When, _} | _] = Fields0, %% Get the location from the first field - %% If we have 'create' constraints they must be complete. - Covering = lists:usort([ Name || {create, {id, _, Name}} <- Fields ]), - %% Does this set of fields uniquely identify a record type? - FieldNames = [ Name || {_Kind, {id, _, Name}} <- Fields ], - UniqueFields = lists:usort(FieldNames), - Candidates = [aeso_tc_env:field_info_record_t(Fld) || Fld <- aeso_tc_env:lookup_record_field(Env, hd(FieldNames))], - TypesAndFields = [case aeso_tc_env:lookup_type(Env, record_type_name(RecType)) of - {_, {_, {_, {record_t, RecFields}}}} -> - {RecType, [Field || {field_t, _, {id, _, Field}, _} <- RecFields]}; - {_, {_, {_, {contract_t, ConFields}}}} -> - %% TODO: is this right? - {RecType, [Field || {field_t, _, {id, _, Field}, _} <- ConFields]}; - false -> %% impossible? - error({no_definition_for, record_type_name(RecType), in, Env}) - end - || RecType <- Candidates], - PartialSolutions = - lists:sort([{RecType, if Covering == [] -> []; true -> RecFields -- Covering end} - || {RecType, RecFields} <- TypesAndFields, - UniqueFields -- RecFields == []]), - Solutions = [RecName || {RecName, []} <- PartialSolutions], - case {Solutions, PartialSolutions} of - {[], []} -> - {no_records_with_all_fields, Fields}; - {[], _} -> - case PartialSolutions of - [{RecType, Missing} | _] -> %% TODO: better error if ambiguous - {missing_fields, When, RecType, Missing} - end; - {[RecType], _} -> - RecName = record_type_name(RecType), - {_, {_, {Formals, {_RecOrCon, _}}}} = aeso_tc_env:lookup_type(Env, RecName), - create_freshen_tvars(), - FreshRecType = freshen(app_t(Attrs, RecName, Formals)), - destroy_freshen_tvars(), - unify(Env, UVar, FreshRecType, {solve_rec_type, UVar, Fields}), - true; - {StillPossible, _} -> - {ambiguous_record, Fields, StillPossible} - end. - %% During type inference, record types are represented by their %% names. But, before we pass the typed program to the code generator, %% we replace record types annotating expressions with their @@ -2365,7 +1888,7 @@ freshen(Ann, {tvar, _, Name}) -> NewT; freshen(Ann, {bytes_t, _, any}) -> X = fresh_uvar(Ann), - add_constraint({is_bytes, X}), + aeso_tc_constraints:add_is_bytes_constraint(X), X; freshen(Ann, T) when is_tuple(T) -> list_to_tuple(freshen(Ann, tuple_to_list(T))); @@ -2381,12 +1904,10 @@ freshen_type_sig(Ann, TypeSig = {type_sig, _, Constr, _, _, _}) -> apply_typesig_constraint(_Ann, none, _FunT) -> ok; apply_typesig_constraint(Ann, address_to_contract, {fun_t, _, [], [_], Type}) -> - add_constraint([#is_contract_constraint{ contract_t = Type, - context = {address_to_contract, Ann}}]); + aeso_tc_constraints:add_is_contract_constraint(Type, {address_to_contract, Ann}); apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) -> - add_constraint({add_bytes, Ann, concat, A, B, C}); + aeso_tc_constraints:add_add_bytes_constraint(Ann, concat, A, B, C); apply_typesig_constraint(Ann, bytes_split, {fun_t, _, [], [C], {tuple_t, _, [A, B]}}) -> - add_constraint({add_bytes, Ann, split, A, B, C}); + aeso_tc_constraints:add_add_bytes_constraint(Ann, split, A, B, C); apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) -> - add_constraint([#is_contract_constraint{ contract_t = Con, - context = {bytecode_hash, Ann} }]). + aeso_tc_constraints:add_is_contract_constraint(Con, {bytecode_hash, Ann}). diff --git a/src/aeso_tc_constraints.erl b/src/aeso_tc_constraints.erl new file mode 100644 index 0000000..fc8d4f2 --- /dev/null +++ b/src/aeso_tc_constraints.erl @@ -0,0 +1,551 @@ +-module(aeso_tc_constraints). + +-export([ solve_constraints/1 + , solve_then_destroy_and_report_unsolved_constraints/1 + , create_constraints/0 + , add_is_contract_constraint/2 + , add_is_contract_constraint/3 + , add_is_bytes_constraint/1 + , add_add_bytes_constraint/5 + , add_aens_resolve_constraint/1 + , add_oracle_type_constraint/2 + , add_named_argument_constraint/3 + , add_field_constraint/5 + , add_dependent_type_constraint/5 + , add_record_create_constraint/3 + ]). + +%% -- Duplicated types ------------------------------------------------------- + +-type uvar() :: {uvar, aeso_syntax:ann(), reference()}. +-type named_args_t() :: uvar() | [{named_arg_t, aeso_syntax:ann(), aeso_syntax:id(), utype(), aeso_syntax:expr()}]. +-type utype() :: aeso_ast_infer_types:utype(). + +%% -- Duplicated macros ------------------------------------------------------ + +-define(is_type_id(T), element(1, T) =:= id orelse + element(1, T) =:= qid orelse + element(1, T) =:= con orelse + element(1, T) =:= qcon). + +%% -- Circular dependency ---------------------------------------------------- + +fresh_uvar(A) -> aeso_ast_infer_types:fresh_uvar(A). +freshen(A) -> aeso_ast_infer_types:freshen(A). +create_freshen_tvars() -> aeso_ast_infer_types:create_freshen_tvars(). +destroy_freshen_tvars() -> aeso_ast_infer_types:destroy_freshen_tvars(). +unify(A, B, C, D) -> aeso_ast_infer_types:unify(A, B, C, D). +unfold_types_in_type(A, B) -> aeso_ast_infer_types:unfold_types_in_type(A, B). +app_t(A, B, C) -> aeso_ast_infer_types:app_t(A, B, C). + +%% -- Moved functions -------------------------------------------------------- + +qname(A) -> aeso_tc_name_manip:qname(A). + +%% ------- + +type_error(A) -> aeso_tc_errors:type_error(A). + +%% ------- + +ensure_monomorphic(A, B) -> aeso_tc_type_utils:ensure_monomorphic(A, B). +ensure_first_order(A, B) -> aeso_tc_type_utils:ensure_first_order(A, B). + +%% --------------------------------------------------------------------------- + +-type env() :: aeso_tc_env:env(). + +-type why_record() :: aeso_syntax:field(aeso_syntax:expr()) + | {var_args, aeso_syntax:ann(), aeso_syntax:expr()} + | {proj, aeso_syntax:ann(), aeso_syntax:expr(), aeso_syntax:id()}. + +-record(named_argument_constraint, + {args :: named_args_t(), + name :: aeso_syntax:id(), + type :: utype()}). + +-record(dependent_type_constraint, + { named_args_t :: named_args_t() + , named_args :: [aeso_syntax:arg_expr()] + , general_type :: utype() + , specialized_type :: utype() + , context :: term() }). + +-type named_argument_constraint() :: #named_argument_constraint{} | #dependent_type_constraint{}. + +-record(field_constraint, + { record_t :: utype() + , field :: aeso_syntax:id() + , field_t :: utype() + , kind :: project | create | update %% Projection constraints can match contract + , context :: why_record() }). %% types, but field constraints only record types. + +%% Constraint checking that 'record_t' has precisely 'fields'. +-record(record_create_constraint, + { record_t :: utype() + , fields :: [aeso_syntax:id()] + , context :: why_record() }). + +-record(is_contract_constraint, + { contract_t :: utype(), + context :: {contract_literal, aeso_syntax:expr()} | + {address_to_contract, aeso_syntax:ann()} | + {bytecode_hash, aeso_syntax:ann()} | + {var_args, aeso_syntax:ann(), aeso_syntax:expr()}, + force_def = false :: boolean() + }). + +-type field_constraint() :: #field_constraint{} | #record_create_constraint{} | #is_contract_constraint{}. + +-type byte_constraint() :: {is_bytes, utype()} + | {add_bytes, aeso_syntax:ann(), concat | split, utype(), utype(), utype()}. + +-type aens_resolve_constraint() :: {aens_resolve_type, utype()}. +-type oracle_type_constraint() :: {oracle_type, aeso_syntax:ann(), utype()}. + +-type constraint() :: named_argument_constraint() | field_constraint() | byte_constraint() + | aens_resolve_constraint() | oracle_type_constraint(). + +-spec add_constraint(constraint()) -> true. +add_constraint(Constraint) -> + aeso_tc_ets_manager:ets_insert_ordered(constraints, Constraint). + +add_is_contract_constraint(ContractT, Context) -> + add_constraint( + #is_contract_constraint{ + contract_t = ContractT, + context = Context }). + +add_is_contract_constraint(ContractT, Context, ForceDef) -> + add_constraint( + #is_contract_constraint{ + contract_t = ContractT, + context = Context, + force_def = ForceDef }). + +add_aens_resolve_constraint(Type) -> + add_constraint({aens_resolve_type, Type}). + +add_oracle_type_constraint(Ann, Type) -> + add_constraint({oracle_type, Ann, Type}). + +add_named_argument_constraint(Args, Name, Type) -> + add_constraint( + #named_argument_constraint{ + args = Args, + name = Name, + type = Type }). + +add_is_bytes_constraint(Type) -> + add_constraint({is_bytes, Type}). + +add_add_bytes_constraint(Ann, Kind, A, B, C) -> + add_constraint({add_bytes, Ann, Kind, A, B, C}). + +add_field_constraint(RecordT, Field, FieldT, Kind, Context) -> + add_constraint(#field_constraint{ + record_t = RecordT, + field = Field, + field_t = FieldT, + kind = Kind, + context = Context }). + +add_dependent_type_constraint(NamedArgsT, NamedArgs, GeneralType, SpecializedType, Context) -> + add_constraint(#dependent_type_constraint{ + named_args_t = NamedArgsT, + named_args = NamedArgs, + general_type = GeneralType, + specialized_type = SpecializedType, + context = Context }). + +add_record_create_constraint(RecordT, Fields, Context) -> + add_constraint(#record_create_constraint{ + record_t = RecordT, + fields = Fields, + context = Context }). + +create_constraints() -> + aeso_tc_ets_manager:ets_new(constraints, [ordered_set]). + +get_constraints() -> + aeso_tc_ets_manager:ets_tab2list_ordered(constraints). + +destroy_constraints() -> + aeso_tc_ets_manager:ets_delete(constraints). + +-spec solve_constraints(env()) -> ok. +solve_constraints(Env) -> + %% First look for record fields that appear in only one type definition + IsAmbiguous = + fun(#field_constraint{ + record_t = RecordType, + field = Field={id, _Attrs, FieldName}, + field_t = FieldType, + kind = Kind, + context = When }) -> + Arity = aeso_tc_type_utils:fun_arity(aeso_tc_type_utils:dereference_deep(FieldType)), + FieldInfos = case Arity of + none -> aeso_tc_env:lookup_record_field(Env, FieldName, Kind); + _ -> aeso_tc_env:lookup_record_field_arity(Env, FieldName, Arity, Kind) + end, + case FieldInfos of + [] -> + type_error({undefined_field, Field}), + false; + [Fld] -> + FldType = aeso_tc_env:field_info_field_t(Fld), + RecType = aeso_tc_env:field_info_record_t(Fld), + create_freshen_tvars(), + FreshFldType = freshen(FldType), + FreshRecType = freshen(RecType), + destroy_freshen_tvars(), + unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}), + unify(Env, FreshRecType, RecordType, {record_constraint, FreshRecType, RecordType, When}), + false; + _ -> + %% ambiguity--need cleverer strategy + true + end; + (_) -> true + end, + AmbiguousConstraints = lists:filter(IsAmbiguous, get_constraints()), + + % The two passes on AmbiguousConstraints are needed + solve_ambiguous_constraints(Env, AmbiguousConstraints ++ AmbiguousConstraints). + +-spec solve_ambiguous_constraints(env(), [constraint()]) -> ok. +solve_ambiguous_constraints(Env, Constraints) -> + Unknown = solve_known_record_types(Env, Constraints), + if Unknown == [] -> ok; + length(Unknown) < length(Constraints) -> + %% progress! Keep trying. + solve_ambiguous_constraints(Env, Unknown); + true -> + case solve_unknown_record_types(Env, Unknown) of + true -> %% Progress! + solve_ambiguous_constraints(Env, Unknown); + _ -> ok %% No progress. Report errors later. + end + end. + +solve_then_destroy_and_report_unsolved_constraints(Env) -> + solve_constraints(Env), + destroy_and_report_unsolved_constraints(Env). + +destroy_and_report_unsolved_constraints(Env) -> + {FieldCs, OtherCs} = + lists:partition(fun(#field_constraint{}) -> true; (_) -> false end, + get_constraints()), + {CreateCs, OtherCs1} = + lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end, + OtherCs), + {ContractCs, OtherCs2} = + lists:partition(fun(#is_contract_constraint{}) -> true; (_) -> false end, OtherCs1), + {NamedArgCs, OtherCs3} = + lists:partition(fun(#dependent_type_constraint{}) -> true; + (#named_argument_constraint{}) -> true; + (_) -> false + end, OtherCs2), + {BytesCs, OtherCs4} = + lists:partition(fun({is_bytes, _}) -> true; + ({add_bytes, _, _, _, _, _}) -> true; + (_) -> false + end, OtherCs3), + {AensResolveCs, OtherCs5} = + lists:partition(fun({aens_resolve_type, _}) -> true; + (_) -> false + end, OtherCs4), + {OracleTypeCs, []} = + lists:partition(fun({oracle_type, _, _}) -> true; + (_) -> false + end, OtherCs5), + + Unsolved = [ S || S <- [ solve_constraint(Env, aeso_tc_type_utils:dereference_deep(C)) || C <- NamedArgCs ], + S == unsolved ], + [ type_error({unsolved_named_argument_constraint, Name, Type}) + || #named_argument_constraint{name = Name, type = Type} <- Unsolved ], + + Unknown = solve_known_record_types(Env, FieldCs), + if Unknown == [] -> ok; + true -> + case solve_unknown_record_types(Env, Unknown) of + true -> ok; + Errors -> [ type_error(Err) || Err <- Errors ] + end + end, + + check_record_create_constraints(Env, CreateCs), + check_is_contract_constraints(Env, ContractCs), + check_bytes_constraints(Env, BytesCs), + check_aens_resolve_constraints(Env, AensResolveCs), + check_oracle_type_constraints(Env, OracleTypeCs), + + destroy_constraints(). + +%% If false, a type error has been emitted, so it's safe to drop the constraint. +-spec check_named_argument_constraint(env(), named_argument_constraint()) -> true | false | unsolved. +check_named_argument_constraint(_Env, #named_argument_constraint{ args = {uvar, _, _} }) -> + unsolved; +check_named_argument_constraint(Env, + #named_argument_constraint{ args = Args, + name = Id = {id, _, Name}, + type = Type }) -> + case [ T || {named_arg_t, _, {id, _, Name1}, T, _} <- Args, Name1 == Name ] of + [] -> + type_error({bad_named_argument, Args, Id}), + false; + [T] -> unify(Env, T, Type, {check_named_arg_constraint, Args, Id, Type}), true + end; +check_named_argument_constraint(Env, + #dependent_type_constraint{ named_args_t = NamedArgsT0, + named_args = NamedArgs, + general_type = GenType, + specialized_type = SpecType, + context = {check_return, App} }) -> + NamedArgsT = aeso_tc_type_utils:dereference(NamedArgsT0), + case aeso_tc_type_utils:dereference(NamedArgsT0) of + [_ | _] = NamedArgsT -> + GetVal = fun(Name, Default) -> + hd([ Val || {named_arg, _, {id, _, N}, Val} <- NamedArgs, N == Name] ++ + [ Default ]) + end, + ArgEnv = maps:from_list([ {Name, GetVal(Name, Default)} + || {named_arg_t, _, {id, _, Name}, _, Default} <- NamedArgsT ]), + GenType1 = specialize_dependent_type(ArgEnv, GenType), + unify(Env, GenType1, SpecType, {check_expr, App, GenType1, SpecType}), + true; + _ -> unify(Env, GenType, SpecType, {check_expr, App, GenType, SpecType}), true + end. + +specialize_dependent_type(Env, Type) -> + case aeso_tc_type_utils:dereference(Type) of + {if_t, _, {id, _, Arg}, Then, Else} -> + Val = maps:get(Arg, Env), + case Val of + {typed, _, {bool, _, true}, _} -> Then; + {typed, _, {bool, _, false}, _} -> Else; + _ -> + type_error({named_argument_must_be_literal_bool, Arg, Val}), + fresh_uvar(aeso_syntax:get_ann(Val)) + end; + _ -> Type %% Currently no deep dependent types + end. + +%% -- Bytes constraints -- + +solve_constraint(_Env, #field_constraint{record_t = {uvar, _, _}}) -> + not_solved; +solve_constraint(Env, C = #field_constraint{record_t = RecType, + field = FieldName, + field_t = FieldType, + context = When}) -> + RecId = record_type_name(RecType), + Attrs = aeso_syntax:get_ann(RecId), + case aeso_tc_env:lookup_type(Env, RecId) of + {_, {_Ann, {Formals, {What, Fields}}}} when What =:= record_t; What =:= contract_t -> + FieldTypes = [{Name, Type} || {field_t, _, {id, _, Name}, Type} <- Fields], + {id, _, FieldString} = FieldName, + case proplists:get_value(FieldString, FieldTypes) of + undefined -> + type_error({missing_field, FieldName, RecId}), + not_solved; + FldType -> + create_freshen_tvars(), + FreshFldType = freshen(FldType), + FreshRecType = freshen(app_t(Attrs, RecId, Formals)), + destroy_freshen_tvars(), + unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}), + unify(Env, FreshRecType, RecType, {record_constraint, FreshRecType, RecType, When}), + C + end; + _ -> + type_error({not_a_record_type, aeso_tc_type_utils:instantiate(RecType), When}), + not_solved + end; +solve_constraint(Env, C = #dependent_type_constraint{}) -> + check_named_argument_constraint(Env, C); +solve_constraint(Env, C = #named_argument_constraint{}) -> + check_named_argument_constraint(Env, C); +solve_constraint(_Env, {is_bytes, _}) -> ok; +solve_constraint(Env, {add_bytes, Ann, _, A0, B0, C0}) -> + A = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(A0)), + B = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(B0)), + C = unfold_types_in_type(Env, aeso_tc_type_utils:dereference(C0)), + case {A, B, C} of + {{bytes_t, _, M}, {bytes_t, _, N}, _} -> unify(Env, {bytes_t, Ann, M + N}, C, {at, Ann}); + {{bytes_t, _, M}, _, {bytes_t, _, R}} when R >= M -> unify(Env, {bytes_t, Ann, R - M}, B, {at, Ann}); + {_, {bytes_t, _, N}, {bytes_t, _, R}} when R >= N -> unify(Env, {bytes_t, Ann, R - N}, A, {at, Ann}); + _ -> ok + end; +solve_constraint(_, _) -> ok. + +check_bytes_constraints(Env, Constraints) -> + InAddConstraint = [ T || {add_bytes, _, _, A, B, C} <- Constraints, + T <- [A, B, C], + element(1, T) /= bytes_t ], + %% Skip is_bytes constraints for types that occur in add_bytes constraints + %% (no need to generate error messages for both is_bytes and add_bytes). + Skip = fun({is_bytes, T}) -> lists:member(T, InAddConstraint); + (_) -> false end, + [ check_bytes_constraint(Env, C) || C <- Constraints, not Skip(C) ]. + +check_bytes_constraint(Env, {is_bytes, Type}) -> + Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)), + case Type1 of + {bytes_t, _, _} -> ok; + _ -> + type_error({unknown_byte_length, Type}) + end; +check_bytes_constraint(Env, {add_bytes, Ann, Fun, A0, B0, C0}) -> + A = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(A0)), + B = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(B0)), + C = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(C0)), + case {A, B, C} of + {{bytes_t, _, _M}, {bytes_t, _, _N}, {bytes_t, _, _R}} -> + ok; %% If all are solved we checked M + N == R in solve_constraint. + _ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C}) + end. + +check_aens_resolve_constraints(_Env, []) -> + ok; +check_aens_resolve_constraints(Env, [{aens_resolve_type, Type} | Rest]) -> + Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)), + {app_t, _, {id, _, "option"}, [Type2]} = Type1, + case Type2 of + {id, _, "string"} -> ok; + {id, _, "address"} -> ok; + {con, _, _} -> ok; + {app_t, _, {id, _, "oracle"}, [_, _]} -> ok; + {app_t, _, {id, _, "oracle_query"}, [_, _]} -> ok; + _ -> type_error({invalid_aens_resolve_type, aeso_syntax:get_ann(Type), Type2}) + end, + check_aens_resolve_constraints(Env, Rest). + +check_oracle_type_constraints(_Env, []) -> + ok; +check_oracle_type_constraints(Env, [{oracle_type, Ann, OType} | Rest]) -> + Type = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(OType)), + {app_t, _, {id, _, "oracle"}, [QType, RType]} = Type, + ensure_monomorphic(QType, {invalid_oracle_type, polymorphic, query, Ann, Type}), + ensure_monomorphic(RType, {invalid_oracle_type, polymorphic, response, Ann, Type}), + ensure_first_order(QType, {invalid_oracle_type, higher_order, query, Ann, Type}), + ensure_first_order(RType, {invalid_oracle_type, higher_order, response, Ann, Type}), + check_oracle_type_constraints(Env, Rest). + +%% -- Field constraints -- + +check_record_create_constraints(_, []) -> ok; +check_record_create_constraints(Env, [C | Cs]) -> + #record_create_constraint{ + record_t = Type, + fields = Fields, + context = When } = C, + Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)), + try aeso_tc_env:lookup_type(Env, record_type_name(Type1)) of + {_QId, {_Ann, {_Args, {record_t, RecFields}}}} -> + ActualNames = [ Fld || {field_t, _, {id, _, Fld}, _} <- RecFields ], + GivenNames = [ Fld || {id, _, Fld} <- Fields ], + case ActualNames -- GivenNames of %% We know already that we don't have too many fields + [] -> ok; + Missing -> type_error({missing_fields, When, Type1, Missing}) + end; + _ -> %% We can get here if there are other type errors. + ok + catch _:_ -> %% Might be unsolved, we get a different error in that case + ok + end, + check_record_create_constraints(Env, Cs). + +is_contract_defined(C) -> + aeso_tc_ets_manager:ets_lookup(defined_contracts, qname(C)) =/= []. + +check_is_contract_constraints(_Env, []) -> ok; +check_is_contract_constraints(Env, [C | Cs]) -> + #is_contract_constraint{ contract_t = Type, context = Cxt, force_def = ForceDef } = C, + Type1 = unfold_types_in_type(Env, aeso_tc_type_utils:instantiate(Type)), + TypeName = record_type_name(Type1), + case aeso_tc_env:lookup_type(Env, TypeName) of + {_, {_Ann, {[], {contract_t, _}}}} -> + case not ForceDef orelse is_contract_defined(TypeName) of + true -> ok; + false -> type_error({contract_lacks_definition, Type1, Cxt}) + end; + _ -> type_error({not_a_contract_type, Type1, Cxt}) + end, + check_is_contract_constraints(Env, Cs). + +-spec solve_unknown_record_types(env(), [field_constraint()]) -> true | [tuple()]. +solve_unknown_record_types(Env, Unknown) -> + UVars = lists:usort([UVar || #field_constraint{record_t = UVar = {uvar, _, _}} <- Unknown]), + Solutions = [solve_for_uvar(Env, UVar, [{Kind, When, Field} + || #field_constraint{record_t = U, field = Field, kind = Kind, context = When} <- Unknown, + U == UVar]) + || UVar <- UVars], + case lists:member(true, Solutions) of + true -> true; + false -> Solutions + end. + +%% This will solve all kinds of constraints but will only return the +%% unsolved field constraints +-spec solve_known_record_types(env(), [constraint()]) -> [field_constraint()]. +solve_known_record_types(Env, Constraints) -> + DerefConstraints = lists:map(fun(C = #field_constraint{record_t = RecordType}) -> + C#field_constraint{record_t = aeso_tc_type_utils:dereference(RecordType)}; + (C) -> aeso_tc_type_utils:dereference_deep(C) + end, Constraints), + SolvedConstraints = lists:map(fun(C) -> solve_constraint(Env, aeso_tc_type_utils:dereference_deep(C)) end, DerefConstraints), + Unsolved = DerefConstraints--SolvedConstraints, + lists:filter(fun(#field_constraint{}) -> true; (_) -> false end, Unsolved). + +record_type_name({app_t, _Attrs, RecId, _Args}) when ?is_type_id(RecId) -> + RecId; +record_type_name(RecId) when ?is_type_id(RecId) -> + RecId; +record_type_name(_Other) -> + %% io:format("~p is not a record type\n", [Other]), + {id, [{origin, system}], "not_a_record_type"}. + +solve_for_uvar(Env, UVar = {uvar, Attrs, _}, Fields0) -> + Fields = [{Kind, Fld} || {Kind, _, Fld} <- Fields0], + [{_, When, _} | _] = Fields0, %% Get the location from the first field + %% If we have 'create' constraints they must be complete. + Covering = lists:usort([ Name || {create, {id, _, Name}} <- Fields ]), + %% Does this set of fields uniquely identify a record type? + FieldNames = [ Name || {_Kind, {id, _, Name}} <- Fields ], + UniqueFields = lists:usort(FieldNames), + Candidates = [aeso_tc_env:field_info_record_t(Fld) || Fld <- aeso_tc_env:lookup_record_field(Env, hd(FieldNames))], + TypesAndFields = [case aeso_tc_env:lookup_type(Env, record_type_name(RecType)) of + {_, {_, {_, {record_t, RecFields}}}} -> + {RecType, [Field || {field_t, _, {id, _, Field}, _} <- RecFields]}; + {_, {_, {_, {contract_t, ConFields}}}} -> + %% TODO: is this right? + {RecType, [Field || {field_t, _, {id, _, Field}, _} <- ConFields]}; + false -> %% impossible? + error({no_definition_for, record_type_name(RecType), in, Env}) + end + || RecType <- Candidates], + PartialSolutions = + lists:sort([{RecType, if Covering == [] -> []; true -> RecFields -- Covering end} + || {RecType, RecFields} <- TypesAndFields, + UniqueFields -- RecFields == []]), + Solutions = [RecName || {RecName, []} <- PartialSolutions], + case {Solutions, PartialSolutions} of + {[], []} -> + {no_records_with_all_fields, Fields}; + {[], _} -> + case PartialSolutions of + [{RecType, Missing} | _] -> %% TODO: better error if ambiguous + {missing_fields, When, RecType, Missing} + end; + {[RecType], _} -> + RecName = record_type_name(RecType), + {_, {_, {Formals, {_RecOrCon, _}}}} = aeso_tc_env:lookup_type(Env, RecName), + create_freshen_tvars(), + FreshRecType = freshen(app_t(Attrs, RecName, Formals)), + destroy_freshen_tvars(), + unify(Env, UVar, FreshRecType, {solve_rec_type, UVar, Fields}), + true; + {StillPossible, _} -> + {ambiguous_record, Fields, StillPossible} + end. diff --git a/src/aeso_tc_errors.erl b/src/aeso_tc_errors.erl index a73b439..67453dc 100644 --- a/src/aeso_tc_errors.erl +++ b/src/aeso_tc_errors.erl @@ -210,9 +210,7 @@ mk_error({bad_named_argument, Args, Name}) -> [ io_lib:format("\n - `~s`", [pp_typed("", Arg, Type)]) || {named_arg_t, _, Arg, Type, _} <- Args ]]), mk_t_err(pos(Name), Msg); -mk_error({unsolved_named_argument_constraint, C}) -> - Name = aeso_ast_infer_types:get_named_argument_constraint_name(C), - Type = aeso_ast_infer_types:get_named_argument_constraint_type(C), +mk_error({unsolved_named_argument_constraint, Name, Type}) -> Msg = io_lib:format("Named argument ~s supplied to function with unknown named arguments.", [pp_typed("", Name, Type)]), mk_t_err(pos(Name), Msg); diff --git a/src/aeso_tc_pp.erl b/src/aeso_tc_pp.erl index 80241b1..43075fa 100644 --- a/src/aeso_tc_pp.erl +++ b/src/aeso_tc_pp.erl @@ -131,11 +131,11 @@ pp_when({list_comp, BindExpr, Inferred0, Expected0}) -> {pos(BindExpr), io_lib:format("when checking rvalue of list comprehension binding `~s` against type `~s`", [pp_typed("", BindExpr, Inferred), pp_type(Expected)])}; -pp_when({check_named_arg_constraint, C}) -> - {id, _, Name} = Arg = aeso_ast_infer_types:get_named_argument_constraint_name(C), - [Type | _] = [ Type || {named_arg_t, _, {id, _, Name1}, Type, _} <- aeso_ast_infer_types:get_named_argument_constraint_args(C), Name1 == Name ], +pp_when({check_named_arg_constraint, CArgs, CName, CType}) -> + {id, _, Name} = Arg = CName, + [Type | _] = [ Type || {named_arg_t, _, {id, _, Name1}, Type, _} <- CArgs, Name1 == Name ], Err = io_lib:format("when checking named argument `~s` against inferred type `~s`", - [pp_typed("", Arg, Type), pp_type(aeso_ast_infer_types:get_named_argument_constraint_type(C))]), + [pp_typed("", Arg, Type), pp_type(CType)]), {pos(Arg), Err}; pp_when({checking_init_args, Ann, Con0, ArgTypes0}) -> Con = aeso_tc_type_utils:instantiate(Con0), diff --git a/src/aeso_tc_type_utils.erl b/src/aeso_tc_type_utils.erl index 70ee177..fbbaa60 100644 --- a/src/aeso_tc_type_utils.erl +++ b/src/aeso_tc_type_utils.erl @@ -5,6 +5,8 @@ , instantiate/1 , typesig_to_fun_t/1 , fun_arity/1 + , ensure_first_order/2 + , ensure_monomorphic/2 ]). typesig_to_fun_t({type_sig, Ann, _Constr, Named, Args, Res}) -> @@ -62,3 +64,19 @@ integer_to_tvar(X) -> fun_arity({fun_t, _, _, Args, _}) -> length(Args); fun_arity(_) -> none. + +ensure_monomorphic(Type, Err) -> + is_monomorphic(Type) orelse aeso_tc_errors:type_error(Err). + +is_monomorphic({tvar, _, _}) -> false; +is_monomorphic(Ts) when is_list(Ts) -> lists:all(fun is_monomorphic/1, Ts); +is_monomorphic(Tup) when is_tuple(Tup) -> is_monomorphic(tuple_to_list(Tup)); +is_monomorphic(_) -> true. + +ensure_first_order(Type, Err) -> + is_first_order(Type) orelse aeso_tc_errors:type_error(Err). + +is_first_order({fun_t, _, _, _, _}) -> false; +is_first_order(Ts) when is_list(Ts) -> lists:all(fun is_first_order/1, Ts); +is_first_order(Tup) when is_tuple(Tup) -> is_first_order(tuple_to_list(Tup)); +is_first_order(_) -> true.