Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feature/fun #207

Merged
merged 32 commits into from
May 9, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
a69779e
unified parse_Pi & parse_Cn
leissa Apr 25, 2023
af05fa6
clang-format
leissa Apr 25, 2023
9d6441a
implemented .Fn A -> B = .Cn [A, .Cn B]
leissa Apr 26, 2023
496ffbd
clang-format
leissa Apr 26, 2023
388510e
wip: fn expr/fun decl
leissa Apr 26, 2023
503903f
clang-format
leissa Apr 26, 2023
7163d77
.fun/.fn working
leissa Apr 26, 2023
ee62e15
added assertin in llvm/insert if mem.M is involved
leissa Apr 26, 2023
75d514f
added static Pi::ret_pi
leissa Apr 26, 2023
db96abf
wip: ret expr/decl
leissa Apr 26, 2023
57aa831
clang-format
leissa Apr 26, 2023
8a1ca2a
fixed gtest lexer test
leissa Apr 26, 2023
0ac7467
docs + better parsing
leissa Apr 26, 2023
a24a37d
clang-format
leissa Apr 26, 2023
f543c58
fixed test case
leissa Apr 26, 2023
a445c1d
clang-format
leissa Apr 26, 2023
368ebcb
docs + test
leissa Apr 26, 2023
4b362c5
broken test case
leissa Apr 26, 2023
f8d5edd
Tag = Tok::Tag
leissa Apr 27, 2023
bae8d9c
clang-format
leissa Apr 27, 2023
df863fc
Merge branch 'ret_expr' into feature/fun
leissa Apr 27, 2023
8fc6d46
fixing test cases
leissa Apr 27, 2023
f1c7be8
docs + test case
leissa Apr 27, 2023
681e6da
docs
leissa Apr 27, 2023
432b825
docs + test case
leissa Apr 27, 2023
03500a3
Merge branch 'master' into feature/fun
leissa Apr 28, 2023
c5721df
Merge branch 'master' into feature/fun
leissa May 2, 2023
61075eb
migrating str.thorin
leissa May 2, 2023
c85674e
using $ as separator in a ret expr
leissa May 2, 2023
23830a9
langref.md: missing return type for .fun/.fn
leissa May 9, 2023
f116bce
fixed doc
leissa May 9, 2023
372af03
Merge branch 'master' into feature/fun
leissa May 9, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .clang-format
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ BraceWrapping:
SplitEmptyFunction: false
SplitEmptyRecord: false
SplitEmptyNamespace: false
BreakBeforeBinaryOperators: None
BreakBeforeBinaryOperators: All
BreakBeforeConceptDeclarations: true
BreakBeforeBraces: Attach
BreakBeforeInheritanceComma: false
Expand Down
5 changes: 3 additions & 2 deletions dialects/core/be/ll.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -539,13 +539,13 @@ std::string Emitter::emit_bb(BB& bb, const Def* def) {
// before emitting the index, as it might be a weird value for mem vars.
if (match<mem::M>(extract->type())) return {};

auto v_idx = emit_unsafe(index);

if (tuple->num_projs() == 2) {
if (match<mem::M>(tuple->proj(2, 0_s)->type())) return v_tup;
if (match<mem::M>(tuple->proj(2, 1_s)->type())) return v_tup;
}

// Adjust index for mem in tuple if present.
auto v_idx = match<mem::M>(tuple->proj(0)->type()) ? std::to_string(Lit::as(index) - 1) : emit_unsafe(index);
auto t_tup = convert(tuple->type());
if (Lit::isa(index)) {
assert(!v_tup.empty());
Expand All @@ -562,6 +562,7 @@ std::string Emitter::emit_bb(BB& bb, const Def* def) {
return bb.assign(name, "load {}, {}* {}.gep", t_elem, t_elem, name);
}
} else if (auto insert = def->isa<Insert>()) {
assert(!match<mem::M>(insert->tuple()->proj(0)->type()));
auto v_tuple = emit(insert->tuple());
auto v_index = emit(insert->index());
auto v_value = emit(insert->value());
Expand Down
209 changes: 132 additions & 77 deletions docs/langref.md

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion lit/clos/malloc.thorin
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
.con f [mem: %mem.M, x: I32, return: .Cn [%mem.M, I32]] = return (mem, %core.wrap.add 0 (x, 42:I32));
.con g [mem: %mem.M, x: I32, return: .Cn [%mem.M, I32]] = return (mem, 1:I32);

.con .extern main [mem: %mem.M, argc: I32, argv: %mem.Ptr («⊤:.Nat; %mem.Ptr («⊤:.Nat; .Idx 256», 0)», 0), return: .Cn [%mem.M, I32]] = {
.fun .extern main(mem: %mem.M, argc: I32, argv: %mem.Ptr («⊤:.Nat; %mem.Ptr («⊤:.Nat; .Idx 256», 0)», 0)) -> [%mem.M, I32] = {
.con h(mem: %mem.M, x: I32, return: .Cn [%mem.M, I32]) = return (mem, %core.wrap.add 0 (x, argc));

.let pb_type = .Cn [%mem.M, I32, .Cn [%mem.M, I32]];
Expand Down
38 changes: 38 additions & 0 deletions lit/clos/malloc.thorin.disabled
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
// once this works, replace old malloc.thorin with this one
// RUN: rm -f %t.ll ; \
// RUN: %thorin -p clos %s --output-ll %t.ll -o -

.plugin core;

.let I32 = .Idx 4294967296;
.lam Ptr T: * = %mem.Ptr (T, 0);

.fun f(mem: %mem.M, x: I32) -> [%mem.M, I32] = return (mem, %core.wrap.add 0 (x, 42:I32));
.fun g(mem: %mem.M, x: I32) -> [%mem.M, I32] = return (mem, 1:I32);

.fun .extern main(mem: %mem.M, argc: I32, argv: Ptr «⊤:.Nat; Ptr «⊤:.Nat; .Idx 256»») -> [%mem.M, I32] = {
.fun h(mem: %mem.M, x: I32) -> [%mem.M, I32] = return (mem, %core.wrap.add 0 (x, argc));

.let pb_type = .Fn [%mem.M, I32] -> [%mem.M, I32];
.let Tas = (pb_type, 0);
.let arr_size = ⊤:.Nat;

.let ('mem, pb_ptr) = %mem.malloc Tas (mem, 32);
.let pb_arr = %core.bitcast (Ptr «⊤:.Nat; .Fn [%mem.M, I32] -> [%mem.M, I32]») pb_ptr;
.let ('mem, a_arr) = %mem.alloc («4; I32», 0) (mem);

.let 'lea = %mem.lea (arr_size, ‹arr_size; pb_type›, 0) (pb_arr, 0:I32);
.let 'mem = %mem.store (mem, lea, f);
.let 'lea = %mem.lea (arr_size, ‹arr_size; pb_type›, 0) (pb_arr, 1:I32);
.let 'mem = %mem.store (mem, lea, g);
.let 'lea = %mem.lea (arr_size, ‹arr_size; pb_type›, 0) (pb_arr, 2:I32);
.let 'mem = %mem.store (mem, lea, h);
.let 'lea = %mem.lea (arr_size, ‹arr_size; I32›, 0) (a_arr, 0:I32);
.let 'mem = %mem.store (mem, lea, 10:I32);
.let 'lea = %mem.lea (arr_size, ‹arr_size; pb_type›, 0) (pb_arr, 2:I32);
.let ('mem, func) = %mem.load (mem, lea);
.let ('mem, val) = %mem.load (mem, lea);

.ret ('mem, x) = func : (mem, 1:I32);
return (mem, x))
};
35 changes: 35 additions & 0 deletions lit/fun.thorin
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
// RUN: rm -f %t.ll ; \
// RUN: %thorin %s -o - | FileCheck %s

.plugin core;

.let _32 = 4294967296;
.let I32 = .Idx _32;
.let I64 = .Idx 0;
.lam Ptr(T: *) -> * = %mem.Ptr (T, 0);

.fun foo(mem: %mem.M, x: I32)@(%core.icmp.e (x, 23:I32)) -> [%mem.M, I32] = return (mem, %core.wrap.add 0 (x, 1:I32));

.fun .extern main(mem: %mem.M, argc: I32, argv: Ptr (Ptr (.Idx 256))) -> [%mem.M, I32] = {
.ret (`mem, x) = foo $ (mem, 23:I32);
.ret (`mem, y) = foo $ (mem, 23:I32);
return (mem, %core.wrap.add 0 (x, y))
};

.lam f1(T: *)((x y: T), return: T -> ⊥) -> ⊥ = return x;
.con f2(T: *)((x y: T), return: .Cn T) = return x;
.fun f3(T: *) (x y: T) = return x;

.let g1 = .lm (T: *)((x y: T), return: T -> ⊥) -> ⊥ = return x;
.let g2 = .cn (T: *)((x y: T), return: .Cn T) = return x;
.let g3 = .fn (T: *) (x y: T) = return x;

.let F1 = Π [T:*][T, T][T -> ⊥] -> ⊥;
.let F2 =.Cn[T:*][T, T][.Cn T];
.let F3 =.Fn[T:*][T, T] -> T;


.let _ = .ret res = f1 .Nat $ (23, 42); res;
.let _ = f1 .Nat ((23, 42), .cn res: .Nat = res);

leissa marked this conversation as resolved.
Show resolved Hide resolved
// CHECK-DAG: return{{.*}}48
12 changes: 6 additions & 6 deletions lit/main_loop.thorin
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,9 @@
// RUN: %t ; test $? -eq 0
// RUN: %t 1 2 3 ; test $? -eq 6

.import core;
.import mem;
.plugin core;

.con .extern main(mem: %mem.M, argc: .Idx 4294967296, argv: %mem.Ptr (%mem.Ptr (.Idx 256, 0), 0), return: .Cn [%mem.M, .Idx 4294967296]) = {
.fun .extern main(mem: %mem.M, argc: .Idx 4294967296, argv: %mem.Ptr (%mem.Ptr (.Idx 256, 0), 0)) -> [%mem.M, .Idx 4294967296] = {
.con loop(mem: %mem.M, i: .Idx 4294967296, acc: .Idx 4294967296) = {
.let cond: (.Idx 2) = %core.icmp.ul (i, argc);
.con body m: %mem.M = {
Expand All @@ -20,14 +19,15 @@
loop (mem, 0:(.Idx 4294967296), 0:(.Idx 4294967296))
};

// CHECK-DAG: .con .extern main _[[mainVarId:[0-9_]+]]::[mem_[[memId:[0-9_]+]]: %mem.M, argc_[[argcId:[0-9_]+]]: .Idx 4294967296, %mem.Ptr (%mem.Ptr (.Idx 256, 0), 0), return_[[returnId:[0-9_]+]]: .Cn [%mem.M, .Idx 4294967296]]{{(@.*)?}}= {
// CHECK-DAG: loop_[[loopId:[0-9_]+]] (mem_[[memId]], 0:(.Idx 4294967296), 0:(.Idx 4294967296))

// CHECK-DAG: .con .extern main _[[mainVarId:[0-9_]+]]::[_{{[0-9]+}}::[mem_[[memId:[0-9_]+]]: %mem.M, argc_[[argcId:[0-9_]+]]: .Idx 4294967296, %mem.Ptr (%mem.Ptr (.Idx 256, 0), 0)], return_[[returnId:[0-9_]+]]: .Cn [%mem.M, .Idx 4294967296]]{{(@.*)?}}= {
// CHECK-DAG: loop_[[loopId:[0-9_]+]] ({{.*}}, 0:(.Idx 4294967296), 0:(.Idx 4294967296))

// CHECK-DAG: .con return_[[returnEtaId:[0-9_]+]] _[[returnEtaVarId:[0-9_]+]]: [%mem.M, .Idx 4294967296]{{(@.*)?}}= {
// CHECK-DAG: return_[[returnId]] _[[returnEtaVarId]]

// CHECK-DAG: .con loop_[[loopId]] _{{[0-9_]+}}::[mem_[[loopMemId:[0-9_]+]]: %mem.M, i_[[iterId:[0-9_]+]]: .Idx 4294967296, acc_[[accId:[0-9_]+]]: .Idx 4294967296]{{(@.*)?}}= {
// CHECK-DAG: _[[condId:[0-9_]+]]: .Idx 2 = %core.icmp.XygLe 4294967296 (i_[[iterId]], argc_[[argcId]]);
// CHECK-DAG: _[[condId:[0-9_]+]]: .Idx 2 = %core.icmp.XygLe 4294967296 (i_[[iterId]], {{.*}});
// CHECK-DAG: (_[[exitId:[0-9_]+]], body_[[bodyId:[0-9_]+]])#_[[condId]] mem_[[loopMemId]]

// CHECK-DAG: .con _[[exitId]] [[mExitVarId:[0-9a-z_]+]]: %mem.M{{(@.*)?}}= {
Expand Down
2 changes: 1 addition & 1 deletion lit/refly/refine.thorin
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
.let _32 = 4294967296;
.let I32 = .Idx _32;
.let I64 = .Idx 0;
.con .extern main [mem: %mem.M, argc: I32, argv: %mem.Ptr (%mem.Ptr (.Idx 256, 0), 0), return: .Cn [%mem.M, I32]] = {
.fun .extern main(mem: %mem.M, argc: I32, argv: %mem.Ptr (%mem.Ptr (.Idx 256, 0), 0)) -> [%mem.M, I32] = {
.let exp = %refly.reify <<4; .Nat>> (0, 1, 2, 3);
.let new = %refly.refine (exp, 1, %refly.reify .Nat 42);
.let tup = %refly.reflect <<4; .Nat>> new;
Expand Down
10 changes: 5 additions & 5 deletions lit/str.thorin
Original file line number Diff line number Diff line change
Expand Up @@ -8,16 +8,16 @@
.let I8 = .Idx 256;
.let I32 = .Idx 4294967296;

.con println_char[%mem.M, I8, .Cn %mem.M];
.con print_str[%mem.M, %mem.Ptr («⊤:.Nat; I8», 0), .Cn %mem.M];
.fun println_char[%mem.M, I8] -> %mem.M;
.fun print_str[%mem.M, %mem.Ptr («⊤:.Nat; I8», 0)] -> %mem.M;

.con .extern main(mem: %mem.M, argc: I32, argv: %mem.Ptr (%mem.Ptr (.Idx 256, 0), 0), return: .Cn [%mem.M, I32]) =
.let (`mem, p1) = %mem.slot («15; I8», 0) (mem, 0);
.let `mem = %mem.store (mem, p1, "Hello, World!\n\0");
.let p2 = %core.bitcast (%mem.Ptr («⊤:.Nat; I8», 0)) p1;
println_char(mem, 'x', .cn mem: %mem.M =
print_str(mem, p2, .cn mem: %mem.M =
return (mem, 0:I32)));
.ret `mem = println_char $ (mem, 'x');
.ret `mem = print_str $ (mem, p2);
return (mem, 0:I32);

// CHECK: x
// CHECK: Hello, World!
10 changes: 6 additions & 4 deletions thorin/fe/ast.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,15 @@ namespace thorin::fe {
* bind
*/

void IdPtrn::bind(Scopes& scopes, const Def* def) const { scopes.bind(dbg(), def, rebind()); }
void IdPtrn::bind(Scopes& scopes, const Def* def, bool rebind) const {
scopes.bind(dbg(), def, rebind || this->rebind());
}

void TuplePtrn::bind(Scopes& scopes, const Def* def) const {
scopes.bind(dbg(), def, rebind());
void TuplePtrn::bind(Scopes& scopes, const Def* def, bool rebind) const {
scopes.bind(dbg(), def, rebind || this->rebind());
for (size_t i = 0, e = num_ptrns(); i != e; ++i) {
auto proj = def->proj(e, i)->set(ptrn(i)->loc(), ptrn(i)->sym());
ptrn(i)->bind(scopes, proj);
ptrn(i)->bind(scopes, proj, rebind);
}
}

Expand Down
8 changes: 4 additions & 4 deletions thorin/fe/ast.h
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ class Ptrn {
Sym sym() const { return dbg_.sym; }
bool rebind() const { return rebind_; }
bool is_anonymous() const { return sym() == '_'; }
virtual void bind(Scopes&, const Def*) const = 0;
virtual const Def* type(World&, Def2Fields&) const = 0;
virtual void bind(Scopes&, const Def*, bool rebind = false) const = 0;
virtual const Def* type(World&, Def2Fields&) const = 0;

protected:
Dbg dbg_;
Expand All @@ -51,7 +51,7 @@ class IdPtrn : public Ptrn {
IdPtrn(Dbg dbg, bool rebind, const Def* type)
: Ptrn(dbg, rebind, type) {}

void bind(Scopes&, const Def*) const override;
void bind(Scopes&, const Def*, bool rebind = false) const override;
const Def* type(World&, Def2Fields&) const override;
};

Expand All @@ -66,7 +66,7 @@ class TuplePtrn : public Ptrn {
const Ptrn* ptrn(size_t i) const { return ptrns_[i].get(); }
size_t num_ptrns() const { return ptrns().size(); }

void bind(Scopes&, const Def*) const override;
void bind(Scopes&, const Def*, bool rebind = false) const override;
const Def* type(World&, Def2Fields&) const override;

private:
Expand Down
1 change: 1 addition & 0 deletions thorin/fe/lexer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,7 @@ Tok Lexer::lex() {
if (accept(U'⊤')) return tok(Tag::T_top);
if (accept(U'□')) return tok(Tag::T_box);
if (accept( ',')) return tok(Tag::T_comma);
if (accept( '$')) return tok(Tag::T_dollar);
if (accept( '#')) return tok(Tag::T_extract);
if (accept(U'λ')) return tok(Tag::T_lm);
if (accept(U'Π')) return tok(Tag::T_Pi);
Expand Down
Loading