module CompositionBased where
open import Data.Nat
open import Data.Product
open import Data.Vec using (Vec; []; _∷_)
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)
import Relation.Binary.HeterogeneousEquality as H
import Derivation
open import ReverseComposition as RC
hiding (_↑_⇨_; module Derivation; module Stack)
data Expr : Set where
val : (n : ℕ) → Expr
_⊖_ : (e₁ e₂ : Expr) → Expr
⟦_⟧ : Expr → ℕ
⟦ val n ⟧ = n
⟦ e₁ ⊖ e₂ ⟧ = ⟦ e₁ ⟧ ∸ ⟦ e₂ ⟧
infixl 5 _↑_
_↑_ : Set → ℕ → Set
A ↑ n = RC._↑_⇨_ A n A
module Compositional where
open RC.Derivation
open MonoidLaws
⟦_⟧↑ : Expr → ℕ ↑ 0
⟦ e ⟧↑ = return ⟦ e ⟧
sub : ℕ ↑ 2
sub = Λ λ m → Λ λ n → return (m ∸ n)
mutual
⟦_⟧C : Expr → ℕ ↑ 0
⟦ e ⟧C = witness (eval e)
eval : (e : Expr) → EqualTo ⟦ e ⟧↑
eval (val n) = ▷ return n ∎
eval (e₁ ⊖ e₂) = ▷
return (⟦ e₁ ⟧ ∸ ⟦ e₂ ⟧) ≡⟨ P.refl ⟩
⟦ e₂ ⟧↑ ⊙ ⟦ e₁ ⟧↑ ⊙ sub ≈⟨ proof (eval e₂) ⊙-cong
proof (eval e₁) ⊙-cong refl sub ⟩
⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧C ⊙ sub ∎
module Accumulator where
open RC.Derivation
open MonoidLaws
open Compositional using (⟦_⟧↑; sub; ⟦_⟧C)
mutual
⟦_⟧A : Expr → ∀ {i} → ℕ ↑ suc i → ℕ ↑ i
⟦ e ⟧A f = witness (eval e f)
eval : ∀ (e : Expr) {i} (f : ℕ ↑ suc i) →
EqualTo (⟦ e ⟧C ⊙ f)
eval (val n) f = ▷ return n ⊙ f ∎
eval (e₁ ⊖ e₂) f = ▷
(⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧C ⊙ sub) ⊙ f ≈⟨ assoc ⟦ e₂ ⟧C (⟦ e₁ ⟧C ⊙ sub) f ⟩
⟦ e₂ ⟧C ⊙ (⟦ e₁ ⟧C ⊙ sub) ⊙ f ≈⟨ refl ⟦ e₂ ⟧C ⊙-cong
assoc ⟦ e₁ ⟧C sub f ⟩
⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧C ⊙ sub ⊙ f ≈⟨ refl ⟦ e₂ ⟧C ⊙-cong
proof (eval e₁ (sub ⊙ f)) ⟩
⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧A (sub ⊙ f) ≈⟨ proof (eval e₂ (⟦ e₁ ⟧A (sub ⊙ f))) ⟩
⟦ e₂ ⟧A (⟦ e₁ ⟧A (sub ⊙ f)) ∎
halt : ℕ ↑ 1
halt = identity
correct : ∀ e → ∃ λ f → ⟦ e ⟧↑ ≈ ⟦ e ⟧A f
correct e = halt , (
⟦ e ⟧↑ ≈⟨ proof $ Compositional.eval e ⟩
⟦ e ⟧C ≈⟨ sym $ right-identity ⟦ e ⟧C ⟩
⟦ e ⟧C ⊙ halt ≈⟨ proof $ eval e halt ⟩
⟦ e ⟧A halt ∎)
⟦_⟧A-cong : (e : Expr) → ∀ {i} {f g : ℕ ↑ suc i} →
f ≈ g → ⟦ e ⟧A f ≈ ⟦ e ⟧A g
⟦_⟧A-cong (val n) f≈g = f≈g ·-cong H.refl
⟦_⟧A-cong (e₁ ⊖ e₂) f≈g =
⟦ e₂ ⟧A-cong (⟦ e₁ ⟧A-cong (refl sub ⊙-cong f≈g))
module Defunctionalised where
open RC.Derivation
open Compositional using (⟦_⟧↑; sub)
open Accumulator using (⟦_⟧A; ⟦_⟧A-cong)
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
apply : ∀ {i} → Term i → ℕ ↑ i
apply (return⊙ n t) = return n ⊙ apply t
apply (sub⊙ t) = sub ⊙ apply t
apply halt = Accumulator.halt
exec : ∀ {i} → Term i → ℕ ↑ i
exec (return⊙ n t) = exec t · n
exec (sub⊙ t) = Λ λ m → Λ λ n → exec t · (m ∸ n)
exec halt = Λ λ n → return n
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 (exec t) ≈ exec t′
comp′ (val n) t = return⊙ n t , (
exec t · n ≡⟨ P.refl ⟩
exec (return⊙ n t) ∎)
comp′ (e₁ ⊖ e₂) t = comp e₂ (comp e₁ (sub⊙ t)) , (
⟦ e₂ ⟧A (⟦ e₁ ⟧A (sub ⊙ exec t)) ≡⟨ P.refl ⟩
⟦ e₂ ⟧A (⟦ e₁ ⟧A (exec (sub⊙ t))) ≈⟨ ⟦ e₂ ⟧A-cong (proj₂ $ comp′ e₁ (sub⊙ t)) ⟩
⟦ e₂ ⟧A (exec (comp e₁ (sub⊙ t))) ≈⟨ proj₂ $ comp′ e₂ (comp e₁ (sub⊙ t)) ⟩
exec (comp e₂ (comp e₁ (sub⊙ t))) ∎)
correct : ∀ e → ⟦ e ⟧↑ ≈ exec (comp e halt)
correct e =
⟦ e ⟧↑ ≈⟨ proj₂ (Accumulator.correct e) ⟩
⟦ e ⟧A Accumulator.halt ≡⟨ P.refl ⟩
⟦ e ⟧A (exec halt) ≈⟨ proj₂ (comp′ e halt) ⟩
exec (comp e halt) ∎
module Stack where
open Derivation
open Compositional using (⟦_⟧↑)
open Defunctionalised using (Term; return⊙; sub⊙; halt; comp)
open P.≡-Reasoning
_^_ : Set → ℕ → Set
A ^ n = Vec A n → A
mutual
exec : ∀ {i} → Term i → ℕ ^ i
exec t = witness ∘ exec′ t
exec′ : ∀ {i} (t : Term i) (xs : Vec ℕ i) →
EqualTo (app (Defunctionalised.exec t) xs)
exec′ (return⊙ n t) s = ▷ begin
app (Defunctionalised.exec t) (n ∷ s) ≡⟨ proof (exec′ t (n ∷ s)) ⟩
exec t (n ∷ s) ∎
exec′ (sub⊙ t) (m ∷ n ∷ s) = ▷ begin
app (Defunctionalised.exec t) (m ∸ n ∷ s) ≡⟨ proof (exec′ t (m ∸ n ∷ s)) ⟩
exec t (m ∸ n ∷ s) ∎
exec′ halt (n ∷ []) = ▷ begin n ∎
correct : ∀ e → ⟦ e ⟧ ≡ exec (comp e halt) []
correct e = begin
⟦ e ⟧ ≡⟨ P.refl ⟩
run ⟦ e ⟧↑ ≡⟨ run-cong (Defunctionalised.correct e) ⟩
run (Defunctionalised.exec (comp e halt)) ≡⟨ P.refl ⟩
app {A = ℕ} (Defunctionalised.exec (comp e halt)) [] ≡⟨ proj₂ $ exec′ (comp e halt) [] ⟩
exec (comp e halt) [] ∎
module Finally where
Code : Set
Code = Defunctionalised.Term 0
comp : Expr → Code
comp e = Defunctionalised.comp e Defunctionalised.halt
exec : Code → ℕ
exec = flip Stack.exec []
correct : ∀ e → ⟦ e ⟧ ≡ exec (comp e)
correct = Stack.correct