From 05c6c22bb8a86beb6a4c4cc1a61341fdb1418104 Mon Sep 17 00:00:00 2001
From: DJ <f52985@gmail.com>
Date: Fri, 10 Jan 2025 20:26:38 +0900
Subject: [PATCH] Change tagtype from functype into deftype

---
 document/core/syntax/types.rst       |  4 ++--
 document/core/valid/instructions.rst |  6 +++---
 document/core/valid/matching.rst     |  7 +++++--
 document/core/valid/types.rst        | 12 +++++++++---
 4 files changed, 19 insertions(+), 10 deletions(-)

diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst
index 450db2bae6..b2fa630f00 100644
--- a/document/core/syntax/types.rst
+++ b/document/core/syntax/types.rst
@@ -483,11 +483,11 @@ Global Types
 Tag Types
 ~~~~~~~~~
 
-*Tag types* classify the signature of :ref:`tags <syntax-tag>` with a function type.
+*Tag types* classify the signature of :ref:`tags <syntax-tag>` with a defined type |deftype|, which expands to a function type |functype|.
 
 .. math::
    \begin{array}{llll}
-   \production{tag type} &\tagtype &::=& \functype \\
+   \production{tag type} &\tagtype &::=& \deftype \\
    \end{array}
 
 Currently tags are only used for categorizing exceptions.
diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
index 8eeaeb094c..8d179ff834 100644
--- a/document/core/valid/instructions.rst
+++ b/document/core/valid/instructions.rst
@@ -2601,15 +2601,15 @@ Control Instructions
 
 * The tag :math:`C.\CTAGS[x]` must be defined in the context.
 
-* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
+* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`expansion <aux-expand-deftype>` of the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
 
 * The :ref:`result type <syntax-resulttype>` :math:`[{t'}^\ast]` must be empty.
 
-* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of  :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
+* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
 
 .. math::
    \frac{
-     C.\CTAGS[x] = [t^\ast] \to []
+     \expanddt(C.\CTAGS[x]) = [t^\ast] \to []
    }{
      C \vdashinstr \THROW~x : [t_1^\ast~t^\ast] \to [t_2^\ast]
    }
diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst
index 12457adf82..564f5db142 100644
--- a/document/core/valid/matching.rst
+++ b/document/core/valid/matching.rst
@@ -580,12 +580,15 @@ A :ref:`global type <syntax-globaltype>` :math:`(\mut_1~t_1)` matches :math:`(\m
 Tag Types
 ~~~~~~~~~
 
-A :ref:`tag type <syntax-tagtype>` :math:`\tagtype_1` matches :math:`\tagtype_2` if and only if they are the same.
+A :ref:`tag type <syntax-tagtype>` :math:`\deftype_1` matches :math:`\deftype_2` if and only if the :ref:`defined type <syntax-deftype>` :math:`\deftype_1` :ref:`matches <match-deftype>` :math:`\deftype_2`, and vice versa.
 
 .. math::
    \frac{
+     C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2
+     \qquad
+     C \vdashdeftypematch \deftype_2 \matchesdeftype \deftype_1
    }{
-     C \vdashtagtypematch \tagtype \matchestagtype \tagtype
+     C \vdashtagtypematch \deftype_1 \matchestagtype \deftype_2
    }
 
 
diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst
index c1a97cb073..ed6138093f 100644
--- a/document/core/valid/types.rst
+++ b/document/core/valid/types.rst
@@ -551,10 +551,13 @@ Memory Types
 Tag Types
 ~~~~~~~~~
 
-:math:`[t_1^n] \to [t_2^m]`
+:math:`\deftype`
 ...........................
 
-* The :ref:`function type <syntax-functype>` :math:`[t_1^n] \to [t_2^m]` must be :ref:`valid <valid-functype>`.
+
+* The :ref:`defined type <syntax-deftype>` :math:`\deftype` must be :ref:`valid <valid-deftype>`.
+
+* The :ref:`expansion <aux-expand-deftype>` of :math:`\deftype` must be a :ref:`function type <syntax-functype>` :math:`\TFUNC~[t_1^n] \toF [t_2^m]`.
 
 * The type sequence :math:`t_2^m` must be empty.
 
@@ -562,8 +565,11 @@ Tag Types
 
 .. math::
    \frac{
+     C \vdashdeftype \deftype \ok
+     \qquad
+     \expanddt(\deftype) = \TFUNC~[t^\ast] \to []
    }{
-     \vdashtagtype [t^\ast] \to [] \ok
+     C \vdashtagtype \deftype \ok
    }