\newcommand{\myprsyn}{\myse{prop}}
\newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}}
\newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
+\newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
\newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
\newcommand{\mybot}{\mytyc{$\bot$}}
\subsubsection{User defined types}
\label{sec:user-type}
-\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}
-
Elaborating user defined types is the real effort. First, let's explain
what we can defined, with some examples.
What we have is equivalent to ITT's dependent products.
\end{description}
+\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}
+
Following the intuition given by the examples, the mechanised
elaboration is presented in figure \ref{fig:elab}, which is essentially
a modification of figure 9 of \citep{McBride2004}\footnote{However, our
\DisplayProof
}
-\subsubsection{Why user defined types?}
+\subsubsection{Why user defined types? Why eliminators?}
% TODO reference levitated theories, indexed containers
It is worth to ask if $\myprop$ is needed at all. It is perfectly
possible to have the type checker identify propositional types
automatically, and in fact that is what The author initially planned to
-identify the propositional fragment iinternally \cite{Jacobs1994}.
+identify the propositional fragment internally \cite{Jacobs1994}.
+
+% TODO finish
\subsubsection{OTT constructs}
\]}
Finally, quotation
% TODO quotation
+
+
\end{description}
$
}
+\begin{figure}[p]
+\mydesc{typing:}{\myctx \vdash \myprsyn \myred \myprsyn}{
+ \footnotesize
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
+ \DisplayProof
+ \end{tabular}
+}
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+ \footnotesize
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
+ \UnaryInfC{$\myjud{\mytop}{\myprop}$}
+ \noLine
+ \UnaryInfC{$\myjud{\mybot}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+ \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
+ \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{$
+ \begin{array}{@{}c}
+ \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
+ \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
+ \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
+ \end{array}
+ $}
+ \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$
+ \begin{array}{c}
+ \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
+ \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
+ \end{array}
+ $}
+ \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
+ \DisplayProof
+ \end{tabular}
+}
+ % TODO equality for decodings
\mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
\footnotesize
+ \AxiomC{}
+ \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
+ \DisplayProof
+
+ \myderivsp
+
\AxiomC{}
\UnaryInfC{$
- \begin{array}{r@{\ }l}
+ \begin{array}{@{}r@{\ }l}
\myctx \vdash &
\myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
- & \myind{2} \mytya_2 \myeq \mytya_1 \myand \\
- & \myind{2} \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
+ & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
\myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1 \myeq \mytyb_2
}}
\end{array}
\myderivsp
- \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+ \AxiomC{}
\UnaryInfC{$
- \begin{array}{r@{\ }l}
+ \begin{array}{@{}r@{\ }l}
\myctx \vdash &
- \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
- & \myind{2} \myjm{\mytya_1}{\myhead(\mytele)}{\mytyb_1}{\myhead(\mytele)} \myand \cdots \myand \\
- & \myind{2} \myjm{\mytya_n}{\myhead(\mytele(A_1 \cdots A_{n-1}))}{\mytyb_n}{\myhead(\mytele(B_1 \cdots B_{n-1}))}
+ \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
+ & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
+ \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
+ \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]}
+ }}
\end{array}
$}
\DisplayProof
+
\myderivsp
- \AxiomC{}
- \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
+ \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+ \UnaryInfC{$
+ \begin{array}{r@{\ }l}
+ \myctx \vdash &
+ \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
+ & \myind{2} \mybigand_{i = 1}^n (\myjm{\mytya_n}{\myhead(\mytele(A_1 \cdots A_{i-1}))}{\mytyb_i}{\myhead(\mytele(B_1 \cdots B_{i-1}))})
+ \end{array}
+ $}
\DisplayProof
\myderivsp
\AxiomC{$
- \begin{array}{c}
+ \begin{array}{@{}c}
\mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
- \mytyc{D}.\mydc{c}_i : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\
+ \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\
\mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
\mytele_B = (\mytele;\mytele')\vec{B}
\end{array}
$}
\UnaryInfC{$
- \begin{array}{l}
- \myctx \vdash \myjm{\mytyc{D}.\mydc{c}_i \myappsp \vec{\mytmm}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c}_i \myappsp \vec{\mytmn}}{\mytyc{D} \myappsp \vec{B}} \myred \\
- \myind{2} \myjm{\mytmm_1}{\myhead(\mytele_A)}{\mytmn_1}{\myhead(\mytele_B)} \myand \cdots \myand \\
- \myind{2} \myjm{\mytmm_n}{\mytya_n}{\mytmn_n}{\mytyb_n}
+ \begin{array}{@{}l@{\ }l}
+ \myctx \vdash & \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \\
+ & \myind{2} \mybigand_{i=1}^n(\myjm{\mytmm_i}{\myhead(\mytele_A (\mytya_i \cdots \mytya_{i-1}))}{\mytmn_i}{\myhead(\mytele_B (\mytyb_i \cdots \mytyb_{i-1}))})
\end{array}
$}
\DisplayProof
\myderivsp
- \AxiomC{$\myisreco(\mytyc{D}, \myctx)$}
- \UnaryInfC{$\myctx \vdash \myjm{\mytmm}{\mytyc{D} \myappsp \vec{A}}{\mytmn}{\mytyc{D} \myappsp \vec{B}} \myred foo$}
+ \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
+ \UnaryInfC{$
+ \myctx \vdash \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c'} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \mybot
+ $}
+ \DisplayProof
+
+ \myderivsp
+
+ \AxiomC{$
+ \begin{array}{@{}c}
+ \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
+ \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
+ \end{array}
+ $}
+ \UnaryInfC{$
+ \begin{array}{@{}l@{\ }l}
+ \myctx \vdash & \myjm{\myse{l}}{\mytyc{D} \myappsp \vec{A}}{\myse{r}}{\mytyc{D} \myappsp \vec{B}} \myred \\ & \myind{2} \mybigand_{i=1}^n(\myjm{\mytyc{D}.\myfun{f}_1 \myappsp \myse{l}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytya};\myse{l})}{\mytyc{D}.\myfun{f}_i \myappsp \myse{r}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytyb};\myse{r})})
+ \end{array}
+ $}
\DisplayProof
\myderivsp
\AxiomC{}
- \UnaryInfC{$\mytya \myeq \mytyb \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
+ \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
\DisplayProof
}
+ \caption{Equality reduction for $\mykant$.}
+ \label{fig:kant-eq-red}
+\end{figure}
\subsubsection{$\myprop$ and the hierarchy}
\label{fig:kant-process}
\end{figure}
-\subsection{Parsing and Sugar}
+\subsection{Parsing and \texttt{Sugar}}
\subsection{Term representation and context}
\label{sec:term-repr}
projects / bitonic-mengthesis.git / commitdiff