From 056ea5b555344aba97ba14b698e2559360a54e05 Mon Sep 17 00:00:00 2001 From: zerbina <100542850+zerbina@users.noreply.github.com> Date: Sun, 6 Apr 2025 22:13:39 +0000 Subject: [PATCH] tests: add tests for inductive data types The current set is missing some error cases. --- tests/expr/t15_inductive_types_1.test | 9 +++++++++ tests/expr/t15_inductive_types_10_error.test | 16 ++++++++++++++++ tests/expr/t15_inductive_types_11.test | 18 ++++++++++++++++++ tests/expr/t15_inductive_types_12.test | 17 +++++++++++++++++ tests/expr/t15_inductive_types_13.test | 16 ++++++++++++++++ tests/expr/t15_inductive_types_14.test | 17 +++++++++++++++++ tests/expr/t15_inductive_types_15_error.test | 16 ++++++++++++++++ tests/expr/t15_inductive_types_16_error.test | 16 ++++++++++++++++ tests/expr/t15_inductive_types_17_error.test | 7 +++++++ tests/expr/t15_inductive_types_2_error.test | 8 ++++++++ tests/expr/t15_inductive_types_3_error.test | 12 ++++++++++++ tests/expr/t15_inductive_types_4.test | 9 +++++++++ tests/expr/t15_inductive_types_5.test | 9 +++++++++ tests/expr/t15_inductive_types_6.test | 15 +++++++++++++++ tests/expr/t15_inductive_types_7.test | 8 ++++++++ tests/expr/t15_inductive_types_8.test | 16 ++++++++++++++++ tests/expr/t15_inductive_types_9_error.test | 15 +++++++++++++++ ...uctive_types_destructure_arity_1_error.test | 11 +++++++++++ ...uctive_types_destructure_arity_2_error.test | 11 +++++++++++ ...e_types_destructure_unique_names_error.test | 11 +++++++++++ ...ctive_types_no_duplicate_names_1_error.test | 6 ++++++ ...ctive_types_no_duplicate_names_2_error.test | 6 ++++++ ...ctive_types_no_duplicate_names_3_error.test | 6 ++++++ ...ctive_types_no_duplicate_names_4_error.test | 6 ++++++ ...ctive_types_no_duplicate_names_5_error.test | 6 ++++++ 25 files changed, 287 insertions(+) create mode 100644 tests/expr/t15_inductive_types_1.test create mode 100644 tests/expr/t15_inductive_types_10_error.test create mode 100644 tests/expr/t15_inductive_types_11.test create mode 100644 tests/expr/t15_inductive_types_12.test create mode 100644 tests/expr/t15_inductive_types_13.test create mode 100644 tests/expr/t15_inductive_types_14.test create mode 100644 tests/expr/t15_inductive_types_15_error.test create mode 100644 tests/expr/t15_inductive_types_16_error.test create mode 100644 tests/expr/t15_inductive_types_17_error.test create mode 100644 tests/expr/t15_inductive_types_2_error.test create mode 100644 tests/expr/t15_inductive_types_3_error.test create mode 100644 tests/expr/t15_inductive_types_4.test create mode 100644 tests/expr/t15_inductive_types_5.test create mode 100644 tests/expr/t15_inductive_types_6.test create mode 100644 tests/expr/t15_inductive_types_7.test create mode 100644 tests/expr/t15_inductive_types_8.test create mode 100644 tests/expr/t15_inductive_types_9_error.test create mode 100644 tests/expr/t15_inductive_types_destructure_arity_1_error.test create mode 100644 tests/expr/t15_inductive_types_destructure_arity_2_error.test create mode 100644 tests/expr/t15_inductive_types_destructure_unique_names_error.test create mode 100644 tests/expr/t15_inductive_types_no_duplicate_names_1_error.test create mode 100644 tests/expr/t15_inductive_types_no_duplicate_names_2_error.test create mode 100644 tests/expr/t15_inductive_types_no_duplicate_names_3_error.test create mode 100644 tests/expr/t15_inductive_types_no_duplicate_names_4_error.test create mode 100644 tests/expr/t15_inductive_types_no_duplicate_names_5_error.test diff --git a/tests/expr/t15_inductive_types_1.test b/tests/expr/t15_inductive_types_1.test new file mode 100644 index 00000000..f9b37796 --- /dev/null +++ b/tests/expr/t15_inductive_types_1.test @@ -0,0 +1,9 @@ +discard """ + description: "Nullary constructors represent values" + output: "val : typ +""" +(Module + (DataTypeDecl typ + (Constr val)) + (ProcDecl test typ (Params) + val)) diff --git a/tests/expr/t15_inductive_types_10_error.test b/tests/expr/t15_inductive_types_10_error.test new file mode 100644 index 00000000..ab601671 --- /dev/null +++ b/tests/expr/t15_inductive_types_10_error.test @@ -0,0 +1,16 @@ +discard """ + description: " + Inductive data types are nominal types: two data types with an identical + structure are not equal in the type system. + " + reject: true +""" +(Module + (DataTypeDecl typ1 + (Constr a) + (Constr b)) + (DataTypeDecl typ2 + (Constr a) + (Constr b)) + (ProcDecl test typ2 (Params) + a)) diff --git a/tests/expr/t15_inductive_types_11.test b/tests/expr/t15_inductive_types_11.test new file mode 100644 index 00000000..00e5b5b6 --- /dev/null +++ b/tests/expr/t15_inductive_types_11.test @@ -0,0 +1,18 @@ +discard """ + description: " + Inductive data type values are destructured via `Match`. A rule must be + present for each constructor. Nullary constructors use `(Constr ...)` + for matching. + " + output: "1 : (IntTy)" +""" +(Module + (DataTypeDecl typ + (Constr a) + (Constr b)) + (ProcDecl test (IntTy) (Params) + (Exprs + (Decl x a) + (Match x + (Rule (Constr a) 1) + (Rule (Constr b) 2))))) diff --git a/tests/expr/t15_inductive_types_12.test b/tests/expr/t15_inductive_types_12.test new file mode 100644 index 00000000..01922b52 --- /dev/null +++ b/tests/expr/t15_inductive_types_12.test @@ -0,0 +1,17 @@ +discard """ + description: " + The return type of n-ary constructors is usable as a pattern, matching + all values for the constructor. + " + output: "1 : (IntTy)" +""" +(Module + (DataTypeDecl typ + (Constr a (IntTy)) + (Constr b (IntTy))) + (ProcDecl test (IntTy) (Params) + (Exprs + (Decl x (Call a 100)) + (Match x + (Rule a 1) + (Rule b 2))))) diff --git a/tests/expr/t15_inductive_types_13.test b/tests/expr/t15_inductive_types_13.test new file mode 100644 index 00000000..268221dc --- /dev/null +++ b/tests/expr/t15_inductive_types_13.test @@ -0,0 +1,16 @@ +discard """ + description: " + The `Constr` pattern is used for destructuring a constructed value. + " + output: "100 : (IntTy)" +""" +(Module + (DataTypeDecl typ + (Constr a (IntTy)) + (Constr b (IntTy))) + (ProcDecl test (IntTy) (Params) + (Exprs + (Decl x (Call a 100)) + (Match x + (Rule (Constr a val) val) + (Rule (Constr b val) 0))))) diff --git a/tests/expr/t15_inductive_types_14.test b/tests/expr/t15_inductive_types_14.test new file mode 100644 index 00000000..d0b155c8 --- /dev/null +++ b/tests/expr/t15_inductive_types_14.test @@ -0,0 +1,17 @@ +discard """ + description: " + The `As` pattern syntax is used for binding whole data type subtypes to + identifiers. + " + output: "(Constr a 100) : (IntTy)" +""" +(Module + (DataTypeDecl typ + (Constr a (IntTy)) + (Constr b (IntTy))) + (ProcDecl test (IntTy) (Params) + (Exprs + (Decl x (Call a 100)) + (Match x + (Rule (As y a) y) + (Rule (As y b) y))))) diff --git a/tests/expr/t15_inductive_types_15_error.test b/tests/expr/t15_inductive_types_15_error.test new file mode 100644 index 00000000..2f6a52d2 --- /dev/null +++ b/tests/expr/t15_inductive_types_15_error.test @@ -0,0 +1,16 @@ +discard """ + description: "`As` patterns don't introduce variables" + reject: true +""" +(Module + (DataTypeDecl typ + (Constr a (IntTy)) + (Constr b (IntTy))) + (ProcDecl test (IntTy) (Params) + (Exprs + (Decl x (Call a 100)) + (Match x + (Rule (As y a) + (Asgn y (Call a 1))) + (Rule (As y b) + (Asgn y (Call b 1))))))) diff --git a/tests/expr/t15_inductive_types_16_error.test b/tests/expr/t15_inductive_types_16_error.test new file mode 100644 index 00000000..9bc7b3b0 --- /dev/null +++ b/tests/expr/t15_inductive_types_16_error.test @@ -0,0 +1,16 @@ +discard """ + description: "`Constr` patterns don't introduce variables" + reject: true +""" +(Module + (DataTypeDecl typ + (Constr a (IntTy)) + (Constr b (IntTy))) + (ProcDecl test (IntTy) (Params) + (Exprs + (Decl x (Call a 100)) + (Match x + (Rule (Constr a val) + (Asgn val 1)) + (Rule (Constr b val) + (Asgn val 1)))))) diff --git a/tests/expr/t15_inductive_types_17_error.test b/tests/expr/t15_inductive_types_17_error.test new file mode 100644 index 00000000..041618e3 --- /dev/null +++ b/tests/expr/t15_inductive_types_17_error.test @@ -0,0 +1,7 @@ +discard """ + description: "Data types cannot be recursive" + reject: true +""" +(DataTypeDecl typ + (Constr a) + (Constr b typ)) diff --git a/tests/expr/t15_inductive_types_2_error.test b/tests/expr/t15_inductive_types_2_error.test new file mode 100644 index 00000000..b652c721 --- /dev/null +++ b/tests/expr/t15_inductive_types_2_error.test @@ -0,0 +1,8 @@ +discard """ + description: "Nullary constructors don't introduce a type" + reject: true +""" +(Module + (DataTypeDecl typ + (Constr val)) + (TypeDecl test val)) diff --git a/tests/expr/t15_inductive_types_3_error.test b/tests/expr/t15_inductive_types_3_error.test new file mode 100644 index 00000000..29223ec3 --- /dev/null +++ b/tests/expr/t15_inductive_types_3_error.test @@ -0,0 +1,12 @@ +discard """ + description: " + Unary constructors are functions, with a signature derived from the + constructors shape. + " + reject: true +""" +(Module + (DataTypeDecl typ + (Constr val (IntTy))) + (ProcDecl test val (Params) + (Call val 1))) diff --git a/tests/expr/t15_inductive_types_4.test b/tests/expr/t15_inductive_types_4.test new file mode 100644 index 00000000..22b89fc1 --- /dev/null +++ b/tests/expr/t15_inductive_types_4.test @@ -0,0 +1,9 @@ +discard """ + description: "Non-nullary constructors are functions" + output: "(proc ...) : (ProcTy unary (IntTy))" +""" +(Module + (DataTypeDecl typ + (Constr unary (IntTy))) + (ProcDecl test (ProcTy unary (IntTy)) (Params) + unary)) diff --git a/tests/expr/t15_inductive_types_5.test b/tests/expr/t15_inductive_types_5.test new file mode 100644 index 00000000..d5a962f0 --- /dev/null +++ b/tests/expr/t15_inductive_types_5.test @@ -0,0 +1,9 @@ +discard """ + description: "Non-nullary constructors are functions" + output: "(proc ...) : (ProcTy binary (IntTy) (FloatTy))" +""" +(Module + (DataTypeDecl typ + (Constr binary (IntTy) (FloatTy))) + (ProcDecl test (ProcTy val (IntTy) (FloatTy)) (Params) + val)) diff --git a/tests/expr/t15_inductive_types_6.test b/tests/expr/t15_inductive_types_6.test new file mode 100644 index 00000000..0d605fe4 --- /dev/null +++ b/tests/expr/t15_inductive_types_6.test @@ -0,0 +1,15 @@ +discard """ + description: " + A non-nullary constructor declaration also introduces a type of the same + name; it's the return type of the constructor and a subtype of the data + type the constructor belongs to. + " + output: "(Call val 1 1.5) : typ" +""" +(Module + (DataTypeDecl typ + (Constr val (IntTy) (FloatTy))) + (ProcDecl cons val (Params) + (Call val 1 1.5)) + (ProcDecl test typ (Params) + (Call cons))) diff --git a/tests/expr/t15_inductive_types_7.test b/tests/expr/t15_inductive_types_7.test new file mode 100644 index 00000000..0d0019dc --- /dev/null +++ b/tests/expr/t15_inductive_types_7.test @@ -0,0 +1,8 @@ +discard """ + description: "Data types may have more than one constructor" + arguments: "c" +""" +(DataTypeDecl typ + (Constr nullary) + (Constr unary (IntTy)) + (Constr binary (IntTy) (FloatTy))) diff --git a/tests/expr/t15_inductive_types_8.test b/tests/expr/t15_inductive_types_8.test new file mode 100644 index 00000000..41894794 --- /dev/null +++ b/tests/expr/t15_inductive_types_8.test @@ -0,0 +1,16 @@ +discard """ + description: " + When inferring the type of a decl, the full data type is preferred over + a subtype (subject to change). + " + output: "b : typ" +""" +(Module + (DataTypeDecl typ + (Constr a) + (Constr b)) + (ProcDecl test typ (Params) + (Exprs + (Decl x a) + (Asgn x b) + x))) diff --git a/tests/expr/t15_inductive_types_9_error.test b/tests/expr/t15_inductive_types_9_error.test new file mode 100644 index 00000000..304aadeb --- /dev/null +++ b/tests/expr/t15_inductive_types_9_error.test @@ -0,0 +1,15 @@ +discard """ + description: " + The immediate subtypes of a data type share their ancestor type, but + they're not directly related. + " + reject: true +""" +(Module + (DataTypeDecl typ + (Constr a (IntTy)) + (Constr b (IntTy))) + (ProcDecl receive (UnitTy) (Params (ParamDecl x a)) + (Return)) + (ProcDecl test (UnitTy) (Params) + (Call receive (Call b 1)))) diff --git a/tests/expr/t15_inductive_types_destructure_arity_1_error.test b/tests/expr/t15_inductive_types_destructure_arity_1_error.test new file mode 100644 index 00000000..602560d4 --- /dev/null +++ b/tests/expr/t15_inductive_types_destructure_arity_1_error.test @@ -0,0 +1,11 @@ +discard """ + reject: true +""" +(Module + (DataTypeDecl typ + (Constr a (IntTy) (IntTy))) + (ProcDecl test (IntTy) (Params) + (Exprs + (Decl x (Call a 100 100)) + (Match x + (Rule (Constr a val) val))))) diff --git a/tests/expr/t15_inductive_types_destructure_arity_2_error.test b/tests/expr/t15_inductive_types_destructure_arity_2_error.test new file mode 100644 index 00000000..6aac661f --- /dev/null +++ b/tests/expr/t15_inductive_types_destructure_arity_2_error.test @@ -0,0 +1,11 @@ +discard """ + reject: true +""" +(Module + (DataTypeDecl typ + (Constr a (IntTy) (IntTy))) + (ProcDecl test (IntTy) (Params) + (Exprs + (Decl x (Call a 100 100)) + (Match x + (Rule (Constr a i1 i2 i3) val))))) diff --git a/tests/expr/t15_inductive_types_destructure_unique_names_error.test b/tests/expr/t15_inductive_types_destructure_unique_names_error.test new file mode 100644 index 00000000..5219e804 --- /dev/null +++ b/tests/expr/t15_inductive_types_destructure_unique_names_error.test @@ -0,0 +1,11 @@ +discard """ + reject: true +""" +(Module + (DataTypeDecl typ + (Constr a (IntTy) (IntTy))) + (ProcDecl test (IntTy) (Params) + (Exprs + (Decl x (Call a 100 100)) + (Match x + (Rule (Constr a val val) val))))) diff --git a/tests/expr/t15_inductive_types_no_duplicate_names_1_error.test b/tests/expr/t15_inductive_types_no_duplicate_names_1_error.test new file mode 100644 index 00000000..2031787e --- /dev/null +++ b/tests/expr/t15_inductive_types_no_duplicate_names_1_error.test @@ -0,0 +1,6 @@ +discard """ + reject: true +""" +(DataTypeDecl typ + (Constr val) + (Constr val)) diff --git a/tests/expr/t15_inductive_types_no_duplicate_names_2_error.test b/tests/expr/t15_inductive_types_no_duplicate_names_2_error.test new file mode 100644 index 00000000..e4e511af --- /dev/null +++ b/tests/expr/t15_inductive_types_no_duplicate_names_2_error.test @@ -0,0 +1,6 @@ +discard """ + reject: true +""" +(DataTypeDecl typ + (Constr val) + (Constr val (IntTy))) diff --git a/tests/expr/t15_inductive_types_no_duplicate_names_3_error.test b/tests/expr/t15_inductive_types_no_duplicate_names_3_error.test new file mode 100644 index 00000000..0f8a28ff --- /dev/null +++ b/tests/expr/t15_inductive_types_no_duplicate_names_3_error.test @@ -0,0 +1,6 @@ +discard """ + reject: true +""" +(DataTypeDecl typ + (Constr val (IntTy)) + (Constr val (IntTy))) diff --git a/tests/expr/t15_inductive_types_no_duplicate_names_4_error.test b/tests/expr/t15_inductive_types_no_duplicate_names_4_error.test new file mode 100644 index 00000000..1db66749 --- /dev/null +++ b/tests/expr/t15_inductive_types_no_duplicate_names_4_error.test @@ -0,0 +1,6 @@ +discard """ + reject: true +""" +(DataTypeDecl typ + (Constr val (IntTy)) + (Constr val (FloatTy))) diff --git a/tests/expr/t15_inductive_types_no_duplicate_names_5_error.test b/tests/expr/t15_inductive_types_no_duplicate_names_5_error.test new file mode 100644 index 00000000..66710080 --- /dev/null +++ b/tests/expr/t15_inductive_types_no_duplicate_names_5_error.test @@ -0,0 +1,6 @@ +discard """ + reject: true +""" +(DataTypeDecl typ + (Constr val (IntTy)) + (Constr val (IntTy) (FloatTy)))