From 2cae527fa3e4af08613e4f82fef881b7dddab3a1 Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Wed, 14 Dec 2022 16:27:47 +0100
Subject: [PATCH] ideas on feature traceability as semantics

---
 src/CC.lagda.md           |  1 +
 src/FeatureTrace.lagda.md | 48 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+)
 create mode 100644 src/FeatureTrace.lagda.md

diff --git a/src/CC.lagda.md b/src/CC.lagda.md
index d3fce083..23359483 100644
--- a/src/CC.lagda.md
+++ b/src/CC.lagda.md
@@ -6,6 +6,7 @@ For termination checking, we have to use sized types (i.e., types that are bound
 We use sizes to constrain the maximum tree-depth of an expression.
 ```agda
 {-# OPTIONS --sized-types #-}
+{-# OPTIONS --allow-unsolved-metas #-} -- REMOVE AT THE END!
 ```
 
 ## Module
diff --git a/src/FeatureTrace.lagda.md b/src/FeatureTrace.lagda.md
new file mode 100644
index 00000000..cfdba6ec
--- /dev/null
+++ b/src/FeatureTrace.lagda.md
@@ -0,0 +1,48 @@
+# Feature Traceability as Denotational Semantics
+
+## Options
+
+```agda
+{-# OPTIONS --sized-types #-}
+```
+
+## Module
+
+```agda
+module FeatureTrace where
+```
+
+## Imports
+
+```agda
+open import Data.Bool using (if_then_else_)
+open import Data.List using (List; _∷_; []; map; concatMap)
+open import Data.List.NonEmpty using (toList)
+
+open import Size using (Size)
+
+open import CC using (CC; Artifact; _⟨_⟩; Dimension; _dim-==_)
+open import SemanticDomains
+```
+
+## Feature Traces in Choice Calculus
+
+The semantics of a variation language is the set of variants it describes, or equivalently a generator that turns configurations into variants.
+For some use cases, yet another formulation of semantics is of interest: feature traces - the knowledge where a certain feature is implemented.
+As an example, we formulize feature traces for choice calculus:
+
+```agda
+CCFeatureTrace : Set → Set
+CCFeatureTrace A = Dimension → List A
+
+collect : {i : Size} {A : Set} → CC i A → List A
+collect = {!!}
+
+trace : {i : Size} {A : Set} → CC i A → CCFeatureTrace A
+trace (Artifact a es) qD = {!!}
+trace (D ⟨ es ⟩) qD = let les = toList es in
+                     if D dim-== qD
+                     then concatMap collect les
+                     else concatMap (λ e → trace e D) les
+```
+Note: Not so easy: Just returning the artifacts is probably too naive because similar or equal elements in the object language cannot be distinguished anymore even though they trace to different features in different locations.