Skip to content

Commit 3eb302a

Browse files
albschalbsch
committed
[erlsem] Parser, caching, proper global state, emptiness
1 parent fb98d99 commit 3eb302a

File tree

16 files changed

+1262
-0
lines changed

16 files changed

+1262
-0
lines changed

‎apps/erlsem/src/dnf/bdd.hrl‎

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
% A generic BDD parameterized over both the 'nodes and 'leafs
2+
%
3+
% hide built-in Erlang node function
4+
-compile([export_all, nowarn_export_all]).
5+
-compile({no_auto_import, [node/1]}).
6+
7+
-ifndef(ATOM).
8+
-define(ATOM, ty_bool).
9+
-endif.
10+
-ifndef(LEAF).
11+
-define(LEAF, ty_bool).
12+
-endif.
13+
14+
-type dnf() :: term(). % TODO
15+
-type bdd() ::
16+
{leaf, ?LEAF:type()}
17+
| {node, _Atom :: ?ATOM:type(), _PositiveEdge :: bdd(), _NegativeEdge :: bdd()}.
18+
19+
-spec any() -> bdd().
20+
any() -> {leaf, ?LEAF:any()}.
21+
22+
-spec empty() -> bdd().
23+
empty() -> {leaf, ?LEAF:empty()}.
24+
25+
-spec singleton(?ATOM:type()) -> bdd().
26+
singleton(Atom) -> {node, Atom, any(), empty()}.
27+
28+
-spec negated_singleton(?ATOM:type()) -> bdd().
29+
negated_singleton(Atom) -> {node, Atom, empty(), any()}.
30+
31+
-spec leaf(?LEAF:type()) -> bdd().
32+
leaf(Leaf) -> {leaf, Leaf}.
33+
34+
-spec equal(bdd(), bdd()) -> bdd().
35+
equal({node, A1, P1, N1}, {node, A2, P2, N2}) ->
36+
?ATOM:equal(A1, A2) andalso equal(P1, P2) andalso equal(N1, N2);
37+
equal({leaf, T1}, {leaf, T2}) ->
38+
?LEAF:equal(T1, T2);
39+
equal(_, _) ->
40+
false.
41+
42+
-spec compare(bdd(), bdd()) -> lt | gt | eq.
43+
compare({leaf, T1}, {leaf, T2}) -> ?LEAF:compare(T1, T2);
44+
compare({leaf, _}, {node, _, _, _}) -> lt;
45+
compare({node, _, _, _}, {leaf, _}) -> gt;
46+
compare({node, A1, P1, N1}, {node, A2, P2, N2}) ->
47+
case ?ATOM:compare(A1, A2) of
48+
eq ->
49+
case compare(P1, P2) of
50+
eq -> compare(N1, N2);
51+
Res -> Res
52+
end;
53+
Res -> Res
54+
end.
55+
56+
-spec negate(bdd()) -> bdd().
57+
negate({leaf, A}) ->
58+
{leaf, ?LEAF:negate(A)};
59+
negate({node, Atom, Pos, Neg}) ->
60+
{node, Atom, negate(Pos), negate(Neg)}.
61+
62+
63+
% simplification for BDDs
64+
% implements a simple form of structural subsumption
65+
% which is not apparant at first glance
66+
% TODO example here
67+
-spec normalize(bdd()) -> bdd().
68+
normalize(Bdd = {node, _Atom, Pos, Neg}) ->
69+
case equal(Pos, Neg) of
70+
true -> Pos;
71+
false -> Bdd
72+
end;
73+
normalize(X) -> X.
74+
75+
-spec op(fun((?LEAF:type(), ?LEAF:type()) -> ?LEAF:type()), bdd(), bdd()) -> bdd().
76+
op(LeafOperation, Bdd1, Bdd2) ->
77+
Op = fun ROp(T1, T2) ->
78+
Res =
79+
case {T1, T2} of
80+
{{leaf, L1}, {leaf, L2}} -> {leaf, LeafOperation(L1, L2)};
81+
{{leaf, L}, {node, A, P, N}} ->
82+
{node, A, ROp({leaf, L}, P), ROp({leaf, L}, N)};
83+
{{node, A, P, N}, {leaf, L}} ->
84+
{node, A, ROp(P, {leaf, L}), ROp(N, {leaf, L})};
85+
{{node, A1, P1, N1}, {node, A2, P2, N2}} ->
86+
case ?ATOM:compare(A1, A2) of
87+
lt ->
88+
{node, A1, ROp(P1, T2), ROp(N1, T2)};
89+
gt ->
90+
{node, A2, ROp(T1, P2), ROp(T1, N2)};
91+
eq ->
92+
{node, A1, ROp(P1, P2), ROp(N1, N2)}
93+
end
94+
end,
95+
normalize(Res)
96+
end,
97+
Op(Bdd1, Bdd2).
98+
99+
-spec union(bdd(), bdd()) -> bdd().
100+
union(T1, T2) ->
101+
op(fun ?LEAF:union/2, T1, T2).
102+
103+
-spec intersect(bdd(), bdd()) -> bdd().
104+
intersect(T1, T2) -> op(fun ?LEAF:intersect/2, T1, T2).
105+
106+
-spec difference(bdd(), bdd()) -> bdd().
107+
difference(T1, T2) -> op(fun ?LEAF:difference/2, T1, T2).
108+
109+
-spec dnf(bdd()) -> dnf().
110+
dnf(T) ->
111+
dnf_acc([], [], [], T).
112+
113+
-spec dnf_acc(dnf(), [?ATOM:type()], [?ATOM:type()], bdd()) -> dnf().
114+
dnf_acc(Acc, Ps, Ns, {leaf, T}) ->
115+
[{Ps, Ns, T} | Acc];
116+
dnf_acc(Acc, Ps, Ns, {node, A, P, N}) ->
117+
% TODO small heuristic add
118+
Acc0 = dnf_acc(Acc, [A | Ps], Ns, P),
119+
dnf_acc(Acc0, Ps, [A | Ns], N).
120+
121+
122+
% is_empty_union(F1, F2) ->
123+
% F1() andalso F2().
124+
125+
% get_dnf(Bdd) ->
126+
% lists:filter(
127+
% fun({_,_,[]}) -> false; ({_, _, T}) ->
128+
% case ?TERMINAL:empty() of
129+
% T -> false;
130+
% _ -> true
131+
% end
132+
% end,
133+
% dnf(Bdd, {fun(P, N, T) -> [{P, N, T}] end, fun(C1, C2) -> C1() ++ C2() end})
134+
% ).
135+
136+
% dnf(Bdd, {ProcessCoclause, CombineResults}) ->
137+
% do_dnf(Bdd, {ProcessCoclause, CombineResults}, _Pos = [], _Neg = []).
138+
139+
% do_dnf({node, Element, Left, Right}, F = {_Process, Combine}, Pos, Neg) ->
140+
% % heuristic: if Left is positive & 1, skip adding the negated Element to the right path
141+
% % TODO can use the see simplifications done in ty_rec:transform to simplify DNF before processing?
142+
% case {terminal, ?TERMINAL:any()} of
143+
% Left ->
144+
% F1 = fun() -> do_dnf(Left, F, [Element | Pos], Neg) end,
145+
% F2 = fun() -> do_dnf(Right, F, Pos, Neg) end,
146+
% Combine(F1, F2);
147+
% _ ->
148+
% F1 = fun() -> do_dnf(Left, F, [Element | Pos], Neg) end,
149+
% F2 = fun() -> do_dnf(Right, F, Pos, [Element | Neg]) end,
150+
% Combine(F1, F2)
151+
% end;
152+
% do_dnf({terminal, Terminal}, {Proc, _Comb}, Pos, Neg) ->
153+
% Proc(Pos, Neg, Terminal).
154+

‎apps/erlsem/src/dnf_ty_function.erl‎

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
-module(dnf_ty_function).
2+
3+
-compile([export_all, nowarn_export_all]).
4+
5+
-define(ATOM, ty_function).
6+
-define(LEAF, ty_bool).
7+
-define(NODE, ty_node).
8+
9+
-include("dnf/bdd.hrl").
10+
11+
12+
% -spec function(ty_function()) -> dnf_ty_function().
13+
% function(TyFunction) -> node(TyFunction).
14+
15+
leq(T1, T2) ->
16+
is_empty(difference(T1, T2)).
17+
18+
is_empty(Ty) ->
19+
Dnf = dnf(Ty),
20+
lists:all(fun is_empty_line/1, Dnf).
21+
22+
is_empty_line({AllPos, Neg, T}) ->
23+
case {AllPos, Neg, ?LEAF:empty()} of
24+
{_, _, T} -> true;
25+
{Ps, Ns, _} ->
26+
% continue searching for any arrow ∈ N such that the line becomes empty
27+
lists:any(fun(NegatedFun) -> is_empty_cont(Ps, NegatedFun) end, Ns)
28+
end.
29+
30+
is_empty_cont(Ps, NegatedFun) ->
31+
%% ∃ Ts-->T2 ∈ N s.t.
32+
%% Ts is in the domains of the function
33+
T1 = ty_function:domain(NegatedFun),
34+
35+
AllDomains = lists:map(fun ty_function:domain/1, Ps),
36+
Disj = ?NODE:disjunction(AllDomains),
37+
?NODE:leq(
38+
T1,
39+
Disj
40+
)
41+
% if so, check if output matches
42+
andalso
43+
explore_function(T1, ?NODE:negate(ty_function:codomain(NegatedFun)), Ps).
44+
45+
46+
47+
% optimized phi' (4.10) from paper covariance and contravariance
48+
% justification for this version of phi can be found in `prop_phi_function.erl`
49+
%-spec explore_function(ty_ref(), ty_ref(), [term()]) -> boolean().
50+
explore_function(_T1, _T2, []) ->
51+
true;
52+
explore_function(T1, T2, [Function | Ps]) ->
53+
{S1, S2} = {ty_function:domain(Function), ty_function:codomain(Function)},
54+
phi(T1, (?NODE:intersect(T2, S2)), Ps)
55+
andalso
56+
phi((?NODE:difference(T1, S1)), T2, Ps).
57+
58+
phi(T1, T2, []) ->
59+
?NODE:is_empty(T1) orelse ?NODE:is_empty(T2);
60+
phi(T1, T2, [Function | Ps]) ->
61+
{S1, S2} = {ty_function:domain(Function), ty_function:codomain(Function)},
62+
?NODE:is_empty(T1)
63+
orelse ?NODE:is_empty(T2)
64+
orelse (
65+
?NODE:leq(T1, S1)
66+
orelse
67+
?NODE:leq(
68+
?NODE:conjunction(lists:map(fun ty_function:codomain/1, Ps)),
69+
?NODE:negate(T2)
70+
)
71+
)
72+
andalso phi(T1, ?NODE:intersect(T2, S2), Ps)
73+
andalso phi(?NODE:difference(T1, S1), T2, Ps).
74+
75+
% TODO tally
76+
% normalize_corec(_Size, DnfTyFunction, [], [], Fixed, M) ->
77+
% dnf(DnfTyFunction, {
78+
% fun(Pos, Neg, DnfTyList) -> normalize_coclause_corec(Pos, Neg, DnfTyList, Fixed, M) end,
79+
% fun constraint_set:meet/2
80+
% })
81+
% ;
82+
% normalize_corec(Size, DnfTyFunction, PVar, NVar, Fixed, M) ->
83+
% Ty = ty_rec:function(Size, dnf_var_ty_function:function(DnfTyFunction)),
84+
% % ntlv rule
85+
% ty_variable:normalize_corec(Ty, PVar, NVar, Fixed, fun(Var) -> ty_rec:function(Size, dnf_var_ty_function:var(Var)) end, M).
86+
87+
% normalize_coclause_corec([], [], T, _Fixed, _M) ->
88+
% case ty_bool:empty() of T -> [[]]; _ -> [] end;
89+
% normalize_coclause_corec(Pos, Neg, T, Fixed, M) ->
90+
% case ty_bool:empty() of
91+
% T -> [[]];
92+
% _ ->
93+
% [First | _] = Pos ++ Neg,
94+
% Size = length(ty_function:domains(First)),
95+
% S = lists:foldl(fun ty_rec:union/2, ty_rec:empty(), [domains_to_tuple(Refs) || {ty_function, Refs, _} <- Pos]),
96+
% normalize_no_vars_corec(Size, S, Pos, Neg, Fixed, M)
97+
% end.
98+
99+
% normalize_no_vars_corec(_Size, _, _, [], _Fixed, _) -> []; % non-empty
100+
% normalize_no_vars_corec(Size, S, P, [Function | N], Fixed, M) ->
101+
% T1 = domains_to_tuple(ty_function:domains(Function)),
102+
% T2 = ty_function:codomain(Function),
103+
% %% ∃ T1-->T2 ∈ N s.t.
104+
% %% T1 is in the domain of the function
105+
% %% S is the union of all domains of the positive function intersections
106+
% X1 = ?F(ty_rec:normalize_corec(ty_rec:intersect(T1, ty_rec:negate(S)), Fixed, M)),
107+
% X2 = ?F(explore_function_norm_corec(Size, T1, ty_rec:negate(T2), P, Fixed, M)),
108+
% R1 = ?F(constraint_set:meet(X1, X2)),
109+
% %% Continue searching for another arrow ∈ N
110+
% R2 = ?F(normalize_no_vars_corec(Size, S, P, N, Fixed, M)),
111+
% constraint_set:join(R1, R2).
112+
113+
114+
% explore_function_norm_corec(_Size, BigT1, T2, [], Fixed, M) ->
115+
% NT1 = ?F(ty_rec:normalize_corec(BigT1, Fixed, M)),
116+
% NT2 = ?F(ty_rec:normalize_corec(T2, Fixed, M)),
117+
% constraint_set:join( NT1, NT2 );
118+
% explore_function_norm_corec(Size, T1, T2, [Function | P], Fixed, M) ->
119+
% NT1 = ?F(ty_rec:normalize_corec(T1, Fixed, M)),
120+
% NT2 = ?F(ty_rec:normalize_corec(T2, Fixed, M)),
121+
122+
% S1 = domains_to_tuple(ty_function:domains(Function)),
123+
% S2 = ty_function:codomain(Function),
124+
125+
% NS1 = ?F(explore_function_norm_corec(Size, T1, ty_rec:intersect(T2, S2), P, Fixed, M)),
126+
% NS2 = ?F(explore_function_norm_corec(Size, ty_rec:diff(T1, S1), T2, P, Fixed, M)),
127+
128+
% constraint_set:join(NT1,
129+
% ?F(constraint_set:join(NT2,
130+
% ?F(constraint_set:meet(NS1, NS2))))).
131+
132+
% apply_to_node(Node, Map, Memo) ->
133+
% substitute(Node, Map, Memo, fun(N, S, M) -> ty_function:substitute(N, S, M) end).

‎apps/erlsem/src/erlsem.app.src‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
{application, erlsem,
2+
[{description, "Set-theroetic types for Erlang"},
3+
{vsn, "1.0.0"},
4+
{applications,
5+
[kernel,
6+
stdlib
7+
]}
8+
]}.

‎apps/erlsem/src/global_state.erl‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
-module(global_state).
2+
3+
-compile([export_all, nowarn_export_all]).
4+
5+
-type state() :: term().
6+
7+
-callback init() -> ok.
8+
9+
-spec modules_with_global_state() -> [module()].
10+
modules_with_global_state() -> [ty_node, ty_parser].
11+
12+
-spec init() -> _.
13+
init() ->
14+
lists:foreach(fun(M) -> M:init() end, modules_with_global_state()).
15+
16+
-spec clean() -> _.
17+
clean() ->
18+
lists:foreach(fun(M) -> M:clean() end, modules_with_global_state()).
19+
20+
-spec get_state(atom()) -> state().
21+
get_state(Table) ->
22+
[{state, State}] = ets:lookup(Table, state),
23+
State.
24+
25+
-spec set_state(atom(), state()) -> ok.
26+
set_state(Table, State) ->
27+
ets:insert(Table, {state, State}).
28+
29+
30+
with_new_state(Fun) ->
31+
clean(),
32+
init(),
33+
Fun().

‎apps/erlsem/src/ty.erl‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
-module(ty).
2+
3+
-compile([export_all, nowarn_export_all]).
4+
5+
compare(A, B) -> ty_node:compare(A, B).
6+
7+
any() ->
8+
ty_node:any().
9+
10+
empty() ->
11+
ty_node:empty().
12+

‎apps/erlsem/src/ty_bool.erl‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
-module(ty_bool).
2+
3+
% only used as a simple boolean terminal node in a BDD where the leafs are 1 and 0 only.
4+
-compile([export_all, nowarn_export_all]).
5+
-export_type([type/0]).
6+
7+
-type type() :: 0 | 1.
8+
9+
compare(0, 0) -> 0; compare(1, 1) -> 0; compare(1, 0) -> 1; compare(0, 1) -> -1.
10+
equal(X, Y) -> X =:= Y.
11+
empty() -> 0.
12+
any() -> 1.
13+
union(X, Y) -> erlang:max(X, Y).
14+
intersect(X, Y) -> erlang:min(X, Y).
15+
difference(_, 1) -> 0; difference(X, _) -> X.
16+
negate(1) -> 0; negate(0) -> 1.
17+
is_any(1) -> true; is_any(_) -> false.
18+
is_empty(0) -> true; is_empty(_) -> false.
19+
substitute(_,X,_,_) -> X.
20+
% there is nothing to substitute in a ty_bool
21+
map_pi(_) -> #{}.
22+
has_ref(_,_) -> false.
23+
all_variables(_, _) -> [].
24+
raw_transform(T, Op) -> transform(T, Op).
25+
transform(0, #{empty := E}) -> E();
26+
transform(1, #{any := A}) -> A().

0 commit comments

Comments
 (0)