Stefan pushed to branch report/itd at Stefan / Typer Commits: 143748a4 by Stefan Monnier at 2018-10-05T15:29:53Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -614,7 +614,8 @@ which is sound and complete. \newcommand \Tind[3] {\kw{Ind}(#1\:#2)\langle#3\rangle} \newcommand \Tcon[2] {\kw{Con}(#1,#2)} -\newcommand \TIcase[4] {{<}#1{>}\kw{Case}~#2:#3~\kw{of}~\langle#4\rangle} +\newcommand \TIcase[4] {{<}#1{>}\kw{Case}~#2%% :#3 + ~\kw{of}~\langle#4\rangle} \newcommand \Tfix[3] {\kw{Fix}_{#1}~#2:#3~=~} \newcommand \JIcon[2][x] {#1 \vdash #2\;\;\kw{con}} @@ -642,12 +643,13 @@ which is sound and complete. \Infer{\JIcon e \\ \JIpos \tau}{\JIcon {\Tsarw \tau e}} %% Actual typing rules - %% FIXME: This lets all inductive types live in Type0!! - \Infer{\Jtyper{\tau}{\Type{\ell}} \\ + \Infer{\Jtyper{\tau}{\Type{\ell+1}} \\ + \tau = \Tmarw{\_}{\_}{\Type{\ell}} \\ \forall i \\ - \Jtyper[\Gamma,x\:\tau]{c_i}{\Type{\ell_i}} \\ - \JIcon {c_i} \\ - \ell_i < \ell} + \Jtyper[\Gamma,x\:\tau]{c_i}{\Type{\ell}} \\ + \JIcon {c_i} %% \\ + %% \ell_i < \ell + } {\Jtyper{\Tind{x}{\tau}{\vec c}}{\tau}} %% FIXME: This presentation doesn't allow `Con(0,Nat)` but requires @@ -703,20 +705,31 @@ which is sound and complete. \Jdecreasing \nu {\vec b}} {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} + %% The rule for the impredicative case! \Infer{\Jdecreasing \nu e \\ \Jdecreasing \nu {\tau_r} \\ \Jdecreasing \nu {\tau_e} \\\\ e = \Tapp{x_e}{\vec \_} \\ x_e \in \nu \cup \{ x_i \} \\ - \tau_e = {\tau_I~{\vec \_}} \\ - \tau_I = \Tind{x_I}{\_}{\vec c} \\ - \Jdecreasing \nu {\vec b} \\\\ \forall i \\ b_i = \Tmlam{y}{\_}{e_i} \\ - c_i = \Tmarw{\_}{\tau_i}{\_} \\ - \nu' = \{~ y_j ~|~ \tau_{ij} = \Tapp{x_I}{\vec \_} ~\} \\ - \Jdecreasing {\nu \cup \nu'} {b_i}} + \Jdecreasing {\nu \cup \vec y} {b_i}} {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} + + %% The rule for the impredicative case! + %% \Infer{\Jdecreasing \nu e \\ + %% \Jdecreasing \nu {\tau_r} \\ + %% \Jdecreasing \nu {\tau_e} \\\\ + %% e = \Tapp{x_e}{\vec \_} \\ + %% x_e \in \nu \cup \{ x_i \} \\ + %% \tau_e = {\tau_I~{\vec \_}} \\ + %% \tau_I = \Tind{x_I}{\_}{\vec c} \\ + %% \forall i \\ + %% b_i = \Tmlam{y}{\_}{e_i} \\ + %% c_i = \Tmarw{\_}{\tau_i}{\_} \\ + %% \nu' = \{~ y_j ~|~ \tau_{ij} = \Tapp{x_I}{\vec \_} ~\} \\ + %% \Jdecreasing {\nu \cup \nu'} {b_i}} + %% {\Jdecreasing \nu {\TIcase{\tau_r}{e}{\tau_e}{\vec b}}} \end{mathpar} %% Reduction rules View it on GitLab: https://gitlab.com/monnier/typer/commit/143748a438cd31ae76a5079816937025fef7... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/143748a438cd31ae76a5079816937025fef7... You're receiving this email because of your account on gitlab.com.