diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index a0c508a..2d65e2f 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -1859,7 +1859,7 @@ infer_op(Env, As, Op, Args, InferOp) -> TypedArgs = [infer_expr(Env, A) || A <- Args], ArgTypes = [T || {typed, _, _, T} <- TypedArgs], Inferred = {fun_t, _, _, OperandTypes, ResultType} = InferOp(Op), - unify(Env, ArgTypes, OperandTypes, {infer_app, Op, [], Inferred, ArgTypes}), + unify(Env, ArgTypes, OperandTypes, {infer_app, Op, [], Args, Inferred, ArgTypes}), {typed, As, {app, As, {typed, As, Op, Inferred}, TypedArgs}, ResultType}. infer_pattern(Env, Pattern) -> diff --git a/src/aeso_ast_refine_types.erl b/src/aeso_ast_refine_types.erl index 953cd20..7bf3262 100644 --- a/src/aeso_ast_refine_types.erl +++ b/src/aeso_ast_refine_types.erl @@ -995,9 +995,9 @@ refine_ast(TCEnv, AST) -> Env5 = register_ast_funs(AST, Env4), {AST1, CS0} = constr_ast(Env5, AST), CS1 = split_constr(CS0), - [ ?DBG("SUBTYPE ~p:\n~s\n<:\n~s", [Id, aeso_pretty:pp(type, strip_typed(T1)), aeso_pretty:pp(type, strip_typed(T2))]) - || {subtype, Id, _, _, T1, T2} <- CS1 - ], + %[ ?DBG("SUBTYPE ~p:\n~s\n<:\n~s", [Id, aeso_pretty:pp(type, strip_typed(T1)), aeso_pretty:pp(type, strip_typed(T2))]) + % || {subtype, Id, _, _, T1, T2} <- CS1 + %], {Env5, solve(Env5, AST1, CS1)} of {EnvErlangSucks, {ok, AST2}} -> {ok, {EnvErlangSucks, AST2}}; @@ -1075,10 +1075,8 @@ constr_letfun(Env0, {letfun, Ann, Id, Args, RetT, Body}, S0) -> end end, Body3 = a_normalize(Body2), - ?DBG("ANORM\n~s", [aeso_pretty:pp(expr, Body1)]), - ?DBG("PURI\n~s", [aeso_pretty:pp(expr, Body2)]), - ?DBG("PURIFIED\n~s", [aeso_pretty:pp(expr, Body3)]), - ?DBG("PURIFIED\n~p", [Body3]), + %?DBG("ANORM\n~s", [aeso_pretty:pp(expr, Body1)]), + %?DBG("PURIFIED\n~s", [aeso_pretty:pp(expr, Body3)]), {BodyT, S1} = constr_expr(Env3, Body3, S0), InnerFunT = {dep_fun_t, Ann, ArgsT, BodyT}, S3 = [ {subtype, constr_id(letfun_top_decl), Ann, Env3, BodyT, GlobRetT} @@ -1152,7 +1150,6 @@ constr_expr(Env, ?typed_p(Expr, Type), S0) -> %% Nothing interesting constr_expr(Env, Expr, Type, S0); true -> - ?DBG("TYPING CAUSE\n~p", [Type]), DType = fresh_liquid(Env, "typed", Type), {ExprT, S1} = constr_expr(Env, Expr, Base, S0), {ExprT, @@ -1403,11 +1400,9 @@ constr_expr(Env, {app, Ann, F = ?typed_p(_, {fun_t, _, NamedT, _, _}), Args0}, _ || {named_arg_t, _, TArgName, _, TArgDefault} <- NamedT ] ++ (Args0 -- NamedArgs), {_FDT = {dep_fun_t, _, ArgsFT, RetT}, S1} = constr_expr(Env, F, S0), - ?DBG("APP OF\n~s", [aeso_pretty:pp(type, _FDT)]), {ArgsT, S2} = constr_expr_list(Env, Args, S1), ArgSubst = [{X, Expr} || {{dep_arg_t, _, X, _}, Expr} <- lists:zip(ArgsFT, Args)], RetT1 = apply_subst(ArgSubst, RetT), - ?DBG("SUBST:\n~s\n->\n~s", [aeso_pretty:pp(type, RetT), aeso_pretty:pp(type, RetT1)]), { RetT1 , [{subtype, constr_id(app), [{context, {app, Ann, F, N}}|?ann_of(ArgT)], Env, ArgT, ArgFT} @@ -1791,7 +1786,6 @@ inst_pred(Env, SelfId, {refined_t, _, _, BaseT, _}) -> inst_pred(Env = #env{tc_env = TCEnv}, SelfId, BaseT) -> case BaseT of ?int_tp -> - %% ?DBG("INST PRED FOR ~s\n~s", [name(SelfId), aeso_pretty:pp(predicate, inst_pred_int(Env, SelfId))]), inst_pred_int(Env, SelfId); ?bool_tp -> inst_pred_bool(Env, SelfId); @@ -2125,9 +2119,9 @@ valid_in({subtype, _Ref, Ann, Env, true -> true; false -> - ?DBG("~s -> ~s", [name(SupId), name(SubId)]), - ?DBG("CONTRADICT ON ~p \n~s\n<:\n~s", [_Ref, aeso_pretty:pp(predicate, strip_typed(pred_of(Assg, Env) ++ AssumpPred)), aeso_pretty:pp(predicate, strip_typed(ConclPred))]), - ?DBG("IN\n~s", [aeso_pretty:pp(predicate, strip_typed(pred_of(Assg, Env1)))]), + %?DBG("~s -> ~s", [name(SupId), name(SubId)]), + %?DBG("CONTRADICT ON ~p \n~s\n<:\n~s", [_Ref, aeso_pretty:pp(predicate, strip_typed(pred_of(Assg, Env) ++ AssumpPred)), aeso_pretty:pp(predicate, strip_typed(ConclPred))]), + %?DBG("IN\n~s", [aeso_pretty:pp(predicate, strip_typed(pred_of(Assg, Env1)))]), SimpAssump = simplify_pred(Assg, Env1, pred_of(Assg, Env1) ++ AssumpPred), add_error({contradict, {Ann, strip_typed(SimpAssump), strip_typed(ConclPred)}}) @@ -2812,7 +2806,6 @@ purify_typed(impure, E, T, ST) -> {impure, ?typed(E, wrap_state_t(purify_type(T, ST), ST))}. purify_expr(?typed_p(E, T), T1, ST) -> - ?DBG("PURI PYK\n~p\n~p",[T, T1]), {Pure, E1} = purify_expr(E, T, ST), purify_typed(Pure, E1, T1, ST); diff --git a/src/aeso_ast_to_fcode.erl b/src/aeso_ast_to_fcode.erl index 4fc952e..f6de0de 100644 --- a/src/aeso_ast_to_fcode.erl +++ b/src/aeso_ast_to_fcode.erl @@ -12,6 +12,7 @@ -export([ast_to_fcode/2, format_fexpr/1]). -export_type([fcode/0, fexpr/0, fun_def/0]). +-include_lib("eunit/include/eunit.hrl"). -include("aeso_utils.hrl"). %% -- Type definitions ------------------------------------------------------- @@ -540,6 +541,10 @@ expr_to_fcode(Env, Expr) -> -spec expr_to_fcode(env(), aeso_syntax:type() | no_type, aeso_syntax:expr()) -> fexpr(). +% Untype op +expr_to_fcode(Env, Type, {app, Ann, {typed, _, {Op, OpAnn}, _}, Args}) when is_atom(Op) -> + expr_to_fcode(Env, Type, {app, Ann, {Op, OpAnn}, Args}); + %% Literals expr_to_fcode(_Env, _Type, {int, _, N}) -> {lit, {int, N}}; expr_to_fcode(_Env, _Type, {char, _, N}) -> {lit, {int, N}}; @@ -684,29 +689,32 @@ expr_to_fcode(Env, _Type, {'if', _, Cond, Then, Else}) -> %% Switch expr_to_fcode(Env, _, {switch, _, Expr = {typed, _, E, Type}, Alts}) -> Switch = fun(X) -> - {switch, alts_to_fcode(Env, type_to_fcode(Env, Type), X, Alts)} + T = type_to_fcode(Env, Type), + Rx = {switch, alts_to_fcode(Env, T, X, Alts)}, + Rx end, - case E of + R = case E of {id, _, X} -> Switch(X); _ -> X = fresh_name(), {'let', X, expr_to_fcode(Env, Expr), Switch(X)} - end; + end, + R; %% Blocks expr_to_fcode(Env, _Type, {block, _, Stmts}) -> stmts_to_fcode(Env, Stmts); %% Binary operator -expr_to_fcode(Env, _Type, Expr = {app, _, {typed, _, {Op, _}, _}, [_, _]}) +expr_to_fcode(Env, _Type, Expr = {app, _, {Op, _}, [_, _]}) when Op == '&&'; Op == '||' -> Tree = expr_to_decision_tree(Env, Expr), decision_tree_to_fcode(Tree); -expr_to_fcode(Env, _Type, {app, _Ann, {typed, _, {Op, _}, _}, [A, B]}) +expr_to_fcode(Env, _Type, {app, _Ann, {Op, _}, [A, B]}) when is_atom(Op) -> {op, Op, [expr_to_fcode(Env, A), expr_to_fcode(Env, B)]}; -expr_to_fcode(Env, _Type, {app, _Ann, {typed, _, {Op, _}, _}, [A]}) +expr_to_fcode(Env, _Type, {app, _Ann, {Op, _}, [A]}) when is_atom(Op) -> case Op of '-' -> {op, '-', [{lit, {int, 0}}, expr_to_fcode(Env, A)]}; @@ -1032,7 +1040,7 @@ pat_to_fcode(Env, _Type, {list, _, Ps}) -> lists:foldr(fun(P, Qs) -> {'::', pat_to_fcode(Env, P), Qs} end, nil, Ps); -pat_to_fcode(Env, _Type, {app, _, {'::', _}, [P, Q]}) -> +pat_to_fcode(Env, _Type, {app, _, {typed, _, {'::', _}, _}, [P, Q]}) -> {'::', pat_to_fcode(Env, P), pat_to_fcode(Env, Q)}; pat_to_fcode(Env, {record_t, Fields}, {record, _, FieldPats}) -> FieldPat = fun(F) -> diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index bb4695e..dfea017 100644 --- a/test/aeso_compiler_tests.erl +++ b/test/aeso_compiler_tests.erl @@ -23,7 +23,6 @@ run_test(Test) -> %% Very simply test compile the given contracts. Only basic checks %% are made on the output, just that it is a binary which indicates %% that the compilation worked. -simple_compile_test_() -> []; simple_compile_test_() -> [ {"Testing the " ++ ContractName ++ " contract with the " ++ atom_to_list(Backend) ++ " backend", fun() -> @@ -95,17 +94,19 @@ simple_compile_test_() -> stdlib_test_() -> {ok, Files} = file:list_dir(aeso_stdlib:stdlib_include_path()), [ { "Testing " ++ File ++ " from the stdlib", - fun() -> - String = "include \"" ++ File ++ "\"\nmain contract Test =\n entrypoint f(x) = x", - Options = [{src_file, File}, {backend, fate}], - case aeso_compiler:from_string(String, Options) of - {ok, #{fate_code := Code}} -> - Code1 = aeb_fate_code:deserialize(aeb_fate_code:serialize(Code)), - ?assertMatch({X, X}, {Code1, Code}); - {error, Error} -> io:format("\n\n~p\n\n", [Error]), print_and_throw(Error) - end - end} || File <- Files, - lists:suffix(".aes", File) + {timeout, 10, + fun() -> + String = "include \"" ++ File ++ "\"\nmain contract Test =\n entrypoint f(x) = x", + Options = [{src_file, File}, {backend, fate}], + case aeso_compiler:from_string(String, Options) of + {ok, #{fate_code := Code}} -> + Code1 = aeb_fate_code:deserialize(aeb_fate_code:serialize(Code)), + ?assertMatch({X, X}, {Code1, Code}); + {error, Error} -> io:format("\n\n~p\n\n", [Error]), print_and_throw(Error) + end + end}} + || File <- Files, + lists:suffix(".aes", File) ]. check_errors(no_error, Actual) -> ?assertMatch(#{}, Actual); @@ -142,7 +143,6 @@ compile(Backend, Name, Options) -> %% compilable_contracts() -> [ContractName]. %% The currently compilable contracts. -compilable_contracts() -> ["hagia"]; compilable_contracts() -> ["complex_types", "counter", @@ -224,7 +224,6 @@ debug_mode_contracts() -> -define(TYPE_ERROR(Name, Errs), ?ERROR("Type", Name, Errs)). -define(PARSE_ERROR(Name, Errs), ?ERROR("Parse", Name, Errs)). -failing_contracts() -> []; failing_contracts() -> {ok, V} = aeso_compiler:numeric_version(), Version = list_to_binary(string:join([integer_to_list(N) || N <- V], ".")), @@ -910,7 +909,6 @@ validation_test_() -> ?assertEqual(ok, validate(C, C)) end} || C <- compilable_contracts()]. -validation_fails() -> []; validation_fails() -> [{"deadcode", "nodeadcode", [<<"Data error:\n" diff --git a/test/aeso_type_refinement_tests.erl b/test/aeso_type_refinement_tests.erl index d7fb46b..72939c5 100644 --- a/test/aeso_type_refinement_tests.erl +++ b/test/aeso_type_refinement_tests.erl @@ -29,6 +29,7 @@ unsetup(_) -> ok. hagia_test_() -> + ?IF(os:find_executable("z3") == false, [], % This turns off hagia tests on machines that don't have Z3 {timeout, 100000000, {inorder, {foreach, local, fun setup/0, fun unsetup/1, @@ -36,7 +37,7 @@ hagia_test_() -> , {timeout, 1000000, refiner_test_group()} ] } - }}. + }}). smt_solver_test_group() -> [ { "x == x"