Skip to content

Commit

Permalink
add tests for value type subtyping
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 19, 2024
1 parent 527ca28 commit 7e73787
Show file tree
Hide file tree
Showing 2 changed files with 158 additions and 0 deletions.
1 change: 1 addition & 0 deletions src/type_system/tests.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ mod new_with_self_references;
mod permission_check;
mod subtyping;
mod type_check;
mod value_types;

/// Check what happens when we encounter a bad class name in a function parameter.
#[test]
Expand Down
157 changes: 157 additions & 0 deletions src/type_system/tests/value_types.rs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,157 @@
use crate::{dada_lang::term, type_system::check_program};
use formality_core::{test, test_util::ResultTestExt};

#[test]
#[allow(non_snake_case)]
fn pair_my_Data_my_Data_to_pair_my_Data_my_Data() {
check_program(&term(
"
class Data { }
class Main {
fn test[perm P](my self, d1: (my Data, my Data)) -> (my Data, my Data) {
d1.give;
}
}
",
))
.assert_ok(expect_test::expect!["()"]);
}

#[test]
#[allow(non_snake_case)]
fn pair_our_Data_our_Data_to_pair_my_Data_my_Data() {
check_program(&term(
"
class Data { }
class Main {
fn test[perm P](my self, d1: (our Data, our Data)) -> (my Data, my Data) {
d1.give;
}
}
",
))
.assert_err(expect_test::expect![[r#"
check program `class Data { } class Main { fn test [perm] (my self d1 : (our Data, our Data)) -> (my Data, my Data) { d1 . give ; } }`
Caused by:
0: check class named `Main`
1: check method named `test`
2: check function body
3: judgment `can_type_expr_as { expr: { d1 . give ; }, as_ty: (my Data, my Data), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "can_type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr_as { expr: { d1 . give ; }, as_ty: (my Data, my Data), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "type_expr_as" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub { a: (our Data, our Data), b: (my Data, my Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
judgment `sub_in_cx { cx_a: my, a: (our Data, our Data), cx_b: my, b: (my Data, my Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(my, (our Data, our Data))}, ty_liens_b: {NamedTy(my, (my Data, my Data))}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(my, (our Data, our Data)), ty_chain_b: NamedTy(my, (my Data, my Data)), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "value ty" failed at step #4 (src/file.rs:LL:CC) because
judgment `sub_in_cx { cx_a: my, a: our Data, cx_b: my, b: my Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(our, Data)}, ty_liens_b: {NamedTy(my, Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(our, Data), ty_chain_b: NamedTy(my, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #4 (src/file.rs:LL:CC) because
judgment had no applicable rules: `sub_lien_chains { a: our, b: my, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: (our Data, our Data)}, assumptions: {}, fresh: 0 } }`"#]]);
}

#[test]
#[allow(non_snake_case)]
fn our_pair_Data_Data_to_pair_Data_Data() {
check_program(&term(
"
class Data { }
class Main {
fn test[perm P](my self, d1: our (Data, Data)) -> (Data, Data) {
d1.give;
}
}
",
))
.assert_err(expect_test::expect![[r#"
check program `class Data { } class Main { fn test [perm] (my self d1 : our (Data, Data)) -> (Data, Data) { d1 . give ; } }`
Caused by:
0: check class named `Main`
1: check method named `test`
2: check function body
3: judgment `can_type_expr_as { expr: { d1 . give ; }, as_ty: (Data, Data), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "can_type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr_as { expr: { d1 . give ; }, as_ty: (Data, Data), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "type_expr_as" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub { a: our (Data, Data), b: (Data, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
judgment `sub_in_cx { cx_a: my, a: our (Data, Data), cx_b: my, b: (Data, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(our, (Data, Data))}, ty_liens_b: {NamedTy(my, (Data, Data))}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(our, (Data, Data)), ty_chain_b: NamedTy(my, (Data, Data)), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "value ty" failed at step #4 (src/file.rs:LL:CC) because
judgment `sub_in_cx { cx_a: our, a: Data, cx_b: my, b: Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(our, Data)}, ty_liens_b: {NamedTy(my, Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(our, Data), ty_chain_b: NamedTy(my, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #4 (src/file.rs:LL:CC) because
judgment had no applicable rules: `sub_lien_chains { a: our, b: my, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }`"#]]);
}

#[test]
#[allow(non_snake_case)]
fn our_pair_Data_Data_to_my_pair_Data_Data() {
check_program(&term(
"
class Data { }
class Main {
fn test[perm P](my self, d1: our (Data, Data)) -> my (Data, Data) {
d1.give;
}
}
",
))
.assert_err(expect_test::expect![[r#"
check program `class Data { } class Main { fn test [perm] (my self d1 : our (Data, Data)) -> my (Data, Data) { d1 . give ; } }`
Caused by:
0: check class named `Main`
1: check method named `test`
2: check function body
3: judgment `can_type_expr_as { expr: { d1 . give ; }, as_ty: my (Data, Data), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "can_type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr_as { expr: { d1 . give ; }, as_ty: my (Data, Data), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "type_expr_as" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub { a: our (Data, Data), b: my (Data, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
judgment `sub_in_cx { cx_a: my, a: our (Data, Data), cx_b: my, b: my (Data, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(our, (Data, Data))}, ty_liens_b: {NamedTy(my, (Data, Data))}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(our, (Data, Data)), ty_chain_b: NamedTy(my, (Data, Data)), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "value ty" failed at step #4 (src/file.rs:LL:CC) because
judgment `sub_in_cx { cx_a: our, a: Data, cx_b: my, b: Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(our, Data)}, ty_liens_b: {NamedTy(my, Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(our, Data), ty_chain_b: NamedTy(my, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #4 (src/file.rs:LL:CC) because
judgment had no applicable rules: `sub_lien_chains { a: our, b: my, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, d1: our (Data, Data)}, assumptions: {}, fresh: 0 } }`"#]]);
}

#[test]
#[allow(non_snake_case)]
fn my_pair_Data_Data_to_our_pair_Data_Data() {
check_program(&term(
"
class Data { }
class Main {
fn test[perm P](my self, d1: my (Data, Data)) -> our (Data, Data) {
d1.give;
}
}
",
))
.assert_ok(expect_test::expect!["()"]);
}

0 comments on commit 7e73787

Please sign in to comment.