QPQ-AG/sophia
10
0
Fork 0
Code Issues 41 Pull Requests 5 Actions Packages Projects Releases 16 Wiki Activity

fix tests

Browse Source
This commit is contained in:
radrow 2021-08-03 11:39:16 +02:00
parent 7ba49c549d
commit ced9b2b2de
5 changed files with 39 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aeso_ast_infer_types.erl
View File

@ -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) ->

23
src/aeso_ast_refine_types.erl
View File

@ -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);

22
src/aeso_ast_to_fcode.erl
View File

@ -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) ->

28
test/aeso_compiler_tests.erl
View File

@ -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"

3
test/aeso_type_refinement_tests.erl
View File

@ -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"