From a961739bbf672eaad0a26fb15372fcc68c902ef1 Mon Sep 17 00:00:00 2001 From: bringert Date: Mon, 6 Mar 2006 16:55:22 +0000 Subject: [PATCH] Transfer type system: some random changes --- transfer/doc/typesystem.tex | 133 +++++++++++++++++++++++++++++------- 1 file changed, 109 insertions(+), 24 deletions(-) diff --git a/transfer/doc/typesystem.tex b/transfer/doc/typesystem.tex index 5268e5638..023783ae3 100644 --- a/transfer/doc/typesystem.tex +++ b/transfer/doc/typesystem.tex @@ -88,8 +88,7 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \and \inferrule[Check by inferring] -{ \Delta;\Gamma \vdash t \uparrow B \\ - \Delta;\Gamma \vdash B \lesssim A } +{ \Delta;\Gamma \vdash t \uparrow A } { \Delta;\Gamma \vdash t \downarrow A } \and @@ -121,7 +120,9 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \inferrule[Application] { \Delta;\Gamma \vdash s \uparrow (x : A) \rightarrow B \\ - \Delta;\Gamma \vdash t \downarrow B } + \Delta;\Gamma \vdash t \downarrow A \\ + \textrm{FIXME: argument can be of a subtype} +} { \Delta;\Gamma \vdash s \ t \uparrow B [x / t] } \and @@ -137,11 +138,12 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ { \Delta;\Gamma \vdash s \uparrow A \\ \Delta \vdash_p p_1 \downarrow A; \Gamma' \\ \Delta;\Gamma,\Gamma' \vdash g_1 \downarrow Bool \\ - \Delta;\Gamma,\Gamma' \vdash t_1 \uparrow B \\ + \Delta;\Gamma,\Gamma' \vdash t_1 \uparrow B_1 \\ \ldots \\ \Delta p_n \vdash_p A; \Gamma' \\ \Delta;\Gamma, \Gamma' \vdash g_n \downarrow Bool \\ - \Delta;\Gamma, \Gamma' \vdash t_n \uparrow B \\ + \Delta;\Gamma, \Gamma' \vdash t_n \uparrow B_n \\ + B = B_1 \vee \ldots \vee B_n } { \Delta;\Gamma \vdash \textrm{case} \ s \ \textrm{of} \ \{ p_1 \mid g_1 \rightarrow t_1; @@ -158,7 +160,7 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \begin{mathpar} \inferrule[Record type] -{ FIXME: labels must occur at most once \\ +{ \textrm{FIXME: labels must occur at most once} \\ \Delta;\Gamma \vdash T_1 \uparrow Type \\ \ldots \\ \Delta;\Gamma, l_1 : T_1, \ldots, l_{n-1} : T_{n-1} \vdash T_n \uparrow Type } @@ -167,7 +169,7 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \and \inferrule[Record] -{ FIXME: labels must occur at most once \\ +{ \textrm{FIXME: labels must occur at most once} \\ \Delta;\Gamma \vdash t_1 \uparrow T_1 \\ \ldots \\ \Delta;\Gamma \vdash t_n \uparrow T_n [l_{n-1} / t_{n-1}] \ldots [l_1 / t_1] } @@ -202,17 +204,22 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \and \inferrule[Constructor pattern] -{ c : (x_1 : T_1) \rightarrow \ldots \rightarrow T \in \Delta \\ +{ c : (x_1 : T_1) \rightarrow \ldots \rightarrow T' \in \Delta \\ + T' = T \\ \Delta \vdash_p p_1 \downarrow T_1; \Gamma_1 \\ \ldots \\ \Delta \vdash_p p_n \downarrow T_n; \Gamma_n \\ + \textrm{FIXME: $x_k$ can occur in $T_{k+1}$} } -{ \Delta \vdash_p c p_1 \ldots p_n \ \downarrow \ T; \Gamma_1, \ldots, \Gamma_n } +{ \Delta \vdash_p c \ p_1 \ldots p_n \ \downarrow \ T; \Gamma_1, \ldots, \Gamma_n } \and -\inferrule[Record pattern FIXME: allow more fields in type, ignore order] -{ \Delta \vdash_p p_1 \ \downarrow \ T_1; \Gamma_1 \\ +\inferrule[Record pattern] +{ \textrm{FIXME: labels must occur at most once} \\ + \textrm{FIXME: allow more fields in type, ignore order} \\ + \textrm{FIXME: types can depend on field values} \\ +\Delta \vdash_p p_1 \ \downarrow \ T_1; \Gamma_1 \\ \ldots \\ \Delta \vdash_p p_n \ \downarrow \ T_n; \Gamma_n \\ } @@ -234,8 +241,8 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \and \end{mathpar} -\caption{Patterns.} -\label{fig:patterns} +\caption{Type-checking patterns.} +\label{fig:typing-patterns} \end{figure} @@ -308,12 +315,14 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \ldots \\ s_n \lesssim t_n \\ } -{ c s_1 \ldots s_n \leq c t_1 \ldots t_n } +{ c \ s_1 \ldots s_n \leq c \ t_1 \ldots t_n } \and \inferrule[Record type conversion] -{ FIXME } +{ A_1 \lesssim B_1 \ldots A_n \lesssim B_n \\ + \textrm{FIXME: types can depend on fields} \\ + \textrm{FIXME: allow more fields on the left, ignore order} } { \textrm{sig} \ \{ l_1 : A_1 \ldots l_n : A_n \} \leq \textrm{sig} \ \{ k_1 : B_1 \ldots k_m : B_m \} } @@ -321,7 +330,10 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \and \inferrule[Record conversion] -{ FIXME } +{ + \textrm{FIXME: allow more fields on the left, ignore order} \\ + s_1 \lesssim t_1 \ldots s_n \lesssim s_n +} { \textrm{rec} \ \{ l_1 = s_1 \ldots l_n = s_n \} \leq \textrm{rec} \ \{ k_1 = t_1 \ldots k_m = t_m \} } @@ -338,6 +350,13 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ +\and + +\inferrule[WHNF-Proj] +{ s \Downarrow_{wh} \textrm{rec} \ \{ \ldots, l = t, \ldots \} } +{ \Gamma \vdash s.l \Downarrow_{wh} t } + + \end{mathpar} @@ -348,7 +367,7 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \begin{figure} \begin{mathpar} -\inferrule[Eval-let] +\inferrule[WHNF-Let] { s \Downarrow_{wh} s' } { \Gamma \vdash \textrm{let} \ x = s \ \textrm{in} \ t \Downarrow_{wh} t [x/s'] @@ -356,25 +375,91 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \and -\inferrule[Eval-case] -{ } +\inferrule[WHNF-Case] +{ \textrm{FIXME: find the right case arm} \\ + \textrm{FIXME: bind / substitute variables in RHS} } { \Gamma \vdash \textrm{case} \ s \ \textrm{of} \{ \overline{p \mid t \rightarrow u} \} + \Downarrow_{wh} } \and -\inferrule[Eval-abstraction] -{ } -{ \Gamma \vdash \lambda x . t \Downarrow_{wh} \lambda x . t \} +\inferrule[WHNF-Beta] +{ \Gamma \vdash s \Downarrow_{wh} \lambda x . s' \\ + \Gamma \vdash t \Downarrow_{wh} t' } +{ \Gamma \vdash s \ t \Downarrow_{wh} s' [x/t'] \} } \and -\inferrule[Eval-function type] +\inferrule[WHNF-Proj] +{ \Gamma \vdash s \Downarrow_{wh} \textrm{rec} \ \{ \ldots, l = t, \ldots \} } +{ \Gamma \vdash s.l \Downarrow_{wh} t } + +\and + +\inferrule[WHNF-Var] +{ x = t \in \Gamma \\ + \textrm{FIXME: there shouldn't be any free variables (but there can be functions and constructors)} } +{ \Gamma \vdash x \Downarrow_{wh} t } + + +% unchanged: + +\and + +\inferrule[WHNF-Lambda] { } -{ \Gamma \vdash (x : s) \rightarrow t \Downarrow_{wh} \} +{ \Gamma \vdash \lambda x . t \Downarrow_{wh} \lambda x . t } + +\and + +\inferrule[WHNF-Pi] +{ } +{ \Gamma \vdash (x : s) \rightarrow t \Downarrow_{wh} (x : s) \rightarrow t } +\and + +\inferrule[WHNF-Sig] +{ } +{ \Gamma \vdash \textrm{sig} \ \{ l_1 : A_1, \ldots, l_n : A_n \} + \Downarrow_{wh} \textrm{sig} \ \{ l_1 : A_1, \ldots, l_n : A_n \} } + +\and + +\inferrule[WHNF-Rec] +{ } +{ \Gamma \vdash \textrm{rec} \ \{ l_1 = t_1, \ldots, l_n = t_n \} + \Downarrow_{wh} \textrm{rec} \ \{ l_1 = t_1, \ldots, l_n = t_n \} } + +\and + +\inferrule[WHNF-Type] +{ } +{ \Gamma \vdash Type \Downarrow_{wh} Type } + +\and + +\inferrule[WHNF-String] +{ } +{ \Gamma \vdash string \Downarrow_{wh} string } + +\and + +\inferrule[WHNF-Integer] +{ } +{ \Gamma \vdash integer \Downarrow_{wh} integer } + +\and + +\inferrule[WHNF-Double] +{ } +{ \Gamma \vdash double \Downarrow_{wh} double } + +% FIXME: applications which are not beta redexes? + + \end{mathpar}