Skip to content

Commit 9c84c83

Browse files
cstmlcstml
authored
Merge pull request #30 from mlabs-haskell/bladyjoker/compiler-class-check
Compiler: Prolog model
2 parents 22dbabe + 41d8e02 commit 9c84c83

File tree

13 files changed

+2031
-31
lines changed

13 files changed

+2031
-31
lines changed

‎experimental/kind_check.pl

Lines changed: 0 additions & 31 deletions
This file was deleted.

‎experimental/prolog/cardinality_check.pl

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
:- module(cardinality_check, [first/2, wrap/3, ty_var/1, ty_lam/3]).
2+
3+
:- use_module(library(yall)).
4+
:- use_module(library(apply)).
5+
:- use_module(library(lambda)).
6+
:- use_module(library(clpfd)).
7+
8+
9+
10+
ty_var(VarName) :- member(VarName, [a, b, c]).
11+
12+
% Maybe a = Just a | Nothing = a + 1
13+
% Maybe Void = Just Void | Nothing = 0 + 1 = 1
14+
% Maybe Unit = Just Unit | Nothing = 1 + 1 = 2
15+
% Maybe Bool = Just Bool | Nothing = 2 + 1 = 3
16+
% Maybe Tern = Just Tern | Nothing = 3 + 1 = 4
17+
% Either a b = Left a | Right b = a + b
18+
% Tuple a b = Tuple a b = a * b
19+
% 2 -> 3 == 3^2
20+
21+
% Foo a = A a Int (Maybe a) (Maybe Int) | B a
22+
23+
first(X, [H|_]) :-
24+
X = H.
25+
first(X, [H|Xs]) :-
26+
X \= H,
27+
first(X, Xs).
28+
29+
:- dynamic state/2.
30+
31+
ty_lam(Ctx, opaque(kind(K), cardinality(Card)), Lam_) :-
32+
cardinality_lam(Ctx, Card, Lam),
33+
wrap(K, Lam, Lam_).
34+
35+
ty_lam(ctx(Vars), ty_ref(RefName), CLam) :-
36+
% state(RefName, Lam) -> true;
37+
ty_def(RefName, Ty),
38+
ty_lam(ctx(Vars), Ty, Lam),
39+
duplicate_term(Lam, CLam),
40+
assertz(state(RefName, Lam)).
41+
42+
ty_lam(ctx(Vars), ty_var(VarName), Var) :-
43+
ty_var(VarName),
44+
first(VarName-Var, Vars).
45+
46+
ty_lam(ctx(Vars),ty_abs(VarName, TyBody), (LamArg-LamBody)) :-
47+
LamArg #>= 0,
48+
ty_lam(ctx([VarName-LamArg|Vars]), TyBody, LamBody).
49+
50+
ty_lam(Ctx, ty_app(TyF, TyArg), LamBody) :-
51+
ty_lam(Ctx, TyArg, LamArg),
52+
ty_lam(Ctx, TyF, (LamArg-LamBody)).
53+
54+
cardinality_lam(ctx(Vars), ty_card(ty_var(VarName)), Lam) :-
55+
writeln(a-Vars),
56+
first(VarName-Lam, Vars).
57+
58+
cardinality_lam(_, k(Cd), Cd).
59+
60+
cardinality_lam(Ctx, L*R, Cd) :-
61+
cardinality_lam(Ctx, L, CdL),
62+
cardinality_lam(Ctx, R, CdR),
63+
Cd #= CdL * CdR.
64+
65+
cardinality_lam(Ctx, L+R, Cd) :-
66+
cardinality_lam(Ctx, L, CdL),
67+
cardinality_lam(Ctx, R, CdR),
68+
Cd #= CdL + CdR.
69+
70+
wrap(0, V, V).
71+
wrap(N, V, (_-B)) :-
72+
N \= 0,
73+
N_ is N - 1,
74+
wrap(N_, V, B).
75+
76+
77+
foo(list(A), B).
78+
foo(A, list(B)).

‎experimental/prolog/class_check.pl

Lines changed: 220 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,220 @@
1+
:- use_module(common_defs).
2+
:- use_module(kind_check).
3+
4+
%% Apply and argument to a type abstraction - assumes Kind validity
5+
% Beta-reduction Apply an argument to a type abstraction - assumes Kind validity
6+
apply(opaque(N, kind(arr(_KL, KR)), Cd), _, opaque(N, kind(KR), Cd)).
7+
8+
apply(ty_ref(RefName), A, ResTy) :-
9+
ty_def(RefName, Ty),
10+
apply(Ty, A, ResTy).
11+
12+
apply(ty_app(L, R), A, Res) :-
13+
apply(L, R, ResApp),
14+
apply(ResApp, A, Res).
15+
16+
apply(ty_abs(ArgName-_, Body), A, Res) :-
17+
subst(ctx(ArgName-A, []), Body, Res).
18+
19+
subst(ctx(VarName-A, Args), ty_var(VarName), Res) :-
20+
first(VarName, Args) -> Res = ty_var(VarName);
21+
Res = A.
22+
23+
subst(ctx(ArgName-_, _), ty_var(VarName), ty_var(VarName)) :-
24+
ArgName \= VarName.
25+
26+
subst(_, opaque(N, K, Cd), opaque(N, K, Cd)).
27+
28+
subst(_, ty_ref(RefName), ty_ref(RefName)).
29+
30+
subst(ctx(Arg, Args), ty_abs(ArgName-KArg, Body), ty_abs(ArgName-KArg, Res)) :-
31+
subst(ctx(Arg, [ArgName|Args]), Body, Res).
32+
33+
subst(Ctx, ty_app(TyAbs, TyArg), ty_app(AbsRes, ArgRes)) :-
34+
subst(Ctx, TyAbs, AbsRes),
35+
subst(Ctx, TyArg, ArgRes).
36+
37+
%% Sum/Product/Rec get normalized into a canonical form Either/Prod/Void/Unit/Opaque
38+
%% Structural rules for types of kind `*`
39+
struct_rule(class(ClassName, class_arg(_, kind(*)), _), Rule) :-
40+
member(Rule, [
41+
(rule(ClassName, opaque(_, kind(*), _)) :- true),
42+
(rule(ClassName, ty_ref(unit)) :- true),
43+
(rule(ClassName, ty_ref(void)) :- true),
44+
(rule(ClassName, ty_app(ty_app(ty_ref(prod), A), B)) :-
45+
(
46+
rule(ClassName, A),
47+
rule(ClassName, B)
48+
)),
49+
(rule(ClassName, ty_app(ty_app(ty_ref(either), A), B)) :-
50+
(
51+
rule(ClassName, A),
52+
rule(ClassName, B)
53+
))
54+
]).
55+
56+
%% User specifiable `derive` rules (the same for any kind?)
57+
%% NOTE(bladyjoker): TyAbs can't be derived for non `*` kinds.
58+
derive_rule(ty_ref(RefName), class(ClassName, _, _), Rule) :-
59+
ty_def(RefName, Ty),
60+
Rule = (rule(ClassName, ty_ref(RefName)) :- rule(ClassName, Ty)).
61+
62+
derive_rule(ty_app(F, A), class(ClassName, _, _), Rule) :-
63+
apply(F, A, Res),
64+
Rule = (rule(ClassName, ty_app(F, A)) :- rule(ClassName, Res)).
65+
66+
%% Experimental structural rules for types of kind * -> *
67+
% Haskell: Functor Deriving https://mail.haskell.org/pipermail/haskell-prime/2007-March/002137.html
68+
%% struct_rule(class(ClassName, class_arg(_, kind(arr(_KL, _KR))), _), Rule) :-
69+
%% member(Rule, [
70+
%% (rule(ClassName, ty_app(TL, TR)) :-
71+
%% (
72+
%% rule(ClassName, TL),
73+
%% apply(TL, TR, Res),
74+
%% rule(ClassName, Res)
75+
%% )),
76+
%% (rule(ClassName, ty_abs(_A, B)) :-
77+
%% (
78+
%% rule(ClassName, B)
79+
%% ))
80+
%% ]
81+
%% ).
82+
83+
84+
85+
class_def(eq, class_arg(a, kind(*)), []).
86+
class_def(ord, class_arg(a, kind(*)), [eq(a)]).
87+
class_def(json, class_arg(a, kind(*)), []).
88+
class_def(functor, class_arg(a, kind(arr(*, *))), []).
89+
90+
91+
derive(Tys, CName, StructRules, UserRules) :-
92+
class_def(CName, CArg, CSups),
93+
findall(StructRule,
94+
(
95+
struct_rule(
96+
class(CName, CArg, CSups),
97+
StructRule
98+
)
99+
),
100+
StructRules
101+
),
102+
findall(UserRule,
103+
(
104+
member(Ty, Tys),
105+
derive_rule(
106+
Ty,
107+
class(CName, CArg, CSups),
108+
UserRule
109+
)
110+
),
111+
UserRules
112+
).
113+
114+
solve(StructRules, UserRules, Goal) :-
115+
Goal =.. [ClassName, Ty],
116+
append(StructRules, UserRules, Rules),
117+
eval_rule(Rules, [], rule(ClassName, Ty)) -> true;
118+
(
119+
print_message(error, rule_failed(Goal)),
120+
fail
121+
).
122+
123+
eval_rule(_, _, true) :-
124+
print_message(informational, rule_true).
125+
126+
eval_rule(Rules, Trace, (RL,RR)) :-
127+
eval_rule(Rules, Trace, RL),
128+
eval_rule(Rules, Trace, RR).
129+
130+
eval_rule(Rules, Trace, rule(ClassName, Ty)) :-
131+
var(Ty) -> print_message(informational, rule_ok(rule(ClassName, Ty))), true;
132+
first(rule(ClassName, Ty), Trace) -> print_message(informational, rule_ok_cycle(rule(ClassName, Ty))), true;
133+
(
134+
print_message(informational, lookup(rule(ClassName, Ty))),
135+
copy_term(Rules, Rules_), %% WARN(bladyjoker): Without this, Rules get unified and instantiated leading to a cycle and just wrong.
136+
first((rule(ClassName, Ty) :- RuleBody), Rules_) -> (
137+
print_message(informational, trying(rule(ClassName, Ty))),
138+
eval_rule(Rules, [rule(ClassName, Ty)|Trace], RuleBody),
139+
print_message(informational, rule_ok(rule(ClassName, Ty)))
140+
);
141+
(
142+
print_message(error, missing_rule(rule(ClassName, Ty), Trace)),
143+
fail
144+
)
145+
).
146+
147+
:- multifile prolog:message//1.
148+
149+
prolog:message(wrong_kind(Ty, got(Got), wanted(Want))) --> [ '~w is of kind ~w but wanted kind ~w'-[Ty, Got, Want]].
150+
prolog:message(normalization_failed(_, Ty)) --> [ 'Normalizing ~w failed'-[Ty]].
151+
prolog:message(lookup(rule(ClassName, Ty))) --> [ 'Looking up rule ~w ~w'-[ClassName, Ty]].
152+
prolog:message(trying(rule(ClassName, Ty))) --> [ 'Trying rule ~w ~w'-[ClassName, Ty]].
153+
prolog:message(rule_ok(rule(ClassName, Ty))) --> [ 'Done with rule ~w ~w'-[ClassName, Ty]].
154+
prolog:message(rule_ok_cycle(rule(ClassName, Ty))) --> [ 'Done with rule because cycle ~w ~w'-[ClassName, Ty]].
155+
prolog:message(rule_true) --> [ 'Done because bottom'].
156+
prolog:message(missing_rule(rule(ClassName, Ty), _)) --> [ 'Missing rule ~w ~w'-[ClassName, Ty]].
157+
prolog:message(rule_failed(rule(ClassName, Ty))) --> [ 'Failed rule ~w ~w'-[ClassName, Ty]].
158+
159+
:- begin_tests(class_check).
160+
161+
test("should_succeed: derive Eq Int)", []) :-
162+
derive([ty_ref(int8)], eq, S, U),
163+
solve(S, U, eq(ty_ref(int8))).
164+
165+
test("should_succeed: derive Eq Maybe Int8)", []) :-
166+
derive([ty_ref(int8), ty_app(ty_ref(maybe), ty_ref(int8))], eq, S, U),
167+
solve(S, U, eq(ty_ref(int8))),
168+
solve(S, U, eq(ty_app(ty_ref(maybe), ty_ref(int8)))).
169+
170+
test("should_succeed: derive Eq (Maybe a))", []) :-
171+
derive([ty_app(ty_ref(maybe), _A)], eq, S, U),
172+
solve(S, U, eq(ty_app(ty_ref(maybe), _B))).
173+
174+
test("should_fail(derive Eq Foo)", [ fail ]) :-
175+
derive([ty_ref(foo)], eq, S, U),
176+
solve(S, U, eq(ty_ref(foo))).
177+
178+
test("should_fail(derive Eq Foo; derive Eq Int8)", [ fail ]) :-
179+
derive([ty_ref(int8), ty_ref(foo)], eq, S, U),
180+
solve(S, U, eq(ty_ref(int8))),
181+
solve(S, U, eq(ty_ref(foo))).
182+
183+
test("should_succeed: derive Eq Foo; derive Eq Int8)", [ ]) :-
184+
derive([
185+
ty_ref(int8),
186+
ty_ref(foo),
187+
ty_app(ty_ref(maybe), _A)
188+
], eq, S, U),
189+
solve(S, U, eq(ty_ref(int8))),
190+
solve(S, U, eq(ty_ref(foo))),
191+
solve(S, U, eq(ty_app(ty_ref(maybe), _B))).
192+
193+
test("should_fail: derive Eq Recfoo", [ fail ]) :-
194+
derive([
195+
ty_ref(recfoo)
196+
], eq, S, U),
197+
solve(S, U, eq(ty_ref(recfoo))).
198+
199+
test("should_succeed: derive Eq Recfoo, Eq Recbar)", [ ]) :-
200+
derive([
201+
ty_ref(recfoo),
202+
ty_ref(recbar)
203+
], eq, S, U),
204+
solve(S, U, eq(ty_ref(recfoo))).
205+
206+
test("should_succeed: derive Maybe (Maybe Int8))", [ ]) :-
207+
derive([
208+
ty_ref(int8),
209+
ty_app(ty_ref(maybe), _A)
210+
], eq, S, U),
211+
solve(S, U, eq(ty_app(ty_ref(maybe), ty_app(ty_ref(maybe), ty_ref(int8))))).
212+
213+
test("should_succeed: derive Maybe (Maybe a)", [ ]) :-
214+
derive([
215+
ty_ref(int8),
216+
ty_app(ty_ref(maybe), _A)
217+
], eq, S, U),
218+
solve(S, U, eq(ty_app(ty_ref(maybe), ty_app(ty_ref(maybe), _B)))).
219+
220+
:- end_tests(class_check).

0 commit comments

Comments
 (0)