Skip to content

Commit 240cf73

Browse files
committed
nil and never as variables
1 parent 1313c86 commit 240cf73

4 files changed

Lines changed: 45 additions & 17 deletions

File tree

Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ LSTSFLAGS = MALLOC_CHECK_=3
88
# recommendation: ulimit -s unlimited
99

1010
dev: install-production
11-
lm --v23 tests/promises/syntax/nil-type.lsts
11+
lm --v23 tests/promises/typechecking/nil-never-variables.lsts
1212
$(CC) $(CFLAGS) tmp.c
1313
./a.out
1414

PLUGINS/BACKEND/C/std-c-compile-expr.lsts

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ let std-c-compile-expr(ctx: FContext, t: AST, is-stmt: Bool): Fragment = (
9494
let f = mk-fragment();
9595
std-c-fragment-context = std-c-fragment-context.bind( lhs, v );
9696
ctx = ctx.bind( name, lt, v );
97-
if lt.is-t(c"Nil",0) or lt <: t1(c"C",t0(c"void")) {
97+
if lt.is-t(c"Nil",0) or lt.is-t(c"Never",0) or lt <: t1(c"C",t0(c"void")) {
9898
} else if lt <: t1(c"C",t0(c":Label")) {
9999
f = f.set(c"expression", v.get(c"expression") + SAtom(c":"));
100100
} else {
@@ -112,7 +112,7 @@ let std-c-compile-expr(ctx: FContext, t: AST, is-stmt: Bool): Fragment = (
112112
_ => (
113113
let rf = std-c-compile-expr(ctx, rhs, false);
114114
f = f.set(c"frame", f.get(c"frame") + rf.get(c"frame"));
115-
if lt.is-t(c"Nil",0) or lt <: t1(c"C",t0(c"void")) {
115+
if lt.is-t(c"Nil",0) or lt.is-t(c"Never",0) or lt <: t1(c"C",t0(c"void")) {
116116
f = f.set(c"expression", SAtom(c"({") + rf.get(c"expression") + SAtom(c";({});})"));
117117
} else {
118118
f = f.set(c"expression", SAtom(c"({")

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

Lines changed: 30 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ let std-c-finish-forced-imports(): S = (
1717
let compile-global-c-main-term = mk-eof();
1818

1919
let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
20+
let kt = typeof-term(term);
2021
std-c-force-import-clib(c"string.h");
2122
if k==c"" then ()
2223
else if k==c"div_t" then std-c-force-import-clib(c"stdlib.h")
@@ -39,13 +40,13 @@ let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
3940
else if k==c"bsearch" then std-c-force-import-clib(c"stdlib.h")
4041
else if k==c"qsort" then std-c-force-import-clib(c"stdlib.h")
4142
else if k==c"__compar_fn_t" then std-c-force-import-clib(c"stdlib.h")
42-
else if typeof-term(term).is-open or typeof-term(term).is-t(c"Blob",0) or typeof-term(term).is-t(c"FFI",0) or typeof-term(term).is-t(c"Prop",0) then ()
43+
else if kt.is-open or kt.is-t(c"Blob",0) or kt.is-t(c"FFI",0) or kt.is-t(c"Prop",0) then ()
4344
else if k==c"main" and not(non-zero(compile-global-c-main-term)) then {
4445
compile-global-c-main-term = term;
4546
} else match term {
4647
App{left:Lit{key:c":"}, right:App{left:ASTNil{}, right:AType{tt=tt}}} => (
4748
if not(tt.is-t(c"C-FFI",0)) and not(tt.is-t(c"C-Fragment",0)) {
48-
let clean-tt = typeof-term(term).weaken.without-phi;
49+
let clean-tt = kt.weaken.without-phi;
4950
k = mangle-identifier(k, clean-tt);
5051
};
5152
(let pre-decl, let post-decl) = std-c-mangle-declaration(tt, term);
@@ -55,28 +56,34 @@ let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
5556
text = text + SAtom(k);
5657
text = text + post-decl;
5758
text = text + SAtom(c";\n");
58-
if can-unify(t1(c"C",t0(c"typedef")), tt) or can-unify(t2(c"Array",t1(c"C",t0(c"typedef")),ta), tt) {
59+
if kt.is-t(c"Nil",0) or kt.is-t(c"Never",0) or kt <: t1(c"C",t0(c"void")) then ()
60+
else if can-unify(t1(c"C",t0(c"typedef")), tt) or can-unify(t2(c"Array",t1(c"C",t0(c"typedef")),ta), tt) {
5961
assemble-header-typedef-section = assemble-header-typedef-section + text;
6062
} else {
6163
assemble-gdecl-section = assemble-gdecl-section + text;
6264
}
6365
);
6466
App{left:Lit{key:c":"}, right:App{t=left, right:AType{tt=tt}}} => (
6567
if not(tt.is-t(c"C-FFI",0)) and not(tt.is-t(c"C-Fragment",0)) {
66-
let clean-tt = typeof-term(term).weaken.without-phi;
68+
let clean-tt = kt.weaken.without-phi;
6769
k = mangle-identifier(k, clean-tt);
6870
};
6971
let gend = false;
7072
if tt.is-t(c"C-Fragment",0) {
7173
match t {
7274
Lit{key=key} => (
73-
assemble-gdecl-section = assemble-gdecl-section + SAtom(key);
75+
if kt.is-t(c"Nil",0) or kt.is-t(c"Never",0) or kt <: t1(c"C",t0(c"void")) then ()
76+
else assemble-gdecl-section = assemble-gdecl-section + SAtom(key);
7477
gend = true;
7578
);
7679
_ => ();
7780
}
7881
};
79-
if not(gend) {
82+
if not(gend) and (kt.is-t(c"Nil",0) or kt.is-t(c"Never",0) or kt <: t1(c"C",t0(c"void"))) {
83+
let inner-expr = std-c-compile-expr( ctx, t, false );
84+
let text = inner-expr.get(c"expression") + SAtom(c";\n");
85+
assemble-global-initializer-section = assemble-global-initializer-section + text;
86+
} else if not(gend) {
8087
(let pre-decl, let post-decl) = std-c-mangle-declaration(tt, term);
8188
let text = SNil();
8289
text = text + pre-decl;
@@ -86,7 +93,10 @@ let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
8693
text = text + SAtom(c";\n");
8794

8895
let inner-expr = std-c-compile-expr( ctx, t, false );
89-
if can-unify(t1(c"C",t0(c"typedef")), tt) or can-unify(t2(c"Array",t1(c"C",t0(c"typedef")),ta), tt) {
96+
if kt.is-t(c"Nil",0) or kt.is-t(c"Never",0) or kt <: t1(c"C",t0(c"void")) then {
97+
text = SNil;
98+
text = SAtom(k) + SAtom(c" = ") + inner-expr.get(c"expression") + SAtom(c";\n");
99+
} else if can-unify(t1(c"C",t0(c"typedef")), tt) or can-unify(t2(c"Array",t1(c"C",t0(c"typedef")),ta), tt) {
90100
assemble-header-typedef-section = assemble-header-typedef-section + text;
91101
} else {
92102
assemble-gdecl-section = assemble-gdecl-section + text;
@@ -96,8 +106,8 @@ let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
96106
}
97107
);
98108
Abs{lhs=lhs,rhs=rhs,tt=tt} => (
99-
if k!=c"main" and not(typeof-term(term).is-t(c"C-FFI_s",0)) {
100-
k = mangle-identifier-function(k, typeof-term(term).without-phi);
109+
if k!=c"main" and not(kt.is-t(c"C-FFI_s",0)) {
110+
k = mangle-identifier-function(k, kt.without-phi);
101111
};
102112
ctx = std-c-compile-destructure-args( ctx, lhs, false );
103113
let loc = term.location;
@@ -154,8 +164,8 @@ let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
154164
};
155165
);
156166
t => (
157-
let tt = typeof-term(term);
158-
if not(typeof-term(term).is-t(c"C-FFI",0)) and not(tt.is-t(c"C-Fragment",0)) {
167+
let tt = kt;
168+
if not(kt.is-t(c"C-FFI",0)) and not(tt.is-t(c"C-Fragment",0)) {
159169
k = mangle-identifier(k, tt.without-phi);
160170
};
161171

@@ -166,11 +176,17 @@ let std-c-compile-global(ctx: FContext, k: CString, term: AST): Nil = (
166176
text = text + SAtom(k);
167177
text = text + post-decl;
168178
text = text + SAtom(c";\n");
169-
assemble-gdecl-section = assemble-gdecl-section + text;
179+
if kt.is-t(c"Nil",0) or kt.is-t(c"Never",0) or kt <: t1(c"C",t0(c"void")) then ()
180+
else assemble-gdecl-section = assemble-gdecl-section + text;
170181

171182
let inner-expr = std-c-compile-expr( ctx, t, false );
172-
text = SAtom(k) + SAtom(c" = ") + inner-expr.get(c"expression") + SAtom(c";\n");
173-
assemble-global-initializer-section = assemble-global-initializer-section + text;
183+
if kt.is-t(c"Nil",0) or kt.is-t(c"Never",0) or kt <: t1(c"C",t0(c"void")) {
184+
text = inner-expr.get(c"expression") + SAtom(c";\n");
185+
assemble-global-initializer-section = assemble-global-initializer-section + text;
186+
} else {
187+
text = SAtom(k) + SAtom(c" = ") + inner-expr.get(c"expression") + SAtom(c";\n");
188+
assemble-global-initializer-section = assemble-global-initializer-section + text;
189+
}
174190
);
175191
}
176192
);
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
2+
import lib/core/bedrock.lsts;
3+
4+
let f() = (
5+
let a = ();
6+
let b = () as Never;
7+
);
8+
9+
let a = ();
10+
let b = () : ();
11+
let c = () as Never;
12+
let d = () as Never : Never;

0 commit comments

Comments
 (0)