Stefan pushed to branch report/hmdup at Stefan / Typer

Commits: 45bf474a by Stefan Monnier at 2020-07-01T13:09:15-04:00 -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -730,13 +730,13 @@ incompatible with things like value polymorphism.

\begin{figure} \begin{mathpar} - \Infer{ + \Infer[(EF-Var)]{ \Gamma(x) = \tau }{ \JEsynth{x}{\tau}{x} }

- \Infer{ + \Infer[(EF-Let)]{ \JEsynth{e_1}{\tau_1}{E_1} \ \overrightarrow{t:*} = \kw{fmv}(\Gamma,\tau_1) \ \JEpoly[\Gamma,x:\MDArw{t:*}{\tau_1}]{e_2}{\tau}{E_2} @@ -745,7 +745,7 @@ incompatible with things like value polymorphism. \Let {x} {\TLam{\overrightarrow{t:*}}{E_1}}{E_2}} }

- \Infer{ + \Infer[(EF-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ \Jfresh{u_1,u_2} \ \JEcheckCoerce{e_1}{\Arw{u_1}{u_2}}{E_1} \ @@ -754,7 +754,7 @@ incompatible with things like value polymorphism. \JEsynth{e_1~e_2}{u_2}{E_1~E_2} }

- \Infer{ + \Infer[(EF-Lam)]{ \Jfresh {\Meta{u_1},\Meta{u_2}} \ \Junify {\tau}{\Arw{\Meta{u_1}}{\Meta{u_2}}} \ \JEcheckCoerce[\Gamma,x:\Meta{u_1}]{e}{\Meta{u_2}}{E} @@ -762,26 +762,26 @@ incompatible with things like value polymorphism. \JEcheck{\Lam x e}{\tau}{\Lam{x:\Meta{u_1}}{E}} }

- \Infer{ + \Infer[(EF-HT)]{ \JEcheckCoerce e \tau E }{ \JEsynth{\HasType{e}{\tau}}{\tau}{E} }

- \Infer{ + \Infer[(EF-Infer)]{ \Jfresh{\Meta{u}} \ \JEcheck{e}{\Meta{u}}{E} }{ %% FIXME: Make it \JsynthCoerce? \JEsynth{e}{\Meta{u}}{E} }

- \Infer{ + \Infer[(EF-Poly)]{ \JEcheck[\Gamma,\overrightarrow{t:*}] e {\tau}{E} }{ \JEcheckCoerce{e}{\MDArw{t:*}{\tau}}{\TLam{\overrightarrow{t:*}}{E}} }

- \Infer{ + \Infer[(EF-Coerce)]{ %% \Jmono{\tau} \ \JEsynth{e}{\tau}{E} \ \JEcoerce {E}{\tau}{E'}{\tau'} @@ -791,7 +791,7 @@ incompatible with things like value polymorphism.

%% FIXME: The rules below don't make much sense yet, I think! %% - \Infer{ + \Infer[(CO-Inst)]{ \Jfresh {\vec {\Meta{u}}} \ \Junify{\tau[\vec {\Meta{u}}/\vec t]}{\tau'} }{ @@ -799,7 +799,7 @@ incompatible with things like value polymorphism. {\TApp{E}{\vec {\Meta{u}}}} {\tau'} }

- \Infer{ + \Infer[(CO-Gen)]{ \Jfresh {\vec {\Meta{u}}} \ \JEcoerce {E} {\tau} {E'} {\tau'[\vec {\Meta{u}}/\vec t]} \ %% FIXME: Maybe "u" was instantiated to some other

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/45bf474a5ceb1f7f7f5f84c7f62885811a...