------------------------------------------------------------------------
-- 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.
------------------------------------------------------------------------

-- This is a first attempt, which did not lead anywhere.

module DanvyFirstAttempt where

open import Data.Nat
open import Derivation
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Function hiding (_∋_)

module Language where

  -- This module defines the simply typed λ-calculus.

  infixl  _·_
  infix   ƛ_
  infixr  _⟶_
  infixl  _▻_ _▷_
  infix   _∋_ _⊢_

  -- 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  _⊙_
  infix   Λ_

  -- (Λ 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  _⊙_
    infix   Λ_
    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...