[Git][monnier/typer][report/itd] -
Stefan pushed to branch report/itd at Stefan / Typer Commits: ca169d0c by Stefan Monnier at 2018-10-03T23:54:17Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -618,7 +618,7 @@ which is sound and complete. \newcommand \JIcon[2][x] {#1 \vdash #2\;\;\kw{con}} \newcommand \JIpos[2][x] {#1 \vdash #2\;\;\kw{pos}} -\newcommand \Jdecreasing[5] {#1,#2,#3,#4 \vdash #5~\kw{decr}} +\newcommand \Jdecreasing[3][x_f,i,x_i] {#1,#2 \vdash #3~\kw{decr}} \newcommand \BT[2] {\id{BT}\llbracket #1 \rrbracket_{#2}} \begin{figure*} @@ -681,8 +681,43 @@ which is sound and complete. \Jtyper[\Gamma,x\:\tau] e \tau \\ e = \Tmlam{z}{\_}{\Tlam y {\_} {e_b}} \\ i = |z| \\ - \Jdecreasing{x}{i}{y}{\emptyset}{e_b}} + \Jdecreasing{\emptyset}{e_b}} {\Jtyper {\Tfix{i}{x}{\tau}{e}} {\tau}} + + %% Decreasing recursive calls + \Infer{x_f \not\in \kw{fv}(e)} + {\Jdecreasing v {e}} + + \Infer{\Jdecreasing v \tau \\ \Jdecreasing v e} + {\Jdecreasing v {\Tlam x \tau e}} + + \Infer{\Jdecreasing v \tau \\ \Jdecreasing v e} + {\Jdecreasing v {\Tarw x \tau e}} + + \Infer{\Jdecreasing v \tau \\ \Jdecreasing v e} + {\Jdecreasing v {\Tfix{i'}{x}{\tau}{e}}} + + \Infer{\Jdecreasing v {e_1} \\ \Jdecreasing v {e_2}} + {\Jdecreasing v {\Tapp{e_1}{e_2}}} + + \Infer{\Jdecreasing v {\vec e} \\ + i < |e| \\ + e_i = \Tapp{x}{\vec e'} \\ + x \in v} + {\Jdecreasing v {\Tapp{x_f}{\vec e}}} + + \Infer{\Jdecreasing v e \\ + \Jdecreasing v {\tau_r} \\ + \Jdecreasing v {\vec b}} + {\Jdecreasing v {\Tcase{\tau_r}{e}{\vec b}}} + + \Infer{\Jdecreasing v e \\ + e = \Tapp{x}{\vec e'} \\ + x \in v \cup \{ x_i \} \\ + ..FIXME.. \\ + \Jdecreasing v {\tau_r} \\ + \Jdecreasing v {\vec b}} + {\Jdecreasing v {\Tcase{\tau_r}{e}{\vec b}}} \end{mathpar} %% Reduction rules View it on GitLab: https://gitlab.com/monnier/typer/commit/ca169d0c4429c5573676d15b153095fcfce8... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/ca169d0c4429c5573676d15b153095fcfce8... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan