[A compiler derivation based on generalised reverse composition. Nils Anders Danielsson **20091119135116 Ignore-this: 57175ff46b32a698d56e261d43fb90f8 ] < [Started formalising "Compiling Exceptions Correctly" by Hutton/Wright. Nils Anders Danielsson **20080205010934] [Renamed exec s ops to ⟪ ops ⟫ s. Nils Anders Danielsson **20080205011003] [Split up the code into reusable modules. Nils Anders Danielsson **20080205013235] [Started on an attempt to calculate an abstract machine. Nils Anders Danielsson **20080206201551 + Unfortunately the proof seems to require extensionality. ] [The module now assumes extensionality. Nils Anders Danielsson **20080206233441] [Broke out some definitions which simplify calculations. Nils Anders Danielsson **20080207022158] [Started extending the calculation to exceptions. Nils Anders Danielsson **20080207023248 + The calculation is mostly finished, but suffers from the same problem as the one in HuttonsRazor.agda. + Note that my calculation is not quite identical to the Hutton/Wright one. ] [Hutton/Wright's code is not structurally recursive. Nils Anders Danielsson **20080207024840 + Hence my problems. ] [Tried showing that the code is terminating. Nils Anders Danielsson **20080209205756 + The termination checker does not accept this code, though. Reason: Inequalities like sizeC c < suc (sizeC c) are not derived. ] [Tried using a slightly different method to prove termination. Nils Anders Danielsson **20080210021346] [Forced the termination proof to completion. Nils Anders Danielsson **20080210021536] [Started formalising one of Wand's derivations. Nils Anders Danielsson **20080224021845] [Replaced type vectors with type lists. Nils Anders Danielsson **20080224022258 + Since I don't need to know the length. ] [Added the first step of the compiler. Nils Anders Danielsson **20080302222628] [Extracted type lists and _⟪_⟫_ into a separate file. Nils Anders Danielsson **20080302224036] [Tried using uncurried functions, but this was awkward. Nils Anders Danielsson **20080302230339] [Tried using uncurried functions, but this was awkward. Nils Anders Danielsson *-20080302230339] [Made it easier (?) to apply the right-assoc lemma. Nils Anders Danielsson **20080303000703 + In the left-to-right direction. ] [Parameterised top-level module on Id (instead of every individual module). Nils Anders Danielsson **20080304230431] [Simplified second step by indexing expressions on their semantics. Nils Anders Danielsson **20080304230717] [Replaced type lists with the new Data.List1. Nils Anders Danielsson **20080305000632] [Added a universe and a variant of the compiler which uses the universe. Nils Anders Danielsson **20080305011239] [Added some examples. Nils Anders Danielsson **20080305021144] [Simplified the universe a little. Nils Anders Danielsson **20080305025215] [Started on the rotation code. Nils Anders Danielsson **20080305025625 + In order to continue I need to either generalise the type of the resulting linear expressions, or specialise the types of the input expressions. ] [Reduced the universe level of a type. Nils Anders Danielsson **20080305025947] [Finished the code for rotation. Nils Anders Danielsson **20080305040437 + Did this by specialising types. The code is currently a bit ugly. I would prefer more general types. + No correctness proof yet. ] [Set the stage to prove correctness of rotation. Nils Anders Danielsson **20080305143644 + Cleaned up the code, proved some lemmas, stated correctness. ] [Removed the universe, which turned out to be unnecessary. Nils Anders Danielsson **20080305234646 + When I specialised the types the type indices turned into integers, so I did not need to pattern match on any elements of Set. ] [Stated the right associativity lemma using casts. Nils Anders Danielsson **20080306014158 + This made both the statement and the proof more complex. ] [Simplified the right associativity statement by using difference lists. Nils Anders Danielsson **20080306134221] [Included the map id ≡ id law as well. Nils Anders Danielsson **20080306134847] [Removed B⋆, renamed B⋆* to B*. Nils Anders Danielsson **20080306135503] [Tried switching from casts to conversion functions. Nils Anders Danielsson **20080306135611 + This didn't help much. ] [Added _⟪_⟫-cong_. Nils Anders Danielsson **20080306135929] [Renamed Fun to _→_. Nils Anders Danielsson **20080306140736] [Added _^_. Nils Anders Danielsson **20080306141239] [Converted Wand to the new _⟪_⟫_. Nils Anders Danielsson **20080306162646] [Renamed _◅_ to _▻_. Nils Anders Danielsson **20080306162910] [Proved rot-lemma. Nils Anders Danielsson **20080306231042] [Started formalising Danvy et al's compiler derivation. Nils Anders Danielsson **20080310021949 + Or something inspired by it. ] [Started using Data.Star from the standard library. Nils Anders Danielsson **20080312003502] [Updated code to reflect changes in library API. Nils Anders Danielsson **20080312010019] [Added a comment. Nils Anders Danielsson **20080312211238] [Started formalising another of Wand's papers. Nils Anders Danielsson **20080314011924 + He claims that the method used in that paper is easier than the one I tried formalising in Wand.agda. ] [Implemented the simply typed lambda calculus with multi-argument functions. Nils Anders Danielsson **20080314052458] [Started on the derivation. Did (parts of) the defunctionalisation. Nils Anders Danielsson **20080315011706] [Updated code to reflect changes in library API. Nils Anders Danielsson **20080513173925] [Another approach to compiling Hutton's razor. Nils Anders Danielsson **20080513181929] [Switched to ordinary ℕ and Vec instead of the variants based on star-lists. Nils Anders Danielsson **20080513193052 + Since the code becomes a bit easier to understand. ] [Proved compiler correctness. Nils Anders Danielsson **20080514095207] [Simplified the correctness proof. Nils Anders Danielsson **20080514095642] [Simplified the proof again. Nils Anders Danielsson **20080514102418] [Updated code to reflect changes in library API. Nils Anders Danielsson **20080918152933] [Made EqualTo universe polymorphic. Nils Anders Danielsson **20091119135025 Ignore-this: dbfd13fc9d3db2b7485f887b1b1467c7 ] [Added ▶_. Nils Anders Danielsson **20091119135037 Ignore-this: f32cd952d3e5c75f85064f606c7ad41e ] [Generalised reverse composition. Nils Anders Danielsson **20091119135051 Ignore-this: 4260670fd7a20df98ba923af4f79cef0 ] > addfile ./CompositionBased.agda hunk ./CompositionBased.agda 1 +------------------------------------------------------------------------ +-- A derivation of a compiler for a simple language +------------------------------------------------------------------------ + +open import Relation.Binary.HeterogeneousEquality as HE + using (_≅_; refl) + +module CompositionBased + -- Extensionality is assumed. (This is probably not + -- necessary.) + (ext : ∀ {A B C : Set} {f : A → B} {g : A → C} → + (∀ x → f x ≅ g x) → f ≅ g) + where + +open import Data.Function +open import Data.Nat +open import Data.Product +open import Relation.Binary.PropositionalEquality + +open import Derivation +import ReverseComposition +open ReverseComposition ext + +------------------------------------------------------------------------ +-- Language + +-- A simple expression language. + +data Expr : Set where + val : (n : ℕ) → Expr + _⊖_ : (e₁ e₂ : Expr) → Expr + +-- The semantics of the language. + +⟦_⟧ : Expr → ℕ +⟦ val n ⟧ = n +⟦ e₁ ⊖ e₂ ⟧ = ⟦ e₁ ⟧ ∸ ⟦ e₂ ⟧ + +------------------------------------------------------------------------ +-- Rewrite the evaluator in "compositional" style + +module Compositional where + + open ≡-Reasoning + + return : ℕ → ℕ ^ 0 + return = λ n → n + + sub : ℕ ^ 2 + sub = _∸_ + + mutual + + ⟦_⟧C : Expr → ℕ ^ 0 + ⟦ e ⟧C = witness (eval e) + + 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₁ ⟧C ∸ ⟦ e₂ ⟧C ≡⟨ refl ⟩ + 0 ∣ 0 ∣ ⟦ e₂ ⟧C ⊙ 0 ∣ 1 ∣ ⟦ e₁ ⟧C ⊙ sub ∎ + +------------------------------------------------------------------------ +-- Rewrite the evaluator in accumulator style + +module Accumulator where + + open HE.≅-Reasoning + open Compositional using (return; sub; ⟦_⟧C) + + mutual + + -- What is the motivation for using suc i and i here? + + ⟦_⟧A : Expr → ∀ i → ℕ ^ suc i → ℕ ^ i + ⟦ e ⟧A i f = witness (eval e i f) + + eval : ∀ (e : Expr) i (f : ℕ ^ suc i) → + EqualTo (0 ∣ i ∣ ⟦ e ⟧C ⊙ f) + eval (val n) i f = ▶ begin 0 ∣ i ∣ return n ⊙ f ∎ + eval (e₁ ⊖ e₂) i f = ▶ begin + 0 ∣ i ∣ (0 ∣ 0 ∣ ⟦ e₂ ⟧C ⊙ (0 ∣ 1 ∣ ⟦ e₁ ⟧C ⊙ sub)) ⊙ f ≅⟨ assoc 0 0 i ⟦ e₂ ⟧C (0 ∣ 1 ∣ ⟦ e₁ ⟧C ⊙ sub) f ⟩ + 0 ∣ i ∣ ⟦ e₂ ⟧C ⊙ (1 ∣ i ∣ (0 ∣ 1 ∣ ⟦ e₁ ⟧C ⊙ sub) ⊙ f) ≅⟨ HE.cong (_∣_∣_⊙_ 0 i ⟦ e₂ ⟧C) + (assoc 0 1 i ⟦ e₁ ⟧C sub f) ⟩ + 0 ∣ i ∣ ⟦ e₂ ⟧C ⊙ (0 ∣ suc i ∣ ⟦ e₁ ⟧C ⊙ 2 ∣ i ∣ sub ⊙ f) ≡⟨ cong (_∣_∣_⊙_ 0 i ⟦ e₂ ⟧C) + (proof (eval e₁ (suc i) (2 ∣ i ∣ sub ⊙ f))) ⟩ + 0 ∣ i ∣ ⟦ e₂ ⟧C ⊙ (⟦ e₁ ⟧A (suc i) (2 ∣ i ∣ sub ⊙ f)) ≡⟨ proof (eval e₂ i (⟦ e₁ ⟧A (suc i) (2 ∣ i ∣ sub ⊙ f))) ⟩ + ⟦ e₂ ⟧A i (⟦ e₁ ⟧A (suc i) (2 ∣ i ∣ sub ⊙ f)) ∎ + + halt : ℕ ^ 1 + halt = id + + correct : ∀ e → ∃ λ f → ⟦ e ⟧ ≡ ⟦ e ⟧A 0 f + correct e = halt , HE.≅-to-≡ (begin + ⟦ e ⟧ ≡⟨ proof $ Compositional.eval e ⟩ + ⟦ e ⟧C ≅⟨ HE.sym $ right-identity 0 ⟦ e ⟧C ⟩ + 0 ∣ 0 ∣ ⟦ e ⟧C ⊙ halt ≡⟨ proof $ eval e 0 id ⟩ + ⟦ e ⟧A 0 halt ∎) + +------------------------------------------------------------------------ +-- Defunctionalise + +module Defunctionalised where + + open Compositional using (return; sub) + open Accumulator using (⟦_⟧A) + open ≡-Reasoning + + data Term : ℕ → Set where + _∣return_⊙_ : ∀ i (n : ℕ) (t : Term (1 + i)) → Term i + _∣sub⊙_ : ∀ i (t : Term (1 + i)) → Term (2 + i) + halt : Term 1 + + -- The semantics of Term. + + apply : ∀ {i} → Term i → ℕ ^ i + apply (i ∣return n ⊙ t) = 0 ∣ i ∣ return n ⊙ apply t + apply (i ∣sub⊙ t) = 2 ∣ i ∣ sub ⊙ apply t + apply halt = Accumulator.halt + + -- The right-hand sides evaluate, so the code above is equivalent to + -- the following one. + + exec : ∀ {i} → Term i → ℕ ^ i + exec (i ∣return n ⊙ t) = exec t n + exec (i ∣sub⊙ t) = λ m n → exec t (m ∸ n) + exec halt = λ n → n + + -- Compiler. + + mutual + + comp : ∀ {i} → Expr → Term (suc i) → Term i + comp e t = proj₁ (comp′ e t) + + comp′ : ∀ (e : Expr) {i} (t : Term (suc i)) → + ∃ λ (t′ : Term i) → ⟦ e ⟧A i (exec t) ≡ exec t′ + comp′ (val n) t = _ ∣return n ⊙ t , (begin + exec t n ≡⟨ refl ⟩ + exec (_ ∣return n ⊙ t) ∎) + comp′ (e₁ ⊖ e₂) {i} t = comp e₂ (comp e₁ (i ∣sub⊙ t)) , (begin + ⟦ e₂ ⟧A i (⟦ e₁ ⟧A (suc i) (2 ∣ i ∣ sub ⊙ exec t)) ≡⟨ refl ⟩ + ⟦ e₂ ⟧A i (⟦ e₁ ⟧A (suc i) (exec (i ∣sub⊙ t))) ≡⟨ cong (⟦_⟧A e₂ i) + (proj₂ $ comp′ e₁ (i ∣sub⊙ t)) ⟩ + ⟦ e₂ ⟧A i (exec (comp e₁ (i ∣sub⊙ t))) ≡⟨ proj₂ $ comp′ e₂ (comp e₁ (i ∣sub⊙ t)) ⟩ + exec (comp e₂ (comp e₁ (i ∣sub⊙ t))) ∎) + + correct : ∀ e → ⟦ e ⟧ ≡ exec (comp e halt) + correct e = begin + ⟦ e ⟧ ≡⟨ proj₂ (Accumulator.correct e) ⟩ + ⟦ e ⟧A 0 Accumulator.halt ≡⟨ refl ⟩ + ⟦ e ⟧A 0 (exec halt) ≡⟨ proj₂ (comp′ e halt) ⟩ + exec (comp e halt) ∎