-\begin{figure}[p]
- \begin{subfigure}[b]{\textwidth}
- \vspace{-1cm}
- \mydesc{syntax}{ }{
- \footnotesize
- $
- \begin{array}{l}
- \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
- \end{array}
- $
- }
-
- \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
- \footnotesize
- $
- \begin{array}{r@{\ }l}
- & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
- \myelabf &
-
- \begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
- \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
- \end{array}
- \end{array}
- $
- }
-
- \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
- \footnotesize
-
- \AxiomC{$
- \begin{array}{c}
- \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
- \mytyc{D} \not\in \myctx \\
- \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
- \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
- \end{array}
- $}
- \UnaryInfC{$
- \begin{array}{r@{\ }c@{\ }l}
- \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
- & & \vspace{-0.2cm} \\
- & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
- & &
- \begin{array}{@{}r@{\ }l l}
- \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
- & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
- & \left.
- \begin{array}{@{}l}
- \myind{3} \vdots \\
- (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
- \end{array} \right \}
- & \textbf{methods} \\
- & \myapp{\myb{P}}{\myb{x}} &
- \end{array}
- \end{array}
- $}
- \DisplayProof \\ \vspace{0.2cm}\ \\
- $
- \begin{array}{@{}l l@{\ } l@{} r c l}
- \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
- & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\
- & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
- \end{array}
- $
-
- }
-
- \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
- \footnotesize
- $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
- \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
- \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
- \BinaryInfC{$
- \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)}
- $}
- \DisplayProof \\ \vspace{0.2cm}\ \\
- $
- \begin{array}{@{}l l@{\ } l@{} r c l}
- \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
- & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes & (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
- & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
- \end{array}
- $
- }
- \end{subfigure}
-
- \begin{subfigure}[b]{\textwidth}
- \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
- \footnotesize
- $
- \begin{array}{r@{\ }c@{\ }l}
- \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
- & \myelabf &
-
- \begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \mytyc{D}.\mydc{constr} \myappsp \mytmsyn^{n} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{f}_n \myappsp \mytmsyn \\
- \end{array}
- \end{array}
- $
-}
-
-
-\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
- \footnotesize
- \AxiomC{$
- \begin{array}{c}
- \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
- \mytyc{D} \not\in \myctx \\
- \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
- \end{array}
- $}
- \UnaryInfC{$
- \begin{array}{r@{\ }c@{\ }l}
- \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
- & & \vspace{-0.2cm} \\
- & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\
- & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
- \end{array}
- $}
- \DisplayProof
-}
-
- \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
- \footnotesize
- $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
- \AxiomC{$\mytyc{D} \in \myctx$}
- \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
- \DisplayProof
- }
-
- \end{subfigure}
- \caption{Elaboration for data types and records.}
- \label{fig:elab}
-\end{figure}
-