------------------------------------------------------------------------ -- Another approach to compiling Hutton's razor ------------------------------------------------------------------------ -- Uses generalised application instead of generalised composition. -- Based on an idea due to Graham and Diana. module ApplicationBased where open import Derivation open import Data.Nat open import Data.Vec open import Data.Product open import Function open import Relation.Binary.PropositionalEquality open ≡-Reasoning ------------------------------------------------------------------------ -- Language -- A simple expression language. I prefer subtraction to addition -- because subtraction is not commutative, so the arguments cannot be -- swapped freely. data Expr : Set where val : ℕ → Expr _⊖_ : Expr → Expr → Expr -- The semantics of the language. ⟦_⟧ : Expr → ℕ ⟦ val n ⟧ = n ⟦ m ⊖ n ⟧ = ⟦ m ⟧ ∸ ⟦ n ⟧ ------------------------------------------------------------------------ -- Stacks -- Stack A n represents stacks of size n, containing elements of -- type A. Stack : Set → ℕ → Set Stack = Vec -- The type A ^ n represents functions from stacks with n elements -- to a single result. The first function argument is the top of the -- stack. _^_ : Set → ℕ → Set A ^ zero = A A ^ suc n = A → A ^ n -- x <$ n $> f puts x at the bottom of the stack given to f: -- -- x <$ n $> f = λ y₁ … y_n → f y₁ … y_n x _<$_$>_ : ∀ {A} → A → (n : ℕ) → A ^ (1 + n) → A ^ n x <$ zero $> f = f x x <$ suc n $> f = λ y → x <$ n $> f y -- app interprets functions of type A ^ m: -- -- app m f (x₁ ∷ … ∷ x_m ∷ ys) = f x_m … x₁ ∷ ys app : ∀ {A} m {n} → A ^ m → Stack A (m + n) → Stack A (1 + n) app zero f xs = f ∷ xs app (suc m) f (x ∷ xs) = app m (x <$ m $> f) xs ------------------------------------------------------------------------ -- First step: Rewrite the evaluator module Step₁ where return : ℕ → ℕ ^ 0 return n = n sub : ℕ ^ 2 sub m n = m ∸ n private mutual ⟦_⟧' : Expr → ℕ ^ 0 ⟦ e ⟧' = witness (eval e) -- Note: This correctness proof is not used anywhere. eval : (e : Expr) → EqualTo ⟦ e ⟧ eval (val n) = ▷ begin return n ∎ eval (e₁ ⊖ e₂) = ▷ begin ⟦ e₁ ⟧ ∸ ⟦ e₂ ⟧ ≡⟨ cong₂ _∸_ (proof (eval e₁)) (proof (eval e₂)) ⟩ ⟦ e₁ ⟧' ∸ ⟦ e₂ ⟧' ≡⟨ refl ⟩ ⟦ e₁ ⟧' <$ 0 $> (⟦ e₂ ⟧' <$ 1 $> sub) ∎ ------------------------------------------------------------------------ -- Second step: Defunctionalise module Step₂ where -- The commands and command trees are indexed on their semantics. data Cmd : (n : ℕ) → ℕ ^ n → Set where return : (n : ℕ) → Cmd 0 (Step₁.return n) sub : Cmd 2 Step₁.sub data Tree : (n : ℕ) → ℕ ^ n → Set where cmd : ∀ {n f} → Cmd n f → Tree n f _$$_ : ∀ {n x f} → Tree 0 x → Tree (1 + n) f → Tree n (x <$ n $> f) comp : (e : Expr) → Tree 0 ⟦ e ⟧ comp (val n) = cmd (return n) comp (e₁ ⊖ e₂) = comp e₁ $$ (comp e₂ $$ cmd sub) ------------------------------------------------------------------------ -- Third step: Linearise the command trees module Step₃ where open Step₂ hiding (comp) open Step₂ hiding (comp) renaming (return to push) -- The code type is indexed on initial and final stack depth, plus -- its semantics. Sem : ℕ → ℕ → Set Sem i f = Stack ℕ i → Stack ℕ f data Code : (i f : ℕ) → Sem i f → Set where ε : ∀ {i} → Code i i id _◅_ : ∀ {n g i f s} → Step₂.Cmd n g → Code (1 + i) f s → Code (n + i) f (s ∘ app n g) -- Virtual machine. exec : ∀ {m n sem} → Code m n sem → Sem m n exec {sem = sem} _ = sem module Details where -- The virtual machine is actually a virtual machine. exec' : ∀ {m n sem} → Code m n sem → Sem m n exec' ε s = s exec' (push x ◅ cs) s = exec' cs (x ∷ s) exec' (sub ◅ cs) (n ∷ m ∷ s) = exec' cs (m ∸ n ∷ s) -- The structure of this proof shows that exec and exec' are -- _identical_ (modulo normalisation). execOK : ∀ {m n sem} (cs : Code m n sem) (s : Stack ℕ m) → exec cs s ≡ exec' cs s execOK ε s = refl execOK (push x ◅ cs) s = execOK cs (x ∷ s) execOK (sub ◅ cs) (n ∷ m ∷ s) = execOK cs (m ∸ n ∷ s) -- Correct compiler. comp : ∀ {m n f sem} → Tree m f → Code (1 + n) 1 sem → Code (m + n) 1 (sem ∘ app m f) comp (cmd c) cs = c ◅ cs comp (t₁ $$ t₂) cs = comp t₁ (comp t₂ cs) ------------------------------------------------------------------------ -- Step four: Assemble the pieces module Step₄ where Code : Set Code = ∃ (Step₃.Code 0 1) comp : Expr → Code comp e = (_ , Step₃.comp (Step₂.comp e) Step₃.ε) exec : Code → ℕ exec cs = head (Step₃.exec (proj₂ cs) []) correct : (e : Expr) → ⟦ e ⟧ ≡ exec (comp e) correct e = refl