```agda
{-# OPTIONS --allow-unsolved-metas #-}
```

# Translating Variability Languages

```agda
module Vatras.Tutorial.B_Translation where

open import Data.Product using (_,_)
open import Data.List using (List)

open import Size using (Size)

open import Vatras.Framework.Definitions
open import Vatras.Framework.Relation.Function using (_⇔_)
open import Vatras.Framework.VariabilityLanguage
open import Vatras.Framework.Compiler using (LanguageCompiler)
```

In this tutorial, we are going to translate our new language from the last tutorial
to another variability language.
So first, we are going to import our previous definitions.
```agda
open import Vatras.Tutorial.A_NewLanguage
```

Let's assume, we want to later prove that our new language is at least as expressive
as binary choice calculus (`2CC`).
We hence want to translate binary choice calculus to our new language:
```agda
open import Vatras.Lang.All
open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩) renaming (⟦_⟧ to ⟦_⟧₂)
```

Translating a variability language requires two steps.

## Translation of Syntax

First, we have to translate terms in one language to terms in another language.
```agda
translate : ∀ {i : Size} {A : 𝔸} → 2CC F i A → MyLang A
translate (a -< cs >-)  = {!!}
translate (D ⟨ l , r ⟩) = {!!}
```

To complete this translation functions, we have to create a new expression of type `MyLang` for
every syntactical case of binary choice calculus.
This means, we have to translate artifacts `a -< cs >-` as well as binary choices `D ⟨ l , r ⟩`.

Since `2CC` is implemented as a sized type, we also have to give a size `i` here.
Moreover, `2CC` is parameterized in the type of dimensions (i.e., what type the dimension `D` in a choice
inhibits).
Often, this will be strings or natural numbers.

## Translation of Configurations

Second, we also have to translate configurations.
Translating a configuration tells us how to configure the translated expression to obtain the same
variant as we would get when confguring the input translation.
To prove that our translation is correct (i.e., preserves semantics),
we need to supply translations of configurations in both directions.
This is necessary to ensure that the translated expression denotes exactly the
same set of variants:
not less, which is checked by `conf`,
and not more, which is checked by `fnoc`.

```agda
conf : ∀ {F : 𝔽} {i : Size} {A : 𝔸}
  → 2CC F i A
  → 2CC.Configuration F → MyConfig
conf e c²ᶜᶜ = {!!}

fnoc : ∀ {F : 𝔽} {i : Size} {A : 𝔸}
  → 2CC F i A
  → MyConfig → 2CC.Configuration F
fnoc e cᵐʸ = {!!}
```

Sometimes, translating a configuration depends on
the actual expression we are translating.
Hence, we supply the input `2CC` expression we
are translating to `MyLang` as an input as well.
If you do not need this input expression,
you may remove it as an input from `conf` and `fnoc`

## Proving Correctness

We can now prove that our translation preserves semantics.
Therefore, we have to show that the translated expression
describes exactly the same set of variants as our input
expression. We do this by proving that the input expression
denotes a subset of the variants of the translated expression
and vice versa.

So our goal is to prove the following, where
`⟦_⟧₂` is the semantics of `2CC`, and
`⟦_⟧` is the semantics of `MyLang`.
```agda
open import Vatras.Data.EqIndexedSet

preservation : ∀ {A : 𝔸} {i : Size}
  → (e : 2CC F i A)
  → ⟦ e ⟧₂ ≅ ⟦ translate e ⟧
```

`≅` is equality of indexed sets as defined in our paper.
Here, it is defined in the `Data.IndexedSet`, which we import
here via the auxiliary module `Data.EqIndexedSet` which fixes
the underlying equivalence relation on the target set to
propositional equaility `≡`.
You may want to look up the definition of `≅` (e.g., via `g d`
in normal mode in Vim or Emacs with evil).

`preservation` simplifies to proving a subset relation in both
directions as explained before.

```agda
preservation-⊆ : ∀ {A : 𝔸} {i : Size}
  → (e : 2CC F i A)
  → ⟦ e ⟧₂ ⊆ ⟦ translate e ⟧

preservation-⊇ : ∀ {A : 𝔸} {i : Size}
  → (e : 2CC F i A)
  → ⟦ translate e ⟧ ⊆ ⟦ e ⟧₂
```

Both theorems require us to prove that
for any variant generated by configuration in the left-hand expression,
there is a configuration for the right-hand expression that produces the same variant.
By may find these other variants in terms of
our translations of configurations, defined earlier.

To make explicit the translation of indices in indexed sets,
indexed sets come with dual definitions of its basic relations:

| Indexed Set Relation | Relation with Explicit Translation of Indices |
| ----- | ----------- |
| `_⊆_` | `_⊆[_]_`    |
| `_≅_` | `_≅[_][_]_` |

where the relations with explicit translation expect a function that
translates the index as an additional argument within the square
brackets `[_]`.
Equivalence `_≅[_][_]_` requires two functions, one for each subset direction.
Whereas the ordinary relations just state that an index must exist,
the relations with translations dictate that that index must be given by
applying the translation function to the input index.
You should check out the definitions in the `Data.IndexedSet` module.

Navigate to the following holes and check what is expected to prove.
You will see that you will have to prove that the input expression `e`,
when configured with `c` yields the same variants as the translated / original
expression when configured with `conf c` or `fnoc c` respectively.

> Note that finished the following proofs require that `2CC`
> can actually be translated to your language. This means, your
> language must be expressive enough to actually model `2CC`.
> Otherwise you won't be able to close the following goals
> (but you may still proceed in reading this tutorial).

```agda
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)

preservation-⊆[] : ∀ {A : 𝔸} {i : Size}
  → (e : 2CC F i A)
  → ⟦ e ⟧₂ ⊆[ conf e ] ⟦ translate e ⟧
preservation-⊆[] e c = {!!}

preservation-⊇[] : ∀ {A : 𝔸} {i : Size}
  → (e : 2CC F i A)
  → ⟦ translate e ⟧ ⊆[ fnoc e ] ⟦ e ⟧₂
preservation-⊇[] e c = {!!}
```

We can now prove that preservation in both directions
because we have shown that this property holds when
translating configurations via `conf` and `fnoc`, respectively.

```agda
preservation-⊆ e = ⊆[]→⊆ (preservation-⊆[] e)
preservation-⊇ e = ⊆[]→⊆ (preservation-⊇[] e)
```

We may now conclude preservation.
```agda
preservation e = preservation-⊆ e , preservation-⊇ e
```

## Bringing it All Together

Using our above proofs, we can now instantiate a
`LanguageCompiler` from our framework to make
our translation available, composable, and reusable
within our framework. In particular,
we may use our compiler to later on conclude theorems
about expressiveness, completeness, our soundness (see later tutorials).

First, we group `conf` and `fnoc` in a compiler for configurations.
This could also be inlined later on if you prefer.
```agda
config-compiler : ∀ {F : 𝔽} {i : Size} {A : 𝔸}
  → 2CC F i A
  → 2CC.Configuration F ⇔ MyConfig
config-compiler e = record
  { to   = conf e
  ; from = fnoc e
  }
```

A compiler requires a stronger version of preservation.
It requires that preservation is satisfied exactly by
the supplied translations for configurations. Luckily,
we can reuse our above definitions anyway.
```agda
preservation[] : ∀ {A : 𝔸} {i : Size}
  → (e : 2CC F i A)
  → ⟦ e ⟧₂ ≅[ conf e ][ fnoc e ] ⟦ translate e ⟧
preservation[] e = preservation-⊆[] e , preservation-⊇[] e
```

Finally, we can define compiler by sticking the pieced together.
Note that the compiler takes the `VariabilityLanguage` instances
as arguments (not the syntax `2CC` and `MyLang`) which is
necessary to inform the compiler about the language's semantics
and configuration type as well.
```agda
my-compiler : LanguageCompiler (2CCL F) MyVarLang
my-compiler = record
  { compile         = translate
  ; config-compiler = config-compiler
  ; preserves       = preservation[]
  }
```
