Merge pull request #22 from pmbittner/2ADT-to-NADT-to-CCC

Compile 2ADT to NADT and NADT to CCC

src/Lang/CCC.lagda.md

@@ -142,17 +142,8 @@ module Encode where
     ; from = λ _ → tt
     }
 
-  {-|
-  Unfortunately, I had to flag this function as terminating.
-  One solution to prove its termination is to use a sized variant (instead of using ∞).
-  The problem is that the semantics ⟦_⟧ forgets the size and sets it to ∞ and hence,
-  the types of ⟦ encode v ⟧ c and v are different and hence their values can never be equivalent regarding ≡.
-
-  The function below indeed terminates but proving it within our framework became a _technical_ challenge (not a mathematical one) for which I found no solution yet.
-  -}
-  {-# TERMINATING #-}
   ccc-encode-idemp : ∀ {A} (v : Rose ∞ A) → (c : Configuration) → ⟦ encode v ⟧ c ≡ v
-  ccc-encode-idemp v@(rose (a At.-< cs >-)) c =
+  ccc-encode-idemp {A} v@(rose (a At.-< cs >-)) c =
     begin
       ⟦ encode v ⟧ c
     ≡⟨⟩
@@ -161,12 +152,13 @@ module Encode where
           Eq.cong (a At.-<_>-) (map-∘ cs) ⟩
       rose (a At.-< map (λ x → ⟦ encode x ⟧ c) cs >-)
     ≡⟨ Eq.cong rose $
-          Eq.cong (a At.-<_>-) (map-cong (λ x → ccc-encode-idemp x c) cs) ⟩
-      rose (a At.-< map id cs >-)
-    ≡⟨ Eq.cong rose $
-          Eq.cong (a At.-<_>-) (map-id cs) ⟩
+          Eq.cong (a At.-<_>-) (go cs) ⟩
       v
     ∎
+    where
+    go : (cs' : List (Rose ∞ A)) → map (λ c' → ⟦ encode c' ⟧ c) cs' ≡ cs'
+    go [] = refl
+    go (c' ∷ cs') = Eq.cong₂ _∷_ (ccc-encode-idemp c' c) (go cs')
 
   preserves : ∀ {A} → (v : Rose ∞ A)
     → Semantics (Variant-is-VL V) v ≅[ to confs ][ from confs ] ⟦ encode v ⟧

src/Lang/NADT.agda

@@ -2,7 +2,7 @@
 
 open import Framework.Definitions
 -- TODO: Generalize level of F
-module Lang.NADT (F : 𝔽) (V : 𝕍) where
+module Lang.NADT (V : 𝕍) (F : 𝔽) where
 
 open import Data.Nat using (ℕ)
 open import Function using (id)
@@ -15,7 +15,7 @@ open import Construct.GrulerArtifacts
 open import Construct.Choices
 
 data NADT : Size → 𝔼 where
-  NADTAsset  : ∀ {i A} → Leaf (V A)                   → NADT i A
+  NADTAsset  : ∀ {i A} → Leaf (V A)                   → NADT (↑ i) A
   NADTChoice : ∀ {i A} → VLChoice.Syntax F (NADT i) A → NADT (↑ i) A
 
 mutual

src/Translation/Lang/2ADT-to-NADT.agda

@@ -1,57 +1,134 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Definitions
-module Translation.Lang.2ADT-to-NADT {F : 𝔽} {A : 𝔸} where
 
-open import Data.Nat using (ℕ)
+open import Framework.Construct using (_∈ₛ_; cons)
+open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
+
+module Translation.Lang.2ADT-to-NADT (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+
+open import Data.Bool using (if_then_else_; true; false)
+import Data.Bool.Properties as Bool
+open import Data.List using (List; []; _∷_)
+open import Data.List.NonEmpty using (_∷_)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Product using () renaming (_,_ to _and_)
 open import Level using (0ℓ)
-open import Size using (Size; ∞; ↑_)
+open import Size using (Size; ∞)
+
+import Util.List as List
+open import Framework.Relation.Function using (from; to)
+open import Framework.Compiler using (LanguageCompiler)
+open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 open Eq.≡-Reasoning
 
-import Data.IndexedSet
+import Data.EqIndexedSet as IndexedSet
+open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym)
 
 open import Construct.Choices
 open import Construct.GrulerArtifacts as GL using ()
 open import Construct.NestedChoice using (value; choice)
 
 open import Framework.Variants using (GrulerVariant)
-open import Lang.2ADT
-open import Lang.NADT
+open import Construct.GrulerArtifacts using (leaf)
+
+import Lang.2ADT
+module 2ADT where
+  module 2ADT-Sem-1 F = Lang.2ADT F Variant
+  open 2ADT-Sem-1 using (2ADT; 2ADTL; Configuration) public
+  module 2ADT-Sem-2 {F} = Lang.2ADT F Variant
+  open 2ADT-Sem-2 using (⟦_⟧) public
+open 2ADT using (2ADT; 2ADTL)
 
-import Translation.Construct.2Choice-to-Choice {F} as 2Choice-to-Choice
+import Lang.CCC
+module CCC where
+  open Lang.CCC public
+  module CCC-Sem-1 F = Lang.CCC.Sem F Variant Artifact∈ₛVariant
+  open CCC-Sem-1 using (CCCL) public
+  module CCC-Sem-2 {F} = Lang.CCC.Sem F Variant Artifact∈ₛVariant
+  open CCC-Sem-2 using (⟦_⟧) public
+open CCC using (CCC; CCCL; _-<_>-; _⟨_⟩)
+
+import Lang.NADT
+module NADT where
+  open Lang.NADT Variant using (NADT; NADTAsset; NADTChoice) renaming (NADTVL to NADTL) public
+  module NADT-Sem {F} = Lang.NADT Variant F
+  open NADT-Sem using () renaming (semantics to ⟦_⟧) public -- TODO
+open NADT using (NADT; NADTAsset; NADTChoice; NADTL)
+
+import Translation.Construct.2Choice-to-Choice as 2Choice-to-Choice
 open 2Choice-to-Choice.Translate using (convert)
 
-{-# TERMINATING #-}
--- TODO: Fix termination checking and also get rid of complicated constructor stuff.
-compile : ∀ {V : 𝕍} → 2ADT F V A → NADT F V ∞ A
-compile (leaf a)      = NADTAsset (GL.leaf a)
-compile {V} (D ⟨ l , r ⟩) = NADTChoice (Choice.map compile (convert (Eq.setoid (2ADT F V A)) (D 2Choice.⟨ l , r ⟩)))
-
-module Preservation where
-  -- open Data.IndexedSet (VariantSetoid GrulerVariant A) using () renaming (_≅_ to _≋_)
-
-  -- TODO: Prove Preservation of compile
-  -- 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
-  -- preserves-l (choice (D ⟨ l , r ⟩)) c =
-  --   begin
-  --     ⟦ choice (D ⟨ l , r ⟩) ⟧-2adt c
-  --   ≡⟨⟩
-  --     BinaryChoice-Semantics 2ADTVL (D ⟨ l , r ⟩) c
-  --   ≡⟨ preserves-conf D l r (default-conf-satisfies-spec D) (preserves-l l) (preserves-l r) c ⟩
-  --     Choice-Semantics NADTVL (convert (D ⟨ l , r ⟩)) (conf' c)
-  --   ≡⟨⟩
-  --     ⟦ compile (choice (D ⟨ l , r ⟩)) ⟧-nadt (conf' c)
-  --   ∎
-
-  -- preserves-r : ∀ (e : 2ADT A) → Fnoc-Preserves 2ADTVL NADTVL e (compile e) fnoc'
-  -- preserves-r (value _) _ = refl
-  -- preserves-r (choice (D ⟨ l , r ⟩)) c = preserves-fnoc D l r (default-fnoc-satisfies-spec D) (preserves-r l) (preserves-r r) c
-
-  -- preserves : ∀ (e : 2ADT A) → ⟦ e ⟧-2adt ≋ ⟦ compile e ⟧-nadt
-  -- preserves e = ⊆-by-index-translation conf' (preserves-l e)
-  --           and ⊆-by-index-translation fnoc' (preserves-r e)
+artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
+
+
+translate : ∀ {F : 𝔽} {A : 𝔸} → 2ADT F A → NADT F ∞ A
+translate (2ADT.leaf a) = NADTAsset (leaf a)
+translate {F = F} {A = A} (f 2ADT.⟨ l , r ⟩) = NADTChoice (f Choice.⟨ translate l ∷ translate r ∷ [] ⟩)
+
+conf : ∀ {F : 𝔽} → 2ADT.Configuration F → CCC.Configuration F
+conf config f with config f
+... | true = 0
+... | false = 1
+
+fnoc : ∀ {F : 𝔽} → CCC.Configuration F → 2ADT.Configuration F
+fnoc config f with config f
+... | zero = true
+... | suc _ = false
+
+preserves-⊆ : ∀ {F : 𝔽} {A : 𝔸} → (expr : 2ADT F A) → NADT.⟦ translate expr ⟧ ⊆[ fnoc ] 2ADT.⟦ expr ⟧
+preserves-⊆ (2ADT.leaf v) config = refl
+preserves-⊆ (f 2ADT.⟨ l , r ⟩) config =
+    NADT.⟦ NADTChoice (f Choice.⟨ translate l ∷ translate r ∷ [] ⟩) ⟧ config
+  ≡⟨⟩
+    NADT.⟦ List.find-or-last (config f) (translate l ∷ translate r ∷ []) ⟧ config
+  ≡⟨ Eq.cong₂ NADT.⟦_⟧ lemma refl ⟩
+    NADT.⟦ if fnoc config f then translate l else translate r ⟧ config
+  ≡⟨ Bool.push-function-into-if (λ e → NADT.⟦ e ⟧ config) (fnoc config f) ⟩
+    (if fnoc config f then NADT.⟦ translate l ⟧ config else NADT.⟦ translate r ⟧ config)
+  ≡⟨ Eq.cong₂ (if fnoc config f then_else_) (preserves-⊆ l config) (preserves-⊆ r config) ⟩
+    (if fnoc config f then 2ADT.⟦ l ⟧ (fnoc config) else 2ADT.⟦ r ⟧ (fnoc config))
+  ≡⟨⟩
+    2ADT.⟦ f Lang.2ADT.⟨ l , r ⟩ ⟧ (fnoc config)
+  ∎
+  where
+  lemma : List.find-or-last (config f) (translate l ∷ translate r ∷ []) ≡ (if fnoc config f then translate l else translate r)
+  lemma with config f
+  ... | zero = refl
+  ... | suc _ = refl
+
+preserves-⊇ : ∀ {F : 𝔽} {A : 𝔸} → (expr : 2ADT F A) → 2ADT.⟦ expr ⟧ ⊆[ conf ] NADT.⟦ translate expr ⟧
+preserves-⊇ (2ADT.leaf v) config = refl
+preserves-⊇ (f 2ADT.⟨ l , r ⟩) config =
+    2ADT.⟦ f Lang.2ADT.⟨ l , r ⟩ ⟧ config
+  ≡⟨⟩
+    (if config f then 2ADT.⟦ l ⟧ config else 2ADT.⟦ r ⟧ config)
+  ≡⟨ Eq.cong₂ (if config f then_else_) (preserves-⊇ l config) (preserves-⊇ r config) ⟩
+    (if config f then NADT.⟦ translate l ⟧ (conf config) else NADT.⟦ translate r ⟧ (conf config))
+  ≡˘⟨ Bool.push-function-into-if (λ e → NADT.⟦ e ⟧ (conf config)) (config f) ⟩
+    NADT.⟦ if config f then translate l else translate r ⟧ (conf config)
+  ≡⟨ Eq.cong₂ NADT.⟦_⟧ lemma refl ⟩
+    NADT.⟦ List.find-or-last (conf config f) (translate l ∷ translate r ∷ []) ⟧ (conf config)
+  ≡⟨⟩
+    NADT.⟦ NADTChoice (f Choice.⟨ translate l ∷ translate r ∷ [] ⟩) ⟧ (conf config)
+  ∎
+  where
+  lemma : (if config f then translate l else translate r) ≡ List.find-or-last (conf config f) (translate l ∷ translate r ∷ [])
+  lemma with config f
+  ... | true = refl
+  ... | false = refl
+
+preserves : ∀ {F : 𝔽} {A : 𝔸} → (expr : 2ADT F A) → NADT.⟦ translate expr ⟧ ≅[ fnoc ][ conf ] 2ADT.⟦ expr ⟧
+preserves expr = preserves-⊆ expr and preserves-⊇ expr
+
+2ADT→NADT : ∀ {i : Size} {F : 𝔽} → LanguageCompiler (2ADTL F) (NADTL F)
+2ADT→NADT .LanguageCompiler.compile = translate
+2ADT→NADT .LanguageCompiler.config-compiler expr .to = conf
+2ADT→NADT .LanguageCompiler.config-compiler expr .from = fnoc
+2ADT→NADT .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr)
+
+NADT≽2ADT : ∀ {F : 𝔽} → NADTL F ≽ 2ADTL F
+NADT≽2ADT = expressiveness-from-compiler 2ADT→NADT

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

@@ -0,0 +1,81 @@
+{-# OPTIONS --sized-types #-}
+
+open import Framework.Construct using (_∈ₛ_)
+open import Construct.Artifact using () renaming (Syntax to Artifact)
+
+module Translation.Lang.NADT-to-CCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+
+open import Construct.Choices
+open import Construct.GrulerArtifacts using (leaf)
+import Data.EqIndexedSet as IndexedSet
+import Data.List.NonEmpty as List⁺
+open import Data.Product using (proj₂)
+open import Framework.Compiler using (LanguageCompiler)
+open import Framework.Definitions
+open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
+open import Framework.Relation.Function using (from; to)
+open import Framework.Variants using (VariantEncoder)
+open import Function using (id)
+open import Relation.Binary.PropositionalEquality as Eq using (refl; _≗_)
+open import Size using (Size; ∞)
+import Util.List as List
+
+open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎)
+open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[])
+
+import Lang.NADT
+module NADT where
+  open Lang.NADT Variant using (NADT; NADTAsset; NADTChoice) renaming (NADTVL to NADTL) public
+  module NADT-Sem {F} = Lang.NADT Variant F
+  open NADT-Sem using () renaming (semantics to ⟦_⟧) public -- TODO
+open NADT using (NADT; NADTAsset; NADTChoice; NADTL)
+
+import Lang.CCC
+module CCC where
+  open Lang.CCC public
+  module CCC-Sem-1 F = Lang.CCC.Sem F Variant Artifact∈ₛVariant
+  open CCC-Sem-1 using (CCCL) public
+  module CCC-Sem-2 {F} = Lang.CCC.Sem F Variant Artifact∈ₛVariant
+  open CCC-Sem-2 using (⟦_⟧) public
+open CCC using (CCC; CCCL; _-<_>-; _⟨_⟩)
+
+
+translate : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → VariantEncoder Variant (CCCL F) → NADT F i A → CCC F ∞ A
+translate Variant→CCC (NADTAsset (leaf v)) = LanguageCompiler.compile Variant→CCC v
+translate Variant→CCC (NADTChoice (f Choice.⟨ alternatives ⟩)) = f CCC.⟨ List⁺.map (translate Variant→CCC) alternatives ⟩
+
+preserves-≗ : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → (Variant→CCC : VariantEncoder Variant (CCCL F)) → (expr : NADT F i A) → CCC.⟦ translate Variant→CCC expr ⟧ ≗ NADT.⟦ expr ⟧
+preserves-≗ {A = A} Variant→CCC (NADTAsset (leaf v)) config =
+    CCC.⟦ translate Variant→CCC (NADTAsset (leaf v)) ⟧ config
+  ≡⟨⟩
+    CCC.⟦ LanguageCompiler.compile Variant→CCC v ⟧ config
+  ≡⟨ proj₂ (LanguageCompiler.preserves Variant→CCC v) config ⟩
+    v
+  ≡⟨⟩
+    NADT.⟦ NADTAsset (leaf v) ⟧ config
+  ∎
+preserves-≗ Variant→CCC (NADTChoice (f Choice.⟨ alternatives ⟩)) config =
+    CCC.⟦ translate Variant→CCC (NADTChoice (f Choice.⟨ alternatives ⟩)) ⟧ config
+  ≡⟨⟩
+    CCC.⟦ f ⟨ List⁺.map (translate Variant→CCC) alternatives ⟩ ⟧ config
+  ≡⟨⟩
+    CCC.⟦ List.find-or-last (config f) (List⁺.map (translate Variant→CCC) alternatives) ⟧ config
+  ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (List.map-find-or-last (translate Variant→CCC) (config f) alternatives) refl ⟩
+    CCC.⟦ translate Variant→CCC (List.find-or-last (config f) alternatives) ⟧ config
+  ≡⟨ preserves-≗ Variant→CCC (List.find-or-last (config f) alternatives) config ⟩
+    NADT.⟦ List.find-or-last (config f) alternatives ⟧ config
+  ≡⟨⟩
+    NADT.⟦ NADTChoice (f Choice.⟨ alternatives ⟩) ⟧ config
+  ∎
+
+preserves : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → (Variant→CCC : VariantEncoder Variant (CCCL F)) → (expr : NADT F i A) → CCC.⟦ translate Variant→CCC expr ⟧ ≅[ id ][ id ] NADT.⟦ expr ⟧
+preserves Variant→CCC expr = ≗→≅[] (preserves-≗ Variant→CCC expr)
+
+NADT→CCC : ∀ {i : Size} {F : 𝔽} → VariantEncoder Variant (CCCL F) → LanguageCompiler (NADTL F) (CCCL F)
+NADT→CCC Variant→CCC .LanguageCompiler.compile = translate Variant→CCC
+NADT→CCC Variant→CCC .LanguageCompiler.config-compiler expr .to = id
+NADT→CCC Variant→CCC .LanguageCompiler.config-compiler expr .from = id
+NADT→CCC Variant→CCC .LanguageCompiler.preserves expr = ≅[]-sym (preserves Variant→CCC expr)
+
+CCC≽NADT : ∀ {F : 𝔽} → VariantEncoder Variant (CCCL F) → CCCL F ≽ NADTL F
+CCC≽NADT Variant→CCC = expressiveness-from-compiler (NADT→CCC Variant→CCC)