WIP Use a compiler from Variant to CCC in NADT to CCC

VariantSync · Mar 14, 2024 · d311c07 · d311c07
1 parent 3ef6fa3
commit d311c07
Showing 1 changed file with 28 additions and 55 deletions.
diff --git a/src/Translation/Lang/NADT-to-CCC.agda b/src/Translation/Lang/NADT-to-CCC.agda
@@ -15,7 +15,7 @@ open import Data.List.Properties as List
 open import Data.List.NonEmpty as List⁺ using (_∷_)
 open import Data.Maybe using (Maybe; nothing; just)
 open import Data.Nat using (ℕ; zero; suc)
-open import Data.Product using () renaming (_,_ to _and_)
+open import Data.Product using (proj₂) renaming (_,_ to _and_)
 open import Function using (id)
 open import Level using (0ℓ)
 open import Size using (Size; ∞)
@@ -37,6 +37,7 @@ open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym; ≗→≅[])
 open import Construct.Choices
 open import Construct.GrulerArtifacts as GL using ()
 open import Construct.NestedChoice using (value; choice)
+open import Framework.Variants using (Variant-is-VL)
 
 open import Framework.Variants using (GrulerVariant)
 open import Construct.GrulerArtifacts using (leaf)
@@ -64,70 +65,42 @@ artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
-{-# TERMINATING #-}
-translateVariant : ∀ {F : 𝔽} {A : 𝔸} → Variant A → CCC F ∞ A
-translateVariant {F} {A} v = lemma (snoc Artifact∈ₛVariant v) refl
-  module translateVariant-Implementation where
-  lemma : (v' : Maybe (Artifact Variant A)) → snoc Artifact∈ₛVariant v ≡ v' → CCC F ∞ A
-  lemma nothing p = ⊥-elim (snoc≢nothing Artifact=Variant v p)
-  lemma (just (artifact-constructor a cs)) p = a -< List.map (λ c → translateVariant c) cs >-
+translate : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → LanguageCompiler (Variant-is-VL Variant) (CCCL F) → NADT F i A → CCC F ∞ A
+translate Variant→CCC (NADTAsset (leaf v)) = LanguageCompiler.compile Variant→CCC v
+translate Variant→CCC (NADT.NADTChoice (f Choice.⟨ alternatives ⟩)) = f CCC.⟨ List⁺.map (translate Variant→CCC) alternatives ⟩
 
-translate : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → NADT F i A → CCC F ∞ A
-translate (NADT.NADTAsset (leaf v)) = translateVariant v
-translate (NADT.NADTChoice (f Choice.⟨ alternatives ⟩)) = f CCC.⟨ List⁺.map translate alternatives ⟩
-
-{-# TERMINATING #-}
-preserves-≗ : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → (expr : NADT F i A) → CCC.⟦ translate expr ⟧ ≗ NADT.⟦ expr ⟧
-preserves-≗ {A = A} (NADT.NADTAsset (leaf v)) config =
-    CCC.⟦ translateVariant v ⟧ config
-  ≡⟨ lemma' v (snoc Artifact∈ₛVariant v) refl ⟩
+preserves-≗ : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → (Variant→CCC : LanguageCompiler (Variant-is-VL Variant) (CCCL F)) → (expr : NADT F i A) → CCC.⟦ translate Variant→CCC expr ⟧ ≗ NADT.⟦ expr ⟧
+preserves-≗ {A = A} Variant→CCC (NADTAsset (leaf v)) config =
+    CCC.⟦ translate Variant→CCC (NADTAsset (leaf v)) ⟧ config
+  ≡⟨⟩
+    CCC.⟦ LanguageCompiler.compile Variant→CCC v ⟧ config
+  ≡⟨ proj₂ (LanguageCompiler.preserves Variant→CCC v) config ⟩
     v
   ≡⟨⟩
-    NADT.⟦ Lang.NADT.NADTAsset (leaf v) ⟧ config
+    NADT.⟦ NADTAsset (leaf v) ⟧ config
   ∎
-  where
-  open translateVariant-Implementation
-  lemma' : (v : Variant A) → (v' : Maybe (Artifact Variant A)) → snoc Artifact∈ₛVariant v ≡ v' → CCC.⟦ translateVariant v ⟧ config ≡ v
-  lemma' v nothing p = ⊥-elim (snoc≢nothing Artifact=Variant v p)
-  lemma' v (just (artifact-constructor a cs)) p =
-      CCC.⟦ lemma v (snoc Artifact∈ₛVariant v) refl ⟧ config
-    ≡⟨ Eq.cong₂ CCC.⟦_⟧ (Eq.dcong₂ (lemma v) p refl) refl ⟩
-      CCC.⟦ lemma v (just (artifact-constructor a cs)) p ⟧ config
-    ≡⟨⟩
-      CCC.⟦ a -< List.map (λ c → translateVariant c) cs >- ⟧ config
-    ≡⟨⟩
-      artifact a (List.map (λ e → CCC.⟦ e ⟧ config) (List.map (λ c → translateVariant c) cs))
-    ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩
-      artifact a (List.map (λ c → CCC.⟦ translateVariant c ⟧ config) cs)
-    ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ c → lemma' c (snoc Artifact∈ₛVariant c) refl) cs) ⟩
-      artifact a (List.map (λ c → c) cs)
-    ≡⟨ Eq.cong₂ artifact refl (List.map-id cs) ⟩
-      artifact a cs
-    ≡⟨ snoc→cons Artifact=Variant v (artifact-constructor a cs) p ⟩
-      v
-    ∎
-preserves-≗ (Lang.NADT.NADTChoice (f Choice.⟨ alternatives ⟩)) config =
-    CCC.⟦ translate (Lang.NADT.NADTChoice (f Choice.⟨ alternatives ⟩)) ⟧ config
+preserves-≗ Variant→CCC (NADT.NADTChoice (f Choice.⟨ alternatives ⟩)) config =
+    CCC.⟦ translate Variant→CCC (Lang.NADT.NADTChoice (f Choice.⟨ alternatives ⟩)) ⟧ config
   ≡⟨⟩
-    CCC.⟦ f ⟨ List⁺.map translate alternatives ⟩ ⟧ config
+    CCC.⟦ f ⟨ List⁺.map (translate Variant→CCC) alternatives ⟩ ⟧ config
   ≡⟨⟩
-    CCC.⟦ List.find-or-last (config f) (List⁺.map translate alternatives) ⟧ config
-  ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (List.map-find-or-last translate (config f) alternatives) refl ⟩
-    CCC.⟦ translate (List.find-or-last (config f) alternatives) ⟧ config
-  ≡⟨ preserves-≗ (List.find-or-last (config f) alternatives) config ⟩
+    CCC.⟦ List.find-or-last (config f) (List⁺.map (translate Variant→CCC) alternatives) ⟧ config
+  ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (List.map-find-or-last (translate Variant→CCC) (config f) alternatives) refl ⟩
+    CCC.⟦ translate Variant→CCC (List.find-or-last (config f) alternatives) ⟧ config
+  ≡⟨ preserves-≗ Variant→CCC (List.find-or-last (config f) alternatives) config ⟩
     NADT.⟦ List.find-or-last (config f) alternatives ⟧ config
   ≡⟨⟩
     NADT.⟦ Lang.NADT.NADTChoice (f Choice.⟨ alternatives ⟩) ⟧ config
   ∎
 
-preserves : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → (expr : NADT F i A) → CCC.⟦ translate expr ⟧ ≅[ id ][ id ] NADT.⟦ expr ⟧
-preserves expr = ≗→≅[] (preserves-≗ expr)
+preserves : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → (Variant→CCC : LanguageCompiler (Variant-is-VL Variant) (CCCL F)) → (expr : NADT F i A) → CCC.⟦ translate Variant→CCC expr ⟧ ≅[ id ][ id ] NADT.⟦ expr ⟧
+preserves Variant→CCC expr = ≗→≅[] (preserves-≗ Variant→CCC expr)
 
-NADT→CCC : ∀ {i : Size} {F : 𝔽} → LanguageCompiler (NADTL F) (CCCL F)
-NADT→CCC .LanguageCompiler.compile = translate
-NADT→CCC .LanguageCompiler.config-compiler expr .to = id
-NADT→CCC .LanguageCompiler.config-compiler expr .from = id
-NADT→CCC .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr)
+NADT→CCC : ∀ {i : Size} {F : 𝔽} → LanguageCompiler (Variant-is-VL Variant) (CCCL F) → LanguageCompiler (NADTL F) (CCCL F)
+NADT→CCC Variant→CCC .LanguageCompiler.compile = translate Variant→CCC
+NADT→CCC Variant→CCC .LanguageCompiler.config-compiler expr .to = id
+NADT→CCC Variant→CCC .LanguageCompiler.config-compiler expr .from = id
+NADT→CCC Variant→CCC .LanguageCompiler.preserves expr = ≅[]-sym (preserves Variant→CCC expr)
 
-CCC≽NADT : ∀ {F : 𝔽} → CCCL F ≽ NADTL F
-CCC≽NADT = expressiveness-from-compiler NADT→CCC
+CCC≽NADT : ∀ {F : 𝔽} → LanguageCompiler (Variant-is-VL Variant) (CCCL F) → CCCL F ≽ NADTL F
+CCC≽NADT Variant→CCC = expressiveness-from-compiler (NADT→CCC Variant→CCC)