Typing Rules (#6)

Author: wildarch

spec/latex/dim.svg

@@ -0,0 +1,62 @@
+\documentclass[preview]{standalone}
+\usepackage{amsmath}
+\usepackage{semantic}
+\begin{document}
+
+\[
+  \inference[dim-nrows]{
+    F, D, L \vdash e : \langle d_1, d_2, R \rangle \\
+  }{
+    F, D, L \vdash_D e \texttt{.nrows} : d_1
+  }
+\]
+
+\[
+  \inference[dim-ncols]{
+    F, D, L \vdash e : \langle d_1, d_2, R \rangle \\
+  }{
+    F, D, L \vdash_D e \texttt{.ncols} : d_2
+  }
+\]
+
+\[
+  \inference[dim-var]{
+    d := D[M] \\
+  }{
+    F, D, L \vdash_D M : d
+  }
+\]
+
+\[
+  \inference[assign-nrows]{
+    \text{if } M_b \in L \text{: } L[M_b] = \langle 1, 1, \texttt{int} \rangle \\
+    F, D, L \vdash e : \langle d_1, d_2, \texttt{int} \rangle \\
+    L_r := L[M_b := \langle 1, 1, \texttt{int} \rangle] \\
+    D_r := D[M_b := d_1] \\
+  }{
+    F, D, L \vdash M_b \texttt{ = } e \texttt{.nrows;} : L_r, D_r
+  }
+\]
+
+\[
+  \inference[assign-ncols]{
+    \text{if } M_b \in L \text{: } L[M_b] = \langle 1, 1, \texttt{int} \rangle \\
+    F, D, L \vdash e : \langle d_1, d_2, \texttt{int} \rangle \\
+    L_r := L[M_b := \langle 1, 1, \texttt{int} \rangle] \\
+    D_r := D[M_b := d_2] \\
+  }{
+    F, D, L \vdash M_b \texttt{ = } e \texttt{.ncols;} : L_r, D_r
+  }
+\]
+
+\[
+  \inference[assign-dim]{
+    \text{if } M_b \in L \text{: } L[M_b] = \langle 1, 1, \texttt{int} \rangle \\
+    L_r := L[M_b := \langle 1, 1, \texttt{int} \rangle] \\
+    D_r := D[M_b := M_e] \\
+  }{
+    F, D, L \vdash M_b \texttt{ = } M_e \texttt{;} : L_r, D_r
+  }
+\]
+
+\end{document}

spec/latex/dim.tex

@@ -0,0 +1,27 @@
+\documentclass[preview]{standalone}
+\usepackage{semantic}
+\begin{document}
+\[
+  \inference[apply-unary]{
+    F, D, L \vdash e : \langle d_1, d_2, R_1 \rangle \\
+    ((\tau_p) \rightarrow \tau_r) := F[f] \\ 
+    \langle 1, 1, R_1 \rangle := \tau_p & \langle 1, 1, R_2 \rangle := \tau_r \\
+  }{
+    F, D, L \vdash \texttt{apply(} f \texttt{, } e \texttt{)} : \langle d_1, d_2, R_2 \rangle
+  }
+\]
+
+\[
+  \inference[apply-binary]{
+    F, D, L \vdash e_1 : \langle d_1, d_2, R_1 \rangle \\
+    F, D, L \vdash e_2 : \langle 1, 1, R_2 \rangle \\
+    ((\tau_{p_1} \times \tau_{p_2}) \rightarrow \tau_r) := F[f] \\ 
+    \langle 1, 1, R_1 \rangle := \tau_{p_1} 
+      & \langle 1, 1, R_2 \rangle := \tau_{p_2} 
+      & \langle 1, 1, R_3 \rangle := \tau_r \\
+  }{
+    F, D, L \vdash \texttt{apply(} f \texttt{, } e_1 \texttt{, } e_2 \texttt{)} : \langle d_1, d_2, R_3 \rangle
+  }
+\]
+
+\end{document}

spec/latex/expr-apply.svg

@@ -0,0 +1,57 @@
+\documentclass[preview]{standalone}
+\usepackage{semantic}
+\begin{document}
+\[
+  \inference[add]{
+    F, D, L \vdash e_1 : \langle 1, 1, R \rangle \\
+    F, D, L \vdash e_2 : \langle 1, 1, R \rangle \\
+  }{
+    F, D, L \vdash e_1 \texttt{ + } e_2 : \langle 1, 1, R \rangle
+  }
+\]
+
+\[
+  \inference[mul]{
+    F, D, L \vdash e_1 : \langle 1, 1, R \rangle \\
+    F, D, L \vdash e_2 : \langle 1, 1, R \rangle \\
+  }{
+    F, D, L \vdash e_1 \texttt{ * } e_2 : \langle 1, 1, R \rangle
+  }
+\]
+
+\[
+  \inference[sub]{
+    F, D, L \vdash e_1 : \langle 1, 1, R \rangle \\
+    F, D, L \vdash e_2 : \langle 1, 1, R \rangle \\
+    R \in \{ \texttt{int}, \texttt{real}\} \\
+  }{
+    F, D, L \vdash e_1 \texttt{ - } e_2 : \langle 1, 1, R \rangle
+  }
+\]
+
+\[
+  \inference[div]{
+    F, D, L \vdash e_1 : \langle 1, 1, \texttt{real} \rangle \\
+    F, D, L \vdash e_2 : \langle 1, 1, \texttt{real} \rangle \\
+  }{
+    F, D, L \vdash e_1 \texttt{ / } e_2 : \langle 1, 1, \texttt{real} \rangle
+  }
+\]
+
+\[
+  \inference[neg]{
+    F, D, L \vdash e : \langle 1, 1, R \rangle \\
+    R \in \{ \texttt{int}, \texttt{real} \}
+  }{
+    F, D, L \vdash \texttt{-}\ e : \langle 1, 1, R \rangle
+  }
+\]
+
+\[
+  \inference[not]{
+    F, D, L \vdash e : \langle 1, 1, \texttt{bool} \rangle \\
+  }{
+    F, D, L \vdash \texttt{!}\ e : \langle 1, 1, \texttt{bool} \rangle
+  }
+\]
+\end{document}

spec/latex/expr-apply.tex

@@ -0,0 +1,13 @@
+\documentclass[preview]{standalone}
+\usepackage{semantic}
+\begin{document}
+
+\[
+  \inference[cast]{
+    F, D, L \vdash e : \langle d_1, d_2, R_2 \rangle \\
+  }{
+    F, D, L \vdash \texttt{cast<} R_1 \texttt{>(} e \texttt{)}: \langle d_1, d_2, R_1 \rangle
+  }
+\]
+
+\end{document}

spec/latex/expr-arith.svg

@@ -0,0 +1,25 @@
+\documentclass[preview]{standalone}
+\usepackage{semantic}
+\begin{document}
+\[
+  \inference[eq]{
+    F, D, L \vdash e_1 : \langle 1, 1, R \rangle \\
+    F, D, L \vdash e_2 : \langle 1, 1, R \rangle \\
+    \diamond \in \{ \texttt{==}, \texttt{!=} \}
+  }{
+    F, D, L \vdash e_1 \diamond e_2 : \langle 1, 1, R \rangle
+  }
+\]
+
+\[
+  \inference[ord]{
+    F, D, L \vdash e_1 : \langle 1, 1, R \rangle \\
+    F, D, L \vdash e_2 : \langle 1, 1, R \rangle \\
+    R \in \{ \texttt{int}, \texttt{real} \} \\
+    \diamond \in \{ \texttt{<}, \texttt{>}, \texttt{<=}, \texttt{>=} \} \\
+  }{
+    F, D, L \vdash e_1 \diamond e_2 : \langle 1, 1, R \rangle
+  }
+\]
+
+\end{document}