diff options
| -rw-r--r-- | transfer/TODO | 2 | ||||
| -rw-r--r-- | transfer/doc/typesystem.tex | 57 | ||||
| -rw-r--r-- | transfer/examples/tricky-type-checking.tra | 6 |
3 files changed, 40 insertions, 25 deletions
diff --git a/transfer/TODO b/transfer/TODO index d3a78d49d..6ad3a3428 100644 --- a/transfer/TODO +++ b/transfer/TODO @@ -12,6 +12,8 @@ - Simplify taking many arguments of the same type: f : (A,B : Type) -> ... +- add record extension operator? + * Improve interpreter - More efficient handling of constructor application diff --git a/transfer/doc/typesystem.tex b/transfer/doc/typesystem.tex index bb2b9e602..fb26b064c 100644 --- a/transfer/doc/typesystem.tex +++ b/transfer/doc/typesystem.tex @@ -88,8 +88,8 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \and \inferrule[Check by inferring] -{ \Delta;\Gamma \vdash t \uparrow A \\ - \textrm{FIXME: conversion (but not subtyping?) } } +{ \Delta;\Gamma \vdash t \uparrow A' \\ + A' \lesssim A} { \Delta;\Gamma \vdash t \downarrow A } \and @@ -121,8 +121,8 @@ 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 A' \\ - A' \lesssim A } + \Delta;\Gamma \vdash t \downarrow A +} { \Delta;\Gamma \vdash s \ t \uparrow B [x / t] } \and @@ -136,14 +136,14 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \inferrule[Case analysis] { \Delta;\Gamma \vdash s \uparrow A \\ + B = B_1 \vee \ldots \vee B_n \\ \Delta \vdash_p p_1 \downarrow A; \Gamma_1 \\ \Delta;\Gamma,\Gamma_1 \vdash g_1 \downarrow Bool \\ \Delta;\Gamma,\Gamma_1 \vdash t_1 \uparrow B_1 \\ \ldots \\ \Delta p_n \vdash_p A; \Gamma_n \\ \Delta;\Gamma, \Gamma_n \vdash g_n \downarrow Bool \\ - \Delta;\Gamma, \Gamma_n \vdash t_n \uparrow B_n \\ - B = B_1 \vee \ldots \vee B_n + \Delta;\Gamma, \Gamma_n \vdash t_n \uparrow B_n } { \Delta;\Gamma \vdash \textrm{case} \ s \ \textrm{of} \ \{ p_1 \mid g_1 \rightarrow t_1; @@ -160,19 +160,20 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \begin{mathpar} \inferrule[Record type] -{ \textrm{FIXME: labels must occur at most once} \\ - \Delta;\Gamma \vdash T_1 \uparrow Type \\ +{ \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 } + \Delta;\Gamma, l_1 : T_1, \ldots, l_{n-1} : T_{n-1} \vdash T_n \uparrow Type \\ + l_1 \ldots l_n \ \textrm{different} +} { \Delta;\Gamma \vdash \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} \uparrow Type } \and \inferrule[Record] -{ \textrm{FIXME: labels must occur at most once} \\ - \Delta;\Gamma \vdash t_1 \uparrow T_1 \\ +{ \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] } + \Delta;\Gamma \vdash t_n \uparrow T_n [l_{n-1} / t_{n-1}] \ldots [l_1 / t_1] \\ + l_1 \ldots l_n \ \textrm{different} } { \Delta;\Gamma \vdash \textrm{rec} \{ l_1 = t_1, \ldots, l_n = t_n \} \uparrow \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} } @@ -204,11 +205,12 @@ 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 (x_n : T_n) \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 \\ + \Gamma_1 \ldots \Gamma_n \ \textrm{disjoint} \\ \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 } @@ -216,12 +218,13 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \and \inferrule[Record pattern] -{ \textrm{FIXME: labels must occur at most once} \\ - \textrm{FIXME: allow more fields in type, ignore order} \\ +{ \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 \\ + \Gamma_1 \ldots \Gamma_n \ \textrm{disjoint} \\ + l_1 \ldots l_n \ \textrm{different} } { \Delta \vdash_p \textrm{rec} \ \{ l_1 = p_1; \ldots; l_n = p_n \} \ \downarrow \ \textrm{sig} \ \{ l_1 : T_1; \ldots; l_n : T_n \}; \Gamma_1, \ldots, \Gamma_n } @@ -346,18 +349,21 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ i_1 =_{integer} i_2} { i_1 \leq i_2 } +\and +\inferrule[String conversion] +{ i_1 \ \textrm{string} \\ + i_2 \ \textrm{string} \\ + i_1 =_{string} i_2} +{ i_1 \leq i_2 } +\and - -\and - -\inferrule[WHNF-Proj] -{ s \Downarrow_{wh} \textrm{rec} \ \{ \ldots, l = t, \ldots \} } -{ \Gamma \vdash s.l \Downarrow_{wh} t } - - - +\inferrule[Double conversion] +{ i_1 \ \textrm{double} \\ + i_2 \ \textrm{double} \\ + i_1 =_{double} i_2} +{ i_1 \leq i_2 } \end{mathpar} \caption{Conversion and subtyping.} @@ -368,7 +374,8 @@ p & ::= & x \ | \ \_ \ | \ (c \overline{p}) \ | \ rec \ \{ \overline{l = p} \} \ \begin{mathpar} \inferrule[WHNF-Let] -{ s \Downarrow_{wh} s' } +{ s \Downarrow_{wh} s' \\ + \textrm{This is a weird way to evaluate a let} } { \Gamma \vdash \textrm{let} \ x = s \ \textrm{in} \ t \Downarrow_{wh} t [x/s'] } diff --git a/transfer/examples/tricky-type-checking.tra b/transfer/examples/tricky-type-checking.tra index 4cc8037ba..ad69c33db 100644 --- a/transfer/examples/tricky-type-checking.tra +++ b/transfer/examples/tricky-type-checking.tra @@ -8,6 +8,12 @@ data Tree : Type -> Type where EInt : Integer -> Tree Integer EFoo : (A:Type) -> A -> Tree A +eval : (B : Type) -> Tree B -> Tree B +eval _ t = case t of + EAdd x y -> EInt (x+y) + EInt i -> EInt i + EFoo T x -> EFoo T x + strip : (B : Type) -> Tree B -> B strip _ t = case t of EAdd x y -> x+y |