Misc cleanups and improvements

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "agda-stdlib"]
 	path = agda-stdlib
-	url = git@github.com:agda/agda-stdlib.git
+	url = https://github.com/agda/agda-stdlib.git

EPVL.agda-lib

@@ -1,3 +1,4 @@
 name: EPVL
 depend: standard-library-2.0
-include: src
+include: src
+flags: --large-indices --no-forced-argument-recursion --sized-types

README.md

@@ -26,6 +26,17 @@ nix-build
 ./result/bin/EPVL
 ```
 
+To use this repository as a library in you own project, you can use `agda.withPackages`:
+```nix
+agda = nixpkgs.agda.withPackages [
+  nixpkgs.agdaPackages.standard-library
+  (import /path/to/this/git/repository {
+    pkgs = nixpkgs;
+  })
+];
+```
+Though, not required, we recommend to use the [nixpkgs pin](nix/sources.json) created using [niv](https://github.com/nmattia/niv) provided in this respository to minimize version conflicts.
+
 #### Manual Installation
 We recommend following the installation instructions from the [Programming Language Foundations in Agda](https://plfa.github.io/GettingStarted/) book to install GHC, Cabal, and Agda (no need to install the book and the standard-library, which is shipped in the right version in the subdirectory `agda-stdlib` here).
 

default.nix

@@ -11,19 +11,14 @@
 pkgs.agdaPackages.mkDerivation {
   version = "1.0";
   pname = "EPVL";
-  src = ./.;
+  src = with pkgs.lib.fileset;
+    toSource {
+      root = ./.;
+      fileset = gitTracked ./.;
+    };
 
   buildInputs = [
-    (pkgs.agdaPackages.standard-library.overrideAttrs
-      (oldAttrs: {
-        version = "1.7.2";
-        src = pkgs.fetchFromGitHub {
-          repo = "agda-stdlib";
-          owner = "agda";
-          rev = "177dc9e";
-          hash = "sha256-ovnhL5otoaACpqHZnk/ucivwtEfBQtGRu4/xw4+Ws+c=";
-        };
-      }))
+    pkgs.agdaPackages.standard-library
   ];
 
   buildPhase = ''
@@ -32,9 +27,9 @@ pkgs.agdaPackages.mkDerivation {
     make build
   '';
 
-  installPhase = ''
+  postInstall = ''
     install -D src/Main "$out/bin/$pname"
   '';
 
-  meta = {description = "On the Expressive Power of Programming Languages";};
+  meta = {description = "On the Expressive Power of Languages for Static Variability";};
 }

flake.nix

@@ -0,0 +1,13 @@
+{
+  outputs = inputs: {
+    packages.x86_64-linux.default = import inputs.self {system = "x86_64-linux";};
+    overlays.default = final: prev: {
+      agdaPackages = prev.agdaPackages.overrideScope' (self: super: {
+        (import inputs.self {
+          system = "x86_64-linux";
+          pkgs = final;
+        };)
+      });
+    };
+  };
+}

nix/sources.json

@@ -5,10 +5,10 @@
         "homepage": null,
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "4ecab3273592f27479a583fb6d975d4aba3486fe",
-        "sha256": "10wn0l08j9lgqcw8177nh2ljrnxdrpri7bp0g7nvrsn9rkawvlbf",
+        "rev": "fd281bd6b7d3e32ddfa399853946f782553163b5",
+        "sha256": "1hy81yj2dcg6kfsm63xcqf8kvigxglim1rcg1xpmy2rb6a8vqvsj",
         "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/4ecab3273592f27479a583fb6d975d4aba3486fe.tar.gz",
+        "url": "https://github.com/NixOS/nixpkgs/archive/fd281bd6b7d3e32ddfa399853946f782553163b5.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
     }
 }

src/Construct/Choices.agda

@@ -2,6 +2,7 @@
 module Construct.Choices where
 
 open import Data.Bool using (Bool; if_then_else_)
+open import Data.Bool.Properties using (if-float)
 open import Data.String using (String; _<+>_; intersperse)
 open import Level using (Level; _⊔_)
 open import Function using (_∘_)
@@ -11,8 +12,6 @@ open Eq.≡-Reasoning
 
 open import Data.EqIndexedSet as ISet
 
-open import Util.AuxProofs using (if-cong)
-
 module NChoice where
   open import Data.Fin using (Fin)
   open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥)
@@ -102,7 +101,7 @@ module 2Choice where
       ⟦ map f (D ⟨ l , r ⟩) ⟧ c
     ≡⟨⟩
       (if c D then f l else f r)
-    ≡⟨ if-cong (c D) f ⟩
+    ≡⟨ if-float f (c D) ⟨
       f (if c D then l else r)
     ≡⟨⟩
       f (⟦ D ⟨ l , r ⟩ ⟧ c)
@@ -152,7 +151,7 @@ module Choice where
       ⟦ map f (D ⟨ as ⟩) ⟧ c
     ≡⟨⟩
       find-or-last (c D) (map-list⁺ f as)
-    ≡˘⟨ map-find-or-last f (c D) as ⟩
+    ≡⟨ map-find-or-last f (c D) as ⟨
       f (find-or-last (c D) as)
     ≡⟨⟩
       f (⟦ D ⟨ as ⟩ ⟧ c)

src/Construct/GrulerArtifacts.agda

@@ -1,5 +1,3 @@
-{-# OPTIONS --sized-types #-}
-
 module Construct.GrulerArtifacts where
 
 open import Data.Maybe using (just; nothing)

src/Construct/NestedChoice.agda

@@ -1,5 +1,3 @@
-{-# OPTIONS --sized-types #-}
-
 open import Framework.Definitions
 
 module Construct.NestedChoice (F : 𝔽) where

src/Data/IndexedSet.lagda.md

@@ -3,8 +3,6 @@
 ## Module
 
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
-
 open import Level using (Level; suc; _⊔_)
 open import Relation.Binary as RB using (
   Rel;
@@ -289,7 +287,7 @@ module ⊆-Reasoning where
 
 module ≅-Reasoning where
   infix  3 _≅-∎
-  infixr 2 _≅⟨⟩_ step-≅ step-≅˘ step-≐ step-≐˘ --step-≅-by-index-translation
+  infixr 2 _≅⟨⟩_ step-≅-⟨ step-≅-⟩ step-≐-⟨ step-≐-⟩ --step-≅-by-index-translation
   infix  1 ≅-begin_
 
   ≅-begin_ : ∀{I J} {A : IndexedSet I} {B : IndexedSet J} → A ≅ B → A ≅ B
@@ -298,11 +296,11 @@ module ≅-Reasoning where
   _≅⟨⟩_ : ∀ {I J} (A : IndexedSet I) {B : IndexedSet J} → A ≅ B → A ≅ B
   _ ≅⟨⟩ A≅B = A≅B
 
-  step-≅ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K}
+  step-≅-⟩ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K}
     → B ≅ C
     → A ≅ B
     → A ≅ C
-  step-≅ _ B≅C A≅B = ≅-trans A≅B B≅C
+  step-≅-⟩ _ B≅C A≅B = ≅-trans A≅B B≅C
 
   -- step-≅-by-index-translation : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K}
   --   → (i→j : I → J)
@@ -313,36 +311,36 @@ module ≅-Reasoning where
   --   → A ≅ C
   -- step-≅-by-index-translation _ i→j j→i ti tj B≅C = ≅-trans (⊆-by-index-translation i→j ti , ⊆-by-index-translation j→i tj) B≅C
 
-  step-≅˘ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K}
+  step-≅-⟨ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K}
     → B ≅ C
     → B ≅ A
     → A ≅ C
-  step-≅˘ A B≅C B≅A = step-≅ A B≅C (≅-sym B≅A)
+  step-≅-⟨ A B≅C B≅A = step-≅-⟩ A B≅C (≅-sym B≅A)
 
-  step-≐ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J}
+  step-≐-⟩ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J}
     → B ≅ C
     → A ≐ B
     → A ≅ C
-  step-≐ _ B≅C A≐B = ≅-trans (≐→≅ A≐B) B≅C
+  step-≐-⟩ _ B≅C A≐B = ≅-trans (≐→≅ A≐B) B≅C
 
-  step-≐˘ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J}
+  step-≐-⟨ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J}
     → B ≅ C
     → B ≐ A
     → A ≅ C
-  step-≐˘ A B≅C B≐A = step-≐ A B≅C (≐-sym B≐A)
+  step-≐-⟨ A B≅C B≐A = step-≐-⟩ A B≅C (≐-sym B≐A)
 
   _≅-∎ : ∀ {I} (A : IndexedSet I) → A ≅ A
   _≅-∎ _ = ≅-refl
 
-  syntax step-≅ A B≅C A≅B = A ≅⟨ A≅B ⟩ B≅C
-  syntax step-≅˘ A B≅C B≅A = A ≅˘⟨ B≅A ⟩ B≅C
-  syntax step-≐ A B≅C (λ i → Ai≈Bi) = A ≐[ i ]⟨ Ai≈Bi ⟩ B≅C
-  syntax step-≐˘ A B≅C (λ i → Bi≈Ai) = A ≐˘[ i ]⟨ Bi≈Ai ⟩ B≅C
+  syntax step-≅-⟩ A B≅C A≅B = A ≅⟨ A≅B ⟩ B≅C
+  syntax step-≅-⟨ A B≅C B≅A = A ≅⟨ B≅A ⟨ B≅C
+  syntax step-≐-⟩ A B≅C (λ i → Ai≈Bi) = A ≐[ i ]⟨ Ai≈Bi ⟩ B≅C
+  syntax step-≐-⟨ A B≅C (λ i → Bi≈Ai) = A ≐[ i ]⟨ Bi≈Ai ⟨ B≅C
   -- syntax step-≅-by-index-translation A i→j j→i ti tj B≅C = A ≅[ i→j ]⟨ ti ⟩[ j→i ]⟨ tj ⟩ B≅C
 
 module ≅[]-Reasoning where
   infix  3 _≅[]-∎
-  infixr 2 _≅[]⟨⟩_ step-≅[] step-≅[]˘ step-≐[] step-≐[]˘
+  infixr 2 _≅[]⟨⟩_ step-≅[]-⟨ step-≅[]-⟩ step-≐[]-⟨ step-≐[]-⟩
   infix  1 ≅[]-begin_
 
   ≅[]-begin_ : ∀{I J} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {g : J → I}
@@ -355,42 +353,42 @@ module ≅[]-Reasoning where
     → A ≅[ f ][ g ] B
   _ ≅[]⟨⟩ A≅B = A≅B
 
-  step-≅[] : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K}
+  step-≅[]-⟩ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K}
                {f : I → J} {f⁻¹ : J → I} {g : J → K} {g⁻¹ : K → J}
     → B ≅[ g ][ g⁻¹ ] C
     → A ≅[ f ][ f⁻¹ ] B
     → A ≅[ g ∘ f ][ f⁻¹ ∘ g⁻¹ ] C
-  step-≅[] _ B≅C A≅B = ≅[]-trans A≅B B≅C
+  step-≅[]-⟩ _ B≅C A≅B = ≅[]-trans A≅B B≅C
 
-  step-≅[]˘ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K}
+  step-≅[]-⟨ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K}
                 {f : I → J} {f⁻¹ : J → I} {g : J → K} {g⁻¹ : K → J}
     → B ≅[ g ][ g⁻¹ ] C
     → B ≅[ f⁻¹ ][ f ] A
     → A ≅[ g ∘ f ][ f⁻¹ ∘ g⁻¹ ] C
-  step-≅[]˘ A B≅C B≅A = step-≅[] A B≅C (≅[]-sym B≅A)
+  step-≅[]-⟨ A B≅C B≅A = step-≅[]-⟩ A B≅C (≅[]-sym B≅A)
 
-  step-≐[] : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J}
+  step-≐[]-⟩ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J}
               {g : I → J} {ginv : J → I}
     → B ≅[ g ][ ginv ] C
     → A ≐ B
     → A ≅[ g ][ ginv ] C
-  step-≐[] _ B≅C A≐B = ≅[]-trans (≐→≅[] A≐B) B≅C
+  step-≐[]-⟩ _ B≅C A≐B = ≅[]-trans (≐→≅[] A≐B) B≅C
 
-  step-≐[]˘ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J}
+  step-≐[]-⟨ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J}
                 {g : I → J} {ginv : J → I}
     → B ≅[ g ][ ginv ] C
     → B ≐ A
     → A ≅[ g ][ ginv ] C
-  step-≐[]˘ A B≅C B≐A = step-≐[] A B≅C (≐-sym B≐A)
+  step-≐[]-⟨ A B≅C B≐A = step-≐[]-⟩ A B≅C (≐-sym B≐A)
 
   _≅[]-∎ : ∀ {I} (A : IndexedSet I)
     → A ≅[ id ][ id ] A
   _≅[]-∎ _ = ≅[]-refl
 
-  syntax step-≅[] A B≅C A≅B = A ≅[]⟨ A≅B ⟩ B≅C
-  syntax step-≅[]˘ A B≅C B≅A = A ≅[]˘⟨ B≅A ⟩ B≅C
-  syntax step-≐[] A B≅C (λ i → Ai≈Bi) = A ≐[ i ]⟨ Ai≈Bi ⟩ B≅C
-  syntax step-≐[]˘ A B≅C (λ i → Bi≈Ai) = A ≐˘[ i ]⟨ Bi≈Ai ⟩ B≅C
+  syntax step-≅[]-⟩ A B≅C A≅B = A ≅[]⟨ A≅B ⟩ B≅C
+  syntax step-≅[]-⟨ A B≅C B≅A = A ≅[]⟨ B≅A ⟨ B≅C
+  syntax step-≐[]-⟩ A B≅C (λ i → Ai≈Bi) = A ≐[ i ]⟨ Ai≈Bi ⟩ B≅C
+  syntax step-≐[]-⟨ A B≅C (λ i → Bi≈Ai) = A ≐[ i ]⟨ Bi≈Ai ⟨ B≅C
 ```
 
 ## Common sets and relations
@@ -476,6 +474,7 @@ We do not require that both relations are indeed equivalence relations but only
     - equivalence of original indices `_≈ᵇ_`
   - Equal original indices index equal source elements. This means that the equality of original indices `_≈ᵇ_` has to be congruent with
     respect to equivalence `_≈_` of the source elements.
+  - `Symmetric _≈ᵃ_`: reflexivity over renamed indices is required for a detail in the proof.
   - `Symmetric _≈ᵇ_`: symmetry over original indices is required for a detail in the proof.
 ```agda
 re-indexʳ : ∀ {A B : Index}
@@ -484,34 +483,36 @@ re-indexʳ : ∀ {A B : Index}
   → (rename : A → B)
   → (M : IndexedSet B)
   → Surjective _≈ᵃ_ _≈ᵇ_ rename
+  → RB.Reflexive _≈ᵃ_
   → RB.Symmetric _≈ᵇ_
   → Congruent _≈ᵇ_ _≈_ M
     ---------------------
   → M ⊆ (M ∘ rename)
-re-indexʳ {A} {B} {_} {_≈ᵇ_} rename M rename-is-surjective ≈ᵇ-sym M-is-congruent b =
+re-indexʳ {A} {B} {_≈ᵃ_} {_≈ᵇ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent b =
   a , same-picks
-  where suitable-a : Σ[ a ∈ A ] (rename a ≈ᵇ b)
+  where suitable-a : Σ[ a ∈ A ] ({z : A} → z ≈ᵃ a → rename z ≈ᵇ b)
         suitable-a = rename-is-surjective b
 
         a : A
         a = proj₁ suitable-a
 
         same-picks : M b ≈ M (rename a)
-        same-picks = M-is-congruent (≈ᵇ-sym (proj₂ suitable-a))
+        same-picks = M-is-congruent (≈ᵇ-sym (proj₂ suitable-a ≈ᵃ-refl))
 
 re-index : ∀ {A B : Index}
     {_≈ᵃ_ : Rel A c} -- Equality of renamed indices
     {_≈ᵇ_ : Rel B c} -- Equality of original indices
   → (rename : A → B)
   → (M : IndexedSet B)
   → Surjective _≈ᵃ_ _≈ᵇ_ rename
+  → RB.Reflexive _≈ᵃ_
   → RB.Symmetric _≈ᵇ_
   → Congruent _≈ᵇ_ _≈_ M
     ---------------------------
   → (M ∘ rename) ≅ M
-re-index {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵇ-sym M-is-congruent =
+re-index {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent =
     re-indexˡ rename M
-  , re-indexʳ {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵇ-sym M-is-congruent
+  , re-indexʳ {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent
 ```
 
 ## Examples

src/Framework/Composition/FeatureAlgebra.agda

@@ -31,7 +31,7 @@ record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) w
   direct-idempotence i =
     begin
       i ⊕ i
-    ≡˘⟨ Eq.cong (i ⊕_) (proj₁ identity i) ⟩
+    ≡⟨ Eq.cong (i ⊕_) (proj₁ identity i) ⟨
       i ⊕ 𝟘 ⊕ i
     ≡⟨ distant-idempotence 𝟘 i ⟩
       𝟘 ⊕ i
@@ -51,13 +51,13 @@ record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) w
   ≤-trans {i} {j} {k} i≤j j≤k =
     begin
       i ⊕ k
-    ≡˘⟨ Eq.cong (i ⊕_) j≤k ⟩
+    ≡⟨ Eq.cong (i ⊕_) j≤k ⟨
       i ⊕ (j ⊕ k)
-    ≡˘⟨ Eq.cong (λ x → i ⊕ x ⊕ k) i≤j ⟩
+    ≡⟨ Eq.cong (λ x → i ⊕ x ⊕ k) i≤j ⟨
       i ⊕ ((i ⊕ j) ⊕ k)
-    ≡˘⟨ assoc i (i ⊕ j) k ⟩
+    ≡⟨ assoc i (i ⊕ j) k ⟨
       (i ⊕ (i ⊕ j)) ⊕ k
-    ≡˘⟨ Eq.cong (_⊕ k) (assoc i i j) ⟩
+    ≡⟨ Eq.cong (_⊕ k) (assoc i i j) ⟨
       ((i ⊕ i) ⊕ j) ⊕ k
     ≡⟨ Eq.cong (_⊕ k) (Eq.cong (_⊕ j) (direct-idempotence i)) ⟩
       (i ⊕ j) ⊕ k
@@ -136,7 +136,7 @@ record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) w
       (i₂ ⊕ i₁) ⊕ i₁ ⊕ i₂
     ≡⟨⟩
       (i₂ ⊕ i₁) ⊕ (i₁ ⊕ i₂)
-    ≡˘⟨ assoc (i₂ ⊕ i₁) i₁ i₂ ⟩
+    ≡⟨ assoc (i₂ ⊕ i₁) i₁ i₂ ⟨
       ((i₂ ⊕ i₁) ⊕ i₁) ⊕ i₂
     ≡⟨ Eq.cong (_⊕ i₂) (assoc i₂ i₁ i₁) ⟩
       (i₂ ⊕ (i₁ ⊕ i₁)) ⊕ i₂

src/Framework/Properties/Finity.agda

@@ -30,6 +30,7 @@ soundness-from-enumerability {L} L-has-finite-semantics {A} e =
         enumerate-configuration
         ⟦ e ⟧
         (enumerate-is-surjective fin)
+        (Eq._≡_.refl)
         (IsEquivalence.sym (≣ⁱ-IsEquivalence L e))
         (≣ⁱ-congruent L e)
       where ⟦_⟧ = Semantics L

src/Framework/Variants.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --sized-types #-}
 {-# OPTIONS --allow-unsolved-metas #-}
 
 module Framework.Variants where
@@ -81,7 +80,7 @@ module _ (V : 𝕍) (A : 𝔸) {Γ : VariabilityLanguage V} (encoder : VariantEn
       ⟦ compile encoder v ⟧ c
     ≡⟨ irrelevant-index (encoded-variant-is-singleton-set v) ⟩
       ⟦ compile encoder v ⟧ (conf encoder v tt)
-    ≡˘⟨ proj₁ (preserves encoder v) tt ⟩
+    ≡⟨ proj₁ (preserves encoder v) tt ⟨
       ⟦ v ⟧ᵥ tt
     ≡⟨⟩
       v
@@ -172,7 +171,7 @@ rose-encoder Γ has c = record
       --     rose x
       --   ≡⟨ {!!} ⟩
       --     (cons (C∈ₛV has) ∘ pcong ArtifactC Γ (map-children t x)) (confi i)
-      --   ≡˘⟨ resistant has (map-children t x) (confi i) ⟩
+      --   ≡⟨ resistant has (map-children t x) (confi i) ⟨
       --     ⟦ cons (C∈ₛΓ has) (map-children t x) ⟧ (confi i)
       --   ∎