[Started formalising Danvy et al's compiler derivation.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310021949
 + Or something inspired by it.
] addfile ./Danvy.agda
hunk ./Danvy.agda 1
+------------------------------------------------------------------------
+-- Derivation of a virtual machine for the simply typed λ-calculus,
+-- inspired by "From Interpreter to Compiler and Virtual Machine: A
+-- Functional Derivation" by Ager/Biernacki/Danvy/Midtgaard.
+------------------------------------------------------------------------
+
+-- Not finished.
+
+module Danvy where
+
+open import Data.Nat
+open import Derivation
+open import Logic
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+open import Data.Function
+
+module Language where
+
+  -- This module defines the simply typed λ-calculus.
+
+  infixl 70 _·_
+  infix  50 λ_
+  infixr 30 _→_
+  infixl 20 _▻_ _▷_
+  infix  10 _∋_ _⊢_
+
+  -- Types.
+
+  data Ty : Set where
+    Nat : Ty
+    _→_ : Ty -> Ty -> Ty
+
+  -- Contexts.
+
+  data Ctxt : Set where
+    -- Empty context.
+    ε   : Ctxt
+    -- Context extension.
+    _▻_ : Ctxt -> Ty -> Ctxt
+
+  -- Variables (de Bruijn indices).
+
+  data _∋_ : Ctxt -> Ty -> Set where
+    -- Zero.
+    vz : forall {Γ σ}   -> Γ ▻ σ ∋ σ
+    -- Successor.
+    vs : forall {Γ σ τ} -> Γ ∋ τ -> Γ ▻ σ ∋ τ
+
+  -- Terms.
+
+  data _⊢_ : Ctxt -> Ty -> Set where
+    var  : forall {Γ τ}   -> Γ ∋ τ -> Γ ⊢ τ
+    λ_   : forall {Γ σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ → τ
+    _·_  : forall {Γ σ τ} -> Γ ⊢ σ → τ -> Γ ⊢ σ -> Γ ⊢ τ
+
+  -- Semantic domains for types.
+
+  ⟦_⟧⋆ : Ty -> Set
+  ⟦ Nat   ⟧⋆ = ℕ
+  ⟦ σ → τ ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆
+
+  -- Value environments.
+
+  data Env : Ctxt -> Set where
+    ∅   : Env ε
+    _▷_ : forall {Γ τ} -> Env Γ -> ⟦ τ ⟧⋆ -> Env (Γ ▻ τ)
+
+  -- Semantic domains.
+
+  Dom : Ctxt -> Ty -> Set
+  Dom Γ τ = Env Γ -> ⟦ τ ⟧⋆
+
+  -- Semantics of variables.
+
+  lookup : forall {Γ τ} -> Γ ∋ τ -> Dom Γ τ
+  lookup vz     (ρ ▷ v) = v
+  lookup (vs x) (ρ ▷ v) = lookup x ρ
+
+  -- Semantics of terms.
+
+  ⟦_⟧ : forall {Γ τ} -> Γ ⊢ τ -> Dom Γ τ
+  ⟦ var x   ⟧ ρ = lookup x ρ
+  ⟦ λ t     ⟧ ρ = \v -> ⟦ t ⟧ (ρ ▷ v)
+  ⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ (⟦ t₂ ⟧ ρ)
+
+module Step₁ where
+
+  open Language
+
+  -- Let's rewrite the semantics a little. This step (indirectly)
+  -- defines the source code of the virtual machine.
+
+  -- Here I aim to put every RHS in the form f ⟦ t₁ ⟧ … ⟦ t_n ⟧ for
+  -- some f.
+
+  infixl 70 _⊙_
+  infix  50 Λ_
+
+  -- (Λ is a capital λ.)
+
+  Λ_ : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ → τ)
+  Λ_ = \f ρ v -> f (ρ ▷ v)
+
+  _⊙_ : forall {Γ σ τ} -> Dom Γ (σ → τ) -> Dom Γ σ -> Dom Γ τ
+  _⊙_ = \f g ρ -> f ρ (g ρ)
+
+  mutual
+
+    ⟦_⟧' : forall {Γ τ} -> Γ ⊢ τ -> Env Γ -> ⟦ τ ⟧⋆
+    ⟦ t ⟧' = witness ⟦ t ⟧'P
+
+    ⟦_⟧'P : forall {Γ τ} (t : Γ ⊢ τ) -> EqualTo ⟦ t ⟧
+    ⟦ var x ⟧'P = ▷ begin lookup x ∎
+    ⟦ λ t   ⟧'P = ▷ begin
+      (\ρ v -> ⟦ t ⟧ (ρ ▷ v))
+        ≡⟨ ≡-refl ⟩
+      Λ ⟦ t ⟧
+        ∎
+    ⟦ t₁ · t₂ ⟧'P = ▷ begin
+      (\ρ -> ⟦ t₁ ⟧ ρ (⟦ t₂ ⟧ ρ))
+        ≡⟨ ≡-refl ⟩
+      ⟦ t₁ ⟧ ⊙ ⟦ t₂ ⟧
+        ∎
+
+module Step₂ where
+
+  open Language hiding (Dom; lookup; ⟦_⟧)
+
+  -- Let us abstract over some details of the semantics, using the
+  -- previous step as inspiration.
+
+  record Model : Set1 where
+    infixl 70 _⊙_
+    infix  50 Λ_
+    field
+      Dom    : Ctxt -> Ty -> Set
+      lookup : forall {Γ τ} -> Γ ∋ τ -> Dom Γ τ
+      Λ_     : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ → τ)
+      _⊙_    : forall {Γ σ τ} -> Dom Γ (σ → τ) -> Dom Γ σ -> Dom Γ τ
+
+    ⟦_⟧ : forall {Γ τ} -> Γ ⊢ τ -> Dom Γ τ
+    ⟦ var x   ⟧ = lookup x
+    ⟦ λ t     ⟧ = Λ ⟦ t ⟧
+    ⟦ t₁ · t₂ ⟧ = ⟦ t₁ ⟧ ⊙ ⟦ t₂ ⟧
+
+  -- We get back what we had before by using the following model:
+
+  eval : Model
+  eval = record
+    { Dom    = Language.Dom
+    ; lookup = Language.lookup
+    ; Λ_     = Step₁.Λ_
+    ; _⊙_    = Step₁._⊙_
+    }
+
+  eval-correct : forall {Γ τ} (t : Γ ⊢ τ) ->
+                let open Model eval in
+                ⟦ t ⟧ ≡ Language.⟦_⟧ t
+  eval-correct (var x)   = ≡-refl
+  eval-correct (λ t)     = ≡-cong Step₁.Λ_ (eval-correct t)
+  eval-correct (t₁ · t₂) =
+    ≡-cong₂ Step₁._⊙_ (eval-correct t₁) (eval-correct t₂)
+
+  -- But we can also define a term model.
+
+  term : Model
+  term = record
+    { Dom    = _⊢_
+    ; lookup = var
+    ; Λ_     = λ_
+    ; _⊙_    = _·_
+    }
+
+  -- Note that the term model's evaluator is rather uninteresting:
+
+  term-uninteresting : forall {Γ τ} (t : Γ ⊢ τ) ->
+                       let open Model term in
+                       ⟦ t ⟧ ≡ t
+  term-uninteresting (var x)   = ≡-refl
+  term-uninteresting (λ t)     = ≡-cong λ_ (term-uninteresting t)
+  term-uninteresting (t₁ · t₂) =
+    ≡-cong₂ _·_ (term-uninteresting t₁) (term-uninteresting t₂)
+
+  -- The next step is to define a virtual machine, i.e. a function
+  -- (written in a restricted way) mapping the output of the term
+  -- model to something equivalent to the output of eval:
+
+  Interpreter : Model -> Model -> Set
+  Interpreter from to = forall {Γ τ} ->
+                        Model.Dom from Γ τ -> Model.Dom to Γ τ
+
+  Correct : (from to : Model) -> Interpreter from to -> Set
+  Correct from to f = forall {Γ τ} (t : Γ ⊢ τ) ->
+                      f (Model.⟦_⟧ from t) ≡ Model.⟦_⟧ to t
+
+  -- In this case it is easy to find a function satisfying the
+  -- equation above, namely Model.⟦_⟧ eval, but this function does not
+  -- count as a virtual machine since it is not written in the right
+  -- way. In fact, the higher-order nature of ⟦_⟧⋆ means that it does
+  -- not lend itself very well to being the result type of a virtual
+  -- machine...