Liquid types

rebar.config

@@ -5,6 +5,7 @@
 {deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"05dfd7f"}}}
        , {getopt, "1.0.1"}
        , {eblake2, "1.0.0"}
+       , {meck, "0.9.2"}
        , {jsx, {git, "https://github.com/talentdeficit/jsx.git",
                      {tag, "2.8.0"}}}
        ]}.

rebar.lock

@@ -12,17 +12,25 @@
        {ref,"60a335668a60328a29f9731b67c4a0e9e3d50ab6"}},
   2},
  {<<"eblake2">>,{pkg,<<"eblake2">>,<<"1.0.0">>},0},
+ {<<"effi">>,
+  {git,"https://github.com/joergen7/effi",
+       {ref,"aac0d5716c322200dd1145cf6bb651f79834bfd5"}},
+  0},
  {<<"enacl">>,
   {git,"https://github.com/aeternity/enacl.git",
        {ref,"26180f42c0b3a450905d2efd8bc7fd5fd9cece75"}},
   2},
  {<<"getopt">>,{pkg,<<"getopt">>,<<"1.0.1">>},0},
+ {<<"jsone">>,{pkg,<<"jsone">>,<<"1.4.7">>},1},
  {<<"jsx">>,
   {git,"https://github.com/talentdeficit/jsx.git",
        {ref,"3074d4865b3385a050badf7828ad31490d860df5"}},
-  0}]}.
+  0},
+ {<<"meck">>,{pkg,<<"meck">>,<<"0.8.12">>},0}]}.
 [
 {pkg_hash,[
  {<<"eblake2">>, <<"EC8AD20E438AAB3F2E8D5D118C366A0754219195F8A0F536587440F8F9BCF2EF">>},
- {<<"getopt">>, <<"C73A9FA687B217F2FF79F68A3B637711BB1936E712B521D8CE466B29CBF7808A">>}]}
+ {<<"getopt">>, <<"C73A9FA687B217F2FF79F68A3B637711BB1936E712B521D8CE466B29CBF7808A">>},
+ {<<"jsone">>, <<"A970C23D9700AE7842B526C57677E6E3F10894B429524696EAD547E9302391C0">>},
+ {<<"meck">>, <<"1F7B1A9F5D12C511848FEC26BBEFD09A21E1432EADB8982D9A8ACEB9891A3CF2">>}]}
 ].

src/aeso_aci.erl

@@ -165,7 +165,9 @@ encode_type({constr_t, _, C, As}) -> #{encode_type(C) => encode_types(As)};
 encode_type({alias_t, Type})      -> encode_type(Type);
 encode_type({fun_t, _, _, As, T}) -> #{function =>
                                          #{arguments => encode_types(As),
-                                           returns => encode_type(T)}}.
+                                           returns => encode_type(T)}};
+encode_type({named_t, _, _, T}) -> encode_type(T);
+encode_type({liquid, _, T, _}) -> encode_type(T).
 
 encode_types(Ts) -> [ encode_type(T) || T <- Ts ].
 

src/aeso_ast_infer_types.erl

@@ -16,6 +16,8 @@
         , infer/2
         , unfold_types_in_type/3
         , pp_type/2
+        , init_env/1
+        , lookup_env/4
         ]).
 
 -include("aeso_utils.hrl").
@@ -130,9 +132,11 @@
     , stateful   = false              :: boolean()
     , current_function = none         :: none | aeso_syntax:id()
     , what       = top                :: top | namespace | contract | contract_interface
+    , allow_liquid = true             :: boolean()
     }).
 
 -type env() :: #env{}.
+-export_type([env/0]).
 
 -define(PRINT_TYPES(Fmt, Args),
         when_option(pp_types, fun () -> io:format(Fmt, Args) end)).
@@ -1094,11 +1098,126 @@ check_type(Env, Type = {fun_t, Ann, NamedArgs, Args, Ret}, Arity) ->
     ensure_base_type(Type, Arity),
     NamedArgs1 = [ check_named_arg(Env, NamedArg) || NamedArg <- NamedArgs ],
     Args1      = [ check_type(Env, Arg, 0) || Arg <- Args ],
-    Ret1       = check_type(Env, Ret, 0),
+    NamedTArgs = [{Var, T} || {refined_t, _, Var, T, _} <- Args1]
+        ++ [{Var, {id, [], "int"}} || {dep_list_t, _, Var, _, _} <- Args1],
+    Env1       = bind_vars(NamedTArgs, Env),
+    Ret1       = check_type(Env1, Ret, 0),
     {fun_t, Ann, NamedArgs1, Args1, Ret1};
 check_type(_Env, Type = {uvar, _, _}, Arity) ->
     ensure_base_type(Type, Arity),
     Type;
+check_type(Env, T = {refined_t, Ann, Id, Base, Pred}, Arity) ->
+    [type_error({illegal_liquid, T}) || not Env#env.allow_liquid],
+    ensure_base_type(Base, Arity),
+    Env1 = Env#env{allow_liquid = false},
+    Base1 = check_type(Env1, Base, Arity),
+    Env2 = bind_var(Id, Base, Env1),
+    Pred1 = [check_expr(Env2, Q, {id, aeso_syntax:get_ann(Q), "bool"}) || Q <- Pred],
+    {refined_t, Ann, Id, Base1, Pred1};
+check_type(Env, T = {dep_record_t, Ann, Base, Fields}, Arity) ->
+    ensure_base_type(T, Arity),
+    [type_error({illegal_liquid, T}) || not Env#env.allow_liquid],
+    Base1 = check_type(Env, Base, Arity),
+    Id = case Base1 of
+             {app_t, _, I, _} -> I;
+             _ -> Base1
+         end,
+    %% TODO Validate fields in record
+    {QId, TrueFields} =
+        case lookup_type(Env, Id) of
+            {QName, {QAnn, {_, {record_t, F}}}} -> {qid(QAnn, QName), F};
+            _ -> type_error({not_a_record_type, Id, T}),
+                 {Id, []}
+        end,
+    Fields1 =
+        [ case [ FieldNew
+                 || FieldNew = {field_t, _, FNameNew, _} <- Fields,
+                    name(FNameNew) == name(FNameOld)] of
+              [{field_t, FAnn, FName, FType}] ->
+                  {field_t, FAnn, FName, check_type(Env, FType)};
+              _ -> FieldOld
+          end
+         || FieldOld = {field_t, _, FNameOld, _} <- TrueFields
+        ],
+    constrain(
+      [ #field_constraint{
+           record_t = QId,
+           field    = FName,
+           field_t  = FType,
+           kind     = project,
+           context  = {proj, Ann, QId, FName} }
+        || {field_t, _, FName, FType} <- Fields
+      ]),
+    {dep_record_t, Ann, QId, Fields1};
+check_type(Env, T = {dep_variant_t, Ann, TId, Base, undefined, Constrs}, Arity) ->
+    ensure_base_type(T, Arity),
+    [type_error({illegal_liquid, T}) || not Env#env.allow_liquid],
+    Base1 = check_type(Env, Base, Arity),
+    Id = case Base1 of
+             {app_t, _, I, _} -> I;
+             _ -> Base1
+         end,
+    Args = case Base1 of
+             {app_t, _, _, A} -> A;
+             _ -> []
+         end,
+    {QId, TrueConstrs} =
+        case lookup_type(Env, Id) of
+            {Q, {QAnn, {_, {variant_t, Cs}}}} -> {{qid, QAnn, Q}, Cs};
+            {["option"], {QAnn, {builtin, _}}} ->
+                {{qid, QAnn, ["option"]},
+                 [ {constr_t, QAnn, {con, QAnn, "None"}, []}
+                 , {constr_t, QAnn, {con, QAnn, "Some"}, Args}
+                 ]
+                }; %% TODO other types
+            _ -> type_error({not_a_variant_type, Id, T}),
+                 {Id, []}
+        end,
+    [ check_expr(Env, Con,
+            case CArgs of
+                [] -> Base1;
+                _ -> {fun_t, CAnn, [], CArgs, Base1}
+            end)
+      || {constr_t, CAnn, Con, CArgs} <- Constrs
+    ],
+    Constrs1 =
+        [ case [ ConstrNew
+                 || ConstrNew = {constr_t, _, CNameNew, _} <- Constrs,
+                    name(CNameNew) == name(CNameOld)] of
+              [{constr_t, FAnn, CName, CArgs}] ->
+                  {constr_t, FAnn, CName,
+                   [ check_type(Env, CArg) || CArg <- CArgs ]
+                  };
+              _ -> ConstrOld
+          end
+          || ConstrOld = {constr_t, _, CNameOld, _} <- TrueConstrs
+        ],
+    OnQcon = fun(A) -> qcon(aeso_syntax:get_ann(QId), lists:droplast(qname(QId)) ++ qname(A)) end,
+    TagPred =
+        case Constrs of
+            [] -> [{bool, [], false}];
+            [{constr_t, CAnn, Con, Args}] ->
+                [{is_tag, CAnn, TId, OnQcon(Con), Args, Base1}];
+            _ ->
+                [ {app, Ann, {'!', Ann},
+                   [{is_tag, CAnn, TId, OnQcon(TrueCon), Args, Base1}]}
+                 || {constr_t, CAnn, TrueCon, Args} <- TrueConstrs,
+                    lists:all(
+                      fun({constr_t, _, Con, _}) ->
+                              qname(Con) /= qname(TrueCon)
+                      end, Constrs
+                     )
+                ]
+        end,
+    {dep_variant_t, Ann, TId, Base1, TagPred, Constrs1};
+check_type(Env, T = {dep_list_t, Ann, Id, ElemT, LenPred}, Arity) ->
+    ensure_base_type(T, Arity),
+    [type_error({illegal_liquid, T}) || not Env#env.allow_liquid],
+    ElemT1 = check_type(Env, ElemT),
+    Env1 = Env#env{allow_liquid = false},
+    Env2 = bind_var(Id, {id, [], "int"}, Env1),
+    LenPred1 = [check_expr(Env2, Q, {id, [], "bool"}) || Q <- LenPred],
+    {dep_list_t, Ann, Id, ElemT1, LenPred1};
 check_type(_Env, {args_t, Ann, Ts}, _) ->
     type_error({new_tuple_syntax, Ann, Ts}),
     {tuple_t, Ann, Ts}.
@@ -1263,7 +1382,12 @@ infer_letrec(Env, Defs) ->
 infer_letfun(Env, {fun_clauses, Ann, Fun = {id, _, Name}, Type, Clauses}) ->
     Type1 = check_type(Env, Type),
     {NameSigs, Clauses1} = lists:unzip([ infer_letfun1(Env, Clause) || Clause <- Clauses ]),
-    {_, Sigs = [Sig | _]} = lists:unzip(NameSigs),
+    {_, Sigs = [Sig0 | _]} = lists:unzip(NameSigs),
+    Sig = case Type1 of
+              {fun_t, TAnn, Named, ArgsT, RetT} ->
+                  {type_sig, TAnn, none, Named, ArgsT, RetT};
+              _ -> Sig0
+          end,
     _ = [ begin
             ClauseT = typesig_to_fun_t(ClauseSig),
             unify(Env, ClauseT, Type1, {check_typesig, Name, ClauseT, Type1})
@@ -1302,8 +1426,8 @@ desugar_clauses(Ann, Fun, {type_sig, _, _, _, ArgTypes, RetType}, Clauses) ->
             {letfun, Ann, Fun, Args, RetType,
              {typed, NoAnn,
               {switch, NoAnn, Tuple(Args),
-                [ {'case', AnnC, Tuple(ArgsC), Body}
+               [ {'case', AnnC, Tuple(ArgsC), Body}
-                || {letfun, AnnC, _, ArgsC, _, Body} <- Clauses ]}, RetType}}
+                 || {letfun, AnnC, _, ArgsC, _, Body} <- Clauses ]}, RetType}}
     end.
 
 print_typesig({Name, TypeSig}) ->
@@ -1735,8 +1859,8 @@ 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, [], Args, Inferred, ArgTypes}),
+    unify(Env, ArgTypes, OperandTypes, {infer_app, Op, [], Inferred, ArgTypes}),
-    {typed, As, {app, As, Op, TypedArgs}, ResultType}.
+    {typed, As, {app, As, {typed, As, Op, Inferred}, TypedArgs}, ResultType}.
 
 infer_pattern(Env, Pattern) ->
     Vars = free_vars(Pattern),
@@ -2226,7 +2350,7 @@ solve_known_record_types(Env, Constraints) ->
                              unify(Env, FreshRecType, RecType, {record_constraint, FreshRecType, RecType, When}),
                              C
                      end;
-                _ ->
+                X ->
                     type_error({not_a_record_type, instantiate(RecType), When}),
                     not_solved
              end
@@ -2264,6 +2388,8 @@ 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({dep_record_t, _, 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"}.
@@ -2390,6 +2516,8 @@ unfold_types_in_type(Env, {constr_t, Ann, Con, Types}, Options) ->
     {constr_t, Ann, Con, unfold_types_in_type(Env, Types, Options)};
 unfold_types_in_type(Env, {named_arg_t, Ann, Con, Types, Default}, Options) ->
     {named_arg_t, Ann, Con, unfold_types_in_type(Env, Types, Options), Default};
+unfold_types_in_type(Env, {dep_arg_t, Ann, Con, Types}, Options) ->
+    {dep_arg_t, Ann, Con, unfold_types_in_type(Env, Types, Options)};
 unfold_types_in_type(Env, T, Options) when is_tuple(T) ->
     list_to_tuple(unfold_types_in_type(Env, tuple_to_list(T), Options));
 unfold_types_in_type(Env, [H|T], Options) ->
@@ -2487,6 +2615,26 @@ unify1(Env, {app_t, _, T, []}, B, When) ->
     unify(Env, T, B, When);
 unify1(Env, A, {app_t, _, T, []}, When) ->
     unify(Env, A, T, When);
+unify1(Env, A, {refined_t, _, _, B, _}, When) ->
+    unify1(Env, A, B, When);
+unify1(Env, {refined_t, _, _, A, _}, B, When) ->
+    unify1(Env, A, B, When);
+unify1(Env, A, {dep_record_t, _, B, _}, When) ->
+    unify1(Env, A, B, When);
+unify1(Env, {dep_record_t, _, A, _}, B, When) ->
+    unify1(Env, A, B, When);
+unify1(Env, A, {dep_variant_t, _, _, B, _, _}, When) ->
+    unify1(Env, A, B, When);
+unify1(Env, {dep_variant_t, _, _, A, _, _}, B, When) ->
+    unify1(Env, A, B, When);
+unify1(Env, A, {dep_list_t, Ann, _, B, _}, When) ->
+    unify1(Env, A, {app_t, Ann, {id, Ann, "list"}, [B]}, When);
+unify1(Env, {dep_list_t, Ann, _, A, _}, B, When) ->
+    unify1(Env, {app_t, Ann, {id, Ann, "list"}, [A]}, B, When);
+unify1(Env, {named_t, _, _, A}, B, When) ->
+    unify1(Env, A, B, When);
+unify1(Env, A, {named_t, _, _, B}, When) ->
+    unify1(Env, A, B, When);
 unify1(_Env, A, B, When) ->
     cannot_unify(A, B, When),
     false.
@@ -2535,6 +2683,18 @@ occurs_check1(R, {if_t, _, _, Then, Else}) ->
     occurs_check(R, [Then, Else]);
 occurs_check1(R, [H | T]) ->
     occurs_check(R, H) orelse occurs_check(R, T);
+occurs_check1(R, {named_t, _, _, T}) ->
+    occurs_check1(R, T);
+occurs_check1(R, {refined_t, _, _, T, _}) ->
+    occurs_check1(R, T);
+occurs_check1(R, {dep_record_t, _, _, T}) ->
+    occurs_check1(R, T);
+occurs_check1(R, {dep_variant_t, _, _, _, _, T}) ->
+    occurs_check1(R, T);
+occurs_check1(R, {constr_t, _, _, T}) ->
+    occurs_check(R, T);
+occurs_check1(R, {dep_list_t, _, _, T, _}) ->
+    occurs_check1(R, T);
 occurs_check1(_, []) -> false.
 
 fresh_uvar(Attrs) ->
@@ -2689,8 +2849,9 @@ mk_error({fundecl_must_have_funtype, _Ann, Id, Type}) ->
                        , [pp(Id), pp_loc(Id), pp(instantiate(Type))]),
     mk_t_err(pos(Id), Msg);
 mk_error({cannot_unify, A, B, When}) ->
-    Msg = io_lib:format("Cannot unify ~s\n         and ~s\n",
+    AStr = pp(instantiate(A)),
-                        [pp(instantiate(A)), pp(instantiate(B))]),
+    BStr = pp(instantiate(B)),
+    Msg = io_lib:format("Cannot unify ~s\n         and ~s\n", [AStr, BStr]),
     {Pos, Ctxt} = pp_when(When),
     mk_t_err(Pos, Msg, Ctxt);
 mk_error({unbound_variable, Id}) ->
@@ -2704,6 +2865,9 @@ mk_error({unbound_variable, Id}) ->
 mk_error({undefined_field, Id}) ->
     Msg = io_lib:format("Unbound field ~s at ~s\n", [pp(Id), pp_loc(Id)]),
     mk_t_err(pos(Id), Msg);
+mk_error({not_a_variant_type, Type}) ->
+    Msg = io_lib:format("~s\n", [pp_type("Not a variant type: ", Type)]),
+    mk_t_err(pos(Type), Msg);
 mk_error({not_a_record_type, Type, Why}) ->
     Msg = io_lib:format("~s\n", [pp_type("Not a record type: ", Type)]),
     {Pos, Ctxt} = pp_why_record(Why),
@@ -2987,6 +3151,9 @@ mk_error({contract_lacks_definition, Type, When}) ->
            ),
     {Pos, Ctxt} = pp_when(When),
     mk_t_err(Pos, Msg, Ctxt);
+mk_error({illegal_liquid, T}) ->
+    Msg = io_lib:format("Illegal liquid type ~s", [pp_type("", T)]),
+    mk_t_err(pos(T), Msg);
 mk_error(Err) ->
     Msg = io_lib:format("Unknown error: ~p\n", [Err]),
     mk_t_err(pos(0, 0), Msg).
@@ -3149,8 +3316,11 @@ pp_why_record(Fld = {field, _Ann, LV, _Alias, _E}) ->
 pp_why_record({proj, _Ann, Rec, FldName}) ->
     {pos(Rec),
      io_lib:format("arising from the projection of the field ~s (at ~s)",
-         [pp(FldName), pp_loc(Rec)])}.
+                   [pp(FldName), pp_loc(Rec)])};
-
+pp_why_record({dep_record_t, _, Rec, _}) ->
+    {pos(Rec),
+     io_lib:format("arising from the record refinement of the type ~s (at ~s)",
+                   [pp(Rec), pp_loc(Rec)])}.
 
 if_branches(If = {'if', Ann, _, Then, Else}) ->
     case proplists:get_value(format, Ann) of

src/aeso_ast_refine_types.hrl

@@ -0,0 +1,56 @@
+
+-define(op(Ann, A, Op, B), {app, [{format, infix}|Ann], {Op, Ann}, [A, B]}).
+-define(op(Ann, Op, B), {app, [{format, prefix}|Ann], {Op, Ann}, [B]}).
+
+-define(int(Ann, I), {int, Ann, I}).
+-define(int_tp, {id, _, "int"}).
+-define(int_t(Ann), {id, Ann, "int"}).
+
+-define(d_pos_int(Ann), ?refined(?int_t(Ann), [?op(Ann, ?nu(Ann), '>', ?int(Ann, 0))])).
+-define(d_nonneg_int(Ann), ?refined(?int_t(Ann), [?op(Ann, ?nu(Ann), '>=', ?int(Ann, 0))])).
+%% -define(d_nonzero_int, refined(?int_t, [?op(?nu(), '!=', ?int(0))])).
+
+-define(bool(Ann, B), {bool, Ann, B}).
+-define(bool_tp, {id, _, "bool"}).
+-define(bool_t(Ann), {id, Ann, "bool"}).
+
+%% -define(tuple(S), {tuple, _, S}).
+-define(tuple_tp(T), {tuple_t, _, T}).
+%% -define(tuple_t(T), {tuple_t, ?ann(), T}).
+
+-define(tuple_proj_id(Ann, N, I),
+        {id, Ann, lists:flatten(io_lib:format("$tuple~p.~p", [N, I]))}).
+-define(adt_proj_id(Ann, QCon, I),
+        {id, Ann, lists:flatten(io_lib:format("~s.~p", [string:join(qname(QCon), "."), I]))}).
+
+%% -define(string(S), {string, _, S}).
+-define(string_tp, {id, _, "string"}).
+%% -define(string_t, {id, ?ann(), "string"}).
+
+-define(typed(Expr, Type), {typed, element(2, Expr), Expr, Type}).
+-define(typed_p(Expr), {typed, _, Expr, _}).
+-define(typed_p(Expr, Type), {typed, _, Expr, Type}).
+
+-define(refined(Id, T, Q),
+    {refined_t, element(2, T), Id, T, Q}).
+-define(refined(T, Q),
+    (fun(Id) ->
+            ?refined(Id, T, apply_subst(?nu(element(2, T)), Id, Q))
+     end)
+      (fresh_id(
+         element(2, T),
+         case T of
+             ?int_tp -> "n";
+             ?bool_tp -> "b";
+             ?string_tp -> "s";
+             _ when element(1, T) == id -> name(T);
+             _ -> "v"
+         end
+        ))).
+-define(refined(T), ?refined(T, [])).
+
+-define(ann(), [{origin, hagia}]).
+-define(ann_of(E), element(2, E)).
+
+-define(nu(Ann), {id, Ann, "$self"}).
+-define(nu_p, {id, _, "$self"}).

src/aeso_ast_refine_types_stdlib.hrl

@@ -0,0 +1,391 @@
+
+-define(IS_STDLIB(NS),
+        (NS == "List" orelse
+         NS == "ListInternal" orelse
+         NS == "Option" orelse
+         NS == "Bits" orelse
+         NS == "Bytes" orelse
+         NS == "Char" orelse
+         NS == "Int" orelse
+         NS == "Map" orelse
+         NS == "Address" orelse
+         NS == "Crypto" orelse
+         NS == "Auth" orelse
+         NS == "Oracle" orelse
+         NS == "AENS" orelse
+         NS == "Contract" orelse
+         NS == "Call" orelse
+         NS == "Chain" orelse
+         false
+        )).
+
+-define(IS_STDLIB_STATEFUL(NS, Fun),
+        ((NS == "List" andalso Fun == "map") orelse
+         (NS == "List" andalso Fun == "flat_map") orelse
+         (NS == "Chain" andalso Fun == "spend") orelse
+         false
+        )).
+
+
+-define(CONSTR(NS, Fun, Args, ArgsT, Body),
+        constr_expr(Env, {app, Ann, {typed, _, {qid, _, [NS, Fun]}, {fun_t, _, [], ArgsT, _}}, Args}, RetT, S0) ->
+               Body;
+       ).
+-define(CONSTR(NS, Fun, Args, Body),
+constr_expr(Env, {app, Ann, {typed, _, {qid, _, [NS, Fun]}, {fun_t, _, [], _, _}}, Args}, RetT, S0) ->
+    Body;
+    ).
+
+-define(UNSOME(Pat, Constrs), [Pat] =
+                   [ ArgT
+                     || C <- Constrs,
+                        ArgT <- case C of
+                                    {dep_constr_t, CAnn, Con = {con, _, "Some"}, [CT]} -> [CT];
+                                    _ -> []
+                                end
+                   ]).
+
+-define(
+   STDLIB_CONSTRS,
+   ?CONSTR("Chain", "spend", [State, Balance, Addr, Amount],
+           begin
+               {_, S1} = constr_expr(Env, State, S0),
+               {BalanceT, S2} = constr_expr(Env, Balance, S1),
+               {_, S3} = constr_expr(Env, Addr, S2),
+               {AmountT, S4} = constr_expr(Env, Amount, S3),
+               ExprT = {tuple_t, _, [_, _, NewBalanceT]} = fresh_liquid(Env, "spend", RetT),
+               {ExprT,
+                [ {well_formed, constr_id(chain_spend), Env, ExprT}
+                , {subtype, constr_id(chain_spend), Ann, Env,
+                   AmountT,
+                   ?refined(?int_t(Ann), [ ?op(Ann, ?nu(Ann), '=<', Balance)
+                                        , ?op(Ann, ?nu(Ann), '>=', ?int(Ann, 0))])}
+                , {subtype, constr_id(chain_spend), Ann, Env,
+                   ?refined(?int_t(Ann), [?op(Ann, ?nu(Ann), '==', ?op(Ann, Balance, '-', Amount))]),
+                   NewBalanceT
+                  }
+                | S4
+                ]
+               }
+           end
+          )
+
+   ?CONSTR("List", "is_empty", [L],
+           begin
+               {_, S1} = constr_expr(Env, L, S0),
+               ExprT = fresh_liquid(Env, "is_empty", RetT),
+               { ExprT
+               , [ {well_formed, constr_id(list_is_empty), Env, ExprT}
+                 , {subtype, constr_id(is_empty), Ann, Env,
+                    ?refined(?bool_t(Ann), [?op(Ann, ?nu(Ann), '==', ?op(Ann, L, '==', ?int(Ann, 0)))]),
+                    ExprT}
+                 | S1
+                 ]
+               }
+           end
+          )
+
+    ?CONSTR("List", "first", [L],
+           begin
+               {{dep_list_t, _, _, ElemT, _}, S1} = constr_expr(Env, L, S0),
+               ExprT = {dep_variant_t, _, Id, _, _, Constrs} = fresh_liquid(Env, "first", RetT),
+               ?UNSOME(RetConT, Constrs),
+               EnvEmpty = assert(?op(Ann, L, '==', ?int(Ann, 0)), Env),
+               EnvCons = assert(?op(Ann, L, '>', ?int(Ann, 0)), Env),
+               { ExprT
+               , [ {well_formed, constr_id(list_first), Env, ExprT}
+                 , {subtype, constr_id(list_first), Ann, EnvEmpty,
+                    {dep_variant_t, Ann, Id, RetT, [{is_tag, Ann, Id, {qcon, Ann, ["None"]}, []}], Constrs},
+                    ExprT}
+                 , {subtype, constr_id(list_first), Ann, EnvCons,
+                    {dep_variant_t, Ann, Id, RetT, [{is_tag, Ann, Id, {qcon, Ann, ["Some"]}, [RetConT]}], Constrs},
+                    ExprT}
+                 , {subtype, constr_id(list_first), Ann, EnvCons, ElemT, RetConT}
+                 | S1
+                 ]
+               }
+           end
+           )
+
+    ?CONSTR("List", "tail", [L],
+           begin
+               {{dep_list_t, _, _, ElemT, _}, S1} = constr_expr(Env, L, S0),
+               {_, S1} = constr_expr(Env, L, S0),
+               ExprT = {dep_variant_t, _, Id, _, _, Constrs} = fresh_liquid(Env, "tail", RetT),
+               ?UNSOME(RetConT, Constrs),
+               EnvEmpty = assert(?op(Ann, L, '==', ?int(Ann, 0)), Env),
+               EnvCons = assert(?op(Ann, L, '>', ?int(Ann, 0)), Env),
+               LId = fresh_id(Ann, "tail_l"),
+               { ExprT
+               , [ {well_formed, constr_id(list_tail), Env, ExprT}
+                 , {subtype, constr_id(list_tail), Ann, EnvEmpty,
+                    {dep_variant_t, Ann, Id, RetT, [{is_tag, Ann, Id, {qcon, Ann, ["None"]}, []}], Constrs},
+                    ExprT}
+                 , {subtype, constr_id(list_tail), Ann, EnvCons,
+                    {dep_variant_t, Ann, Id, RetT, [{is_tag, Ann, Id, {qcon, Ann, ["Some"]}, [RetConT]}], Constrs},
+                    ExprT}
+                 , {subtype, constr_id(list_tail), Ann, EnvCons,
+                   {dep_list_t, Ann, LId, ElemT, [?op(Ann, LId, '==', ?op(Ann, L, '-', ?int(Ann, 1)))]}, RetConT}
+                 | S1
+                 ]
+               }
+           end
+           )
+
+    ?CONSTR("List", "last", [L],
+           begin
+               {{dep_list_t, _, _, ElemT, _}, S1} = constr_expr(Env, L, S0),
+               ExprT = {dep_variant_t, _, Id, _, _, Constrs} = fresh_liquid(Env, "last", RetT),
+               ?UNSOME(RetConT, Constrs),
+               EnvEmpty = assert(?op(Ann, L, '==', ?int(Ann, 0)), Env),
+               EnvCons = assert(?op(Ann, L, '>', ?int(Ann, 0)), Env),
+               { ExprT
+               , [ {well_formed, constr_id(list_last), Env, ExprT}
+                 , {subtype, constr_id(list_last), Ann, EnvEmpty,
+                    {dep_variant_t, Ann, Id, RetT, [{is_tag, Ann, Id, {qcon, Ann, ["None"]}, []}], Constrs},
+                    ExprT}
+                 , {subtype, constr_id(list_last), Ann, EnvCons,
+                    {dep_variant_t, Ann, Id, RetT, [{is_tag, Ann, Id, {qcon, Ann, ["Some"]}, [RetConT]}], Constrs},
+                    ExprT}
+                 , {subtype, constr_id(list_last), Ann, EnvCons, ElemT, RetConT}
+                 | S1
+                 ]
+               }
+           end
+           )
+
+   %% TODO contains – force false if no way to fulfill
+
+   %% TODO find – reduce type to fulfill the predicate
+
+    ?CONSTR("List", "find_indices", [P, L], %% TODO: len == 0 if no way to fulfill
+           begin
+               {_, S1} = constr_expr(Env, P, S0),
+               {_, S2} = constr_expr(Env, L, S1),
+               ExprT = {dep_list_t, _, _, ElemT, _} = fresh_liquid(Env, "find_indices", RetT),
+               LId = fresh_id(Ann, "find_indices_l"),
+               { ExprT
+               , [ {well_formed, constr_id(list_find_indices), Env, ExprT}
+                 , {subtype, constr_id(list_find_indices), Ann, Env,
+                    {dep_list_t, Ann, LId, ElemT, [?op(Ann, LId, '=<', L)]},
+                    ExprT
+                   }
+                 , {subtype, constr_id(list_find_indices), Ann, Env, ?d_nonneg_int(Ann), ElemT}
+                 | S2
+                 ]
+               }
+           end
+           )
+
+    ?CONSTR("List", "nth", [I, L],
+           begin
+               {IT, S1} = constr_expr(Env, I, S0),
+               {{dep_list_t, _, _, ElemT, _}, S2} = constr_expr(Env, L, S1),
+               ExprT = {dep_variant_t, _, Id, _, _, Constrs} = fresh_liquid(Env, "nth", RetT),
+               ?UNSOME(RetConT, Constrs),
+               EnvEmpty = assert(?op(Ann, L, '==', ?int(Ann, 0)), Env),
+               EnvCons = assert(?op(Ann, L, '>', ?int(Ann, 0)), Env),
+               { ExprT
+               , [ {well_formed, constr_id(list_nth), Env, ExprT}
+                 , {subtype, constr_id(list_nth), Ann, EnvEmpty,
+                    {dep_variant_t, Ann, Id, RetT, [{is_tag, Ann, Id, {qcon, Ann, ["None"]}, []}], Constrs},
+                    ExprT}
+                 , {subtype, constr_id(list_nth), Ann, EnvCons,
+                    {dep_variant_t, Ann, Id, RetT, [{is_tag, Ann, Id, {qcon, Ann, ["Some"]}, [RetConT]}], Constrs},
+                    ExprT}
+                 , {subtype, constr_id(list_nth), Ann, EnvCons, ElemT, RetConT}
+                 , {subtype, constr_id(list_nth), Ann, Env, IT, ?d_nonneg_int(Ann)}
+                 | S2
+                 ]
+               }
+           end
+           )
+
+   ?CONSTR("List", "get", [I, L],
+           begin
+               {IT, S1} = constr_expr(Env, I, S0),
+               {{dep_list_t, _, _, ElemT, _}, S2} = constr_expr(Env, L, S1),
+               ExprT = fresh_liquid(Env, "get", RetT),
+               LId = fresh_id(Ann, "get_l"),
+               { ExprT
+               , [ {well_formed, constr_id(list_get), Env, ExprT}
+                 , {subtype, constr_id(list_get), Ann, Env,
+                    IT,
+                    {refined_t, Ann, LId, ?int_t(Ann), [?op(Ann, LId, '<', L)]}}
+                 , {subtype, constr_id(list_get), Ann, Env, ElemT, ExprT}
+                 , {subtype, constr_id(list_get), Ann, Env, IT, ?d_nonneg_int(Ann)}
+                 | S2
+                 ]
+               }
+           end
+          )
+
+   ?CONSTR("List", "length", [L],
+           begin
+               {_, S1} = constr_expr(Env, L, S0),
+               ExprT = fresh_liquid(Env, "length", RetT),
+               LId = fresh_id(Ann, "length_l"),
+               { ExprT
+               , [ {well_formed, constr_id(list_length), Env, ExprT}
+                 , {subtype, constr_id(list_length), Ann, Env,
+                   {refined_t, Ann, LId, ?int_t(Ann), [?op(Ann, LId, '==', L)]}
+                   , ExprT}
+                 | S1
+                 ]
+               }
+           end
+           )
+
+   ?CONSTR("List", "from_to", [From, To],
+           begin
+               {_, S1} = constr_expr(Env, From, S0),
+               {_, S2} = constr_expr(Env, To, S1),
+               ExprT = fresh_liquid(Env, "from_to", RetT),
+               ElemT = ?refined(?int_t(Ann), [?op(Ann, From, '=<', ?nu(Ann)), ?op(Ann, ?nu(Ann), '=<', To)]),
+               EnvEmpty = assert(?op(Ann, To, '<', From), Env),
+               EnvSome = assert(?op(Ann, To, '>=', From), Env),
+               LId = fresh_id(Ann, "from_to_l"),
+               { ExprT
+               , [ {well_formed, constr_id(list_from_to), Env, ExprT}
+                 , {subtype, constr_id(list_from_to), Ann, EnvEmpty,
+                    {dep_list_t, Ann, LId, ElemT, [?op(Ann, LId, '==', ?int(Ann, 0))]},
+                    ExprT}
+                 , {subtype, constr_id(list_from_to), Ann, EnvSome,
+                    {dep_list_t, Ann, LId, ElemT, [?op(Ann, LId, '==', ?op(Ann, ?op(Ann, To, '-', From), '+', ?int(Ann, 1)))]},
+                    ExprT}
+                 | S2
+                 ]
+               }
+           end
+          )
+
+   ?CONSTR("List", "from_to_step", [From, To, Step],
+           begin
+               {_, S1} = constr_expr(Env, From, S0),
+               {_, S2} = constr_expr(Env, To, S1),
+               {StepT, S3} = constr_expr(Env, Step, S2),
+               ExprT = fresh_liquid(Env, "from_to_step", RetT),
+               ElemT = ?refined(?int_t(Ann), [?op(Ann, From, '=<', ?nu(Ann)), ?op(Ann, ?nu(Ann), '=<', To)]),
+               EnvEmpty = assert(?op(Ann, To, '<', From), Env),
+               EnvSome = assert(?op(Ann, To, '>=', From), Env),
+               LId = fresh_id(Ann, "from_to_l_step"),
+               { ExprT
+               , [ {well_formed, constr_id(list_from_to_step), Env, ExprT}
+                 , {subtype, constr_id(list_from_to_step), Ann, EnvEmpty,
+                    {dep_list_t, Ann, LId, ElemT, [?op(Ann, LId, '==', ?int(Ann, 0))]},
+                    ExprT}
+                 , {subtype, constr_id(list_from_to_step), Ann, EnvSome,
+                    {dep_list_t, Ann, LId, ElemT,
+                     [?op(Ann, LId, '==', ?op(Ann, ?op(Ann, ?op(Ann, To, '-', From), '/', Step), '+', ?int(Ann, 1)))]},
+                    ExprT}
+                 , {subtype, constr_id(list_from_to_step), Ann, Env, StepT, ?refined(?int_t(Ann), [?op(Ann, ?nu(Ann), '>', ?int(Ann, 0))])}
+                 | S2
+                 ]
+               }
+           end
+          )
+
+   %% TODO insert_at – consider length and update ElemT
+
+   %% TODO insert_by – consider length and update ElemT. skip comparator
+
+   ?CONSTR("List", "reverse", [L],
+           begin
+               {LT, S1} = constr_expr(Env, L, S0),
+               ExprT = fresh_liquid(Env, "reverse", RetT),
+               { ExprT
+               , [ {well_formed, constr_id(list_reverse), Env, ExprT}
+                 , {subtype, constr_id(list_reverse), Ann, Env, LT, ExprT}
+                 | S1
+                 ]
+               }
+           end
+          )
+
+   ?CONSTR("List", "map", [State = ?typed_p(_, StateT), Balance = ?typed_p(_, BalanceT), F = ?typed_p(UF), L],
+           [_, _, {fun_t, _, _, [_, _, _], _}, _],
+           begin
+               IsStateful = is_stateful(Env, UF),
+               {_, S1} = constr_expr(Env, State, S0),
+               {_, S2} = constr_expr(Env, Balance, S1),
+               NewStateT = fresh_liquid(Env, "map_state", StateT),
+               NewBalanceT = fresh_liquid(Env, "map_balance", BalanceT),
+               {{dep_list_t, _, LId, ElemT, LenQual}, S3} = constr_expr(Env, L, S2),
+               {{dep_fun_t, _,
+                 [ {dep_arg_t, _, StateId, StateArgT}
+                 , {dep_arg_t, _, BalanceId, BalanceArgT}
+                 , {dep_arg_t, _, ArgId, ArgT}
+                 ], FunResT}, S4} = constr_expr(Env, F, S3),
+               case IsStateful of
+                   true  -> {tuple_t, _, [ResT|_]} = FunResT;
+                   false -> ResT = FunResT
+               end,
+               {tuple_t, ExAnn, [ExprT|_]} = fresh_liquid(Env, "map", RetT),
+               STExprT = {tuple_t, ExAnn, [ExprT, NewStateT, NewBalanceT]},
+               AbstractElem = fresh_id(Ann, "map_list_elem"),
+               AppEnv = bind_var(AbstractElem, ElemT, Env),
+               AppElemT =
+                   apply_subst(
+                     [ {StateId, State}
+                     , {BalanceId, Balance}
+                     , {ArgId, AbstractElem}
+                     ], ResT
+                    ),
+               { STExprT
+               , [ {well_formed, constr_id(list_map_wf), Env, STExprT}
+                 , {subtype, constr_id(list_map_len_preserve), Ann, AppEnv,
+                   {dep_list_t, Ann, LId, AppElemT, LenQual}, ExprT}
+                 , {subtype, constr_id(list_map_state), Ann, Env, StateT, StateArgT}
+                 , {subtype, constr_id(list_map_balance), Ann, Env, BalanceT, BalanceArgT}
+                 | S4
+                 ]
+               }
+           end
+          )
+
+   ?CONSTR("List", "flat_map", [State = ?typed_p(_, StateT), Balance = ?typed_p(_, BalanceT), F = ?typed_p(UF), L],
+           [_, _, {fun_t, _, _, [_, _, _], _}, _],
+           begin
+               IsStateful = is_stateful(Env, UF),
+               {_, S1} = constr_expr(Env, State, S0),
+               {_, S2} = constr_expr(Env, Balance, S1),
+               NewStateT = fresh_liquid(Env, "flat_map_state", StateT),
+               NewBalanceT = fresh_liquid(Env, "flat_map_balance", BalanceT),
+               {{dep_list_t, _, LId, ElemT, _}, S3} = constr_expr(Env, L, S2),
+               {QWE = {dep_fun_t, _,
+                 [ {dep_arg_t, _, StateId, StateArgT}
+                 , {dep_arg_t, _, BalanceId, BalanceArgT}
+                 , {dep_arg_t, _, ArgId, ArgT}
+                 ], FunResT}, S4} = constr_expr(Env, F, S3),
+               case IsStateful of
+                   true  -> {tuple_t, _, [ResT|_]} = FunResT;
+                   false -> ResT = FunResT
+               end,
+               {dep_list_t, _, _, ResElemT, _} = ResT,
+               {tuple_t, ExAnn, [ExprT|_]} = fresh_liquid(Env, "flat_map", RetT),
+               STExprT = {tuple_t, ExAnn, [ExprT, NewStateT, NewBalanceT]},
+               AbstractElem = fresh_id(Ann, "flat_map_list_elem"),
+               AbstractGen = fresh_id(Ann, "flat_map_gen"),
+               ResSubst =
+                   [ {StateId, State}
+                   , {BalanceId, Balance}
+                   , {ArgId, AbstractElem}
+                   ],
+               AppEnv = bind_vars(
+                          [ {AbstractElem, ElemT}
+                          , {AbstractGen, apply_subst(ResSubst, ResT)}
+                          ], Env),
+               AppElemT = apply_subst(ResSubst, ResElemT),
+               { STExprT
+               , [ {well_formed, constr_id(list_flat_map), Env, STExprT}
+                 , {subtype, constr_id(list_flat_map), Ann, AppEnv,
+                    {dep_list_t, Ann, LId, AppElemT, [?op(Ann, LId, '>=', ?int(Ann, 0)), ?op(Ann, LId, '=<', ?op(Ann, L, '*', AbstractGen))]},
+                    ExprT}
+                 , {subtype, constr_id(list_flat_map), Ann, Env, StateT, StateArgT}
+                 , {subtype, constr_id(list_flat_map), Ann, Env, BalanceT, BalanceArgT}
+                 | S4
+                 ]
+               }
+           end
+          )
+  ).

src/aeso_ast_to_fcode.erl

@@ -699,12 +699,15 @@ expr_to_fcode(Env, _Type, {block, _, Stmts}) ->
     stmts_to_fcode(Env, Stmts);
 
 %% Binary operator
-expr_to_fcode(Env, _Type, Expr = {app, _, {Op, _}, [_, _]}) when Op == '&&'; Op == '||' ->
+expr_to_fcode(Env, _Type, Expr = {app, _, {typed, _, {Op, _}, _}, [_, _]})
+  when Op == '&&'; Op == '||' ->
     Tree = expr_to_decision_tree(Env, Expr),
     decision_tree_to_fcode(Tree);
-expr_to_fcode(Env, _Type, {app, _Ann, {Op, _}, [A, B]}) when is_atom(Op) ->
+expr_to_fcode(Env, _Type, {app, _Ann, {typed, _, {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, {Op, _}, [A]}) when is_atom(Op) ->
+expr_to_fcode(Env, _Type, {app, _Ann, {typed, _, {Op, _}, _}, [A]})
+  when is_atom(Op) ->
     case Op of
         '-' -> {op, '-', [{lit, {int, 0}}, expr_to_fcode(Env, A)]};
         '!' -> {op, '!', [expr_to_fcode(Env, A)]}
@@ -2211,6 +2214,8 @@ pp_pat(P = {Tag, _}) when Tag == bool; Tag == int; Tag == string
                          -> pp_fexpr({lit, P});
 pp_pat(Pat)              -> pp_fexpr(Pat).
 
+is_infix({typed, _, Op, _}) ->
+    is_infix(Op);
 is_infix(Op) ->
     C = hd(atom_to_list(Op)),
     C < $a orelse C > $z.

src/aeso_ast_to_icode.erl

@@ -302,12 +302,12 @@ ast_body({app, _, {'..', _}, [A, B]}, Icode) ->
 ast_body({app, As, Fun, Args}, Icode) ->
     case aeso_syntax:get_ann(format, As) of
         infix  ->
-            {Op, _} = Fun,
+            {typed, _, {Op, _}, _} = Fun,
-            [A, B]  = Args,
+            [A, B] = Args,
             ast_binop(Op, As, A, B, Icode);
         prefix ->
-            {Op, _} = Fun,
+            {typed, _, {Op, _}, _} = Fun,
-            [A]     = Args,
+            [A] = Args,
             #unop{op = Op, rand = ast_body(A, Icode)};
         _ ->
             {typed, _, Fun1, {fun_t, _, _, ArgsT, RetT}} = Fun,

src/aeso_parse_lib.hrl

@@ -15,6 +15,8 @@
 -define(RULE(A, B, C, D,       Do), map(fun({_1, _2, _3, _4}) ->         Do end, {A, B, C, D}      )).
 -define(RULE(A, B, C, D, E,    Do), map(fun({_1, _2, _3, _4, _5}) ->     Do end, {A, B, C, D, E}   )).
 -define(RULE(A, B, C, D, E, F, Do), map(fun({_1, _2, _3, _4, _5, _6}) -> Do end, {A, B, C, D, E, F})).
+-define(RULE(A, B, C, D, E, F, G, Do), map(fun({_1, _2, _3, _4, _5, _6, _7}) -> Do end, {A, B, C, D, E, F, G})).
+-define(RULE(A, B, C, D, E, F, G, H, Do), map(fun({_1, _2, _3, _4, _5, _6, _7, _8}) -> Do end, {A, B, C, D, E, F, G, H})).
 
 -import(aeso_parse_lib,
         [tok/1, tok/2, between/3, many/1, many1/1, sep/2, sep1/2,

src/aeso_parser.erl

@@ -17,6 +17,8 @@
          run_parser/2,
          run_parser/3]).
 
+-include("aeso_ast_refine_types.hrl").
+
 -include("aeso_parse_lib.hrl").
 -import(aeso_parse_lib, [current_file/0, set_current_file/1]).
 
@@ -181,7 +183,14 @@ constructor() ->    %% TODO: format for Con() vs Con
 
 con_args()   -> paren_list(con_arg()).
 type_args()  -> paren_list(type()).
-field_type() -> ?RULE(id(), tok(':'), type(), {field_t, get_ann(_1), _1, _3}).
+field_type() ->
+    ?LAZY_P(choice(
+    [ ?RULE(tok('{'), id(), tok(':'), typeRefinable(), tok('|'), comma_sep1(expr()), tok('}'),
+            {field_t, get_ann(_2), _2, {refined_t, get_ann(_4), _2, _4, _6}})
+    ,  ?RULE(tok('{'), id(), tok(':'), id("list"), parens(type()), tok('|'), comma_sep1(expr()), tok('}'),
+             {field_t, get_ann(_2), _2, {dep_list_t, get_ann(_4), _2, _5, _7}})
+    , ?RULE(id(), tok(':'), type(), {field_t, get_ann(_1), _1, _3})
+    ])).
 
 con_arg()    -> choice(type(), ?RULE(keyword(indexed), type(), set_ann(indexed, true, _2))).
 
@@ -224,15 +233,41 @@ type300() ->
 
 type400() ->
     choice(
-    [?RULE(typeAtom(), optional(type_args()),
+    [?RULE(id("bytes"), parens(token(int)),
-          case _2 of
+           {bytes_t, get_ann(_1), element(3, _2)}),
-            none       -> _1;
+     %% Refined
-            {ok, Args} -> {app_t, get_ann(_1), _1, Args}
+     ?RULE(tok('{'), id(), tok(':'), typeRefinable(), tok('|'), comma_sep(expr()), tok('}'),
-          end),
+           refined_t(get_ann(_1), _2, _4, _6)
-     ?RULE(id("bytes"), parens(token(int)),
+          ),
-           {bytes_t, get_ann(_1), element(3, _2)})
+     %% Refined without pred
+     ?RULE(tok('{'), id(), tok(':'), typeRefinable(), tok('}'),
+           refined_t(get_ann(_1), _2, _4, [])
+          ),
+     %% Dep record
+     ?RULE(tok('{'), type500(), tok('<:'), comma_sep1(field_type()), tok('}'),
+           dep_record_t(get_ann(_1), _2, _4)
+          ),
+     %% Dep variant
+     ?RULE(tok('{'), type500(), tok('<:'), typedef(variant), tok('}'),
+           dep_variant_t(get_ann(_1), _2, _4)
+          ),
+     %% Dep list
+     ?RULE(tok('{'), id(), tok(':'), id("list"), parens(type()), tok('|'), comma_sep(expr()), tok('}'),
+           dep_list_t(get_ann(_1), _2, _5, _7)),
+     %% Dep list without pred
+     ?RULE(tok('{'), id(), tok(':'), id("list"), parens(type()), tok('}'),
+           dep_list_t(get_ann(_1), _2, _5, [])
+          ),
+     ?RULE(type500(), _1)
     ]).
 
+type500() ->
+    ?RULE(typeAtom(), optional(type_args()),
+          case _2 of
+              none       -> _1;
+              {ok, Args} -> {app_t, get_ann(_1), _1, Args}
+          end).
+
 typeAtom() ->
     ?LAZY_P(choice(
     [ parens(type())
@@ -240,6 +275,9 @@ typeAtom() ->
     , id(), token(con), token(qcon), token(qid), tvar()
     ])).
 
+typeRefinable() ->
+    ?LAZY_P(choice([id(), tvar()])).
+
 args_t() ->
     ?LAZY_P(choice(
     [ ?RULE(tok('('), tok(')'), {args_t, get_ann(_1), []})
@@ -247,6 +285,7 @@ args_t() ->
     , ?RULE(tok('('), type(), tok(','), sep1(type(), tok(',')), tok(')'), {args_t, get_ann(_1), [_2|_4]})
     ])).
 
+
 %% -- Statements -------------------------------------------------------------
 
 body() ->
@@ -478,6 +517,7 @@ parens(P)   -> between(tok('('), P, tok(')')).
 braces(P)   -> between(tok('{'), P, tok('}')).
 brackets(P) -> between(tok('['), P, tok(']')).
 comma_sep(P) -> sep(P, tok(',')).
+comma_sep1(P) -> sep1(P, tok(',')).
 
 paren_list(P)   -> parens(comma_sep(P)).
 brace_list(P)   -> braces(comma_sep(P)).
@@ -557,6 +597,18 @@ else_branches([Else = {else, _, _} | Stmts], Acc) ->
 else_branches(Stmts, Acc) ->
     {lists:reverse(Acc), Stmts}.
 
+refined_t(Ann, Id, Type, Pred) ->
+    {refined_t, Ann, Id, Type, Pred}.
+
+dep_record_t(Ann, Base, Fields) ->
+    {dep_record_t, Ann, Base, Fields}.
+
+dep_variant_t(Ann, Base, {variant_t, Constrs}) ->
+    {dep_variant_t, Ann, ?nu(Ann), Base, undefined, Constrs}.
+
+dep_list_t(Ann, Id, ElemT, LenPred) ->
+    {dep_list_t, Ann, Id, ElemT, LenPred}.
+
 tuple_t(_Ann, [Type]) -> Type;  %% Not a tuple
 tuple_t(Ann, Types)   -> {tuple_t, Ann, Types}.
 

src/aeso_pretty.erl

@@ -11,6 +11,8 @@
 
 -export([decls/1, decls/2, decl/1, decl/2, expr/1, expr/2, type/1, type/2]).
 
+-export([constr/1, dep_type/1, predicate/1, pp/2]).
+
 -export_type([options/0]).
 
 -include("aeso_utils.hrl").
@@ -207,7 +209,8 @@ name({con, _,  Name})  -> text(Name);
 name({qid, _,  Names}) -> text(string:join(Names, "."));
 name({qcon, _, Names}) -> text(string:join(Names, "."));
 name({tvar, _, Name})  -> text(Name);
-name({typed, _, Name, _}) -> name(Name).
+name({typed, _, Name, _}) -> name(Name);
+name({ltvar, Name}) -> text(Name).
 
 -spec letdecl(string(), aeso_syntax:letbind()) -> doc().
 letdecl(Let, {letval, _, P, E}) ->
@@ -282,7 +285,198 @@ type(T = {id, _, _})   -> name(T);
 type(T = {qid, _, _})  -> name(T);
 type(T = {con, _, _})  -> name(T);
 type(T = {qcon, _, _}) -> name(T);
-type(T = {tvar, _, _}) -> name(T).
+type(T = {tvar, _, _}) -> name(T);
+
+type(T) -> dep_type(T).
+
+
+dep_type({refined_t, _, Id, BaseType, []}) ->
+    beside(
+      [ text("{")
+      , hsep(
+          [ name(Id)
+          , text(":")
+          , type(BaseType)
+          ])
+      , text("}")
+      ]);
+dep_type({refined_t, _, Id, BaseType, Pred}) ->
+    beside(
+      [ text("{")
+      , hsep(
+          [ name(Id)
+          , text(":")
+          , type(BaseType)
+          , text("|")
+          , predicate(Pred)
+          ])
+      , text("}")
+      ]);
+dep_type({dep_fun_t, _, Args, Ret}) ->
+    follow
+      ( hsep
+          ( tuple([
+                   case DT of
+                       {refined_t, _, Id, _, _} when Id == ArgId ->
+                           dep_type(DT);
+                       {dep_list_t, _, Id, _, _} when Id == ArgId ->
+                           dep_type(DT);
+                       _ ->
+                           beside(
+                             [ text("{")
+                             , hsep(
+                                 [ name(ArgId)
+                                 , text(":")
+                                 , type(DT)
+                                 ])
+                             , text("}")
+                             ]
+                            )
+                   end
+                    || {dep_arg_t, _, ArgId, DT} <- Args])
+          , text("=>")
+          )
+      , type(Ret)
+      );
+dep_type({dep_record_t, _, Type, Fields}) ->
+    beside(
+      [ text("{")
+      , hsep(
+          [ type(Type)
+          , text("<:")
+          , par(punctuate(
+                  text(","),
+                  [ case FType of
+                        {refined_t, _, Id, _, _} when Id == FName ->
+                            dep_type(FType);
+                        _ -> hsep([name(FName), text(":"), type(FType)])
+                    end
+                    || {dep_field_t, _, FName, FType} <- Fields]
+                 ))
+          ])
+      , text("}")
+      ]);
+dep_type({dep_variant_t, _, _, Type, Pred, Constrs}) ->
+    PredList = if is_list(Pred) -> Pred;
+                  true -> []
+               end,
+    IsTags =
+        [ case HEAD of
+              con -> Tag;
+              qcon -> lists:last(Tag)
+          end
+         || {is_tag, _, _, {HEAD, _, Tag}, _, _} <- PredList],
+    NotIsTags =
+        [ case HEAD of
+              con -> Tag;
+              qcon -> lists:last(Tag)
+          end
+         || {app, _, {'!', _}, [{is_tag, _, _, {HEAD, _, Tag}, _, _}]} <- PredList],
+    Constrs1 =
+        case IsTags of
+            [] -> [ Con
+                   || Con = {constr_t, _, {con, _, CName}, _} <- Constrs,
+                      not lists:member(CName, NotIsTags)
+                  ];
+            _ ->
+                [ Con
+                  || Con = {constr_t, _, {con, _, CName}, _} <- Constrs,
+                     lists:member(CName, IsTags)
+                ]
+        end,
+    beside(
+      [ text("{")
+      , hsep(
+          [ type(Type)
+          , text("<:")
+          , if is_list(Pred) -> prettypr:empty();
+               true -> predicate(Pred)
+            end
+          , par(punctuate(text(" |"), lists:map(fun constructor_t/1, Constrs1)))
+          ])
+      , text("}")
+      ]);
+dep_type({dep_list_t, _, Id, Elem, []}) ->
+    beside(
+      [ text("{")
+      , hsep(
+          [ name(Id)
+          , text(":")
+          , type({app_t, [], {id, [], "list"}, [Elem]})
+          ])
+      , text("}")
+      ]);
+dep_type({dep_list_t, _, Id, Elem, LenPred}) ->
+    beside(
+      [ text("{")
+      , hsep(
+          [ name(Id)
+          , text(":")
+          , type({app_t, [], {id, [], "list"}, [Elem]})
+          , text("|")
+          , predicate(LenPred)
+          ])
+      , text("}")
+      ]
+     );
+dep_type(T = {tvar, _, _}) ->
+    name(T).
+
+subst(Subst) ->
+    beside(
+      [ text("[")
+      , hsep(
+          [ par(punctuate(
+                  text(";"),
+                  [ beside([expr(V), text("/"), expr(Q)])
+                    || {V, Q} <- Subst
+                  ]))
+          ])
+      , text("]")
+      ]
+     ).
+
+predicate({template, [], {ltvar, Var}}) -> text(Var);
+predicate({template, Subst, {ltvar, Var}}) ->
+    beside(subst(Subst), text(Var));
+predicate([]) -> text("true");
+predicate(L) when is_list(L) ->
+    par(punctuate(text(" &&"), [expr(E) || E <- L]));
+predicate(Constraints) when is_list(Constraints) ->
+    par(punctuate(text(","), [expr(C) || C <- Constraints])).
+
+constr_env(Env) ->
+    above(
+      [ par(punctuate(
+              text(","),
+              [beside([expr(Var), text(" : "), type(T)])
+               || {Var, {_, T}} <- aeso_ast_refine_types:type_binds(Env)])
+           )
+      , predicate(aeso_ast_refine_types:path_pred(Env))
+      ]).
+
+under_constr_env(Env, X) ->
+    above([ constr_env(Env)
+          , text("--------------")
+          , X
+          ]
+     ).
+
+constr({well_formed, _, Env, T}) ->
+    under_constr_env(Env, type(T));
+constr({subtype, Ref, _, Env, T1, T2}) ->
+    under_constr_env(
+      Env,
+      beside([ text(io_lib:format("~p\t", [Ref]))
+             , type(T1)
+             , text(" <: ")
+             , type(T2)
+             ]));
+constr({unreachable, _, _, Env}) ->
+    under_constr_env(Env, text("false"));
+constr({reachable, _, _, Env}) ->
+    above(text("SAT"), constr_env(Env)).
+
 
 -spec args_type([aeso_syntax:type()]) -> doc().
 args_type(Args) ->
@@ -346,6 +540,8 @@ expr_p(P, {assign, _, LV, E}) ->
 %% -- Operators
 expr_p(_, {app, _, {'..', _}, [A, B]}) ->
     list([infix(0, '..', A, B)]);
+expr_p(P, {app, As, {typed, _, {Op, OpAs}, _}, Args}) when is_atom(Op) ->
+    expr_p(P, {app, As, {Op, OpAs}, Args});
 expr_p(P, E = {app, _, F = {Op, _}, Args}) when is_atom(Op) ->
     case {aeso_syntax:get_ann(format, E), Args} of
         {infix, [A, B]} -> infix(P, Op, A, B);
@@ -398,7 +594,13 @@ expr_p(_, E = {qcon, _, _}) -> name(E);
 %% -- For error messages
 expr_p(_, {Op, _}) when is_atom(Op) ->
     paren(text(atom_to_list(Op)));
-expr_p(_, {lvalue, _, LV})  -> lvalue(LV).
+expr_p(_, {lvalue, _, LV})  -> lvalue(LV);
+expr_p(P, {is_tag, _, What, Con, Args, _}) ->
+    beside(
+      [ expr_p(P, What), text("==")
+      , app(P, Con, [{id, [], "_"} || _ <- Args])
+      ]
+     ).
 
 stmt_p({'if', _, Cond, Then}) ->
     block_expr(200, beside(text("if"), paren(expr(Cond))), Then);
@@ -504,3 +706,5 @@ get_elifs(If = {'if', Ann, Cond, Then, Else}, Elifs) ->
     end;
 get_elifs(Else, Elifs) -> {lists:reverse(Elifs), {else, Else}}.
 
+pp(PP, X) ->
+    prettypr:format(apply(aeso_pretty, PP, [X])).

src/aeso_smt.erl

@@ -0,0 +1,94 @@
+-module(aeso_smt).
+
+-compile([export_all]).
+
+-type formula() :: {var, string()}
+                 | {param, string()}
+                 | {int, integer()}
+                 | {list, [formula()]}
+                 | {app, string(), [formula()]}
+                   .
+
+-define(TIMEOUT, 10000).
+
+start_z3() ->
+    PortOpts = [exit_status, {line, 100000}],
+    Port = open_port({spawn, "z3 -in -t:" ++ integer_to_list(?TIMEOUT)}, PortOpts),
+    persistent_term:put(z3_connection, Port),
+    send_z3_success({app, "set-option", [{param, "print-success"}, {var, "true"}]}),
+    ok.
+
+stop_z3() ->
+    port_close(persistent_term:get(z3_connection)),
+    persistent_term:erase(z3_connection).
+
+get_z3() ->
+    Z3 = persistent_term:get(z3_connection, undefined),
+    if Z3 =:= undefined -> throw(z3_disconnected);
+       true -> ok
+    end,
+    Z3.
+
+send_z3(Query) ->
+    Z3 = get_z3(),
+    QueryStr = pp_formula(Query),
+    %% io:format("~s\n", [QueryStr]),
+    port_command(Z3, binary:list_to_bin(QueryStr ++ "\n")).
+
+check_sat() ->
+    send_z3({app, "check-sat", []}),
+    receive
+        {_, {data, {eol, Resp}}} ->
+            %% io:format("Z3: " ++ Resp ++ "\n"),
+            case string:trim(Resp) of
+                "sat"   -> true;
+                "unsat" -> false;
+                X -> throw({smt_error, X})
+            end
+    after ?TIMEOUT * 2 -> {error, timeout}
+    end.
+
+send_z3_success(Query) ->
+    send_z3(Query),
+    receive
+        {_, {data, {eol, Resp}}} ->
+            %% io:format("Z3: " ++ Resp ++ "\n"),
+            case string:trim(Resp) of
+                "success" -> success;
+                X         -> error({smt_error, X})
+            end
+    after 5000 -> {error, timeout}
+    end.
+
+assert(Form) ->
+    send_z3_success({app, "assert", [Form]}).
+
+declare_const(Var, Type) ->
+    send_z3_success({app, "declare-const", [Var, Type]}).
+
+push() ->
+    send_z3_success({app, "push", []}).
+pop() ->
+    send_z3_success({app, "pop", []}).
+scoped(Fun) ->
+    push(),
+    R = Fun(),
+    pop(),
+    R.
+
+
+pp_formula({var, Name}) -> Name;
+pp_formula({param, Name}) -> [$:, Name];
+pp_formula({int, I}) -> integer_to_list(I);
+pp_formula({app, Fun, Args}) ->
+    io_lib:format("(~s)", [pp_formulae([{var, Fun}|Args])]);
+pp_formula({list, Xs}) ->
+    io_lib:format("(~s)", [pp_formulae(Xs)]).
+
+
+pp_formulae([]) ->
+    "";
+pp_formulae([H]) ->
+    pp_formula(H);
+pp_formulae([H|T]) ->
+    io_lib:format("~s ~s", [pp_formula(H), pp_formulae(T)]).

src/aeso_syntax.erl

@@ -16,7 +16,9 @@
 -export_type([decl/0, letbind/0, typedef/0, pragma/0]).
 -export_type([arg/0, field_t/0, constructor_t/0, named_arg_t/0]).
 -export_type([type/0, constant/0, expr/0, arg_expr/0, field/1, stmt/0, alt/0, lvalue/0, elim/0, pat/0]).
+-export_type([letfun/0, letval/0, fundecl/0]).
 -export_type([ast/0]).
+-export_type([predicate/0, liquid_type/0, dep_type/1, dep_arg_t/1]).
 
 -type ast() :: [decl()].
 
@@ -72,15 +74,37 @@
 
 -type constructor_t() :: {constr_t, ann(), con(), [type()]}.
 
+
 -type type() :: {fun_t, ann(), [named_arg_t()], [type()], type()}
               | {app_t, ann(), type(), [type()]}
               | {tuple_t, ann(), [type()]}
               | {args_t, ann(), [type()]}   %% old tuple syntax, old for error messages
               | {bytes_t, ann(), integer() | any}
+              | {named_t, ann(), id(), type()}
               | id()  | qid()
               | con() | qcon()  %% contracts
               | tvar().
 
+%% Predicate for a liquid type
+-type predicate() :: [expr()].
+
+%% Dependent type
+%% FIXME it is very inconsistent with the reality...
+-type dep_type(Qual)
+    :: {refined_t, ann(), id(), type(), Qual}
+     | {dep_fun_t, ann(), [dep_arg_t(Qual)], dep_type(Qual)}
+     | {dep_record_t, ann(), type(), [dep_field_t(Qual)]}
+     | {dep_variant_t, ann(), id(), type(), Qual | undefined, [dep_constr_t(Qual)]}
+     | {dep_list_t, ann(), id(), dep_type(Qual), Qual}
+     | tvar().
+-type liquid_type() :: dep_type(predicate()).
+
+-type dep_constr_t(Qual) :: {constr_t, ann(), con(), [dep_type(Qual)]}.
+
+-type dep_arg_t(Qual) :: {dep_arg_t, ann(), id(), dep_type(Qual)}.
+
+-type dep_field_t(Qual) :: {field_t, ann(), id(), dep_type(Qual)}.
+
 -type named_arg_t() :: {named_arg_t, ann(), id(), type(), expr()}.
 
 -type constant()

src/aeso_syntax_utils.erl

@@ -153,4 +153,3 @@ used(D) ->
                (_, _)             -> #{}
             end, decl, D)),
     lists:filter(NotBound, Xs).
-

test/aeso_calldata_tests.erl

@@ -93,6 +93,7 @@ check_errors(Expect, ErrorString) ->
 %% compilable_contracts() -> [ContractName].
 %%  The currently compilable contracts.
 
+compilable_contracts() -> [];     
 compilable_contracts() ->
     [
      {"identity", "init", []},

test/aeso_compiler_tests.erl

@@ -23,6 +23,7 @@ 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() ->
@@ -141,7 +142,7 @@ compile(Backend, Name, Options) ->
 
 %% compilable_contracts() -> [ContractName].
 %%  The currently compilable contracts.
-
+compilable_contracts() -> ["hagia"];
 compilable_contracts() ->
     ["complex_types",
      "counter",
@@ -199,7 +200,6 @@ compilable_contracts() ->
      "clone",
      "clone_simple",
      "create",
-     "child_contract_init_bug",
      "test" % Custom general-purpose test file. Keep it last on the list.
     ].
 
@@ -224,7 +224,7 @@ 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,6 +910,7 @@ validation_test_() ->
         ?assertEqual(ok, validate(C, C))
       end} || C <- compilable_contracts()].
 
+validation_fails() -> [];      
 validation_fails() ->
     [{"deadcode", "nodeadcode",
       [<<"Data error:\n"

test/aeso_type_refinement_tests.erl

@@ -0,0 +1,171 @@
+%%% -*- erlang-indent-level:4; indent-tabs-mode: nil -*-
+%%%-------------------------------------------------------------------
+%%% @doc Test Sophia liquid type system.
+%%%
+%%% @end
+%%%-------------------------------------------------------------------
+
+-module(aeso_type_refinement_tests).
+
+-compile([export_all, nowarn_export_all]).
+
+-include_lib("eunit/include/eunit.hrl").
+-include("../src/aeso_ast_refine_types.hrl").
+
+-define(nu(), ?nu(?ann())).
+-define(nu_op(Op, Rel), ?op(?ann(), ?nu(), Op, Rel)).
+-define(id(V), {id, ?ann(), V}).
+-define(int(V), {int, ?ann(), V}).
+-define(unstate(T), {tuple_t, ?ann(), [T, nope, nope]}).
+
+setup() ->
+    erlang:system_flag(backtrace_depth, 100),
+    aeso_smt:start_z3(),
+    aeso_ast_refine_types:init_refiner(),
+    ok.
+
+unsetup(_) ->
+    aeso_smt:stop_z3(),
+    ok.
+
+hagia_test_() ->
+    {timeout, 100000000,
+     {inorder,
+      {foreach, local, fun setup/0, fun unsetup/1,
+       [ {timeout, 5, smt_solver_test_group()}
+       , {timeout, 1000000, refiner_test_group()}
+       ]
+      }
+     }}.
+
+smt_solver_test_group() ->
+    [ { "x == x"
+      , fun() ->
+                ?assert(aeso_ast_refine_types:impl_holds(
+                          aeso_ast_refine_types:bind_var(
+                            ?nu(), ?id("int"),
+                            aeso_ast_refine_types:init_env(aeso_ast_infer_types:init_env([]))),
+                          [],
+                          [?nu_op('==', ?nu())]))
+        end
+      }
+    ].
+
+refiner_test_group() ->
+    [ {"Testing type refinement of the " ++ ContractName ++ ".aes contract",
+       {timeout, 600,
+        fun() ->
+                try {run_refine("hagia/" ++ ContractName), Expect} of
+                    {{ok, {Env, AST}}, {success, Assertions}} ->
+                        check_ast_refinement(Env, AST, Assertions);
+                    {{error, {refinement_errors, Errs}}, {error, ExpErrors}} ->
+                        check_errors(Errs, ExpErrors);
+                    {{error, Err}, _} ->
+                        io:format(aeso_ast_refine_types:pp_error(Err)),
+                        error(Err)
+                catch E:T:S -> io:format("Caught:\n~p: ~p\nstack:\n~p\n", [E, T, S]), error(T)
+                end
+        end}} || {ContractName, Expect} <- compilable_contracts()].
+
+
+run_refine(Name) ->
+    ContractString = aeso_test_utils:read_contract(Name),
+    Ast = aeso_parser:string(ContractString, sets:new(), [{file, Name}]),
+    {TEnv, TAst, _} = aeso_ast_infer_types:infer(Ast, [return_env, dont_unfold, {file, Name}]),
+    RAst = aeso_ast_refine_types:refine_ast(TEnv, TAst),
+    RAst.
+
+check_ast_refinement(Env, AST, Assertions) ->
+    [ case maps:get({Name, FName}, Assertions, unchecked) of
+          unchecked -> ok;
+          {Scope, ExRetType} -> check_type(Env, AST, Scope, ExRetType, Type)
+      end
+     || {_, _, {con, _, Name}, Defs} <- AST,
+        {fun_decl, _, {id, _, FName}, Type} <- Defs
+    ].
+
+check_type(Env, AST, Scope, ExRet, Fun = {dep_fun_t, Ann, Args, _}) ->
+    put(refiner_errors, []),
+    Left  = {subtype, {test, 0}, ?ann(), Env, Fun, {dep_fun_t, Ann, Args, ExRet}},
+    Right = {subtype, {test, 0}, ?ann(), Env, {dep_fun_t, Ann, Args, ExRet}, Fun},
+    CS = aeso_ast_refine_types:split_constr(
+           case Scope of
+               iff -> [Left, Right];
+               sub -> [Left]
+           end),
+    aeso_ast_refine_types:solve(Env, AST, CS),
+    case get(refiner_errors) of
+        [] -> ok;
+        Errs -> throw({refinement_errors, Errs})
+    end.
+
+check_errors(Errs, ExpErrs) ->
+    ?assertEqual(length(ExpErrs), length(Errs)).
+
+compilable_contracts() ->
+    [ {"simple",
+       {success,
+        #{{"C", "f"} => {iff, ?refined(?nu(), ?int_t(?ann()), [?nu_op('==', ?int(123))])}}
+       }
+      }
+    %% , {"len",
+    %%    {success,
+    %%     #{{"C", "f"} => {iff, ?refined(?nu(), ?int_t(?ann()), [?nu_op('==', ?id("l"))])}}
+    %%    }
+    %%   }
+    %% , {"max",
+    %%    {success,
+    %%     #{{"C", "max"}  => {iff, ?refined(?nu(), ?int_t(?ann()), [?nu_op('>=', ?id("a")), ?nu_op('>=', ?id("b"))])}
+    %%     , {"C", "trim"} => {iff, ?refined(?nu(), ?int_t(?ann()), [?nu_op('>=', ?int(0)), ?nu_op('>=', ?id("x"))])}
+    %%     }
+    %%    }
+    %%   }
+    %% , {"switch",
+    %%    {success,
+    %%     #{{"C", "f"} => {iff, ?refined(?nu(), ?int_t(?ann()), [?nu_op('==', ?id("x"))])}
+    %%     , {"C", "g"} => {iff, ?refined(?nu(), ?int_t(?ann()), [?nu_op('==', ?int(2))])}
+    %%     }
+    %%    }
+    %%   }
+    %% , {"require",
+    %%    {success,
+    %%     #{{"C", "f1"} => {iff, ?refined(?nu(), ?int_t(?ann()), [?nu_op('==', ?int(0))])}
+    %%     , {"C", "f2"} => {iff, ?refined(?nu(), ?int_t(?ann()),
+    %%                               [?nu_op('=<', ?id("x")), ?nu_op('>=', ?int(0)),
+    %%                                ?nu_op('=<', ?int(1)),  ?nu_op('!=', ?op(?ann(), ?id("x"), '-', ?int(1)))
+    %%                               ])}
+    %%     }
+    %%    }
+    %%   }
+    %% , {"balance",
+    %%    {success,
+    %%     #{{"C", "f1"} => {iff, ?refined(?nu(), ?int_t(?ann()), [?nu_op('==', ?int(0))])}
+    %%     , {"C", "f2"} => {sub, ?unstate(?refined(?nu(), ?int_t(?ann()), [?nu_op('==', ?int(0))]))}
+    %%     }
+    %%    }
+    %%   }
+    %% , {"types",
+    %%    {success,
+    %%     #{{"C", "test_i"} => ?refined(?nu(), ?int_t(?ann()), [?nu_op('==', ?int(123))])
+    %%     , {"C", "test_ii"} => ?refined(?nu(), ?int_t(?ann()), [?nu_op('==', ?int(123))])
+    %%     }
+    %%    }
+    %%   }
+    %% , {"args",
+    %%    {success,
+    %%     #{{"C", "f"} => {iff, ?refined(?nu(), ?int_t(?ann()), [?nu_op('=<', ?id("n"))])}
+    %%     }
+    %%    }
+    %%   }
+    %% , {"state",
+    %%   {success,
+    %%    #{{"C", "f"} => {iff, ?unstate(?refined(?nu(), ?int_t(?ann()), [?nu_op('==', {proj, [], ?id("$init_state"), ?id("C.state.x")})]))}
+    %%    }
+    %%   }
+    %%  }
+    %% , {"failing",
+    %%    {error,
+    %%     lists:seq(1, 7)
+    %%    }
+    %%   }
+    ].

test/contracts/hagia.aes

@@ -0,0 +1,14 @@
+
+
+contract C =
+  stateful entrypoint f(a, x:int) =
+    if(a < x) a else x
+
+
+
+
+
+
+
+
+

test/contracts/hagia/args.aes

@@ -0,0 +1,8 @@
+contract C =
+  entrypoint fff() = 123
+ 
+  function
+    f : {n : int | n > 0} => {res : int | res =< n}
+    f(x) =
+      switch(x)
+        _ => 1 / x

test/contracts/hagia/balance.aes

@@ -0,0 +1,9 @@
+contract C =
+  entrypoint f1() =
+    1 / (Contract.balance + 2)
+
+  stateful entrypoint f2(a) =
+    require(Contract.balance > 11, "")
+    Chain.spend(a, 10)
+    1 / Contract.balance
+

test/contracts/hagia/failing.aes

@@ -0,0 +1,23 @@
+contract C =
+  entrypoint f() = 1 / 0
+
+  entrypoint g(x) = 1 / x
+
+  stateful entrypoint h(a, x) = Chain.spend(a, x)
+
+  entrypoint i(x) =
+    switch(x)
+      0 => 1
+
+  entrypoint j(x) =
+    switch(x)
+      _ => 1
+      _ => 2
+
+  entrypoint k(x) =
+    let 0 = x
+    x
+
+  entrypoint
+    l : () => {n : int | n > 0}
+    l() = 0

test/contracts/hagia/len.aes

@@ -0,0 +1,5 @@
+contract C =
+  entrypoint
+    len : {l : list('a)} => {r : int | r == l}
+    len([]) = 0
+    len(_::t) = len(t)

test/contracts/hagia/max.aes

@@ -0,0 +1,6 @@
+contract C =
+  entrypoint max(a : int, b : int) =
+    if(a >= b) a else b
+
+  entrypoint trim(x) =
+    max(0, x)

test/contracts/hagia/require.aes

@@ -0,0 +1,9 @@
+contract C =
+  stateful entrypoint f1(a) =
+    require(Contract.balance == 10, "xd")
+    Chain.spend(a, 10)
+    Contract.balance
+
+  entrypoint f2(x) =
+    require(x > 0, "")
+    1 / x

test/contracts/hagia/simple.aes

@@ -0,0 +1,15 @@
+include "List.aes"
+
+contract C =
+  payable stateful entrypoint split(targets : list(address)) =
+    require(targets != [], "NO_TARGETS")
+    let value_per_person = Call.value / List.length(targets)
+    spend_to_all(value_per_person, targets)
+
+  stateful function
+    spend_to_all : ({v : int | v >= 0}, list(address)) => unit
+    spend_to_all(_, []) = ()
+    spend_to_all(value, addr::rest) =
+      require(value < Contract.balance, "")
+      Chain.spend(addr, value)
+      spend_to_all(value, rest)

test/contracts/hagia/state.aes

@@ -0,0 +1,7 @@
+contract C =
+  record state = {x : int}
+
+  function inc(x) = x + 1
+  stateful entrypoint f() =
+    let s = state
+    state.x

test/contracts/hagia/switch.aes

@@ -0,0 +1,12 @@
+contract C =
+  entrypoint f(x) =
+    switch(x)
+      1 => x
+      2 => 2
+      y => (x + y) / 2
+
+  function
+    g : {n : int | n > 0 && n < 4} => {r : int | r == 2}
+    g(1) = 2
+    g(2) = 2
+    g(3) = g(1) + 0

test/contracts/hagia/test.aes

@@ -0,0 +1,8 @@
+
+include "List.aes"
+
+contract Test =
+  stateful entrypoint f(l, a) =
+    require(Contract.balance > 10, "xd")
+    Chain.spend(l, 10)
+

test/contracts/hagia/types.aes

@@ -0,0 +1,50 @@
+contract C =
+  type i('a) = 'a
+  type ii = i(int)
+  datatype iii = III(ii)
+  datatype ib = I(i(int)) | B(bool) | IB(int, bool)
+  datatype d_nest = DNest(ib)
+
+  datatype maybe('a) = Nothing | Just('a)
+
+  type maybemaybe('a) = maybe(maybe('a))
+  type maybe_int = maybe(int)
+
+  record r = {i : int, b : bool}
+  record rr = {r : r}
+
+  entrypoint
+    test_i : () => {res : int | res == 123}
+    test_i() = 123
+    
+  entrypoint
+    test_ii : (ii) => {res : int | res == 123}
+    test_ii(x) = x - x + 123
+
+  entrypoint
+    test_iii1() = III(123)
+  entrypoint
+    test_iii2 : () => {iii <: III({res : int | res > 0})}
+    test_iii2() = III(123)
+/*
+  entrypoint
+    test_ib1() = I(1)
+  entrypoint
+    test_ib2() = B(true)
+  entrypoint
+    test_ib3() = IB(123, true)
+  function
+    test_ib4 : {ib <: I({n : int | n == 0})} => {res : int | res == 1}
+    test_ib4(I(0)) = 1
+  function
+    test_ib5 : {ib <: I({n : int | n == 0})} => {res : int | res == 1}
+    test_ib5(q) = switch(q)
+     _ => 1
+  function
+    test_ib6 : bool => {ib <: IB({n : int | n == 0}, bool)}
+    test_ib6(b) = IB(0, b)
+
+  entrypoint test_maybemaybe() = Just(Nothing)
+
+  entrypoint test_maybe_int() = Nothing
+*/