lang: add inductive data types

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))

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))

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)))))

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)))))

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)))))

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)))))

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)))))))

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))))))

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))

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))

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)))

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))

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))

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)))

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)))

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)))

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))))

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)))))

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)))))

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)))))

tests/expr/t15_inductive_types_no_duplicate_names_1_error.test

@@ -0,0 +1,6 @@
+discard """
+  reject: true
+"""
+(DataTypeDecl typ
+  (Constr val)
+  (Constr val))

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)))

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)))

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)))

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)))