From 7e737870966c354c1da437d71df15c6598609895 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sun, 18 Feb 2024 21:39:11 -0500 Subject: [PATCH] add tests for value type subtyping --- src/type_system/tests.rs | 1 + src/type_system/tests/value_types.rs | 157 +++++++++++++++++++++++++++ 2 files changed, 158 insertions(+) create mode 100644 src/type_system/tests/value_types.rs diff --git a/src/type_system/tests.rs b/src/type_system/tests.rs index feed859..8fb8bbe 100644 --- a/src/type_system/tests.rs +++ b/src/type_system/tests.rs @@ -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] diff --git a/src/type_system/tests/value_types.rs b/src/type_system/tests/value_types.rs new file mode 100644 index 0000000..4be3c21 --- /dev/null +++ b/src/type_system/tests/value_types.rs @@ -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!["()"]); +}