[Added a condensed version of the HOAS.SimplyTyped modules.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080711142214] {
hunk ./Everything.agda 60
+-- A condensed version of the HOAS.SimplyTyped modules above (no
+-- comments, but no imports and less than one page long).
+
+import HOAS.SimplyTyped
+
addfile ./HOAS/SimplyTyped.agda
hunk ./HOAS/SimplyTyped.agda 1
+module HOAS.SimplyTyped where
+
+infixl 70 _·_
+infix  50 λ_
+infixr 30 _→_
+
+data Ty : Set where
+  base : Ty
+  _→_  : (σ τ : Ty) -> Ty
+
+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 τ
+
+Tm : Ty -> Set1
+Tm σ = forall {V} -> Tm' V σ
+
+Val' : (Ty -> Set) -> Ty -> Set
+Val' B base    = B base
+Val' B (σ → τ) = Val' B σ -> Val' B τ
+
+Val : Ty -> Set1
+Val σ = forall {V} -> Val' V σ
+
+⟦_⟧' : forall {B τ} -> Tm' (Val' B) τ -> Val' B τ
+⟦ var x   ⟧' = x
+⟦ λ t     ⟧' = \x -> ⟦ t x ⟧'
+⟦ t₁ · t₂ ⟧' = ⟦ t₁ ⟧' ⟦ t₂ ⟧'
+
+⟦_⟧ : forall {τ} -> Tm τ -> Val τ
+⟦ t ⟧ = ⟦ t ⟧'
+
+mutual
+
+  data Ne' (V : Ty -> Set) : Ty -> Set where
+    var : forall {τ} (x : V τ) -> Ne' V τ
+    _·_ : forall {σ τ} (t₁ : Ne' V (σ → τ)) (t₂ : NF' V σ) -> Ne' V τ
+
+  data NF' (V : Ty -> Set) : Ty -> Set where
+    ne : (t : Ne' V base) -> NF' V base
+    λ_ : forall {σ τ} (t : V σ -> NF' V τ) -> NF' V (σ → τ)
+
+NF : Ty -> Set1
+NF σ = forall {V} -> NF' V σ
+
+mutual
+
+  reflect : forall {V} τ -> Ne' V τ -> Val' (Ne' V) τ
+  reflect base    t = t
+  reflect (σ → τ) t = \v -> reflect τ (t · reify σ v)
+
+  reify : forall {V} τ -> Val' (Ne' V) τ -> NF' V τ
+  reify base    t = ne t
+  reify (σ → τ) f = λ (\x -> reify τ (f (reflect σ (var x))))
+
+nf : forall {τ} -> Tm τ -> NF τ
+nf t = reify _ ⟦ t ⟧
}