Skip to content

Commit 39ef8b9

Browse files
bladyjokerbladyjoker
authored
Merge pull request #60 from mlabs-haskell/bladyjoker/codegen
Codegen: Scaffolding
2 parents 57eb9aa + 7f561c9 commit 39ef8b9

File tree

37 files changed

+1255
-390
lines changed

37 files changed

+1255
-390
lines changed

‎_typos.toml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
[default.extend-words]
22
substituters = "substituters"
3+
hask= "hask"
34

45
[type.pdf]
56
extend-glob = ["*.pdf"]

‎experimental/prolog/class_check.pl‎

Lines changed: 184 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -38,30 +38,47 @@
3838
%% Structural rules for types of kind `*`
3939
struct_rule(class(ClassName, class_arg(_, kind(*)), _), Rule) :-
4040
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)) :-
41+
(goal(ClassName, opaque(_, kind(*), _)) :- true),
42+
(goal(ClassName, ty_ref(unit)) :- true),
43+
(goal(ClassName, ty_ref(void)) :- true),
44+
(goal(ClassName, ty_app(ty_app(ty_ref(prod), A), B)) :-
4545
(
46-
rule(ClassName, A),
47-
rule(ClassName, B)
46+
goal(ClassName, A),
47+
goal(ClassName, B)
4848
)),
49-
(rule(ClassName, ty_app(ty_app(ty_ref(either), A), B)) :-
49+
(goal(ClassName, ty_app(ty_app(ty_ref(either), A), B)) :-
5050
(
51-
rule(ClassName, A),
52-
rule(ClassName, B)
51+
goal(ClassName, A),
52+
goal(ClassName, B)
5353
))
5454
]).
5555

56+
conj(Goal, (Goal, Conj), Conj).
57+
58+
superclass_goal(Ty, Cl_, Conj) :-
59+
copy_term(Cl_, Cl),
60+
class(_ClassName, class_arg(Ty, _K), ClassSups) = Cl,
61+
findall(R, (
62+
member(Sup_, ClassSups),
63+
copy_term(Sup_, Sup),
64+
Sup =.. [SupName, Ty],
65+
R = goal(SupName, Ty)
66+
),
67+
Rules),
68+
foldl(conj, Rules, Conj, true).
69+
70+
5671
%% User specifiable `derive` rules (the same for any kind?)
5772
%% NOTE(bladyjoker): TyAbs can't be derived for non `*` kinds.
58-
derive_rule(ty_ref(RefName), class(ClassName, _, _), Rule) :-
73+
derive_rule(ty_ref(RefName), class(ClassName, ClassArgs, ClassSups), Rule) :-
5974
ty_def(RefName, Ty),
60-
Rule = (rule(ClassName, ty_ref(RefName)) :- rule(ClassName, Ty)).
75+
superclass_goal(ty_ref(RefName), class(ClassName, ClassArgs, ClassSups), SupGoals),
76+
Rule = (goal(ClassName, ty_ref(RefName)) :- goal(ClassName, Ty), SupGoals).
6177

62-
derive_rule(ty_app(F, A), class(ClassName, _, _), Rule) :-
78+
derive_rule(ty_app(F, A), class(ClassName, ClassArgs, ClassSups), Rule) :-
6379
apply(F, A, Res),
64-
Rule = (rule(ClassName, ty_app(F, A)) :- rule(ClassName, Res)).
80+
superclass_goal(ty_app(F, A), class(ClassName, ClassArgs, ClassSups), SupGoals),
81+
Rule = (goal(ClassName, ty_app(F, A)) :- goal(ClassName, Res), SupGoals).
6582

6683
%% Experimental structural rules for types of kind * -> *
6784
% Haskell: Functor Deriving https://mail.haskell.org/pipermail/haskell-prime/2007-March/002137.html
@@ -82,10 +99,10 @@
8299

83100

84101

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(*, *))), []).
102+
class_def(eq, class_arg(_A, kind(*)), []).
103+
class_def(ord, class_arg(A, kind(*)), [eq(A)]).
104+
class_def(json, class_arg(_A, kind(*)), []).
105+
class_def(functor, class_arg(_A, kind(arr(*, *))), []).
89106

90107

91108
derive(Tys, CName, StructRules, UserRules) :-
@@ -114,47 +131,118 @@
114131
solve(StructRules, UserRules, Goal) :-
115132
Goal =.. [ClassName, Ty],
116133
append(StructRules, UserRules, Rules),
117-
eval_rule(Rules, [], rule(ClassName, Ty)) -> true;
118-
(
119-
print_message(error, rule_failed(Goal)),
120-
fail
121-
).
134+
solve_goal(Rules, [], goal(ClassName, Ty)) ->( true;
135+
print_message(error, goal_failed(goal(ClassName, Ty))),
136+
fail
137+
).
122138

123-
eval_rule(_, _, true) :-
124-
print_message(informational, rule_true).
139+
solve_goal(_, Trace, true) :-
140+
print_message(informational, goal_true(Trace)).
125141

126-
eval_rule(Rules, Trace, (RL,RR)) :-
127-
eval_rule(Rules, Trace, RL),
128-
eval_rule(Rules, Trace, RR).
142+
solve_goal(Rules, Trace, (GL,GR)) :-
143+
solve_goal(Rules, Trace, GL),
144+
solve_goal(Rules, Trace, GR).
129145

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;
146+
solve_goal(Rules, Trace, goal(ClassName, Ty)) :-
147+
var(Ty) -> print_message(informational, goal_ok(goal(ClassName, Ty), Trace)), true;
148+
check_cycle(Trace, goal(ClassName, Ty)) -> true;
133149
(
134-
print_message(informational, lookup(rule(ClassName, Ty))),
150+
print_message(informational,
151+
lookup(goal(ClassName, Ty), Trace)
152+
),
135153
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)))
154+
first((goal(ClassName, Ty) :- RuleBody), Rules_) -> (
155+
print_message(informational,
156+
running(goal(ClassName, Ty), Trace)
157+
),
158+
solve_goal(Rules, [goal(ClassName, Ty)|Trace], RuleBody),
159+
print_message(informational,
160+
goal_ok(goal(ClassName, Ty), Trace)
161+
)
140162
);
141163
(
142-
print_message(error, missing_rule(rule(ClassName, Ty), Trace)),
164+
print_message(error, missing_rule(goal(ClassName, Ty), Trace)),
143165
fail
144166
)
145167
).
146168

169+
check_cycle(Trace, Goal) :-
170+
copy_term(Trace, Trace_), %% WARN(bladyjoker): Without this, Trace gets unified and instantiated.
171+
print_message(informational, checking_cycle(Goal, Trace)),
172+
(member(TracedGoal, Trace_), TracedGoal =@= Goal) -> print_message(informational, goal_ok_cycle(Goal, Trace)); fail.
173+
174+
147175
:- multifile prolog:message//1.
148176

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]].
177+
trace_to_indentation([], "").
178+
trace_to_indentation([_|Xs], I) :-
179+
trace_to_indentation(Xs, Is),
180+
string_concat(".", Is, I).
181+
182+
prolog:message(checking_cycle(G, Trace)) --> {
183+
trace_to_indentation(Trace, I),
184+
pretty_goal(G, PG)
185+
}, [
186+
'~w ~w Checking cycle for for goal'-[I, PG]
187+
].
188+
189+
prolog:message(lookup(G, Trace)) --> {
190+
trace_to_indentation(Trace, I),
191+
pretty_goal(G, PG)
192+
}, [
193+
'~w ~w Looking up rule for goal'-[I, PG]
194+
].
195+
prolog:message(running(G, Trace)) --> {
196+
trace_to_indentation(Trace, I),
197+
pretty_goal(G, PG)
198+
}, [
199+
'~w ~w Running goal'-[I, PG]
200+
].
201+
prolog:message(goal_ok(G, Trace)) --> {
202+
trace_to_indentation(Trace, I),
203+
pretty_goal(G, PG)
204+
}, [
205+
'~w ~w Done with goal'-[I, PG]
206+
].
207+
prolog:message(goal_ok_cycle(G, Trace)) --> {
208+
trace_to_indentation(Trace, I),
209+
pretty_goal(G, PG),
210+
pretty_trace(Trace, PTrace)
211+
}, [
212+
'~w ~w Done with goal because cycle ~w '-[I, PG, PTrace]
213+
].
214+
prolog:message(goal_true(Trace)) --> { trace_to_indentation(Trace, I) }, [ '~w Done because bottom'-[I]].
215+
prolog:message(missing_rule(G, Trace)) --> {
216+
trace_to_indentation(Trace, I),
217+
pretty_goal(G, PG)
218+
}, [
219+
'~w ~w Missing rule for goal'-[I, PG]
220+
].
221+
prolog:message(goal_failed(G)) --> {pretty_goal(G, PG)}, ['~w Failed goal'-[PG]].
222+
223+
%% Pretty represenationts
224+
%% ?- pretty_ty(ty_app(ty_app(ty_ref(either), ty_ref(int)), B), P).
225+
%% P = either(int, B).
226+
pretty_ty(TyVar, TyVar) :-
227+
var(TyVar).
228+
pretty_ty(opaque(N, _, _), P) :-
229+
atom_concat('_', N, OpaqueN),
230+
P =.. [OpaqueN].
231+
pretty_ty(ty_ref(RefName), P) :-
232+
P =.. [RefName].
233+
pretty_ty(ty_app(TyF, TyA), P) :-
234+
(var(TyF) -> PTyF = TyF; pretty_ty(TyF, PTyF)),
235+
(var(TyA) -> PTyA = TyA; pretty_ty(TyA, PTyA)),
236+
PTyF =.. [N|Args],
237+
append(Args, [PTyA], PArgs),
238+
P =.. [N|PArgs].
239+
240+
pretty_goal(goal(ClassName, Ty), P) :-
241+
pretty_ty(Ty, PTy),
242+
P =.. [ClassName, PTy].
243+
244+
pretty_trace(Trace, PTrace) :-
245+
findall(P, (member(R, Trace), pretty_goal(R, P)), PTrace).
158246

159247
:- begin_tests(class_check).
160248

@@ -203,18 +291,67 @@
203291
], eq, S, U),
204292
solve(S, U, eq(ty_ref(recfoo))).
205293

206-
test("should_succeed: derive Maybe (Maybe Int8))", [ ]) :-
294+
test("should_succeed: derive Eq Maybe (Maybe Int8))", [ ]) :-
207295
derive([
208296
ty_ref(int8),
209297
ty_app(ty_ref(maybe), _A)
210298
], eq, S, U),
211299
solve(S, U, eq(ty_app(ty_ref(maybe), ty_app(ty_ref(maybe), ty_ref(int8))))).
212300

213-
test("should_succeed: derive Maybe (Maybe a)", [ ]) :-
301+
test("should_succeed: derive Eq Maybe (Maybe a)", [ ]) :-
214302
derive([
215303
ty_ref(int8),
216304
ty_app(ty_ref(maybe), _A)
217305
], eq, S, U),
218306
solve(S, U, eq(ty_app(ty_ref(maybe), ty_app(ty_ref(maybe), _B)))).
219307

308+
test("should_fail: derive Ord (Maybe Int)", [ fail ]) :-
309+
derive([
310+
ty_app(ty_ref(maybe), _A)
311+
], ord, S, U),
312+
solve(S, U, ord(ty_app(ty_ref(maybe), ty_app(ty_ref(maybe), ty_ref(int8))))).
313+
314+
test("should_fail: derive Ord (Maybe Int)", [ fail ]) :-
315+
derive([
316+
ty_ref(int8),
317+
ty_app(ty_ref(maybe), _A)
318+
], ord, S, U),
319+
solve(S, U, ord(ty_app(ty_ref(maybe), ty_app(ty_ref(maybe), ty_ref(int8))))).
320+
321+
test("should_succeed: derive Ord (Maybe a)", [ fail ]) :-
322+
derive([
323+
ty_ref(int8)
324+
], eq, EqS, EqU),
325+
derive([
326+
ty_ref(int8),
327+
ty_app(ty_ref(maybe), __A)
328+
], ord, OrdS, OrdU),
329+
append(EqS, OrdS, S),
330+
append(EqU, OrdU, U),
331+
solve(S, U, ord(ty_app(ty_ref(maybe), ty_app(ty_ref(maybe), ty_ref(int8))))).
332+
333+
test("should_succeed: derive Ord (Maybe a)", [ ]) :-
334+
derive([
335+
ty_ref(int8),
336+
ty_app(ty_ref(maybe), _A)
337+
], eq, EqS, EqU),
338+
derive([
339+
ty_ref(int8),
340+
ty_app(ty_ref(maybe), __A)
341+
], ord, OrdS, OrdU),
342+
append(EqS, OrdS, S),
343+
append(EqU, OrdU, U),
344+
solve(S, U, ord(ty_app(ty_ref(maybe), ty_app(ty_ref(maybe), ty_ref(int8))))).
345+
346+
test("should_fails: Eq List a => Eq List a", [ ]) :-
347+
solve([
348+
(
349+
goal(eq, ty_app(ty_ref(list), A)) :-
350+
(goal(eq, ty_app(ty_ref(list), A)),true)
351+
)
352+
],
353+
[],
354+
eq(ty_app(ty_ref(list), _B))
355+
).
356+
220357
:- end_tests(class_check).

‎flake.nix‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,15 @@
101101
};
102102
frontendFlake = flakeAbstraction frontendBuild;
103103

104+
# Codegen Build
105+
codegenBuild = buildAbstraction {
106+
import-location = ./lambda-buffers-codegen/build.nix;
107+
additional = {
108+
lambda-buffers-compiler = ./lambda-buffers-compiler;
109+
};
110+
};
111+
codegenFlake = flakeAbstraction codegenBuild;
112+
104113
# Utilities
105114
renameAttrs = rnFn: pkgs.lib.attrsets.mapAttrs' (n: value: { name = rnFn n; inherit value; });
106115
in
@@ -109,7 +118,7 @@
109118
inherit pkgs;
110119

111120
# Standard flake attributes
112-
packages = { inherit (protosBuild) compilerHsPb; } // compilerFlake.packages // frontendFlake.packages // extrasFlake.packages;
121+
packages = { inherit (protosBuild) compilerHsPb; } // compilerFlake.packages // frontendFlake.packages // codegenFlake.packages // extrasFlake.packages;
113122

114123
devShells = rec {
115124
dev-pre-commit = preCommitDevShell;
@@ -118,12 +127,13 @@
118127
dev-protos = protosBuild.devShell;
119128
dev-compiler = compilerFlake.devShell;
120129
dev-frontend = frontendFlake.devShell;
130+
dev-codegen = codegenFlake.devShell;
121131
dev-common = extrasFlake.devShell;
122132
default = preCommitDevShell;
123133
};
124134

125135
# nix flake check --impure --keep-going --allow-import-from-derivation
126-
checks = { inherit pre-commit-check; } // devShells // packages // renameAttrs (n: "check-${n}") (frontendFlake.checks // compilerFlake.checks // extrasFlake.checks);
136+
checks = { inherit pre-commit-check; } // devShells // packages // renameAttrs (n: "check-${n}") (compilerFlake.checks // frontendFlake.checks // codegenFlake.checks // extrasFlake.checks);
127137

128138
}
129139
) // {

‎lambda-buffers-codegen/.envrc‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
use flake ..#dev-codegen

‎lambda-buffers-codegen/app/LambdaBuffers/Codegen/Cli/Gen.hs‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
2+
3+
module LambdaBuffers.Codegen.Cli.Gen (GenOpts (..), gen) where
4+
5+
import Control.Lens (makeLenses)
6+
7+
data GenOpts = GenOpts
8+
{ _compiled :: FilePath
9+
, _debug :: Bool
10+
, _workingDir :: Maybe FilePath
11+
}
12+
deriving stock (Eq, Show)
13+
14+
makeLenses ''GenOpts
15+
16+
-- | Generate code given some options.
17+
gen :: GenOpts -> IO ()
18+
gen _opts = error "not implemented"

0 commit comments

Comments
 (0)