GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-09 04:59:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

Transfer: some TODOs. Lots of minor fixes in type checking algorithm.

Browse Source
This commit is contained in:
bringert
2006-03-20 18:23:55 +00:00
parent 8d1543684a
commit 0419860b4e
3 changed files with 40 additions and 25 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
transfer/TODO
View File

@@ -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

57
transfer/doc/typesystem.tex
View File

@@ -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']
}

6
transfer/examples/tricky-type-checking.tra
View File

@@ -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