module CompositionBased.Exceptions where
open import Category.Monad
open import Data.List using (List; []; [_]; _∷_)
open import Data.Maybe as Maybe
open import Data.Nat
open import Data.Product
open import Data.Vec using (Vec; []; _∷_)
open import Function
import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)
import Relation.Binary.HeterogeneousEquality as H
private
open module M = RawMonadPlus (Maybe.monadPlus {f = Level.zero})
using (∅; _<$>_; _⊛_; _∣_)
import Derivation
open import ReverseComposition as RC
hiding (_↑_⇨_; module Derivation; push; pop; module Stack)
data Expr : Set where
val : (n : ℕ) → Expr
_⊖_ : (e₁ e₂ : Expr) → Expr
throw : Expr
_catch_ : (e₁ e₂ : Expr) → Expr
⟦_⟧ : Expr → Maybe ℕ
⟦ val n ⟧ = M.return n
⟦ e₁ ⊖ e₂ ⟧ = _∸_ <$> ⟦ e₁ ⟧ ⊛ ⟦ e₂ ⟧
⟦ throw ⟧ = ∅
⟦ e₁ catch e₂ ⟧ = ⟦ e₁ ⟧ ∣ ⟦ e₂ ⟧
infixl 5 _↑_
_↑_ : Set → ℕ → Set
A ↑ n = RC._↑_⇨_ A n (Maybe A)
module Compositional where
open RC.Derivation
open LawsM
open MonoidLawsM
⟦_⟧↑ : Expr → ℕ ↑ 0
⟦ e ⟧↑ = return ⟦ e ⟧
sub : ℕ ↑ 2
sub = Λ λ m → Λ λ n → returnM (m ∸ n)
private
lemma : ∀ m₁ m₂ →
return (_∸_ <$> m₁ ⊛ m₂) ≡ return m₂ ⊙M return m₁ ⊙M sub
lemma (just n₁) (just n₂) = P.refl
lemma (just n₁) nothing = P.refl
lemma nothing (just n₂) = P.refl
lemma nothing nothing = P.refl
mutual
⟦_⟧C : Expr → ℕ ↑ 0
⟦ e ⟧C = witness (eval e)
eval : (e : Expr) → EqualTo ⟦ e ⟧↑
eval (val n) = ▷
return (just n) ≡⟨ P.refl ⟩
returnM n ∎
eval (e₁ ⊖ e₂) = ▷
return (_∸_ <$> ⟦ e₁ ⟧ ⊛ ⟦ e₂ ⟧) ≡⟨ lemma ⟦ e₁ ⟧ ⟦ e₂ ⟧ ⟩
⟦ e₂ ⟧↑ ⊙M ⟦ e₁ ⟧↑ ⊙M sub ≈⟨ proof (eval e₂) ⊙M-cong proof (eval e₁) ⊙M-cong refl sub ⟩
⟦ e₂ ⟧C ⊙M ⟦ e₁ ⟧C ⊙M sub ∎
eval throw = ▷
return nothing ≡⟨ P.refl ⟩
zeroM ∎
eval (e₁ catch e₂) = ▷
return (⟦ e₁ ⟧ ∣ ⟦ e₂ ⟧) ≡⟨ P.refl ⟩
⟦ e₁ ⟧↑ ⊕ ⟦ e₂ ⟧↑ ≈⟨ proof (eval e₁) ⊕-cong proof (eval e₂) ⟩
⟦ e₁ ⟧C ⊕ ⟦ e₂ ⟧C ∎
module Accumulator where
open RC.Derivation
open LawsM
open MonoidLawsM
private
open module C = Compositional using (⟦_⟧↑; ⟦_⟧C)
push : ∀ {i} → ℕ → (ℕ → ℕ ↑ i) → ℕ ↑ i
push n s = s n
sub : ∀ {i} → (ℕ → ℕ ↑ i) → ℕ → ℕ ↑ 1 + i
sub s = λ y → Λ λ x → s (y ∸ x)
pop : ∀ {i} → ℕ ↑ i → ℕ ↑ 1 + i
pop f = const⋆ [ ℕ ] f
mutual
⟦_⟧A : Expr → ∀ {i} → (ℕ → ℕ ↑ i) → ℕ ↑ i → ℕ ↑ i
⟦ e ⟧A s f = witness (eval e s f)
eval : ∀ (e : Expr) {i} (s : ℕ → ℕ ↑ i) (f : ℕ ↑ i) →
EqualTo (⟦ e ⟧C then s else f)
eval (val n) s f = ▷
s n ≡⟨ P.refl ⟩
push n s ∎
eval (e₁ ⊖ e₂) s f = ▷
(⟦ e₂ ⟧C ⊙M ⟦ e₁ ⟧C ⊙M C.sub) then s else f ≈⟨ distrib ⟦ e₂ ⟧C (_·_ (⟦ e₁ ⟧C ⊙M C.sub)) (maybe s f) ⟩
⟦ e₂ ⟧C then (λ x → (⟦ e₁ ⟧C ⊙M C.sub) · x then s else f)
else f ≈⟨ refl ⟦ e₂ ⟧C
then (λ x → complete (then-else-·₀ ⟦ e₁ ⟧C (_·_ C.sub))
then (λ _ → refl _)
else-cong refl f)
else-cong refl f ⟩
⟦ e₂ ⟧C then (λ x → (⟦ e₁ ⟧C ⊙M (Λ λ y → C.sub · y · x))
then s else f)
else f ≈⟨ refl ⟦ e₂ ⟧C
then (λ x → distrib ⟦ e₁ ⟧C (λ y → C.sub · y · x) (maybe s f))
else-cong refl f ⟩
⟦ e₂ ⟧C then (λ x → ⟦ e₁ ⟧C then (λ y → C.sub · y · x ⊙M Λ s)
else f)
else f ≡⟨ P.refl ⟩
⟦ e₂ ⟧C then (λ x → ⟦ e₁ ⟧C then (λ y → (Λ λ x → s (y ∸ x)) · x)
else const⋆ [ ℕ ] f · x)
else f ≈⟨ refl ⟦ e₂ ⟧C
then (λ _ → complete $ P.sym $
then-else-·₀ ⟦ e₁ ⟧C (λ y → Λ λ x → s (y ∸ x)))
else-cong refl f ⟩
⟦ e₂ ⟧C then _·_ (⟦ e₁ ⟧C then (λ y → Λ λ x → s (y ∸ x))
else const⋆ [ ℕ ] f)
else f ≡⟨ P.refl ⟩
⟦ e₂ ⟧C then _·_ (⟦ e₁ ⟧C then sub s else pop f) else f ≈⟨ refl ⟦ e₂ ⟧C
then (λ _ → proof (eval e₁ (sub s) (pop f)) ·-cong H.refl)
else-cong refl f ⟩
⟦ e₂ ⟧C then _·_ (⟦ e₁ ⟧A (sub s) (pop f)) else f ≈⟨ proof (eval e₂ _ _) ⟩
⟦ e₂ ⟧A (_·_ (⟦ e₁ ⟧A (sub s) (pop f))) f ∎
eval throw s f = ▷ f ∎
eval (e₁ catch e₂) s f = ▷
⟦ e₁ ⟧C ⊕ ⟦ e₂ ⟧C then s else f ≈⟨ ⊕₀ ⟦ e₁ ⟧C _ then (λ _ → refl _) else-cong refl _ ⟩
(⟦ e₁ ⟧C then returnM else ⟦ e₂ ⟧C) then s else f ≈⟨ distrib ⟦ e₁ ⟧C returnM (maybe s f) ⟩
⟦ e₁ ⟧C then (λ x → returnM x then s else f)
else (⟦ e₂ ⟧C then s else f) ≡⟨ P.refl ⟩
⟦ e₁ ⟧C then s else (⟦ e₂ ⟧C then s else f) ≈⟨ refl ⟦ e₁ ⟧C then (λ _ → refl _) else-cong proof (eval e₂ s f) ⟩
⟦ e₁ ⟧C then s else (⟦ e₂ ⟧A s f) ≈⟨ proof (eval e₁ s (⟦ e₂ ⟧A s f)) ⟩
⟦ e₁ ⟧A s (⟦ e₂ ⟧A s f) ∎
halt : ℕ → ℕ ↑ 0
halt = _·_ identityM
crash : ℕ ↑ 0
crash = zeroM
correct : ∀ e → ∃₂ λ f s → ⟦ e ⟧↑ ≈ ⟦ e ⟧A f s
correct e = halt , crash , (
⟦ e ⟧↑ ≈⟨ proof $ Compositional.eval e ⟩
⟦ e ⟧C ≈⟨ sym $ right-identities ⟦ e ⟧C ⟩
⟦ e ⟧C then halt else crash ≈⟨ proof $ eval e halt crash ⟩
⟦ e ⟧A halt crash ∎)
push-cong : ∀ {i} (n : ℕ) {s₁ s₂ : ℕ → ℕ ↑ i} →
(∀ x → s₁ x ≈ s₂ x) → push n s₁ ≈ push n s₂
push-cong n s₁≈s₂ = s₁≈s₂ n
sub-cong : ∀ {i} {s₁ s₂ : ℕ → ℕ ↑ i} →
(∀ x → s₁ x ≈ s₂ x) → ∀ x → sub s₁ x ≈ sub s₂ x
sub-cong s₁≈s₂ = λ x → Λ-cong λ y → s₁≈s₂ (x ∸ y)
pop-cong : ∀ {i} {f₁ f₂ : ℕ ↑ i} → f₁ ≈ f₂ → pop f₁ ≈ pop f₂
pop-cong f₁≈f₂ = Λ-cong λ _ → f₁≈f₂
⟦_⟧A-cong : (e : Expr) → ∀ {i} {s₁ s₂ : ℕ → ℕ ↑ i} {f₁ f₂ : ℕ ↑ i} →
(∀ x → s₁ x ≈ s₂ x) → f₁ ≈ f₂ →
⟦ e ⟧A s₁ f₁ ≈ ⟦ e ⟧A s₂ f₂
⟦ val n ⟧A-cong s₁≈s₂ f₁≈f₂ = push-cong n s₁≈s₂
⟦ e₁ ⊖ e₂ ⟧A-cong s₁≈s₂ f₁≈f₂ = ⟦ e₂ ⟧A-cong (λ _ → ⟦ e₁ ⟧A-cong (sub-cong s₁≈s₂) (pop-cong f₁≈f₂) ·-cong H.refl) f₁≈f₂
⟦ throw ⟧A-cong s₁≈s₂ f₁≈f₂ = f₁≈f₂
⟦ e₁ catch e₂ ⟧A-cong s₁≈s₂ f₁≈f₂ = ⟦ e₁ ⟧A-cong s₁≈s₂ (⟦ e₂ ⟧A-cong s₁≈s₂ f₁≈f₂)
module Defunctionalised where
open RC.Derivation
open Compositional using (⟦_⟧↑)
open Accumulator using (⟦_⟧A; ⟦_⟧A-cong)
data Term : ℕ → Set where
push : ∀ {i} (n : ℕ) (t : Term (1 + i)) → Term i
pop : ∀ {i} (t : Term i) → Term (1 + i)
sub : ∀ {i} (t : Term (1 + i)) → Term (2 + i)
halt : Term 1
crash : Term 0
apply : ∀ {i} → Term i → ℕ ↑ i
apply (push n t) = Accumulator.push n (_·_ (apply t))
apply (pop t) = Accumulator.pop (apply t)
apply (sub t) = Λ (Accumulator.sub (_·_ (apply t)))
apply halt = Λ Accumulator.halt
apply crash = Accumulator.crash
exec : ∀ {i} → Term i → ℕ ↑ i
exec (push n t) = exec t · n
exec (pop t) = Λ λ _ → exec t
exec (sub t) = Λ λ x → Λ λ y → exec t · (x ∸ y)
exec halt = Λ λ x → return (just x)
exec crash = return nothing
mutual
comp : ∀ {i} → Expr → Term (suc i) → Term i → Term i
comp e s f = proj₁ (comp′ e s f)
comp′ : ∀ (e : Expr) {i} (s : Term (suc i)) (f : Term i) →
∃ λ (t : Term i) → ⟦ e ⟧A (_·_ (exec s)) (exec f) ≈ exec t
comp′ (val n) s f = push n s , (
exec s · n ≡⟨ P.refl ⟩
exec (push n s) ∎)
comp′ (e₁ ⊖ e₂) s f = comp e₂ (comp e₁ (sub s) (pop f)) f , (
⟦ e₂ ⟧A (_·_ (⟦ e₁ ⟧A (Accumulator.sub (_·_ (exec s)))
(Accumulator.pop (exec f))))
(exec f) ≡⟨ P.refl ⟩
⟦ e₂ ⟧A (_·_ (⟦ e₁ ⟧A (_·_ (exec (sub s))) (exec (pop f))))
(exec f) ≈⟨ ⟦ e₂ ⟧A-cong (λ _ → proj₂ (comp′ e₁ (sub s) (pop f)) ·-cong H.refl) (refl _) ⟩
⟦ e₂ ⟧A (_·_ (exec (comp e₁ (sub s) (pop f)))) (exec f) ≈⟨ proj₂ $ comp′ e₂ (comp e₁ (sub s) (pop f)) f ⟩
exec (comp e₂ (comp e₁ (sub s) (pop f)) f) ∎)
comp′ throw s f = f , (
exec f ∎)
comp′ (e₁ catch e₂) s f = comp e₁ s (comp e₂ s f) , (
⟦ e₁ ⟧A (_·_ (exec s)) (⟦ e₂ ⟧A (_·_ (exec s)) (exec f)) ≈⟨ ⟦ e₁ ⟧A-cong (λ _ → refl _) (proj₂ $ comp′ e₂ s f) ⟩
⟦ e₁ ⟧A (_·_ (exec s)) (exec (comp e₂ s f)) ≈⟨ proj₂ $ comp′ e₁ s (comp e₂ s f) ⟩
exec (comp e₁ s (comp e₂ s f)) ∎)
correct : ∀ e → ⟦ e ⟧↑ ≈ exec (comp e halt crash)
correct e =
⟦ e ⟧↑ ≈⟨ proj₂ $ proj₂ $ Accumulator.correct e ⟩
⟦ e ⟧A Accumulator.halt Accumulator.crash ≡⟨ P.refl ⟩
⟦ e ⟧A (_·_ (exec halt)) (exec crash) ≈⟨ proj₂ (comp′ e halt crash) ⟩
exec (comp e halt crash) ∎
module Stack where
open Derivation
open Compositional using (⟦_⟧↑)
open Defunctionalised using (Term; comp)
open Defunctionalised.Term
open P.≡-Reasoning
_^_ : Set → ℕ → Set
A ^ n = Vec A n → Maybe 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′ (push n t) xs = ▷ begin
app (Defunctionalised.exec t · n) xs ≡⟨ proj₂ (exec′ t (n ∷ xs)) ⟩
exec t (n ∷ xs) ∎
exec′ (pop t) (x ∷ xs) = ▷ begin
app (Defunctionalised.exec t) xs ≡⟨ proj₂ (exec′ t xs) ⟩
exec t xs ∎
exec′ (sub t) (x ∷ y ∷ xs) = ▷ begin
app (Defunctionalised.exec t · (x ∸ y)) xs ≡⟨ proj₂ (exec′ t (x ∸ y ∷ xs)) ⟩
exec t (x ∸ y ∷ xs) ∎
exec′ halt (x ∷ []) = ▷ begin just x ∎
exec′ crash [] = ▷ begin nothing ∎
correct : ∀ e → ⟦ e ⟧ ≡ exec (comp e halt crash) []
correct e = begin
⟦ e ⟧ ≡⟨ P.refl ⟩
run ⟦ e ⟧↑ ≡⟨ run-cong (Defunctionalised.correct e) ⟩
run (Defunctionalised.exec (comp e halt crash)) ≡⟨ P.refl ⟩
app {A = ℕ} (Defunctionalised.exec (comp e halt crash)) [] ≡⟨ proj₂ $ exec′ (comp e halt crash) [] ⟩
exec (comp e halt crash) [] ∎
module Finally where
Code : Set
Code = Defunctionalised.Term 0
comp : Expr → Code
comp e = Defunctionalised.comp e
Defunctionalised.halt Defunctionalised.crash
exec : Code → Maybe ℕ
exec = flip Stack.exec []
correct : ∀ e → ⟦ e ⟧ ≡ exec (comp e)
correct = Stack.correct