176 lines
7.1 KiB
Agda
176 lines
7.1 KiB
Agda
module Ahmed.Day1 where
|
||
|
||
open import Agda.Builtin.Sigma
|
||
open import Data.Bool
|
||
open import Data.Empty
|
||
open import Data.Fin
|
||
open import Data.Maybe
|
||
open import Data.Nat
|
||
open import Data.Product
|
||
open import Data.Sum
|
||
open import Relation.Nullary
|
||
|
||
id : {A : Set} → A → A
|
||
id {A} x = x
|
||
|
||
data type : Set where
|
||
bool : type
|
||
_-→_ : type → type → type
|
||
|
||
data term : Set where
|
||
`_ : ℕ → term
|
||
`true : term
|
||
`false : term
|
||
`if_then_else_ : term → term → term → term
|
||
`λ[_]_ : (τ : type) → (e : term) → term
|
||
_∙_ : term → term → term
|
||
|
||
data ctx : Set where
|
||
nil : ctx
|
||
cons : ctx → type → ctx
|
||
|
||
lookup : ctx → ℕ → Maybe type
|
||
lookup nil _ = nothing
|
||
lookup (cons ctx₁ x) zero = just x
|
||
lookup (cons ctx₁ x) (suc n) = lookup ctx₁ n
|
||
|
||
data sub : Set where
|
||
nil : sub
|
||
cons : sub → term → sub
|
||
|
||
subst : term → term → term
|
||
subst (` zero) v = v
|
||
subst (` suc x) v = ` x
|
||
subst `true v = `true
|
||
subst `false v = `false
|
||
subst (`if x then x₁ else x₂) v = `if (subst x v) then (subst x₁ v) else (subst x₂ v)
|
||
subst (`λ[ τ ] x) v = `λ[ τ ] subst x v
|
||
subst (x ∙ x₁) v = (subst x v) ∙ (subst x₁ v)
|
||
|
||
data value-rel : type → term → Set where
|
||
v-`true : value-rel bool `true
|
||
v-`false : value-rel bool `false
|
||
v-`λ[_]_ : ∀ {τ₁ τ₂ e} → value-rel (τ₁ -→ τ₂) (`λ[ τ₁ ] e)
|
||
|
||
data good-subst : ctx → sub → Set where
|
||
nil : good-subst nil nil
|
||
cons : ∀ {ctx τ γ v}
|
||
→ good-subst ctx γ
|
||
→ value-rel τ v
|
||
→ good-subst (cons ctx τ) γ
|
||
|
||
data step : term → term → Set where
|
||
step-if-e : ∀ {e e' e₁ e₂} → step e e' → step (`if e then e₁ else e₂) (`if e' then e₁ else e₂)
|
||
step-if-1 : ∀ {e₁ e₂} → step (`if `true then e₁ else e₂) e₁
|
||
step-if-2 : ∀ {e₁ e₂} → step (`if `false then e₁ else e₂) e₂
|
||
step-`λ-1 : ∀ {e₁ e₁' e₂} → step e₁ e₁' → step (e₁ ∙ e₂) (e₁' ∙ e₂)
|
||
step-`λ-2 : ∀ {τ e₁ e₂ e₂'} → step e₂ e₂' → step ((`λ[ τ ] e₁) ∙ e₂) ((`λ[ τ ] e₁) ∙ e₂')
|
||
step-`λ-β : ∀ {τ e v} → step ((`λ[ τ ] e) ∙ v) (subst e v)
|
||
|
||
data steps : ℕ → term → term → Set where
|
||
zero : ∀ {e} → steps zero e e
|
||
suc : ∀ {e e' e''} → (n : ℕ) → step e e' → steps n e' e'' → steps (suc n) e e''
|
||
|
||
safe : (τ : type) → (e : term) → Set
|
||
safe τ e = ∀ {n} → (e' : term) → steps n e e' → (value-rel τ e') ⊎ (∃ λ e'' → step e' e'')
|
||
|
||
data _⊢_∶_ : ctx → term → type → Set where
|
||
type-`true : ∀ {ctx} → ctx ⊢ `true ∶ bool
|
||
type-`false : ∀ {ctx} → ctx ⊢ `false ∶ bool
|
||
type-`ifthenelse : ∀ {ctx e e₁ e₂ τ}
|
||
→ ctx ⊢ e ∶ bool
|
||
→ ctx ⊢ e₁ ∶ τ
|
||
→ ctx ⊢ e₂ ∶ τ
|
||
→ ctx ⊢ (`if e then e₁ else e₂) ∶ τ
|
||
type-`x : ∀ {ctx x}
|
||
→ (p : Is-just (lookup ctx x))
|
||
→ ctx ⊢ (` x) ∶ (to-witness p)
|
||
type-`λ : ∀ {ctx τ₁ τ₂ e}
|
||
→ (cons ctx τ₁) ⊢ e ∶ τ₂
|
||
→ ctx ⊢ (`λ[ τ₁ ] e) ∶ (τ₁ -→ τ₂)
|
||
type-∙ : ∀ {ctx τ₁ τ₂ e₁ e₂}
|
||
→ ctx ⊢ e₁ ∶ (τ₁ -→ τ₂)
|
||
→ ctx ⊢ e₂ ∶ τ₂
|
||
→ ctx ⊢ (e₁ ∙ e₂) ∶ τ₂
|
||
|
||
irreducible : term → Set
|
||
irreducible e = ¬ (∃ λ e' → step e e')
|
||
|
||
data term-rel : type → term → Set where
|
||
e-term : ∀ {τ e}
|
||
→ (∀ {n} → (e' : term) → steps n e e' → irreducible e' → value-rel τ e')
|
||
→ term-rel τ e
|
||
|
||
type-soundness : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Set
|
||
type-soundness {Γ} {e} {τ} s = ∀ {n} → (e' : term) → steps n e e' → (value-rel τ e') ⊎ (∃ λ e'' → step e' e'')
|
||
|
||
type-sound : (e : term) → (τ : type) → (p : nil ⊢ e ∶ τ) → type-soundness p
|
||
type-sound .`true .bool type-`true .`true zero = inj₁ v-`true
|
||
type-sound .`false .bool type-`false .`false zero = inj₁ v-`false
|
||
type-sound .(`if _ then _ else _) τ (type-`ifthenelse p p₁ p₂) e' steps = {! !}
|
||
type-sound .(`λ[ _ ] _) .(_ -→ _) (type-`λ p) e' steps = {! !}
|
||
type-sound .(_ ∙ _) τ (type-∙ p p₁) e' steps = {! !}
|
||
|
||
_⊨_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
|
||
_⊨_∶_ Γ e τ = (γ : sub) → (good-subst Γ γ) → term-rel τ e
|
||
|
||
fundamental : ∀ {Γ e τ} → (well-typed : Γ ⊢ e ∶ τ) → type-soundness well-typed → Γ ⊨ e ∶ τ
|
||
fundamental {Γ} {e} {τ} well-typed tsound γ good-sub = e-term f
|
||
where
|
||
f : {n : ℕ} (e' : term) → steps n e e' → irreducible e' → value-rel τ e'
|
||
f e' steps irred = [ id , (λ exists → ⊥-elim (irred exists)) ] (tsound e' steps)
|
||
|
||
module semantic-type-soundness where
|
||
part1 : (e : term) → (τ : type) → nil ⊢ e ∶ τ → term-rel τ e
|
||
part1 (` x) _ (type-`x ())
|
||
part1 `true bool p = e-term f
|
||
where
|
||
f : {n : ℕ} (e' : term) → steps n `true e' → irreducible e' → value-rel bool e'
|
||
f {.zero} .`true zero irred = v-`true
|
||
part1 `false bool p = e-term f
|
||
where
|
||
f : {n : ℕ} (e' : term) → steps n `false e' → irreducible e' → value-rel bool e'
|
||
f {zero} .`false zero irred = v-`false
|
||
part1 (`λ[ τ₁ ] e) (.τ₁ -→ τ₂) (type-`λ p) = e-term f
|
||
where
|
||
f : {n : ℕ} (e' : term) → steps n (`λ[ τ₁ ] e) e' → irreducible e' → value-rel (τ₁ -→ τ₂) e'
|
||
f .(`λ[ τ₁ ] e) zero irred = v-`λ[_]_
|
||
part1 (`if e then e₁ else e₂) τ (type-`ifthenelse p p₁ p₂) = e-term f
|
||
where
|
||
v : ∀ {n} → (e' : term) → steps n e e' → value-rel bool e' → ∃ (step (`if e then e₁ else e₂))
|
||
v .`true zero v-`true = e₁ , step-if-1
|
||
v .`false zero v-`false = e₂ , step-if-2
|
||
v e' (suc {_} {e''} n step steps) val =
|
||
(`if e'' then e₁ else e₂) , step-if-e step
|
||
|
||
f : {n : ℕ} (e' : term) → steps n (`if e then e₁ else e₂) e' → irreducible e' → value-rel τ e'
|
||
f .(`if e then e₁ else e₂) zero irred with part1 e bool p
|
||
f .(`if e then e₁ else e₂) zero irred | e-term f' =
|
||
let
|
||
wtf = v e zero {! !}
|
||
wtf3 = {! irred ? !}
|
||
-- wtf2 = v e wtf
|
||
-- wtf3 = irred wtf2
|
||
-- in ⊥-elim wtf3
|
||
in {! !}
|
||
f e' (suc n (step-if-e step) steps) irred = {! !}
|
||
f e' (suc n step-if-1 steps) irred with part1 e₁ τ p₁
|
||
f e' (suc n step-if-1 steps) irred | e-term f' = f' e' steps irred
|
||
f e' (suc n step-if-2 steps) irred with part1 e₂ τ p₂
|
||
f e' (suc n step-if-2 steps) irred | e-term f' = f' e' steps irred
|
||
part1 (e₁ ∙ e₂) τ₂ (type-∙ {_} {τ₁} p₁ p₂) = e-term f
|
||
where
|
||
f : {n : ℕ} (e' : term) → steps n (e₁ ∙ e₂) e' → irreducible e' → value-rel τ₂ e'
|
||
f .(e₁ ∙ e₂) zero irred = {! !}
|
||
f e' (suc n (step-`λ-1 step) steps) irred with part1 e₁ (τ₁ -→ τ₂) p₁
|
||
f e' (suc _ (step-`λ-1 step) steps) irred | e-term f' = {! !}
|
||
f e' (suc n (step-`λ-2 step) steps) irred = {! !}
|
||
f e' (suc n step-`λ-β steps) irred = {! !}
|
||
|
||
part2 : (e : term) → (τ : type) → term-rel τ e → safe τ e
|
||
part2 e τ (e-term p) .e zero =
|
||
inj₁ (p e zero λ q → {! !})
|
||
where
|
||
v : ⊥
|
||
v = {! !}
|
||
part2 e τ (e-term p) e' (suc {f} {g} n step steps) = inj₂ ({! !} , {! step !}) |