[Turned _⇨_ into a data type with the constructors return and Λ. Nils Anders Danielsson **20091130171248 Ignore-this: 10f167b1e081a4c0cbab04a4f49a1cb4 + This made some proofs more complicated, because less evaluation takes place. However, the definition of _>>=_ is nicer. ] hunk ./CompositionBased.agda 12 -open P.≡-Reasoning +import Relation.Binary.HeterogeneousEquality as H hunk ./CompositionBased.agda 14 -open import Derivation -open import ReverseComposition +open import ReverseComposition as RC hiding (module Derivation) hunk ./CompositionBased.agda 36 - [⟦_⟧] : Expr → ℕ ↑ 0 - [⟦ e ⟧] = [ ⟦ e ⟧ ] + open RC.Derivation + open MonoidLaws + + ⟦_⟧↑ : Expr → ℕ ↑ 0 + ⟦ e ⟧↑ = return ⟦ e ⟧ hunk ./CompositionBased.agda 43 - sub = [ _∸_ ] + sub = Λ λ m → Λ λ n → return (m ∸ n) hunk ./CompositionBased.agda 50 - eval : (e : Expr) → EqualTo [⟦ e ⟧] - eval (val n) = ▷ begin return n ∎ - eval (e₁ ⊖ e₂) = ▷ begin - [ ⟦ e₁ ⟧ ∸ ⟦ e₂ ⟧ ] ≡⟨ P.refl ⟩ - [⟦ e₂ ⟧] ⊙ [⟦ e₁ ⟧] ⊙ sub ≡⟨ P.cong₂ (λ f g → f ⊙ g ⊙ sub) - (proof (eval e₂)) - (proof (eval e₁)) ⟩ - ⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧C ⊙ sub ∎ + 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 ∎ hunk ./CompositionBased.agda 63 - open Compositional using ([⟦_⟧]; sub; ⟦_⟧C) + open RC.Derivation + open MonoidLaws + open Compositional using (⟦_⟧↑; sub; ⟦_⟧C) hunk ./CompositionBased.agda 74 - eval (val n) f = ▷ begin return n ⊙ f ∎ - eval (e₁ ⊖ e₂) f = ▷ begin - (⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧C ⊙ sub) ⊙ f ≡⟨ P.refl ⟩ - ⟦ e₂ ⟧C ⊙ (⟦ e₁ ⟧C ⊙ sub) ⊙ f ≡⟨ P.refl ⟩ - ⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧C ⊙ sub ⊙ f ≡⟨ P.cong (_⊙_ ⟦ e₂ ⟧C) - (proof (eval e₁ (sub ⊙ f))) ⟩ - ⟦ e₂ ⟧C ⊙ ⟦ e₁ ⟧A (sub ⊙ f) ≡⟨ proof (eval e₂ (⟦ e₁ ⟧A (sub ⊙ 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))) ⟩ hunk ./CompositionBased.agda 87 - correct : ∀ e → ∃ λ f → [⟦ e ⟧] ≡ ⟦ e ⟧A f + correct : ∀ e → ∃ λ f → ⟦ e ⟧↑ ≈ ⟦ e ⟧A f hunk ./CompositionBased.agda 89 - [⟦ e ⟧] ≡⟨ proof $ Compositional.eval e ⟩ - ⟦ e ⟧C ≡⟨ P.refl ⟩ - ⟦ e ⟧C ⊙ halt ≡⟨ proof $ eval e halt ⟩ + ⟦ e ⟧↑ ≈⟨ proof $ Compositional.eval e ⟩ + ⟦ e ⟧C ≈⟨ sym $ right-identity ⟦ e ⟧C ⟩ + ⟦ e ⟧C ⊙ halt ≈⟨ proof $ eval e halt ⟩ hunk ./CompositionBased.agda 94 + -- ⟦_⟧A preserves equality of the accumulators. + + ⟦_⟧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)) + hunk ./CompositionBased.agda 107 - open Compositional using ([⟦_⟧]; sub) - open Accumulator using (⟦_⟧A) + open RC.Derivation + open Compositional using (⟦_⟧↑; sub) + open Accumulator using (⟦_⟧A; ⟦_⟧A-cong) hunk ./CompositionBased.agda 129 - exec halt = [ (λ n → n) ] + exec halt = Λ λ n → return n hunk ./CompositionBased.agda 139 - ∃ λ (t′ : Term i) → ⟦ e ⟧A (exec t) ≡ exec t′ + ∃ λ (t′ : Term i) → ⟦ e ⟧A (exec t) ≈ exec t′ hunk ./CompositionBased.agda 145 - ⟦ e₂ ⟧A (⟦ e₁ ⟧A (exec (sub⊙ t))) ≡⟨ P.cong (⟦_⟧A e₂) (proj₂ $ comp′ e₁ (sub⊙ t)) ⟩ - ⟦ e₂ ⟧A (exec (comp e₁ (sub⊙ t))) ≡⟨ proj₂ $ comp′ e₂ (comp e₁ (sub⊙ t)) ⟩ + ⟦ 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)) ⟩ hunk ./CompositionBased.agda 149 - correct : ∀ e → [⟦ e ⟧] ≡ exec (comp e halt) + correct : ∀ e → ⟦ e ⟧↑ ≈ exec (comp e halt) hunk ./CompositionBased.agda 151 - [⟦ e ⟧] ≡⟨ proj₂ (Accumulator.correct e) ⟩ + ⟦ e ⟧↑ ≈⟨ proj₂ (Accumulator.correct e) ⟩ hunk ./CompositionBased.agda 153 - ⟦ e ⟧A (exec halt) ≡⟨ proj₂ (comp′ e halt) ⟩ + ⟦ e ⟧A (exec halt) ≈⟨ proj₂ (comp′ e halt) ⟩ hunk ./CompositionBased.agda 161 + open import Derivation + open P.≡-Reasoning hunk ./CompositionBased.agda 188 + open H.≅-Reasoning + hunk ./CompositionBased.agda 200 - correct e = begin - ⟦ e ⟧ ≡⟨ P.cong ! $ Defunctionalised.correct e ⟩ + correct e = H.≅-to-≡ (begin + ⟦ e ⟧ ≅⟨ !-cong (Defunctionalised.correct e) ⟩ hunk ./CompositionBased.agda 204 - exec (comp e) ∎ + exec (comp e) ∎) hunk ./ReverseComposition.agda 19 -infixl 5 _⇨′_ _⇨_ _↑_ +infixl 5 _⇨_ hunk ./ReverseComposition.agda 21 -_⇨′_ : List Set → Set → Set -[] ⇨′ B = B -(A ∷ As) ⇨′ B = A → (As ⇨′ B) - --- Given a value of type As ⇨′ B Agda cannot infer the values of As or --- B, because As ⇨′ B is equal to [] ⇨′ (As ⇨′ B). However, by --- wrapping up the function space in a type one can ensure that the --- parameters can be inferred. - -record _⇨_ (As : List Set) (B : Set) : Set where - constructor [_] - field - ! : As ⇨′ B - -open _⇨_ public +data _⇨_ : List Set → Set → Set₁ where + return : ∀ {B} (x : B) → [] ⇨ B + Λ : ∀ {A As B} (f : A → As ⇨ B) → (A ∷ As) ⇨ B hunk ./ReverseComposition.agda 30 -f · x = [ ! f x ] +Λ f · x = f x hunk ./ReverseComposition.agda 32 --- Abstraction. +-- Extraction of the result. hunk ./ReverseComposition.agda 34 -Λ : ∀ {A As B} → (A → As ⇨ B) → (A ∷ As) ⇨ B -Λ f = [ ! ∘ f ] +! : ∀ {B} → [] ⇨ B → B +! (return x) = x hunk ./ReverseComposition.agda 40 -_↑_ : Set → ℕ → Set +infixl 5 _↑_ + +_↑_ : Set → ℕ → Set₁ hunk ./ReverseComposition.agda 48 -app x [] = ! x -app f (x ∷ xs) = app (f · x) xs +app {n = zero} x [] = ! x +app {n = suc n} f (x ∷ xs) = app (f · x) xs hunk ./ReverseComposition.agda 57 - val : ∀ {B} {x : [] ⇨ B} → x ≈ x - fun : ∀ {A As₁ B₁ As₂ B₂} {f₁ : A ∷ As₁ ⇨ B₁} {f₂ : A ∷ As₂ ⇨ B₂} - (f₁≈f₂ : ∀ x → f₁ · x ≈ f₂ · x) → f₁ ≈ f₂ + return : ∀ {B} {x : B} → return x ≈ return x + Λ : ∀ {A As₁ B₁ As₂ B₂} {f₁ : A → As₁ ⇨ B₁} {f₂ : A → As₂ ⇨ B₂} + (f₁≈f₂ : ∀ x → f₁ x ≈ f₂ x) → Λ f₁ ≈ Λ f₂ hunk ./ReverseComposition.agda 61 -refl : ∀ {As B} {f : As ⇨ B} → f ≈ f -refl {[]} = val -refl {A ∷ As} = fun (λ _ → refl) +refl : ∀ {As B} (f : As ⇨ B) → f ≈ f +refl (return x) = return +refl (Λ f) = Λ (λ x → refl (f x)) hunk ./ReverseComposition.agda 67 -sym val = val -sym (fun f≈g) = fun (sym ∘ f≈g) +sym return = return +sym (Λ f≈g) = Λ (sym ∘ f≈g) hunk ./ReverseComposition.agda 73 -trans val val = val -trans (fun f≈g) (fun g≈h) = fun (λ x → trans (f≈g x) (g≈h x)) +trans return return = return +trans (Λ f≈g) (Λ g≈h) = Λ (λ x → trans (f≈g x) (g≈h x)) + +-- Equational reasoning. hunk ./ReverseComposition.agda 103 - _ ∎ = relTo refl + f ∎ = relTo (refl f) + +-- A module which can be used when deriving code from a specification +-- of the form "∃ λ g → f ≈ g". + +module Derivation where + + open ≈-Reasoning public + + infix 0 ▷_ + + EqualTo : ∀ {As B} → As ⇨ B → Set₁ + EqualTo {As} {B} f = ∃ λ (g : As ⇨ B) → f ≈ g + + ▷_ : ∀ {As B} {f g : As ⇨ B} → f IsRelatedTo g → EqualTo f + ▷ f≈g = , (begin f≈g) + + witness : ∀ {As B} {f : As ⇨ B} → EqualTo f → As ⇨ B + witness = proj₁ + + proof : ∀ {As B} {f : As ⇨ B} (f≈ : EqualTo f) → f ≈ witness f≈ + proof = proj₂ + +-- Eta equality. + +η : ∀ {A As B} {f : (A ∷ As) ⇨ B} → Λ (λ x → f · x) ≡ f +η {f = Λ f} = P.refl + +-- Some congruences. + +_·-cong_ : ∀ {A₁ As₁ B₁ x₁} {f₁ : A₁ ∷ As₁ ⇨ B₁} + {A₂ As₂ B₂ x₂} {f₂ : A₂ ∷ As₂ ⇨ B₂} → + f₁ ≈ f₂ → x₁ ≅ x₂ → f₁ · x₁ ≈ f₂ · x₂ +Λ f₁≈f₂ ·-cong H.refl = f₁≈f₂ _ + +!-cong : ∀ {B₁} {x₁ : [] ⇨ B₁} + {B₂} {x₂ : [] ⇨ B₂} → + x₁ ≈ x₂ → ! x₁ ≅ ! x₂ +!-cong return = H.refl hunk ./ReverseComposition.agda 146 -infixr 9 _⊙_ hunk ./ReverseComposition.agda 149 -_>>=_ {[]} x g = g (! x) -_>>=_ {A ∷ As} f g = Λ λ x → f · x >>= g - -return : ∀ {A} → A → [] ⇨ A -return x = [ x ] +return x >>= g = g x +Λ f >>= g = Λ λ x → f x >>= g hunk ./ReverseComposition.agda 158 - left-identity f x = refl + left-identity f x = refl (f x) hunk ./ReverseComposition.agda 161 - right-identity {[]} x = refl - right-identity {A ∷ As} f = fun (λ x → right-identity (f · x)) + right-identity (return x) = return + right-identity (Λ f) = Λ (λ x → right-identity (f x)) hunk ./ReverseComposition.agda 167 - assoc {[]} x g h = refl - assoc {A ∷ As} f g h = fun (λ x → assoc (f · x) g h) + assoc (return x) g h = refl (g x >>= h) + assoc (Λ f) g h = Λ (λ x → assoc (f x) g h) + + infixl 6 _>>=-cong_ + + _>>=-cong_ : ∀ {As₁ B₁ Bs₁ C₁} {f₁ : As₁ ⇨ B₁} {g₁ : B₁ → Bs₁ ⇨ C₁} + {As₂ B₂ Bs₂ C₂} {f₂ : As₂ ⇨ B₂} {g₂ : B₂ → Bs₂ ⇨ C₂} → + f₁ ≈ f₂ → (∀ {x₁ x₂} → x₁ ≅ x₂ → g₁ x₁ ≈ g₂ x₂) → + f₁ >>= g₁ ≈ f₂ >>= g₂ + return >>=-cong g₁≈g₂ = g₁≈g₂ H.refl + Λ f₁≈f₂ >>=-cong g₁≈g₂ = Λ λ x → f₁≈f₂ x >>=-cong g₁≈g₂ hunk ./ReverseComposition.agda 181 +infixr 9 _⊙_ + hunk ./ReverseComposition.agda 191 + open MonadLaws using (_>>=-cong_) hunk ./ReverseComposition.agda 207 - (Λ λ x → f · x) ≡⟨ P.refl ⟩ + (Λ λ x → f · x) ≡⟨ η ⟩ hunk ./ReverseComposition.agda 215 - assoc f g h = begin - (f ⊙ g) ⊙ h ≡⟨ P.refl ⟩ - f >>= _·_ g >>= _·_ h ≈⟨ MonadLaws.assoc f (_·_ g) (_·_ h) ⟩ - f >>= (λ x → g · x >>= _·_ h) ≡⟨ P.refl ⟩ - f ⊙ (g ⊙ h) ∎ - ------------------------------------------------------------------------- --- Various congruences which could come in handy - -module Congruences where - - _·-cong_ : ∀ {A₁ As₁ B₁ x₁} {f₁ : A₁ ∷ As₁ ⇨ B₁} - {A₂ As₂ B₂ x₂} {f₂ : A₂ ∷ As₂ ⇨ B₂} → - f₁ ≈ f₂ → x₁ ≅ x₂ → f₁ · x₁ ≈ f₂ · x₂ - fun f₁≈f₂ ·-cong H.refl = f₁≈f₂ _ - - Λ-cong : ∀ {A₁ As₁ B₁} {f₁ : A₁ → As₁ ⇨ B₁} - {A₂ As₂ B₂} {f₂ : A₂ → As₂ ⇨ B₂} → - A₁ ≡ A₂ → (∀ {x₁ x₂} → x₁ ≅ x₂ → f₁ x₁ ≈ f₂ x₂) → - Λ f₁ ≈ Λ f₂ - Λ-cong P.refl f₁≈f₂ = fun (λ _ → f₁≈f₂ H.refl) - - _>>=-cong_ : ∀ {As₁ B₁ Bs₁ C₁} {f₁ : As₁ ⇨ B₁} {g₁ : B₁ → Bs₁ ⇨ C₁} - {As₂ B₂ Bs₂ C₂} {f₂ : As₂ ⇨ B₂} {g₂ : B₂ → Bs₂ ⇨ C₂} → - f₁ ≈ f₂ → (∀ {x₁ x₂} → x₁ ≅ x₂ → g₁ x₁ ≈ g₂ x₂) → - f₁ >>= g₁ ≈ f₂ >>= g₂ - val >>=-cong g₁≈g₂ = g₁≈g₂ H.refl - fun f₁≈f₂ >>=-cong g₁≈g₂ = fun (λ x → f₁≈f₂ x >>=-cong g₁≈g₂) + assoc f (Λ g) h = begin + (f ⊙ Λ g) ⊙ h ≡⟨ P.refl ⟩ + f >>= g >>= _·_ h ≈⟨ MonadLaws.assoc f g (_·_ h) ⟩ + f >>= (λ x → g x >>= _·_ h) ≈⟨ refl f >>=-cong (λ x₁≅x₂ → + (refl (Λ g) ·-cong x₁≅x₂) >>=-cong + _·-cong_ (refl h)) ⟩ + f ⊙ (Λ g ⊙ h) ∎ hunk ./ReverseComposition.agda 223 - return-cong : ∀ {A₁ A₂} {x₁ : A₁} {x₂ : A₂} → - x₁ ≅ x₂ → return x₁ ≈ return x₂ - return-cong H.refl = refl + infixr 9 _⊙-cong_ hunk ./ReverseComposition.agda 231 - identity-cong = refl + identity-cong = refl identity