Require DecidableEquality for artifacts

`DecidableEquality` is required for `FST`s and shouldn't practically
restrict the artifact type because in practice this will always be the
case (e.g. Git also relies upon this).

src/Construct/Artifact.agda

@@ -2,7 +2,7 @@ module Construct.Artifact where
 
 open import Data.List using (List; map)
 open import Data.List.Properties using (map-cong; map-∘)
-open import Data.Product using (proj₁; proj₂; _,_)
+open import Data.Product using (_,_)
 open import Level using (_⊔_)
 open import Function using (id; flip; _$_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
@@ -17,7 +17,7 @@ import Data.IndexedSet
 open import Construct.Plain.Artifact public
 
 Syntax : ℂ
-Syntax E A = Artifact A (E A)
+Syntax E A = Artifact (artifactType A) (E A)
 
 Construct : PlainConstruct
 Construct = Plain-⟪ Syntax , (λ Γ e c → map-children (flip (Semantics Γ) c) e) ⟫

src/Construct/GrulerArtifacts.agda

@@ -23,15 +23,15 @@ record ParallelComposition {ℓ} (A : Set ℓ) : Set ℓ where
 
 module VLLeaf where
   Syntax : ℂ
-  Syntax _ A = Leaf A
+  Syntax _ A = Leaf (artifactType A)
 
   make-leaf :
     ∀ {E : 𝔼} → Syntax ∈ₛ E
-    → {A : 𝔸} → A
+    → {A : 𝔸} → artifactType A
     → E A
   make-leaf mkLeaf a = cons mkLeaf (leaf a)
 
-  elim-leaf : ∀ {V} → Syntax ∈ₛ V → ∀ {A} → Leaf A → V A
+  elim-leaf : ∀ {V} → Syntax ∈ₛ V → ∀ {A} → Leaf (artifactType A) → V A
   elim-leaf leaf∈V l = cons leaf∈V l
 
   Construct : PlainConstruct

src/Construct/NestedChoice.agda

@@ -9,7 +9,7 @@ open import Size using (Size; ↑_)
 
 open import Construct.Choices
 
-data NestedChoice : Size → 𝔼 where
+data NestedChoice : Size → Set → Set where
   value  : ∀ {i A} → A → NestedChoice i A
   choice : ∀ {i A} → 2Choice.Syntax F (NestedChoice i A) → NestedChoice (↑ i) A
 

src/Framework/Definitions.agda

@@ -1,10 +1,11 @@
 module Framework.Definitions where
 
 open import Data.Maybe using (Maybe; just)
-open import Data.Product using (_×_; Σ-syntax; proj₁; proj₂) renaming (_,_ to _and_)
+open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂) renaming (_,_ to _and_)
 open import Data.Unit using (⊤; tt) public
 open import Function using (id; _∘_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl)
+open import Relation.Binary using (DecidableEquality)
 open import Relation.Nullary.Negation using (¬_)
 
 -- open import Level using (suc; _⊔_)
@@ -16,7 +17,10 @@ We have no assumptions on that data so its just a type.
 -- 𝔸 : ∀ {ℓ} → Set (suc ℓ)
 -- 𝔸 {ℓ} = Set ℓ
 𝔸 : Set₁
-𝔸 = Set
+𝔸 = Σ Set DecidableEquality
+
+artifactType : 𝔸 → Set
+artifactType = proj₁
 
 {-
 Variant Language.

src/Framework/Relation/Index.lagda.md

@@ -1,5 +1,5 @@
 ```agda
-open import Framework.Definitions using (𝕍)
+open import Framework.Definitions using (𝕍; 𝔸)
 module Framework.Relation.Index (V : 𝕍) where
 
 open import Level using (0ℓ)
@@ -15,7 +15,7 @@ Two indices are equivalent for an expression when they produce the same output f
 ```agda
 𝕃 = VariabilityLanguage V
 
-module _ {A : Set} where
+module _ {A : 𝔸} where
   _∋_⊢_≣ⁱ_ :
     ∀ (L : 𝕃)
     → Expression L A

src/Framework/Variants.agda

@@ -9,20 +9,20 @@ open import Data.List using ([]; _∷_; map)
 open import Function using (id; _∘_; flip)
 open import Size using (Size; ↑_; ∞)
 
-open import Framework.Definitions using (𝕍; 𝔸)
+open import Framework.Definitions using (𝕍; 𝔸; artifactType)
 open import Framework.VariabilityLanguage
 open import Construct.Artifact as At using (_-<_>-; map-children) renaming (Syntax to Artifact; Construct to ArtifactC)
 
 open import Data.EqIndexedSet
 
 data GrulerVariant : 𝕍 where
-  asset : ∀ {A : 𝔸} (a : A) → GrulerVariant A
+  asset : ∀ {A : 𝔸} (a : artifactType A) → GrulerVariant A
   _∥_   : ∀ {A : 𝔸} (l : GrulerVariant A) → (r : GrulerVariant A) → GrulerVariant A
 
 data Rose : Size → 𝕍 where
   rose : ∀ {i} {A : 𝔸} → Artifact (Rose i) A → Rose (↑ i) A
 
-rose-leaf : ∀ {A : 𝔸} → A → Rose ∞ A
+rose-leaf : ∀ {A : 𝔸} → artifactType A → Rose ∞ A
 rose-leaf {A} a = rose (At.leaf a)
 
 -- Variants are also variability languages
@@ -46,7 +46,7 @@ RoseVL : VariabilityLanguage (Rose ∞)
 RoseVL = Variant-is-VL (Rose ∞)
 
 open import Data.String using (String; _++_; intersperse)
-show-rose : ∀ {i} {A} → (A → String) → Rose i A → String
+show-rose : ∀ {i} {A} → (artifactType A → String) → Rose i A → String
 show-rose show-a (rose (a -< [] >-)) = show-a a
 show-rose show-a (rose (a -< es@(_ ∷ _) >-)) = show-a a ++ "-<" ++ (intersperse ", " (map (show-rose show-a) es)) ++ ">-"
 

src/Lang/2CC.lagda.md

@@ -21,6 +21,7 @@ open import Data.Bool using (Bool; true; false; if_then_else_)
 open import Data.List
   using (List; []; _∷_; lookup)
   renaming (map to mapl)
+open import Data.Product using (_,_)
 open import Function using (id)
 open import Size using (Size; ↑_; ∞)
 
@@ -91,7 +92,7 @@ Some transformation rules:
     open Sem V mkArtifact
 
     module _ {A : 𝔸} where
-      ast-factoring : ∀ {i} {D : Dimension} {a : A} {n : ℕ}
+      ast-factoring : ∀ {i} {D : Dimension} {a : artifactType A} {n : ℕ}
         → (xs ys : Vec (2CC Dimension i A) n)
           -------------------------------------------------------------------------------------
         → 2CCL Dimension ⊢
@@ -189,25 +190,25 @@ Some transformation rules:
   open Data.List using (concatMap) renaming (_++_ to _++l_)
 
   -- get all dimensions used in a binary CC expression
-  dims : ∀ {i : Size} {A : Set} → 2CC Dimension i A → List Dimension
+  dims : ∀ {i : Size} {A : 𝔸} → 2CC Dimension i A → List Dimension
   dims (_ -< es >-) = concatMap dims es
   dims (D ⟨ l , r ⟩) = D ∷ (dims l ++l dims r)
 ```
 
 ## Show
 
 ```agda
-  open import Data.String using (String; _++_; intersperse)
+  open import Data.String as String using (String; _++_; intersperse)
   module Pretty (show-D : Dimension → String) where
     open import Show.Lines
 
-    show : ∀ {i} → 2CC Dimension i String → String
+    show : ∀ {i} → 2CC Dimension i (String , 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} → 2CC Dimension i String → Lines
+    pretty : ∀ {i : Size} → 2CC Dimension i (String , String._≟_) → Lines
     pretty (a -< [] >-) = > a
     pretty (a -< es@(_ ∷ _) >-) = do
       > a ++ "-<"

src/Lang/CCC.lagda.md

@@ -187,18 +187,18 @@ Maybe its smarter to do this for ADDs and then to conclude by transitivity of tr
   -- get all dimensions used in a CCC Dimension expression
   open Data.List using (concatMap)
 
-  dims : ∀ {i : Size} {A : Set} → CCC Dimension i A → List Dimension
+  dims : ∀ {i : Size} {A : 𝔸} → CCC Dimension i A → List Dimension
   dims (_ -< es >-) = concatMap dims es
   dims (D ⟨ es ⟩) = D ∷ concatMap dims (toList es)
 ```
 
 ## Show
 
 ```agda
-  open import Data.String using (String; _++_)
+  open import Data.String as String using (String; _++_)
 
-  show : ∀ {i} → (Dimension → String) → CCC Dimension i String → String
+  show : ∀ {i} → (Dimension → String) → CCC Dimension i (String , String._≟_) → String
   show _ (a -< [] >-) = a
   show show-D (a -< es@(_ ∷ _) >- ) = a ++ "-<" ++ (foldl _++_ "" (map (show show-D) es)) ++ ">-"
-  show show-D (D ⟨ es ⟩) = show-D D ++ "⟨" ++ (Data.String.intersperse ", " (toList (map⁺ (show show-D) es))) ++ "⟩"
+  show show-D (D ⟨ es ⟩) = show-D D ++ "⟨" ++ (String.intersperse ", " (toList (map⁺ (show show-D) es))) ++ "⟩"
 ```

src/Lang/Gruler.agda

@@ -23,7 +23,7 @@ private
   pc-semantics = PlainConstruct-Semantics VLParallelComposition.Construct VLParallelComposition.ParallelComposition∈ₛGrulerVariant
 
 data Gruler : Size → 𝔼 where
-  GAsset  : ∀ {i A} → Leaf A                           → Gruler i A
+  GAsset  : ∀ {i A} → Leaf (artifactType A)            → Gruler i A
   GPComp  : ∀ {i A} → ParallelComposition (Gruler i A) → Gruler (↑ i) A
   GChoice : ∀ {i A} → VL2Choice.Syntax F (Gruler i) A  → Gruler (↑ i) A
 
@@ -42,7 +42,7 @@ gruler-has-leaf {i} = record
   ; snoc = snoc'
   ; id-l = λ _ → refl
   }
-  where snoc' : ∀ {A} → Gruler i A → Maybe (Leaf A)
+  where snoc' : ∀ {A} → Gruler i A → Maybe (Leaf (artifactType A))
         snoc' (GAsset A)  = just A
         snoc' _ = nothing
 

src/Lang/NCC.lagda.md

@@ -26,6 +26,7 @@ open import Data.Bool using (Bool; true; false; if_then_else_)
 open import Data.List
   using (List; []; _∷_; lookup)
   renaming (map to mapl)
+open import Data.Product using (_,_)
 open import Function using (id)
 open import Size using (Size; ↑_; ∞)
 
@@ -74,25 +75,25 @@ module _ {n : ℕ≥ 2} {Dimension : 𝔽} where
   import Data.Vec as Vec
 
   -- get all dimensions used in a binary CC expression
-  dims : ∀ {i : Size} {A : Set} → NCC n Dimension i A → List Dimension
+  dims : ∀ {i : Size} {A : 𝔸} → NCC n Dimension 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)
+  open import Data.String as String using (String; _++_; intersperse)
   module Pretty (show-D : Dimension → String) where
     open import Show.Lines
 
-    show : ∀ {i} → NCC n Dimension i String → String
+    show : ∀ {i} → NCC n Dimension i (String , 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 n Dimension i String → Lines
+    pretty : ∀ {i : Size} → NCC n Dimension i (String , String._≟_) → Lines
     pretty (a -< [] >-) = > a
     pretty (a -< es@(_ ∷ _) >-) = do
       > a ++ "-<"

src/Lang/OC.lagda.md

@@ -19,7 +19,7 @@ module Lang.OC where
 ```agda
 open import Data.Bool using (Bool; true; false; if_then_else_)
 open import Data.List using (List; []; _∷_)
-open import Data.String using (String)
+open import Data.String as String using (String)
 open import Size using (Size; ∞; ↑_)
 open import Function using (_∘_)
 
@@ -46,7 +46,7 @@ data OC (Option : 𝔽) : Size → 𝔼 where
   Maybe reusing Artifact hides something from the Agda
   compiler that it needs for termination checking.
   -}
-  _-<_>- : ∀ {i A} → A → List (OC Option i A) → OC Option (↑ i) A
+  _-<_>- : ∀ {i A} → artifactType A → List (OC Option i A) → OC Option (↑ i) A
   _❲_❳ : ∀ {i : Size} {A : 𝔸} →
     Option → OC Option i A → OC Option (↑ i) A
 infixl 6 _❲_❳
@@ -144,7 +144,7 @@ And now for the semantics of well-formed option calculus which just reuses the s
 
 ```agda
 open import Data.Fin using (zero; suc)
-open import Data.Nat using (ℕ; zero; suc)
+open import Data.Nat as ℕ using (ℕ; zero; suc)
 open import Data.Product   using (_,_; ∃-syntax; ∄-syntax)
 open import Util.Existence using (_,_)
 open import Data.List.Relation.Unary.All using (_∷_; [])
@@ -163,12 +163,12 @@ As our counter example, we use the set `{0, 1}` as our variants:
   -- TODO: Can this be generalized to other types of variants as well?
   module IncompleteOnRose where
     open import Framework.Variants using (Rose; Artifact∈ₛRose)
-    open import Framework.VariantMap (Rose ∞) ℕ
+    open import Framework.VariantMap (Rose ∞) (ℕ , ℕ._≟_)
     open import Framework.Properties.Completeness (Rose ∞) using (Incomplete)
     open Sem (Rose ∞) Artifact∈ₛRose
 
-    variant-0 = rose-leaf 0
-    variant-1 = rose-leaf 1
+    variant-0 = rose-leaf {A = (ℕ , ℕ._≟_)} 0
+    variant-1 = rose-leaf {A = (ℕ , ℕ._≟_)} 1
     -- variant-0 = cons mkArtifact (At.leaf 0)
     -- variant-1 = cons mkArtifact (At.leaf 1)
 
@@ -183,7 +183,7 @@ So we show that given an expression `e`, a proof that `e` can be configured to `
 ```agda
     does-not-describe-variants-0-and-1 :
       ∀ {i : Size}
-      → (e : WFOC Option i ℕ)
+      → (e : WFOC Option i (ℕ , ℕ._≟_))
       → ∃[ c ] (variant-0 ≡ ⟦ e ⟧ c)
       → ∄[ c ] (variant-1 ≡ ⟦ e ⟧ c)
     -- If e has 0 as root, it may be configured to 0 but never to 1.
@@ -208,14 +208,14 @@ Another way is to enrich the annotation language, for example using propositiona
 ## Utility
 
 ```agda
-  oc-leaf : ∀ {i : Size} {A : 𝔸} → A → OC Option (↑ i) A
+  oc-leaf : ∀ {i : Size} {A : 𝔸} → artifactType A → OC Option (↑ i) A
   oc-leaf a = a -< [] >-
 
   -- alternative name that does not require writing tortoise shell braces
   opt : ∀ {i : Size} {A : 𝔸} → Option → OC Option i A → OC Option (↑ i) A
   opt O = _❲_❳ O
 
-  singleton : ∀ {i : Size} {A : 𝔸} → A → OC Option i A → OC Option (↑ i) A
+  singleton : ∀ {i : Size} {A : 𝔸} → artifactType A → OC Option i A → OC Option (↑ i) A
   singleton a e = a -< e ∷ [] >-
 
   open import Util.Named
@@ -233,15 +233,15 @@ Another way is to enrich the annotation language, for example using propositiona
 ## Show
 
 ```agda
-open Data.String using (_++_; intersperse)
+open String using (_++_; intersperse)
 open import Function using (_∘_)
 
 module Show (Option : 𝔽) (print-opt : Option → String) where
-  show-oc : ∀ {i : Size} → OC Option i String → String
+  show-oc : ∀ {i : Size} → OC Option i (String , String._≟_) → String
   show-oc (s -< [] >-) = s
   show-oc (s -< es@(_ ∷ _) >-) = s ++ "-<" ++ (intersperse ", " (map show-oc es)) ++ ">-"
   show-oc (O ❲ e ❳) = print-opt O ++ "❲" ++ show-oc e ++ "❳"
 
-  show-wfoc : ∀ {i : Size} → WFOC Option i String → String
+  show-wfoc : ∀ {i : Size} → WFOC Option i (String , String._≟_) → String
   show-wfoc = show-oc ∘ forgetWF
 ```

src/Test/Examples/CCC.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --sized-types #-}
 module Test.Examples.CCC where
 
-open import Data.String using (String)
+open import Data.String as String using (String)
 open import Data.List using (List; _∷_; [])
 open import Data.List.NonEmpty
   using (List⁺; _∷_; toList)
@@ -11,26 +11,27 @@ open import Data.Product
 open import Size
   using (Size; ∞; ↑_)
 
+open import Framework.Definitions using (𝔸; artifactType)
 open import Construct.Plain.Artifact using (leaf; leaves⁺)
 
 open import Lang.All
 open CCC -- use strings as dimensions
 open import Test.Example
 
 CCCExample : Set
-CCCExample = Example (CCC String ∞ String)
+CCCExample = Example (CCC String ∞ (String , String._≟_))
 
 -- some smart constructors
-ccA : ∀ {i : Size} {A : Set} → List⁺ (CCC String i A) → CCC String (↑ i) A
+ccA : ∀ {i : Size} {A : 𝔸} → List⁺ (CCC String i A) → CCC String (↑ i) A
 ccA es = "A" ⟨ es ⟩
 
-cc-leaves : ∀ {i : Size} {A : Set} → String → List⁺ A → CCC String (↑ ↑ i) A
+cc-leaves : ∀ {i : Size} {A : 𝔸} → String → List⁺ (artifactType A) → CCC String (↑ ↑ i) A
 cc-leaves D es = D ⟨ map⁺ atom (leaves⁺ es) ⟩
 
-ccA-leaves : ∀ {i : Size} {A : Set} → List⁺ A → CCC String (↑ ↑ i) A
+ccA-leaves : ∀ {i : Size} {A : 𝔸} → List⁺ (artifactType A) → CCC String (↑ ↑ i) A
 ccA-leaves = cc-leaves "A"
 
-cc-leaf : ∀ {i : Size} {A : Set} → A → CCC String (↑ i) A
+cc-leaf : ∀ {i : Size} {A : 𝔸} → (artifactType A) → CCC String (↑ i) A
 cc-leaf a = atom (leaf a)
 
 -- examples

src/Test/Examples/OC.agda

@@ -3,7 +3,8 @@
 module Test.Examples.OC where
 
 open import Data.List using (List; []; _∷_; [_])
-open import Data.String using (String)
+open import Data.String as String using (String)
+open import Data.Product using (_,_)
 open import Size using (Size; ↑_; ∞)
 
 -- open import Framework.Annotation.Name using (Option)
@@ -14,7 +15,7 @@ open OC
 open import Test.Example
 
 OCExample : Set
-OCExample = Example (WFOC String ∞ String)
+OCExample = Example (WFOC String ∞ (String , String._≟_))
 
 optex-unary : OCExample
 optex-unary = "unary" ≔ (Root "r" [ opt "O" (oc-leaf "lol") ])