diff --git a/README.md b/README.md index 37f3726f..9311ecae 100644 --- a/README.md +++ b/README.md @@ -63,7 +63,7 @@ The library is organized as follows: Definitions for expressiveness and other relations are in the [Relation](src/Framework/Relation) sub-directory. Theorems for proving completeness, soundness, and expressiveness based on their relationships (Section 4.5) are within the [Proof](src/Framework/Proof) sub-directory. - [src/Lang](src/Lang) contains instantiations of particular variability languages. -- [src/Translation](src/Translation) contains translations between variability languages, such as the translation of option calculus to binary choice calculus in [OC-to-BCC.lagda.md](src/Translation/OC-to-BCC.lagda.md) (Section 5.3 in our paper). +- [src/Translation](src/Translation) contains translations between variability languages, such as the translation of option calculus to binary choice calculus in [OC-to-2CC.lagda.md](src/Translation/OC-to-2CC.lagda.md) (Section 5.3 in our paper). - [src/Test](src/Test) contains definitions of unit tests for translations and some experiments that are run, when running the library. [agda-badge-version-svg]: https://img.shields.io/badge/agda-v2.6.3-blue.svg diff --git a/src/Construct/Artifact.agda b/src/Construct/Artifact.agda index 3d6d0c44..88c46701 100644 --- a/src/Construct/Artifact.agda +++ b/src/Construct/Artifact.agda @@ -21,51 +21,3 @@ Syntax E A = Artifact A (E A) Construct : PlainConstruct Construct = Plain-⟪ Syntax , (λ Γ e c → map-children (flip (Semantics Γ) c) e) ⟫ - -open import Data.EqIndexedSet as ISet -map-children-preserves : ∀ {V : 𝕍} {Γ₁ Γ₂ : VariabilityLanguage V} {A} - → (mkArtifact : Syntax ∈ₛ V) - → (t : LanguageCompiler Γ₁ Γ₂) - → (a : Syntax (Expression Γ₁) A) - → PlainConstruct-Semantics Construct mkArtifact Γ₁ a - ≅[ conf t ][ fnoc t ] - PlainConstruct-Semantics Construct mkArtifact Γ₂ (map-children (compile t) a) -map-children-preserves {V} {Γ₁} {Γ₂} {A} mkArtifact t (a -< cs >-) = - ≅[]-begin - (λ c → cons mkArtifact (a -< map (λ e → ⟦ e ⟧₁ c) cs >-)) - ≅[]⟨ t-⊆ , t-⊇ ⟩ - (λ c → cons mkArtifact (a -< map (λ e → ⟦ e ⟧₂ c) (map (compile t) cs) >-)) - ≅[]-∎ - where - -- module I = IVSet V A - -- open I using (_≅[_][_]_; _⊆[_]_) - open ISet.≅[]-Reasoning - open Eq.≡-Reasoning - - ⟦_⟧₁ = Semantics Γ₁ - ⟦_⟧₂ = Semantics Γ₂ - - -- TODO: The following two proofs contain quite some redundancy that can probably be abstracted. - t-⊆ : (λ c → cons mkArtifact (a -< map (λ e → ⟦ e ⟧₁ c) cs >-)) - ⊆[ conf t ] - (λ z → cons mkArtifact (a -< map (λ e → ⟦ e ⟧₂ z) (map (compile t) cs) >-)) - t-⊆ i = Eq.cong (cons mkArtifact) $ Eq.cong (a -<_>-) $ - begin - map (λ e → ⟦ e ⟧₁ i) cs - ≡⟨ map-cong (λ e → proj₁ (preserves t e) i) cs ⟩ - map (λ e → ⟦ compile t e ⟧₂ (conf t i)) cs - ≡⟨ map-∘ cs ⟩ - map (λ e → ⟦ e ⟧₂ (conf t i)) (map (compile t) cs) - ∎ - - t-⊇ : (λ z → cons mkArtifact (a -< map (λ e → ⟦ e ⟧₂ z) (map (compile t) cs) >-)) - ⊆[ fnoc t ] - (λ c → cons mkArtifact (a -< map (λ e → ⟦ e ⟧₁ c) cs >-)) - t-⊇ i = Eq.cong (cons mkArtifact) $ Eq.cong (a -<_>-) $ - begin - map (λ e → ⟦ e ⟧₂ i) (map (compile t) cs) - ≡˘⟨ map-∘ cs ⟩ - map (λ e → ⟦ compile t e ⟧₂ i) cs - ≡⟨ map-cong (λ e → proj₂ (preserves t e) i) cs ⟩ - map (λ e → ⟦ e ⟧₁ (fnoc t i)) cs - ∎ diff --git a/src/Construct/Choices.agda b/src/Construct/Choices.agda index 1055d131..a9535280 100644 --- a/src/Construct/Choices.agda +++ b/src/Construct/Choices.agda @@ -13,58 +13,58 @@ open import Data.EqIndexedSet as ISet open import Util.AuxProofs using (if-cong) -module Choice-Fix where +module NChoice where open import Data.Fin using (Fin) - open import Data.Nat using (ℕ) + open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥) open import Data.Vec using (Vec; lookup; toList) renaming (map to map-vec) open import Data.Vec.Properties using (lookup-map) - record Syntax (n : ℕ) (Q : Set) (A : Set) : Set where + record Syntax (n : ℕ≥ 2) (Q : Set) (A : Set) : Set where constructor _⟨_⟩ field dim : Q - alternatives : Vec A n + alternatives : Vec A (ℕ≥.toℕ n) - Config : ℕ → Set → Set - Config n Q = Q → Fin n + Config : ℕ≥ 2 → Set → Set + Config n Q = Q → Fin (ℕ≥.toℕ n) -- choice-elimination - Standard-Semantics : ∀ {n : ℕ} {A : Set} {Q : Set} → Syntax n Q A → Config n Q → A - Standard-Semantics (D ⟨ alternatives ⟩) c = lookup alternatives (c D) + ⟦_⟧ : ∀ {n : ℕ≥ 2} {A : Set} {Q : Set} → Syntax n Q A → Config n Q → A + ⟦_⟧ (D ⟨ alternatives ⟩) c = lookup alternatives (c D) - map : ∀ {n : ℕ} {Q : Set} {A : Set} {B : Set} + map : ∀ {n : ℕ≥ 2} {Q : Set} {A : Set} {B : Set} → (A → B) → Syntax n Q A → Syntax n Q B map f (D ⟨ alternatives ⟩) = D ⟨ map-vec f alternatives ⟩ -- -- rename - map-dim : ∀ {n : ℕ} {Q : Set} {R : Set} {A : Set} + map-dim : ∀ {n : ℕ≥ 2} {Q : Set} {R : Set} {A : Set} → (Q → R) → Syntax n Q A → Syntax n R A map-dim f (D ⟨ es ⟩) = (f D) ⟨ es ⟩ - map-preserves : ∀ {n : ℕ} {Q : Set} {A : Set} {B : Set} + map-preserves : ∀ {n : ℕ≥ 2} {Q : Set} {A : Set} {B : Set} → (f : A → B) → (chc : Syntax n Q A) → (c : Config n Q) - → Standard-Semantics (map f chc) c ≡ f (Standard-Semantics chc c) - map-preserves f (D ⟨ es ⟩) c = + → ⟦ map f chc ⟧ c ≡ f (⟦ chc ⟧ c) + map-preserves {n} f (D ⟨ es ⟩) c = begin - Standard-Semantics (map f (D ⟨ es ⟩)) c + ⟦ map {n} f (D ⟨ es ⟩) ⟧ c ≡⟨⟩ lookup (map-vec f es) (c D) ≡⟨ lookup-map (c D) f es ⟩ f (lookup es (c D)) ≡⟨⟩ - f (Standard-Semantics (D ⟨ es ⟩) c) + f (⟦_⟧ {n} (D ⟨ es ⟩) c) -- TODO implicit argument ∎ - show : ∀ {n : ℕ} {Q : Set} {A : Set} → (Q → String) → (A → String) → Syntax n Q A → String + show : ∀ {n : ℕ≥ 2} {Q : Set} {A : Set} → (Q → String) → (A → String) → Syntax n Q A → String show show-q show-a (D ⟨ es ⟩) = show-q D <+> "⟨" <+> (intersperse " , " (toList (map-vec show-a es))) <+> "⟩" -module Choice₂ where +module 2Choice where record Syntax (Q : Set) (A : Set) : Set where constructor _⟨_,_⟩ field @@ -76,8 +76,8 @@ module Choice₂ where Config Q = Q → Bool -- choice-elimination - Standard-Semantics : ∀ {A : Set} {Q : Set} → Syntax Q A → Config Q → A - Standard-Semantics (D ⟨ l , r ⟩) c = if c D then l else r + ⟦_⟧ : ∀ {A : Set} {Q : Set} → Syntax Q A → Config Q → A + ⟦_⟧ (D ⟨ l , r ⟩) c = if c D then l else r map : ∀ {Q : Set} {A : Set} {B : Set} → (A → B) @@ -96,16 +96,16 @@ module Choice₂ where → (f : A → B) → (chc : Syntax Q A) → (c : Config Q) - → Standard-Semantics (map f chc) c ≡ f (Standard-Semantics chc c) + → ⟦ map f chc ⟧ c ≡ f (⟦ chc ⟧ c) map-preserves f (D ⟨ l , r ⟩) c = begin - Standard-Semantics (map f (D ⟨ l , r ⟩)) c + ⟦ map f (D ⟨ l , r ⟩) ⟧ c ≡⟨⟩ (if c D then f l else f r) ≡⟨ if-cong (c D) f ⟩ f (if c D then l else r) ≡⟨⟩ - f (Standard-Semantics (D ⟨ l , r ⟩) c) + f (⟦ D ⟨ l , r ⟩ ⟧ c) ∎ show : ∀ {Q : Set} {A : Set} → (Q → String) → (A → String) → Syntax Q A → String @@ -115,7 +115,7 @@ open import Data.Nat using (ℕ) open import Data.List.NonEmpty using (List⁺; toList) renaming (map to map-list⁺) open import Util.List using (find-or-last; map-find-or-last) -module Choiceₙ where +module Choice where record Syntax (Q : Set) (A : Set) : Set where constructor _⟨_⟩ field @@ -126,8 +126,8 @@ module Choiceₙ where Config Q = Q → ℕ -- choice-elimination - Standard-Semantics : ∀ {Q : Set} {A : Set} → Syntax Q A → Config Q → A - Standard-Semantics (D ⟨ alternatives ⟩) c = find-or-last (c D) alternatives + ⟦_⟧ : ∀ {Q : Set} {A : Set} → Syntax Q A → Config Q → A + ⟦_⟧ (D ⟨ alternatives ⟩) c = find-or-last (c D) alternatives map : ∀ {Q : Set} {A : Set} {B : Set} → (A → B) @@ -146,16 +146,16 @@ module Choiceₙ where → (f : A → B) → (chc : Syntax Q A) → (c : Config Q) -- todo: use ≐ here? - → Standard-Semantics (map f chc) c ≡ f (Standard-Semantics chc c) + → ⟦ map f chc ⟧ c ≡ f (⟦ chc ⟧ c) map-preserves f (D ⟨ as ⟩) c = begin - Standard-Semantics (map f (D ⟨ as ⟩)) c + ⟦ map f (D ⟨ as ⟩) ⟧ c ≡⟨⟩ find-or-last (c D) (map-list⁺ f as) ≡˘⟨ map-find-or-last f (c D) as ⟩ f (find-or-last (c D) as) ≡⟨⟩ - f (Standard-Semantics (D ⟨ as ⟩) c) + f (⟦ D ⟨ as ⟩ ⟧ c) ∎ show : ∀ {Q : Set} {A : Set} → (Q → String) → (A → String) → Syntax Q A → String @@ -169,166 +169,42 @@ open import Framework.Construct open import Data.Product using (_,_; proj₁; proj₂) open import Function using (id) -module VLChoice₂ where - open Choice₂ using (_⟨_,_⟩; Config; Standard-Semantics; map; map-preserves) - open Choice₂.Syntax using (dim) +module VLNChoice where + open import Util.Nat.AtLeast using (ℕ≥) + open NChoice using (Config; map; map-preserves) + open NChoice.Syntax using (dim) - open import Framework.Compiler as Comp using (LanguageCompiler; ConstructFunctor) - open LanguageCompiler + Syntax : ℕ≥ 2 → 𝔽 → ℂ + Syntax n F E A = NChoice.Syntax n F (E A) + + Semantics : ∀ (n : ℕ≥ 2) (V : 𝕍) (F : 𝔽) → VariationalConstruct-Semantics V (Config n F) (Syntax n F) + Semantics _ _ _ (⟪ _ , _ , ⟦_⟧ ⟫) extract chc c = ⟦ NChoice.⟦ chc ⟧ (extract c) ⟧ c + + Construct : ∀ n (V : 𝕍) (F : 𝔽) → VariabilityConstruct V + Construct n V F = Variational-⟪ Syntax n F , Config n F , Semantics n V F ⟫ + +module VL2Choice where + open 2Choice using (_⟨_,_⟩; Config; map; map-preserves) + open 2Choice.Syntax using (dim) Syntax : 𝔽 → ℂ - Syntax F E A = Choice₂.Syntax F (E A) + Syntax F E A = 2Choice.Syntax F (E A) Semantics : ∀ (V : 𝕍) (F : 𝔽) → VariationalConstruct-Semantics V (Config F) (Syntax F) - Semantics _ _ (⟪ _ , _ , ⟦_⟧ ⟫) extract chc c = ⟦ Standard-Semantics chc (extract c) ⟧ c + Semantics _ _ (⟪ _ , _ , ⟦_⟧ ⟫) extract chc c = ⟦ 2Choice.⟦ chc ⟧ (extract c) ⟧ c Construct : ∀ (V : 𝕍) (F : 𝔽) → VariabilityConstruct V Construct V F = Variational-⟪ Syntax F , Config F , Semantics V F ⟫ - map-compile-preserves : ∀ {F V A} - → (Γ₁ Γ₂ : VariabilityLanguage V) - → (extract : Compatible (Construct V F) Γ₁) - → (t : LanguageCompiler Γ₁ Γ₂) - → (chc : Syntax F (Expression Γ₁) A) - → to-is-Embedding (config-compiler t) - → Semantics V F Γ₁ extract chc - ≅[ conf t ][ fnoc t ] - Semantics V F Γ₂ (extract ∘ fnoc t) (map (compile t) chc) - map-compile-preserves {F} {V} {A} Γ₁ Γ₂ extract t chc stable = - ≅[]-begin - Semantics V F Γ₁ extract chc - ≅[]⟨⟩ - (λ c → ⟦ Standard-Semantics chc (extract c) ⟧₁ c) - -- First compiler proof composition: - -- We apply the hypotheses that t preserves semantics and that its configuration compiler is stable. - ≅[]⟨ t-⊆ , t-⊇ ⟩ - (λ c → ⟦ compile t (Standard-Semantics chc (extract (fnoc t c))) ⟧₂ c) - -- Second compiler proof composition: - -- We can just apply map-preserves directly. - -- We need a cong to apply the proof to the first compiler phase instead of the second. - ≐˘[ c ]⟨ Eq.cong (λ x → ⟦ x ⟧₂ c) (map-preserves (compile t) chc (extract (fnoc t c))) ⟩ - (λ c → ⟦ Standard-Semantics (map (compile t) chc) (extract (fnoc t c)) ⟧₂ c) - ≅[]⟨⟩ - Semantics V F Γ₂ (extract ∘ fnoc t) (map (compile t) chc) - ≅[]-∎ - where open ISet.≅[]-Reasoning - - ⟦_⟧₁ = VL.Semantics Γ₁ - ⟦_⟧₂ = VL.Semantics Γ₂ - - t-⊆ : (λ c → ⟦ Standard-Semantics chc (extract c) ⟧₁ c) - ⊆[ conf t ] - (λ f → ⟦ compile t (Standard-Semantics chc (extract (fnoc t f))) ⟧₂ f) - t-⊆ i = - begin - ⟦ Standard-Semantics chc (extract i) ⟧₁ i - ≡⟨ proj₁ (preserves t (Standard-Semantics chc (extract i))) i ⟩ - ⟦ compile t (Standard-Semantics chc (extract i)) ⟧₂ (conf t i) - ≡˘⟨ Eq.cong (λ eq → ⟦ compile t (Standard-Semantics chc (extract eq)) ⟧₂ (conf t i)) (stable i) ⟩ - ⟦ compile t (Standard-Semantics chc (extract (fnoc t (conf t i)))) ⟧₂ (conf t i) - ≡⟨⟩ - (λ f → ⟦ compile t (Standard-Semantics chc (extract (fnoc t f))) ⟧₂ f) (conf t i) - ∎ - - t-⊇ : (λ f → ⟦ compile t (Standard-Semantics chc (extract (fnoc t f))) ⟧₂ f) - ⊆[ fnoc t ] - (λ c → ⟦ Standard-Semantics chc (extract c) ⟧₁ c) - t-⊇ i = - begin - ⟦ compile t (Standard-Semantics chc (extract (fnoc t i))) ⟧₂ i - ≡⟨ proj₂ (preserves t (Standard-Semantics chc (extract (fnoc t i)))) i ⟩ - ⟦ Standard-Semantics chc (extract (fnoc t i)) ⟧₁ (fnoc t i) - ≡⟨⟩ - (λ c → ⟦ Standard-Semantics chc (extract c) ⟧₁ c) (fnoc t i) - ∎ - - cong-compiler : ∀ V F → ConstructFunctor (Construct V F) - cong-compiler _ _ = record - { map = map - ; preserves = map-compile-preserves - } - -module VLChoiceₙ where - open Choiceₙ using (_⟨_⟩; Config; Standard-Semantics; map; map-preserves) - open Choiceₙ.Syntax using (dim) - - open import Framework.Compiler as Comp using (LanguageCompiler; ConstructFunctor) - open LanguageCompiler +module VLChoice where + open Choice using (_⟨_⟩; Config; map; map-preserves) + open Choice.Syntax using (dim) Syntax : 𝔽 → ℂ - Syntax F E A = Choiceₙ.Syntax F (E A) + Syntax F E A = Choice.Syntax F (E A) Semantics : ∀ (V : 𝕍) (F : 𝔽) → VariationalConstruct-Semantics V (Config F) (Syntax F) - Semantics _ _ (⟪ _ , _ , ⟦_⟧ ⟫) extract choice c = ⟦ Choiceₙ.Standard-Semantics choice (extract c) ⟧ c + Semantics _ _ (⟪ _ , _ , ⟦_⟧ ⟫) extract choice c = ⟦ Choice.⟦ choice ⟧ (extract c) ⟧ c Construct : ∀ (V : 𝕍) (F : 𝔽) → VariabilityConstruct V Construct V F = Variational-⟪ Syntax F , Config F , Semantics V F ⟫ - - -- Interestingly, this proof is entirely copy and paste from VLChoice₂.map-compile-preserves. - -- Only minor adjustments to adapt the theorem had to be made. - -- Is there something useful to extract to a common definition here? - -- This proof is oblivious of at least - -- - the implementation of map, we only need the preservation theorem - -- - the Standard-Semantics, we only need the preservation theorem of t, and that the config-compiler is stable. - map-compile-preserves : ∀ {F V A} - → (Γ₁ Γ₂ : VariabilityLanguage V) - → (extract : Compatible (Construct V F) Γ₁) - → (t : LanguageCompiler Γ₁ Γ₂) - → (chc : Syntax F (Expression Γ₁) A) - → to-is-Embedding (config-compiler t) - → Semantics V F Γ₁ extract chc - ≅[ conf t ][ fnoc t ] - Semantics V F Γ₂ (extract ∘ fnoc t) (map (compile t) chc) - map-compile-preserves {F} {V} {A} Γ₁ Γ₂ extract t chc stable = - ≅[]-begin - Semantics V F Γ₁ extract chc - ≅[]⟨⟩ - (λ c → ⟦ Standard-Semantics chc (extract c) ⟧₁ c) - -- First compiler proof composition: - -- We apply the hypotheses that t preserves semantics and that its configuration compiler is stable. - ≅[]⟨ t-⊆ , t-⊇ ⟩ - (λ c → ⟦ compile t (Standard-Semantics chc (extract (fnoc t c))) ⟧₂ c) - -- Second compiler proof composition: - -- We can just apply map-preserves directly. - -- We need a cong to apply the proof to the first compiler phase instead of the second. - ≐˘[ c ]⟨ Eq.cong (λ x → ⟦ x ⟧₂ c) (map-preserves (compile t) chc (extract (fnoc t c))) ⟩ - (λ c → ⟦ Standard-Semantics (map (compile t) chc) (extract (fnoc t c)) ⟧₂ c) - ≅[]⟨⟩ - Semantics V F Γ₂ (extract ∘ fnoc t) (map (compile t) chc) - ≅[]-∎ - where open ISet.≅[]-Reasoning - - ⟦_⟧₁ = VL.Semantics Γ₁ - ⟦_⟧₂ = VL.Semantics Γ₂ - - t-⊆ : (λ c → ⟦ Standard-Semantics chc (extract c) ⟧₁ c) - ⊆[ conf t ] - (λ f → ⟦ compile t (Standard-Semantics chc (extract (fnoc t f))) ⟧₂ f) - t-⊆ i = - begin - ⟦ Standard-Semantics chc (extract i) ⟧₁ i - ≡⟨ proj₁ (preserves t (Standard-Semantics chc (extract i))) i ⟩ - ⟦ compile t (Standard-Semantics chc (extract i)) ⟧₂ (conf t i) - ≡˘⟨ Eq.cong (λ eq → ⟦ compile t (Standard-Semantics chc (extract eq)) ⟧₂ (conf t i)) (stable i) ⟩ - ⟦ compile t (Standard-Semantics chc (extract (fnoc t (conf t i)))) ⟧₂ (conf t i) - ≡⟨⟩ - (λ f → ⟦ compile t (Standard-Semantics chc (extract (fnoc t f))) ⟧₂ f) (conf t i) - ∎ - - t-⊇ : (λ f → ⟦ compile t (Standard-Semantics chc (extract (fnoc t f))) ⟧₂ f) - ⊆[ fnoc t ] - (λ c → ⟦ Standard-Semantics chc (extract c) ⟧₁ c) - t-⊇ i = - begin - ⟦ compile t (Standard-Semantics chc (extract (fnoc t i))) ⟧₂ i - ≡⟨ proj₂ (preserves t (Standard-Semantics chc (extract (fnoc t i)))) i ⟩ - ⟦ Standard-Semantics chc (extract (fnoc t i)) ⟧₁ (fnoc t i) - ≡⟨⟩ - (λ c → ⟦ Standard-Semantics chc (extract c) ⟧₁ c) (fnoc t i) - ∎ - - cong-compiler : ∀ V F → ConstructFunctor (Construct V F) - cong-compiler _ _ = record - { map = map - ; preserves = map-compile-preserves - } diff --git a/src/Construct/NestedChoice.agda b/src/Construct/NestedChoice.agda index 2e4752e7..0fdf2e6d 100644 --- a/src/Construct/NestedChoice.agda +++ b/src/Construct/NestedChoice.agda @@ -7,21 +7,20 @@ module Construct.NestedChoice (F : 𝔽) where open import Data.String using (String) open import Size using (Size; ↑_) -import Construct.Choices as Chc -open Chc.Choice₂ renaming (Syntax to 2Choice; Standard-Semantics to ⟦_⟧₂; Config to Config₂; show to show-2choice) +open import Construct.Choices data NestedChoice : Size → 𝔼 where value : ∀ {i A} → A → NestedChoice i A - choice : ∀ {i A} → 2Choice F (NestedChoice i A) → NestedChoice (↑ i) A + choice : ∀ {i A} → 2Choice.Syntax F (NestedChoice i A) → NestedChoice (↑ i) A -⟦_⟧ : ∀ {i A} → NestedChoice i A → Config₂ F → A +⟦_⟧ : ∀ {i A} → NestedChoice i A → 2Choice.Config F → A ⟦ value v ⟧ c = v -⟦ choice chc ⟧ c = ⟦ ⟦ chc ⟧₂ c ⟧ c +⟦ choice chc ⟧ c = ⟦ 2Choice.⟦ chc ⟧ c ⟧ c show-nested-choice : ∀ {i A} → (F → String) → (A → String) → NestedChoice i A → String show-nested-choice show-q show-carrier ( value v) = show-carrier v show-nested-choice show-q show-carrier (choice c) = - show-2choice + 2Choice.show show-q (show-nested-choice show-q show-carrier) c diff --git a/src/Data/IndexedSet.lagda.md b/src/Data/IndexedSet.lagda.md index b84142be..3076dc23 100644 --- a/src/Data/IndexedSet.lagda.md +++ b/src/Data/IndexedSet.lagda.md @@ -30,7 +30,7 @@ open import Data.Empty.Polymorphic using (⊥) open import Data.Unit.Polymorphic using (⊤; tt) open import Data.Product using (_×_; _,_; ∃-syntax; Σ-syntax; proj₁; proj₂) -open import Relation.Binary.PropositionalEquality using (_≗_) +open import Relation.Binary.PropositionalEquality using (_≗_; subst) open import Relation.Nullary using (¬_) open import Function using (id; _∘_; Congruent; Surjective) --IsSurjection) @@ -254,6 +254,9 @@ irrelevant-index-≅ x const-A const-B = ≅[]-trans {A = A} {C = C} (A⊆B , B⊆A) (B⊆C , C⊆B) = ⊆[]-trans {C = C} A⊆B B⊆C , ⊆[]-trans {C = A} C⊆B B⊆A + +⊆→≅ : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} → (f : I → J) → (f⁻¹ : J → I) → f ∘ f⁻¹ ≗ id → A ⊆[ f ] B → A ≅[ f ][ f⁻¹ ] B +⊆→≅ {A = A} {B = B} f f⁻¹ f∘f⁻¹ A⊆B = A⊆B , (λ i → Eq.sym (subst (λ j → A (f⁻¹ i) ≈ B j) (f∘f⁻¹ i) (A⊆B (f⁻¹ i)))) ``` ## Equational Reasoning diff --git a/src/Framework/Compiler.agda b/src/Framework/Compiler.agda index 35ea7353..9f9105b6 100644 --- a/src/Framework/Compiler.agda +++ b/src/Framework/Compiler.agda @@ -24,16 +24,19 @@ record LanguageCompiler {V} (Γ₁ Γ₂ : VariabilityLanguage V) : Set₁ where field compile : ∀ {A} → L₁ A → L₂ A - config-compiler : Config Γ₁ ⇔ Config Γ₂ + config-compiler : ∀ {A} → L₁ A → Config Γ₁ ⇔ Config Γ₂ preserves : ∀ {A} (e : L₁ A) - → ⟦ e ⟧₁ ≅[ to config-compiler ][ from config-compiler ] ⟦ compile e ⟧₂ + → ⟦ e ⟧₁ ≅[ to (config-compiler e) ][ from (config-compiler e) ] ⟦ compile e ⟧₂ -- TODO: It might nice to have syntax -- ≅[ config-compiler ] -- to abbreviate -- ≅[ to config-compiler ][ from config-compiler ]. - conf = to config-compiler - fnoc = from config-compiler + conf : ∀ {A} → L₁ A → Config Γ₁ → Config Γ₂ + conf e = to (config-compiler e) + + fnoc : ∀ {A} → L₁ A → Config Γ₂ → Config Γ₁ + fnoc e = from (config-compiler e) -- Compiles a single construct to another one without altering the underlying sub expressions. record ConstructCompiler {V} (VC₁ VC₂ : VariabilityConstruct V) (Γ : VariabilityLanguage V) : Set₁ where @@ -49,31 +52,6 @@ record ConstructCompiler {V} (VC₁ VC₂ : VariabilityConstruct V) (Γ : Variab preserves : ∀ {A} (c : C₁ (Expression Γ) A) → Kem₁ Γ extract c ≅ Kem₂ Γ (to config-compiler ∘ extract) (compile c) -{-| -Compiles languages below constructs. -This means that an expression in a language Γ₁ of which we know that it has a specific -syntactic construct VC at the top is compiled to Γ₂ retaining the very same construct at the top. --} -record ConstructFunctor {V} (VC : VariabilityConstruct V) : Set₁ where - open LanguageCompiler - field - map : ∀ {A} {L₁ L₂ : 𝔼} - → (L₁ A → L₂ A) - → VSyntax VC L₁ A → VSyntax VC L₂ A - - -- Note: There also should be an extract₂ but it must be - -- equivalent to extract₁ ∘ fnoc t. - -- extract₂ : Config Γ₂ → construct-config - preserves : ∀ {A} - → (Γ₁ Γ₂ : VariabilityLanguage V) - → (extract : Compatible VC Γ₁) - → (t : LanguageCompiler Γ₁ Γ₂) - → (c : VSyntax VC (Expression Γ₁) A) - → to-is-Embedding (config-compiler t) - → VSemantics VC Γ₁ extract c - ≅[ conf t ][ fnoc t ] - VSemantics VC Γ₂ (extract ∘ fnoc t) (map (compile t) c) - _⊕ᶜᶜ_ : ∀ {K₁ K₂ K₃ : 𝕂} → K₁ ⇔ K₂ → K₂ ⇔ K₃ @@ -104,16 +82,16 @@ _⊕ᶜᶜ_ : ∀ {K₁ K₂ K₃ : 𝕂} id c₁ ∎ -_⊕ˡ_ : ∀ {V} +_⊕_ : ∀ {V} {Γ₁ : VariabilityLanguage V} {Γ₂ : VariabilityLanguage V} {Γ₃ : VariabilityLanguage V} → LanguageCompiler Γ₁ Γ₂ → LanguageCompiler Γ₂ Γ₃ → LanguageCompiler Γ₁ Γ₃ -_⊕ˡ_ {V} {Γ₁} {Γ₂} {Γ₃} L₁→L₂ L₂→L₃ = record +_⊕_ {V} {Γ₁} {Γ₂} {Γ₃} L₁→L₂ L₂→L₃ = record { compile = compile L₂→L₃ ∘ compile L₁→L₂ - ; config-compiler = record { to = conf'; from = fnoc' } + ; config-compiler = λ expr → record { to = conf' expr; from = fnoc' expr } ; preserves = p } where open LanguageCompiler @@ -121,16 +99,15 @@ _⊕ˡ_ {V} {Γ₁} {Γ₂} {Γ₃} L₁→L₂ L₂→L₃ = record ⟦_⟧₁ = Semantics Γ₁ ⟦_⟧₃ = Semantics Γ₃ - conf' : Config Γ₁ → Config Γ₃ - conf' = conf L₂→L₃ ∘ conf L₁→L₂ + conf' : ∀ {A} → Expression Γ₁ A → Config Γ₁ → Config Γ₃ + conf' expr = conf L₂→L₃ (compile L₁→L₂ expr) ∘ conf L₁→L₂ expr - fnoc' : Config Γ₃ → Config Γ₁ - fnoc' = fnoc L₁→L₂ ∘ fnoc L₂→L₃ + fnoc' : ∀ {A} → Expression Γ₁ A → Config Γ₃ → Config Γ₁ + fnoc' expr = fnoc L₁→L₂ expr ∘ fnoc L₂→L₃ (compile L₁→L₂ expr) - module _ {A : 𝔸} where - -- this pattern is very similar of ⊆[]-trans - p : ∀ (e : L₁ A) → ⟦ e ⟧₁ ≅[ conf' ][ fnoc' ] ⟦ compile L₂→L₃ (compile L₁→L₂ e) ⟧₃ - p e = ≅[]-trans (preserves L₁→L₂ e) (preserves L₂→L₃ (compile L₁→L₂ e)) + -- this pattern is very similar of ⊆[]-trans + p : ∀ {A : 𝔸} (e : L₁ A) → ⟦ e ⟧₁ ≅[ conf' e ][ fnoc' e ] ⟦ compile L₂→L₃ (compile L₁→L₂ e) ⟧₃ + p e = ≅[]-trans (preserves L₁→L₂ e) (preserves L₂→L₃ (compile L₁→L₂ e)) -- _⊕ᶜ_ : ∀ {K} {VC₁ VC₂ VC₃ : VariabilityConstruct K} -- → ConstructCompiler VC₁ VC₂ diff --git a/src/Framework/Relation/Expressiveness.lagda.md b/src/Framework/Relation/Expressiveness.lagda.md index b023d8a3..7177aad4 100644 --- a/src/Framework/Relation/Expressiveness.lagda.md +++ b/src/Framework/Relation/Expressiveness.lagda.md @@ -2,6 +2,7 @@ open import Framework.Definitions module Framework.Relation.Expressiveness (V : 𝕍) where +open import Data.EqIndexedSet using (≅[]→≅) open import Data.Product using (_,_; _×_; Σ-syntax; proj₁; proj₂) open import Relation.Nullary.Negation using (¬_) open import Relation.Binary using (IsEquivalence; Reflexive; Symmetric; Transitive; Antisymmetric) @@ -11,6 +12,7 @@ open import Function using (_∘_; Injective) open import Framework.VariabilityLanguage open import Framework.Relation.Expression V open import Framework.Relation.Function using (_⇒ₚ_) +open import Framework.Compiler ``` We say that a language `L₁` is as expressive as another language `L₂` **iff** for any expression `e₂` in `L₂`, there exists an expression `e₁` in `L₁` that describes the same function. @@ -80,4 +82,9 @@ expressiveness-by-translation : ∀ {L₁ L₂ : VariabilityLanguage V} → SemanticsPreserving L₁ L₂ t → L₂ ≽ L₁ expressiveness-by-translation t t-pres = λ e₂ → t e₂ , t-pres e₂ -- this implementation is very similar to ⊆[]→⊆ + +expressiveness-from-compiler : ∀ {L₁ L₂ : VariabilityLanguage V} + → LanguageCompiler L₁ L₂ + → L₂ ≽ L₁ +expressiveness-from-compiler compiler = expressiveness-by-translation (LanguageCompiler.compile compiler) (λ e → ≅[]→≅ (LanguageCompiler.preserves compiler e)) ``` diff --git a/src/Framework/TODO.lagda.md b/src/Framework/TODO.lagda.md index 08561b5f..ac80fc2a 100644 --- a/src/Framework/TODO.lagda.md +++ b/src/Framework/TODO.lagda.md @@ -10,8 +10,7 @@ open import Level using (0ℓ) open import Framework.Definitions open import Framework.VariabilityLanguage open import Framework.Construct -import Construct.Choices as Chc -open Chc.VLChoice₂ renaming (Syntax to 2Choice) +open import Construct.Choices open import Construct.NestedChoice using (NestedChoice) ``` @@ -132,7 +131,7 @@ postulate -- When levels are generalized, we do not have to specifically use 0ℓ here. embed : ∀ {V F A} {i} → (Γ : VariabilityLanguage V) - → 2Choice F ∈ₛ Expression Γ + → VL2Choice.Syntax F ∈ₛ Expression Γ → NestedChoice F i (Expression Γ A) → Expression Γ A ``` diff --git a/src/Framework/Variants.agda b/src/Framework/Variants.agda index 0aadb72c..f3454793 100644 --- a/src/Framework/Variants.agda +++ b/src/Framework/Variants.agda @@ -11,7 +11,7 @@ open import Size using (Size; ↑_; ∞) open import Framework.Definitions using (𝕍; 𝔸) open import Framework.VariabilityLanguage -open import Construct.Artifact as At using (_-<_>-; map-children; map-children-preserves) renaming (Syntax to Artifact; Construct to ArtifactC) +open import Construct.Artifact as At using (_-<_>-; map-children) renaming (Syntax to Artifact; Construct to ArtifactC) open import Data.EqIndexedSet @@ -80,7 +80,7 @@ module _ (V : 𝕍) (A : 𝔸) {Γ : VariabilityLanguage V} (encoder : VariantEn begin ⟦ compile encoder v ⟧ c ≡⟨ irrelevant-index (encoded-variant-is-singleton-set v) ⟩ - ⟦ compile encoder v ⟧ (conf encoder tt) + ⟦ compile encoder v ⟧ (conf encoder v tt) ≡˘⟨ proj₁ (preserves encoder v) tt ⟩ ⟦ v ⟧ᵥ tt ≡⟨⟩ @@ -94,7 +94,7 @@ rose-encoder : → VariantEncoder (Rose ∞) Γ rose-encoder Γ has c = record { compile = t - ; config-compiler = record { to = confi; from = fnoci } + ; config-compiler = λ _ → record { to = confi; from = fnoci } ; preserves = p } where diff --git a/src/Lang/2ADT.agda b/src/Lang/2ADT.agda index c3f772fc..db5224a9 100644 --- a/src/Lang/2ADT.agda +++ b/src/Lang/2ADT.agda @@ -12,18 +12,14 @@ open import Framework.VariabilityLanguage open import Framework.Variants using (GrulerVariant) open import Construct.GrulerArtifacts open import Construct.Choices -open import Construct.NestedChoice F public - -private - Choice₂ = VLChoice₂.Syntax - Config₂ = Choice₂.Config +open import Construct.NestedChoice F as NestedChoice using (NestedChoice) 2ADT : Size → 𝔼 2ADT i A = NestedChoice i (Leaf A) mutual 2ADTVL : ∀ {i : Size} → VariabilityLanguage GrulerVariant - 2ADTVL {i} = ⟪ 2ADT i , Config₂ F , semantics ⟫ + 2ADTVL {i} = ⟪ 2ADT i , 2Choice.Config F , semantics ⟫ - semantics : ∀ {i : Size} → 𝔼-Semantics GrulerVariant (Config₂ F) (2ADT i) - semantics e c = VLLeaf.elim-leaf VLLeaf.Leaf∈ₛGrulerVariant (⟦ e ⟧ c) + semantics : ∀ {i : Size} → 𝔼-Semantics GrulerVariant (2Choice.Config F) (2ADT i) + semantics e c = VLLeaf.elim-leaf VLLeaf.Leaf∈ₛGrulerVariant (NestedChoice.⟦ e ⟧ c) diff --git a/src/Lang/BCC.lagda.md b/src/Lang/2CC.lagda.md similarity index 81% rename from src/Lang/BCC.lagda.md rename to src/Lang/2CC.lagda.md index ef6c54ae..b25a0282 100644 --- a/src/Lang/BCC.lagda.md +++ b/src/Lang/2CC.lagda.md @@ -11,7 +11,7 @@ ```agda open import Framework.Definitions -module Lang.BCC (Dimension : 𝔽) where +module Lang.2CC (Dimension : 𝔽) where ``` ## Imports @@ -28,9 +28,7 @@ open import Framework.Variants open import Framework.VariabilityLanguage open import Framework.Construct open import Construct.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct) -import Construct.Choices as Chc -open Chc.VLChoice₂ using () renaming (Syntax to Choice₂; Semantics to chc-sem) -open Chc.Choice₂ using () renaming (Config to Config₂) +open import Construct.Choices ``` ## Syntax @@ -38,12 +36,12 @@ open Chc.Choice₂ using () renaming (Config to Config₂) In the following we formalize the binary normal forms for choice calculus. We express a normal form as a new data type such that a conversion of a choice calculus expression is proven in the type system. Our goal is to prove that every choice calculus expression can be expressed as a variant-equivalent choice calculus expression in which every choice is binary. ```agda -data BCC : Size → 𝔼 where - atom : ∀ {i A} → Artifact (BCC i) A → BCC (↑ i) A - chc : ∀ {i A} → Choice₂ Dimension (BCC i) A → BCC (↑ i) A +data 2CC : Size → 𝔼 where + atom : ∀ {i A} → Artifact (2CC i) A → 2CC (↑ i) A + chc : ∀ {i A} → VL2Choice.Syntax Dimension (2CC i) A → 2CC (↑ i) A pattern _-<_>- a cs = atom (a At.-< cs >-) -pattern _⟨_,_⟩ D l r = chc (D Chc.Choice₂.⟨ l , r ⟩) +pattern _⟨_,_⟩ D l r = chc (D 2Choice.⟨ l , r ⟩) ``` ## Semantics @@ -61,16 +59,16 @@ Defining it the other way around is also possible but we have to pick one defini We choose this order to follow the known _if c then a else b_ pattern where the evaluation of a condition _c_ to true means choosing the then-branch, which is the left one. ```agda Configuration : 𝕂 -Configuration = Config₂ Dimension +Configuration = 2Choice.Config Dimension module Sem (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where mutual - BCCL : ∀ {i : Size} → VariabilityLanguage V - BCCL {i} = ⟪ BCC i , Configuration , ⟦_⟧ ⟫ + 2CCL : ∀ {i : Size} → VariabilityLanguage V + 2CCL {i} = ⟪ 2CC i , Configuration , ⟦_⟧ ⟫ - ⟦_⟧ : ∀ {i : Size} → 𝔼-Semantics V Configuration (BCC i) - ⟦ atom x ⟧ = PlainConstruct-Semantics Artifact-Construct mkArtifact BCCL x - ⟦ chc x ⟧ = chc-sem V Dimension BCCL id x + ⟦_⟧ : ∀ {i : Size} → 𝔼-Semantics V Configuration (2CC i) + ⟦ atom x ⟧ = PlainConstruct-Semantics Artifact-Construct mkArtifact 2CCL x + ⟦ chc x ⟧ = VL2Choice.Semantics V Dimension 2CCL id x ``` ## Properties @@ -90,16 +88,16 @@ module Properties (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where module _ {A : 𝔸} where ast-factoring : ∀ {i} {D : Dimension} {a : A} {n : ℕ} - → (xs ys : Vec (BCC i A) n) + → (xs ys : Vec (2CC i A) n) ------------------------------------------------------------------------------------- - → BCCL ⊢ + → 2CCL ⊢ D ⟨ a -< toList xs >- , a -< toList ys >- ⟩ ≣₁ a -< toList (zipWith (D ⟨_,_⟩) xs ys) >- ast-factoring xs ys c = {!!} - choice-idempotency : ∀ {D} {e : BCC ∞ A} -- do not use ∞ here? + choice-idempotency : ∀ {D} {e : 2CC ∞ A} -- do not use ∞ here? --------------------------- - → BCCL ⊢ D ⟨ e , e ⟩ ≣₁ e + → 2CCL ⊢ D ⟨ e , e ⟩ ≣₁ e choice-idempotency {D} {e} c with c D ... | false = refl ... | true = refl @@ -117,9 +115,9 @@ module Properties (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where Then we could say: ∀ expressions 'e' and 'e′', prefix 'p', and tail 't' - with 'BCC , ⟦_⟧ ⊢ e ≈ e′' + with '2CC , ⟦_⟧ ⊢ e ≈ e′' ----------------------------------------------------------------------------------- - 'BCC , ⟦_⟧ ⊢ Artifact a (toList (p -∷ e ∷- t)) ≈ Artifact a (toList (p -∷ e′ ∷- t))' + '2CC , ⟦_⟧ ⊢ Artifact a (toList (p -∷ e ∷- t)) ≈ Artifact a (toList (p -∷ e′ ∷- t))' where toList turns a zipper to a list and '-∷' and '∷-' denote the focus location behind the prefix and before the tail in the zipper. I expect proving this theorem to be quite boilerplaty but easy in theory: To show that both artifacts are semantically equivalent, we have to show that all the child nodes remain semantically equal. @@ -127,18 +125,18 @@ module Properties (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where for e and e′, we know it per assumption. -} - choice-l-congruence : ∀ {i : Size} {D : Dimension} {l l′ r : BCC i A} - → BCCL ⊢ l ≣₁ l′ + choice-l-congruence : ∀ {i : Size} {D : Dimension} {l l′ r : 2CC i A} + → 2CCL ⊢ l ≣₁ l′ --------------------------------------- - → BCCL ⊢ D ⟨ l , r ⟩ ≣₁ D ⟨ l′ , r ⟩ + → 2CCL ⊢ D ⟨ l , r ⟩ ≣₁ D ⟨ l′ , r ⟩ choice-l-congruence {D = D} l≣l′ c with c D ... | false = refl ... | true = l≣l′ c - choice-r-congruence : ∀ {i : Size} {D : Dimension} {l r r′ : BCC i A} - → BCCL ⊢ r ≣₁ r′ + choice-r-congruence : ∀ {i : Size} {D : Dimension} {l r r′ : 2CC i A} + → 2CCL ⊢ r ≣₁ r′ --------------------------------------- - → BCCL ⊢ D ⟨ l , r ⟩ ≣₁ D ⟨ l , r′ ⟩ + → 2CCL ⊢ D ⟨ l , r ⟩ ≣₁ D ⟨ l , r′ ⟩ choice-r-congruence {D = D} r≣r′ c with c D ... | false = r≣r′ c ... | true = refl @@ -158,7 +156,7 @@ module Redundancy (_==_ : Dimension → Dimension → Bool) where then just b else scope D' - eliminate-redundancy-in : ∀ {i : Size} {A : 𝔸} → Scope → BCC i A → BCC ∞ A + eliminate-redundancy-in : ∀ {i : Size} {A : 𝔸} → Scope → 2CC i A → 2CC ∞ A eliminate-redundancy-in scope (a -< es >-) = a -< mapl (eliminate-redundancy-in scope) es >- eliminate-redundancy-in scope (D ⟨ l , r ⟩) with scope D ... | just true = eliminate-redundancy-in scope l @@ -167,16 +165,16 @@ module Redundancy (_==_ : Dimension → Dimension → Bool) where , eliminate-redundancy-in (refine scope D false) r ⟩ - eliminate-redundancy : ∀ {i : Size} {A : 𝔸} → BCC i A → BCC ∞ A + eliminate-redundancy : ∀ {i : Size} {A : 𝔸} → 2CC i A → 2CC ∞ A eliminate-redundancy = eliminate-redundancy-in (λ _ → nothing) open import Framework.Compiler using (LanguageCompiler) module _ (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where open Sem V mkArtifact - Redundancy-Elimination : LanguageCompiler BCCL BCCL + Redundancy-Elimination : LanguageCompiler 2CCL 2CCL Redundancy-Elimination = record { compile = eliminate-redundancy - ; config-compiler = record { to = id ; from = id } + ; config-compiler = λ _ → record { to = id ; from = id } ; preserves = {!!} } ``` @@ -187,7 +185,7 @@ module Redundancy (_==_ : Dimension → Dimension → Bool) where open Data.List using (concatMap) renaming (_++_ to _++l_) -- get all dimensions used in a binary CC expression -dims : ∀ {i : Size} {A : Set} → BCC i A → List Dimension +dims : ∀ {i : Size} {A : Set} → 2CC i A → List Dimension dims (_ -< es >-) = concatMap dims es dims (D ⟨ l , r ⟩) = D ∷ (dims l ++l dims r) ``` @@ -199,13 +197,13 @@ open import Data.String using (String; _++_; intersperse) module Pretty (show-D : Dimension → String) where open import Show.Lines - show : ∀ {i} → BCC i String → String + show : ∀ {i} → 2CC i String → String show (a -< [] >-) = a show (a -< es@(_ ∷ _) >-) = a ++ "-<" ++ (intersperse ", " (mapl show es)) ++ ">-" show (D ⟨ l , r ⟩) = show-D D ++ "⟨" ++ (show l) ++ ", " ++ (show r) ++ "⟩" - pretty : ∀ {i : Size} → BCC i String → Lines + pretty : ∀ {i : Size} → 2CC i String → Lines pretty (a -< [] >-) = > a pretty (a -< es@(_ ∷ _) >-) = do > a ++ "-<" diff --git a/src/Lang/CCC.lagda.md b/src/Lang/CCC.lagda.md index ddf0b0a2..5ec88942 100644 --- a/src/Lang/CCC.lagda.md +++ b/src/Lang/CCC.lagda.md @@ -37,9 +37,7 @@ open import Framework.Construct open import Data.EqIndexedSet as ISet open import Construct.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct) -import Construct.Choices as Chc -open Chc.VLChoiceₙ using () renaming (Syntax to Choiceₙ; Semantics to chc-sem) -open Chc.Choiceₙ using () renaming (Config to Configₙ) +open import Construct.Choices ``` ## Syntax @@ -47,10 +45,10 @@ open Chc.Choiceₙ using () renaming (Config to Configₙ) ```agda data CCC : Size → 𝔼 where atom : ∀ {i A} → Artifact (CCC i) A → CCC (↑ i) A - chc : ∀ {i A} → Choiceₙ Dimension (CCC i) A → CCC (↑ i) A + chc : ∀ {i A} → VLChoice.Syntax Dimension (CCC i) A → CCC (↑ i) A pattern _-<_>- a cs = atom (a At.-< cs >-) -pattern _⟨_⟩ D cs = chc (D Chc.Choiceₙ.⟨ cs ⟩) +pattern _⟨_⟩ D cs = chc (D Choice.⟨ cs ⟩) ``` ## Semantics @@ -67,7 +65,7 @@ Thus, and for much simpler proofs, we choose the functional semantics. First, we define configurations as functions that evaluate dimensions by tags: ```agda Configuration : 𝕂 -Configuration = Configₙ Dimension +Configuration = Choice.Config Dimension ``` We can now define the semantics. @@ -79,9 +77,9 @@ module Sem (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where CCCL : ∀ {i : Size} → VariabilityLanguage V CCCL {i} = ⟪ CCC i , Configuration , ⟦_⟧ ⟫ - ⟦_⟧ : ∀ {i : Size} → 𝔼-Semantics V (Configₙ Dimension) (CCC i) + ⟦_⟧ : ∀ {i : Size} → 𝔼-Semantics V (Choice.Config Dimension) (CCC i) ⟦ atom x ⟧ = PlainConstruct-Semantics Artifact-Construct mkArtifact CCCL x - ⟦ chc x ⟧ = chc-sem V Dimension CCCL id x + ⟦ chc x ⟧ = VLChoice.Semantics V Dimension CCCL id x ``` ## Properties @@ -181,7 +179,7 @@ module Encode where encoder : VariantEncoder V CCCL encoder = record { compile = encode - ; config-compiler = confs + ; config-compiler = λ _ → confs ; preserves = preserves } ``` diff --git a/src/Lang/Gruler.agda b/src/Lang/Gruler.agda index c4fba174..f84424ec 100644 --- a/src/Lang/Gruler.agda +++ b/src/Lang/Gruler.agda @@ -16,27 +16,25 @@ open import Framework.Construct open import Construct.Choices open import Construct.GrulerArtifacts -open Construct.Choices.Choice₂ using (_⟨_,_⟩) renaming (Config to Config₂) +open 2Choice using (_⟨_,_⟩) private PC = VLParallelComposition.Syntax pc-semantics = PlainConstruct-Semantics VLParallelComposition.Construct VLParallelComposition.ParallelComposition∈ₛGrulerVariant - Choice₂ = VLChoice₂.Syntax - choice₂-semantics = VLChoice₂.Semantics data Gruler : Size → 𝔼 where GAsset : ∀ {i A} → Leaf A → Gruler i A GPComp : ∀ {i A} → ParallelComposition (Gruler i A) → Gruler (↑ i) A - GChoice : ∀ {i A} → Choice₂ F (Gruler i) A → Gruler (↑ i) A + GChoice : ∀ {i A} → VL2Choice.Syntax F (Gruler i) A → Gruler (↑ i) A -semantics : ∀ {i : Size} → 𝔼-Semantics GrulerVariant (Config₂ F) (Gruler i) +semantics : ∀ {i : Size} → 𝔼-Semantics GrulerVariant (2Choice.Config F) (Gruler i) GrulerVL : ∀ {i : Size} → VariabilityLanguage GrulerVariant -GrulerVL {i} = ⟪ Gruler i , Config₂ F , semantics ⟫ +GrulerVL {i} = ⟪ Gruler i , 2Choice.Config F , semantics ⟫ semantics (GAsset a) _ = VLLeaf.elim-leaf VLLeaf.Leaf∈ₛGrulerVariant a semantics (GPComp pc) = pc-semantics GrulerVL pc -semantics (GChoice chc) = choice₂-semantics GrulerVariant F GrulerVL id chc +semantics (GChoice chc) = VL2Choice.Semantics GrulerVariant F GrulerVL id chc gruler-has-leaf : ∀ {i} → VLLeaf.Syntax ∈ₛ Gruler i gruler-has-leaf {i} = record @@ -48,21 +46,21 @@ gruler-has-leaf {i} = record snoc' (GAsset A) = just A snoc' _ = nothing -gruler-has-choice : Choice₂ F ∈ₛ Gruler ∞ +gruler-has-choice : VL2Choice.Syntax F ∈ₛ Gruler ∞ gruler-has-choice = record { cons = GChoice ; snoc = snoc' ; id-l = λ _ → refl } - where snoc' : ∀ {i A} → Gruler (↑ i) A → Maybe (Choice₂ F (Gruler i) A) + where snoc' : ∀ {i A} → Gruler (↑ i) A → Maybe (VL2Choice.Syntax F (Gruler i) A) snoc' (GChoice chc) = just chc snoc' _ = nothing -gruler-models-choice : VLChoice₂.Construct GrulerVariant F ⟦∈⟧ᵥ GrulerVL +gruler-models-choice : VL2Choice.Construct GrulerVariant F ⟦∈⟧ᵥ GrulerVL make gruler-models-choice = gruler-has-choice extract gruler-models-choice = id preservation gruler-models-choice _ _ = refl gruler-choice-preserves : ∀ {A : 𝔸} {D l r c} - → semantics (GChoice {A = A} (D ⟨ l , r ⟩)) c ≡ choice₂-semantics GrulerVariant F GrulerVL id (D ⟨ l , r ⟩) c + → semantics (GChoice {A = A} (D ⟨ l , r ⟩)) c ≡ VL2Choice.Semantics GrulerVariant F GrulerVL id (D ⟨ l , r ⟩) c gruler-choice-preserves = refl diff --git a/src/Lang/NADT.agda b/src/Lang/NADT.agda index 9a693d2e..cdc9345e 100644 --- a/src/Lang/NADT.agda +++ b/src/Lang/NADT.agda @@ -8,24 +8,20 @@ open import Data.Nat using (ℕ) open import Function using (id) open import Size using (Size; ↑_) +open import Framework.Construct open import Framework.VariabilityLanguage open import Framework.Variants using (GrulerVariant) open import Construct.GrulerArtifacts open import Construct.Choices -private - Choiceₙ = VLChoiceₙ.Syntax - Configₙ = Choiceₙ.Config - choice-semantics = VLChoiceₙ.Semantics - data NADT : Size → 𝔼 where - NADTAsset : ∀ {i A} → Leaf A → NADT i A - NADTChoice : ∀ {i A} → Choiceₙ F (NADT i) A → NADT (↑ i) A + NADTAsset : ∀ {i A} → Leaf A → NADT i A + NADTChoice : ∀ {i A} → VLChoice.Syntax F (NADT i) A → NADT (↑ i) A mutual NADTVL : ∀ {i : Size} → VariabilityLanguage GrulerVariant - NADTVL {i} = ⟪ NADT i , Configₙ F , semantics ⟫ + NADTVL {i} = ⟪ NADT i , Choice.Config F , semantics ⟫ - semantics : ∀ {i : Size} → 𝔼-Semantics GrulerVariant (Configₙ F) (NADT i) + semantics : ∀ {i : Size} → 𝔼-Semantics GrulerVariant (Choice.Config F) (NADT i) semantics (NADTAsset a) _ = VLLeaf.elim-leaf VLLeaf.Leaf∈ₛGrulerVariant a - semantics (NADTChoice chc) = choice-semantics GrulerVariant F NADTVL id chc + semantics (NADTChoice chc) = VLChoice.Semantics GrulerVariant F NADTVL id chc diff --git a/src/Lang/NCC.lagda.md b/src/Lang/NCC.lagda.md new file mode 100644 index 00000000..a7d94ab5 --- /dev/null +++ b/src/Lang/NCC.lagda.md @@ -0,0 +1,103 @@ +# Fixed Arity Choice Calculus + +## Options + +```agda +{-# OPTIONS --sized-types #-} +{-# OPTIONS --allow-unsolved-metas #-} +``` + +## Module + +It's required that arity is at least one to have a semantic. However, we require +that the arity is at least two, otherwise there is this annoying one-arity +language in the NCC language family which is incomplete. + +```agda +open import Framework.Definitions +open import Util.Nat.AtLeast using (ℕ≥) +module Lang.NCC (n : ℕ≥ 2) (Dimension : 𝔽) where +``` + +## Imports + +```agda +open import Data.Bool using (Bool; true; false; if_then_else_) +open import Data.List + using (List; []; _∷_; lookup) + renaming (map to mapl) +open import Function using (id) +open import Size using (Size; ↑_; ∞) + +open import Framework.Variants +open import Framework.VariabilityLanguage +open import Framework.Construct +open import Construct.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct) +open import Construct.Choices +``` + +## Syntax + +```agda +data NCC : Size → 𝔼 where + atom : ∀ {i A} → Artifact (NCC i) A → NCC (↑ i) A + chc : ∀ {i A} → VLNChoice.Syntax n Dimension (NCC i) A → NCC (↑ i) A + +pattern _-<_>- a cs = atom (a At.-< cs >-) +pattern _⟨_⟩ D cs = chc (D NChoice.⟨ cs ⟩) +``` + +## Semantics + +```agda +Configuration : 𝕂 +Configuration = NChoice.Config n Dimension + +module Sem (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where + mutual + NCCL : ∀ {i : Size} → VariabilityLanguage V + NCCL {i} = ⟪ NCC i , Configuration , ⟦_⟧ ⟫ + + ⟦_⟧ : ∀ {i : Size} → 𝔼-Semantics V Configuration (NCC i) + ⟦ atom x ⟧ = PlainConstruct-Semantics Artifact-Construct mkArtifact NCCL x + ⟦ chc x ⟧ = VLNChoice.Semantics n V Dimension NCCL id x +``` + +## Utility + +```agda +open Data.List using (concatMap) renaming (_++_ to _++l_) +import Data.Vec as Vec + +-- get all dimensions used in a binary CC expression +dims : ∀ {i : Size} {A : Set} → NCC i A → List Dimension +dims (_ -< es >-) = concatMap dims es +dims (D ⟨ cs ⟩) = D ∷ concatMap dims (Vec.toList cs) +``` + +## Show + +```agda +open import Data.String using (String; _++_; intersperse) +module Pretty (show-D : Dimension → String) where + open import Show.Lines + + show : ∀ {i} → NCC i String → String + show (a -< [] >-) = a + show (a -< es@(_ ∷ _) >-) = a ++ "-<" ++ (intersperse ", " (mapl show es)) ++ ">-" + show (D ⟨ cs ⟩) = show-D D ++ "⟨" ++ (intersperse ", " (mapl show (Vec.toList cs))) ++ "⟩" + + + pretty : ∀ {i : Size} → NCC i String → Lines + pretty (a -< [] >-) = > a + pretty (a -< es@(_ ∷ _) >-) = do + > a ++ "-<" + indent 2 do + lines (mapl pretty es) + > ">-" + pretty (D ⟨ cs ⟩) = do + > show-D D ++ "⟨" + indent 2 do + lines (mapl pretty (Vec.toList cs)) + > "⟩" +``` diff --git a/src/Lang/OC.lagda.md b/src/Lang/OC.lagda.md index 1ba386e5..5de31049 100644 --- a/src/Lang/OC.lagda.md +++ b/src/Lang/OC.lagda.md @@ -27,9 +27,6 @@ open import Framework.Variants open import Framework.VariabilityLanguage open import Framework.Construct open import Construct.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct) -import Construct.Choices as Chc -open Chc.VLChoice₂ using () renaming (Syntax to Choice₂; Semantics to chc-sem) -open Chc.Choice₂ using () renaming (Config to Config₂) ``` ## Syntax @@ -42,7 +39,7 @@ data OC : Size → 𝔼 where Below is a commented out variant of this type where we reuse that constructor. However, for some unfathomable reason then termination - checking fails within OC-to-BCC.agda + checking fails within OC-to-2CC.agda because prepending an 'OC i A' to a 'Vec (OC (↑ i) A) n' is illegal then (but as of now just works). I have no idea what's the reason for this. @@ -141,7 +138,7 @@ TODO: Maybe we can still explicitly construct the `Unsound` predicate. ### Well-formed option calculus is sound ```agda --- TODO (Probably prove via soundness-by-expressiveness (done) and soundness of BCC (todo)) +-- TODO (Probably prove via soundness-by-expressiveness (done) and soundness of 2CC (todo)) ``` diff --git a/src/Main.agda b/src/Main.agda index c8d202e5..3808eb79 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -21,10 +21,10 @@ open import Lang.OC using (WFOC) open import Test.Examples.CCC using (cccex-all) open import Test.Examples.OC using (optex-all) -open import Test.Experiments.CCC-to-BCC -open import Test.Experiments.OC-to-BCC +open import Test.Experiments.CCC-to-2CC +open import Test.Experiments.OC-to-2CC -open import Translation.Experiments.NChoice-to-2Choice-Experiment using (exp; all-ex) +open import Translation.Experiments.Choice-to-2Choice-Experiment using (exp; all-ex) {-| A list of programs that we want to run. diff --git a/src/Test/Experiments/CCC-to-BCC.agda b/src/Test/Experiments/CCC-to-2CC.agda similarity index 78% rename from src/Test/Experiments/CCC-to-BCC.agda rename to src/Test/Experiments/CCC-to-2CC.agda index f6eea515..9e689123 100644 --- a/src/Test/Experiments/CCC-to-BCC.agda +++ b/src/Test/Experiments/CCC-to-2CC.agda @@ -1,6 +1,6 @@ {-# OPTIONS --sized-types #-} -module Test.Experiments.CCC-to-BCC where +module Test.Experiments.CCC-to-2CC where open import Data.Bool using (Bool) @@ -25,12 +25,12 @@ open import Framework.Annotation.Name using (Dimension) -- open import Lang.CCC -- renaming (Configuration to Configurationₙ; -- ⟦_⟧ to ⟦_⟧ₙ) --- open import Lang.BCC +-- open import Lang.2CC -- renaming (Configuration to Configuration₂; -- ⟦_⟧ to ⟦_⟧₂) -- open import Framework.Definitions using (ℂ) --- open import Translation.CCC-to-BCC using (CCC→BCC) +-- open import Translation.CCC-to-2CC using (CCC→2CC) -- open import Framework.Proof.Translation using (expr; conf; fnoc) -- open import Util.ShowHelpers @@ -48,23 +48,23 @@ open import Framework.Annotation.Name using (Dimension) -- all-n : ℕ → Named Configurationₙ -- all-n n = (λ _ → n) called ("all-" ++ show-nat n) --- CCC→BCC-Test : UnitTest ℕ --- CCC→BCC-Test n = ForAllExamplesIn cccex-all (test-translation CCC→BCC (get (all-n n))) +-- CCC→2CC-Test : UnitTest ℕ +-- CCC→2CC-Test n = ForAllExamplesIn cccex-all (test-translation CCC→2CC (get (all-n n))) --- CCC→BCC-Test-fnoc∘conf : UnitTest ℕ --- CCC→BCC-Test-fnoc∘conf n = ForAllExamplesIn cccex-all (test-translation-fnoc∘conf≡id CCC→BCC (get (all-n n))) +-- CCC→2CC-Test-fnoc∘conf : UnitTest ℕ +-- CCC→2CC-Test-fnoc∘conf n = ForAllExamplesIn cccex-all (test-translation-fnoc∘conf≡id CCC→2CC (get (all-n n))) --- CCC→BCC-Test-all0 : RunTest CCC→BCC-Test 0 --- CCC→BCC-Test-all0 = refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ []))))) +-- CCC→2CC-Test-all0 : RunTest CCC→2CC-Test 0 +-- CCC→2CC-Test-all0 = refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ []))))) --- CCC→BCC-Test-all1 : RunTest CCC→BCC-Test 1 --- CCC→BCC-Test-all1 = refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ []))))) +-- CCC→2CC-Test-all1 : RunTest CCC→2CC-Test 1 +-- CCC→2CC-Test-all1 = refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ []))))) --- CCC→BCC-Test-fnoc∘conf-all0 : RunTest CCC→BCC-Test-fnoc∘conf 0 --- CCC→BCC-Test-fnoc∘conf-all0 = refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ []))))) +-- CCC→2CC-Test-fnoc∘conf-all0 : RunTest CCC→2CC-Test-fnoc∘conf 0 +-- CCC→2CC-Test-fnoc∘conf-all0 = refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ []))))) --- CCC→BCC-Test-fnoc∘conf-all1 : RunTest CCC→BCC-Test-fnoc∘conf 1 --- CCC→BCC-Test-fnoc∘conf-all1 = refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ []))))) +-- CCC→2CC-Test-fnoc∘conf-all1 : RunTest CCC→2CC-Test-fnoc∘conf 1 +-- CCC→2CC-Test-fnoc∘conf-all1 = refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ (refl ∷ []))))) -- -- Print all values of a configuration for a list of given dimensions: -- show-nary-config : Configurationₙ → List Dimension → String @@ -76,15 +76,15 @@ open import Framework.Annotation.Name using (Dimension) -- -- Convert a given named choice calculus formula to binary normal form and back and print all intermediate results. -- -- Do so for two configurations, one configuration that always selects 0, and one that always selects 1. -- exp-to-binary-and-back : Experiment (CCC ∞ String) --- getName exp-to-binary-and-back = "CCC to BCC and back" +-- getName exp-to-binary-and-back = "CCC to 2CC and back" -- get exp-to-binary-and-back ex@(cc called name) = -- let -- conf-vals : List ℕ -- conf-vals = 0 ∷ 1 ∷ 2 ∷ [] --- translation-result = CCC→BCC cc +-- translation-result = CCC→2CC cc --- expr-named : Named (BCC ∞ String) +-- expr-named : Named (2CC ∞ String) -- expr-named = expr translation-result called "toCC₂ " ++ name -- conf-named : Named Configurationₙ → Named Configuration₂ @@ -105,7 +105,7 @@ open import Framework.Annotation.Name using (Dimension) -- show-all-n : ℕ → String -- show-all-n = λ n → show-named (λ c → show-nary-config c (Lang.CCC.dims cc)) (all-n n) -- show-conf-all-n : ℕ → String --- show-conf-all-n = λ n → show-named (λ c → show-binary-config c (Lang.BCC.dims (get expr-named))) (conf-named (all-n n)) +-- show-conf-all-n = λ n → show-named (λ c → show-binary-config c (Lang.2CC.dims (get expr-named))) (conf-named (all-n n)) -- show-fnoc-conf-all-n : ℕ → String -- show-fnoc-conf-all-n = λ n → show-named (λ c → show-nary-config c (Lang.CCC.dims cc)) (fnoc-named (conf-named (all-n n))) -- in do @@ -114,7 +114,7 @@ open import Framework.Annotation.Name using (Dimension) -- lines (mapl eval-all-n conf-vals) -- linebreak --- > show-named Lang.BCC.show expr-named +-- > show-named Lang.2CC.show expr-named -- >∷ mapl (show-conf-all-n) conf-vals -- lines (mapl eval-forth-all-n conf-vals) -- linebreak diff --git a/src/Test/Experiments/OC-to-BCC.agda b/src/Test/Experiments/OC-to-2CC.agda similarity index 68% rename from src/Test/Experiments/OC-to-BCC.agda rename to src/Test/Experiments/OC-to-2CC.agda index aa12d951..6e7ca4bb 100644 --- a/src/Test/Experiments/OC-to-BCC.agda +++ b/src/Test/Experiments/OC-to-2CC.agda @@ -1,6 +1,6 @@ {-# OPTIONS --sized-types #-} -module Test.Experiments.OC-to-BCC where +module Test.Experiments.OC-to-2CC where open import Data.Bool using (Bool; true; false) open import Data.List using (_∷_; []) @@ -23,14 +23,14 @@ Variant = Rose ∞ mkArtifact = Artifact∈ₛRose open import Lang.OC Feature as OCL renaming (Configuration to Conf-oc) -open import Lang.BCC Feature as BCCL +open import Lang.2CC Feature as 2CCL open OCL.Sem Variant mkArtifact renaming (⟦_⟧ to ⟦_⟧-oc) open OCL.Show id -open BCCL.Sem Variant mkArtifact -open BCCL.Redundancy _==_ -open BCCL.Pretty id +open 2CCL.Sem Variant mkArtifact +open 2CCL.Redundancy _==_ +open 2CCL.Pretty id -open import Translation.Lang.OC-to-BCC Feature using (compile; compile-configs) +open import Translation.Lang.OC-to-2CC Feature using (compile; compile-configs) open import Show.Lines open import Util.Named @@ -42,30 +42,30 @@ open import Test.Examples.OC open import Test.UnitTest -OC→BCC-Test : UnitTest Conf-oc -OC→BCC-Test c = ForAllExamplesIn optex-all (test-translation WFOCL BCCL compile compile-configs c) +OC→2CC-Test : UnitTest Conf-oc +OC→2CC-Test c = ForAllExamplesIn optex-all (test-translation WFOCL 2CCL compile compile-configs c) -OC→BCC-Test-conffnoc : UnitTest Conf-oc -OC→BCC-Test-conffnoc c = ForAllExamplesIn optex-all (test-translation-fnoc∘conf≡id WFOCL BCCL compile-configs c) +OC→2CC-Test-conffnoc : UnitTest Conf-oc +OC→2CC-Test-conffnoc c = ForAllExamplesIn optex-all (test-translation-fnoc∘conf≡id WFOCL 2CCL compile-configs c) -- agda computes this value automatically! -- Better: When we add a new example to optex-all, the test wont compile before we adapted it. So we can never forget to test it. -OC→BCC-Test-allyes : RunTest OC→BCC-Test (get allyes-oc) -OC→BCC-Test-allyes = refl ∷ refl ∷ refl ∷ refl ∷ [] +OC→2CC-Test-allyes : RunTest OC→2CC-Test (get allyes-oc) +OC→2CC-Test-allyes = refl ∷ refl ∷ refl ∷ refl ∷ [] -OC→BCC-Test-allno : RunTest OC→BCC-Test (get allno-oc) -OC→BCC-Test-allno = refl ∷ refl ∷ refl ∷ refl ∷ [] +OC→2CC-Test-allno : RunTest OC→2CC-Test (get allno-oc) +OC→2CC-Test-allno = refl ∷ refl ∷ refl ∷ refl ∷ [] -OC→BCC-Test-conffnoc-allyes : RunTest OC→BCC-Test-conffnoc (get allyes-oc) -OC→BCC-Test-conffnoc-allyes = refl ∷ refl ∷ refl ∷ refl ∷ [] +OC→2CC-Test-conffnoc-allyes : RunTest OC→2CC-Test-conffnoc (get allyes-oc) +OC→2CC-Test-conffnoc-allyes = refl ∷ refl ∷ refl ∷ refl ∷ [] -OC→BCC-Test-conffnoc-allno : RunTest OC→BCC-Test-conffnoc (get allno-oc) -OC→BCC-Test-conffnoc-allno = refl ∷ refl ∷ refl ∷ refl ∷ [] +OC→2CC-Test-conffnoc-allno : RunTest OC→2CC-Test-conffnoc (get allno-oc) +OC→2CC-Test-conffnoc-allno = refl ∷ refl ∷ refl ∷ refl ∷ [] -- Translate an option calculus expression. -- Then configure it with an all-yes and an all-no config and print the resulting variants. exp-oc-to-bcc : Experiment (WFOC ∞ String) -getName exp-oc-to-bcc = "Translate OC to BCC" +getName exp-oc-to-bcc = "Translate OC to 2CC" get exp-oc-to-bcc ex@(name ≔ oc) = do let --trans-result = translate oc --bcc = expr trans-result diff --git a/src/Translation/Construct/2Choice-to-Choice-VL.agda b/src/Translation/Construct/2Choice-to-Choice-VL.agda new file mode 100644 index 00000000..018f78a2 --- /dev/null +++ b/src/Translation/Construct/2Choice-to-Choice-VL.agda @@ -0,0 +1,77 @@ +open import Framework.Definitions + +module Translation.Construct.2Choice-to-Choice-VL where + +open import Data.Bool using (Bool) +open import Data.Nat using (ℕ) +open import Data.Product using (proj₁; proj₂) +open import Function using (_∘_) + +-- open import Relation.Binary using (Setoid; IsEquivalence) +open import Relation.Binary.PropositionalEquality as Eq using (_≗_; refl) + +import Data.IndexedSet + +open import Framework.VariabilityLanguage +open import Framework.Construct +open import Framework.Compiler using (LanguageCompiler) +open import Framework.Relation.Function using (to-is-Embedding) + +import Translation.Construct.2Choice-to-Choice as 2Choice-to-Choice +open 2Choice-to-Choice using (ConfContract; FnocContract) + +open import Construct.Choices + +module Translate {Q : 𝔽} {V : 𝕍} {A : 𝔸} + (Γ₁ Γ₂ : VariabilityLanguage V) + (extract₁ : Compatible (VL2Choice.Construct V Q) Γ₁) + (t : LanguageCompiler Γ₁ Γ₂) + (confi : 2Choice.Config Q → Choice.Config Q) + (fnoci : Choice.Config Q → 2Choice.Config Q) + where + private + L₁ = Expression Γ₁ + ⟦_⟧₁ = Semantics Γ₁ + L₂ = Expression Γ₂ + ⟦_⟧₂ = Semantics Γ₂ + open LanguageCompiler t + + -- TODO: Generalize to any setoids over L₁ or L₂. + module 2Choice-to-Choice-T₁ = 2Choice-to-Choice.Translate {Q} (Eq.setoid (L₁ A)) + open 2Choice-to-Choice-T₁ using () renaming (convert to convert₁) + module 2Choice-to-Choice-T₂ = 2Choice-to-Choice.Translate {Q} (Eq.setoid (L₂ A)) + open 2Choice-to-Choice-T₂ using () renaming (convert to convert₂) + + {-| + Composition of two compilers: + First, we convert all alternatives from one language to another using `map₂ compile`. + Second, we convert the binary choice to an n-ary choice via convert, not changing any data. + The order of these steps does not matter, as proven by `convert-comm` below. + -} + compile-convert : VL2Choice.Syntax Q L₁ A → VLChoice.Syntax Q L₂ A + compile-convert = convert₂ ∘ 2Choice.map compile + + {-| + The same compiler as compile-convert, but the steps are executed in the other order. + -} + convert-compile : VL2Choice.Syntax Q L₁ A → VLChoice.Syntax Q L₂ A + convert-compile = Choice.map compile ∘ convert₁ + + {-| + Proof that the following square commutes. + This means that it does not matter in which order we + - convert a binary to an n-ary choice, + - compile subterms. + + Algebraically: + mapₙ compile ∘ convert ≗ convert ∘ map₂ compile + + Graphically: + binary L₁ ── convert ──→ nary L₁ + | | + | map₂ compile | mapₙ compile + ↓ ↓ + binary L₂ ── convert ──→ nary L₂ + -} + convert-comm : convert-compile ≗ compile-convert + convert-comm _ = refl diff --git a/src/Translation/Construct/2Choice-to-NChoice.agda b/src/Translation/Construct/2Choice-to-Choice.agda similarity index 70% rename from src/Translation/Construct/2Choice-to-NChoice.agda rename to src/Translation/Construct/2Choice-to-Choice.agda index 080655c3..06f18753 100644 --- a/src/Translation/Construct/2Choice-to-NChoice.agda +++ b/src/Translation/Construct/2Choice-to-Choice.agda @@ -1,5 +1,5 @@ {-# OPTIONS --allow-unsolved-metas #-} -module Translation.Construct.2Choice-to-NChoice {Q : Set} where +module Translation.Construct.2Choice-to-Choice {Q : Set} where open import Data.Bool using (Bool; false; true) open import Data.List using (List; _∷_; []) @@ -15,11 +15,10 @@ import Data.IndexedSet open import Framework.Definitions using (𝔽) open import Framework.Compiler using (ConstructCompiler) -open import Construct.Choices as Chc -open Chc.Choice₂ using (_⟨_,_⟩) renaming (Syntax to 2Choice; Standard-Semantics to ⟦_⟧₂; Config to Config₂) -open Chc.Choiceₙ using (_⟨_⟩) renaming (Syntax to NChoice; Standard-Semantics to ⟦_⟧ₙ; Config to Configₙ) -open Chc.VLChoice₂ using () renaming (Construct to C₂) -open Chc.VLChoiceₙ using () renaming (Construct to Cₙ) +open import Construct.Choices + +open 2Choice using (_⟨_,_⟩) +open Choice using (_⟨_⟩) {-| ConfContract and FnocContract define the requirements we have on translated configurations @@ -31,13 +30,13 @@ To simplify things, we fix these two numbers to be 0 for true, and 1 for false. `D < l , r >` lines up with `D < l :: r :: [] >` -} -record ConfContract (f : Q) (conf : Config₂ Q → Configₙ Q) : Set where +record ConfContract (f : Q) (conf : 2Choice.Config Q → Choice.Config Q) : Set where field - false→1 : ∀ (c : Config₂ Q) + false→1 : ∀ (c : 2Choice.Config Q) → c f ≡ false → (conf c) f ≡ 1 - true→0 : ∀ (c : Config₂ Q) + true→0 : ∀ (c : 2Choice.Config Q) → c f ≡ true → (conf c) f ≡ 0 open ConfContract @@ -51,23 +50,23 @@ that we can associate each natural numbers with the boolean values true and fals such that the association is inverse to ConfContract. Hence, we associate 0 with true and all other numbers with false. -} -record FnocContract (f : Q) (fnoc : Configₙ Q → Config₂ Q) : Set where +record FnocContract (f : Q) (fnoc : Choice.Config Q → 2Choice.Config Q) : Set where field - suc→false : ∀ {n} (c : Configₙ Q) + suc→false : ∀ {n} (c : Choice.Config Q) → c f ≡ suc n → (fnoc c) f ≡ false - zero→true : ∀ (c : Configₙ Q) + zero→true : ∀ (c : Choice.Config Q) → c f ≡ zero → (fnoc c) f ≡ true open FnocContract -default-conf : Config₂ Q → Configₙ Q +default-conf : 2Choice.Config Q → Choice.Config Q default-conf cb f with cb f ... | false = 1 ... | true = 0 -default-fnoc : Configₙ Q → Config₂ Q +default-fnoc : Choice.Config Q → 2Choice.Config Q default-fnoc cn f with cn f ... | zero = true ... | (suc _) = false @@ -88,34 +87,34 @@ module Translate (S : Setoid 0ℓ 0ℓ) where -- However, that might not be possible because it would require to abstract -- arbitrary requirements on the configuration compiler. -- Maybe this could be done via type parameters but lets see whether it pays off. - convert : 2Choice Q Carrier → NChoice Q Carrier + convert : 2Choice.Syntax Q Carrier → Choice.Syntax Q Carrier convert (D ⟨ l , r ⟩) = D ⟨ l ∷ r ∷ [] ⟩ module Preservation - (conf : Config₂ Q → Configₙ Q) - (fnoc : Configₙ Q → Config₂ Q) - (chc : 2Choice Q Carrier) + (conf : 2Choice.Config Q → Choice.Config Q) + (fnoc : Choice.Config Q → 2Choice.Config Q) + (chc : 2Choice.Syntax Q Carrier) where open Data.IndexedSet S using (_⊆[_]_; _≅[_][_]_; _≅_) preserves-conf : - ConfContract (2Choice.dim chc) conf - → ⟦ chc ⟧₂ ⊆[ conf ] ⟦ convert chc ⟧ₙ - preserves-conf conv c with c (2Choice.dim chc) in eq + ConfContract (2Choice.Syntax.dim chc) conf + → 2Choice.⟦ chc ⟧ ⊆[ conf ] Choice.⟦ convert chc ⟧ + preserves-conf conv c with c (2Choice.Syntax.dim chc) in eq ... | false rewrite false→1 conv c eq = ≈-Eq.refl ... | true rewrite true→0 conv c eq = ≈-Eq.refl preserves-fnoc : - FnocContract (2Choice.dim chc) fnoc - → ⟦ convert chc ⟧ₙ ⊆[ fnoc ] ⟦ chc ⟧₂ - preserves-fnoc vnoc c with c (2Choice.dim chc) in eq + FnocContract (2Choice.Syntax.dim chc) fnoc + → Choice.⟦ convert chc ⟧ ⊆[ fnoc ] 2Choice.⟦ chc ⟧ + preserves-fnoc vnoc c with c (2Choice.Syntax.dim chc) in eq ... | zero rewrite zero→true vnoc c eq = ≈-Eq.refl ... | suc _ rewrite suc→false vnoc c eq = ≈-Eq.refl convert-preserves : - ConfContract (2Choice.dim chc) conf - → FnocContract (2Choice.dim chc) fnoc - → ⟦ chc ⟧₂ ≅[ conf ][ fnoc ] ⟦ convert chc ⟧ₙ + ConfContract (2Choice.Syntax.dim chc) conf + → FnocContract (2Choice.Syntax.dim chc) fnoc + → 2Choice.⟦ chc ⟧ ≅[ conf ][ fnoc ] Choice.⟦ convert chc ⟧ convert-preserves conv vnoc = preserves-conf conv and preserves-fnoc vnoc -- compiler : ∀ (F : 𝔽) → ConstructCompiler (C₂ F) (Cₙ F) diff --git a/src/Translation/Construct/2Choice-to-NChoice-VL.agda b/src/Translation/Construct/2Choice-to-NChoice-VL.agda deleted file mode 100644 index 13c05156..00000000 --- a/src/Translation/Construct/2Choice-to-NChoice-VL.agda +++ /dev/null @@ -1,135 +0,0 @@ -open import Framework.Definitions - -module Translation.Construct.2Choice-to-NChoice-VL where - -open import Data.Bool using (Bool) -open import Data.Nat using (ℕ) -open import Data.Product using (proj₁; proj₂) -open import Function using (_∘_) - --- open import Relation.Binary using (Setoid; IsEquivalence) -open import Relation.Binary.PropositionalEquality as Eq using (_≗_; refl) - -import Data.IndexedSet - -open import Framework.VariabilityLanguage -open import Framework.Construct -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Relation.Function using (to-is-Embedding) - -import Translation.Construct.2Choice-to-NChoice as 2→N -open 2→N using (ConfContract; FnocContract) - -open import Construct.Choices as Chc -open Chc.Choice₂ using (_⟨_,_⟩) renaming (Config to Config₂; map to map₂) -open Chc.Choiceₙ using () renaming (Config to Configₙ; map to mapₙ) - -module Translate {Q : 𝔽} {V : 𝕍} {A : 𝔸} - (Γ₁ Γ₂ : VariabilityLanguage V) - (extract₁ : Compatible (Chc.VLChoice₂.Construct V Q) Γ₁) - (t : LanguageCompiler Γ₁ Γ₂) - (confi : Config₂ Q → Configₙ Q) - (fnoci : Configₙ Q → Config₂ Q) - where - private - L₁ = Expression Γ₁ - ⟦_⟧₁ = Semantics Γ₁ - L₂ = Expression Γ₂ - ⟦_⟧₂ = Semantics Γ₂ - open LanguageCompiler t - - open VariabilityConstruct (Chc.VLChoice₂.Construct V Q) using () - renaming (VSyntax to 2Choice; VSemantics to Sem₂) - open VariabilityConstruct (Chc.VLChoiceₙ.Construct V Q) using () - renaming (VSyntax to NChoice; VSemantics to Semₙ) - - -- TODO: Generalize to any setoids over L₁ or L₂. - module 2→N-T₁ = 2→N.Translate {Q} (Eq.setoid (L₁ A)) - open 2→N-T₁ using () renaming (convert to convert₁) - module 2→N-T₂ = 2→N.Translate {Q} (Eq.setoid (L₂ A)) - open 2→N-T₂ using () renaming (convert to convert₂) - - {-| - Composition of two compilers: - First, we convert all alternatives from one language to another using `map₂ compile`. - Second, we convert the binary choice to an n-ary choice via convert, not changing any data. - The order of these steps does not matter, as proven by `convert-comm` below. - -} - compile-convert : 2Choice L₁ A → NChoice L₂ A - compile-convert = convert₂ ∘ map₂ compile - - {-| - The same compiler as compile-convert, but the steps are executed in the other order. - -} - convert-compile : 2Choice L₁ A → NChoice L₂ A - convert-compile = mapₙ compile ∘ convert₁ - - {-| - Proof that the following square commutes. - This means that it does not matter in which order we - - convert a binary to an n-ary choice, - - compile subterms. - - Algebraically: - mapₙ compile ∘ convert ≗ convert ∘ map₂ compile - - Graphically: - binary L₁ ── convert ──→ nary L₁ - | | - | map₂ compile | mapₙ compile - ↓ ↓ - binary L₂ ── convert ──→ nary L₂ - -} - convert-comm : convert-compile ≗ compile-convert - convert-comm _ = refl - - module Preservation - (D : Q) - (l r : L₁ A) - where - open 2→N-T₂.Preservation confi fnoci using (convert-preserves) - - open import Data.EqIndexedSet as ISet - open ISet.≅[]-Reasoning - - extract₂ : Compatible (Chc.VLChoiceₙ.Construct V Q) Γ₂ - extract₂ = confi ∘ extract₁ ∘ fnoc -- proof by diagram chasing - - convert-compile-preserves : - ∀ (conv : ConfContract D confi) - → (vnoc : FnocContract D fnoci) - → to-is-Embedding config-compiler - → Sem₂ Γ₁ extract₁ (D ⟨ l , r ⟩) - ≅[ conf ][ fnoc ] - Semₙ Γ₂ extract₂ (convert-compile (D ⟨ l , r ⟩)) - convert-compile-preserves conv vnoc stable = - ≅[]-begin - (Sem₂ Γ₁ extract₁ (D ⟨ l , r ⟩)) - ≅[]⟨⟩ - (λ c → ⟦ Choice₂.Standard-Semantics (D ⟨ l , r ⟩) (extract₁ c) ⟧₁ c) - ≅[]⟨ VLChoice₂.map-compile-preserves Γ₁ Γ₂ extract₁ t (D ⟨ l , r ⟩) stable ⟩ - (λ c → ⟦ Choice₂.Standard-Semantics (map₂ compile (D ⟨ l , r ⟩)) (extract₁ (fnoc c)) ⟧₂ c) - ≐[ c ]⟨ Eq.cong (λ x → ⟦ x ⟧₂ c) - (proj₁ (convert-preserves (map₂ compile (D ⟨ l , r ⟩)) conv vnoc) (extract₁ (fnoc (c))) )⟩ - (λ c → ⟦ Choiceₙ.Standard-Semantics (convert₂ (map₂ compile (D ⟨ l , r ⟩))) (extract₂ c) ⟧₂ c) - ≅[]⟨⟩ - (Semₙ Γ₂ extract₂ (convert₂ (map₂ compile (D ⟨ l , r ⟩)))) - ≅[]⟨⟩ - (Semₙ Γ₂ extract₂ (convert-compile (D ⟨ l , r ⟩))) - ≅[]-∎ - - compile-convert-preserves : - ∀ (conv : ConfContract D confi) - → (vnoc : FnocContract D fnoci) - → to-is-Embedding config-compiler - → Sem₂ Γ₁ extract₁ (D ⟨ l , r ⟩) - ≅[ conf ][ fnoc ] - Semₙ Γ₂ extract₂ (compile-convert (D ⟨ l , r ⟩)) - compile-convert-preserves conv vnoc stable = - ≅[]-begin - Sem₂ Γ₁ extract₁ (D ⟨ l , r ⟩) - ≅[]⟨ convert-compile-preserves conv vnoc stable ⟩ - Semₙ Γ₂ extract₂ (convert-compile (D ⟨ l , r ⟩)) - ≐[ c ]⟨ Eq.cong (λ eq → ⟦ Choiceₙ.Standard-Semantics eq (extract₂ c) ⟧₂ c) (convert-comm (D ⟨ l , r ⟩)) ⟩ - Semₙ Γ₂ extract₂ (compile-convert (D ⟨ l , r ⟩)) - ≅[]-∎ diff --git a/src/Translation/Construct/NChoice-to-2Choice.agda b/src/Translation/Construct/Choice-to-2Choice.agda similarity index 92% rename from src/Translation/Construct/NChoice-to-2Choice.agda rename to src/Translation/Construct/Choice-to-2Choice.agda index f7c1db87..d0800f80 100644 --- a/src/Translation/Construct/NChoice-to-2Choice.agda +++ b/src/Translation/Construct/Choice-to-2Choice.agda @@ -1,5 +1,5 @@ {-# OPTIONS --sized-types #-} -module Translation.Construct.NChoice-to-2Choice {Q : Set} where +module Translation.Construct.Choice-to-2Choice {Q : Set} where open import Data.Bool using (Bool; false; true) renaming (_≟_ to _≟ᵇ_) open import Data.List using (List; _∷_; []) @@ -24,9 +24,10 @@ open import Relation.Binary using (Setoid; IsEquivalence) open import Util.AuxProofs using (true≢false; n≡ᵇn; n_) -exp : Experiment (NChoice String ℕ) +exp : Experiment (Choice.Syntax String ℕ) getName exp = "Check N → 2 Choice trans" get exp (name ≔ e) = do let open Trans (Eq.setoid ℕ) using (convert; show-nested-choice) - > name <+> "=" <+> show-nchoice id show-ℕ e + > name <+> "=" <+> Choice.show id show-ℕ e > phantom name <+> "⇝" <+> show-nested-choice id show-ℕ (convert e) -un-ex : Example (NChoice String ℕ) +un-ex : Example (Choice.Syntax String ℕ) un-ex = "e₁" ≔ "D" ⟨ 0 ∷ [] ⟩ -bi-ex : Example (NChoice String ℕ) +bi-ex : Example (Choice.Syntax String ℕ) bi-ex = "e₂" ≔ "D" ⟨ 0 ∷ 1 ∷ [] ⟩ -tri-ex : Example (NChoice String ℕ) +tri-ex : Example (Choice.Syntax String ℕ) tri-ex = "e₃" ≔ "D" ⟨ 0 ∷ 1 ∷ 2 ∷ [] ⟩ -many-ex : Example (NChoice String ℕ) +many-ex : Example (Choice.Syntax String ℕ) many-ex = "e₄" ≔ "D" ⟨ 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ 8 ∷ [] ⟩ -all-ex : List (Example (NChoice String ℕ)) +all-ex : List (Example (Choice.Syntax String ℕ)) all-ex = un-ex ∷ bi-ex ∷ tri-ex ∷ many-ex ∷ [] diff --git a/src/Translation/Lang/2ADT-to-NADT.agda b/src/Translation/Lang/2ADT-to-NADT.agda index 1dd20fc3..7c53cd96 100644 --- a/src/Translation/Lang/2ADT-to-NADT.agda +++ b/src/Translation/Lang/2ADT-to-NADT.agda @@ -12,25 +12,25 @@ open Eq.≡-Reasoning import Data.IndexedSet -import Construct.Choices -open Construct.Choices.Choiceₙ renaming (map to mapₙ) +open import Construct.Choices +open import Construct.NestedChoice using (value; choice) open import Framework.Variants using (GrulerVariant) open import Lang.2ADT open import Lang.NADT -import Translation.Construct.2Choice-to-NChoice {F} as 2→N -open 2→N.Translate using (convert) +import Translation.Construct.2Choice-to-Choice {F} as 2Choice-to-Choice +open 2Choice-to-Choice.Translate using (convert) compile : ∀ {i} → 2ADT F i A → NADT F i A compile (value a) = NADTAsset a -compile (choice {i} c) = NADTChoice (mapₙ compile (convert (Eq.setoid (2ADT F i A)) c)) +compile (choice {i} c) = NADTChoice (Choice.map compile (convert (Eq.setoid (2ADT F i A)) c)) module Preservation where -- open Data.IndexedSet (VariantSetoid GrulerVariant A) using () renaming (_≅_ to _≋_) -- TODO: Prove Preservation of compile - -- open 2→N.Translate.Preservation 2ADTVL NADTVL compile conf' fnoc' using (preserves-conf; preserves-fnoc) + -- open 2Choice-to-Choice.Translate.Preservation 2ADTVL NADTVL compile conf' fnoc' using (preserves-conf; preserves-fnoc) -- preserves-l : ∀ (e : 2ADT A) → Conf-Preserves 2ADTVL NADTVL e (compile e) conf' -- preserves-l (value _) _ = refl diff --git a/src/Translation/Lang/2CC-to-2CC.agda b/src/Translation/Lang/2CC-to-2CC.agda new file mode 100644 index 00000000..6ff51170 --- /dev/null +++ b/src/Translation/Lang/2CC-to-2CC.agda @@ -0,0 +1,138 @@ +{-# OPTIONS --sized-types #-} + +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 + +open import Data.Bool using (if_then_else_) +open import Data.Bool.Properties as Bool +import Data.EqIndexedSet as IndexedSet +open import Data.List as List using (List) +import Data.List.Properties as List +open import Data.Product using () renaming (_,_ to _and_) +open import Framework.Compiler using (LanguageCompiler) +open import Framework.Definitions using (𝔸; 𝔽) +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 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; _-<_>-; _⟨_,_⟩) + + +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 : 𝔸} + → (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 ⟩ + +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 ⟧ +preserves-⊆ f f⁻¹ (a -< cs >-) config = + 2CC.⟦ map-dim f (a -< cs >-) ⟧ config + ≡⟨⟩ + 2CC.⟦ a -< List.map (map-dim f) cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) (List.map (map-dim f) cs)) + ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → 2CC.⟦ map-dim 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.⟦ f d ⟨ map-dim f l , map-dim 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 + ≡⟨ preserves-⊆ f f⁻¹ (if config (f d) then l else r) config ⟩ + 2CC.⟦ if config (f d) then l else r ⟧ (config ∘ f) + ≡⟨⟩ + 2CC.⟦ if config (f d) then l else r ⟧ (config ∘ f) + ≡⟨⟩ + 2CC.⟦ d ⟨ l , r ⟩ ⟧ (config ∘ f) + ∎ + +preserves-⊇ : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸} + → (f : D₁ → D₂) + → (f⁻¹ : D₂ → D₁) + → f⁻¹ ∘ f ≗ id + → (expr : 2CC D₁ i A) + → 2CC.⟦ expr ⟧ ⊆[ 2CC-map-config f⁻¹ ] 2CC.⟦ map-dim 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) + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → 2CC.⟦ e ⟧ (config ∘ f⁻¹)) (List.map (map-dim f) cs)) + ≡⟨⟩ + 2CC.⟦ a -< List.map (map-dim f) cs >- ⟧ (config ∘ f⁻¹) + ≡⟨⟩ + 2CC.⟦ map-dim f (a -< cs >-) ⟧ (config ∘ f⁻¹) + ∎ +preserves-⊇ f f⁻¹ is-inverse (d ⟨ l , r ⟩) config = + 2CC.⟦ d ⟨ l , r ⟩ ⟧ config + ≡⟨⟩ + 2CC.⟦ if config d then l else 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.⟦ f d ⟨ map-dim f l , map-dim f r ⟩ ⟧ (config ∘ f⁻¹) + ≡⟨⟩ + 2CC.⟦ map-dim 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 ⟧ +preserves f f⁻¹ is-inverse expr = preserves-⊆ f f⁻¹ expr and preserves-⊇ f f⁻¹ is-inverse expr + +2CC-map-dim : ∀ {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) diff --git a/src/Translation/Lang/2CC-to-CCC.agda b/src/Translation/Lang/2CC-to-CCC.agda new file mode 100644 index 00000000..22c6ba2e --- /dev/null +++ b/src/Translation/Lang/2CC-to-CCC.agda @@ -0,0 +1,32 @@ +{-# OPTIONS --sized-types #-} + +open import Framework.Construct using (_∈ₛ_) +open import Construct.Artifact using () renaming (Syntax to Artifact) + +module Translation.Lang.2CC-to-CCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where + +open import Data.Nat using (zero) +open import Framework.Compiler using (LanguageCompiler; _⊕_) +open import Framework.Definitions using (𝔽) +open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_) +open import Size using (Size) +open import Util.Nat.AtLeast using (sucs) + +import Lang.CCC +module CCC D = Lang.CCC.Sem D Variant Artifact∈ₛVariant +open CCC using (CCCL) + +import Lang.2CC +module 2CC D = Lang.2CC.Sem D Variant Artifact∈ₛVariant +open 2CC using (2CCL) + +import Translation.Lang.2CC-to-NCC +open Translation.Lang.2CC-to-NCC.2Ary Variant Artifact∈ₛVariant using (2CC→NCC) +open import Translation.Lang.NCC-to-CCC Variant Artifact∈ₛVariant using (NCC→CCC) + + +2CC→CCC : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (2CCL D {i}) (CCCL D) +2CC→CCC = 2CC→NCC ⊕ NCC→CCC (sucs zero) + +CCC≽2CC : ∀ {D : 𝔽} → CCCL D ≽ 2CCL D +CCC≽2CC = expressiveness-from-compiler 2CC→CCC diff --git a/src/Translation/Lang/2CC-to-NCC.agda b/src/Translation/Lang/2CC-to-NCC.agda new file mode 100644 index 00000000..2feef894 --- /dev/null +++ b/src/Translation/Lang/2CC-to-NCC.agda @@ -0,0 +1,164 @@ +{-# 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-NCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where + +open import Data.Bool using (true; false; if_then_else_) +open import Data.Bool.Properties as Bool +import Data.EqIndexedSet as IndexedSet +open import Data.Fin using (zero; suc) +open import Data.List as List using (List) +import Data.List.Properties as List +open import Data.Nat using (zero) +open import Data.Product using () renaming (_,_ to _and_) +open import Data.Vec as Vec using (Vec; []; _∷_) +import Data.Vec.Properties as Vec +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 Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) +open import Size using (Size) +open import Util.Nat.AtLeast using (ℕ≥; sucs) + +open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) + +import Lang.NCC +module NCC where + open Lang.NCC public + module NCC-Sem-1 n D = Lang.NCC.Sem n D Variant Artifact∈ₛVariant + open NCC-Sem-1 using (NCCL) public + module NCC-Sem-2 {n} {D} = Lang.NCC.Sem n D Variant Artifact∈ₛVariant + open NCC-Sem-2 using (⟦_⟧) public +open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) + +import Lang.2CC +module 2CC where + open Lang.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 Translation.Lang.NCC-to-NCC +open Translation.Lang.NCC-to-NCC.IncreaseArity Variant Artifact∈ₛVariant using (NCC→NCC) + +artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A +artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs) + + +module 2Ary where + translate : ∀ {i : Size} {D : 𝔽} {A : 𝔽} + → 2CC D i A + → NCC (sucs zero) D i A + translate (a -< cs >-) = a -< List.map translate cs >- + translate (d ⟨ l , r ⟩) = d ⟨ translate l ∷ translate r ∷ [] ⟩ + + conf : ∀ {D : Set} → 2CC.Configuration D → NCC.Configuration (sucs zero) D + conf config d with config d + ... | true = zero + ... | false = suc zero + + fnoc : ∀ {D : Set} → NCC.Configuration (sucs zero) D → 2CC.Configuration D + fnoc config d with config d + ... | zero = true + ... | suc zero = false + + preserves-⊆ : ∀ {i : Size} {D : 𝔽} {A : 𝔽} + → (expr : 2CC D i A) + → NCC.⟦ translate expr ⟧ ⊆[ fnoc ] 2CC.⟦ expr ⟧ + preserves-⊆ (a -< cs >-) config = + NCC.⟦ translate (a -< cs >-) ⟧ config + ≡⟨⟩ + NCC.⟦ a -< List.map translate cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ config) (List.map translate cs)) + ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ translate e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ e config) cs) ⟩ + artifact a (List.map (λ e → 2CC.⟦ e ⟧ (fnoc config)) cs) + ≡⟨⟩ + 2CC.⟦ a -< cs >- ⟧ (fnoc config) + ∎ + preserves-⊆ (d ⟨ l , r ⟩) config = + NCC.⟦ translate (d ⟨ l , r ⟩) ⟧ config + ≡⟨⟩ + NCC.⟦ d ⟨ translate l ∷ translate r ∷ [] ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup (translate l ∷ translate r ∷ []) (config d) ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (config d) translate (l ∷ r ∷ [])) refl ⟩ + NCC.⟦ translate (Vec.lookup (l ∷ r ∷ []) (config d)) ⟧ config + ≡⟨ preserves-⊆ (Vec.lookup (l ∷ r ∷ []) (config d)) config ⟩ + 2CC.⟦ Vec.lookup (l ∷ r ∷ []) (config d) ⟧ (fnoc config) + ≡⟨ Eq.cong₂ 2CC.⟦_⟧ lemma refl ⟩ + 2CC.⟦ if (fnoc config d) then l else r ⟧ (fnoc config) + ≡⟨⟩ + 2CC.⟦ d ⟨ l , r ⟩ ⟧ (fnoc config) + ∎ + where + lemma : {A : Set} → {a b : A} → Vec.lookup (a ∷ b ∷ []) (config d) ≡ (if fnoc config d then a else b) + lemma with config d + ... | zero = refl + ... | suc zero = refl + + preserves-⊇ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (expr : 2CC D i A) + → 2CC.⟦ expr ⟧ ⊆[ conf ] NCC.⟦ translate expr ⟧ + preserves-⊇ (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-⊇ e config) cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ translate e ⟧ (conf config)) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ (conf config)) (List.map translate cs)) + ≡⟨⟩ + NCC.⟦ a -< List.map translate cs >- ⟧ (conf config) + ≡⟨⟩ + NCC.⟦ translate (a -< cs >-) ⟧ (conf config) + ∎ + preserves-⊇ (d ⟨ l , r ⟩) config = + 2CC.⟦ d ⟨ l , r ⟩ ⟧ config + ≡⟨⟩ + 2CC.⟦ if config d then l else r ⟧ config + ≡⟨⟩ + 2CC.⟦ if config d then l else r ⟧ config + ≡⟨ preserves-⊇ (if config d then l else r) config ⟩ + NCC.⟦ translate (if config d then l else r) ⟧ (conf config) + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Bool.push-function-into-if (translate) (config d)) refl ⟩ + NCC.⟦ if config d then translate l else translate r ⟧ (conf config) + ≡⟨ Eq.cong₂ NCC.⟦_⟧ lemma refl ⟩ + NCC.⟦ Vec.lookup (translate l ∷ translate r ∷ []) (conf config d) ⟧ (conf config) + ≡⟨⟩ + NCC.⟦ d ⟨ translate l ∷ translate r ∷ [] ⟩ ⟧ (conf config) + ≡⟨⟩ + NCC.⟦ translate (d ⟨ l , r ⟩) ⟧ (conf config) + ∎ + where + lemma : {A : Set} → {a b : A} → (if config d then a else b) ≡ Vec.lookup (a ∷ b ∷ []) (conf config d) + lemma with config d + ... | true = refl + ... | false = refl + + preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (e : 2CC D i A) + → NCC.⟦ translate e ⟧ ≅[ fnoc ][ conf ] 2CC.⟦ e ⟧ + preserves expr = preserves-⊆ expr and preserves-⊇ expr + + 2CC→NCC : ∀ {i : Size} {D : Set} → LanguageCompiler (2CCL D {i}) (NCCL (sucs zero) D {i}) + 2CC→NCC .LanguageCompiler.compile = translate + 2CC→NCC .LanguageCompiler.config-compiler expr .to = conf + 2CC→NCC .LanguageCompiler.config-compiler expr .from = fnoc + 2CC→NCC .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr) + + +-- 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 + +NCC≽2CC : ∀ {D : Set} → (n : ℕ≥ 2) → NCCL n D ≽ 2CCL D +NCC≽2CC n = expressiveness-from-compiler (2CC→NCC n) diff --git a/src/Translation/Lang/CCC-to-2CC.agda b/src/Translation/Lang/CCC-to-2CC.agda new file mode 100644 index 00000000..76aaeeba --- /dev/null +++ b/src/Translation/Lang/CCC-to-2CC.agda @@ -0,0 +1,33 @@ +{-# OPTIONS --sized-types #-} + +open import Framework.Construct using (_∈ₛ_) +open import Construct.Artifact as At using () renaming (Syntax to Artifact) + +module Translation.Lang.CCC-to-2CC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where + +open import Data.Nat using (ℕ; zero) +open import Data.Product using (_×_) +open import Framework.Compiler using (LanguageCompiler; _⊕_) +open import Framework.Definitions using (𝔽) +open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_) +open import Size using (Size) +open import Util.Nat.AtLeast using (sucs) + +import Lang.CCC +module CCC-Sem D = Lang.CCC.Sem D Variant Artifact∈ₛVariant +open CCC-Sem using (CCCL) + +import Lang.2CC +module 2CC-Sem D = Lang.2CC.Sem D Variant Artifact∈ₛVariant +open 2CC-Sem using (2CCL) + +open import Translation.Lang.CCC-to-NCC Variant Artifact∈ₛVariant using (CCC→NCC) +import Translation.Lang.NCC-to-2CC +open Translation.Lang.NCC-to-2CC.2Ary Variant Artifact∈ₛVariant using (NCC→2CC) + + +CCC→2CC : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (CCCL D {i}) (2CCL (D × ℕ)) +CCC→2CC = CCC→NCC (sucs zero) ⊕ NCC→2CC + +2CC≽CCC : ∀ {D : 𝔽} → 2CCL (D × ℕ) ≽ CCCL D +2CC≽CCC = expressiveness-from-compiler CCC→2CC diff --git a/src/Translation/Lang/CCC-to-NCC.agda b/src/Translation/Lang/CCC-to-NCC.agda new file mode 100644 index 00000000..e8b1ca62 --- /dev/null +++ b/src/Translation/Lang/CCC-to-NCC.agda @@ -0,0 +1,396 @@ +{-# 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.CCC-to-NCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where + +import Data.EqIndexedSet as IndexedSet +open import Data.Fin as Fin using (Fin) +open import Data.List as List using (List; []; _∷_) +open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_) +open import Data.Nat using (ℕ; zero; suc; _≤_; s≤s) +open import Data.Nat.Properties as ℕ using (≤-reflexive; ≤-trans) +open import Data.Product using (_×_; _,_) +open import Data.Vec as Vec using (Vec; []; _∷_) +import Data.Vec.Properties as Vec +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 import Util.List using (find-or-last; map-find-or-last; find-or-last⇒lookup) +open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs; _⊔_) +import Util.Vec as Vec + +open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) +open IndexedSet.≅[]-Reasoning using (step-≅[]; step-≅[]˘; _≅[]⟨⟩_; _≅[]-∎) + +import Lang.CCC +module CCC where + open Lang.CCC public + module CCC-Sem-1 D = Lang.CCC.Sem D Variant Artifact∈ₛVariant + open CCC-Sem-1 using (CCCL) public + module CCC-Sem-2 {D} = Lang.CCC.Sem D Variant Artifact∈ₛVariant + open CCC-Sem-2 using (⟦_⟧) public +open CCC using (CCC; CCCL; _-<_>-; _⟨_⟩) + +import Lang.NCC +module NCC where + open Lang.NCC public + module NCC-Sem-1 n D = Lang.NCC.Sem n D Variant Artifact∈ₛVariant + open NCC-Sem-1 using (NCCL) public + module NCC-Sem-2 {n} {D} = Lang.NCC.Sem n D Variant Artifact∈ₛVariant + 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) +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. + -- The saturated semantics of `CCC` (see `find-or-last`) ensures that, by reusing the last element, the semantic of the expression doesn't change. + -- Such a saturated `CCC` expression can then be translated into a `NCC` expression by converting the alternative lists into vectors. + -- However, the arity of the `NCC` language is the length of these vectors, which depends on the length of the alternative lists in the unsaturated `CCC` expression. + -- Hence, we need to calculate the maximum choice length (`⌈_⌉`) and a proof (`NumberOfAlternatives≤`) that all choice lengths are smaller than that (`numberOfAlternatives≤⌈_⌉`). + + maximum : List (ℕ≥ 2) → ℕ≥ 2 + maximum [] = sucs zero + maximum (n ∷ ns) = n ⊔ maximum ns + + maximum⁺ : List⁺ (ℕ≥ 2) → ℕ≥ 2 + maximum⁺ (n ∷ ns) = maximum (n ∷ ns) + + -- Calculcates the `maximum number of alternatives ⊔ 2`. + -- 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 + ⌈ d ⟨ c₁ ∷ c₂ ∷ cs ⟩ ⌉ = sucs (List.length cs) ⊔ maximum⁺ (List⁺.map ⌈_⌉ (c₁ ∷ c₂ ∷ cs)) + + mutual + -- A proof that an expression's longest alternative list is at maximum `n`. + data NumberOfAlternatives≤ {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → CCC D i A → Set where + maxArtifact : {i : Size} → {a : A} → {cs : List (CCC D i A)} → NumberOfAlternatives≤-List n {i} cs → NumberOfAlternatives≤ n {↑ i} (a -< cs >-) + maxChoice : {i : Size} → {d : D} → {cs : List⁺ (CCC D i A)} → List⁺.length cs ≤ ℕ≥.toℕ n → NumberOfAlternatives≤-List⁺ n {i} cs → NumberOfAlternatives≤ n {↑ i} (d ⟨ cs ⟩) + + data NumberOfAlternatives≤-List {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → List (CCC D i A) → Set where + [] : {i : Size} → NumberOfAlternatives≤-List n {i} [] + _∷_ : {i : Size} → {c : CCC D i A} → {cs : List (CCC D i A)} → NumberOfAlternatives≤ n {i} c → NumberOfAlternatives≤-List n {i} cs → NumberOfAlternatives≤-List n {i} (c ∷ cs) + + data NumberOfAlternatives≤-List⁺ {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → List⁺ (CCC D i A) → Set where + _∷_ : {i : Size} → {c : CCC D i A} → {cs : List (CCC D i A)} → NumberOfAlternatives≤ n {i} c → NumberOfAlternatives≤-List n {i} cs → NumberOfAlternatives≤-List⁺ n {i} (c ∷ cs) + + mutual + NumberOfAlternatives≤-respects-≤ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {cs : CCC D i A} {n₁ n₂ : ℕ≥ 2} + → n₁ ℕ≥.≤ n₂ + → NumberOfAlternatives≤ n₁ cs + → NumberOfAlternatives≤ n₂ cs + NumberOfAlternatives≤-respects-≤ n₁≤n₂ (maxArtifact max-cs) = maxArtifact (NumberOfAlternatives≤-List-respects-≤ n₁≤n₂ max-cs) + NumberOfAlternatives≤-respects-≤ {cs = d ⟨ cs ⟩} {n₁ = n₁} {n₂ = n₂} n₁≤n₂ (maxChoice max-cs≤n max-cs) = maxChoice (≤-trans max-cs≤n n₁≤n₂) (NumberOfAlternatives≤-List⁺-respects-≤ n₁≤n₂ max-cs) + + NumberOfAlternatives≤-List-respects-≤ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {cs : List (CCC D i A)} {n₁ n₂ : ℕ≥ 2} + → n₁ ℕ≥.≤ n₂ + → NumberOfAlternatives≤-List n₁ cs + → NumberOfAlternatives≤-List n₂ cs + NumberOfAlternatives≤-List-respects-≤ n₁≤n₂ [] = [] + NumberOfAlternatives≤-List-respects-≤ n₁≤n₂ (c ∷ cs) = NumberOfAlternatives≤-respects-≤ n₁≤n₂ c ∷ NumberOfAlternatives≤-List-respects-≤ n₁≤n₂ cs + + NumberOfAlternatives≤-List⁺-respects-≤ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {cs : List⁺ (CCC D i A)} {n₁ n₂ : ℕ≥ 2} + → n₁ ℕ≥.≤ n₂ + → NumberOfAlternatives≤-List⁺ n₁ cs + → NumberOfAlternatives≤-List⁺ n₂ cs + NumberOfAlternatives≤-List⁺-respects-≤ n₁≤n₂ (c ∷ cs) = NumberOfAlternatives≤-respects-≤ n₁≤n₂ c ∷ NumberOfAlternatives≤-List-respects-≤ n₁≤n₂ cs + + mutual + -- Proof that `⌈_⌉` calculates a correct choice lenght limit. + numberOfAlternatives≤⌈_⌉ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (expr : CCC D i A) + → NumberOfAlternatives≤ ⌈ expr ⌉ expr + numberOfAlternatives≤⌈_⌉ (a -< cs >-) = maxArtifact (numberOfAlternatives≤⌈_⌉-List cs) + numberOfAlternatives≤⌈_⌉ (d ⟨ c ∷ [] ⟩) = maxChoice (≤-trans (ℕ.n≤1+n 1) (ℕ≥.≤-toℕ ⌈ c ⌉)) (numberOfAlternatives≤⌈_⌉ c ∷ []) + numberOfAlternatives≤⌈_⌉ (d ⟨ c₁ ∷ c₂ ∷ cs ⟩) = maxChoice (ℕ≥.m≤m⊔n (sucs (List.length cs)) (maximum⁺ (List⁺.map ⌈_⌉ (c₁ ∷ c₂ ∷ cs)))) (NumberOfAlternatives≤-List⁺-respects-≤ (ℕ≥.m≤n⊔m (sucs (List.length cs)) (maximum⁺ (List⁺.map ⌈_⌉ (c₁ ∷ c₂ ∷ cs)))) (numberOfAlternatives≤⌈_⌉-List⁺ (c₁ ∷ c₂ ∷ cs))) + + numberOfAlternatives≤⌈_⌉-List : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (cs : List (CCC D i A)) + → NumberOfAlternatives≤-List (maximum (List.map ⌈_⌉ cs)) cs + numberOfAlternatives≤⌈_⌉-List [] = [] + numberOfAlternatives≤⌈_⌉-List (c ∷ cs) = NumberOfAlternatives≤-respects-≤ (ℕ≥.m≤m⊔n ⌈ c ⌉ (maximum (List.map ⌈_⌉ cs))) (numberOfAlternatives≤⌈_⌉ c) ∷ NumberOfAlternatives≤-List-respects-≤ (ℕ≥.m≤n⊔m ⌈ c ⌉ (maximum (List.map ⌈_⌉ cs))) (numberOfAlternatives≤⌈_⌉-List cs) + + numberOfAlternatives≤⌈_⌉-List⁺ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (cs : List⁺ (CCC D i A)) + → NumberOfAlternatives≤-List⁺ (maximum⁺ (List⁺.map ⌈_⌉ cs)) cs + numberOfAlternatives≤⌈_⌉-List⁺ (c ∷ cs) with numberOfAlternatives≤⌈_⌉-List (c ∷ cs) + ... | max-c ∷ max-cs = max-c ∷ max-cs + + mutual + translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (expr : CCC D i A) + → NumberOfAlternatives≤ n {i} expr + → NCC n D i A + translate n (a -< cs >-) (maxArtifact max-cs) = a -< zipWith n (translate n) cs max-cs >- + translate (sucs n) (d ⟨ c ∷ cs ⟩) (maxChoice max≤n (max-c ∷ max-cs)) = + d ⟨ Vec.saturate max≤n (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) ⟩ + + -- TODO Can probably be generalized + zipWith : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set} + → (n : ℕ≥ 2) + → ((expr : CCC D i A) → NumberOfAlternatives≤ n expr → Result) + → (cs : List (CCC D i A)) + → NumberOfAlternatives≤-List n cs + → List Result + zipWith n f [] [] = [] + zipWith n f (c ∷ cs) (max-c ∷ max-cs) = f c max-c ∷ zipWith n f cs max-cs + + length-zipWith : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set} + → (n : ℕ≥ 2) + → {f : (expr : CCC D i A) → NumberOfAlternatives≤ n expr → Result} + → (cs : List (CCC D i A)) + → (max-cs : NumberOfAlternatives≤-List n cs) + → List.length (zipWith {i} n f cs max-cs) ≡ List.length cs + length-zipWith n [] [] = refl + length-zipWith n (c ∷ cs) (max-c ∷ max-cs) = Eq.cong suc (length-zipWith n cs max-cs) + + map∘zipWith : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result₁ Result₂ : Set} + → (n : ℕ≥ 2) + → {g : Result₁ → Result₂} + → {f : (expr : CCC D i A) → NumberOfAlternatives≤ n expr → Result₁} + → (cs : List (CCC D i A)) + → (max-cs : NumberOfAlternatives≤-List n cs) + → List.map g (zipWith n f cs max-cs) ≡ zipWith n (λ e max-e → g (f e max-e)) cs max-cs + map∘zipWith n [] [] = refl + map∘zipWith n (c ∷ cs) (max-c ∷ max-cs) = Eq.cong₂ _∷_ refl (map∘zipWith n cs max-cs) + + zipWith-cong : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set} + → (n : ℕ≥ 2) + → {f g : (expr : CCC D i A) → NumberOfAlternatives≤ n expr → Result} + → ((e : CCC D i A) → (max-e : NumberOfAlternatives≤ n e) → f e max-e ≡ g e max-e) + → (cs : List (CCC D i A)) + → (max-cs : NumberOfAlternatives≤-List n cs) + → zipWith n f cs max-cs ≡ zipWith n g cs max-cs + zipWith-cong n f≗g [] [] = refl + zipWith-cong n f≗g (c ∷ cs) (max-c ∷ max-cs) = Eq.cong₂ _∷_ (f≗g c max-c) (zipWith-cong n f≗g cs max-cs) + + zipWith⇒map : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set} + → (n : ℕ≥ 2) + → (f : (expr : CCC D i A) → Result) + → (cs : List (CCC D i A)) + → (max-cs : NumberOfAlternatives≤-List n cs) + → zipWith n (λ e max-e → f e) cs max-cs ≡ List.map f cs + zipWith⇒map n f [] [] = refl + zipWith⇒map n f (c ∷ cs) (max-c ∷ max-cs) = Eq.cong₂ _∷_ refl (zipWith⇒map n f cs max-cs) + + + conf : ∀ {D : 𝔽} → (n : ℕ≥ 2) → CCC.Configuration D → NCC.Configuration n D + conf (sucs n) config d = ℕ≥.cappedFin (config d) + + fnoc : ∀ {D : 𝔽} → (n : ℕ≥ 2) → NCC.Configuration n D → CCC.Configuration D + fnoc n config d = Fin.toℕ (config d) + + preserves-⊆ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (expr : CCC D i A) + → (choiceLengthLimit : NumberOfAlternatives≤ n expr) + → NCC.⟦ translate n expr choiceLengthLimit ⟧ ⊆[ fnoc n ] CCC.⟦ expr ⟧ + preserves-⊆ n (a -< cs >-) (maxArtifact max-cs) config = + NCC.⟦ translate n (a -< cs >-) (maxArtifact max-cs) ⟧ config + ≡⟨⟩ + NCC.⟦ a -< zipWith n (translate n) cs max-cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ config) (zipWith n (translate n) cs max-cs)) + ≡⟨ Eq.cong₂ artifact refl (map∘zipWith n cs max-cs) ⟩ + artifact a (zipWith n (λ e max-e → NCC.⟦ translate n e max-e ⟧ config) cs max-cs) + ≡⟨ Eq.cong₂ artifact refl (zipWith-cong n (λ e max-e → preserves-⊆ n e max-e config) cs max-cs) ⟩ + artifact a (zipWith n (λ e max-e → CCC.⟦ e ⟧ (fnoc n config)) cs max-cs) + ≡⟨ Eq.cong₂ artifact refl (zipWith⇒map n (λ e → CCC.⟦ e ⟧ (fnoc n config)) cs max-cs) ⟩ + artifact a (List.map (λ e → CCC.⟦ e ⟧ (fnoc n config)) cs) + ≡⟨⟩ + CCC.⟦ a -< cs >- ⟧ (fnoc n config) + ∎ + preserves-⊆ (sucs n) (d ⟨ c ∷ cs ⟩) (maxChoice max≤n (max-c ∷ max-cs)) config = + NCC.⟦ translate (sucs n) (d ⟨ c ∷ cs ⟩) (maxChoice (max≤n) (max-c ∷ max-cs)) ⟧ config + ≡⟨⟩ + NCC.⟦ d ⟨ Vec.saturate max≤n (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup (Vec.saturate max≤n (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)))) (config d) ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate max≤n (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (config d)) refl ⟩ + NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (ℕ≥.cappedFin (Fin.toℕ (config d))) ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup (Vec.cast (Eq.cong suc (length-zipWith (sucs n) cs max-cs)) (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (ℕ≥.cappedFin (Fin.toℕ (config d))) ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-cast₁ (Eq.cong suc (length-zipWith (sucs n) cs max-cs)) (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (ℕ≥.cappedFin (Fin.toℕ (config d)))) refl ⟩ + NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (Fin.cast (Eq.sym (Eq.cong suc (length-zipWith (sucs n) cs max-cs))) (ℕ≥.cappedFin (Fin.toℕ (config d)))) ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)}) (ℕ≥.cast-cappedFin (Fin.toℕ (config d)) (Eq.sym (Eq.cong suc (length-zipWith (sucs n) cs max-cs))))) refl ⟩ + NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (ℕ≥.cappedFin (Fin.toℕ (config d))) ⟧ config + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (find-or-last⇒lookup (translate (sucs n) c max-c) (zipWith (sucs n) (translate (sucs n)) cs max-cs)) refl ⟩ + NCC.⟦ find-or-last (Fin.toℕ (config d)) (translate (sucs n) c max-c ∷ zipWith (sucs n) (translate (sucs n)) cs max-cs) ⟧ config + ≡⟨ map-find-or-last (λ e → NCC.⟦ e ⟧ config) (Fin.toℕ (config d)) (translate (sucs n) c max-c ∷ zipWith (sucs n) (translate (sucs n)) cs max-cs) ⟩ + find-or-last (Fin.toℕ (config d)) (NCC.⟦ translate (sucs n) c max-c ⟧ config ∷ List.map (λ e → NCC.⟦ e ⟧ config) (zipWith (sucs n) (translate (sucs n)) cs max-cs)) + ≡⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ refl (map∘zipWith (sucs n) cs max-cs)) ⟩ + find-or-last (Fin.toℕ (config d)) (NCC.⟦ translate (sucs n) c max-c ⟧ config ∷ zipWith (sucs n) (λ e max-e → NCC.⟦ translate (sucs n) e max-e ⟧ config) cs max-cs) + ≡⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ (preserves-⊆ (sucs n) c max-c config) (zipWith-cong (sucs n) (λ e max-e → preserves-⊆ (sucs n) e max-e config) cs max-cs)) ⟩ + find-or-last (Fin.toℕ (config d)) (CCC.⟦ c ⟧ (fnoc (sucs n) config) ∷ zipWith (sucs n) (λ e max-e → CCC.⟦ e ⟧ (fnoc (sucs n) config)) cs max-cs) + ≡⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ refl (zipWith⇒map (sucs n) (λ e → CCC.⟦ e ⟧ (fnoc (sucs n) config)) cs max-cs)) ⟩ + find-or-last (Fin.toℕ (config d)) (CCC.⟦ c ⟧ (fnoc (sucs n) config) ∷ List.map (λ e → CCC.⟦ e ⟧ (fnoc (sucs n) config)) cs) + ≡⟨⟩ + find-or-last (Fin.toℕ (config d)) (List⁺.map (λ e → CCC.⟦ e ⟧ (fnoc (sucs n) config)) (c ∷ cs)) + ≡˘⟨ map-find-or-last (λ e → CCC.⟦ e ⟧ (fnoc (sucs n) config)) (fnoc (sucs n) config d) (c ∷ cs) ⟩ + CCC.⟦ find-or-last (fnoc (sucs n) config d) (c ∷ cs) ⟧ (fnoc (sucs n) config) + ≡⟨⟩ + CCC.⟦ d ⟨ c ∷ cs ⟩ ⟧ (fnoc (sucs n) config) + ∎ + + preserves-⊇ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (expr : CCC D i A) + → (choiceLengthLimit : NumberOfAlternatives≤ n {i} expr) + → CCC.⟦ expr ⟧ ⊆[ conf n ] NCC.⟦ translate n expr choiceLengthLimit ⟧ + preserves-⊇ n (a -< cs >-) (maxArtifact max-cs) config = + CCC.⟦ a -< cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → CCC.⟦ e ⟧ config) cs) + ≡˘⟨ Eq.cong₂ artifact refl (zipWith⇒map n (λ e → CCC.⟦ e ⟧ config) cs max-cs) ⟩ + artifact a (zipWith n (λ e max-e → CCC.⟦ e ⟧ config) cs max-cs) + ≡⟨ Eq.cong₂ artifact refl (zipWith-cong n (λ e max-e → preserves-⊇ n e max-e config) cs max-cs) ⟩ + artifact a (zipWith n (λ e max-e → NCC.⟦ translate n e max-e ⟧ (conf n config)) cs max-cs) + ≡˘⟨ Eq.cong₂ artifact refl (map∘zipWith n cs max-cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ (conf n config)) (zipWith n (translate n) cs max-cs)) + ≡⟨⟩ + NCC.⟦ a -< zipWith n (translate n) cs max-cs >- ⟧ (conf n config) + ≡⟨⟩ + NCC.⟦ translate n (a -< cs >-) (maxArtifact max-cs) ⟧ (conf n config) + ∎ + preserves-⊇ (sucs n) (d ⟨ c ∷ cs ⟩) (maxChoice (s≤s max≤n) (max-c ∷ max-cs)) config = + CCC.⟦ d ⟨ c ∷ cs ⟩ ⟧ config + ≡⟨⟩ + CCC.⟦ find-or-last (config d) (c ∷ cs) ⟧ config + ≡⟨ map-find-or-last (λ e → CCC.⟦ e ⟧ config) (config d) (c ∷ cs) ⟩ + find-or-last (config d) (List⁺.map (λ e → CCC.⟦ e ⟧ config) (c ∷ cs)) + ≡⟨⟩ + find-or-last (config d) (CCC.⟦ c ⟧ config ∷ List.map (λ e → CCC.⟦ e ⟧ config) cs) + ≡˘⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ refl (zipWith⇒map (sucs n) (λ e → CCC.⟦ e ⟧ config) cs max-cs)) ⟩ + find-or-last (config d) (CCC.⟦ c ⟧ config ∷ zipWith (sucs n) (λ e max-e → CCC.⟦ e ⟧ config) cs max-cs) + ≡⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ (preserves-⊇ (sucs n) c max-c config) (zipWith-cong (sucs n) (λ e max-e → preserves-⊇ (sucs n) e max-e config) cs max-cs)) ⟩ + find-or-last (config d) (NCC.⟦ translate (sucs n) c max-c ⟧ (conf (sucs n) config) ∷ zipWith (sucs n) (λ e max-e → NCC.⟦ translate (sucs n) e max-e ⟧ (conf (sucs n) config)) cs max-cs) + ≡˘⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ refl (map∘zipWith (sucs n) cs max-cs)) ⟩ + find-or-last (config d) (NCC.⟦ translate (sucs n) c max-c ⟧ (conf (sucs n) config) ∷ List.map (λ e → NCC.⟦ e ⟧ (conf (sucs n) config)) (zipWith (sucs n) (translate (sucs n)) cs max-cs)) + ≡˘⟨ map-find-or-last (λ e → NCC.⟦ e ⟧ (conf (sucs n) config)) (config d) (translate (sucs n) c max-c ∷ zipWith (sucs n) (translate (sucs n)) cs max-cs) ⟩ + NCC.⟦ find-or-last (config d) (translate (sucs n) c max-c ∷ zipWith (sucs n) (translate (sucs n)) cs max-cs) ⟧ (conf (sucs n) config) + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (find-or-last⇒lookup (translate (sucs n) c max-c) (zipWith (sucs n) (translate (sucs n)) cs max-cs)) refl ⟩ + NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (ℕ≥.cappedFin (config d)) ⟧ (conf (sucs n) config) + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)}) (ℕ≥.cast-cappedFin (config d) (Eq.sym (Eq.cong suc (length-zipWith (sucs n) cs max-cs))))) refl ⟩ + NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (Fin.cast (Eq.sym (Eq.cong suc (length-zipWith (sucs n) cs max-cs))) (ℕ≥.cappedFin (config d))) ⟧ (conf (sucs n) config) + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-cast₁ (Eq.cong suc (length-zipWith (sucs n) cs max-cs)) (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (ℕ≥.cappedFin (config d))) refl ⟩ + NCC.⟦ Vec.lookup (Vec.cast (Eq.cong suc (length-zipWith (sucs n) cs max-cs)) (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (ℕ≥.cappedFin (config d)) ⟧ (conf (sucs n) config) + ≡⟨⟩ + NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (ℕ≥.cappedFin (config d)) ⟧ (conf (sucs n) config) + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))}) (ℕ≥.cappedFin-idempotent max≤n (config d))) refl ⟩ + NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (ℕ≥.cappedFin (Fin.toℕ (conf (sucs n) config d))) ⟧ (conf (sucs n) config) + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate (s≤s max≤n) (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (conf (sucs n) config d)) refl ⟩ + NCC.⟦ Vec.lookup (Vec.saturate (s≤s max≤n) (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)))) (conf (sucs n) config d) ⟧ (conf (sucs n) config) + ≡⟨⟩ + NCC.⟦ d ⟨ Vec.saturate (s≤s max≤n) (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) ⟩ ⟧ (conf (sucs n) config) + ≡⟨⟩ + NCC.⟦ translate (sucs n) (d ⟨ c ∷ cs ⟩) (maxChoice (s≤s max≤n) (max-c ∷ max-cs)) ⟧ (conf (sucs n) config) + ∎ + + preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (expr : CCC D i A) + → (choiceLengthLimit : NumberOfAlternatives≤ n expr) + → NCC.⟦ translate n expr choiceLengthLimit ⟧ ≅[ fnoc n ][ conf n ] CCC.⟦ expr ⟧ + preserves n expr choiceLengthLimit = preserves-⊆ n expr choiceLengthLimit , preserves-⊇ n expr choiceLengthLimit + + -- Can't instantiate a LanguageCompiler because the expression compiler depends on the expression + + -- CCC→NCC : {i : Size} → {D : 𝔽} → LanguageCompiler (CCCL D {i}) (λ e → NCCL ⌈ e ⌉ D) + -- -- ^^^^^^ this unrepresentable in our framework + -- CCC→NCC n .LanguageCompiler.compile expr = translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr) + -- CCC→NCC n .LanguageCompiler.config-compiler expr .to = conf ⌈ expr ⌉ + -- CCC→NCC n .LanguageCompiler.config-compiler expr .from = fnoc ⌈ expr ⌉ + -- CCC→NCC n .LanguageCompiler.preserves expr = ≅[]-sym (preserves ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr)) + + -- Having the output language depend on the input expression brings along a lot of complications and problems. + -- Introducing such complications can be avoided by generalizing `translate` to translate into an arbitrary ary `NCCL` by composing it with `NCC→NCC`. + -- This is implemented in the rest of this file. + + +open Exact using (⌈_⌉; numberOfAlternatives≤⌈_⌉) + +-- Gets rid of the `⌈_⌉` in the `IndexedDimension`, here `n`. +Fin→ℕ : ∀ {D : 𝔽} → (n : ℕ≥ 2) -> IndexedDimension D n → D × ℕ +Fin→ℕ n (d , i) = (d , Fin.toℕ i) + +Fin→ℕ⁻¹ : ∀ {D : 𝔽} → (n : ℕ≥ 2) -> D × ℕ → IndexedDimension D n +Fin→ℕ⁻¹ n (d , i) = (d , ℕ≥.cappedFin {ℕ≥.pred n} i) + +Fin→ℕ⁻¹-Fin→ℕ : ∀ {D : 𝔽} → (n : ℕ≥ 2) → Fin→ℕ⁻¹ {D} n ∘ Fin→ℕ {D} n ≗ id +Fin→ℕ⁻¹-Fin→ℕ (sucs n) (d , i) = Eq.cong₂ _,_ refl (ℕ≥.cappedFin-toℕ i) + +translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → 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→NCC.compile ⌈ expr ⌉ (sucs n) + (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) + +conf : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → CCC D i A + → CCC.Configuration D + → NCC.Configuration n (D × ℕ) +conf n expr = + NCC-map-config n (Fin→ℕ⁻¹ ⌈ expr ⌉) + ∘ NCC→NCC.conf ⌈ expr ⌉ n (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr)) + ∘ Exact.conf ⌈ expr ⌉ + +fnoc : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → CCC D i A + → NCC.Configuration n (D × ℕ) + → CCC.Configuration D +fnoc n expr = + Exact.fnoc ⌈ expr ⌉ + ∘ NCC→NCC.fnoc ⌈ expr ⌉ n (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr)) + ∘ (NCC-map-config n (Fin→ℕ ⌈ expr ⌉)) + +preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (expr : CCC D i A) + → NCC.⟦ translate n expr ⟧ ≅[ fnoc n expr ][ conf n expr ] CCC.⟦ expr ⟧ +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→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) ⟧ + ≅[]⟨ Exact.preserves ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr) ⟩ + CCC.⟦ expr ⟧ + ≅[]-∎ + +CCC→NCC : ∀ {i : Size} {D : 𝔽} → (n : ℕ≥ 2) → LanguageCompiler (CCCL D {i}) (NCCL n (D × ℕ)) +CCC→NCC n .LanguageCompiler.compile = translate n +CCC→NCC n .LanguageCompiler.config-compiler expr .to = conf n expr +CCC→NCC n .LanguageCompiler.config-compiler expr .from = fnoc n expr +CCC→NCC n .LanguageCompiler.preserves expr = ≅[]-sym (preserves n expr) + +NCC≽CCC : ∀ {D : 𝔽} → (n : ℕ≥ 2) → NCCL n (D × ℕ) ≽ CCCL D +NCC≽CCC n = expressiveness-from-compiler (CCC→NCC n) diff --git a/src/Translation/Lang/NCC-to-2CC.agda b/src/Translation/Lang/NCC-to-2CC.agda new file mode 100644 index 00000000..48e0397a --- /dev/null +++ b/src/Translation/Lang/NCC-to-2CC.agda @@ -0,0 +1,157 @@ +{-# 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.NCC-to-2CC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where + +open import Data.Bool using (true; false; if_then_else_) +open import Data.Bool.Properties as Bool +import Data.EqIndexedSet as IndexedSet +open import Data.Fin as Fin using (Fin; zero; suc) +open import Data.List as List using (List) +import Data.List.Properties as List +open import Data.Nat using (zero; suc) +open import Data.Product using (_×_) renaming (_,_ to _and_) +open import Data.Vec as Vec using (Vec; []; _∷_) +import Data.Vec.Properties as Vec +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 Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) +open import Size using (Size; ∞) +open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) + +open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) + +open import Lang.2CC as 2CC using (2CC; _-<_>-; _⟨_,_⟩) +module 2CC-Sem-1 D = 2CC.Sem D Variant Artifact∈ₛVariant +open 2CC-Sem-1 using (2CCL) +module 2CC-Sem-2 {D} = 2CC.Sem D Variant Artifact∈ₛVariant +open 2CC-Sem-2 using () renaming (⟦_⟧ to ⟦_⟧₂) + +open import Lang.NCC as NCC using (NCC; _-<_>-; _⟨_⟩) +module NCC-Sem-1 n D = NCC.Sem n D Variant Artifact∈ₛVariant +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 + +artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A +artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs) + + +module 2Ary where + translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → NCC (sucs zero) D i A → 2CC D ∞ A + translate (a -< cs >-) = a -< List.map translate cs >- + translate (d ⟨ l ∷ r ∷ [] ⟩) = d ⟨ translate l , translate r ⟩ + + conf : ∀ {D : 𝔽} → NCC.Configuration (sucs zero) D → 2CC.Configuration D + conf config d with config d + ... | zero = true + ... | suc zero = false + + fnoc : ∀ {D : 𝔽} → 2CC.Configuration D → NCC.Configuration (sucs zero) D + fnoc config d with config d + ... | true = zero + ... | false = suc zero + + preserves-⊆ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (expr : NCC (sucs zero) D i A) + → ⟦ translate expr ⟧₂ ⊆[ fnoc ] ⟦ expr ⟧ₙ + preserves-⊆ (a -< cs >-) config = + ⟦ translate (a -< cs >-) ⟧₂ config + ≡⟨⟩ + ⟦ (a -< List.map translate cs >-) ⟧₂ config + ≡⟨⟩ + artifact a (List.map (λ e → ⟦ e ⟧₂ config) (List.map translate cs)) + ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → ⟦ translate e ⟧₂ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ e config) cs) ⟩ + artifact a (List.map (λ e → ⟦ e ⟧ₙ (fnoc config)) cs) + ≡⟨⟩ + ⟦ a -< cs >- ⟧ₙ (fnoc config) + ∎ + preserves-⊆ (d ⟨ l ∷ r ∷ [] ⟩) config = + ⟦ translate (d ⟨ l ∷ r ∷ [] ⟩) ⟧₂ config + ≡⟨⟩ + ⟦ d ⟨ translate l , translate r ⟩ ⟧₂ config + ≡⟨⟩ + ⟦ if config d then translate l else translate r ⟧₂ config + ≡⟨ Bool.push-function-into-if (λ e → ⟦ e ⟧₂ config) (config d) ⟩ + (if config d then ⟦ translate l ⟧₂ config else ⟦ translate r ⟧₂ config) + ≡⟨ Eq.cong₂ (if_then_else_ (config d)) (preserves-⊆ l config) (preserves-⊆ r config) ⟩ + (if config d then ⟦ l ⟧ₙ (fnoc config) else ⟦ r ⟧ₙ (fnoc config)) + ≡⟨ lemma ⟩ + Vec.lookup (⟦ l ⟧ₙ (fnoc config) ∷ ⟦ r ⟧ₙ (fnoc config) ∷ []) (fnoc config d) + ≡⟨ Vec.lookup-map (fnoc config d) (λ e → ⟦ e ⟧ₙ (fnoc config)) (l ∷ r ∷ []) ⟩ + ⟦ Vec.lookup (l ∷ r ∷ []) (fnoc config d) ⟧ₙ (fnoc config) + ≡⟨⟩ + ⟦ d ⟨ l ∷ r ∷ [] ⟩ ⟧ₙ (fnoc config) + ∎ + where + lemma : ∀ {A : 𝔸} {a b : A} → (if config d then a else b) ≡ Vec.lookup (a ∷ b ∷ []) (fnoc config d) + lemma with config d + ... | true = refl + ... | false = refl + + preserves-⊇ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (expr : NCC (sucs zero) D i A) + → ⟦ expr ⟧ₙ ⊆[ conf ] ⟦ translate expr ⟧₂ + preserves-⊇ (a -< cs >-) config = + ⟦ a -< cs >- ⟧ₙ config + ≡⟨⟩ + artifact a (List.map (λ e → ⟦ e ⟧ₙ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊇ e config) cs) ⟩ + artifact a (List.map (λ e → ⟦ translate e ⟧₂ (conf config)) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → ⟦ e ⟧₂ (conf config)) (List.map translate cs)) + ≡⟨⟩ + ⟦ (a -< List.map translate cs >-) ⟧₂ (conf config) + ≡⟨⟩ + ⟦ translate (a -< cs >-) ⟧₂ (conf config) + ∎ + preserves-⊇ (d ⟨ l ∷ r ∷ [] ⟩) config = + ⟦ d ⟨ l ∷ r ∷ [] ⟩ ⟧ₙ config + ≡⟨⟩ + ⟦ Vec.lookup (l ∷ r ∷ []) (config d) ⟧ₙ config + ≡˘⟨ Vec.lookup-map (config d) (λ e → ⟦ e ⟧ₙ config) (l ∷ r ∷ []) ⟩ + Vec.lookup (⟦ l ⟧ₙ config ∷ ⟦ r ⟧ₙ config ∷ []) (config d) + ≡⟨ lemma ⟩ + (if conf config d then ⟦ l ⟧ₙ config else ⟦ r ⟧ₙ config) + ≡⟨ Eq.cong₂ (if_then_else_ (conf config d)) (preserves-⊇ l config) (preserves-⊇ r config) ⟩ + (if conf config d then ⟦ translate l ⟧₂ (conf config) else ⟦ translate r ⟧₂ (conf config)) + ≡˘⟨ Bool.push-function-into-if (λ e → ⟦ e ⟧₂ (conf config)) (conf config d) ⟩ + ⟦ if conf config d then translate l else translate r ⟧₂ (conf config) + ≡⟨⟩ + ⟦ d ⟨ translate l , translate r ⟩ ⟧₂ (conf config) + ≡⟨⟩ + ⟦ translate (d ⟨ l ∷ r ∷ [] ⟩) ⟧₂ (conf config) + ∎ + where + lemma : {A : 𝔸} → {a b : A} → Vec.lookup (a ∷ b ∷ []) (config d) ≡ (if conf config d then a else b) + lemma with config d + ... | zero = refl + ... | suc zero = refl + + preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (expr : NCC (sucs zero) D i A) + → ⟦ translate expr ⟧₂ ≅[ fnoc ][ conf ] ⟦ expr ⟧ₙ + preserves expr = preserves-⊆ expr and preserves-⊇ expr + + NCC→2CC : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (NCCL (sucs zero) D {i}) (2CCL D) + NCC→2CC .LanguageCompiler.compile = translate + NCC→2CC .LanguageCompiler.config-compiler expr .to = conf + NCC→2CC .LanguageCompiler.config-compiler expr .from = fnoc + NCC→2CC .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr) + + +NCC→2CC : ∀ {i : Size} {D : 𝔽} → (n : ℕ≥ 2) → LanguageCompiler (NCCL n D {i}) (2CCL (D × Fin (ℕ≥.toℕ (ℕ≥.pred n)))) +NCC→2CC n = NCC→NCC n (sucs zero) ⊕ 2Ary.NCC→2CC + +2CC≽NCC : ∀ {D : 𝔽} → (n : ℕ≥ 2) → 2CCL (IndexedDimension D n) ≽ NCCL n D +2CC≽NCC n = expressiveness-from-compiler (NCC→2CC n) diff --git a/src/Translation/Lang/NCC-to-CCC.agda b/src/Translation/Lang/NCC-to-CCC.agda new file mode 100644 index 00000000..56ea5357 --- /dev/null +++ b/src/Translation/Lang/NCC-to-CCC.agda @@ -0,0 +1,151 @@ +{-# 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.NCC-to-CCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where + +import Data.EqIndexedSet as IndexedSet +open import Data.Fin as Fin using (Fin) +open import Data.List as List using (List; []; _∷_) +import Data.List.NonEmpty as List⁺ +import Data.List.Properties as List +open import Data.Product using (_,_) +open import Data.Vec as Vec using (Vec; []; _∷_) +import Data.Vec.Properties as Vec +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 Relation.Binary.PropositionalEquality as Eq using (refl) +open import Size using (Size; ∞) +open import Util.List using (find-or-last; lookup⇒find-or-last) +open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) + +open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) + +import Lang.CCC +module CCC where + open Lang.CCC public + module CCC-Sem-1 D = Lang.CCC.Sem D Variant Artifact∈ₛVariant + open CCC-Sem-1 using (CCCL) public + module CCC-Sem-2 {D} = Lang.CCC.Sem D Variant Artifact∈ₛVariant + open CCC-Sem-2 using (⟦_⟧) public +open CCC using (CCC; CCCL; _-<_>-; _⟨_⟩) + +import Lang.NCC +module NCC where + open Lang.NCC public + module NCC-Sem-1 n D = Lang.NCC.Sem n D Variant Artifact∈ₛVariant + open NCC-Sem-1 using (NCCL) public + module NCC-Sem-2 {n} {D} = Lang.NCC.Sem n D Variant Artifact∈ₛVariant + open NCC-Sem-2 using (⟦_⟧) public +open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) + +artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A +artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs) + + +translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → NCC n D i A + → CCC D ∞ A +translate n (a -< cs >-) = a -< List.map (translate n) cs >- +translate (sucs n) (d ⟨ c ∷ cs ⟩) = d ⟨ List⁺.fromVec (Vec.map (translate (sucs n)) (c ∷ cs)) ⟩ + +conf : ∀ {D : 𝔽} + → (n : ℕ≥ 2) + → NCC.Configuration n D + → CCC.Configuration D +conf (sucs n) config d = Fin.toℕ (config d) + +fnoc : ∀ {D : 𝔽} + → (n : ℕ≥ 2) + → CCC.Configuration D + → NCC.Configuration n D +fnoc (sucs n) config d = ℕ≥.cappedFin (config d) + + +preserves-⊆ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (expr : NCC n D i A) + → CCC.⟦ translate n expr ⟧ ⊆[ fnoc n ] NCC.⟦ expr ⟧ +preserves-⊆ n (a -< cs >-) config = + CCC.⟦ translate n (a -< cs >-) ⟧ config + ≡⟨⟩ + CCC.⟦ a -< List.map (translate n) cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → CCC.⟦ e ⟧ config) (List.map (translate n) cs)) + ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ {g = (λ e → CCC.⟦ e ⟧ config)} {f = translate n} cs) ⟩ + artifact a (List.map (λ e → CCC.⟦ translate n e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ n e config) cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ (fnoc n config)) cs) + ≡⟨⟩ + NCC.⟦ a -< cs >- ⟧ (fnoc n config) + ∎ +preserves-⊆ (sucs n) (d ⟨ c ∷ cs ⟩) config = + CCC.⟦ translate (sucs n) (d ⟨ c ∷ cs ⟩) ⟧ config + ≡⟨⟩ + CCC.⟦ d ⟨ List⁺.fromVec (Vec.map (translate (sucs n)) (c ∷ cs)) ⟩ ⟧ config + ≡⟨⟩ + CCC.⟦ find-or-last (config d) (List⁺.fromVec (Vec.map (translate (sucs n)) (c ∷ cs))) ⟧ config + ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (lookup⇒find-or-last {m = config d} (translate (sucs n) c ∷ Vec.map (translate (sucs n)) cs)) refl ⟩ + CCC.⟦ Vec.lookup (Vec.map (translate (sucs n)) (c ∷ cs)) (ℕ≥.cappedFin (config d)) ⟧ config + ≡⟨ Eq.cong₂ CCC.⟦_⟧ (Vec.lookup-map (ℕ≥.cappedFin (config d)) (translate (sucs n)) (c ∷ cs)) refl ⟩ + CCC.⟦ translate (sucs n) (Vec.lookup (c ∷ cs) (ℕ≥.cappedFin (config d))) ⟧ config + ≡⟨ preserves-⊆ (sucs n) (Vec.lookup (c ∷ cs) (ℕ≥.cappedFin (config d))) config ⟩ + NCC.⟦ Vec.lookup (c ∷ cs) (fnoc (sucs n) config d) ⟧ (fnoc (sucs n) config) + ≡⟨⟩ + NCC.⟦ d ⟨ c ∷ cs ⟩ ⟧ (fnoc (sucs n) config) + ∎ + +preserves-⊇ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (expr : NCC n D i A) + → NCC.⟦ expr ⟧ ⊆[ conf n ] CCC.⟦ translate n expr ⟧ +preserves-⊇ n (a -< cs >-) config = + NCC.⟦ a -< cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊇ n e config) cs) ⟩ + artifact a (List.map (λ e → CCC.⟦ translate n e ⟧ (conf n config)) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ {g = (λ e → CCC.⟦ e ⟧ (conf n config))} {f = translate n} cs) ⟩ + artifact a (List.map (λ e → CCC.⟦ e ⟧ (conf n config)) (List.map (translate n) cs)) + ≡⟨⟩ + CCC.⟦ a -< List.map (translate n) cs >- ⟧ (conf n config) + ≡⟨⟩ + CCC.⟦ translate n (a -< cs >-) ⟧ (conf n config) + ∎ +preserves-⊇ {D} {A} (sucs n) (d ⟨ c ∷ cs ⟩) config = + NCC.⟦ d ⟨ c ∷ cs ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup (c ∷ cs) (config d) ⟧ config + ≡⟨ preserves-⊇ (sucs n) (Vec.lookup (c ∷ cs) (config d)) config ⟩ + CCC.⟦ translate (sucs n) (Vec.lookup (c ∷ cs) (config d)) ⟧ (conf (sucs n) config) + ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (Vec.lookup-map (config d) (translate (sucs n)) (c ∷ cs)) refl ⟩ + CCC.⟦ Vec.lookup (Vec.map (translate (sucs n)) (c ∷ cs)) (config d) ⟧ (conf (sucs n) config) + ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = Vec.map (translate (sucs n)) (c ∷ cs)}) (ℕ≥.cappedFin-toℕ (config d))) refl ⟩ + CCC.⟦ Vec.lookup (Vec.map (translate (sucs n)) (c ∷ cs)) (ℕ≥.cappedFin (Fin.toℕ (config d))) ⟧ (conf (sucs n) config) + ≡⟨ Eq.cong₂ CCC.⟦_⟧ (lookup⇒find-or-last {m = Fin.toℕ (config d)} (translate (sucs n) c ∷ Vec.map (translate (sucs n)) cs)) refl ⟩ + CCC.⟦ find-or-last (Fin.toℕ (config d)) (List⁺.fromVec (Vec.map (translate (sucs n)) (c ∷ cs))) ⟧ (conf (sucs n) config) + ≡⟨⟩ + CCC.⟦ d ⟨ List⁺.fromVec (Vec.map (translate (sucs n)) (c ∷ cs)) ⟩ ⟧ (conf (sucs n) config) + ≡⟨⟩ + CCC.⟦ translate (sucs n) (d ⟨ c ∷ cs ⟩) ⟧ (conf (sucs n) config) + ∎ + +preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (expr : NCC n D i A) + → CCC.⟦ translate n expr ⟧ ≅[ fnoc n ][ conf n ] NCC.⟦ expr ⟧ +preserves n expr = preserves-⊆ n expr , preserves-⊇ n expr + +NCC→CCC : ∀ {i : Size} {D : 𝔽} → (n : ℕ≥ 2) → LanguageCompiler (NCCL n D {i}) (CCCL D) +NCC→CCC n .LanguageCompiler.compile = translate n +NCC→CCC n .LanguageCompiler.config-compiler expr .to = conf n +NCC→CCC n .LanguageCompiler.config-compiler expr .from = fnoc n +NCC→CCC n .LanguageCompiler.preserves expr = ≅[]-sym (preserves n expr) + +CCC≽NCC : {D : 𝔽} → (n : ℕ≥ 2) → CCCL D ≽ NCCL n D +CCC≽NCC n = expressiveness-from-compiler (NCC→CCC n) diff --git a/src/Translation/Lang/NCC-to-NCC.agda b/src/Translation/Lang/NCC-to-NCC.agda new file mode 100644 index 00000000..7681c173 --- /dev/null +++ b/src/Translation/Lang/NCC-to-NCC.agda @@ -0,0 +1,675 @@ +{-# 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.NCC-to-NCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where + +open import Data.Empty using (⊥-elim) +import Data.EqIndexedSet as IndexedSet +open import Data.Fin as Fin using (Fin; zero; suc) +import Data.Fin.Properties as Fin +open import Data.List as List using (List; []; _∷_) +import Data.List.Properties as List +open import Data.Nat using (ℕ; zero; suc; _<_; s≤s; z≤n; _+_; _∸_) +open import Data.Nat.Properties as ℕ using (≤-refl; ≤-reflexive; ≤-trans; <-trans) +open import Data.Product using (_×_; _,_) +open import Data.Vec as Vec using (Vec; []; _∷_) +import Data.Vec.Properties as Vec +open import Framework.Compiler using (LanguageCompiler; _⊕_) +open import Framework.Definitions using (𝔸; 𝔽) +open import Framework.Relation.Function using (from; to) +open import Function using (id; _∘_) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≢_; refl; _≗_) +open import Relation.Nullary.Decidable using (yes; no) +open import Size using (Size; ∞) +import Util.AuxProofs as ℕ +open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +import Util.Vec as Vec + +open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) + +import Lang.NCC +module NCC where + open Lang.NCC public + module NCC-Sem-1 n D = Lang.NCC.Sem n D Variant Artifact∈ₛVariant + open NCC-Sem-1 using (NCCL) public + module NCC-Sem-2 {n} {D} = Lang.NCC.Sem n D Variant Artifact∈ₛVariant + open NCC-Sem-2 using (⟦_⟧) public +open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) + +artifact : {A : 𝔸} → A → List (Variant A) → Variant A +artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs) + + +module map-dim where + NCC-map-config : ∀ {D₁ D₂ : Set} + → (n : ℕ≥ 2) + → (D₂ → D₁) + → NCC.Configuration n D₁ + → NCC.Configuration n D₂ + NCC-map-config n f config = config ∘ f + + map-dim : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (D₁ → D₂) + → NCC n D₁ i A + → NCC n D₂ i A + map-dim n f (a -< cs >-) = a -< List.map (map-dim n f) cs >- + map-dim n f (d ⟨ cs ⟩) = f d ⟨ Vec.map (map-dim n f) cs ⟩ + + preserves-⊆ : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (f : D₁ → D₂) + → (f⁻¹ : D₂ → D₁) + → (expr : NCC n D₁ i A) + → NCC.⟦ map-dim n f expr ⟧ ⊆[ NCC-map-config n f ] NCC.⟦ expr ⟧ + preserves-⊆ n f f⁻¹ (a -< cs >-) config = + NCC.⟦ map-dim n f (a -< cs >-) ⟧ config + ≡⟨⟩ + NCC.⟦ a -< List.map (map-dim n f) cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ config) (List.map (map-dim n f) cs)) + ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ map-dim n f e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ n f f⁻¹ e config) cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ (config ∘ f)) cs) + ≡⟨⟩ + NCC.⟦ a -< cs >- ⟧ (config ∘ f) + ∎ + preserves-⊆ n f f⁻¹ (d ⟨ cs ⟩) config = + NCC.⟦ map-dim n f (d ⟨ cs ⟩) ⟧ config + ≡⟨⟩ + NCC.⟦ f d ⟨ Vec.map (map-dim n f) cs ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup (Vec.map (map-dim n f) cs) (config (f d)) ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (config (f d)) (map-dim n f) cs) refl ⟩ + NCC.⟦ map-dim n f (Vec.lookup cs (config (f d))) ⟧ config + ≡⟨ preserves-⊆ n f f⁻¹ (Vec.lookup cs (config (f d))) config ⟩ + NCC.⟦ Vec.lookup cs (config (f d)) ⟧ (config ∘ f) + ≡⟨⟩ + NCC.⟦ d ⟨ cs ⟩ ⟧ (config ∘ f) + ∎ + + preserves-⊇ : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (f : D₁ → D₂) + → (f⁻¹ : D₂ → D₁) + → f⁻¹ ∘ f ≗ id + → (expr : NCC n D₁ i A) + → NCC.⟦ expr ⟧ ⊆[ NCC-map-config n f⁻¹ ] NCC.⟦ map-dim n f expr ⟧ + preserves-⊇ n f f⁻¹ is-inverse (a -< cs >-) config = + NCC.⟦ a -< cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊇ n f f⁻¹ is-inverse e config) cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ map-dim n f e ⟧ (config ∘ f⁻¹)) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ (config ∘ f⁻¹)) (List.map (map-dim n f) cs)) + ≡⟨⟩ + NCC.⟦ a -< List.map (map-dim n f) cs >- ⟧ (config ∘ f⁻¹) + ≡⟨⟩ + NCC.⟦ map-dim n f (a -< cs >-) ⟧ (config ∘ f⁻¹) + ∎ + preserves-⊇ n f f⁻¹ is-inverse (d ⟨ cs ⟩) config = + NCC.⟦ d ⟨ cs ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup cs (config d) ⟧ config + ≡⟨ preserves-⊇ n f f⁻¹ is-inverse (Vec.lookup cs (config d)) config ⟩ + NCC.⟦ map-dim n f (Vec.lookup cs (config d)) ⟧ (config ∘ f⁻¹) + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (config d) (map-dim n f) cs) refl ⟩ + NCC.⟦ Vec.lookup (Vec.map (map-dim n f) cs) (config d) ⟧ (config ∘ f⁻¹) + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = Vec.map (map-dim n f) cs} refl (Eq.cong config (is-inverse d))) refl ⟩ + NCC.⟦ Vec.lookup (Vec.map (map-dim n f) cs) (config ((f⁻¹ ∘ f) d)) ⟧ (config ∘ f⁻¹) + ≡⟨⟩ + NCC.⟦ f d ⟨ Vec.map (map-dim n f) cs ⟩ ⟧ (config ∘ f⁻¹) + ≡⟨⟩ + NCC.⟦ map-dim n f (d ⟨ cs ⟩) ⟧ (config ∘ f⁻¹) + ∎ + + preserves : ∀ {i : Size} {D₁ D₂ : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → (f : D₁ → D₂) + → (f⁻¹ : D₂ → D₁) + → f⁻¹ ∘ f ≗ id + → (e : NCC n D₁ i A) + → NCC.⟦ map-dim n f e ⟧ ≅[ NCC-map-config n f ][ NCC-map-config n f⁻¹ ] NCC.⟦ e ⟧ + preserves n f f⁻¹ is-inverse expr = preserves-⊆ n f f⁻¹ expr , preserves-⊇ n f f⁻¹ is-inverse expr + + NCC-map-dim : ∀ {i : Size} {D₁ D₂ : Set} + → (n : ℕ≥ 2) + → (f : D₁ → D₂) + → (f⁻¹ : D₂ → D₁) + → f⁻¹ ∘ f ≗ id + → LanguageCompiler (NCCL n D₁ {i}) (NCCL n D₂ {i}) + NCC-map-dim n f f⁻¹ is-inverse .LanguageCompiler.compile = map-dim n f + NCC-map-dim n f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .to = NCC-map-config n f⁻¹ + NCC-map-dim n f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .from = NCC-map-config n f + NCC-map-dim n f f⁻¹ is-inverse .LanguageCompiler.preserves expr = ≅[]-sym (preserves n f f⁻¹ is-inverse expr) + +module IncreaseArity where + -- Increasing the arity is straight forward, just duplicate one element (we choose the last one to be consistent with the saturation semantic of `CCC`, see `find-or-last`) until the arity difference is zero. + -- For symmetry, this module provides a translation from the 2-ary `NCC`, because, for simplicity of the proof, DecreaseArity translates to the 2-ary `NCC`. + -- However, the proof of the generalizaton is almost identical so we proof the generalization in a submodule and specialize the result. + module General where + translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n m : ℕ≥ 2) + → n ℕ≥.≤ m + → NCC n D i A + → NCC m D i A + translate n m n≤m (a -< cs >-) = a -< List.map (translate n m n≤m) cs >- + translate (sucs n) m n≤m (d ⟨ cs ⟩) = d ⟨ Vec.saturate n≤m (Vec.map (translate (sucs n) m n≤m) cs) ⟩ + + conf : ∀ {D : 𝔽} + → (n m : ℕ≥ 2) + → n ℕ≥.≤ m + → NCC.Configuration n D + → NCC.Configuration m D + conf (sucs n) (sucs m) n≤m config d = Fin.inject≤ (config d) n≤m + + fnoc : ∀ {D : 𝔽} + → (n m : ℕ≥ 2) + → n ℕ≥.≤ m + → NCC.Configuration m D + → NCC.Configuration n D + fnoc (sucs n) (sucs m) n≤m config d = ℕ≥.cappedFin (Fin.toℕ (config d)) + + preserves-⊆ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n m : ℕ≥ 2) + → (n≤m : n ℕ≥.≤ m) + → (expr : NCC n D i A) + → NCC.⟦ translate n m n≤m expr ⟧ ⊆[ fnoc n m n≤m ] NCC.⟦ expr ⟧ + preserves-⊆ n m n≤m (a -< cs >-) config = + NCC.⟦ translate n m n≤m (a -< cs >-) ⟧ config + ≡⟨⟩ + NCC.⟦ a -< List.map (translate n m n≤m) cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ config) (List.map (translate n m n≤m) cs)) + ≡˘⟨ Eq.cong₂ artifact Eq.refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ translate n m n≤m e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact Eq.refl (List.map-cong (λ e → preserves-⊆ n m n≤m e config) cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ (fnoc n m n≤m config)) cs) + ≡⟨⟩ + NCC.⟦ a -< cs >- ⟧ (fnoc n m n≤m config) + ∎ + preserves-⊆ (sucs n) (sucs m) n≤m (d ⟨ cs ⟩) config = + NCC.⟦ translate (sucs n) (sucs m) n≤m (d ⟨ cs ⟩) ⟧ config + ≡⟨⟩ + NCC.⟦ d ⟨ Vec.saturate n≤m (Vec.map (translate (sucs n) (sucs m) n≤m) cs) ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup (Vec.saturate n≤m (Vec.map (translate (sucs n) (sucs m) n≤m) cs)) (config d) ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (Vec.saturate-map n≤m (translate (sucs n) (sucs m) n≤m) cs) refl) refl ⟩ + NCC.⟦ Vec.lookup (Vec.map (translate (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) (config d) ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (config d) (translate (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) refl ⟩ + NCC.⟦ (translate (sucs n) (sucs m) n≤m) (Vec.lookup (Vec.saturate n≤m cs) (config d)) ⟧ config + ≡⟨ preserves-⊆ (sucs n) (sucs m) n≤m (Vec.lookup (Vec.saturate n≤m cs) (config d)) config ⟩ + NCC.⟦ Vec.lookup (Vec.saturate n≤m cs) (config d) ⟧ (fnoc (sucs n) (sucs m) n≤m config) + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate n≤m cs (config d)) refl ⟩ + NCC.⟦ Vec.lookup cs (fnoc (sucs n) (sucs m) n≤m config d) ⟧ (fnoc (sucs n) (sucs m) n≤m config) + ≡⟨⟩ + NCC.⟦ d ⟨ cs ⟩ ⟧ (fnoc (sucs n) (sucs m) n≤m config) + ∎ + + preserves-⊇ : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n m : ℕ≥ 2) + → (n≤m : n ℕ≥.≤ m) + → (expr : NCC n D i A) + → NCC.⟦ expr ⟧ ⊆[ conf n m n≤m ] NCC.⟦ translate n m n≤m expr ⟧ + preserves-⊇ n m n≤m (a -< cs >-) config = + artifact a (List.map (λ e → NCC.⟦ e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact Eq.refl (List.map-cong (λ e → preserves-⊇ n m n≤m e config) cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ translate n m n≤m e ⟧ (conf n m n≤m config)) cs) + ≡⟨ Eq.cong₂ artifact Eq.refl (List.map-∘ cs) ⟩ + NCC.⟦ a -< List.map (translate n m n≤m) cs >- ⟧ (conf n m n≤m config) + ≡⟨⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ (conf n m n≤m config)) (List.map (translate n m n≤m) cs)) + ∎ + preserves-⊇ (sucs n) (sucs m) n≤m (d ⟨ cs ⟩) config = + NCC.⟦ d ⟨ cs ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup cs (config d) ⟧ config + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = cs}) (ℕ≥.cappedFin-toℕ (config d))) refl ⟩ + NCC.⟦ Vec.lookup cs (ℕ≥.cappedFin (Fin.toℕ (config d))) ⟧ config + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = cs}) (Eq.cong ℕ≥.cappedFin (Fin.toℕ-inject≤ (config d) n≤m))) refl ⟩ + NCC.⟦ Vec.lookup cs (ℕ≥.cappedFin (Fin.toℕ (Fin.inject≤ (config d) n≤m))) ⟧ config + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate n≤m cs (Fin.inject≤ (config d) n≤m)) refl ⟩ + NCC.⟦ Vec.lookup (Vec.saturate n≤m cs) (Fin.inject≤ (config d) n≤m) ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup (Vec.saturate n≤m cs) (conf (sucs n) (sucs m) n≤m config d) ⟧ config + ≡⟨ preserves-⊇ (sucs n) (sucs m) n≤m (Vec.lookup (Vec.saturate n≤m cs) (conf (sucs n) (sucs m) n≤m config d)) config ⟩ + NCC.⟦ (translate (sucs n) (sucs m) n≤m) (Vec.lookup (Vec.saturate n≤m cs) (conf (sucs n) (sucs m) n≤m config d)) ⟧ (conf (sucs n) (sucs m) n≤m config) + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (conf (sucs n) (sucs m) n≤m config d) (translate (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) refl ⟩ + NCC.⟦ Vec.lookup (Vec.map (translate (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) (conf (sucs n) (sucs m) n≤m config d) ⟧ (conf (sucs n) (sucs m) n≤m config) + ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (Vec.saturate-map n≤m (translate (sucs n) (sucs m) n≤m) cs) refl) refl ⟩ + NCC.⟦ Vec.lookup (Vec.saturate n≤m (Vec.map (translate (sucs n) (sucs m) n≤m) cs)) (conf (sucs n) (sucs m) n≤m config d) ⟧ (conf (sucs n) (sucs m) n≤m config) + ≡⟨⟩ + NCC.⟦ d ⟨ Vec.saturate n≤m (Vec.map (translate (sucs n) (sucs m) n≤m) cs) ⟩ ⟧ (conf (sucs n) (sucs m) n≤m config) + ≡⟨⟩ + NCC.⟦ translate (sucs n) (sucs m) n≤m (d ⟨ cs ⟩) ⟧ (conf (sucs n) (sucs m) n≤m config) + ∎ + + preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n m : ℕ≥ 2) + → (n≤m : n ℕ≥.≤ m) + → (expr : NCC n D i A) + → NCC.⟦ translate n m n≤m expr ⟧ ≅[ fnoc n m n≤m ][ conf n m n≤m ] NCC.⟦ expr ⟧ + preserves n m n≤m expr = preserves-⊆ n m n≤m expr , preserves-⊇ n m n≤m expr + + NCC→NCC : ∀ {i : Size} {D : 𝔽} + → (n m : ℕ≥ 2) + → n ℕ≥.≤ m + → LanguageCompiler (NCCL n D {i}) (NCCL m D {i}) + NCC→NCC n m n≤m .LanguageCompiler.compile = translate n m n≤m + NCC→NCC n m n≤m .LanguageCompiler.config-compiler expr .to = conf n m n≤m + NCC→NCC n m n≤m .LanguageCompiler.config-compiler expr .from = fnoc n m n≤m + NCC→NCC n m n≤m .LanguageCompiler.preserves expr = ≅[]-sym (preserves n m n≤m expr) + + NCC→NCC : ∀ {i : Size} {D : 𝔽} → (n : ℕ≥ 2) → LanguageCompiler (NCCL (sucs zero) D {i}) (NCCL n D {i}) + NCC→NCC (sucs n) = General.NCC→NCC (sucs zero) (sucs n) (ℕ≥.lift≤ z≤n) + + +module DecreaseArity where + -- To simplify the implementation and the proof, we constrain the translation to result in 2-ary `NCC` expressions. + -- The idea of the translation is to represent the each alternative vector as a `List` of alternatives where each `c ∷ cs` is represented by an alternative `d ⟨ c ∷ cs ∷ [] ⟩`. + -- However, this requires that each dimension `d` in this list of alternatives can be configured independently. + -- Otherwise only the first, or last alternative can be selected by configuring `d`. + -- The solution is to extend the dimension `d` by an index (`IndexedDimension`) which numbers the list of alternatives. + -- Note that the last choice in the list of alternatives holds two alternatives, so there will be one less dimension index than there are alternatives. + + IndexedDimension : Set → ℕ≥ 2 → Set + IndexedDimension D n = D × Fin (ℕ≥.toℕ (ℕ≥.pred n)) + + translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸} + → (n : ℕ≥ 2) + → NCC n D i A + → NCC (sucs zero) (IndexedDimension D n) ∞ A + translate n (a -< cs >-) = a -< List.map (translate n) cs >- + translate {i} {D} {A} (sucs n) (d ⟨ cs ⟩) = go n (ℕ.n<1+n n) cs + module translate-Implementation where + go : {i : Size} → (m : ℕ) → (m≤n : m < suc n) → Vec (NCC (sucs n) D i A) (suc (suc m)) → NCC (sucs zero) (D × Fin (suc n)) ∞ A + go zero m≤n (l ∷ r ∷ []) = (d , Fin.opposite (Fin.fromℕ< {zero} m≤n)) ⟨ translate (sucs n) l ∷ translate (sucs n) r ∷ [] ⟩ + go (suc m) m≤n (c ∷ cs) = (d , Fin.opposite (Fin.fromℕ< {suc m} m≤n)) ⟨ translate (sucs n) c ∷ go m (<-trans (ℕ.n<1+n m) m≤n) cs ∷ [] ⟩ + + conf : ∀ {D : 𝔽} + → (n : ℕ≥ 2) + → NCC.Configuration n D + → NCC.Configuration (sucs zero) (IndexedDimension D n) + conf (sucs n) config (d , m) with config d Fin.≟ (Fin.inject₁ m) + ... | yes _ = zero + ... | no _ = suc zero + + module ConfLemmas where + config≡0' : ∀ {D : 𝔽} {d : D} {n : ℕ} + → (config : NCC.Configuration (sucs n) D) + → (j : Fin (suc n)) + → config d ≡ (Fin.inject₁ j) + → conf (sucs n) config (d , j) ≡ zero + config≡0' {d = d} config j config-d≡j with config d Fin.≟ (Fin.inject₁ j) + ... | yes _ = refl + ... | no config-d≢j = ⊥-elim (config-d≢j config-d≡j) + + config≡1' : ∀ {D : 𝔽} {d : D} {n : ℕ} + → (config : NCC.Configuration (sucs n) D) + → (j : Fin (suc n)) + → config d ≢ (Fin.inject₁ j) + → conf (sucs n) config (d , j) ≡ suc zero + config≡1' {d = d} config j config-d≢j with config d Fin.≟ (Fin.inject₁ j) + ... | yes config-d≡j = ⊥-elim (config-d≢j config-d≡j) + ... | no _ = refl + + fnoc : ∀ {D : 𝔽} + → (n : ℕ≥ 2) + → NCC.Configuration (sucs zero) (IndexedDimension D n) + → NCC.Configuration n D + fnoc (sucs n) config d = go n (ℕ.n<1+n n) + module fnoc-Implementation where + go : (m : ℕ) → m < suc n → Fin (suc (suc n)) + go m m m≰j) + go' m m-) config = + NCC.⟦ translate (sucs n) (a -< cs >-) ⟧ config + ≡⟨⟩ + NCC.⟦ a -< List.map (translate (sucs n)) cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ config) (List.map (translate (sucs n)) cs)) + ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ translate (sucs n) e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ (sucs n) e config) cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ (fnoc (sucs n) config)) cs) + ≡⟨⟩ + NCC.⟦ a -< cs >- ⟧ (fnoc (sucs n) config) + ∎ + preserves-⊆ {D = D} {A = A} (sucs n) (d ⟨ cs ⟩) config = + NCC.⟦ translate (sucs n) (d ⟨ cs ⟩) ⟧ config + ≡⟨ lemma n (ℕ.n<1+n n) cs (fnoc (sucs n) config d) (ℕ.+-comm n (Fin.toℕ (fnoc (sucs n) config d))) ⟩ + NCC.⟦ Vec.lookup cs (fnoc (sucs n) config d) ⟧ (fnoc (sucs n) config) + ≡⟨⟩ + NCC.⟦ d ⟨ cs ⟩ ⟧ (fnoc (sucs n) config) + ∎ + where + open translate-Implementation + + -- The key to this lemma, which is an induction over `m`, is to introduce a + -- number `j` which enables stating the invariant provided as the last + -- argument: + -- `m + Fin.toℕ (fnoc (sucs n) config d) ≡ Fin.toℕ j + n` + -- It states that the alternative which is `j` choices deep is selected. At + -- the start of the induction (`m ≡ n`), `j` is determined by the + -- configuration, specifically `fnoc (sucs n) config d`. In each step of the + -- induction both `m` and `j` are decreased so the invariant is obeyed. + -- Hence, as base cases of the induction, we have the cases where `m ≡ zero` + -- or `j ≡ zero`. In all cases we can inspect `j` to conclude if the first + -- (`j ≡ zero`) or second (`j > zero`) alternative is chosen, which is all + -- that is needed to conclude the proof. + lemma + : {i : Size} + → (m : ℕ) + → (m≤n : m < suc n) + → (cs' : Vec (NCC (sucs n) D i A) (suc (suc m))) + → (j : Fin (suc (suc m))) + → m + Fin.toℕ (fnoc (sucs n) config d) ≡ Fin.toℕ j + n + → NCC.⟦ go n d cs m m≤n cs' ⟧ config ≡ NCC.⟦ Vec.lookup cs' j ⟧ (fnoc (sucs n) config) + lemma zero m≤n (l ∷ r ∷ []) zero m+config-d≡j+n = + NCC.⟦ go n d cs zero m≤n (l ∷ r ∷ []) ⟧ config + ≡⟨⟩ + NCC.⟦ (d , Fin.opposite (Fin.fromℕ< {zero} m≤n)) ⟨ translate (sucs n) l ∷ translate (sucs n) r ∷ [] ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup (translate (sucs n) l ∷ translate (sucs n) r ∷ []) (config (d , Fin.opposite (Fin.fromℕ< {zero} m≤n))) ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = translate (sucs n) l ∷ translate (sucs n) r ∷ []} refl (FnocLemmas.config≡0 config (Fin.opposite (Fin.fromℕ< m≤n)) (Fin.toℕ-injective (Eq.trans m+config-d≡j+n (Eq.trans (Eq.sym (Fin.toℕ-fromℕ n)) (Eq.trans (Eq.cong Fin.toℕ (Eq.cong Fin.opposite (Eq.sym (Fin.fromℕ<-toℕ zero m≤n)))) (Eq.sym (Fin.toℕ-inject₁ (Fin.opposite (Fin.fromℕ< m≤n)))))))))) refl ⟩ + NCC.⟦ Vec.lookup (translate (sucs n) l ∷ translate (sucs n) r ∷ []) zero ⟧ config + ≡⟨⟩ + NCC.⟦ translate (sucs n) l ⟧ config + ≡⟨ preserves-⊆ (sucs n) l config ⟩ + NCC.⟦ l ⟧ (fnoc (sucs n) config) + ∎ + lemma zero m≤n (l ∷ r ∷ []) (suc zero) m+config-d≡j+n = + NCC.⟦ (d , Fin.opposite (Fin.fromℕ< m≤n)) ⟨ translate (sucs n) l ∷ translate (sucs n) r ∷ [] ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup (translate (sucs n) l ∷ translate (sucs n) r ∷ []) (config (d , Fin.opposite (Fin.fromℕ< m≤n))) ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = translate (sucs n) l ∷ translate (sucs n) r ∷ []} refl (FnocLemmas.config≡1 config (Fin.opposite (Fin.fromℕ< m≤n)) + (let module ≤ = ℕ.≤-Reasoning in + ≤.begin-strict + Fin.toℕ (Fin.opposite (Fin.fromℕ< m≤n)) + ≤.≡⟨ Fin.opposite-prop (Fin.fromℕ< m≤n) ⟩ + n ∸ Fin.toℕ (Fin.fromℕ< m≤n) + ≤.≡⟨ Eq.cong₂ _∸_ refl (Fin.toℕ-fromℕ< m≤n) ⟩ + n + ≤.<⟨ ℕ.n<1+n n ⟩ + suc n + ≤.≡˘⟨ m+config-d≡j+n ⟩ + Fin.toℕ (fnoc (sucs n) config d) + ≤.∎ + ))) refl ⟩ + NCC.⟦ translate (sucs n) r ⟧ config + ≡⟨ preserves-⊆ (sucs n) r config ⟩ + NCC.⟦ r ⟧ (fnoc (sucs n) config) + ∎ + lemma (suc m) m≤n (c ∷ cs') zero m+config-d≡j+n = + NCC.⟦ (d , Fin.opposite (Fin.fromℕ< m≤n)) ⟨ translate (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) m≤n) cs' ∷ [] ⟩ ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = translate (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) m≤n) cs' ∷ []} refl (FnocLemmas.config≡0 config (Fin.opposite (Fin.fromℕ< {suc m} m≤n)) (Fin.toℕ-injective ( + Fin.toℕ (fnoc (sucs n) config d) + ≡˘⟨ ℕ.m+n∸m≡n (suc m) (Fin.toℕ (fnoc (sucs n) config d)) ⟩ + suc m + Fin.toℕ (fnoc (sucs n) config d) ∸ suc m + ≡⟨ Eq.cong (λ n → n ∸ suc m) m+config-d≡j+n ⟩ + n ∸ suc m + ≡˘⟨ Eq.cong₂ _∸_ refl (Fin.toℕ-fromℕ< m≤n) ⟩ + n ∸ (Fin.toℕ (Fin.fromℕ< m≤n)) + ≡˘⟨ Fin.opposite-prop (Fin.fromℕ< m≤n) ⟩ + Fin.toℕ (Fin.opposite (Fin.fromℕ< m≤n)) + ≡˘⟨ Fin.toℕ-inject₁ (Fin.opposite (Fin.fromℕ< m≤n)) ⟩ + Fin.toℕ (Fin.inject₁ (Fin.opposite (Fin.fromℕ< m≤n))) + ∎ + )))) refl ⟩ + NCC.⟦ translate (sucs n) c ⟧ config + ≡⟨ preserves-⊆ (sucs n) c config ⟩ + NCC.⟦ c ⟧ (fnoc (sucs n) config) + ∎ + lemma (suc m) (s≤s m≤n) (c ∷ cs') (suc j) m+config-d≡j+n = + NCC.⟦ (d , Fin.opposite (Fin.fromℕ< (s≤s m≤n))) ⟨ translate (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) (s≤s m≤n)) cs' ∷ [] ⟩ ⟧ config + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = translate (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) (s≤s m≤n)) cs' ∷ []} refl (FnocLemmas.config≡1 config (Fin.opposite (Fin.fromℕ< (s≤s m≤n))) + (let module ≤ = ℕ.≤-Reasoning in + ≤.begin-strict + Fin.toℕ (Fin.inject₁ (Fin.opposite (Fin.fromℕ< m≤n))) + ≤.≡⟨ Fin.toℕ-inject₁ (Fin.opposite (Fin.fromℕ< m≤n)) ⟩ + Fin.toℕ (Fin.opposite (Fin.fromℕ< m≤n)) + ≤.≡⟨ Fin.opposite-prop (Fin.fromℕ< m≤n) ⟩ + n ∸ suc (Fin.toℕ (Fin.fromℕ< m≤n)) + ≤.≡⟨ Eq.cong₂ _∸_ {x = n} refl (Eq.cong suc (Fin.toℕ-fromℕ< m≤n)) ⟩ + n ∸ suc m + ≤.<⟨ ℕ.m≤n⇒m≤o+n (Fin.toℕ j) (ℕ.m∸n≢0⇒nn⇒m∸n≢0 (ℕ.n∸1+m-) config = + NCC.⟦ a -< cs >- ⟧ config + ≡⟨⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ config) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊇ (sucs n) e config) cs) ⟩ + artifact a (List.map (λ z → NCC.⟦ translate (sucs n) z ⟧ (conf (sucs n) config)) cs) + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + artifact a (List.map (λ e → NCC.⟦ e ⟧ (conf (sucs n) config)) (List.map (translate (sucs n)) cs)) + ≡⟨⟩ + NCC.⟦ translate (sucs n) (a -< cs >-) ⟧ (conf (sucs n) config) + ∎ + preserves-⊇ {D = D} {A = A} (sucs n) (d ⟨ cs ⟩) config = + NCC.⟦ d ⟨ cs ⟩ ⟧ config + ≡⟨⟩ + NCC.⟦ Vec.lookup cs (config d) ⟧ config + ≡˘⟨ lemma n (ℕ.n<1+n n) cs (config d) (ℕ.+-comm n (Fin.toℕ (config d))) ⟩ + NCC.⟦ translate (sucs n) (d ⟨ cs ⟩) ⟧ (conf (sucs n) config) + ∎ + where + open translate-Implementation + + -- The key to this lemma, which is an induction over `m`, is to introduce a + -- number `j` which enables stating the invariant provided as the last + -- argument: + -- `m + Fin.toℕ (config d) ≡ Fin.toℕ j + n` + -- It states that the alternative which is `j` choices deep is selected. At + -- the start of the induction (`m ≡ n`), `j` is determined by the + -- configuration, specifically `config d`. In each step of the + -- induction both `m` and `j` are decreased so the invariant is obeyed. + -- Hence, as base cases of the induction, we have the cases where `m ≡ zero` + -- or `j ≡ zero`. In all cases we can inspect `j` to conclude if the first + -- (`j ≡ zero`) or second (`j > zero`) alternative is chosen, which is all + -- that is needed to conclude the proof + lemma + : {i : Size} + → (m : ℕ) + → (m≤n : m < suc n) + → (cs' : Vec (NCC (sucs n) D i A) (suc (suc m))) + → (j : Fin (suc (suc m))) + → m + Fin.toℕ (config d) ≡ Fin.toℕ j + n + → NCC.⟦ go n d cs m m≤n cs' ⟧ (conf (sucs n) config) ≡ NCC.⟦ Vec.lookup cs' j ⟧ config + lemma zero m≤n (l ∷ r ∷ []) zero m+config-d≡j+n = + NCC.⟦ go n d cs zero m≤n (l ∷ r ∷ []) ⟧ (conf (sucs n) config) + ≡⟨⟩ + NCC.⟦ (d , Fin.opposite (Fin.fromℕ< {zero} m≤n)) ⟨ translate (sucs n) l ∷ translate (sucs n) r ∷ [] ⟩ ⟧ (conf (sucs n) config) + ≡⟨⟩ + NCC.⟦ Vec.lookup (translate (sucs n) l ∷ translate (sucs n) r ∷ []) (conf (sucs n) config (d , Fin.opposite (Fin.fromℕ< {zero} m≤n))) ⟧ (conf (sucs n) config) + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = translate (sucs n) l ∷ translate (sucs n) r ∷ []} refl (ConfLemmas.config≡0' config (Fin.opposite (Fin.fromℕ< m≤n)) (Fin.toℕ-injective ( + Fin.toℕ (config d) + ≡⟨ m+config-d≡j+n ⟩ + n + ≡˘⟨ Fin.toℕ-fromℕ n ⟩ + Fin.toℕ (Fin.fromℕ n) + ≡⟨ Eq.cong Fin.toℕ (Eq.cong Fin.opposite (Eq.sym (Fin.fromℕ<-toℕ zero m≤n))) ⟩ + Fin.toℕ (Fin.opposite (Fin.fromℕ< m≤n)) + ≡˘⟨ Fin.toℕ-inject₁ (Fin.opposite (Fin.fromℕ< m≤n)) ⟩ + Fin.toℕ (Fin.inject₁ (Fin.opposite (Fin.fromℕ< m≤n))) + ∎ + )))) refl ⟩ + NCC.⟦ Vec.lookup (translate (sucs n) l ∷ translate (sucs n) r ∷ []) zero ⟧ (conf (sucs n) config) + ≡⟨⟩ + NCC.⟦ translate (sucs n) l ⟧ (conf (sucs n) config) + ≡˘⟨ preserves-⊇ (sucs n) l config ⟩ + NCC.⟦ l ⟧ config + ∎ + lemma zero m≤n (l ∷ r ∷ []) (suc zero) m+config-d≡j+n = + NCC.⟦ (d , Fin.opposite (Fin.fromℕ< m≤n)) ⟨ translate (sucs n) l ∷ translate (sucs n) r ∷ [] ⟩ ⟧ (conf (sucs n) config) + ≡⟨⟩ + NCC.⟦ Vec.lookup (translate (sucs n) l ∷ translate (sucs n) r ∷ []) (conf (sucs n) config (d , Fin.opposite (Fin.fromℕ< m≤n))) ⟧ (conf (sucs n) config) + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = translate (sucs n) l ∷ translate (sucs n) r ∷ []} refl (ConfLemmas.config≡1' config (Fin.opposite (Fin.fromℕ< m≤n)) (λ config-d≡opposite-m → ℕ.1+n≢n ( + suc n + ≡˘⟨ m+config-d≡j+n ⟩ + Fin.toℕ (config d) + ≡⟨ Eq.cong Fin.toℕ config-d≡opposite-m ⟩ + Fin.toℕ (Fin.inject₁ (Fin.opposite (Fin.fromℕ< m≤n))) + ≡⟨ Fin.toℕ-inject₁ (Fin.opposite (Fin.fromℕ< m≤n)) ⟩ + Fin.toℕ (Fin.opposite (Fin.fromℕ< m≤n)) + ≡⟨ Fin.opposite-prop (Fin.fromℕ< m≤n) ⟩ + n ∸ Fin.toℕ (Fin.fromℕ< m≤n) + ≡⟨ Eq.cong₂ _∸_ refl (Fin.toℕ-fromℕ< m≤n) ⟩ + n ∸ zero + ≡⟨⟩ + n + ∎ + )))) refl ⟩ + NCC.⟦ translate (sucs n) r ⟧ (conf (sucs n) config) + ≡˘⟨ preserves-⊇ (sucs n) r config ⟩ + NCC.⟦ r ⟧ config + ∎ + lemma (suc m) m≤n (c ∷ cs') zero m+config-d≡j+n = + NCC.⟦ (d , Fin.opposite (Fin.fromℕ< m≤n)) ⟨ translate (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) m≤n) cs' ∷ [] ⟩ ⟧ (conf (sucs n) config) + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = translate (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) m≤n) cs' ∷ []} refl (ConfLemmas.config≡0' config (Fin.opposite (Fin.fromℕ< m≤n)) (Fin.toℕ-injective ( + Fin.toℕ (config d) + ≡˘⟨ ℕ.m+n∸m≡n (suc m) (Fin.toℕ (config d)) ⟩ + suc m + Fin.toℕ (config d) ∸ suc m + ≡⟨ Eq.cong (λ n → n ∸ suc m) m+config-d≡j+n ⟩ + n ∸ suc m + ≡˘⟨ Eq.cong₂ _∸_ refl (Fin.toℕ-fromℕ< m≤n) ⟩ + n ∸ (Fin.toℕ (Fin.fromℕ< m≤n)) + ≡˘⟨ Fin.opposite-prop (Fin.fromℕ< m≤n) ⟩ + Fin.toℕ (Fin.opposite (Fin.fromℕ< m≤n)) + ≡˘⟨ Fin.toℕ-inject₁ (Fin.opposite (Fin.fromℕ< m≤n)) ⟩ + Fin.toℕ (Fin.inject₁ (Fin.opposite (Fin.fromℕ< m≤n))) + ∎ + )))) refl ⟩ + NCC.⟦ translate (sucs n) c ⟧ (conf (sucs n) config) + ≡˘⟨ preserves-⊇ (sucs n) c config ⟩ + NCC.⟦ c ⟧ config + ∎ + lemma (suc m) (s≤s m≤n) (c ∷ cs') (suc j) m+config-d≡j+n = + NCC.⟦ (d , Fin.opposite (Fin.fromℕ< (s≤s m≤n))) ⟨ translate (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) (s≤s m≤n)) cs' ∷ [] ⟩ ⟧ (conf (sucs n) config) + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = translate (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) (s≤s m≤n)) cs' ∷ []} refl (ConfLemmas.config≡1' config (Fin.opposite (Fin.fromℕ< (s≤s m≤n))) + (λ config-d≡opposite-m → (ℕ.<⇒≢ (ℕ.m≤n⇒m≤o+n (Fin.toℕ j) (ℕ.m∸n≢0⇒nn⇒m∸n≢0 (ℕ.n∸1+m- to Artifactₒ) -open LOC.Sem F V mkArtifact -import Lang.BCC as LBCC -open LBCC F renaming (Configuration to Conf₂; _-<_>- to Artifact₂) -open LBCC.Sem F V mkArtifact renaming (⟦_⟧ to ⟦_⟧₂) +import Lang.OC as OC +open OC F renaming (_-<_>- to Artifactₒ) +open OC.Sem F V mkArtifact +import Lang.2CC as 2CC +open 2CC F renaming (_-<_>- to Artifact₂) +open 2CC.Sem F V mkArtifact renaming (⟦_⟧ to ⟦_⟧₂) open import Data.EqIndexedSet @@ -88,7 +88,7 @@ record Zip (work : ℕ) (i : Size) (A : 𝔸) : Set where constructor _-<_≪_>- --\T field parent : A - siblingsL : List (BCC ∞ A) + siblingsL : List (2CC ∞ A) siblingsR : Vec (OC i A) work open Zip public infix 4 _-<_≪_>- @@ -97,7 +97,7 @@ infix 4 _-<_≪_>- Zip-is-𝔼 : ℕ → Size → 𝔼 Zip-is-𝔼 = Zip -⟦_⟧ₜ : ∀ {w i} → 𝔼-Semantics V Confₒ (Zip w i) +⟦_⟧ₜ : ∀ {w i} → 𝔼-Semantics V (OC.Configuration F) (Zip w i) ⟦ a -< ls ≪ rs >- ⟧ₜ c = let ⟦ls⟧ = map (flip ⟦_⟧₂ c) ls ⟦rs⟧ = ⟦ toList rs ⟧ₒ-recurse c @@ -111,24 +111,24 @@ data _⊢_⟶ₒ_ : ∀ {n : ℕ} {A : 𝔸} → (i : Size) -- We have to make sizes explicit here because otherwise, Agda sometimes infers ∞ which makes termination checking fail. → Zip n i A - → BCC ∞ A + → 2CC ∞ A → Set infix 3 _⊢_⟶ₒ_ data _⊢_⟶ₒ_ where {-| We finished translating a subtree. All work is done. - We thus wrap up the zipper to the OC→BCCd subtree it represents. + We thus wrap up the zipper to the OC→2CCd subtree it represents. -} T-done : ∀ {i : Size} {A : 𝔸} {a : A} - {ls : List (BCC ∞ A)} + {ls : List (2CC ∞ A)} -------------------------------------- → i ⊢ a -< ls ≪ [] >- ⟶ₒ Artifact₂ a ls {-| - If the next expression to OC→BCC is an artifact, + If the next expression to OC→2CC is an artifact, we recursively proceed all its children (obtaining e₁) an then proceed with the remaining expressions (obtaining e₂). -} @@ -137,19 +137,19 @@ data _⊢_⟶ₒ_ where {n : ℕ } {A : 𝔸} {a b : A } - {ls : List (BCC ∞ A) } + {ls : List (2CC ∞ A) } {es : List (OC i A) } {rs : Vec (OC (↑ i) A) n} - {e₁ : BCC ∞ A} - {e₂ : BCC ∞ A} + {e₁ : 2CC ∞ A} + {e₂ : 2CC ∞ A} → i ⊢ b -< [] ≪ (fromList es) >- ⟶ₒ e₁ → ↑ i ⊢ a -< ls ∷ʳ e₁ ≪ rs >- ⟶ₒ e₂ --------------------------------------------- → ↑ i ⊢ a -< ls ≪ Artifactₒ b es ∷ rs >- ⟶ₒ e₂ {-| - If the next expression to OC→BCC is an option, - we OC→BCC the current subtree once with the option picked (obtaining eᵒ⁻ʸ) + If the next expression to OC→2CC is an option, + we OC→2CC the current subtree once with the option picked (obtaining eᵒ⁻ʸ) and once without the option picked (obtaining eᵒ⁻ʸ). We can then put both results into a binary choice, where going left means picking the option, and going right means not picking the option. @@ -161,10 +161,10 @@ data _⊢_⟶ₒ_ where {a : A } {O : Option} {e : OC i A} - {ls : List (BCC ∞ A) } + {ls : List (2CC ∞ A) } {rs : Vec (OC (↑ i) A) n} - {eᵒ⁻ʸ : BCC ∞ A} - {eᵒ⁻ⁿ : BCC ∞ A} + {eᵒ⁻ʸ : 2CC ∞ A} + {eᵒ⁻ⁿ : 2CC ∞ A} → ↑ i ⊢ a -< ls ≪ e ∷ rs >- ⟶ₒ eᵒ⁻ʸ → ↑ i ⊢ a -< ls ≪ rs >- ⟶ₒ eᵒ⁻ⁿ ---------------------------------------------------- @@ -173,7 +173,7 @@ data _⊢_⟶ₒ_ where data _⟶_ : ∀ {i : Size} {A : 𝔸} → WFOC i A - → BCC ∞ A + → 2CC ∞ A → Set infix 4 _⟶_ data _⟶_ where @@ -182,7 +182,7 @@ data _⟶_ where {A : 𝔸} {a : A} {es : List (OC i A)} - {e : BCC ∞ A} + {e : 2CC ∞ A} → i ⊢ a -< [] ≪ (fromList es) >- ⟶ₒ e ------------------------------------ → Root a es ⟶ e @@ -190,9 +190,9 @@ data _⟶_ where ## Determinism -Every OC expression is OC→BCCd to at most one BCC expression. +Every OC expression is OC→2CCd to at most one 2CC expression. ```agda -⟶ₒ-is-deterministic : ∀ {n} {i} {A} {z : Zip n i A} {b b' : BCC ∞ A} +⟶ₒ-is-deterministic : ∀ {n} {i} {A} {z : Zip n i A} {b b' : 2CC ∞ A} → i ⊢ z ⟶ₒ b → i ⊢ z ⟶ₒ b' ------------ @@ -207,7 +207,7 @@ Every OC expression is OC→BCCd to at most one BCC expression. r₁≡r₂ = ⟶ₒ-is-deterministic ⟶r₁ ⟶r₂ in Eq.cong₂ (O ⟨_,_⟩) l₁≡l₂ r₁≡r₂ -⟶-is-deterministic : ∀ {i} {A} {e : WFOC i A} {b b' : BCC ∞ A} +⟶-is-deterministic : ∀ {i} {A} {e : WFOC i A} {b b' : 2CC ∞ A} → e ⟶ b → e ⟶ b' ------- @@ -217,7 +217,7 @@ Every OC expression is OC→BCCd to at most one BCC expression. ## Totality (i.e., Progress) -Every OC expression is OC→BCCd to at least one BCC expression. +Every OC expression is OC→2CCd to at least one 2CC expression. Since we have already proven determinism, the proof for totality and thus a translation is unique. ```agda Totalₒ : ∀ {n} {i} {A} → (e : Zip n i A) → Set @@ -267,18 +267,18 @@ Theorems: ```agda preservesₒ : ∀ {n} {i} {A} - {b : BCC ∞ A} + {b : 2CC ∞ A} {z : Zip n i A} - → (c : Confₒ) + → (c : OC.Configuration F) → i ⊢ z ⟶ₒ b ------------------- → ⟦ z ⟧ₜ c ≡ ⟦ b ⟧₂ c preserves : ∀ {i} {A} - {b : BCC ∞ A} + {b : 2CC ∞ A} {e : WFOC i A} - → (c : Confₒ) + → (c : OC.Configuration F) → e ⟶ b ------------------ → ⟦ e ⟧ c ≡ ⟦ b ⟧₂ c @@ -300,8 +300,8 @@ Agda fails to see that "preserves" directly unpacks this constructor again and c Since Agda fails here, we have to avoid the re- and unpacking below T-root and thus introduce this auxiliary function. -} preserves-without-T-root : - ∀ {i} {A} {b : A} {es : List (OC i A)} {e : BCC ∞ A} - → (c : Confₒ) + ∀ {i} {A} {b : A} {es : List (OC i A)} {e : 2CC ∞ A} + → (c : OC.Configuration F) → (⟶e : i ⊢ b -< [] ≪ fromList es >- ⟶ₒ e) ------------------------------------------ → ⟦ Root b es ⟧ c ≡ ⟦ e ⟧₂ c @@ -327,9 +327,9 @@ The concrete formulas are a bit convoluted here because they are partially norma preservesₒ-artifact : ∀ {i} {A} {c} {b : A} - {ls : List (BCC ∞ A)} + {ls : List (2CC ∞ A)} {es : List (OC i A)} - {e : BCC ∞ A} + {e : 2CC ∞ A} → (rs : List (V A)) → (⟶e : i ⊢ b -< [] ≪ fromList es >- ⟶ₒ e) ---------------------------------------------------------------- @@ -368,7 +368,7 @@ So we show Agda that ⟦_⟧ₒ never does so. This theorem has no real meaning and is rather a technical necessity. -} preservesₒ-option-size : - ∀ {n} {i} {A} {c} {a : A} {ls : List (BCC ∞ A)} {rs : Vec (OC (↑ i) A) n} + ∀ {n} {i} {A} {c} {a : A} {ls : List (2CC ∞ A)} {rs : Vec (OC (↑ i) A) n} → (e : OC i A) ----------------------------------------------------------------------------------------------------- → Artifactᵥ a (map (flip ⟦_⟧₂ c) ls ++ catMaybes (⟦_⟧ₒ {i } {A} e c ∷ map (flip ⟦_⟧ₒ c) (toList rs))) @@ -444,7 +444,7 @@ open import Framework.VariabilityLanguage open import Framework.Relation.Expressiveness V open import Framework.Relation.Function using (_⇔_) -compile : ∀ {i : Size} {A : 𝔸} → WFOC i A → BCC ∞ A +compile : ∀ {i : Size} {A : 𝔸} → WFOC i A → 2CC ∞ A compile = proj₁ ∘ ⟶-is-total compile-preserves : ∀ {i : Size} {A : 𝔸} @@ -459,20 +459,16 @@ compile-preserves {i} {A} e = left , sym ∘ left -- this works because id is ou derivation = proj₂ trans in preserves c derivation -compile-configs : Confₒ ⇔ Conf₂ +compile-configs : OC.Configuration F ⇔ 2CC.Configuration F compile-configs = record { to = id ; from = id } -OC→BCC : LanguageCompiler WFOCL BCCL -OC→BCC = record +OC→2CC : LanguageCompiler WFOCL 2CCL +OC→2CC = record { compile = compile - ; config-compiler = compile-configs + ; config-compiler = λ _ → compile-configs ; preserves = compile-preserves } -BCC-is-at-least-as-expressive-as-OC : BCCL ≽ WFOCL -BCC-is-at-least-as-expressive-as-OC = expressiveness-by-translation compile compile-preserves-semantics - where - -- this drops the knowledge on id, id being the configuration compiler - compile-preserves-semantics : SemanticsPreserving WFOCL BCCL compile - compile-preserves-semantics {A} e = ≅[]→≅ (compile-preserves e) +2CC≽OC : 2CCL ≽ WFOCL +2CC≽OC = expressiveness-from-compiler OC→2CC ``` diff --git a/src/Translation/Lang/VariantList-to-CCC.lagda.md b/src/Translation/Lang/VariantList-to-CCC.lagda.md index f5c8ddd8..a4c00be9 100644 --- a/src/Translation/Lang/VariantList-to-CCC.lagda.md +++ b/src/Translation/Lang/VariantList-to-CCC.lagda.md @@ -152,7 +152,7 @@ module Translate VariantList→CCC : LanguageCompiler VariantListL CCCL VariantList→CCC = record { compile = translate - ; config-compiler = record { to = conf ; from = fnoc } + ; config-compiler = λ _ → record { to = conf ; from = fnoc } ; preserves = λ {A} e → let open Preservation A in preserves-⊆ e , preserves-⊇ e diff --git a/src/Translation/LanguageMap.lagda.md b/src/Translation/LanguageMap.lagda.md index 4c0ec343..ec054c6d 100644 --- a/src/Translation/LanguageMap.lagda.md +++ b/src/Translation/LanguageMap.lagda.md @@ -30,28 +30,28 @@ open import Framework.Proof.Transitive Variant using (less-expressive-from-compl open import Construct.Artifact as At using () renaming (Syntax to Artifact) import Lang.OC -import Lang.BCC +import Lang.2CC import Lang.CCC -- DONE -import Translation.Lang.OC-to-BCC --- import Translation.Lang.BCC-to-CCC +import Translation.Lang.OC-to-2CC +-- import Translation.Lang.2CC-to-CCC -- IN PROGRESS --- import Translation.Lang.CCC-to-BCC +-- import Translation.Lang.CCC-to-2CC ``` ## Core Choice Calculus vs Binary Choice Calculus ```agda --- open Translation.CCC-to-BCC using ( +-- open Translation.CCC-to-2CC using ( -- -- TODO: Still unproven --- -- BCC-is-at-least-as-expressive-as-CCC +-- -- 2CC-is-at-least-as-expressive-as-CCC -- ) public --- open Translation.BCC-to-CCC using ( --- CCC-is-at-least-as-expressive-as-BCC; --- BCC→CCC-is-semantics-preserving +-- open Translation.2CC-to-CCC using ( +-- CCC-is-at-least-as-expressive-as-2CC; +-- 2CC→CCC-is-semantics-preserving -- ) public -- For any type of variant that we can encode in CCC: @@ -75,14 +75,14 @@ module CCC-Props (F : 𝔽) (D : F) where ```agda module _ (F : 𝔽) where open Lang.OC.Sem F Variant mkArtifact using (WFOCL) - open Lang.BCC.Sem F Variant mkArtifact using (BCCL) + open Lang.2CC.Sem F Variant mkArtifact using (2CCL) open Lang.OC.IncompleteOnRose F using (OC-is-incomplete) - {- TODO: Substitute completeness proof of BCC here. -} - OC-is-less-expressive-than-BCC : WFOCL ⋡ BCCL - OC-is-less-expressive-than-BCC = less-expressive-from-completeness {!!} OC-is-incomplete + {- TODO: Substitute completeness proof of 2CC here. -} + OC-is-less-expressive-than-2CC : WFOCL ⋡ 2CCL + OC-is-less-expressive-than-2CC = less-expressive-from-completeness {!!} OC-is-incomplete -open Translation.Lang.OC-to-BCC using ( - BCC-is-at-least-as-expressive-as-OC +open Translation.Lang.OC-to-2CC using ( + 2CC≽OC ) public ``` diff --git a/src/Util/AuxProofs.agda b/src/Util/AuxProofs.agda index b13f95a6..fd36cb15 100644 --- a/src/Util/AuxProofs.agda +++ b/src/Util/AuxProofs.agda @@ -7,7 +7,7 @@ open import Data.Bool using (Bool; false; true; if_then_else_) open import Data.Nat using (ℕ; zero; suc; NonZero; _≡ᵇ_; _⊓_; _+_; _∸_; _<_; _≤_; s≤s; z≤n) open import Data.Fin using (Fin; zero; suc; fromℕ<) -open import Data.Nat.Properties using (m⊓n≤m; +-comm; +-∸-comm; n∸n≡0) +open import Data.Nat.Properties using (n<1+n; m⊓n≤m; +-comm; +-∸-comm; n∸n≡0) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; _≢_; _≗_; refl) @@ -57,6 +57,10 @@ n