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...