Skip to content

Commit e96f533

Browse files
bladyjokerbladyjoker
committed
Simplify and fix instance resolution
1 parent b8a9d2d commit e96f533

File tree

1 file changed

+103
-124
lines changed

1 file changed

+103
-124
lines changed

‎experimental/prolog/class_check.pl‎

Lines changed: 103 additions & 124 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
%% Apply and argument to a type abstraction - assumes Kind validity
55
% 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)).
6+
apply(opaque(N, kind(arr(_KL, KR)), Cd), _, opaque(N, kind(KR), Cd)).
77

88
apply(ty_ref(RefName), A, ResTy) :-
99
ty_def(RefName, Ty),
@@ -35,78 +35,52 @@
3535
subst(Ctx, TyArg, ArgRes).
3636

3737
%% Sum/Product/Rec get normalized into a canonical form Either/Prod/Void/Unit/Opaque
38-
struct_rule(class(ClassName, class_arg(_, kind(*)), _),
39-
rule(ClassName, ty_ref(unit)) :- true
40-
).
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)).
4161

42-
struct_rule(class(ClassName, class_arg(_, kind(*)), _),
43-
rule(ClassName, ty_ref(void)) :- true
44-
).
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)).
4565

46-
struct_rule(class(ClassName, class_arg(_, kind(*)), _),
47-
rule(ClassName, ty_app(ty_app(ty_ref(prod), A), B)) :-
48-
(
49-
%kind(ty_app(ty_app(ty_ref(prod), A), B), kind(*)),
50-
rule(ClassName, A),
51-
rule(ClassName, B)
52-
)
53-
).
54-
55-
struct_rule(class(ClassName, class_arg(_, kind(*)), _),
56-
rule(ClassName, ty_app(ty_app(ty_ref(either), A), B)) :-
57-
(
58-
%kind(ty_app(ty_app(ty_ref(either), A), B), kind(*)),
59-
rule(ClassName, A),
60-
rule(ClassName, B)
61-
)
62-
).
63-
64-
%% NOTE(bladjoker): Experimentals class rules on types of kind ->
66+
%% Experimental structural rules for types of kind * -> *
6567
% Haskell: Functor Deriving https://mail.haskell.org/pipermail/haskell-prime/2007-March/002137.html
66-
struct_rule(class(ClassName, class_arg(_, kind(arr(KL, KR))), _),
67-
rule(ClassName, ty_app(TL, TR)) :-
68-
(
69-
%kind(ty_app(TL, TR), kind(arr(KL, KR))),
70-
rule(ClassName, TL),
71-
apply(TL, TR, Res),
72-
rule(ClassName, Res)
73-
)
74-
).
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+
%% ).
7582

76-
struct_rule(class(ClassName, class_arg(_, Kind), _),
77-
(rule(ClassName, ty_abs(A, B)) :-
78-
(
79-
%kind(ty_abs(A, B), Kind),
80-
rule(ClassName, B)
81-
)
82-
)
83-
).
84-
85-
% Opaque stuff
86-
struct_rule(class(ClassName, class_arg(_, Kind), _),
87-
rule(ClassName, opaque(_, Kind, _)) :- true
88-
).
8983

90-
% User specifiable rules (this is what the API gets)
91-
user_rule(class(ClassName, class_arg(_, Kind), _),
92-
rule(ClassName, ty_ref(RefName)) :-
93-
(
94-
%kind(ty_ref(RefName), Kind),
95-
ty_def(RefName, Ty),
96-
rule(ClassName, Ty)
97-
)
98-
).
99-
100-
user_rule(class(ClassName, class_arg(_, Kind), _),
101-
(rule(ClassName, ty_app(F, A)) :-
102-
(
103-
%kind(ty_app(F, A), Kind),
104-
%% TODO(bladyjoker): Ask gnumonik@ if beta-reduction is what's really needed here. Imo, it is.
105-
apply(F, A, Res),
106-
rule(ClassName, Res)
107-
)
108-
)
109-
).
11084

11185
class_def(eq, class_arg(a, kind(*)), []).
11286
class_def(ord, class_arg(a, kind(*)), [eq(a)]).
@@ -120,49 +94,46 @@
12094
(
12195
struct_rule(
12296
class(CName, CArg, CSups),
123-
(rule(CName, Ty) :- RuleBody)
124-
),
125-
StructRule = (rule(CName, Ty) :- RuleBody)
97+
StructRule
98+
)
12699
),
127100
StructRules
128101
),
129102
findall(UserRule,
130103
(
131104
member(Ty, Tys),
132-
user_rule(
105+
derive_rule(
106+
Ty,
133107
class(CName, CArg, CSups),
134-
(rule(CName, Ty) :- RuleBody)
135-
),
136-
UserRule = (rule(CName, Ty) :- RuleBody)
108+
UserRule
109+
)
137110
),
138111
UserRules
139112
).
140113

141-
eval_rules(StructRules, UserRules) :-
114+
solve(StructRules, UserRules, Goal) :-
115+
Goal =.. [ClassName, Ty],
142116
append(StructRules, UserRules, Rules),
143-
member((RuleHead :- RuleBody), UserRules),
144-
print_message(informational, trying(RuleHead)),
145-
(
146-
eval_rule(Rules, [RuleHead], RuleBody) -> print_message(informational, rule_ok(RuleHead));
117+
eval_rule(Rules, [], rule(ClassName, Ty)) -> true;
147118
(
148-
print_message(error, rule_failed(RuleHead)),
119+
print_message(error, rule_failed(Goal)),
149120
fail
150-
)
151-
).
121+
).
152122

153-
eval_rule(_, Trace, true) :-
154-
print_message(informational, rules_reached_true(Trace)).
123+
eval_rule(_, _, true) :-
124+
print_message(informational, rule_true).
155125

156126
eval_rule(Rules, Trace, (RL,RR)) :-
157127
eval_rule(Rules, Trace, RL),
158128
eval_rule(Rules, Trace, RR).
159129

160130
eval_rule(Rules, Trace, rule(ClassName, Ty)) :-
161131
var(Ty) -> print_message(informational, rule_ok(rule(ClassName, Ty))), true;
162-
first(rule(ClassName, Ty), Trace) -> true;
132+
first(rule(ClassName, Ty), Trace) -> print_message(informational, rule_ok_cycle(rule(ClassName, Ty))), true;
163133
(
164134
print_message(informational, lookup(rule(ClassName, Ty))),
165-
first((rule(ClassName, Ty) :- RuleBody), Rules) -> (
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_) -> (
166137
print_message(informational, trying(rule(ClassName, Ty))),
167138
eval_rule(Rules, [rule(ClassName, Ty)|Trace], RuleBody),
168139
print_message(informational, rule_ok(rule(ClassName, Ty)))
@@ -173,62 +144,70 @@
173144
)
174145
).
175146

176-
eval_rule(_, Trace, apply(F, A, Res)) :-
177-
apply(F, A, Res) -> print_message(info, apply(F, A, Res)),true;
178-
(
179-
print_message(error, normalization_failed(Trace, F, A)),
180-
fail
181-
).
182-
183-
eval_rule(_, _, kind(Ty, kind(Kind))) :-
184-
ty_kind(Ty, Kind) -> true;
185-
(
186-
(
187-
ty_kind(Ty, Kind_) -> print_message(error, wrong_kind(Ty, got(Kind_), wanted(Kind)));
188-
print_message(error, invalid_kind(Ty))
189-
),
190-
fail
191-
).
192-
193-
eval_rule(_, _, ty_def(RefName, Ty)) :-
194-
ty_def(RefName, Ty).
195-
196147
:- multifile prolog:message//1.
197148

198149
prolog:message(wrong_kind(Ty, got(Got), wanted(Want))) --> [ '~w is of kind ~w but wanted kind ~w'-[Ty, Got, Want]].
199150
prolog:message(normalization_failed(_, Ty)) --> [ 'Normalizing ~w failed'-[Ty]].
200151
prolog:message(lookup(rule(ClassName, Ty))) --> [ 'Looking up rule ~w ~w'-[ClassName, Ty]].
201152
prolog:message(trying(rule(ClassName, Ty))) --> [ 'Trying rule ~w ~w'-[ClassName, Ty]].
202153
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'].
203156
prolog:message(missing_rule(rule(ClassName, Ty), _)) --> [ 'Missing rule ~w ~w'-[ClassName, Ty]].
204157
prolog:message(rule_failed(rule(ClassName, Ty))) --> [ 'Failed rule ~w ~w'-[ClassName, Ty]].
205158

206159
:- begin_tests(class_check).
207160

208161
test("should_succeed(derive_eq_of_int)", []) :-
209-
derive([ty_ref(int8)],eq,S,U), eval_rules(S, U).
162+
derive([ty_ref(int8)], eq, S, U),
163+
solve(S, U, eq(ty_ref(int8))).
210164

211165
test("should_succeed(derive_eq_of_maybe_int)", []) :-
212166
derive([ty_ref(int8), ty_app(ty_ref(maybe), ty_ref(int8))], eq, S, U),
213-
eval_rules(S, U).
167+
solve(S, U, eq(ty_ref(int8))),
168+
solve(S, U, eq(ty_app(ty_ref(maybe), ty_ref(int8)))).
214169

215170
test("should_succeed(derive_eq_of_maybe_a)", []) :-
216-
derive([ty_app(ty_ref(maybe), _A)], eq, S, U), eval_rules(S, U).
217-
218-
test("should_succeed(derive_functor_of_maybe)", []) :-
219-
derive([ty_ref(maybe)], functor,S,U),
220-
eval_rules(S, U).
221-
222-
test("should_succeed(derive_functor_of_either_int)", []) :-
223-
derive([ty_app(
224-
ty_ref(either),
225-
ty_ref(int8)
226-
)], functor, S, U), eval_rules(S, U).
227-
228-
test("should_fail(derive_functor_of_either)", [ fail ]) :-
229-
derive([ty_ref(either)], functor, S, U), eval_rules(S, U).
171+
derive([ty_app(ty_ref(maybe), _A)], eq, S, U),
172+
solve(S, U, eq(ty_app(ty_ref(maybe), _B))).
230173

231174
test("should_fail(derive_eq_of_foo)", [ fail ]) :-
232-
derive([ty_ref(foo)], eq, S, U), eval_rules(S, U).
175+
derive([ty_ref(foo)], eq, S, U),
176+
solve(S, U, eq(ty_ref(foo))).
177+
178+
test("should_fail(derive_eq_of_foo with 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_of_foo with 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_of_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_of_recfoo with 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_eq_of_recfoo with recbar)", [ ]) :-
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))))).
233212

234213
:- end_tests(class_check).

0 commit comments

Comments
 (0)