From 63e012183dba4d09e6f453579ebc42d13a910c08 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Wed, 13 Mar 2024 00:16:04 +0100 Subject: [PATCH] Compile 2CC to 2ADT --- src/Data/IndexedSet.lagda.md | 3 + src/Translation/Lang/2CC-to-2ADT.agda | 138 ++++++++++++++++++++++++++ 2 files changed, 141 insertions(+) create mode 100644 src/Translation/Lang/2CC-to-2ADT.agda diff --git a/src/Data/IndexedSet.lagda.md b/src/Data/IndexedSet.lagda.md index 3076dc23..71a6566f 100644 --- a/src/Data/IndexedSet.lagda.md +++ b/src/Data/IndexedSet.lagda.md @@ -191,6 +191,9 @@ syntax ≅[]→≅ e = ≅-by-index-translation e (λ i → A≐B i ) , (λ i → sym (A≐B i)) +≗→≅[] : ∀ {I} {A B : IndexedSet I} → A ≗ B → A ≅[ id ][ id ] B +≗→≅[] = ≐→≅[] ∘ ≗→≐ + irrelevant-index-⊆ : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} → (x : Carrier) → (∀ i → A i ≈ x) diff --git a/src/Translation/Lang/2CC-to-2ADT.agda b/src/Translation/Lang/2CC-to-2ADT.agda new file mode 100644 index 00000000..d85f9d8a --- /dev/null +++ b/src/Translation/Lang/2CC-to-2ADT.agda @@ -0,0 +1,138 @@ +{-# OPTIONS --sized-types #-} + +open import Framework.Construct using (_∈ₛ_; cons) +open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) + +module Translation.Lang.2CC-to-2ADT (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where + +import Data.EqIndexedSet as IndexedSet +open import Data.Bool as Bool using (if_then_else_) +open import Data.Bool.Properties as Bool +open import Data.List as List using (List; []; _∷_; _ʳ++_) +import Data.List.Properties as List +open import Framework.Compiler using (LanguageCompiler) +open import Framework.Definitions using (𝔸; 𝔽) +open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_) +open import Framework.Relation.Function using (from; to) +open import Function using (id) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_) +open import Size using (Size) + +open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[]) + +import Lang.2CC +module 2CC where + open Lang.2CC using (2CC; _-<_>-; _⟨_,_⟩) public + module 2CC-Sem-1 D = Lang.2CC.Sem D Variant Artifact∈ₛVariant + open 2CC-Sem-1 using (2CCL) public + module 2CC-Sem-2 {D} = Lang.2CC.Sem D Variant Artifact∈ₛVariant + open 2CC-Sem-2 using (⟦_⟧) public +open 2CC using (2CC; 2CCL) + +import Lang.2ADT +module 2ADT where + module 2ADT-Sem-1 D = Lang.2ADT D Variant + open 2ADT-Sem-1 using (2ADT; 2ADTL; Configuration) public + module 2ADT-Sem-2 {D} = Lang.2ADT D Variant + open 2ADT-Sem-2 using (⟦_⟧) public +open 2ADT using (2ADT; 2ADTL) + +artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A +artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs) + + +push-down-artifact : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → A → List (2ADT D A) → 2ADT D A +push-down-artifact {A = A} a cs = go cs [] + module push-down-artifact-Implementation where + go : ∀ {i : Size} {D : 𝔽} → List (2ADT D A) → List (Variant A) → 2ADT D A + go [] vs = 2ADT.leaf (artifact a (List.reverse vs)) + go (2ADT.leaf v ∷ cs) vs = go cs (v ∷ vs) + go (d 2ADT.⟨ c₁ , c₂ ⟩ ∷ cs) vs = d 2ADT.⟨ go (c₁ ∷ cs) vs , go (c₂ ∷ cs) vs ⟩ + +translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → 2CC D i A + → 2ADT D A +translate (a 2CC.-< cs >-) = push-down-artifact a (List.map translate cs) +translate (d 2CC.⟨ l , r ⟩) = d 2ADT.⟨ translate l , translate r ⟩ + +⟦push-down-artifact⟧ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (a : A) + → (cs : List (2ADT D A)) + → (config : 2ADT.Configuration D) + → 2ADT.⟦ push-down-artifact a cs ⟧ config ≡ artifact a (List.map (λ e → 2ADT.⟦ e ⟧ config) cs) +⟦push-down-artifact⟧ {D = D} {A = A} a cs config = go' cs [] + where + open push-down-artifact-Implementation + + go' : ∀ {i : Size} + → (cs' : List (2ADT D A)) + → (vs : List (Variant A)) + → 2ADT.⟦ go a cs cs' vs ⟧ config ≡ artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) cs') + go' [] vs = Eq.sym (Eq.cong₂ artifact refl (Eq.trans (List.ʳ++-defn vs) (List.++-identityʳ (List.reverse vs)))) + go' (2ADT.leaf v ∷ cs') vs = Eq.trans (go' cs' (v ∷ vs)) (Eq.cong₂ artifact refl (List.ʳ++-++ List.[ v ] {ys = vs})) + go' ((d 2ADT.⟨ c₁ , c₂ ⟩) ∷ cs') vs = + 2ADT.⟦ d 2ADT.⟨ go a cs (c₁ ∷ cs') vs , go a cs (c₂ ∷ cs') vs ⟩ ⟧ config + ≡⟨⟩ + (if config d + then 2ADT.⟦ go a cs (c₁ ∷ cs') vs ⟧ config + else 2ADT.⟦ go a cs (c₂ ∷ cs') vs ⟧ config) + ≡⟨ Eq.cong₂ (if config d then_else_) (go' (c₁ ∷ cs') vs) (go' (c₂ ∷ cs') vs) ⟩ + (if config d + then artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (c₁ ∷ cs')) + else artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (c₂ ∷ cs'))) + ≡˘⟨ Bool.push-function-into-if (λ c → artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (c ∷ cs'))) (config d) ⟩ + artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) ((if config d then c₁ else c₂) ∷ cs')) + ≡⟨⟩ + artifact a (vs ʳ++ 2ADT.⟦ if config d then c₁ else c₂ ⟧ config ∷ List.map (λ e → 2ADT.⟦ e ⟧ config) cs') + ≡⟨ Eq.cong₂ artifact refl (Eq.cong₂ _ʳ++_ {x = vs} refl (Eq.cong₂ _∷_ (Bool.push-function-into-if (λ e → 2ADT.⟦ e ⟧ config) (config d)) refl)) ⟩ + artifact a (vs ʳ++ (if config d then 2ADT.⟦ c₁ ⟧ config else 2ADT.⟦ c₂ ⟧ config) ∷ List.map (λ e → 2ADT.⟦ e ⟧ config) cs') + ≡⟨⟩ + artifact a (vs ʳ++ 2ADT.⟦ d 2ADT.⟨ c₁ , c₂ ⟩ ⟧ config ∷ List.map (λ e → 2ADT.⟦ e ⟧ config) cs') + ≡⟨⟩ + artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (d 2ADT.⟨ c₁ , c₂ ⟩ ∷ cs')) + ∎ + +preserves-≗ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (expr : 2CC D i A) + → 2ADT.⟦ translate expr ⟧ ≗ 2CC.⟦ expr ⟧ +preserves-≗ {D = D} {A = A} (a 2CC.-< cs >-) config = + 2ADT.⟦ translate (a 2CC.-< cs >-) ⟧ config + ≡⟨⟩ + 2ADT.⟦ push-down-artifact a (List.map translate cs) ⟧ config + ≡⟨ ⟦push-down-artifact⟧ a (List.map translate cs) config ⟩ + artifact a (List.map (λ e → 2ADT.⟦ e ⟧ config) (List.map translate cs)) + ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → 2ADT.⟦ translate e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-≗ e config) cs) ⟩ + artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) cs) + ≡⟨⟩ + 2CC.⟦ a 2CC.-< cs >- ⟧ config + ∎ +preserves-≗ (d 2CC.⟨ l , r ⟩) config = + 2ADT.⟦ translate (d 2CC.⟨ l , r ⟩) ⟧ config + ≡⟨⟩ + 2ADT.⟦ d 2ADT.⟨ translate l , translate r ⟩ ⟧ config + ≡⟨⟩ + (if config d then 2ADT.⟦ translate l ⟧ config else 2ADT.⟦ translate r ⟧ config) + ≡˘⟨ Bool.push-function-into-if (λ e → 2ADT.⟦ translate e ⟧ config) (config d) ⟩ + 2ADT.⟦ translate (if config d then l else r) ⟧ config + ≡⟨ preserves-≗ (if config d then l else r) config ⟩ + 2CC.⟦ if config d then l else r ⟧ config + ≡⟨⟩ + 2CC.⟦ d 2CC.⟨ l , r ⟩ ⟧ config + ∎ + +preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (expr : 2CC D i A) + → 2ADT.⟦ translate expr ⟧ ≅[ id ][ id ] 2CC.⟦ expr ⟧ +preserves expr = ≗→≅[] (preserves-≗ expr) + +2CC→2ADT : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (2CCL D {i}) (2ADTL D) +2CC→2ADT .LanguageCompiler.compile = translate +2CC→2ADT .LanguageCompiler.config-compiler expr .to = id +2CC→2ADT .LanguageCompiler.config-compiler expr .from = id +2CC→2ADT .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr) + +2ADT≽2CC : ∀ {D : 𝔽} → 2ADTL D ≽ 2CCL D +2ADT≽2CC = expressiveness-from-compiler 2CC→2ADT