[Updated the code to reflect changes in Agda and the library API. Nils Anders Danielsson **20090408103917 Ignore-this: d750703da1a696ccb11e6048cb232072 ] { hunk ./HOAS/SimplyTyped.agda 4 -infix 50 λ_ -infixr 30 _→_ +infix 50 ƛ_ +infixr 30 _⟶_ hunk ./HOAS/SimplyTyped.agda 9 - _→_ : (σ τ : Ty) -> Ty + _⟶_ : (σ τ : Ty) → Ty hunk ./HOAS/SimplyTyped.agda 11 -data Tm' (V : Ty -> Set) : Ty -> Set where - var : forall {σ} (x : V σ) -> Tm' V σ - λ_ : forall {σ τ} (t : V σ -> Tm' V τ) -> Tm' V (σ → τ) - _·_ : forall {σ τ} (t₁ : Tm' V (σ → τ)) (t₂ : Tm' V σ) -> Tm' V τ +data Tm' (V : Ty → Set) : Ty → Set where + var : ∀ {σ} (x : V σ) → Tm' V σ + ƛ_ : ∀ {σ τ} (t : V σ → Tm' V τ) → Tm' V (σ ⟶ τ) + _·_ : ∀ {σ τ} (t₁ : Tm' V (σ ⟶ τ)) (t₂ : Tm' V σ) → Tm' V τ hunk ./HOAS/SimplyTyped.agda 16 -Tm : Ty -> Set1 -Tm σ = forall {V} -> Tm' V σ +Tm : Ty → Set1 +Tm σ = ∀ {V} → Tm' V σ hunk ./HOAS/SimplyTyped.agda 19 -Val' : (Ty -> Set) -> Ty -> Set +Val' : (Ty → Set) → Ty → Set hunk ./HOAS/SimplyTyped.agda 21 -Val' B (σ → τ) = Val' B σ -> Val' B τ +Val' B (σ ⟶ τ) = Val' B σ → Val' B τ hunk ./HOAS/SimplyTyped.agda 23 -Val : Ty -> Set1 -Val σ = forall {V} -> Val' V σ +Val : Ty → Set1 +Val σ = ∀ {V} → Val' V σ hunk ./HOAS/SimplyTyped.agda 26 -⟦_⟧' : forall {B τ} -> Tm' (Val' B) τ -> Val' B τ +⟦_⟧' : ∀ {B τ} → Tm' (Val' B) τ → Val' B τ hunk ./HOAS/SimplyTyped.agda 28 -⟦ λ t ⟧' = \x -> ⟦ t x ⟧' +⟦ ƛ t ⟧' = λ x → ⟦ t x ⟧' hunk ./HOAS/SimplyTyped.agda 31 -⟦_⟧ : forall {τ} -> Tm τ -> Val τ +⟦_⟧ : ∀ {τ} → Tm τ → Val τ hunk ./HOAS/SimplyTyped.agda 36 - data Ne' (V : Ty -> Set) : Ty -> Set where - var : forall {τ} (x : V τ) -> Ne' V τ - _·_ : forall {σ τ} (t₁ : Ne' V (σ → τ)) (t₂ : NF' V σ) -> Ne' V τ + data Ne' (V : Ty → Set) : Ty → Set where + var : ∀ {τ} (x : V τ) → Ne' V τ + _·_ : ∀ {σ τ} (t₁ : Ne' V (σ ⟶ τ)) (t₂ : NF' V σ) → Ne' V τ hunk ./HOAS/SimplyTyped.agda 40 - data NF' (V : Ty -> Set) : Ty -> Set where - ne : (t : Ne' V base) -> NF' V base - λ_ : forall {σ τ} (t : V σ -> NF' V τ) -> NF' V (σ → τ) + data NF' (V : Ty → Set) : Ty → Set where + ne : (t : Ne' V base) → NF' V base + ƛ_ : ∀ {σ τ} (t : V σ → NF' V τ) → NF' V (σ ⟶ τ) hunk ./HOAS/SimplyTyped.agda 44 -NF : Ty -> Set1 -NF σ = forall {V} -> NF' V σ +NF : Ty → Set1 +NF σ = ∀ {V} → NF' V σ hunk ./HOAS/SimplyTyped.agda 49 - reflect : forall {V} τ -> Ne' V τ -> Val' (Ne' V) τ + reflect : ∀ {V} τ → Ne' V τ → Val' (Ne' V) τ hunk ./HOAS/SimplyTyped.agda 51 - reflect (σ → τ) t = \v -> reflect τ (t · reify σ v) + reflect (σ ⟶ τ) t = λ v → reflect τ (t · reify σ v) hunk ./HOAS/SimplyTyped.agda 53 - reify : forall {V} τ -> Val' (Ne' V) τ -> NF' V τ + reify : ∀ {V} τ → Val' (Ne' V) τ → NF' V τ hunk ./HOAS/SimplyTyped.agda 55 - reify (σ → τ) f = λ (\x -> reify τ (f (reflect σ (var x)))) + reify (σ ⟶ τ) f = ƛ (λ x → reify τ (f (reflect σ (var x)))) hunk ./HOAS/SimplyTyped.agda 57 -nf : forall {τ} -> Tm τ -> NF τ +nf : ∀ {τ} → Tm τ → NF τ hunk ./HOAS/SimplyTyped/Evaluation.agda 9 - (Base : ℕ -> Set) + (Base : ℕ → Set) hunk ./HOAS/SimplyTyped/Evaluation.agda 16 -⟦_⟧⋆ : Ty -> Set +⟦_⟧⋆ : Ty → Set hunk ./HOAS/SimplyTyped/Evaluation.agda 18 -⟦ σ → τ ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆ +⟦ σ ⟶ τ ⟧⋆ = ⟦ σ ⟧⋆ → ⟦ τ ⟧⋆ hunk ./HOAS/SimplyTyped/Evaluation.agda 22 -⟦_⟧' : forall {τ} -> Tm' ⟦_⟧⋆ τ -> ⟦ τ ⟧⋆ +⟦_⟧' : ∀ {τ} → Tm' ⟦_⟧⋆ τ → ⟦ τ ⟧⋆ hunk ./HOAS/SimplyTyped/Evaluation.agda 24 -⟦ λ t ⟧' = \x -> ⟦ t x ⟧' +⟦ ƛ t ⟧' = λ x → ⟦ t x ⟧' hunk ./HOAS/SimplyTyped/Evaluation.agda 27 -⟦_⟧ : forall {τ} -> Tm τ -> ⟦ τ ⟧⋆ +⟦_⟧ : ∀ {τ} → Tm τ → ⟦ τ ⟧⋆ hunk ./HOAS/SimplyTyped/NormalForm.agda 12 -infix 50 λ_ +infix 50 ƛ_ hunk ./HOAS/SimplyTyped/NormalForm.agda 16 - data Ne (V : Ty -> Set) : Ty -> Set where - var : forall {τ} (x : V τ) -> Ne V τ - _·_ : forall {σ τ} (t₁ : Ne V (σ → τ)) (t₂ : NF' V σ) -> Ne V τ + data Ne (V : Ty → Set) : Ty → Set where + var : ∀ {τ} (x : V τ) → Ne V τ + _·_ : ∀ {σ τ} (t₁ : Ne V (σ ⟶ τ)) (t₂ : NF' V σ) → Ne V τ hunk ./HOAS/SimplyTyped/NormalForm.agda 20 - data NF' (V : Ty -> Set) : Ty -> Set where - ne : forall {n} (t : Ne V (base n)) -> NF' V (base n) - λ_ : forall {σ τ} (t : V σ -> NF' V τ) -> NF' V (σ → τ) + data NF' (V : Ty → Set) : Ty → Set where + ne : ∀ {n} (t : Ne V (base n)) → NF' V (base n) + ƛ_ : ∀ {σ τ} (t : V σ → NF' V τ) → NF' V (σ ⟶ τ) hunk ./HOAS/SimplyTyped/NormalForm.agda 24 -NF : Ty -> Set1 -NF σ = forall {V} -> NF' V σ +NF : Ty → Set1 +NF σ = ∀ {V} → NF' V σ hunk ./HOAS/SimplyTyped/NormalForm.agda 31 - neToTm : forall {V τ} -> Ne V τ -> Tm' V τ + neToTm : ∀ {V τ} → Ne V τ → Tm' V τ hunk ./HOAS/SimplyTyped/NormalForm.agda 35 - nfToTm' : forall {V τ} -> NF' V τ -> Tm' V τ + nfToTm' : ∀ {V τ} → NF' V τ → Tm' V τ hunk ./HOAS/SimplyTyped/NormalForm.agda 37 - nfToTm' (λ t) = λ (\x -> nfToTm' (t x)) + nfToTm' (ƛ t) = ƛ (λ x → nfToTm' (t x)) hunk ./HOAS/SimplyTyped/NormalForm.agda 39 -nfToTm : forall {τ} -> NF τ -> Tm τ +nfToTm : ∀ {τ} → NF τ → Tm τ hunk ./HOAS/SimplyTyped/Normalisation.agda 13 -nf : forall {τ} -> Tm τ -> NF τ +nf : ∀ {τ} → Tm τ → NF τ hunk ./HOAS/SimplyTyped/TypeSystem.agda 7 -open import SimplyTyped.TypeSystem public using (Ty; base; _→_) +open import SimplyTyped.TypeSystem public using (Ty; base; _⟶_) hunk ./HOAS/SimplyTyped/TypeSystem.agda 10 -infix 50 λ_ +infix 50 ƛ_ hunk ./HOAS/SimplyTyped/TypeSystem.agda 14 -data Tm' (V : Ty -> Set) : Ty -> Set where - var : forall {σ} (x : V σ) -> Tm' V σ - λ_ : forall {σ τ} (t : V σ -> Tm' V τ) -> Tm' V (σ → τ) - _·_ : forall {σ τ} (t₁ : Tm' V (σ → τ)) (t₂ : Tm' V σ) -> Tm' V τ +data Tm' (V : Ty → Set) : Ty → Set where + var : ∀ {σ} (x : V σ) → Tm' V σ + ƛ_ : ∀ {σ τ} (t : V σ → Tm' V τ) → Tm' V (σ ⟶ τ) + _·_ : ∀ {σ τ} (t₁ : Tm' V (σ ⟶ τ)) (t₂ : Tm' V σ) → Tm' V τ hunk ./HOAS/SimplyTyped/TypeSystem.agda 19 -Tm : Ty -> Set1 -Tm σ = forall {V} -> Tm' V σ +Tm : Ty → Set1 +Tm σ = ∀ {V} → Tm' V σ hunk ./HOAS/SimplyTyped/Value.agda 13 -Val' : (Ty -> Set) -> Ty -> Set +Val' : (Ty → Set) → Ty → Set hunk ./HOAS/SimplyTyped/Value.agda 15 -Val' V (σ → τ) = Val' V σ -> Val' V τ +Val' V (σ ⟶ τ) = Val' V σ → Val' V τ hunk ./HOAS/SimplyTyped/Value.agda 17 -Val : Ty -> Set1 -Val σ = forall {V} -> Val' V σ +Val : Ty → Set1 +Val σ = ∀ {V} → Val' V σ hunk ./HOAS/SimplyTyped/Value.agda 24 - reflect : forall {V} τ -> Ne V τ -> Val' V τ + reflect : ∀ {V} τ → Ne V τ → Val' V τ hunk ./HOAS/SimplyTyped/Value.agda 26 - reflect (σ → τ) t = \v -> reflect τ (t · reify σ v) + reflect (σ ⟶ τ) t = λ v → reflect τ (t · reify σ v) hunk ./HOAS/SimplyTyped/Value.agda 28 - reify : forall {V} τ -> Val' V τ -> NF' V τ + reify : ∀ {V} τ → Val' V τ → NF' V τ hunk ./HOAS/SimplyTyped/Value.agda 30 - reify (σ → τ) f = λ (\x -> reify τ (f (reflect σ (var x)))) + reify (σ ⟶ τ) f = ƛ (λ x → reify τ (f (reflect σ (var x)))) hunk ./HOAS/SimplyTyped/Value.agda 36 -_·ˢ_ : forall {σ τ} -> Val (σ → τ) -> Val σ -> Val τ +_·ˢ_ : ∀ {σ τ} → Val (σ ⟶ τ) → Val σ → Val τ hunk ./HOAS/SimplyTyped/Value.agda 41 -varToVal : forall {V τ} -> V τ -> Val' V τ -varToVal = reflect _ ∘ var +varToVal : ∀ {V τ} → V τ → Val' V τ +varToVal = reflect _ ∘′ var hunk ./HOAS/SimplyTyped/Value.agda 44 -valToTm : forall {τ} -> Val τ -> Tm τ +valToTm : ∀ {τ} → Val τ → Tm τ hunk ./HOAS/SimplyTyped/Value.agda 49 -⟦_⟧' : forall {V τ} -> Tm' (Val' V) τ -> Val' V τ +⟦_⟧' : ∀ {V τ} → Tm' (Val' V) τ → Val' V τ hunk ./HOAS/SimplyTyped/Value.agda 51 -⟦ λ t ⟧' = \v -> ⟦ t v ⟧' +⟦ ƛ t ⟧' = λ v → ⟦ t v ⟧' hunk ./HOAS/SimplyTyped/Value.agda 54 -⟦_⟧ : forall {τ} -> Tm τ -> Val τ +⟦_⟧ : ∀ {τ} → Tm τ → Val τ hunk ./SimplyTyped/ApplicativeStructure.agda 17 - Var : forall {Γ τ} -> Γ ∋ τ -> Dom Γ τ - Lam : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ → τ) - App : forall {Γ σ τ} -> Dom Γ (σ → τ) -> Dom Γ σ -> Dom Γ τ + Var : ∀ {Γ τ} → Γ ∋ τ → Dom Γ τ + Lam : ∀ {Γ σ τ} → Dom (Γ ▻ σ) τ → Dom Γ (σ ⟶ τ) + App : ∀ {Γ σ τ} → Dom Γ (σ ⟶ τ) → Dom Γ σ → Dom Γ τ hunk ./SimplyTyped/ApplicativeStructure.agda 24 - ⟦_⟧ : forall {Γ τ} -> Γ ⊢ τ -> Dom Γ τ + ⟦_⟧ : ∀ {Γ τ} → Γ ⊢ τ → Dom Γ τ hunk ./SimplyTyped/ApplicativeStructure.agda 26 - ⟦ λ t ⟧ = Lam ⟦ t ⟧ + ⟦ ƛ t ⟧ = Lam ⟦ t ⟧ hunk ./SimplyTyped/ContextExtension.agda 14 -_▻▻_ : Ctxt -> Ctxt -> Ctxt +_▻▻_ : Ctxt → Ctxt → Ctxt hunk ./SimplyTyped/ContextExtension.agda 20 -▻▻-assoc : forall Γ Γ⁺ Γ⁺⁺ -> Γ ▻▻ (Γ⁺ ▻▻ Γ⁺⁺) ≡ (Γ ▻▻ Γ⁺) ▻▻ Γ⁺⁺ -▻▻-assoc Γ Γ⁺ ε = ≡-refl -▻▻-assoc Γ Γ⁺ (Γ⁺⁺ ▻ τ) = ≡-cong (\Γ -> Γ ▻ τ) (▻▻-assoc Γ Γ⁺ Γ⁺⁺) +▻▻-assoc : ∀ Γ Γ⁺ Γ⁺⁺ → Γ ▻▻ (Γ⁺ ▻▻ Γ⁺⁺) ≡ (Γ ▻▻ Γ⁺) ▻▻ Γ⁺⁺ +▻▻-assoc Γ Γ⁺ ε = refl +▻▻-assoc Γ Γ⁺ (Γ⁺⁺ ▻ τ) = cong (λ Γ → Γ ▻ τ) (▻▻-assoc Γ Γ⁺ Γ⁺⁺) hunk ./SimplyTyped/Environment.agda 11 -module SimplyTyped.Environment (Contents : Ty -> Set) where +module SimplyTyped.Environment (Contents : Ty → Set) where hunk ./SimplyTyped/Environment.agda 15 -data Env : Ctxt -> Set where +data Env : Ctxt → Set where hunk ./SimplyTyped/Environment.agda 17 - _▷_ : forall {Γ τ} -> Env Γ -> Contents τ -> Env (Γ ▻ τ) + _▷_ : ∀ {Γ τ} → Env Γ → Contents τ → Env (Γ ▻ τ) hunk ./SimplyTyped/Environment.agda 19 -lookup : forall {Γ τ} -> Γ ∋ τ -> Env Γ -> Contents τ +lookup : ∀ {Γ τ} → Γ ∋ τ → Env Γ → Contents τ hunk ./SimplyTyped/Evaluation.agda 9 - (Base : ℕ -> Set) + (Base : ℕ → Set) hunk ./SimplyTyped/Evaluation.agda 18 -⟦_⟧⋆ : Ty -> Set +⟦_⟧⋆ : Ty → Set hunk ./SimplyTyped/Evaluation.agda 20 -⟦ σ → τ ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆ +⟦ σ ⟶ τ ⟧⋆ = ⟦ σ ⟧⋆ → ⟦ τ ⟧⋆ hunk ./SimplyTyped/Evaluation.agda 28 - { Dom = \Γ τ -> Env Γ -> ⟦ τ ⟧⋆ + { Dom = λ Γ τ → Env Γ → ⟦ τ ⟧⋆ hunk ./SimplyTyped/Evaluation.agda 30 - ; Lam = \f ρ v -> f (ρ ▷ v) - ; App = \f x ρ -> f ρ (x ρ) + ; Lam = λ f ρ v → f (ρ ▷ v) + ; App = λ f x ρ → f ρ (x ρ) hunk ./SimplyTyped/Evaluation.agda 40 - ⟦_⟧ : forall {Γ τ} -> Γ ⊢ τ -> Env Γ -> ⟦ τ ⟧⋆ + ⟦_⟧ : ∀ {Γ τ} → Γ ⊢ τ → Env Γ → ⟦ τ ⟧⋆ hunk ./SimplyTyped/Evaluation.agda 42 - ⟦ λ t ⟧ ρ = \v -> ⟦ t ⟧ (ρ ▷ v) + ⟦ ƛ t ⟧ ρ = λ v → ⟦ t ⟧ (ρ ▷ v) hunk ./SimplyTyped/NormalForm.agda 14 -infix 50 λⁿ_ +infix 50 ƛⁿ_ hunk ./SimplyTyped/NormalForm.agda 19 - varⁿ : forall {Γ τ} -> Γ ∋ τ -> Ne Γ τ - _·ⁿ_ : forall {Γ σ τ} -> Ne Γ (σ → τ) -> NF Γ σ -> Ne Γ τ + varⁿ : ∀ {Γ τ} → Γ ∋ τ → Ne Γ τ + _·ⁿ_ : ∀ {Γ σ τ} → Ne Γ (σ ⟶ τ) → NF Γ σ → Ne Γ τ hunk ./SimplyTyped/NormalForm.agda 23 - ne : forall {Γ n} -> Ne Γ (base n) -> NF Γ (base n) - λⁿ_ : forall {Γ σ τ} -> NF (Γ ▻ σ) τ -> NF Γ (σ → τ) + ne : ∀ {Γ n} → Ne Γ (base n) → NF Γ (base n) + ƛⁿ_ : ∀ {Γ σ τ} → NF (Γ ▻ σ) τ → NF Γ (σ ⟶ τ) hunk ./SimplyTyped/NormalForm.agda 32 - _[_]ⁿ' : forall {Γ Δ τ} -> Ne Γ τ -> Γ ⇒ Δ -> Ne Δ τ + _[_]ⁿ' : ∀ {Γ Δ τ} → Ne Γ τ → Γ ⇒ Δ → Ne Δ τ hunk ./SimplyTyped/NormalForm.agda 36 - _[_]ⁿ : forall {Γ Δ τ} -> NF Γ τ -> Γ ⇒ Δ -> NF Δ τ + _[_]ⁿ : ∀ {Γ Δ τ} → NF Γ τ → Γ ⇒ Δ → NF Δ τ hunk ./SimplyTyped/NormalForm.agda 38 - λⁿ t [ ρ ]ⁿ = λⁿ (t [ ρ ↑ ]ⁿ) + ƛⁿ t [ ρ ]ⁿ = ƛⁿ (t [ ρ ↑ ]ⁿ) hunk ./SimplyTyped/NormalForm.agda 44 - neToTm : forall {Γ τ} -> Ne Γ τ -> Γ ⊢ τ + neToTm : ∀ {Γ τ} → Ne Γ τ → Γ ⊢ τ hunk ./SimplyTyped/NormalForm.agda 48 - nfToTm : forall {Γ τ} -> NF Γ τ -> Γ ⊢ τ + nfToTm : ∀ {Γ τ} → NF Γ τ → Γ ⊢ τ hunk ./SimplyTyped/NormalForm.agda 50 - nfToTm (λⁿ t) = λ nfToTm t + nfToTm (ƛⁿ t) = ƛ nfToTm t hunk ./SimplyTyped/Normalisation.agda 15 -nf : forall {Γ τ} -> Γ ⊢ τ -> NF Γ τ +nf : ∀ {Γ τ} → Γ ⊢ τ → NF Γ τ hunk ./SimplyTyped/Semantics.agda 15 -infix 10 _⟶_ +infix 10 _⇾_ hunk ./SimplyTyped/Semantics.agda 17 -data _⟶_ : forall {Γ σ} -> Rel (Γ ⊢ σ) where - β : forall {Γ σ τ} (t₁ : Γ ▻ σ ⊢ τ) t₂ -> - (λ t₁) · t₂ ⟶ t₁ [ sub t₂ ] - η : forall {Γ σ τ} (t : Γ ⊢ σ → τ) -> - t ⟶ λ (t [ wk {σ = σ} ]) · var vz +data _⇾_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) where + β : ∀ {Γ σ τ} (t₁ : Γ ▻ σ ⊢ τ) t₂ → + (ƛ t₁) · t₂ ⇾ t₁ [ sub t₂ ] + η : ∀ {Γ σ τ} (t : Γ ⊢ σ ⟶ τ) → + t ⇾ ƛ (t [ wk {σ = σ} ]) · var vz hunk ./SimplyTyped/Semantics.agda 28 -infix 50 λ•_ +infix 50 ƛ•_ hunk ./SimplyTyped/Semantics.agda 32 - λ•_ : forall {Γ σ τ} -> - RedCtxt Δ χ (Γ ▻ σ) τ -> RedCtxt Δ χ Γ (σ → τ) - _•·_ : forall {Γ σ τ} -> - RedCtxt Δ χ Γ (σ → τ) -> Γ ⊢ σ -> RedCtxt Δ χ Γ τ - _·•_ : forall {Γ σ τ} -> - Γ ⊢ σ → τ -> RedCtxt Δ χ Γ σ -> RedCtxt Δ χ Γ τ + ƛ•_ : ∀ {Γ σ τ} → RedCtxt Δ χ (Γ ▻ σ) τ → RedCtxt Δ χ Γ (σ ⟶ τ) + _•·_ : ∀ {Γ σ τ} → RedCtxt Δ χ Γ (σ ⟶ τ) → Γ ⊢ σ → RedCtxt Δ χ Γ τ + _·•_ : ∀ {Γ σ τ} → Γ ⊢ σ ⟶ τ → RedCtxt Δ χ Γ σ → RedCtxt Δ χ Γ τ hunk ./SimplyTyped/Semantics.agda 40 -_⟨_⟩ : forall {Δ χ Γ σ} -> RedCtxt Δ χ Γ σ -> Δ ⊢ χ -> Γ ⊢ σ +_⟨_⟩ : ∀ {Δ χ Γ σ} → RedCtxt Δ χ Γ σ → Δ ⊢ χ → Γ ⊢ σ hunk ./SimplyTyped/Semantics.agda 42 -λ• C ⟨ t ⟩ = λ (C ⟨ t ⟩) +ƛ• C ⟨ t ⟩ = ƛ (C ⟨ t ⟩) hunk ./SimplyTyped/Semantics.agda 50 -data _⇛_ : forall {Γ σ} -> Rel (Γ ⊢ σ) where - red : forall {Γ σ Δ τ t₁ t₂} (C : RedCtxt Γ σ Δ τ) -> - t₁ ⟶ t₂ -> C ⟨ t₁ ⟩ ⇛ C ⟨ t₂ ⟩ +data _⇛_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) where + red : ∀ {Γ σ Δ τ t₁ t₂} (C : RedCtxt Γ σ Δ τ) → + t₁ ⇾ t₂ → C ⟨ t₁ ⟩ ⇛ C ⟨ t₂ ⟩ hunk ./SimplyTyped/Semantics.agda 58 -_⇛⋆_ : forall {Γ σ} -> Rel (Γ ⊢ σ) +_⇛⋆_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) hunk ./SimplyTyped/Semantics/Lemmas.agda 10 +open import Data.Star.Properties hunk ./SimplyTyped/Semantics/Lemmas.agda 18 - renaming (_⟶⋆⟨_⟩_ to _⇛⋆⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_) - - infixr 2 _⇛⟨_⟩_ - - _⇛⟨_⟩_ : forall x {y z} -> - x ⇛ y -> y IsRelatedTo z -> x IsRelatedTo z - t₁ ⇛⟨ t₁⇛t₂ ⟩ t₂⇛⋆t₃ = t₁ ⇛⋆⟨ t₁⇛t₂ ◅ ε ⟩ t₂⇛⋆t₃ + renaming (_⟶⟨_⟩_ to _⇛⟨_⟩_; _⟶⋆⟨_⟩_ to _⇛⋆⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_) hunk ./SimplyTyped/Semantics/Lemmas.agda 24 -λ-cong : forall {Γ σ τ} {t₁ t₂ : Γ ▻ σ ⊢ τ} -> - t₁ ⇛⋆ t₂ -> λ t₁ ⇛⋆ λ t₂ -λ-cong = gmap _ λ-cong' +ƛ-cong : ∀ {Γ σ τ} {t₁ t₂ : Γ ▻ σ ⊢ τ} → + t₁ ⇛⋆ t₂ → ƛ t₁ ⇛⋆ ƛ t₂ +ƛ-cong = gmap _ ƛ-cong' hunk ./SimplyTyped/Semantics/Lemmas.agda 28 - λ-cong' : forall {Γ σ τ} {t₁ t₂ : Γ ▻ σ ⊢ τ} -> - t₁ ⇛ t₂ -> λ t₁ ⇛ λ t₂ - λ-cong' (red C t₁⟶t₂) = red (λ• C) t₁⟶t₂ + ƛ-cong' : ∀ {Γ σ τ} {t₁ t₂ : Γ ▻ σ ⊢ τ} → + t₁ ⇛ t₂ → ƛ t₁ ⇛ ƛ t₂ + ƛ-cong' (red C t₁⟶t₂) = red (ƛ• C) t₁⟶t₂ hunk ./SimplyTyped/Semantics/Lemmas.agda 32 -_·-cong_ : forall {Γ σ τ} {t₁ t₂ : Γ ⊢ σ → τ} {u₁ u₂ : Γ ⊢ σ} -> - t₁ ⇛⋆ t₂ -> u₁ ⇛⋆ u₂ -> t₁ · u₁ ⇛⋆ t₂ · u₂ +_·-cong_ : ∀ {Γ σ τ} {t₁ t₂ : Γ ⊢ σ ⟶ τ} {u₁ u₂ : Γ ⊢ σ} → + t₁ ⇛⋆ t₂ → u₁ ⇛⋆ u₂ → t₁ · u₁ ⇛⋆ t₂ · u₂ hunk ./SimplyTyped/Semantics/Lemmas.agda 42 - ·-cong₁ : forall {Γ σ τ} {t₁ t₂ : Γ ⊢ σ → τ} u -> - t₁ ⇛ t₂ -> t₁ · u ⇛ t₂ · u + ·-cong₁ : ∀ {Γ σ τ} {t₁ t₂ : Γ ⊢ σ ⟶ τ} u → + t₁ ⇛ t₂ → t₁ · u ⇛ t₂ · u hunk ./SimplyTyped/Semantics/Lemmas.agda 46 - ·-cong₂ : forall {Γ σ τ} {u₁ u₂} (t : Γ ⊢ σ → τ) -> - u₁ ⇛ u₂ -> t · u₁ ⇛ t · u₂ + ·-cong₂ : ∀ {Γ σ τ} {u₁ u₂} (t : Γ ⊢ σ ⟶ τ) → + u₁ ⇛ u₂ → t · u₁ ⇛ t · u₂ hunk ./SimplyTyped/Substitution.agda 38 - _⇒_ : Ctxt -> Ctxt -> Set + _⇒_ : Ctxt → Ctxt → Set hunk ./SimplyTyped/Substitution.agda 43 - Applier : TmLike -> TmLike -> Set - Applier _•₁_ _•₂_ = forall {Γ Δ τ} -> Γ •₁ τ -> Γ ⇒ Δ -> Δ •₂ τ + Applier : TmLike → TmLike → Set + Applier _•₁_ _•₂_ = ∀ {Γ Δ τ} → Γ •₁ τ → Γ ⇒ Δ → Δ •₂ τ hunk ./SimplyTyped/Substitution.agda 51 - vr : forall {Γ τ} -> Γ ∋ τ -> Γ • τ - weaken : forall {Γ σ τ} -> Γ • τ -> Γ ▻ σ • τ - tm : forall {Γ τ} -> Γ • τ -> Γ ⊢ τ + vr : ∀ {Γ τ} → Γ ∋ τ → Γ • τ + weaken : ∀ {Γ σ τ} → Γ • τ → Γ ▻ σ • τ + tm : ∀ {Γ τ} → Γ • τ → Γ ⊢ τ hunk ./SimplyTyped/Substitution.agda 78 - wk⇒ : forall {Γ Δ σ} -> Γ ⇒ Δ -> Γ ⇒ Δ ▻ σ + wk⇒ : ∀ {Γ Δ σ} → Γ ⇒ Δ → Γ ⇒ Δ ▻ σ hunk ./SimplyTyped/Substitution.agda 84 - _↑ : forall {Γ Δ σ} -> Γ ⇒ Δ -> Γ ▻ σ ⇒ Δ ▻ σ + _↑ : ∀ {Γ Δ σ} → Γ ⇒ Δ → Γ ▻ σ ⇒ Δ ▻ σ hunk ./SimplyTyped/Substitution.agda 89 - idˢ : forall {Γ} -> Γ ⇒ Γ + idˢ : ∀ {Γ} → Γ ⇒ Γ hunk ./SimplyTyped/Substitution.agda 95 - wk : forall {Γ σ} -> Γ ⇒ Γ ▻ σ + wk : ∀ {Γ σ} → Γ ⇒ Γ ▻ σ hunk ./SimplyTyped/Substitution.agda 100 - sub : forall {Γ τ} -> Γ • τ -> Γ ▻ τ ⇒ Γ + sub : ∀ {Γ τ} → Γ • τ → Γ ▻ τ ⇒ Γ hunk ./SimplyTyped/Substitution.agda 107 - λ t [ ρ ] = λ (t [ ρ ↑ ]) + ƛ t [ ρ ] = ƛ (t [ ρ ↑ ]) hunk ./SimplyTyped/Substitution.agda 112 - wk⇒⋆ : forall {Γ Δ} Δ⁺ -> Γ ⇒ Δ -> Γ ⇒ Δ ▻▻ Δ⁺ + wk⇒⋆ : ∀ {Γ Δ} Δ⁺ → Γ ⇒ Δ → Γ ⇒ Δ ▻▻ Δ⁺ hunk ./SimplyTyped/Substitution.agda 116 - wk⋆ : forall {Γ} Γ⁺ -> Γ ⇒ Γ ▻▻ Γ⁺ + wk⋆ : ∀ {Γ} Γ⁺ → Γ ⇒ Γ ▻▻ Γ⁺ hunk ./SimplyTyped/Substitution.agda 133 - _∘ˢ_ : forall {Γ Δ X} -> Γ ⇒ Δ -> Δ ⇒ X -> Γ ⇒ X + _∘ˢ_ : ∀ {Γ Δ X} → Γ ⇒ Δ → Δ ⇒ X → Γ ⇒ X hunk ./SimplyTyped/Substitution.agda 162 - ; weaken = \t -> t [ wk ] + ; weaken = λ t → t [ wk ] hunk ./SimplyTyped/TypeSystem.agda 10 -infix 50 λ_ -infixr 30 _→_ +infix 50 ƛ_ +infixr 30 _⟶_ hunk ./SimplyTyped/TypeSystem.agda 18 - base : ℕ -> Ty - _→_ : Ty -> Ty -> Ty + base : ℕ → Ty + _⟶_ : Ty → Ty → Ty hunk ./SimplyTyped/TypeSystem.agda 27 - _▻_ : Ctxt -> Ty -> Ctxt + _▻_ : Ctxt → Ty → Ctxt hunk ./SimplyTyped/TypeSystem.agda 32 -TmLike = Ctxt -> Ty -> Set +TmLike = Ctxt → Ty → Set hunk ./SimplyTyped/TypeSystem.agda 38 - vz : forall {Γ σ} -> Γ ▻ σ ∋ σ + vz : ∀ {Γ σ} → Γ ▻ σ ∋ σ hunk ./SimplyTyped/TypeSystem.agda 40 - vs : forall {Γ σ τ} -> Γ ∋ τ -> Γ ▻ σ ∋ τ + vs : ∀ {Γ σ τ} → Γ ∋ τ → Γ ▻ σ ∋ τ hunk ./SimplyTyped/TypeSystem.agda 45 - var : forall {Γ τ} -> Γ ∋ τ -> Γ ⊢ τ - λ_ : forall {Γ σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ → τ - _·_ : forall {Γ σ τ} -> Γ ⊢ σ → τ -> Γ ⊢ σ -> Γ ⊢ τ + var : ∀ {Γ τ} → Γ ∋ τ → Γ ⊢ τ + ƛ_ : ∀ {Γ σ τ} → Γ ▻ σ ⊢ τ → Γ ⊢ σ ⟶ τ + _·_ : ∀ {Γ σ τ} → Γ ⊢ σ ⟶ τ → Γ ⊢ σ → Γ ⊢ τ hunk ./SimplyTyped/Value.agda 19 -Val Γ (σ → τ) = forall Γ⁺ -> Val (Γ ▻▻ Γ⁺) σ -> Val (Γ ▻▻ Γ⁺) τ +Val Γ (σ ⟶ τ) = ∀ Γ⁺ → Val (Γ ▻▻ Γ⁺) σ → Val (Γ ▻▻ Γ⁺) τ hunk ./SimplyTyped/Value.agda 25 -_·ˢ_ : forall {Γ σ τ} -> Val Γ (σ → τ) -> Val Γ σ -> Val Γ τ +_·ˢ_ : ∀ {Γ σ τ} → Val Γ (σ ⟶ τ) → Val Γ σ → Val Γ τ hunk ./SimplyTyped/Value.agda 32 - reflect : forall {Γ} τ -> Ne Γ τ -> Val Γ τ + reflect : ∀ {Γ} τ → Ne Γ τ → Val Γ τ hunk ./SimplyTyped/Value.agda 34 - reflect (σ → τ) t = \Γ⁺ v -> + reflect (σ ⟶ τ) t = λ Γ⁺ v → hunk ./SimplyTyped/Value.agda 38 - reify : forall {Γ} τ -> Val Γ τ -> NF Γ τ + reify : ∀ {Γ} τ → Val Γ τ → NF Γ τ hunk ./SimplyTyped/Value.agda 40 - reify (σ → τ) f = λⁿ (reify τ (f (ε ▻ σ) (reflect σ (varⁿ vz)))) + reify (σ ⟶ τ) f = ƛⁿ (reify τ (f (ε ▻ σ) (reflect σ (varⁿ vz)))) hunk ./SimplyTyped/Value.agda 44 -wkˢ : forall {Γ} τ Γ⁺ -> Val Γ τ -> Val (Γ ▻▻ Γ⁺) τ +wkˢ : ∀ {Γ} τ Γ⁺ → Val Γ τ → Val (Γ ▻▻ Γ⁺) τ hunk ./SimplyTyped/Value.agda 46 -wkˢ {Γ} (σ → τ) Γ⁺ f = \Γ⁺⁺ v -> - let cast₁ = ≡-subst (\Γ -> Val Γ σ) (≡-sym $ ▻▻-assoc Γ Γ⁺ Γ⁺⁺) - cast₂ = ≡-subst (\Γ -> Val Γ τ) (▻▻-assoc Γ Γ⁺ Γ⁺⁺) +wkˢ {Γ} (σ ⟶ τ) Γ⁺ f = λ Γ⁺⁺ v → + let cast₁ = subst (λ Γ → Val Γ σ) (sym $ ▻▻-assoc Γ Γ⁺ Γ⁺⁺) + cast₂ = subst (λ Γ → Val Γ τ) (▻▻-assoc Γ Γ⁺ Γ⁺⁺) hunk ./SimplyTyped/Value.agda 55 -varToVal : forall {Γ τ} -> Γ ∋ τ -> Val Γ τ +varToVal : ∀ {Γ τ} → Γ ∋ τ → Val Γ τ hunk ./SimplyTyped/Value.agda 58 -valToTm : forall {Γ τ} -> Val Γ τ -> Γ ⊢ τ +valToTm : ∀ {Γ τ} → Val Γ τ → Γ ⊢ τ hunk ./SimplyTyped/Value.agda 77 - { Dom = \Γ τ -> forall {Δ} -> Γ ⇒ Δ -> Val Δ τ - ; Var = \x ρ -> lookup x ρ - ; Lam = \f ρ Δ⁺ v -> f (wk⇒⋆ Δ⁺ ρ ▷ v) - ; App = \v₁ v₂ ρ -> v₁ ρ ·ˢ v₂ ρ + { Dom = λ Γ τ → ∀ {Δ} → Γ ⇒ Δ → Val Δ τ + ; Var = λ x ρ → lookup x ρ + ; Lam = λ f ρ Δ⁺ v → f (wk⇒⋆ Δ⁺ ρ ▷ v) + ; App = λ v₁ v₂ ρ → v₁ ρ ·ˢ v₂ ρ hunk ./SimplyTyped/Value.agda 88 - ⟦_⟧ : forall {Γ Δ τ} -> Γ ⊢ τ -> Γ ⇒ Δ -> Val Δ τ + ⟦_⟧ : ∀ {Γ Δ τ} → Γ ⊢ τ → Γ ⇒ Δ → Val Δ τ hunk ./SimplyTyped/Value.agda 90 - ⟦ λ t ⟧ ρ = \Δ⁺ v -> ⟦ t ⟧ (wk⇒⋆ Δ⁺ ρ ▷ v) + ⟦ ƛ t ⟧ ρ = λ Δ⁺ v → ⟦ t ⟧ (wk⇒⋆ Δ⁺ ρ ▷ v) }