dead end for Raw, hard to convert to Scoped
This commit is contained in:
wadler
parent
dfad6e0822
commit
8afc6f9ce0
6 changed files with 967 additions and 120 deletions
|
|
@ -39,12 +39,7 @@ open import Relation.Nullary.Product using (_×-dec_)
|
|||
## Collections
|
||||
|
||||
\begin{code}
|
||||
infix 0 _↔_
|
||||
|
||||
_↔_ : Set → Set → Set
|
||||
A ↔ B = (A → B) × (B → A)
|
||||
|
||||
module CollectionDec (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
|
||||
module Collections (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
|
||||
|
||||
Coll : Set → Set
|
||||
Coll A = List A
|
||||
|
|
|
|||
421
src/Raw.lagda
421
src/Raw.lagda
|
|
@ -21,8 +21,8 @@ open import Data.Empty using (⊥; ⊥-elim)
|
|||
open import Data.List using (List; []; _∷_; _++_; map; foldr; filter; length)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_)
|
||||
import Data.String as String
|
||||
open import Data.String using (String)
|
||||
-- open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.String using (String; _≟_)
|
||||
open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||
-- open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
-- open import Function using (_∘_)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
|
|
@ -35,6 +35,7 @@ pattern [_,_,_] w x y = w ∷ x ∷ y ∷ []
|
|||
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
|
||||
\end{code}
|
||||
|
||||
|
||||
## First development: Raw
|
||||
|
||||
\begin{code}
|
||||
|
|
@ -54,9 +55,9 @@ module Raw where
|
|||
`ℕ : Type
|
||||
_`→_ : Type → Type → Type
|
||||
|
||||
data Env : Set where
|
||||
ε : Env
|
||||
_,_`:_ : Env → Id → Type → Env
|
||||
data Ctx : Set where
|
||||
ε : Ctx
|
||||
_,_`:_ : Ctx → Id → Type → Ctx
|
||||
|
||||
data Term : Set where
|
||||
⌊_⌋ : Id → Term
|
||||
|
|
@ -83,10 +84,7 @@ module Raw where
|
|||
### Lists of identifiers
|
||||
|
||||
\begin{code}
|
||||
_≟_ : ∀ (x : Id) (y : Id) → Dec (x ≡ y)
|
||||
_≟_ = String._≟_
|
||||
|
||||
open Collections.CollectionDec (Id) (_≟_)
|
||||
open Collections (Id) (_≟_)
|
||||
\end{code}
|
||||
|
||||
### Free variables
|
||||
|
|
@ -180,22 +178,46 @@ module Raw where
|
|||
### Values
|
||||
|
||||
\begin{code}
|
||||
data Value : Term → Set where
|
||||
data Natural : Term → Set where
|
||||
|
||||
Zero :
|
||||
----------
|
||||
Value `zero
|
||||
--------------
|
||||
Natural `zero
|
||||
|
||||
Suc : ∀ {V}
|
||||
→ Natural V
|
||||
-----------------
|
||||
→ Natural (`suc V)
|
||||
|
||||
data Value : Term → Set where
|
||||
|
||||
Nat : ∀ {V}
|
||||
→ Natural V
|
||||
----------
|
||||
→ Value V
|
||||
--------------
|
||||
→ Value (`suc V)
|
||||
|
||||
|
||||
Fun : ∀ {x N}
|
||||
-----------------
|
||||
→ Value (`λ x `→ N)
|
||||
\end{code}
|
||||
|
||||
### Decide whether a term is a value
|
||||
|
||||
Not needed, and no longer correct.
|
||||
|
||||
\begin{code}
|
||||
{-
|
||||
value : ∀ (M : Term) → Dec (Value M)
|
||||
value ⌊ x ⌋ = no (λ())
|
||||
value (`λ x `→ N) = yes Fun
|
||||
value (L · M) = no (λ())
|
||||
value `zero = yes Zero
|
||||
value (`suc M) with value M
|
||||
... | yes VM = yes (Suc VM)
|
||||
... | no ¬VM = no (λ{(Suc VM) → (¬VM VM)})
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
### Reduction
|
||||
|
||||
\begin{code}
|
||||
|
|
@ -249,6 +271,33 @@ module Raw where
|
|||
begin M⟶*N = M⟶*N
|
||||
\end{code}
|
||||
|
||||
### Decide whether a term reduces
|
||||
|
||||
\begin{code}
|
||||
{-
|
||||
data Step (M : Term) : Set where
|
||||
step : ∀ {N}
|
||||
→ M ⟶ N
|
||||
-------
|
||||
→ Step M
|
||||
|
||||
reduce : ∀ (M : Term) → Dec (Step M)
|
||||
reduce ⌊ x ⌋ = no (λ{(step ())})
|
||||
reduce (`λ x `→ N) = no (λ{(step ())})
|
||||
reduce (L · M) with reduce L
|
||||
... | yes (step L⟶L′) = yes (step (ξ-·₁ L⟶L′))
|
||||
... | no ¬L⟶L′ with value L
|
||||
... | no ¬VL = no (λ{ (step (β-→ _)) → (¬VL Fun)
|
||||
; (step (ξ-·₁ L⟶L′)) → (¬L⟶L′ (step L⟶L′))
|
||||
; (step (ξ-·₂ VL _)) → (¬VL VL) })
|
||||
... | yes VL with reduce M
|
||||
... | yes (step M⟶M′) = yes (step (ξ-·₂ VL M⟶M′))
|
||||
... | no ¬M⟶M′ = {!!}
|
||||
reduce `zero = {!!}
|
||||
reduce (`suc M) = {!!}
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
### Stuck terms
|
||||
|
||||
\begin{code}
|
||||
|
|
@ -265,14 +314,14 @@ module Raw where
|
|||
--------------
|
||||
→ Stuck (V · M)
|
||||
|
||||
st-·-zero : ∀ {M}
|
||||
------------------
|
||||
→ Stuck (`zero · M)
|
||||
st-·-nat : ∀ {V M}
|
||||
→ Natural V
|
||||
--------------
|
||||
→ Stuck (V · M)
|
||||
|
||||
st-·-suc : ∀ {V M}
|
||||
→ Value V
|
||||
-------------------
|
||||
→ Stuck (`suc V · M)
|
||||
st-suc-λ : ∀ {x N}
|
||||
-------------------------
|
||||
→ Stuck (`suc (`λ x `→ N))
|
||||
|
||||
st-suc : ∀ {M}
|
||||
→ Stuck M
|
||||
|
|
@ -280,6 +329,42 @@ module Raw where
|
|||
→ Stuck (`suc M)
|
||||
\end{code}
|
||||
|
||||
### Closed terms
|
||||
|
||||
\begin{code}
|
||||
Closed : Term → Set
|
||||
Closed M = free M ≡ []
|
||||
|
||||
Ax-lemma : ∀ {x} → ¬ (Closed ⌊ x ⌋)
|
||||
Ax-lemma ()
|
||||
|
||||
closed-·₁ : ∀ {L M} → Closed (L · M) → Closed L
|
||||
closed-·₁ r = lemma r
|
||||
where
|
||||
lemma : ∀ {A : Set} {xs ys : List A} → xs ++ ys ≡ [] → xs ≡ []
|
||||
lemma {xs = []} _ = refl
|
||||
lemma {xs = x ∷ xs} ()
|
||||
|
||||
closed-·₂ : ∀ {L M} → Closed (L · M) → Closed M
|
||||
closed-·₂ r = lemma r
|
||||
where
|
||||
lemma : ∀ {A : Set} {xs ys : List A} → xs ++ ys ≡ [] → ys ≡ []
|
||||
lemma {xs = []} refl = refl
|
||||
lemma {xs = x ∷ xs} ()
|
||||
|
||||
·-closed : ∀ {L M} → Closed L → Closed M → Closed (L · M)
|
||||
·-closed r s = lemma r s
|
||||
where
|
||||
lemma : ∀ {A : Set} {xs ys : List A} → xs ≡ [] → ys ≡ [] → xs ++ ys ≡ []
|
||||
lemma refl refl = refl
|
||||
|
||||
closed-suc : ∀ {M} → Closed (`suc M) → Closed M
|
||||
closed-suc r = r
|
||||
|
||||
suc-closed : ∀ {M} → Closed M → Closed (`suc M)
|
||||
suc-closed r = r
|
||||
\end{code}
|
||||
|
||||
### Progress
|
||||
|
||||
\begin{code}
|
||||
|
|
@ -290,74 +375,78 @@ module Raw where
|
|||
-----------
|
||||
→ Progress M
|
||||
|
||||
done :
|
||||
Value M
|
||||
-----------
|
||||
→ Progress M
|
||||
|
||||
stuck :
|
||||
Stuck M
|
||||
-----------
|
||||
→ Progress M
|
||||
\end{code}
|
||||
|
||||
I can show that every closed term makes progess in the above sense,
|
||||
and then use that to compute the normal form of a term.
|
||||
|
||||
### Closed terms
|
||||
|
||||
\begin{code}
|
||||
Closed : Term → Set
|
||||
Closed M = free M ≡ []
|
||||
|
||||
Ax-lemma : ∀ {x} → ¬ (Closed ⌊ x ⌋)
|
||||
Ax-lemma ()
|
||||
|
||||
·-lemma₁ : ∀ {L M} → Closed (L · M) → Closed L
|
||||
·-lemma₁ r = lemma r
|
||||
where
|
||||
lemma : ∀ {A : Set} {xs ys : List A} → xs ++ ys ≡ [] → xs ≡ []
|
||||
lemma {xs = []} _ = refl
|
||||
lemma {xs = x ∷ xs} ()
|
||||
|
||||
·-lemma₂ : ∀ {L M} → Closed (L · M) → Closed M
|
||||
·-lemma₂ r = lemma r
|
||||
where
|
||||
lemma : ∀ {A : Set} {xs ys : List A} → xs ++ ys ≡ [] → ys ≡ []
|
||||
lemma {xs = []} refl = refl
|
||||
lemma {xs = x ∷ xs} ()
|
||||
|
||||
suc-lemma : ∀ {M} → Closed (`suc M) → Closed M
|
||||
suc-lemma r = r
|
||||
done :
|
||||
Value M
|
||||
-----------
|
||||
→ Progress M
|
||||
\end{code}
|
||||
|
||||
### Progress
|
||||
|
||||
\begin{code}
|
||||
progress : ∀ (M : Term) → Closed M → Progress M
|
||||
progress ⌊ x ⌋ Cx = ⊥-elim (Ax-lemma Cx)
|
||||
progress (L · M) CLM with progress L (·-lemma₁ {L} {M} CLM)
|
||||
... | step L⟶L′ = step (ξ-·₁ L⟶L′)
|
||||
... | stuck SL = stuck (st-·₁ SL)
|
||||
... | done VL with progress M (·-lemma₂ {L} {M} CLM)
|
||||
... | step M⟶M′ = step (ξ-·₂ VL M⟶M′)
|
||||
... | stuck SM = stuck (st-·₂ VL SM)
|
||||
progress ⌊ x ⌋ Cx = ⊥-elim (Ax-lemma Cx)
|
||||
progress (L · M) CLM with progress L (closed-·₁ {L} {M} CLM)
|
||||
... | step L⟶L′ = step (ξ-·₁ L⟶L′)
|
||||
... | stuck SL = stuck (st-·₁ SL)
|
||||
... | done VL with progress M (closed-·₂ {L} {M} CLM)
|
||||
... | step M⟶M′ = step (ξ-·₂ VL M⟶M′)
|
||||
... | stuck SM = stuck (st-·₂ VL SM)
|
||||
... | done VM with VL
|
||||
... | Zero = stuck st-·-zero
|
||||
... | Suc VL′ = stuck (st-·-suc VL′)
|
||||
... | Fun = step (β-→ VM)
|
||||
progress (`λ x `→ N) CxN = done Fun
|
||||
progress `zero Cz = done Zero
|
||||
progress (`suc M) CsM with progress M (suc-lemma {M} CsM)
|
||||
... | step M⟶M′ = step (ξ-suc M⟶M′)
|
||||
... | stuck SM = stuck (st-suc SM)
|
||||
... | done VM = done (Suc VM)
|
||||
... | Nat NL = stuck (st-·-nat NL)
|
||||
... | Fun = step (β-→ VM)
|
||||
progress (`λ x `→ N) CxN = done Fun
|
||||
progress `zero Cz = done (Nat Zero)
|
||||
progress (`suc M) CsM with progress M (closed-suc {M} CsM)
|
||||
... | step M⟶M′ = step (ξ-suc M⟶M′)
|
||||
... | stuck SM = stuck (st-suc SM)
|
||||
... | done (Nat NL) = done (Nat (Suc NL))
|
||||
... | done Fun = stuck st-suc-λ
|
||||
\end{code}
|
||||
|
||||
### Repeated progress
|
||||
### Preservation
|
||||
|
||||
Preservation of closed terms is not so easy.
|
||||
|
||||
\begin{code}
|
||||
preservation : ∀ {M N : Term} → Closed M → M ⟶ N → Closed N
|
||||
preservation = {!!}
|
||||
{-
|
||||
preservation CLM (ξ-·₁ L⟶L′)
|
||||
= ·-closed (preservation (closed-·₁ CLM) L⟶L′) (closed-·₂ CLM)
|
||||
preservation CLM (ξ-·₂ _ M⟶M′)
|
||||
= ·-closed (closed-·₁ CLM) (preservation (closed-·₂ CLM) M⟶M′)
|
||||
preservation CM (β-→ VM) = {!!} -- requires closure under substitution!
|
||||
preservation CM (ξ-suc M⟶M′)
|
||||
= suc-closed (preservation (closed-suc CM) M⟶M′)
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
### Evaluation
|
||||
|
||||
\begin{code}
|
||||
Gas : Set
|
||||
Gas = ℕ
|
||||
|
||||
data Eval (M : Term) : Set where
|
||||
out-of-gas : ∀ {N} → M ⟶* N → Eval M
|
||||
stuck : ∀ {N} → M ⟶* N → Stuck N → Eval M
|
||||
done : ∀ {V} → M ⟶* V → Value V → Eval M
|
||||
|
||||
eval : Gas → (L : Term) → Closed L → Eval L
|
||||
eval zero L CL = out-of-gas (L ∎)
|
||||
eval (suc n) L CL with progress L CL
|
||||
... | stuck SL = stuck (L ∎) SL
|
||||
... | done VL = done (L ∎) VL
|
||||
... | step {M} L⟶M with eval n M (preservation CL L⟶M)
|
||||
... | out-of-gas M⟶*N = out-of-gas (L ⟶⟨ L⟶M ⟩ M⟶*N)
|
||||
... | stuck M⟶*N SN = stuck (L ⟶⟨ L⟶M ⟩ M⟶*N) SN
|
||||
... | done M⟶*V VV = done (L ⟶⟨ L⟶M ⟩ M⟶*V) VV
|
||||
\end{code}
|
||||
|
||||
|
||||
|
|
@ -367,44 +456,176 @@ and then use that to compute the normal form of a term.
|
|||
module Scoped where
|
||||
\end{code}
|
||||
|
||||
### Syntax
|
||||
|
||||
\begin{code}
|
||||
infix 4 _⊢*
|
||||
infix 4 _∋*
|
||||
infixl 5 _,*
|
||||
infix 5 `λ_`→_
|
||||
infixl 6 _·_
|
||||
infix 7 S_
|
||||
|
||||
Id : Set
|
||||
Id = String
|
||||
|
||||
data Ctx : Set where
|
||||
ε : Ctx
|
||||
_,* : Ctx → Ctx
|
||||
|
||||
data _∋* : Ctx → Set where
|
||||
|
||||
Z : ∀ {Γ}
|
||||
------------
|
||||
→ Γ ,* ∋*
|
||||
|
||||
S_ : ∀ {Γ}
|
||||
→ Γ ∋*
|
||||
--------
|
||||
→ Γ ,* ∋*
|
||||
|
||||
data _⊢* : Ctx → Set where
|
||||
|
||||
⌊_⌋ : ∀ {Γ}
|
||||
→ Γ ∋*
|
||||
-----
|
||||
→ Γ ⊢*
|
||||
|
||||
`λ_`→_ : ∀ {Γ} (x : Id)
|
||||
→ Γ ,* ⊢*
|
||||
--------
|
||||
→ Γ ⊢*
|
||||
|
||||
_·_ : ∀ {Γ}
|
||||
→ Γ ⊢*
|
||||
→ Γ ⊢*
|
||||
-----
|
||||
→ Γ ⊢*
|
||||
|
||||
`zero : ∀ {Γ}
|
||||
-----
|
||||
→ Γ ⊢*
|
||||
|
||||
`suc : ∀ {Γ}
|
||||
→ Γ ⊢*
|
||||
-----
|
||||
→ Γ ⊢*
|
||||
\end{code}
|
||||
|
||||
## Conversion: Raw to Scoped
|
||||
|
||||
\begin{code}
|
||||
infix 4 _∈_
|
||||
|
||||
data _∈_ : Id → List Id → Set where
|
||||
|
||||
here : ∀ {x xs} →
|
||||
----------
|
||||
x ∈ x ∷ xs
|
||||
|
||||
there : ∀ {w x xs} →
|
||||
w ∈ xs →
|
||||
----------
|
||||
w ∈ x ∷ xs
|
||||
|
||||
_?∈_ : ∀ (x : Id) (xs : List Id) → Dec (x ∈ xs)
|
||||
x ?∈ [] = no (λ())
|
||||
x ?∈ (y ∷ ys) with x ≟ y
|
||||
... | yes refl = yes here
|
||||
... | no x≢ with x ?∈ ys
|
||||
... | yes x∈ = yes (there x∈)
|
||||
... | no x∉ = no (λ{ here → x≢ refl
|
||||
; (there x∈) → x∉ x∈
|
||||
})
|
||||
|
||||
distinct : List Id → List Id
|
||||
distinct [] = []
|
||||
distinct (x ∷ xs) with x ?∈ distinct xs
|
||||
... | yes x∈ = distinct xs
|
||||
... | no x∉ = x ∷ distinct xs
|
||||
|
||||
context : Raw.Term → Ctx
|
||||
context M = helper (distinct (Raw.free M))
|
||||
where
|
||||
helper : List Id → Ctx
|
||||
helper [] = ε
|
||||
helper (x ∷ xs) = helper xs ,*
|
||||
|
||||
raw→scoped : (M : Raw.Term) → (context M ⊢*)
|
||||
raw→scoped M = {!!}
|
||||
where
|
||||
|
||||
xs₀ = distinct (Raw.free M)
|
||||
|
||||
{-
|
||||
The following does not work because `context M` should shrink on recursive calls.
|
||||
|
||||
lookup : Id → (context M ⊢*)
|
||||
lookup w = helper w xs₀
|
||||
where
|
||||
helper : Id → List Id → (context M ⊢*)
|
||||
helper w [] = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
helper w (x ∷ xs) with w ≟ x
|
||||
... | yes _ = Z
|
||||
... | no _ = S (helper xs)
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
|
||||
|
||||
## Third development: Typed
|
||||
|
||||
\begin{code}
|
||||
module Typed where
|
||||
\end{code}
|
||||
infix 4 _⊢_
|
||||
infix 4 _∋_
|
||||
infixl 5 _,_
|
||||
infixr 5 _`→_
|
||||
infix 5 ƛ_`→_
|
||||
infixl 6 _·_
|
||||
infix 7 S_
|
||||
|
||||
infix 4 _∋_`:_
|
||||
infix 4 _⊢_`:_
|
||||
infixl 5 _,_`:_
|
||||
infixr 6 _`→_
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
_`→_ : Type → Type → Type
|
||||
|
||||
data _∋_`:_ : Env → Id → Type → Set where
|
||||
data _∋_ : Ctx → Type → Set where
|
||||
|
||||
Z : ∀ {Γ A x}
|
||||
--------------------
|
||||
→ Γ , x `: A ∋ x `: A
|
||||
Z : ∀ {Γ A}
|
||||
----------
|
||||
→ Γ , A ∋ A
|
||||
|
||||
S : ∀ {Γ A B x w}
|
||||
→ w ≢ x
|
||||
→ Γ ∋ w `: B
|
||||
--------------------
|
||||
→ Γ , x `: A ∋ w `: B
|
||||
S_ : ∀ {Γ A B}
|
||||
→ Γ ∋ B
|
||||
---------
|
||||
→ Γ , A ∋ B
|
||||
|
||||
data _⊢_`:_ : Env → Term → Type → Set where
|
||||
data _⊢_ : Ctx → Type → Set where
|
||||
|
||||
Ax : ∀ {Γ A x}
|
||||
→ Γ ∋ x `: A
|
||||
--------------
|
||||
→ Γ ⊢ ` x `: A
|
||||
⌊_⌋ : ∀ {Γ} {A}
|
||||
→ Γ ∋ A
|
||||
------
|
||||
→ Γ ⊢ A
|
||||
|
||||
⊢λ : ∀ {Γ x N A B}
|
||||
→ Γ , x `: A ⊢ N `: B
|
||||
--------------------------
|
||||
→ Γ ⊢ (`λ x `→ N) `: A `→ B
|
||||
`λ_`→_ : ∀ {Γ A B} (x : Id)
|
||||
→ Γ , A ⊢ B
|
||||
-----------
|
||||
→ Γ ⊢ A `→ B
|
||||
|
||||
_·_ : ∀ {Γ L M A B}
|
||||
→ Γ ⊢ L `: A `→ B
|
||||
→ Γ ⊢ M `: A
|
||||
----------------
|
||||
→ Γ ⊢ L · M `: B
|
||||
_·_ : ∀ {Γ} {A B}
|
||||
→ Γ ⊢ A `→ B
|
||||
→ Γ ⊢ A
|
||||
-----------
|
||||
→ Γ ⊢ B
|
||||
|
||||
`zero : ∀ {Γ}
|
||||
----------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`suc : ∀ {Γ}
|
||||
→ Γ ⊢ `ℕ
|
||||
-------
|
||||
→ Γ ⊢ `ℕ
|
||||
\end{code}
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
|
|||
open import Function using (_∘_)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Relation.Nullary.Negation using (¬?)
|
||||
open import Collections
|
||||
import Collections
|
||||
|
||||
pattern [_] x = x ∷ []
|
||||
pattern [_,_] x y = x ∷ y ∷ []
|
||||
|
|
@ -269,7 +269,7 @@ erase-lemma (⊢Y ⊢M) = cong `Y_ (erase-lemma ⊢M)
|
|||
### Lists as sets
|
||||
|
||||
\begin{code}
|
||||
open Collections.CollectionDec (Id) (_≟_)
|
||||
open Collections (Id) (_≟_)
|
||||
\end{code}
|
||||
|
||||
### Free variables
|
||||
|
|
|
|||
|
|
@ -29,24 +29,24 @@ open import Relation.Nullary.Product using (_×-dec_)
|
|||
## Syntax
|
||||
|
||||
\begin{code}
|
||||
infixl 6 _,_
|
||||
infix 4 _⊢_
|
||||
infix 4 _∋_
|
||||
infixl 5 _,_
|
||||
infixr 5 _⇒_
|
||||
infixl 5 _·_
|
||||
infix 6 S_
|
||||
infix 4 ƛ_
|
||||
infix 4 μ_
|
||||
infix 5 ƛ_
|
||||
infix 5 μ_
|
||||
infixl 6 _·_
|
||||
infix 7 S_
|
||||
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
_⇒_ : Type → Type → Type
|
||||
|
||||
data Env : Set where
|
||||
ε : Env
|
||||
_,_ : Env → Type → Env
|
||||
data Ctx : Set where
|
||||
ε : Ctx
|
||||
_,_ : Ctx → Type → Ctx
|
||||
|
||||
data _∋_ : Env → Type → Set where
|
||||
data _∋_ : Ctx → Type → Set where
|
||||
|
||||
Z : ∀ {Γ} {A}
|
||||
----------
|
||||
|
|
@ -57,7 +57,7 @@ data _∋_ : Env → Type → Set where
|
|||
---------
|
||||
→ Γ , A ∋ B
|
||||
|
||||
data _⊢_ : Env → Type → Set where
|
||||
data _⊢_ : Ctx → Type → Set where
|
||||
|
||||
⌊_⌋ : ∀ {Γ} {A}
|
||||
→ Γ ∋ A
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
|
|||
open import Function using (_∘_)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Relation.Nullary.Negation using (¬?)
|
||||
open import Collections
|
||||
import Collections
|
||||
|
||||
pattern [_] x = x ∷ []
|
||||
pattern [_,_] x y = x ∷ y ∷ []
|
||||
|
|
@ -270,7 +270,7 @@ erase-lemma (⊢Y ⊢M) = cong `Y_ (erase-lemma ⊢M)
|
|||
### Lists as sets
|
||||
|
||||
\begin{code}
|
||||
open Collections.CollectionDec (Id) (_≟_)
|
||||
open Collections (Id) (_≟_)
|
||||
\end{code}
|
||||
|
||||
### Free variables
|
||||
|
|
|
|||
631
src/extra/Raw-deadend.lagda
Normal file
631
src/extra/Raw-deadend.lagda
Normal file
|
|
@ -0,0 +1,631 @@
|
|||
---
|
||||
title : "Raw: Raw, Scoped, Typed"
|
||||
layout : page
|
||||
permalink : /Raw
|
||||
---
|
||||
|
||||
This version uses raw terms.
|
||||
|
||||
The substitution algorithm is based on one by McBride.
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
module Raw where
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.List using (List; []; _∷_; _++_; map; foldr; filter; length)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_)
|
||||
import Data.String as String
|
||||
open import Data.String using (String; _≟_)
|
||||
open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||
-- open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
-- open import Function using (_∘_)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Relation.Nullary.Negation using (¬?)
|
||||
import Collections
|
||||
|
||||
pattern [_] w = w ∷ []
|
||||
pattern [_,_] w x = w ∷ x ∷ []
|
||||
pattern [_,_,_] w x y = w ∷ x ∷ y ∷ []
|
||||
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
|
||||
\end{code}
|
||||
|
||||
|
||||
## First development: Raw
|
||||
|
||||
\begin{code}
|
||||
module Raw where
|
||||
\end{code}
|
||||
|
||||
### Syntax
|
||||
|
||||
\begin{code}
|
||||
infix 6 `λ_`→_
|
||||
infixl 9 _·_
|
||||
|
||||
Id : Set
|
||||
Id = String
|
||||
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
_`→_ : Type → Type → Type
|
||||
|
||||
data Ctx : Set where
|
||||
ε : Ctx
|
||||
_,_`:_ : Ctx → Id → Type → Ctx
|
||||
|
||||
data Term : Set where
|
||||
⌊_⌋ : Id → Term
|
||||
`λ_`→_ : Id → Term → Term
|
||||
_·_ : Term → Term → Term
|
||||
`zero : Term
|
||||
`suc : Term → Term
|
||||
\end{code}
|
||||
|
||||
### Example terms
|
||||
|
||||
\begin{code}
|
||||
two : Term
|
||||
two = `λ "s" `→ `λ "z" `→ ⌊ "s" ⌋ · (⌊ "s" ⌋ · ⌊ "z" ⌋)
|
||||
|
||||
plus : Term
|
||||
plus = `λ "m" `→ `λ "n" `→ `λ "s" `→ `λ "z" `→
|
||||
⌊ "m" ⌋ · ⌊ "s" ⌋ · (⌊ "n" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋)
|
||||
|
||||
norm : Term
|
||||
norm = `λ "m" `→ ⌊ "m" ⌋ · (`λ "x" `→ `suc ⌊ "x" ⌋) · `zero
|
||||
\end{code}
|
||||
|
||||
### Lists of identifiers
|
||||
|
||||
\begin{code}
|
||||
open Collections (Id) (_≟_)
|
||||
\end{code}
|
||||
|
||||
### Free variables
|
||||
|
||||
\begin{code}
|
||||
free : Term → List Id
|
||||
free (⌊ x ⌋) = [ x ]
|
||||
free (`λ x `→ N) = free N \\ x
|
||||
free (L · M) = free L ++ free M
|
||||
free (`zero) = []
|
||||
free (`suc M) = free M
|
||||
\end{code}
|
||||
|
||||
### Identifier maps
|
||||
|
||||
\begin{code}
|
||||
∅ : Id → Term
|
||||
∅ x = ⌊ x ⌋
|
||||
|
||||
infixl 5 _,_↦_
|
||||
|
||||
_,_↦_ : (Id → Term) → Id → Term → (Id → Term)
|
||||
(ρ , x ↦ M) w with w ≟ x
|
||||
... | yes _ = M
|
||||
... | no _ = ρ w
|
||||
\end{code}
|
||||
|
||||
### Fresh variables
|
||||
|
||||
\begin{code}
|
||||
fresh : List Id → Id → Id
|
||||
fresh xs₀ y = helper xs₀ (length xs₀) y
|
||||
where
|
||||
|
||||
prime : Id → Id
|
||||
prime x = x String.++ "′"
|
||||
|
||||
helper : List Id → ℕ → Id → Id
|
||||
helper [] _ w = w
|
||||
helper (x ∷ xs) n w with w ≟ x
|
||||
helper (x ∷ xs) n w | no _ = helper xs n w
|
||||
helper (x ∷ xs) (suc n) w | yes refl = helper xs₀ n (prime w)
|
||||
helper (x ∷ xs) zero w | yes refl = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
|
||||
\end{code}
|
||||
|
||||
### Substitution
|
||||
|
||||
\begin{code}
|
||||
subst : List Id → (Id → Term) → Term → Term
|
||||
subst ys ρ ⌊ x ⌋ = ρ x
|
||||
subst ys ρ (`λ x `→ N) = `λ y `→ subst (y ∷ ys) (ρ , x ↦ ⌊ y ⌋) N
|
||||
where
|
||||
y = fresh ys x
|
||||
subst ys ρ (L · M) = subst ys ρ L · subst ys ρ M
|
||||
subst ys ρ (`zero) = `zero
|
||||
subst ys ρ (`suc M) = `suc (subst ys ρ M)
|
||||
|
||||
_[_:=_] : Term → Id → Term → Term
|
||||
N [ x := M ] = subst (free M ++ (free N \\ x)) (∅ , x ↦ M) N
|
||||
\end{code}
|
||||
|
||||
### Testing substitution
|
||||
|
||||
\begin{code}
|
||||
_ : fresh [ "y" ] "y" ≡ "y′"
|
||||
_ = refl
|
||||
|
||||
_ : fresh [ "z" ] "y" ≡ "y"
|
||||
_ = refl
|
||||
|
||||
_ : (⌊ "s" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋) [ "z" := `zero ] ≡ (⌊ "s" ⌋ · ⌊ "s" ⌋ · `zero)
|
||||
_ = refl
|
||||
|
||||
_ : (`λ "y" `→ ⌊ "x" ⌋) [ "x" := ⌊ "z" ⌋ ] ≡ (`λ "y" `→ ⌊ "z" ⌋)
|
||||
_ = refl
|
||||
|
||||
_ : (`λ "y" `→ ⌊ "x" ⌋) [ "x" := ⌊ "y" ⌋ ] ≡ (`λ "y′" `→ ⌊ "y" ⌋)
|
||||
_ = refl
|
||||
|
||||
_ : (⌊ "s" ⌋ · ⌊ "s" ⌋ · ⌊ "z" ⌋) [ "s" := (`λ "m" `→ `suc ⌊ "m" ⌋) ]
|
||||
[ "z" := `zero ]
|
||||
≡ (`λ "m" `→ `suc ⌊ "m" ⌋) · (`λ "m" `→ `suc ⌊ "m" ⌋) · `zero
|
||||
_ = refl
|
||||
|
||||
_ : subst [] (∅ , "m" ↦ two , "n" ↦ `zero) (⌊ "m" ⌋ · ⌊ "n" ⌋) ≡ (two · `zero)
|
||||
_ = refl
|
||||
\end{code}
|
||||
|
||||
### Values
|
||||
|
||||
\begin{code}
|
||||
data Natural : Term → Set where
|
||||
|
||||
Zero :
|
||||
--------------
|
||||
Natural `zero
|
||||
|
||||
Suc : ∀ {V}
|
||||
→ Natural V
|
||||
-----------------
|
||||
→ Natural (`suc V)
|
||||
|
||||
data Value : Term → Set where
|
||||
|
||||
Nat : ∀ {V}
|
||||
→ Natural V
|
||||
----------
|
||||
→ Value V
|
||||
|
||||
Fun : ∀ {x N}
|
||||
-----------------
|
||||
→ Value (`λ x `→ N)
|
||||
\end{code}
|
||||
|
||||
### Decide whether a term is a value
|
||||
|
||||
Not needed, and no longer correct.
|
||||
|
||||
\begin{code}
|
||||
{-
|
||||
value : ∀ (M : Term) → Dec (Value M)
|
||||
value ⌊ x ⌋ = no (λ())
|
||||
value (`λ x `→ N) = yes Fun
|
||||
value (L · M) = no (λ())
|
||||
value `zero = yes Zero
|
||||
value (`suc M) with value M
|
||||
... | yes VM = yes (Suc VM)
|
||||
... | no ¬VM = no (λ{(Suc VM) → (¬VM VM)})
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
### Reduction
|
||||
|
||||
\begin{code}
|
||||
infix 4 _⟶_
|
||||
|
||||
data _⟶_ : Term → Term → Set where
|
||||
|
||||
ξ-·₁ : ∀ {L L′ M}
|
||||
→ L ⟶ L′
|
||||
----------------
|
||||
→ L · M ⟶ L′ · M
|
||||
|
||||
ξ-·₂ : ∀ {V M M′}
|
||||
→ Value V
|
||||
→ M ⟶ M′
|
||||
----------------
|
||||
→ V · M ⟶ V · M′
|
||||
|
||||
β-→ : ∀ {x N V}
|
||||
→ Value V
|
||||
--------------------------------
|
||||
→ (`λ x `→ N) · V ⟶ N [ x := V ]
|
||||
|
||||
ξ-suc : ∀ {M M′}
|
||||
→ M ⟶ M′
|
||||
------------------
|
||||
→ `suc M ⟶ `suc M′
|
||||
\end{code}
|
||||
|
||||
### Reflexive and transitive closure
|
||||
|
||||
\begin{code}
|
||||
infix 2 _⟶*_
|
||||
infix 1 begin_
|
||||
infixr 2 _⟶⟨_⟩_
|
||||
infix 3 _∎
|
||||
|
||||
data _⟶*_ : Term → Term → Set where
|
||||
|
||||
_∎ : ∀ (M : Term)
|
||||
-------------
|
||||
→ M ⟶* M
|
||||
|
||||
_⟶⟨_⟩_ : ∀ (L : Term) {M N}
|
||||
→ L ⟶ M
|
||||
→ M ⟶* N
|
||||
---------
|
||||
→ L ⟶* N
|
||||
|
||||
begin_ : ∀ {M N} → (M ⟶* N) → (M ⟶* N)
|
||||
begin M⟶*N = M⟶*N
|
||||
\end{code}
|
||||
|
||||
### Decide whether a term reduces
|
||||
|
||||
\begin{code}
|
||||
{-
|
||||
data Step (M : Term) : Set where
|
||||
step : ∀ {N}
|
||||
→ M ⟶ N
|
||||
-------
|
||||
→ Step M
|
||||
|
||||
reduce : ∀ (M : Term) → Dec (Step M)
|
||||
reduce ⌊ x ⌋ = no (λ{(step ())})
|
||||
reduce (`λ x `→ N) = no (λ{(step ())})
|
||||
reduce (L · M) with reduce L
|
||||
... | yes (step L⟶L′) = yes (step (ξ-·₁ L⟶L′))
|
||||
... | no ¬L⟶L′ with value L
|
||||
... | no ¬VL = no (λ{ (step (β-→ _)) → (¬VL Fun)
|
||||
; (step (ξ-·₁ L⟶L′)) → (¬L⟶L′ (step L⟶L′))
|
||||
; (step (ξ-·₂ VL _)) → (¬VL VL) })
|
||||
... | yes VL with reduce M
|
||||
... | yes (step M⟶M′) = yes (step (ξ-·₂ VL M⟶M′))
|
||||
... | no ¬M⟶M′ = {!!}
|
||||
reduce `zero = {!!}
|
||||
reduce (`suc M) = {!!}
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
### Stuck terms
|
||||
|
||||
\begin{code}
|
||||
data Stuck : Term → Set where
|
||||
|
||||
st-·₁ : ∀ {L M}
|
||||
→ Stuck L
|
||||
--------------
|
||||
→ Stuck (L · M)
|
||||
|
||||
st-·₂ : ∀ {V M}
|
||||
→ Value V
|
||||
→ Stuck M
|
||||
--------------
|
||||
→ Stuck (V · M)
|
||||
|
||||
st-·-nat : ∀ {V M}
|
||||
→ Natural V
|
||||
--------------
|
||||
→ Stuck (V · M)
|
||||
|
||||
st-suc-λ : ∀ {x N}
|
||||
-------------------------
|
||||
→ Stuck (`suc (`λ x `→ N))
|
||||
|
||||
st-suc : ∀ {M}
|
||||
→ Stuck M
|
||||
--------------
|
||||
→ Stuck (`suc M)
|
||||
\end{code}
|
||||
|
||||
### Closed terms
|
||||
|
||||
\begin{code}
|
||||
Closed : Term → Set
|
||||
Closed M = free M ≡ []
|
||||
|
||||
Ax-lemma : ∀ {x} → ¬ (Closed ⌊ x ⌋)
|
||||
Ax-lemma ()
|
||||
|
||||
closed-·₁ : ∀ {L M} → Closed (L · M) → Closed L
|
||||
closed-·₁ r = lemma r
|
||||
where
|
||||
lemma : ∀ {A : Set} {xs ys : List A} → xs ++ ys ≡ [] → xs ≡ []
|
||||
lemma {xs = []} _ = refl
|
||||
lemma {xs = x ∷ xs} ()
|
||||
|
||||
closed-·₂ : ∀ {L M} → Closed (L · M) → Closed M
|
||||
closed-·₂ r = lemma r
|
||||
where
|
||||
lemma : ∀ {A : Set} {xs ys : List A} → xs ++ ys ≡ [] → ys ≡ []
|
||||
lemma {xs = []} refl = refl
|
||||
lemma {xs = x ∷ xs} ()
|
||||
|
||||
·-closed : ∀ {L M} → Closed L → Closed M → Closed (L · M)
|
||||
·-closed r s = lemma r s
|
||||
where
|
||||
lemma : ∀ {A : Set} {xs ys : List A} → xs ≡ [] → ys ≡ [] → xs ++ ys ≡ []
|
||||
lemma refl refl = refl
|
||||
|
||||
closed-suc : ∀ {M} → Closed (`suc M) → Closed M
|
||||
closed-suc r = r
|
||||
|
||||
suc-closed : ∀ {M} → Closed M → Closed (`suc M)
|
||||
suc-closed r = r
|
||||
\end{code}
|
||||
|
||||
### Progress
|
||||
|
||||
\begin{code}
|
||||
data Progress (M : Term) : Set where
|
||||
|
||||
step : ∀ {N}
|
||||
→ M ⟶ N
|
||||
-----------
|
||||
→ Progress M
|
||||
|
||||
stuck :
|
||||
Stuck M
|
||||
-----------
|
||||
→ Progress M
|
||||
|
||||
done :
|
||||
Value M
|
||||
-----------
|
||||
→ Progress M
|
||||
\end{code}
|
||||
|
||||
### Progress
|
||||
|
||||
\begin{code}
|
||||
progress : ∀ (M : Term) → Closed M → Progress M
|
||||
progress ⌊ x ⌋ Cx = ⊥-elim (Ax-lemma Cx)
|
||||
progress (L · M) CLM with progress L (closed-·₁ {L} {M} CLM)
|
||||
... | step L⟶L′ = step (ξ-·₁ L⟶L′)
|
||||
... | stuck SL = stuck (st-·₁ SL)
|
||||
... | done VL with progress M (closed-·₂ {L} {M} CLM)
|
||||
... | step M⟶M′ = step (ξ-·₂ VL M⟶M′)
|
||||
... | stuck SM = stuck (st-·₂ VL SM)
|
||||
... | done VM with VL
|
||||
... | Nat NL = stuck (st-·-nat NL)
|
||||
... | Fun = step (β-→ VM)
|
||||
progress (`λ x `→ N) CxN = done Fun
|
||||
progress `zero Cz = done (Nat Zero)
|
||||
progress (`suc M) CsM with progress M (closed-suc {M} CsM)
|
||||
... | step M⟶M′ = step (ξ-suc M⟶M′)
|
||||
... | stuck SM = stuck (st-suc SM)
|
||||
... | done (Nat NL) = done (Nat (Suc NL))
|
||||
... | done Fun = stuck st-suc-λ
|
||||
\end{code}
|
||||
|
||||
### Preservation
|
||||
|
||||
Preservation of closed terms is not so easy.
|
||||
|
||||
\begin{code}
|
||||
preservation : ∀ {M N : Term} → Closed M → M ⟶ N → Closed N
|
||||
preservation = {!!}
|
||||
{-
|
||||
preservation CLM (ξ-·₁ L⟶L′)
|
||||
= ·-closed (preservation (closed-·₁ CLM) L⟶L′) (closed-·₂ CLM)
|
||||
preservation CLM (ξ-·₂ _ M⟶M′)
|
||||
= ·-closed (closed-·₁ CLM) (preservation (closed-·₂ CLM) M⟶M′)
|
||||
preservation CM (β-→ VM) = {!!} -- requires closure under substitution!
|
||||
preservation CM (ξ-suc M⟶M′)
|
||||
= suc-closed (preservation (closed-suc CM) M⟶M′)
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
### Evaluation
|
||||
|
||||
\begin{code}
|
||||
Gas : Set
|
||||
Gas = ℕ
|
||||
|
||||
data Eval (M : Term) : Set where
|
||||
out-of-gas : ∀ {N} → M ⟶* N → Eval M
|
||||
stuck : ∀ {N} → M ⟶* N → Stuck N → Eval M
|
||||
done : ∀ {V} → M ⟶* V → Value V → Eval M
|
||||
|
||||
eval : Gas → (L : Term) → Closed L → Eval L
|
||||
eval zero L CL = out-of-gas (L ∎)
|
||||
eval (suc n) L CL with progress L CL
|
||||
... | stuck SL = stuck (L ∎) SL
|
||||
... | done VL = done (L ∎) VL
|
||||
... | step {M} L⟶M with eval n M (preservation CL L⟶M)
|
||||
... | out-of-gas M⟶*N = out-of-gas (L ⟶⟨ L⟶M ⟩ M⟶*N)
|
||||
... | stuck M⟶*N SN = stuck (L ⟶⟨ L⟶M ⟩ M⟶*N) SN
|
||||
... | done M⟶*V VV = done (L ⟶⟨ L⟶M ⟩ M⟶*V) VV
|
||||
\end{code}
|
||||
|
||||
|
||||
## Second development: Scoped
|
||||
|
||||
\begin{code}
|
||||
module Scoped where
|
||||
\end{code}
|
||||
|
||||
### Syntax
|
||||
|
||||
\begin{code}
|
||||
infix 4 _⊢*
|
||||
infix 4 _∋*
|
||||
infixl 5 _,*
|
||||
infix 5 `λ_`→_
|
||||
infixl 6 _·_
|
||||
infix 7 S_
|
||||
|
||||
Id : Set
|
||||
Id = String
|
||||
|
||||
data Ctx : Set where
|
||||
ε : Ctx
|
||||
_,* : Ctx → Ctx
|
||||
|
||||
data _∋* : Ctx → Set where
|
||||
|
||||
Z : ∀ {Γ}
|
||||
------------
|
||||
→ Γ ,* ∋*
|
||||
|
||||
S_ : ∀ {Γ}
|
||||
→ Γ ∋*
|
||||
--------
|
||||
→ Γ ,* ∋*
|
||||
|
||||
data _⊢* : Ctx → Set where
|
||||
|
||||
⌊_⌋ : ∀ {Γ}
|
||||
→ Γ ∋*
|
||||
-----
|
||||
→ Γ ⊢*
|
||||
|
||||
`λ_`→_ : ∀ {Γ} (x : Id)
|
||||
→ Γ ,* ⊢*
|
||||
--------
|
||||
→ Γ ⊢*
|
||||
|
||||
_·_ : ∀ {Γ}
|
||||
→ Γ ⊢*
|
||||
→ Γ ⊢*
|
||||
-----
|
||||
→ Γ ⊢*
|
||||
|
||||
`zero : ∀ {Γ}
|
||||
-----
|
||||
→ Γ ⊢*
|
||||
|
||||
`suc : ∀ {Γ}
|
||||
→ Γ ⊢*
|
||||
-----
|
||||
→ Γ ⊢*
|
||||
\end{code}
|
||||
|
||||
## Conversion: Raw to Scoped
|
||||
|
||||
\begin{code}
|
||||
infix 4 _∈_
|
||||
|
||||
data _∈_ : Id → List Id → Set where
|
||||
|
||||
here : ∀ {x xs} →
|
||||
----------
|
||||
x ∈ x ∷ xs
|
||||
|
||||
there : ∀ {w x xs} →
|
||||
w ∈ xs →
|
||||
----------
|
||||
w ∈ x ∷ xs
|
||||
|
||||
_?∈_ : ∀ (x : Id) (xs : List Id) → Dec (x ∈ xs)
|
||||
x ?∈ [] = no (λ())
|
||||
x ?∈ (y ∷ ys) with x ≟ y
|
||||
... | yes refl = yes here
|
||||
... | no x≢ with x ?∈ ys
|
||||
... | yes x∈ = yes (there x∈)
|
||||
... | no x∉ = no (λ{ here → x≢ refl
|
||||
; (there x∈) → x∉ x∈
|
||||
})
|
||||
|
||||
distinct : List Id → List Id
|
||||
distinct [] = []
|
||||
distinct (x ∷ xs) with x ?∈ distinct xs
|
||||
... | yes x∈ = distinct xs
|
||||
... | no x∉ = x ∷ distinct xs
|
||||
|
||||
context : Raw.Term → Ctx
|
||||
context M = helper (distinct (Raw.free M))
|
||||
where
|
||||
helper : List Id → Ctx
|
||||
helper [] = ε
|
||||
helper (x ∷ xs) = helper xs ,*
|
||||
|
||||
raw→scoped : (M : Raw.Term) → (context M ⊢*)
|
||||
raw→scoped M = {!!}
|
||||
where
|
||||
|
||||
xs₀ = distinct (Raw.free M)
|
||||
|
||||
{-
|
||||
The following does not work because `context M` should shrink on recursive calls.
|
||||
|
||||
lookup : Id → (context M ⊢*)
|
||||
lookup w = helper w xs₀
|
||||
where
|
||||
helper : Id → List Id → (context M ⊢*)
|
||||
helper w [] = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
helper w (x ∷ xs) with w ≟ x
|
||||
... | yes _ = Z
|
||||
... | no _ = S (helper xs)
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
|
||||
|
||||
## Third development: Typed
|
||||
|
||||
\begin{code}
|
||||
module Typed where
|
||||
\end{code}
|
||||
infix 4 _⊢_
|
||||
infix 4 _∋_
|
||||
infixl 5 _,_
|
||||
infixr 5 _`→_
|
||||
infix 5 ƛ_`→_
|
||||
infixl 6 _·_
|
||||
infix 7 S_
|
||||
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
_`→_ : Type → Type → Type
|
||||
|
||||
data _∋_ : Ctx → Type → Set where
|
||||
|
||||
Z : ∀ {Γ A}
|
||||
----------
|
||||
→ Γ , A ∋ A
|
||||
|
||||
S_ : ∀ {Γ A B}
|
||||
→ Γ ∋ B
|
||||
---------
|
||||
→ Γ , A ∋ B
|
||||
|
||||
data _⊢_ : Ctx → Type → Set where
|
||||
|
||||
⌊_⌋ : ∀ {Γ} {A}
|
||||
→ Γ ∋ A
|
||||
------
|
||||
→ Γ ⊢ A
|
||||
|
||||
`λ_`→_ : ∀ {Γ A B} (x : Id)
|
||||
→ Γ , A ⊢ B
|
||||
-----------
|
||||
→ Γ ⊢ A `→ B
|
||||
|
||||
_·_ : ∀ {Γ} {A B}
|
||||
→ Γ ⊢ A `→ B
|
||||
→ Γ ⊢ A
|
||||
-----------
|
||||
→ Γ ⊢ B
|
||||
|
||||
`zero : ∀ {Γ}
|
||||
----------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`suc : ∀ {Γ}
|
||||
→ Γ ⊢ `ℕ
|
||||
-------
|
||||
→ Γ ⊢ `ℕ
|
||||
\end{code}
|
||||
Loading…
Add table
Reference in a new issue