diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-26 18:41:41 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-26 18:41:41 +0100 |
| commit | 0cc576553729adf6081e9322c7621fc8241113e1 (patch) | |
| tree | 111d8d109c3f2a8792ff72151c8c06caa195bacc /sec | |
| parent | 6312e6ce1406cbacddae0b4ccddb9bc4c068548c (diff) | |
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/compiler.ltx | 47 |
1 files changed, 24 insertions, 23 deletions
diff --git a/sec/compiler.ltx b/sec/compiler.ltx index f1abca9..a9ab7f8 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -90,14 +90,26 @@ raw AST.\@ \subsection{Bidirectional Type Checker} \begin{figure} + \small \[ - \begin{array}{cccc} + \begin{array}{ccc} \begin{prooftree} \hypo{x : A \in \Gamma} \infer1{\judgement{\Gamma}{x}[\Rightarrow]{A}} \end{prooftree} & \begin{prooftree} + \hypo{\judgement{\Gamma}{t}[\Rightarrow]{A}} + \hypo{A = B} + \infer2{\judgement{\Gamma}{t}[\Leftarrow]{B}} + \end{prooftree} + & + \begin{prooftree} + \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A}} + \infer1{\judgement{\Gamma}{t : A}[\Rightarrow]{A}} + \end{prooftree} + \\\\ + \begin{prooftree} \hypo{\judgement{\Gamma, x : A}{t}[\Leftarrow]{B}} \infer1{\judgement{\Gamma}{\lambda x.t}[\Leftarrow]{A \to B}} \end{prooftree} @@ -115,35 +127,24 @@ raw AST.\@ \end{prooftree} \\\\ \begin{prooftree} - \hypo{\rangeover{\judgement{\Gamma}{t_i}[\Leftrightarrow]{A_i}}{i}} - \infer1{\judgement{\Gamma}{\tuple{\rangeover{t_i}{i}}}[\Leftrightarrow]{\prod_i A_i}} + \hypo{\rangeover{\judgement{\Gamma}{t_\ell}[\Leftrightarrow]{A_\ell}}{\ell}} + \infer1{\judgement{\Gamma}{\tuple{\ell : \rangeover{t_\ell}{\ell}}}[\Leftrightarrow]{\prod_{\ell \in I} A_\ell}} \end{prooftree} & \begin{prooftree} - \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\prod_i A_i}} - \infer1{\judgement{\Gamma}{t.i}[\Rightarrow]{A_i}} + \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A_{\hat{\ell}}}} + \infer1{\judgement{\Gamma}{\hat{\ell}~t}[\Leftarrow]{\sum_{\ell \in I} A_\ell}} \end{prooftree} & \begin{prooftree} - \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A_i}} - \infer1{\judgement{\Gamma}{\tuple{i, t}}[\Leftarrow]{\sum_i A_i}} - \end{prooftree} - & - \begin{prooftree} - \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\sum_i A_i}} - \hypo{\rangeover{\judgement{\Gamma, x_i : A_i}{t_i}[\Leftarrow]{B}}{i}} - \infer2{\judgement{\Gamma}{\casetm{t}{\tuple{i,x_i}}{t_i}{i}}[\Leftarrow]{B}} + \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\sum_{\ell \in I} A_\ell}} + \hypo{\rangeover{\judgement{\Gamma, x_\ell : A_\ell}{t_\ell}[\Leftarrow]{B}}{\ell}} + \infer2{\judgement{\Gamma}{\casetm{t}{\ell~x_\ell}{t_\ell}{\ell}}[\Leftarrow]{B}} \end{prooftree} \\\\ \begin{prooftree} - \hypo{\judgement{\Gamma}{t}[\Rightarrow]{A}} - \hypo{A = B} - \infer2{\judgement{\Gamma}{t}[\Leftarrow]{B}} - \end{prooftree} - & - \begin{prooftree} - \hypo{\judgement{\Gamma}{t}[\Leftarrow]{A}} - \infer1{\judgement{\Gamma}{t : A}[\Rightarrow]{A}} + \hypo{\judgement{\Gamma}{t}[\Rightarrow]{\prod_{\ell \in I} A_\ell}} + \infer1{\judgement{\Gamma}{t.\hat{\ell}}[\Rightarrow]{A_{\hat{\ell}}}} \end{prooftree} & \begin{prooftree} @@ -158,7 +159,7 @@ raw AST.\@ \end{prooftree} \end{array} \] - \caption{Bidirectional typing rules for + \caption{\TODO{un-small}. Bidirectional typing rules for \lang{}.\@ We say \(t\) synthesises type \(A\) when \(\judgement{\Gamma}{t}[\Rightarrow]{A}\) and \(t\) checks at type \(A\) when \(\judgement{\Gamma}{t}[\Leftarrow]{A}\). We use \(\Leftrightarrow\) when a term can both @@ -168,7 +169,7 @@ raw AST.\@ \Cref{fig:bidir} shows how we have modified the \lang{} typing rules for bidirectional type checking. The changes are -standard~\cref{bidir}. Products can both check and synthesise types. +standard~\cite{bidir}. Products can both check and synthesise types. The \roll{} operator can only be checked as there is no unique correct guess for the shape type. The body of a \foldkw{} must be checked. The induction hypothesis is added to the context, so its type must be |