Refactoring the module structure of translations

src/Framework/Annotation/IndexedDimension.agda

@@ -0,0 +1,15 @@
+{-
+This module defines an annotation with equips another annotation with an index.
+The index is bounded (i.e., it is a Fin).
+IndexedDimension is used for conversions from NCC to NCC with lower arity (in particular 2).
+TODO: Abstract this to not have pred? How does it relate to IndexedName?
+-}
+module Framework.Annotation.IndexedDimension where
+
+open import Data.Fin using (Fin)
+open import Data.Product using (_×_)
+open import Util.Nat.AtLeast using (ℕ≥; toℕ; pred)
+open import Framework.Definitions using (𝔽)
+
+IndexedDimension : 𝔽 → ℕ≥ 2 → 𝔽
+IndexedDimension D n = D × Fin (toℕ (pred n))

src/Translation/Lang/2CC-to-NCC.agda

@@ -44,8 +44,7 @@ module 2CC where
   open 2CC-Sem-2 using (⟦_⟧) public
 open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩)
 
-import Translation.Lang.NCC-to-NCC
-open Translation.Lang.NCC-to-NCC.IncreaseArity Variant Artifact∈ₛVariant using (NCC→NCC)
+open import Translation.Lang.NCC.Grow Variant Artifact∈ₛVariant using (growFrom2Compiler)
 
 artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
@@ -158,7 +157,7 @@ module 2Ary where
 
 -- A generalization which translates to an arbitrary n instead of 2.
 2CC→NCC : ∀ {i : Size} {D : Set} → (n : ℕ≥ 2) → LanguageCompiler (2CCL D {i}) (NCCL n D {i})
-2CC→NCC n = 2Ary.2CC→NCC ⊕ NCC→NCC n
+2CC→NCC n = 2Ary.2CC→NCC ⊕ growFrom2Compiler n
 
 NCC≽2CC : ∀ {D : Set} → (n : ℕ≥ 2) → NCCL n D ≽ 2CCL D
 NCC≽2CC n = expressiveness-from-compiler (2CC→NCC n)

src/Translation/Lang/2CC-to-2CC.agda → src/Translation/Lang/2CC/Rename.agda

@@ -1,9 +1,13 @@
 {-# OPTIONS --sized-types #-}
 
+open import Framework.Definitions using (𝕍)
 open import Framework.Construct using (_∈ₛ_; cons)
 open import Construct.Artifact using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
-module Translation.Lang.2CC-to-2CC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+{-
+This module renames dimensions in binary choice calculus expressions.
+-}
+module Translation.Lang.2CC.Rename (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 open import Data.Bool using (if_then_else_)
 open import Data.Bool.Properties as Bool
@@ -30,50 +34,48 @@ module 2CC where
   open 2CC-Sem-2 using (⟦_⟧) public
 open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩)
 
-
 artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
-
 2CC-map-config : ∀ {D₁ D₂ : 𝔽}
   → (D₂ → D₁)
   → 2CC.Configuration D₁
   → 2CC.Configuration D₂
 2CC-map-config f config = config ∘ f
 
-map-dim : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸}
+rename : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸}
   → (D₁ → D₂)
   → 2CC D₁ i A
   → 2CC D₂ i A
-map-dim f (a -< cs >-) = a -< List.map (map-dim f) cs >-
-map-dim f (d ⟨ l , r ⟩) = f d ⟨ map-dim f l , map-dim f r ⟩
+rename f (a -< cs >-) = a -< List.map (rename f) cs >-
+rename f (d ⟨ l , r ⟩) = f d ⟨ rename f l , rename f r ⟩
 
 preserves-⊆ : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸}
   → (f : D₁ → D₂)
   → (f⁻¹ : D₂ → D₁)
   → (expr : 2CC D₁ i A)
-  → 2CC.⟦ map-dim f expr ⟧ ⊆[ 2CC-map-config f ] 2CC.⟦ expr ⟧
+  → 2CC.⟦ rename f expr ⟧ ⊆[ 2CC-map-config f ] 2CC.⟦ expr ⟧
 preserves-⊆ f f⁻¹ (a -< cs >-) config =
-    2CC.⟦ map-dim f (a -< cs >-) ⟧ config
+    2CC.⟦ rename f (a -< cs >-) ⟧ config
   ≡⟨⟩
-    2CC.⟦ a -< List.map (map-dim f) cs >- ⟧ config
+    2CC.⟦ a -< List.map (rename f) cs >- ⟧ config
   ≡⟨⟩
-    artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) (List.map (map-dim f) cs))
+    artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) (List.map (rename f) cs))
   ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩
-    artifact a (List.map (λ e → 2CC.⟦ map-dim f e ⟧ config) cs)
+    artifact a (List.map (λ e → 2CC.⟦ rename f e ⟧ config) cs)
   ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ f f⁻¹ e config) cs) ⟩
     artifact a (List.map (λ e → 2CC.⟦ e ⟧ (config ∘ f)) cs)
   ≡⟨⟩
     2CC.⟦ a -< cs >- ⟧ (config ∘ f)
   ∎
 preserves-⊆ f f⁻¹ (d ⟨ l , r ⟩) config =
-    2CC.⟦ map-dim f (d ⟨ l , r ⟩) ⟧ config
+    2CC.⟦ rename f (d ⟨ l , r ⟩) ⟧ config
   ≡⟨⟩
-    2CC.⟦ f d ⟨ map-dim f l , map-dim f r ⟩ ⟧ config
+    2CC.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ config
   ≡⟨⟩
-    2CC.⟦ if config (f d) then map-dim f l else map-dim f r ⟧ config
-  ≡˘⟨ Eq.cong₂ 2CC.⟦_⟧ (Bool.push-function-into-if (map-dim f) (config (f d))) refl ⟩
-    2CC.⟦ map-dim f (if config (f d) then l else r) ⟧ config
+    2CC.⟦ if config (f d) then rename f l else rename f r ⟧ config
+  ≡˘⟨ Eq.cong₂ 2CC.⟦_⟧ (Bool.push-function-into-if (rename f) (config (f d))) refl ⟩
+    2CC.⟦ rename f (if config (f d) then l else r) ⟧ config
   ≡⟨ preserves-⊆ f f⁻¹ (if config (f d) then l else r) config ⟩
     2CC.⟦ if config (f d) then l else r ⟧ (config ∘ f)
   ≡⟨⟩
@@ -87,19 +89,19 @@ preserves-⊇ : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸}
   → (f⁻¹ : D₂ → D₁)
   → f⁻¹ ∘ f ≗ id
   → (expr : 2CC D₁ i A)
-  → 2CC.⟦ expr ⟧ ⊆[ 2CC-map-config f⁻¹ ] 2CC.⟦ map-dim f expr ⟧
+  → 2CC.⟦ expr ⟧ ⊆[ 2CC-map-config f⁻¹ ] 2CC.⟦ rename f expr ⟧
 preserves-⊇ f f⁻¹ is-inverse (a -< cs >-) config =
     2CC.⟦ a -< cs >- ⟧ config
   ≡⟨⟩
     artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) cs)
   ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊇ f f⁻¹ is-inverse e config) cs) ⟩
-    artifact a (List.map (λ e → 2CC.⟦ map-dim f e ⟧ (config ∘ f⁻¹)) cs)
+    artifact a (List.map (λ e → 2CC.⟦ rename f e ⟧ (config ∘ f⁻¹)) cs)
   ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩
-    artifact a (List.map (λ e → 2CC.⟦ e ⟧ (config ∘ f⁻¹)) (List.map (map-dim f) cs))
+    artifact a (List.map (λ e → 2CC.⟦ e ⟧ (config ∘ f⁻¹)) (List.map (rename f) cs))
   ≡⟨⟩
-    2CC.⟦ a -< List.map (map-dim f) cs >- ⟧ (config ∘ f⁻¹)
+    2CC.⟦ a -< List.map (rename f) cs >- ⟧ (config ∘ f⁻¹)
   ≡⟨⟩
-    2CC.⟦ map-dim f (a -< cs >-) ⟧ (config ∘ f⁻¹)
+    2CC.⟦ rename f (a -< cs >-) ⟧ (config ∘ f⁻¹)
   ∎
 preserves-⊇ f f⁻¹ is-inverse (d ⟨ l , r ⟩) config =
     2CC.⟦ d ⟨ l , r ⟩ ⟧ config
@@ -108,31 +110,31 @@ preserves-⊇ f f⁻¹ is-inverse (d ⟨ l , r ⟩) config =
   ≡⟨⟩
     2CC.⟦ if config d then l else r ⟧ config
   ≡⟨ preserves-⊇ f f⁻¹ is-inverse (if config d then l else r) config ⟩
-    2CC.⟦ map-dim f (if config d then l else r) ⟧ (config ∘ f⁻¹)
-  ≡⟨ Eq.cong₂ 2CC.⟦_⟧ (push-function-into-if (map-dim f) (config d)) refl ⟩
-    2CC.⟦ if config d then map-dim f l else map-dim f r ⟧ (config ∘ f⁻¹)
-  ≡˘⟨ Eq.cong₂ 2CC.⟦_⟧ (Eq.cong-app (Eq.cong-app (Eq.cong if_then_else_ (Eq.cong config (is-inverse d))) (map-dim f l)) (map-dim f r)) refl ⟩
-    2CC.⟦ if config (f⁻¹ (f d)) then map-dim f l else map-dim f r ⟧ (config ∘ f⁻¹)
+    2CC.⟦ rename f (if config d then l else r) ⟧ (config ∘ f⁻¹)
+  ≡⟨ Eq.cong₂ 2CC.⟦_⟧ (push-function-into-if (rename f) (config d)) refl ⟩
+    2CC.⟦ if config d then rename f l else rename f r ⟧ (config ∘ f⁻¹)
+  ≡˘⟨ Eq.cong₂ 2CC.⟦_⟧ (Eq.cong-app (Eq.cong-app (Eq.cong if_then_else_ (Eq.cong config (is-inverse d))) (rename f l)) (rename f r)) refl ⟩
+    2CC.⟦ if config (f⁻¹ (f d)) then rename f l else rename f r ⟧ (config ∘ f⁻¹)
   ≡⟨⟩
-    2CC.⟦ f d ⟨ map-dim f l , map-dim f r ⟩ ⟧ (config ∘ f⁻¹)
+    2CC.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ (config ∘ f⁻¹)
   ≡⟨⟩
-    2CC.⟦ map-dim f (d ⟨ l , r ⟩) ⟧ (config ∘ f⁻¹)
+    2CC.⟦ rename f (d ⟨ l , r ⟩) ⟧ (config ∘ f⁻¹)
   ∎
 
 preserves : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸}
   → (f : D₁ → D₂)
   → (f⁻¹ : D₂ → D₁)
   → f⁻¹ ∘ f ≗ id
   → (e : 2CC D₁ i A)
-  → 2CC.⟦ map-dim f e ⟧ ≅[ 2CC-map-config f ][ 2CC-map-config f⁻¹ ] 2CC.⟦ e ⟧
+  → 2CC.⟦ rename f e ⟧ ≅[ 2CC-map-config f ][ 2CC-map-config f⁻¹ ] 2CC.⟦ e ⟧
 preserves f f⁻¹ is-inverse expr = preserves-⊆ f f⁻¹ expr and preserves-⊇ f f⁻¹ is-inverse expr
 
-2CC-map-dim : ∀ {i : Size} {D₁ D₂ : 𝔽}
+2CC-rename : ∀ {i : Size} {D₁ D₂ : 𝔽}
   → (f : D₁ → D₂)
   → (f⁻¹ : D₂ → D₁)
   → f⁻¹ ∘ f ≗ id
   → LanguageCompiler (2CCL D₁ {i}) (2CCL D₂ {i})
-2CC-map-dim f f⁻¹ is-inverse .LanguageCompiler.compile = map-dim f
-2CC-map-dim f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .to = 2CC-map-config f⁻¹
-2CC-map-dim f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .from = 2CC-map-config f
-2CC-map-dim f f⁻¹ is-inverse .LanguageCompiler.preserves expr = ≅[]-sym (preserves f f⁻¹ is-inverse expr)
+2CC-rename f f⁻¹ is-inverse .LanguageCompiler.compile = rename f
+2CC-rename f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .to = 2CC-map-config f⁻¹
+2CC-rename f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .from = 2CC-map-config f
+2CC-rename f f⁻¹ is-inverse .LanguageCompiler.preserves expr = ≅[]-sym (preserves f f⁻¹ is-inverse expr)

src/Translation/Lang/CCC-to-NCC.agda

@@ -47,18 +47,15 @@ module NCC where
   open NCC-Sem-2 using (⟦_⟧) public
 open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩)
 
-
-import Translation.Lang.NCC-to-NCC
-open Translation.Lang.NCC-to-NCC Variant Artifact∈ₛVariant using (NCC→NCC)
-open Translation.Lang.NCC-to-NCC.map-dim Variant Artifact∈ₛVariant using (NCC-map-dim; NCC-map-config)
-module NCC-map-dim {i} {D₁} {D₂} n f f⁻¹ is-inverse = LanguageCompiler (NCC-map-dim {i} {D₁} {D₂} n f f⁻¹ is-inverse)
-open Translation.Lang.NCC-to-NCC Variant Artifact∈ₛVariant using (IndexedDimension)
+open import Framework.Annotation.IndexedDimension
+open import Translation.Lang.NCC.NCC-to-NCC Variant Artifact∈ₛVariant using (NCC→NCC)
+open import Translation.Lang.NCC.Rename Variant Artifact∈ₛVariant using (NCC-rename; NCC-map-config)
+module NCC-rename {i} {D₁} {D₂} n f f⁻¹ is-inverse = LanguageCompiler (NCC-rename {i} {D₁} {D₂} n f f⁻¹ is-inverse)
 module NCC→NCC {i} {D} n m = LanguageCompiler (NCC→NCC {i} {D} n m)
 
 artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
-
 module Exact where
   -- Idea of this translation:
   -- We want to extend the list of alternatives in each choice of a `CCC` expression to such that they all have the same length.
@@ -78,8 +75,8 @@ module Exact where
   -- We want to translate into `NCC` which has an arity of at leat 2 so we
   -- ensure that the result is ≥ 2
   ⌈_⌉ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → CCC D i A → ℕ≥ 2
-  ⌈ a -< cs >- ⌉ = maximum (List.map ⌈_⌉ cs)
-  ⌈ d ⟨ c ∷ [] ⟩ ⌉ = ⌈_⌉ c
+  ⌈ a -< cs >-         ⌉ = maximum (List.map ⌈_⌉ cs)
+  ⌈ d ⟨ c ∷ [] ⟩       ⌉ = ⌈ c ⌉
   ⌈ d ⟨ c₁ ∷ c₂ ∷ cs ⟩ ⌉ = sucs (List.length cs) ⊔ maximum⁺ (List⁺.map ⌈_⌉ (c₁ ∷ c₂ ∷ cs))
 
   mutual
@@ -346,7 +343,7 @@ translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
   → CCC D i A
   → NCC n (D × ℕ) ∞ A
 translate (sucs n) expr =
-  NCC-map-dim.compile (sucs n) (Fin→ℕ ⌈ expr ⌉) (Fin→ℕ⁻¹ ⌈ expr ⌉) (Fin→ℕ⁻¹-Fin→ℕ ⌈ expr ⌉)
+  NCC-rename.compile (sucs n) (Fin→ℕ ⌈ expr ⌉) (Fin→ℕ⁻¹ ⌈ expr ⌉) (Fin→ℕ⁻¹-Fin→ℕ ⌈ expr ⌉)
     (NCC→NCC.compile ⌈ expr ⌉ (sucs n)
       (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr)))
 
@@ -377,8 +374,8 @@ preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
 preserves (sucs n) expr =
   NCC.⟦ translate (sucs n) expr ⟧
   ≅[]⟨⟩
-    NCC.⟦ NCC-map-dim.compile (sucs n) (Fin→ℕ ⌈ expr ⌉) (Fin→ℕ⁻¹ ⌈ expr ⌉) (Fin→ℕ⁻¹-Fin→ℕ ⌈ expr ⌉) (NCC→NCC.compile ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟧
-  ≅[]˘⟨ NCC-map-dim.preserves (sucs n) (Fin→ℕ ⌈ expr ⌉) (Fin→ℕ⁻¹ ⌈ expr ⌉) (Fin→ℕ⁻¹-Fin→ℕ ⌈ expr ⌉) (NCC→NCC.compile ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟩
+    NCC.⟦ NCC-rename.compile (sucs n) (Fin→ℕ ⌈ expr ⌉) (Fin→ℕ⁻¹ ⌈ expr ⌉) (Fin→ℕ⁻¹-Fin→ℕ ⌈ expr ⌉) (NCC→NCC.compile ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟧
+  ≅[]˘⟨ NCC-rename.preserves (sucs n) (Fin→ℕ ⌈ expr ⌉) (Fin→ℕ⁻¹ ⌈ expr ⌉) (Fin→ℕ⁻¹-Fin→ℕ ⌈ expr ⌉) (NCC→NCC.compile ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟩
     NCC.⟦ NCC→NCC.compile ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr)) ⟧
   ≅[]˘⟨ (NCC→NCC.preserves ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟩
     NCC.⟦ Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr) ⟧

src/Translation/Lang/NCC-to-2CC.agda

@@ -38,9 +38,8 @@ open NCC-Sem-1 using (NCCL)
 module NCC-Sem-2 {n} {D} = NCC.Sem n D Variant Artifact∈ₛVariant
 open NCC-Sem-2 using () renaming (⟦_⟧ to ⟦_⟧ₙ)
 
-open import Translation.Lang.NCC-to-NCC Variant Artifact∈ₛVariant using (NCC→NCC)
-open import Translation.Lang.NCC-to-NCC Variant Artifact∈ₛVariant using (IndexedDimension) public
-
+open import Framework.Annotation.IndexedDimension
+open import Translation.Lang.NCC.NCC-to-NCC Variant Artifact∈ₛVariant using (NCC→NCC)
 artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)