Skip to content

Commit 142b915

Browse files
andrew-johnson-4andrew-johnson-4
authored
Merge pull request #1553 from andrew-johnson-4/finish-type2-codegen-fqqsss
Github Actions is running out of memory trying to check this.
2 parents d3eac46 + b8d1ed3 commit 142b915

17 files changed

+32919
-32527
lines changed

‎BOOTSTRAP/cli.c

Lines changed: 32811 additions & 32497 deletions
Large diffs are not rendered by default.

‎Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "lambda_mountain"
3-
version = "1.21.14"
3+
version = "1.22.5"
44
authors = ["Andrew <andrew@subarctic.org>"]
55
license = "MIT"
66
description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

‎PLUGINS/BACKEND/C/compile-c-typedef.lm

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -127,16 +127,16 @@ compile-c-typedef-concrete := λ(: tctx Maybe<TContext>)(: base-type Type)(: bod
127127
)))
128128
) (
129129
(set is-cstruct-hard-compiled-index (.bind( is-cstruct-hard-compiled-index base-type 1_u64 )))
130-
(set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom 'struct\s_s)) )))
131-
(set assemble-header-section (SCons( (close assemble-header-section) (close(mangle-c-type( base-type body ))) )))
132-
(set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom '{\n_s)) )))
133-
(set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom '\tlong\sfield_0\:\n_s)) )))
130+
(set assemble-types-section (SCons( (close assemble-types-section) (close(SAtom 'struct\s_s)) )))
131+
(set assemble-types-section (SCons( (close assemble-types-section) (close(mangle-c-type( base-type body ))) )))
132+
(set assemble-types-section (SCons( (close assemble-types-section) (close(SAtom '{\n_s)) )))
133+
(set assemble-types-section (SCons( (close assemble-types-section) (close(SAtom '\tlong\sfield_0\:\n_s)) )))
134134
(if has-case (
135-
(set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom '\tunion\s{\n_s)) )))
136-
(set assemble-header-section (SCons( (close assemble-header-section) (close cases) )))
137-
(set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom '\t}\:\n_s)) )))
135+
(set assemble-types-section (SCons( (close assemble-types-section) (close(SAtom '\tunion\s{\n_s)) )))
136+
(set assemble-types-section (SCons( (close assemble-types-section) (close cases) )))
137+
(set assemble-types-section (SCons( (close assemble-types-section) (close(SAtom '\t}\:\n_s)) )))
138138
) ())
139-
(set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom '}\:\n_s)) )))
139+
(set assemble-types-section (SCons( (close assemble-types-section) (close(SAtom '}\:\n_s)) )))
140140
))
141141
))
142142
) Nil);

‎PLUGINS/BACKEND/C/compile-c.lm

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,9 @@ plugins-backend-c-compile := λ . (: (
3939
( (@( td (Typedef( _ _ )) )) (
4040
(set typedefs (+( typedefs td )))
4141
))
42+
( (@( td (Typedef2( _ )) )) (
43+
(std-c-compile-type2-typedef td)
44+
))
4245
( _ () )
4346
)))
4447
(for-each-v (td in (.unroll-seq typedefs)) (match td (

‎PLUGINS/BACKEND/C/compile-finish.lm

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@ compile-finish-c := λ. (: (
77
(let output SNil)
88
(set output (SCons( (close output) (close(std-c-finish-forced-imports())) )))
99
(set output (SCons( (close output) (close assemble-header-section) )))
10+
(set output (SCons( (close output) (close assemble-types-section) )))
11+
(set output (SCons( (close output) (close assemble-gdecl-section) )))
1012
(set output (+( output assemble-text-section )))
1113
(if (not compile-global-c-has-main) (
1214
(set output (+( output (SAtom 'int\smain\[\]{\n_s) )))

‎PLUGINS/BACKEND/C/compile-global.lm

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ compile-global-c := λ(: ctx FContext)(: k String)(: term AST). (: (
4545
(set text (SCons( (close text) (close(compile-c-function-args(ctx lhs))) )))
4646
(set text (SCons( (close text) (close(SAtom '\]\:\n_s)) )))
4747
(if (==( k 'main_s )) () (
48-
(set assemble-header-section (SCons( (close assemble-header-section) (close text) )))
48+
(set assemble-gdecl-section (SCons( (close assemble-gdecl-section) (close text) )))
4949
))
5050

5151
(set text SNil)
@@ -92,14 +92,14 @@ compile-global-c := λ(: ctx FContext)(: k String)(: term AST). (: (
9292
(set text (SCons( (close text) (close(SAtom '\]\[_s)) )))
9393
(set text (SCons( (close text) (close(mangle-c-type( domaint term ))) )))
9494
(set text (SCons( (close text) (close(SAtom '\]\:\n_s)) )))
95-
(set assemble-header-section (SCons( (close assemble-header-section) (close text) )))
95+
(set assemble-gdecl-section (SCons( (close assemble-gdecl-section) (close text) )))
9696
))
9797
( _ (
9898
(set text (SCons( (close text) (close(mangle-c-type( clean-tt term ))) )))
9999
(set text (SCons( (close text) (close(SAtom '\s_s)) )))
100100
(set text (SCons( (close text) (close(SAtom mid)) )))
101101
(set text (SCons( (close text) (close(SAtom '\:\n_s)) )))
102-
(set assemble-header-section (SCons( (close assemble-header-section) (close text) )))
102+
(set assemble-gdecl-section (SCons( (close assemble-gdecl-section) (close text) )))
103103
))
104104
))
105105

@@ -141,7 +141,7 @@ compile-global-main := λ(: ctx FContext)(: k String)(: term AST). (: (
141141
(set text (SCons( (close text) (close(SAtom '\[_s)) )))
142142
(set text (SCons( (close text) (close(compile-c-function-args(ctx lhs))) )))
143143
(set text (SCons( (close text) (close(SAtom '\]\:\n_s)) )))
144-
(set assemble-header-section (SCons( (close assemble-header-section) (close text) )))
144+
(set assemble-gdecl-section (SCons( (close assemble-gdecl-section) (close text) )))
145145

146146
(set text SNil)
147147

‎PLUGINS/BACKEND/C/index-index.lm

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,3 +42,4 @@ import PLUGINS/BACKEND/C/std-c-compile-destructure-args.lsts;
4242
import PLUGINS/BACKEND/C/escape-as-cstring.lsts;
4343
import PLUGINS/BACKEND/C/escape-string.lm;
4444
import PLUGINS/BACKEND/C/std-c-compile-push-args.lsts;
45+
import PLUGINS/BACKEND/C/std-c-compile-type2-typedef.lsts;

‎PLUGINS/BACKEND/C/std-c-compile-global.lsts

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -44,14 +44,14 @@ let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
4444
text = text + SAtom{k};
4545
text = text + post-decl;
4646
text = text + SAtom{c";\n"};
47-
assemble-header-section = assemble-header-section + text;
47+
assemble-gdecl-section = assemble-gdecl-section + text;
4848
);
4949
App{left:Lit{key:c":"}, right:App{t=left, right:AType{tt=tt}}} => (
5050
let gend = false;
5151
if tt.is-t(c"C-Fragment") {
5252
match t {
5353
Lit{key=key} => (
54-
assemble-header-section = assemble-header-section + SAtom{key};
54+
assemble-gdecl-section = assemble-gdecl-section + SAtom{key};
5555
gend = true;
5656
);
5757
_ => ();
@@ -68,7 +68,11 @@ let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
6868
let inner-expr = std-c-compile-expr( ctx, t, false );
6969
text = text + inner-expr.get(c"expression");
7070
text = text + SAtom{c";\n"};
71-
assemble-header-section = assemble-header-section + text;
71+
if can-unify(t2(c"C",t1(c"typedef")), tt) {
72+
assemble-header-section = assemble-header-section + text;
73+
} else {
74+
assemble-gdecl-section = assemble-gdecl-section + text;
75+
}
7276
}
7377
);
7478
Abs{lhs=lhs,rhs=rhs,tt=tt} => (
@@ -93,7 +97,11 @@ let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
9397
text = text + SAtom{c"("};
9498
text = text + std-c-compile-function-args(ctx, lhs);
9599
text = text + SAtom{c");\n"};
96-
assemble-header-section = assemble-header-section + text;
100+
if can-unify(t2(c"C",t1(c"typedef")), tt) {
101+
assemble-header-section = assemble-header-section + text;
102+
} else {
103+
assemble-gdecl-section = assemble-gdecl-section + text;
104+
}
97105
};
98106

99107
if initialized {

‎PLUGINS/BACKEND/C/std-c-compile-type2-typedef.lsts

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
2+
let std-c-compile-type2-typedef(td: AST): Nil = (
3+
match td { Typedef2{} => (); };
4+
let location = (td as Tag::Typedef2).location;
5+
let lhs-type = (td as Tag::Typedef2).lhs-type;
6+
let implements = (td as Tag::Typedef2).implements;
7+
let implies = (td as Tag::Typedef2).implies;
8+
let constraints = (td as Tag::Typedef2).constraints;
9+
let size = (td as Tag::Typedef2).size;
10+
let alias = (td as Tag::Typedef2).alias;
11+
let opaque-alias = (td as Tag::Typedef2).opaque-alias;
12+
let cases = (td as Tag::Typedef2).cases;
13+
14+
for concrete-type in concrete-type-instances-index.lookup(lhs-type.ground-tag-and-arity, [] :: List<Type>) {
15+
assemble-header-section = assemble-header-section + SAtom{c"typedef struct "} + mangle-c-type(concrete-type, td)
16+
+ SAtom{c" "} + mangle-c-type(concrete-type, td) + SAtom{c";\n"};
17+
};
18+
19+
for concrete-type in concrete-type-instances-index.lookup(lhs-type.ground-tag-and-arity, [] :: List<Type>) {
20+
let tctx = unify(lhs-type, concrete-type);
21+
assemble-types-section = assemble-types-section + SAtom{c"struct "} + mangle-c-type(concrete-type, td) + SAtom{c"{\n"};
22+
23+
let has-cases = false;
24+
for vector Tuple{case-tag=first, case-fields=second} in cases {
25+
if case-tag==c"" {
26+
for vector Tuple{field-name=first, field-type=second} in case-fields {
27+
field-type = substitute(tctx, field-type);
28+
(let pre-tt, let post-tt) = mangle-c-declaration(field-type, td);
29+
assemble-types-section = assemble-types-section + SAtom{c" "} + pre-tt + SAtom{c" "} + mangle-identifier(field-name) + post-tt + SAtom{c";\n"};
30+
}
31+
} else has-cases = true;
32+
};
33+
34+
if has-cases {
35+
assemble-types-section = assemble-types-section + SAtom{c"unsigned int discriminator_case_tag"} + SAtom{c";\n"};
36+
37+
assemble-types-section = assemble-types-section + SAtom{c" union {\n"};
38+
for vector Tuple{case-tag=first, case-fields=second} in cases {
39+
if case-tag!=c"" && case-fields.length > 0 {
40+
assemble-types-section = assemble-types-section + SAtom{c" struct {\n"};
41+
for vector Tuple{field-name=first, field-type=second} in case-fields {
42+
field-type = substitute(tctx, field-type);
43+
(let pre-tt, let post-tt) = mangle-c-declaration(field-type, td);
44+
assemble-types-section = assemble-types-section + SAtom{c" "} + pre-tt + SAtom{c" "} + mangle-identifier(field-name) + post-tt + SAtom{c";\n"};
45+
};
46+
assemble-types-section = assemble-types-section + SAtom{c" };\n"};
47+
};
48+
};
49+
assemble-types-section = assemble-types-section + SAtom{c" };\n"};
50+
};
51+
52+
assemble-types-section = assemble-types-section + SAtom{c"};\n"};
53+
};
54+
);

‎SRC/class-info-index.lsts

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ let add-class-info-layout(cls: Type, layout: StructLayout): Nil = (
3030
);
3131
);
3232

33-
let .is-class(cls: Type): U64 = class-info-index.has(cls.ground-tag-and-arity);
33+
let .is-class(cls: Type): U64 = class-info-index.has(cls.ground-tag-and-arity) || cls.is-type2;
3434
let .is-lm-struct(cls: Type): U64 = (
3535
let ta = cls.ground-tag-and-arity;
3636
is(class-info-index.lookup(ta, class-info-default).layout, LM1Style)

‎SRC/index-concrete-type-instances.lm

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,15 @@ add-concrete-type-instance := λ(: tt Type). (: (
77
(if (non-zero lt) (set tt lt) (set tt (.with-only-class tt)))
88
(if (non-zero tt) (match tt (
99
()
10-
( (TGround( tag LEOF )) () )
10+
( (TGround( tag LEOF )) (
11+
(if (&&( (.is-type2 tt) (not(does-concrete-type-instance-exist tt)) )) (
12+
(let k (Tuple( tag 0_u64 )))
13+
(set concrete-type-instances-index (.bind(
14+
concrete-type-instances-index k
15+
(cons( tt (.lookup( concrete-type-instances-index k (: LEOF List<Type>) )) ))
16+
)))
17+
) ())
18+
))
1119
( (TGround( tag ts )) (
1220
(if (does-concrete-type-instance-exist tt) () (
1321
(let k (Tuple( tag (.length ts) )))
@@ -25,7 +33,6 @@ does-concrete-type-instance-exist := λ(: tt Type). (: (
2533
(let r 0_u64)
2634
(match tt (
2735
()
28-
( (TGround( tag LEOF )) () )
2936
( (TGround( tag ts )) (
3037
(let k (Tuple( tag (.length ts) )))
3138
(for-each (vt in (.lookup( concrete-type-instances-index k (: LEOF List<Type>) ))) (

‎SRC/index-globals.lm

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11

22
assemble-header-section := (: SNil S);
3+
assemble-types-section := (: SNil S);
4+
assemble-gdecl-section := (: SNil S);
35
assemble-text-section := (: SNil S);
46
assemble-init-section := (: SNil S);
57
assemble-data-section := (: SNil S);

‎SRC/infer-type2-definition.lsts

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ let visit-field-template(field-name: CString, base-type: Type, field-type: Type,
2222

2323
let type2-base-type-index = {} :: HashtableEq<(CString,U64),U64>;
2424

25-
let is-type2(tt: Type): U64 = (
25+
let .is-type2(tt: Type): U64 = (
2626
let gta = normalize(tt).ground-tag-and-arity;
2727
type2-base-type-index.has(gta)
2828
);
@@ -101,7 +101,7 @@ let infer-type2-yield-constructor(base-type: Type, case-tag: CString, case-numbe
101101

102102
let return-id = uuid();
103103

104-
let body = mk-lit(c"{").ascript(t1(c"L"));
104+
let body = mk-lit(c"({").ascript(t1(c"L"));
105105
body = mk-cons(body, mk-app(mk-var(c"mangle-pre"),mk-atype(t2(c"Type",base-type))) );
106106
body = mk-cons(body, mk-lit(c" ").ascript(t1(c"L")));
107107
body = mk-cons(body, mk-lit(return-id).ascript(t1(c"L")));
@@ -125,7 +125,7 @@ let infer-type2-yield-constructor(base-type: Type, case-tag: CString, case-numbe
125125
};
126126

127127
body = mk-cons(body, mk-lit(return-id).ascript(t1(c"L")));
128-
body = mk-cons(body, mk-lit(c";}").ascript(t1(c"L")));
128+
body = mk-cons(body, mk-lit(c";})").ascript(t1(c"L")));
129129

130130
let constructor = mk-glb( mk-token(case-tag).with-location(blame.location), mk-abs(args, body.ascript(base-type), t1(c"Blob")) );
131131
infer-global-context(constructor);

‎SRC/std-infer-expr.lsts

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ let std-infer-expr(tctx: Maybe<TContext>, term: AST, is-scoped: Bool, used: IsUs
183183
};
184184
};
185185

186-
if not(is-macro) && not(is-cons) && typeof(l).is-arrow && (non-zero(var-name-if-var(l)) || is-type2(typeof(term))) {
186+
if not(is-macro) && not(is-cons) && typeof(l).is-arrow && (non-zero(var-name-if-var(l)) || typeof(term).is-type2) {
187187
mark-var-to-def-todo(tctx, var-name-if-var(l), typeof(r), l);
188188
apply-global-callable(var-name-if-var(l),typeof(r),term);
189189
};

‎nano/lsts.nanorc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ syntax lsts "\.lsts$"
55
magic "LSTS "
66
comment "#"
77

8-
color green "[;,\t\n ]\<(let|match|if|then|else|while|for|set|type|fn)\>"
8+
color green "[;,\t\n(){} ]\<(let|match|if|then|else|while|for|set|type|fn)\>"
99
color cyan ""[^"]*""
1010

1111
color blue "#.*"

‎tests/unit/type-inference.lsts.skip

Whitespace-only changes.

‎tests/unit/typedefs.lsts

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,12 +15,13 @@ let f(p1: F<c,d>, p2: A): A = p2;
1515
type2 F<c,d> implements E;
1616

1717
type2 TT<a,b> = { a: a, b: b };
18-
type2 G = { a: A, b: B, h: H };
19-
type2 H = { g: TT<A,A> } H1 { g2: A } | H2 { g3: B };
18+
type2 G = { a: I64, b: I32, h: H[] };
19+
type2 H = { g: TT<U64,U64> } H1 { g2: I64 } | H2 { g3: U32 };
2020
type2 I = { i: U64 } I1 { j: U64 };
2121

2222
let t1 = TT{ 1, 2 };
23-
let t2 = I1{ 1, 2 };
23+
let t2 = I1{ 3, 4 };
24+
25+
print("TT a=\{t1.a}, b=\{t1.b}\n");
26+
print("I a=\{t2.i}, b=\{(t2 as Tag::I1).j}\n");
2427

25-
# TODO constructor / instantiate
26-
# TODO field get/set/get indirect/set indirect

0 commit comments

Comments
 (0)