Stefan pushed to branch report/itd at Stefan / Typer

Commits: 556c1ffa by Stefan Monnier at 2018-11-17T06:40:11Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -1531,13 +1531,21 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \newcommand \TIrefl {\kw{refl}~} \newcommand \TIJ[3] {\kw{J}~#1~#2~#3}

-\begin{figure} +\begin{figure}[tb] \begin{displaymath} \begin{array}{l@{;=;}l} \TIUnit & \Tind{x}{\Type0}{x} \ \TIunit & \Tcon{0}{\TIUnit} \ \TIPair{x}{\tau_1}{\tau_2} & \Tind{y}{\Type?}{\Tarw{x}{\tau_1}{\Tsarw{\tau_2}{y}}} \ \TIpair{x}{e_1}{e_2}{\tau_2} & \Tcon{0}{\TIPair{x}{,?}{\tau_2}}~e_1~e_2 \ + \TIproj 1 e & + \TIcase{\Tlam{_}{,?}{\tau_1}}{e}{?}{\Tlam{x}{,?}{\Tlam{_}{,?}{x}}} + %% ;;;;\text{where }\Jtype{e}{\TIPair{x}{\tau_1}{\tau_2}} + \ + \TIproj 2 e & + \TIcase{\Tlam{x_e}{,?}%% {\TIPair{x}{\tau_1}{\tau_2}} + {\Tapp{(\Tlam{x}{,?}{\tau_2})}{(\TIproj 1 x_e)}}} + {e}{?}{\Tlam{_}{,?}{\Tlam{x}{,?}{x}}} \ \TIeq{e_1} & \Tind{x}{,\Tsarw{?}{x}}{\Tapp{x}{e_1}} \ \TIrefl{e_1} & \Tcon{0}{\TIeq{e_1}} \ \TIJ{e_\equiv}{e_f}{e} & @@ -1564,6 +1572,11 @@ system differs from that of~\citet{Gimenez94} in the following aspects: ;;;;;;;\text{if }\Jsubtype {\tau_1}{\tau_3} \end{array} \end{displaymath} + \caption{Auxiliary definitions used to map CUC to CIC.} + \label{fig:cuc-to-cic-aux} +\end{figure} + +\begin{figure} \begin{displaymath} \begin{array}{l@{;=;}l} \Ftocic x & x \ @@ -1597,21 +1610,24 @@ system differs from that of~\citet{Gimenez94} in the following aspects: }} \ \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} i}} & \MAlign{ - \TIcase {\Tlam _ {\tau_{e_2}} {?}} {e_2} {?} - {\Tlam {x_0} {\tau_0} {\Tlam {y} {\Ftocic{\Tuple \Delta}} {?}}} \ + \Tapp{(\TIcase {\tau_r} {e_2} {?} + {b})} + {(\TIrefl{(\TIproj 1 {e_2})})} \ ;;\text{where } \MAlign{ - %% ¡¡FIXME: \tau_1 is not equal to the type of y.(i-1)!! - %% We can get a proof `P : x₀=π₁ e₂` and then use - %% `J P y` to get y' that will have the appropriate type, - %% but then \JIdecreasing will not know that y' is - %% smaller than e₂ so termination checking fails! \FIXME{Wow!} \ + b = {\Tlam {x_0} {\tau_0} {\Tlam {y} {\Ftocic{\Tuple \Delta}} + {\textsl{body}}}} \ + \textsl{body} = \Tlam{x_\equiv}{\Teq{x_0}{\TIproj 1 {e_2}}}{?} \ e' = \Ftocic{\Tapp{(\Tlam x {\tau_1} {e_1})} {\Tproj {y} {(i - 1)}}} \ \Jtype{e_2}{\tau_{e_2}} \text{ and }{\tau_{e_2} = \Tuple {x_0:\tau_0,\Delta}} \ - \Jtype[\Gamma,x:\tau_1]{e_1}{\tau_2}}} + \Jtype[\Gamma,x:\tau_1]{e_1}{\tau_2} \ + \tau_r = \Tlam {x_e} {,?} {\Tarw{_} + {\Teq{\TIproj 1 {x_e}}{\TIproj 1 {e_2}}} + {\Subst{\tau_2}{\Ftocic{\Tproj {e_2}{i}}}{x}}} + }} \medskip \ \Ftocic {\Teq{e_1}{e_2}} & \TIeq{\Ftocic{e_1}}~{\Ftocic{e_2}} \ \Ftocic {\Trefl{e_1}} & \TIrefl{\Ftocic{e_1}} \

View it on GitLab: https://gitlab.com/monnier/typer/commit/556c1ffa897f9f5322cc04578abef1521705...