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

Implement type inference for simple bodies #344

Merged
merged 1 commit into from
Feb 8, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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 aeneas/src/main/Version.v3
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,6 @@

// Updated by VCS scripts. DO NOT EDIT.
component Version {
def version: string = "III-9.1794";
def version: string = "III-9.1795";
var buildData: string;
}
27 changes: 19 additions & 8 deletions aeneas/src/vst/MethodEnv.v3
Original file line number Diff line number Diff line change
Expand Up @@ -1009,14 +1009,15 @@ class MethodEnv {
}
def inferMemberType(member: VstMember) -> Type {
var memberType = member.getType();
if (memberType == null) {
if (VstField.?(member)) return inferFieldType(VstField.!(member));
else return Void.ERROR_TYPE;
if (memberType != null) return memberType;
match (member) {
x: VstField => return inferFieldType(x);
x: VstMethod => return inferMethodType(x);
_ => return Void.ERROR_TYPE;
}
return memberType;
}
def inferFieldType(fdecl: VstField) -> Type {
if (fdecl.initEnv != null) return fdecl.vtype = cyclicFieldTypeInference(fdecl);
if (fdecl.initEnv != null) return fdecl.vtype = cyclicMemberTypeInference(fdecl);
var compound = fdecl.receiver, cv = compound.verifier;
var methodEnv = MethodEnv.new(compound, null, cv.newThisParam(), cv, VarEnvironment.new());
fdecl.initEnv = methodEnv;
Expand All @@ -1029,10 +1030,20 @@ class MethodEnv {
fdecl.initEnv = null;
return fdecl.vtype;
}
def cyclicFieldTypeInference(fdecl: VstField) -> Type {
def inferMethodType(mdecl: VstMethod) -> Type {
if (mdecl.initEnv != null) return mdecl.ftype = cyclicMemberTypeInference(mdecl);
var compound = mdecl.receiver, cv = compound.verifier;
var methodEnv = MethodEnv.new(compound, mdecl, cv.newThisParam(), cv, VarEnvironment.new());
mdecl.initEnv = methodEnv;
var tc = TypeChecker.new(verifier.verifier.ERROR, cv.file);
tc.enterMethod(methodEnv);
tc.typeCheckBody(mdecl.body);
return mdecl.getType();
}
def cyclicMemberTypeInference(fdecl: VstMember) -> Type {
// render a more useful error message by including the fields involved in the cycle
var compound = fdecl.receiver;
var msg = Strings.builderOf("cannot infer type of field (cycle in ");
var msg = Strings.builderOf("cannot infer type of member (cycle in ");
var list = List.new(VstMember.!(fdecl), null), p = this;
while (p != null && p.initField != null) {
list = List.new(p.initField, list);
Expand All @@ -1043,7 +1054,7 @@ class MethodEnv {
if (l.tail != null) msg.puts(" -> ");
}
msg.puts(")");
compound.verifier.errAtDecl(fdecl).FieldDeclError(msg.toString());
compound.verifier.errAtDecl(fdecl).TypeInferError(msg.toString());
return Void.ERROR_TYPE;
}
// Error message helpers
Expand Down
2 changes: 1 addition & 1 deletion aeneas/src/vst/Vst.v3
Original file line number Diff line number Diff line change
Expand Up @@ -313,6 +313,7 @@ class VstMember extends Decl {
var receiver: VstCompound;
var index: int;
var repHints: List<VstRepHint>;
var initEnv: MethodEnv;

new(isPrivate, name: Token) super(name) { }

Expand Down Expand Up @@ -422,7 +423,6 @@ class VstField extends VstMember {
var pointedAt: bool;
var vtype: Type;
var initOrder: int;
var initEnv: MethodEnv;
var enumVals: Record;

new(isPrivate: bool, writability, name: Token, tref, init, repHints: List<VstRepHint>) super(isPrivate, name) {
Expand Down
2 changes: 1 addition & 1 deletion test/core/seman/def_cyclic01.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 3:30
//@seman = TypeInferError @ 3:30
component defcyclic01a {
var a = defcyclic01b.b;
}
Expand Down
2 changes: 1 addition & 1 deletion test/core/seman/def_cyclic02.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 3:30
//@seman = TypeInferError @ 3:30
component defcyclic02a {
var a = defcyclic02b.b;
}
Expand Down
2 changes: 1 addition & 1 deletion test/core/seman/def_cyclic03.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 3:30
//@seman = TypeInferError @ 3:30
component defcyclic03a {
def a = defcyclic03b.b;
}
Expand Down
2 changes: 1 addition & 1 deletion test/core/seman/def_cyclic05.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 3:30
//@seman = TypeInferError @ 3:30
class defcyclic05a {
def a = defcyclic05b.new().b;
}
Expand Down
2 changes: 1 addition & 1 deletion test/core/seman/def_cyclic06.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 3:30
//@seman = TypeInferError @ 3:30
class defcyclic06a {
def a = defcyclic06b.new().b;
}
Expand Down
2 changes: 1 addition & 1 deletion test/core/seman/def_cyclic07.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 3:30
//@seman = TypeInferError @ 3:30
class defcyclic07a {
def a = defcyclic07b.new().b;
}
Expand Down
2 changes: 0 additions & 2 deletions test/core/seman/failures.txt
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
body_expr01.v3
body_expr07.v3
infer16.v3
inh_priv01.v3
private_override00.v3
2 changes: 1 addition & 1 deletion test/core/seman/field_init14.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 4:17
//@seman = TypeInferError @ 4:17
component C {
var h = g;
var g = h;
Expand Down
2 changes: 1 addition & 1 deletion test/core/seman/top_cylic01.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 3:9
//@seman = TypeInferError @ 3:9
var a = b;
var b = a;

1 change: 0 additions & 1 deletion test/core/seman/type_func09.v3
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
//@seman = TypeError @ 6:25

class type_func09 {
var f: void = g;
def g() -> int { return 0; }
Expand Down
2 changes: 1 addition & 1 deletion test/core/seman/var14.v3
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
//@seman = FieldDeclError @ 2:10
//@seman = TypeInferError @ 2:10
var v = v + 0;
2 changes: 1 addition & 1 deletion test/core/seman/var_cyclic01.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 4:17
//@seman = TypeInferError @ 4:17
component varcyclic01 {
var a = b;
var b = a;
Expand Down
2 changes: 1 addition & 1 deletion test/core/seman/var_cyclic04.v3
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@seman = FieldDeclError @ 5:13
//@seman = TypeInferError @ 5:13
class varcyclic04 {
var a = b;
var b = c;
Expand Down
3 changes: 3 additions & 0 deletions test/funexpr/seman/cyc_field00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman = FieldDeclError @ 2:12
def m = n;
def n = m;
3 changes: 3 additions & 0 deletions test/funexpr/seman/cyc_simple00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman = TypeInferError @ 2:12
def m() => n();
def n() => m();
2 changes: 2 additions & 0 deletions test/funexpr/seman/simple_15.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
//@seman = TypeError @ 2:31
def testm(a: Array<int>) => a[false] = 0;
3 changes: 3 additions & 0 deletions test/funexpr/seman/simple_array21.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman
var a_01: Array<void -> int> = [m, m];
def m() => 0;
10 changes: 10 additions & 0 deletions test/funexpr/seman/simple_bin02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
//@seman
class bin02 {
var f: int = 0b0;
def m(a: int) -> int {
var x: int = id(0b0);
var y = id(0b0);
return x + y + f;
}
def id<T>(x: T) => x;
}
2 changes: 1 addition & 1 deletion test/funexpr/seman/simple_body01.v3
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
//@seman = TypeError @ 2:12
//@seman = TypeInferError @ 2:12
def m() => m;
3 changes: 3 additions & 0 deletions test/funexpr/seman/simple_body09.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman
def m(a: int, b: bool) => a;
def x: int = m(0, false);
3 changes: 3 additions & 0 deletions test/funexpr/seman/simple_body10.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman = TypeError @ 3:15
def m(a: int, b: bool) => a;
def x: bool = m(1, true);
3 changes: 3 additions & 0 deletions test/funexpr/seman/simple_body11.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman
def m(a: int, b: bool) => b;
def x: bool = m(2, true);
3 changes: 3 additions & 0 deletions test/funexpr/seman/simple_body12.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman = TypeError @ 3:14
def m(a: int, b: bool) => b;
def x: int = m(33, false);
3 changes: 3 additions & 0 deletions test/funexpr/seman/simple_body13.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman
def testm(a: Array<int>) => a[0];
def x: int = testm(null);
3 changes: 3 additions & 0 deletions test/funexpr/seman/simple_body14.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman
def testm(a: Array<int>) => a[0] = 0;
def x: int = testm(null);
2 changes: 2 additions & 0 deletions test/funexpr/seman/simple_body15.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
//@seman = TypeError @ 2:36
def testm(a: Array<int>) => a[0] = false;
3 changes: 3 additions & 0 deletions test/funexpr/seman/simple_byte_op19.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman
var x: byte, y: byte;
def m() => ~x + ~y;
3 changes: 3 additions & 0 deletions test/funexpr/seman/simple_call00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
//@seman
def f() => 0;
def g: int = f();
11 changes: 11 additions & 0 deletions test/funexpr/seman/simple_clparam_sup04.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
//@seman = InvalidThisUse @ 5:23
class Self<T>(me: T) {
}
class A extends Self<A> {
new() super(this) { }
def foo() => me;
}
class B extends Self<B> {
new() super(this) { }
def foo() => me;
}
9 changes: 9 additions & 0 deletions test/funexpr/seman/simple_clparam_sup05.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
//@seman = InvalidThisUse @ 4:25
class Self<T>(me: T) {
}
class A extends Self<A>(this) {
def foo() => me;
}
class B extends Self<B>(this) {
def foo() => me;
}
17 changes: 17 additions & 0 deletions test/funexpr/seman/simple_constructor27.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
//@seman = InvalidThisUse @ 10:19
class Self<T> {
var me: T;
new(t: T) {
me = t;
}
}

class A extends Self<A> {
new() super(this) { }
def foo() => me;
}

class B extends Self<B> {
new() super(this) { }
def foo() => me;
}
11 changes: 11 additions & 0 deletions test/funexpr/seman/simple_constructor29.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
//@seman = InvalidThisUse @ 7:41
class constructor29_a {
new(i: int) { }
}
class constructor29_b extends constructor29_a {
var f: int;
new() super(constructor29.n32(this)) { }
}
component constructor29 {
def n32(o: constructor29_a) => 32;
}
7 changes: 7 additions & 0 deletions test/funexpr/seman/simple_def_mparam03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
//@seman
class C {
def m<T>(v: L<T>) => v;
def caller() { m(L<int>.new()); }
}
class L<T> {
}
5 changes: 5 additions & 0 deletions test/funexpr/seman/simple_order00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@seman
def m() => 0;
class C {
def f = m();
}
6 changes: 6 additions & 0 deletions test/funexpr/seman/simple_order01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@seman
class C {
def f = m();
def g: int;
}
def m() => C.new().g;
6 changes: 6 additions & 0 deletions test/funexpr/seman/simple_order02.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@seman
class C {
def f = m();
def g = 0;
}
def m() => C.new().g;
6 changes: 6 additions & 0 deletions test/funexpr/seman/simple_type00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@seman
type T {
def m() => this;
}
def t: T;
def u: T = t.m();
6 changes: 6 additions & 0 deletions test/funexpr/seman/simple_type01.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@seman
type T {
def m() => 99;
}
def t: T;
def u: int = t.m();
5 changes: 5 additions & 0 deletions test/funexpr/seman/simple_type_func09.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@seman = TypeError @ 6:25
class type_func09 {
var f: void = g;
def g() => 0;
}
2 changes: 2 additions & 0 deletions test/funexpr/seman/simple_void_app04.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
//@seman
def m() => void(0);