Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
b744911d
Commit
b744911d
authored
Oct 28, 2020
by
Mickael Laurent
Browse files
simplify grammar
parent
8df46b7f
Changes
1
Hide whitespace changes
Inline
Side-by-side
new_system2.tex
View file @
b744911d
...
...
@@ -8,10 +8,9 @@
\begin{equation}
\label
{
expressions2
}
\begin{array}
{
lrclr
}
\textbf
{
Atomic Expr
}
&
a
&
::=
&
c
\alt
x
\alt\lambda
x:t.e
\alt
(a,a)
\\
[.3mm]
\textbf
{
U-Expr
}
&
u
&
::=
&
x x
\alt
\tcase
{
x
}{
t
}{
e
}{
e
}
\alt
\pi
_
i x
\\
[.3mm]
\textbf
{
P-Expr
}
&
p
&
::=
&
u
\alt
a
\\
[.3mm]
\textbf
{
Expressions
}
&
e
&
::=
&
\letexp
{
x
}{
p
}{
e
}
\alt
p
\\
[.3mm]
\textbf
{
Atomic expr
}
&
a
&
::=
&
c
\alt
x
\alt\lambda
x:t.e
\alt
(x,x)
\alt
x x
\alt
\tcase
{
x
}{
t
}{
e
}{
e
}
\alt
\pi
_
i x
\\
[.3mm]
\textbf
{
Expressions
}
&
e
&
::=
&
\letexp
{
x
}{
a
}{
e
}
\alt
a
\\
[.3mm]
\textbf
{
Values
}
&
v
&
::=
&
c
\alt\lambda
x:t.e
\alt
(v,v)
\\
\end{array}
\end{equation}
...
...
@@ -25,8 +24,6 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
TODO: Should we allow expr as let definition?
TODO: Simplify pairs (only with variables) + simplify grammar accordingly (no need to distinguish a and u)
\subsection
{
Typing rules
}
\begin{mathpar}
...
...
@@ -61,8 +58,8 @@ TODO: Simplify pairs (only with variables) + simplify grammar accordingly (no ne
{
}
\qquad
\Infer
[Pair]
{
\Gamma
\vdash
a
_
1:t
_
1
\and
\Gamma
\vdash
a
_
2:t
_
2
}
{
\Gamma
\vdash
(
a
_
1,
a
_
2):
\pair
{
t
_
1
}
{
t
_
2
}}
{
\Gamma
\vdash
x
_
1:t
_
1
\and
\Gamma
\vdash
x
_
2:t
_
2
}
{
\Gamma
\vdash
(
x
_
1,
x
_
2):
\pair
{
t
_
1
}
{
t
_
2
}}
{
}
\\
\Infer
[App]
...
...
@@ -110,7 +107,7 @@ TODO: Simplify pairs (only with variables) + simplify grammar accordingly (no ne
{
\Gamma
,(x:u)
\vdash
e:t
}
{
\Gamma\vdash
_{
u
}
\letexp
x
p
e : t
\Gamma\vdash
_{
u
}
\letexp
x
a
e : t
}
{
}
\\
...
...
@@ -118,21 +115,21 @@ TODO: Simplify pairs (only with variables) + simplify grammar accordingly (no ne
{
\Gamma
,(x:t')
\vdash
e
\triangleright
_
x
\dt\\
\dt
' =
\dt\cup\{
t'
\setminus\textstyle\bigcup
_{
u
\in\dt
}
u
\}\\
\forall
u
\in
\dt
'.
\ \Gamma\bvdash
{
p
}{
u
}
\{
t
_
u
^
i,
\Gamma
_
u
^
i
\}
_{
i
\in
I
_
u
}
\\
\forall
u
\in
\dt
'.
\ \forall
i
\in
I
_
u.
\ \Gamma
_
u
^
i
\vdash
_{
t
_
u
^
i
}
\letexp
x
p
e : t
}
\forall
u
\in
\dt
'.
\ \Gamma\bvdash
{
a
}{
u
}
\{
t
_
u
^
i,
\Gamma
_
u
^
i
\}
_{
i
\in
I
_
u
}
\\
\forall
u
\in
\dt
'.
\ \forall
i
\in
I
_
u.
\ \Gamma
_
u
^
i
\vdash
_{
t
_
u
^
i
}
\letexp
x
a
e : t
}
{
\Gamma\vdash
_{
t'
}
\letexp
x
p
e : t
\Gamma\vdash
_{
t'
}
\letexp
x
a
e : t
}
{
}
\\
\Infer
[Let]
{
%\Gamma\cvdash p:\{(t_i,\Gamma_i)\}_{i\in I}\\
%\forall i\in I.\ \Gamma_i\vdash_{t_i}\letexp x p e : t
\Gamma\vdash
p
:s
\\
\Gamma\vdash
_{
s
}
\letexp
x
p
e : t
\Gamma\vdash
a
:s
\\
\Gamma\vdash
_{
s
}
\letexp
x
a
e : t
}
{
\Gamma\vdash\letexp
x
p
e : t
\Gamma\vdash\letexp
x
a
e : t
}
{
}
\end{mathpar}
...
...
@@ -188,8 +185,8 @@ TODO: Algorithmic rules
\\
\Infer
[Pair]
{
i
\in\{
1,2
\}\\
\Gamma
\vdash
a
_
i
\triangleright
_
x
\dt
}
{
\Gamma
\vdash
(
a
_
1,
a
_
2)
\triangleright
_
x
\dt
}
\Gamma
\vdash
x
_
i
\triangleright
_
x
\dt
}
{
\Gamma
\vdash
(
x
_
1,
x
_
2)
\triangleright
_
x
\dt
}
{}
\\
\Infer
[ProjDom]
...
...
@@ -223,7 +220,7 @@ TODO: Algorithmic rules
{
\Gamma\vdash
\tcase
{
y
}{
t
}{
e
_
1
}{
e
_
2
}
\triangleright
_
x
\dt
}
{}
\\
\Infer
[App
1
]
\Infer
[App
L
]
{
\Gamma
\vdash
x : t
\\
t
\land
(
\arrow
{
\Empty
}{
\Any
}
)
\equiv
\textstyle
{
\bigvee
_{
i
\in
I
}
t
_
i
}
...
...
@@ -231,7 +228,7 @@ TODO: Algorithmic rules
{
\Gamma
\vdash
x y
\triangleright
_
x
\textstyle
{
\bigcup
_{
i
\in
I
}
\{
t
_
i
\}
}}
{}
\qquad
\Infer
[App
2
]
\Infer
[App
R
]
{
\Gamma
\vdash
y :
\arrow
{
s
}{
t
}
}
...
...
@@ -243,7 +240,7 @@ TODO: Algorithmic rules
{
\Gamma
\vdash
y z
\triangleright
_
x
\{\}
}
{}
\\
\Infer
[App
2
*]
\Infer
[App
R
*]
{
\Gamma
\vdash
y :
\textstyle
{
\bigwedge
_{
i
\in
I
}
s
_
i
\to
t
_
i
}
}
...
...
@@ -253,9 +250,9 @@ TODO: Algorithmic rules
\Infer
[LetBase]
{
\Gamma
, (y:u)
\vdash
e
\triangleright
_
y
\dt\\
\forall
v
\in
\dt
.
\ \Gamma\fvdash
{
p
}{
v
}
\{
(
\_
,
\Gamma
_
v
^
i)
\}
_{
i
\in
I
_
v
}
\forall
v
\in
\dt
.
\ \Gamma\fvdash
{
a
}{
v
}
\{
(
\_
,
\Gamma
_
v
^
i)
\}
_{
i
\in
I
_
v
}
}{
\Gamma\vdash
_{
u
}
\letexp
y
p
e
\triangleright
_
x
\textstyle
{
\Gamma\vdash
_{
u
}
\letexp
y
a
e
\triangleright
_
x
\textstyle
{
\bigcup
_{
v
\in
\dt
}
\bigcup
_{
i
\in
I
_
v
}
\{\Gamma
_
v
^
i(x)
\}
}}
{
}
...
...
@@ -263,31 +260,31 @@ TODO: Algorithmic rules
\Infer
[LetSplit]
{
\Gamma
,(y:t')
\vdash
e
\triangleright
_
y
\dt\\
\forall
u
\in
\dt
.
\ \Gamma\bvdash
{
p
}{
u
}
\{
t
_
u
^
i,
\Gamma
_
u
^
i
\}
_{
i
\in
I
_
u
}
\\
\forall
u
\in
\dt
.
\ \forall
i
\in
I
_
u.
\ \Gamma
_
u
^
i
\vdash
_{
t
_
u
^
i
}
\letexp
x
p
e
\triangleright
_
x
\dt
_
u
^
i
\forall
u
\in
\dt
.
\ \Gamma\bvdash
{
a
}{
u
}
\{
t
_
u
^
i,
\Gamma
_
u
^
i
\}
_{
i
\in
I
_
u
}
\\
\forall
u
\in
\dt
.
\ \forall
i
\in
I
_
u.
\ \Gamma
_
u
^
i
\vdash
_{
t
_
u
^
i
}
\letexp
x
a
e
\triangleright
_
x
\dt
_
u
^
i
}
{
\Gamma\vdash
_{
t'
}
\letexp
y
p
e
\triangleright
_
x
\textstyle\bigcup
_{
u
\in
\dt
}
\bigcup
_{
i
\in
I
_
u
}
\dt
_
u
^
i
\Gamma\vdash
_{
t'
}
\letexp
y
a
e
\triangleright
_
x
\textstyle\bigcup
_{
u
\in
\dt
}
\bigcup
_{
i
\in
I
_
u
}
\dt
_
u
^
i
}
{
}
\\
\Infer
[LetDef]
{
\Gamma\vdash
p
\triangleright
_
x
\dt
\Gamma\vdash
a
\triangleright
_
x
\dt
}
{
\Gamma\vdash\letexp
y
p
e
\triangleright
_
x
\dt
\Gamma\vdash\letexp
y
a
e
\triangleright
_
x
\dt
}
{
}
\qquad
\Infer
[Let]
{
%\Gamma\cvdash p:\{(t_i,\Gamma_i)\}_{i\in I}\\
%\forall i\in I.\ \Gamma_i\vdash_{t_i}\letexp x p e \triangleright_x \dt_i
\Gamma\vdash
p
:s
\\
\Gamma\vdash
_{
s
}
\letexp
x
p
e
\triangleright
_
x
\dt
\Gamma\vdash
a
:s
\\
\Gamma\vdash
_{
s
}
\letexp
x
a
e
\triangleright
_
x
\dt
}
{
\Gamma\vdash\letexp
y
p
e
\triangleright
_
x
\dt
%\textstyle\bigcup_{i\in I} \dt_i
\Gamma\vdash\letexp
y
a
e
\triangleright
_
x
\dt
%\textstyle\bigcup_{i\in I} \dt_i
}
{
}
\end{mathpar}
...
...
@@ -368,9 +365,14 @@ TODO: Algorithmic rules
{
}
\\
\Infer
[Pair]
{
\forall
i
\in
I.
\ \Gamma\bvdash
{
a
_
1
}{
t
_
i
}
\{
(t
_
i
^
j,
\Gamma
_{
1,i
}^
j)
\}
_{
j
\in
J
_
i
}
\\
\forall
i
\in
I.
\ \Gamma\bvdash
{
a
_
2
}{
s
_
i
}
\{
(s
_
i
^
k,
\Gamma
_{
2,i
}^
k)
\}
_{
k
\in
K
_
i
}}
{
\Gamma\bvdash
{
(a
_
1,a
_
2)
}
{
\bigcup
_{
i
\in
I
}
(t
_
i,s
_
i)
}
\bigcup
_{
i
\in
I
}
\{
(
\pair
{
t
_
i
^
j
}{
s
_
i
^
k
}
,
\Gamma
_{
1,i
}^
j
\land\Gamma
_{
2,i
}^
k)
\
|
\
j
\in
J
_
i, k
\in
K
_
i
\}
}
{
%\forall i\in I.\ \Gamma\bvdash{x_1}{t_i}\{(t_i^j,\Gamma_{1,i}^j)\}_{j\in J_i}\\
\Gamma\vdash
x
_
1:t
_
\circ\\
\Gamma\vdash
x
_
2:s
_
\circ\\
\forall
i
\in
I.
\ \Gamma
_
1
^
i =
\Gamma\subst
{
x
_
1
}{
t
_
\circ\land
t
_
i
}
\\
%\forall i\in I.\ \Gamma\bvdash{x_2}{s_i}\{(s_i^k,\Gamma_{2,i}^k)\}_{k\in K_i}
\forall
i
\in
I.
\ \Gamma
_
2
^
i =
\Gamma\subst
{
x
_
2
}{
s
_
\circ\land
s
_
i
}
\\
}
{
\Gamma\bvdash
{
(x
_
1,x
_
2)
}
{
\bigcup
_{
i
\in
I
}
(t
_
i,s
_
i)
}
\bigcup
_{
i
\in
I
}
\{
(
\pair
{
(t
_
\circ\land
t
_
i)
}{
(s
_
\circ\land
s
_
i)
}
,
\Gamma
_
1
^
i
\land\Gamma
_
2
^
i)
\}
}
{
}
\\
\Infer
[Proj]
...
...
@@ -418,7 +420,7 @@ TODO: Algorithmic rules
\Gamma
,(x:s)
\bvdash
{
e
}{
t
}
\{
(t
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
}
{
\Gamma\ubvdash
{
s
}{
\letexp
{
x
}{
p
}{
e
}}{
t
}
\{
(t
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\Gamma\ubvdash
{
s
}{
\letexp
{
x
}{
a
}{
e
}}{
t
}
\{
(t
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
}
{
}
\\
...
...
@@ -426,20 +428,20 @@ TODO: Algorithmic rules
{
\Gamma
,(x:s)
\vdash
e
\triangleright
_
x
\dt\\
\dt
' =
\dt\cup\{
s
\setminus\textstyle\bigcup
_{
u
\in\dt
}
u
\}\\
\forall
u
\in
\dt
'.
\ \Gamma\bvdash
{
p
}{
u
}
\{
t
_
u
^
i,
\Gamma
_
u
^
i
\}
_{
i
\in
I
_
u
}
\\
\forall
u
\in
\dt
'.
\ \forall
i
\in
I
_
u.
\ \Gamma\ubvdash
{
u
}{
\letexp
{
x
}{
p
}{
e
}}{
t
}
\{
(t
_
i
^
j,
\Gamma
_
i
^
j)
\}
_{
j
\in
J
_
i
}}
\forall
u
\in
\dt
'.
\ \Gamma\bvdash
{
a
}{
u
}
\{
t
_
u
^
i,
\Gamma
_
u
^
i
\}
_{
i
\in
I
_
u
}
\\
\forall
u
\in
\dt
'.
\ \forall
i
\in
I
_
u.
\ \Gamma\ubvdash
{
u
}{
\letexp
{
x
}{
a
}{
e
}}{
t
}
\{
(t
_
i
^
j,
\Gamma
_
i
^
j)
\}
_{
j
\in
J
_
i
}}
{
\Gamma\ubvdash
{
s
}{
\letexp
{
x
}{
p
}{
e
}}{
t
}
\bigcup
_{
u
\in\dt
'
}
\bigcup
_{
i
\in
I
_
u
}
\{
(t
_
i
^
j,
\Gamma
_
i
^
j)
\}
_{
j
\in
J
_
i
}
\Gamma\ubvdash
{
s
}{
\letexp
{
x
}{
a
}{
e
}}{
t
}
\bigcup
_{
u
\in\dt
'
}
\bigcup
_{
i
\in
I
_
u
}
\{
(t
_
i
^
j,
\Gamma
_
i
^
j)
\}
_{
j
\in
J
_
i
}
}
{
}
\\
\Infer
[Let]
{
\Gamma\vdash
p
:s
\\
\Gamma\ubvdash
{
s
}{
\letexp
{
x
}{
p
}{
e
}}{
t
}
\{
(t
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\Gamma\vdash
a
:s
\\
\Gamma\ubvdash
{
s
}{
\letexp
{
x
}{
a
}{
e
}}{
t
}
\{
(t
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
}
{
\Gamma\bvdash
{
\letexp
{
x
}{
p
}{
e
}}{
t
}
\{
(t
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\Gamma\bvdash
{
\letexp
{
x
}{
a
}{
e
}}{
t
}
\{
(t
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
}
{
}
\end{mathpar}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment
