123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354 |
- E ::= n
- | x
- | f(E…)
- | let x = E in E
- P ::= int | intptr[l]
- C ::= P(x) | C & C | ⊤
- Σ ::= l…; x… ⊢ C
- Γ ::= ε | Γ,f(Σ)→Σ | Γ,y | Γ,x:=α
- W ::= ε | E:W | apply[f]:W | let[x,E]:W | drop[x]:W
- S ::= ε | α:S
- Defn [ <Γ;C;S;W> → <Γ;C;S;W> ]
- x:=y in Γ
- ------------
- <Γ; C; S; x:W> → <Γ; C; y:S; W>
- x free in Γ
- ------------
- <Γ; C; S; n:W> → <Γ,x; C & int(x); x:S; W>
- ------------
- <Γ; C; S; f(E…):W> → <Γ; C; S; E…:apply[f]:W>
- ------------
- <Γ; C; S; (let x = E1 in E2):W> → <Γ; C; S; E1:bind[x]:E2:drop[x]:W>
- y free in Γ
- Γ ⊢ f(x…) → l…; y : C' ⇒ C"
- ⊢ C' ⊆ C
- ----------------------------------------
- <Γ; C; x…:S; apply[f]:W> → <Γ,l…,y; (C & C"); y:S; W>
- ----------------------------------------
- <Γ; C; y:S; bind[x]:W> → <Γ,x:=y; C; S; W>
- f<N>(vec: Vec<A, N+1>)
- let x: Vec<A, M+1>
- f(x)
- N + 1
- M + 2
- M = 1 + N
|