Merge pull request #18 from pmbittner/sound

2ADT -> VariantList

src/Lang/2ADT.agda

@@ -1,25 +1,21 @@
-{-# OPTIONS --sized-types #-}
-
 open import Framework.Definitions
--- TODO: Generalize level of F
-module Lang.2ADT (F : 𝔽) where
-
-open import Data.Bool using (Bool)
-open import Function using (id)
-open import Size using (Size; ↑_)
+module Lang.2ADT (F : 𝔽) (V : 𝕍) where
 
+open import Data.Bool using (Bool; if_then_else_)
 open import Framework.VariabilityLanguage
-open import Framework.Variants using (GrulerVariant)
-open import Construct.GrulerArtifacts
-open import Construct.Choices
-open import Construct.NestedChoice F as NestedChoice using (NestedChoice)
 
-2ADT : Size → 𝔼
-2ADT i A = NestedChoice i (Leaf A)
+data 2ADT : 𝔼 where
+  leaf   : ∀ {A} → V A → 2ADT A
+  _⟨_,_⟩ : ∀ {A} → (D : F) → (l : 2ADT A) → (r : 2ADT A) → 2ADT A
+
+Configuration : Set
+Configuration = F → Bool
 
-mutual
-  2ADTVL : ∀ {i : Size} → VariabilityLanguage GrulerVariant
-  2ADTVL {i} = ⟪ 2ADT i , 2Choice.Config F , semantics ⟫
+⟦_⟧ : 𝔼-Semantics V Configuration 2ADT
+⟦ leaf v      ⟧ _ = v
+⟦ D ⟨ l , r ⟩ ⟧ c = if c D
+                    then ⟦ l ⟧ c
+                    else ⟦ r ⟧ c
 
-  semantics : ∀ {i : Size} → 𝔼-Semantics GrulerVariant (2Choice.Config F) (2ADT i)
-  semantics e c = VLLeaf.elim-leaf VLLeaf.Leaf∈ₛGrulerVariant (NestedChoice.⟦ e ⟧ c)
+2ADTL : VariabilityLanguage V
+2ADTL = ⟪ 2ADT , Configuration , ⟦_⟧ ⟫

src/Lang/2ADT/Path.agda

@@ -0,0 +1,203 @@
+open import Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼)
+open import Relation.Binary using (DecidableEquality; Rel)
+module Lang.2ADT.Path
+  (F : 𝔽)
+  (V : 𝕍)
+  (_==_ : DecidableEquality F)
+  where
+
+open import Level using (0ℓ)
+open import Function using (_∘_)
+
+open import Data.Bool using (Bool; true; false; if_then_else_)
+open import Data.Empty using (⊥-elim)
+open import Data.List using (List; []; _∷_)
+open import Data.List.Relation.Unary.Any using (Any; here; there)
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
+open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
+open import Data.Product using (_×_; ∃-syntax)
+
+open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Decidable using (yes; no; False; True; isYes; fromWitness; toWitness; fromWitnessFalse; toWitnessFalse)
+open import Relation.Binary using (Decidable; Symmetric)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
+open Eq.≡-Reasoning
+
+open import Framework.VariabilityLanguage
+open import Util.Suffix using (_endswith_)
+open import Lang.2ADT F V using (2ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧)
+
+-- A selection of a feature matches it to a boolean value.
+record Selection : Set where
+  constructor _↣_
+  field
+    feature : F
+    value : Bool
+open Selection public
+
+-- A list of selection which denotes a path from the root of a 2ADT to a leaf node.
+Path : Set
+Path = List Selection
+
+-- Two Selections are considered different iff they have different features.
+-- Notable, (A ↣ true) is not different to (A ↣ false).
+different : Rel Selection 0ℓ
+different (A ↣ _) (B ↣ _) = False (A == B)
+
+sym-different : Symmetric different
+sym-different neq = fromWitnessFalse λ eq → toWitnessFalse neq (sym eq)
+
+-- Two selections are considered the same of they assign the same feature.
+same : Rel Selection 0ℓ
+same (A ↣ _) (B ↣ _) = True (A == B)
+
+-- Checks whether a given features was assigned in a selection.
+is : F → Selection → Set
+is A (B ↣ _) = True (A == B)
+
+is-refl : ∀ (D : F) → (b : Bool) → is D (D ↣ b)
+is-refl _ _ = fromWitness refl
+
+==-isYes-refl : ∀ (D : F) → isYes (D == D) ≡ true
+==-isYes-refl D with D == D
+... | yes refl = refl
+... | no D≠D = ⊥-elim (D≠D refl)
+
+-- Checks whether a feature is assigned somewhere in a path.
+_∈_ : F → Path → Set
+a ∈ as = Any (is a) as
+
+_∉_ : F → Path → Set
+D ∉ fs = ¬ (D ∈ fs)
+
+∉-head : ∀ {D x xs} → D ∉ (x ∷ xs) → (b : Bool) → different x (D ↣ b)
+∉-head D∉x∷xs b = fromWitnessFalse λ x≡D → D∉x∷xs (here (fromWitness (sym x≡D)))
+
+∉-tail : ∀ {D x xs} → D ∉ (x ∷ xs) → D ∉ xs
+∉-tail D∉x∷xs D∈xs = D∉x∷xs (there D∈xs)
+
+-- Finds the assigned value of a feature within a path.
+getValue : ∀ {a fs} → a ∈ fs → Bool
+getValue (here {_ ↣ value} _) = value
+getValue (there fs) = getValue fs
+
+-- Containment _∈_ is decidable.
+_∈?_ : Decidable _∈_
+a ∈? [] = no λ ()
+a ∈? ((x ↣ v) ∷ xs) with a == x
+... | yes p = yes (here (fromWitness p))
+... | no ¬p with a ∈? xs
+...   | yes q = yes (there q)
+...   | no ¬q = no nope
+  where
+    nope : ¬ Any (is a) ((x ↣ v) ∷ xs)
+    nope (here  p) = ¬p (toWitness p)
+    nope (there q) = ¬q q
+
+-- Turns an ¬ Any to a All ¬.
+-- TODO: Reuse ¬Any⇒All¬ from the standard library.
+∉→All-different : ∀ {D} → (as : Path) → D ∉ as → All (different (D ↣ true)) as
+∉→All-different [] _ = []
+∉→All-different (a ∷ as) nope =
+    fromWitnessFalse (λ x → nope (here (fromWitness x)))
+  ∷ ∉→All-different as λ x → nope (there x)
+
+All-different→∉ : ∀ {D} (b : Bool) (as : Path) → All (different (D ↣ b)) as → D ∉ as
+All-different→∉ b (a ∷ as) (pa ∷ pas) (here D-is-a) = toWitnessFalse pa (toWitness D-is-a)
+All-different→∉ b (a ∷ as) (pa ∷ pas) (there D∈as)  = All-different→∉ b as pas D∈as
+
+{-
+All features mentioned in the path are unique (i.e., no feature is mentioned more than once).
+This means that there cannot be conflicts in the path.
+-}
+Unique : Path → Set
+Unique = AllPairs different
+
+{-
+A path is starts at a node if it leads to a leaf.
+This relation can be seen as a type system for paths within a particular tree.
+Note: The symmetry between the rules walk-left and walk-right causes many
+      proofs to have quite some redundancy as well because we have to match
+      on these rules a lot.
+      However, we cannot merge the rules into a single rule
+      because we have to recurse on either the left or right alternative (not both).
+-}
+data _starts-at_ : ∀ {A} → (p : Path) → (e : 2ADT A) → Set where
+  tleaf : ∀ {A} {v : V A}
+      ------------------
+    → [] starts-at (leaf v)
+
+  walk-left : ∀ {A} {D : F} {l r : 2ADT A} {pl : Path}
+    → pl starts-at l
+      -------------------------------------
+    → ((D ↣ true) ∷ pl) starts-at (D ⟨ l , r ⟩)
+
+  walk-right : ∀ {A} {D : F} {l r : 2ADT A} {pr : Path}
+    → pr starts-at r
+      --------------------------------------
+    → ((D ↣ false) ∷ pr) starts-at (D ⟨ l , r ⟩)
+
+{-
+An expression does not contain a feature name
+if all paths do not contain that feature name.
+-}
+_∉'_ : ∀{A} → F → 2ADT A → Set
+D ∉' e = ∀ (p : Path) → p starts-at e → D ∉ p
+
+{-
+A path serves as a configuration for an expression e
+if it starts at that expression and ends at a leaf.
+-}
+record PathConfig {A} (e : 2ADT A) : Set where
+  constructor _is-valid_
+  field
+    path : Path
+    valid : path starts-at e
+open PathConfig public
+
+{-
+Alternative semantics of 2ADTs by walking a path.
+This walk may be illegal by choosing different alternatives for the same choice within a path.
+For example in D ⟨ D ⟨ 1 , dead ⟩ , 2 ⟩ we can reach 'dead' via (D ↣ true ∷ D ↣ false ∷ []).
+However, walking like this is fine as long as the path is unique as we will later prove.
+-}
+walk : ∀ {A} → (e : 2ADT A) → PathConfig e → V A
+walk (leaf v) ([] is-valid tleaf) = v
+walk (D ⟨ l , _ ⟩) ((.(D ↣ true ) ∷ pl) is-valid walk-left  t) = walk l (pl is-valid t)
+walk (D ⟨ _ , r ⟩) ((.(D ↣ false) ∷ pr) is-valid walk-right t) = walk r (pr is-valid t)
+
+{-
+An expression a is a sub-expression of b
+iff all valid paths from a lead to paths from b.
+-}
+_subexprof_ : ∀ {A} → 2ADT A → 2ADT A → Set
+a subexprof b = ∀ (pa : Path) → pa starts-at a → ∃[ pb ] ((pb starts-at b) × (pb endswith pa))
+
+{-
+A configuration matches a selection
+if the configuration returns the same
+result for the given feature as dictated
+by the selection.
+-}
+matches : Configuration → Selection → Set
+matches c (f ↣ val) = c f ≡ val
+
+{-
+Predicate that tells whether a path matches a configuration.
+This essentially makes the given path a partial configuration.
+-}
+_⊑_ : Path → Configuration → Set
+p ⊑ c = All (matches c) p
+
+{-
+If we make a lookup in a path for a certain feature,
+any matching configuration will yield the same result.
+-}
+lookup-partial : ∀ {p} {c} {D}
+  → p ⊑ c
+  → (has : D ∈ p)
+  → getValue has ≡ c D
+lookup-partial (refl ∷ px) (here D-is-f) rewrite toWitness D-is-f = refl
+lookup-partial (refl ∷ px) (there has) = lookup-partial px has
+

src/Lang/NADT.agda

@@ -2,7 +2,7 @@
 
 open import Framework.Definitions
 -- TODO: Generalize level of F
-module Lang.NADT (F : 𝔽) where
+module Lang.NADT (F : 𝔽) (V : 𝕍) where
 
 open import Data.Nat using (ℕ)
 open import Function using (id)
@@ -15,13 +15,13 @@ open import Construct.GrulerArtifacts
 open import Construct.Choices
 
 data NADT : Size → 𝔼 where
-  NADTAsset  : ∀ {i A} → Leaf 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
-  NADTVL : ∀ {i : Size} → VariabilityLanguage GrulerVariant
+  NADTVL : ∀ {i : Size} → VariabilityLanguage V
   NADTVL {i} = ⟪ NADT i , Choice.Config F , semantics ⟫
 
-  semantics : ∀ {i : Size} → 𝔼-Semantics GrulerVariant (Choice.Config F) (NADT i)
-  semantics (NADTAsset a) _  = VLLeaf.elim-leaf VLLeaf.Leaf∈ₛGrulerVariant a
-  semantics (NADTChoice chc) = VLChoice.Semantics GrulerVariant F NADTVL id chc
+  semantics : ∀ {i : Size} → 𝔼-Semantics V (Choice.Config F) (NADT i)
+  semantics (NADTAsset (leaf v)) _ = v
+  semantics (NADTChoice chc)       = VLChoice.Semantics V F NADTVL id chc

src/Lang/VariantList.lagda.md

@@ -1,12 +1,5 @@
 # Lists of Variants are Also Variability Languages
 
-## Options
-
-```agda
-{-# OPTIONS --sized-types #-}
-{-# OPTIONS --allow-unsolved-metas #-}
-```
-
 ## Module
 
 ```agda
@@ -23,7 +16,6 @@ open import Data.List.NonEmpty using (List⁺; _∷_; toList; length)
 open import Data.Nat using (ℕ; zero; suc)
 open import Data.Product using (∃-syntax; _,_; proj₁; proj₂)
 open import Function using (_∘_; Surjective)
-open import Size using (Size; ∞)
 
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 

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

@@ -5,14 +5,15 @@ module Translation.Lang.2ADT-to-NADT {F : 𝔽} {A : 𝔸} where
 
 open import Data.Nat using (ℕ)
 open import Level using (0ℓ)
-open import Size using (∞; ↑_)
+open import Size using (Size; ∞; ↑_)
 
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 open Eq.≡-Reasoning
 
 import Data.IndexedSet
 
 open import Construct.Choices
+open import Construct.GrulerArtifacts as GL using ()
 open import Construct.NestedChoice using (value; choice)
 
 open import Framework.Variants using (GrulerVariant)
@@ -22,9 +23,11 @@ open import Lang.NADT
 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 (Choice.map compile (convert (Eq.setoid (2ADT F i A)) c))
+{-# 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 _≋_)