[Git][monnier/typer][report/itd] -
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... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/556c1ffa897f9f5322cc04578abef1521705... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan