From bc95fea515cc8e600e8aa9cc537ac90f26ad7f17 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Tue, 23 Apr 2024 22:55:57 +0200 Subject: [PATCH] Get rid of `--large-indicies` using higher levels Agda disables this option by default because it can cause inconsistencies (especially with `--forced-argument-recursion`, which is enabled by default). Hence, it's better to disable it as well. Unfortunately, `MonadWriter` cannot handle different `Level`s for the Value and the Result type. Hence, `ignore-value` and `return-value` hack is required to shift the `Level`s as required. There are still some cases in `IndexedSet` where the `Level`s could be generalized even more. I know of at least the `Transitive` laws. However, the standard library doesn't provide a `Trans` definition allowing different indices as for homogeneous transitivity. We don't need this generality yet, so I just left it out for now. --- EPVL.agda-lib | 2 +- src/Construct/Choices.agda | 45 ++--- src/Construct/GrulerArtifacts.agda | 13 +- src/Construct/NestedChoice.agda | 7 +- src/Data/EqIndexedSet.agda | 6 +- src/Data/IndexedSet.lagda.md | 164 +++++++++--------- src/Framework/Construct.agda | 18 +- src/Framework/Definitions.agda | 13 +- src/Framework/Relation/Expression.lagda.md | 6 +- src/Framework/Relation/Index.lagda.md | 6 +- src/Framework/VariabilityLanguage.lagda.md | 2 +- src/Framework/VariantMap.agda | 4 +- src/Lang/ADT/Path.agda | 8 +- src/Lang/FST.agda | 32 ++-- src/Lang/Gruler.agda | 9 +- src/Lang/VariantList.lagda.md | 2 +- src/Main.agda | 2 +- src/Show/Lines.agda | 40 +++-- src/Test/Examples/CCC.agda | 2 +- src/Test/Examples/OC.agda | 2 +- src/Test/Experiments/RoundTrip.agda | 23 ++- src/Test/UnitTest.agda | 38 ++-- .../Construct/2Choice-to-Choice.agda | 2 +- .../Construct/Choice-to-2Choice.agda | 2 +- src/Translation/Lang/2CC-to-NCC.agda | 4 +- src/Translation/Lang/ADT/DeadElim.agda | 4 +- src/Translation/Lang/CCC-to-NCC.agda | 18 +- src/Translation/Lang/NCC-to-2CC.agda | 4 +- src/Translation/Lang/OC-to-2CC.lagda.md | 10 +- src/Util/List.agda | 4 +- src/Util/Suffix.agda | 2 +- src/Util/Vec.agda | 14 +- 32 files changed, 268 insertions(+), 240 deletions(-) diff --git a/EPVL.agda-lib b/EPVL.agda-lib index 7c0e6583..d069d5b1 100644 --- a/EPVL.agda-lib +++ b/EPVL.agda-lib @@ -1,4 +1,4 @@ name: EPVL depend: standard-library-2.0 include: src -flags: --large-indices --no-forced-argument-recursion --sized-types +flags: --sized-types diff --git a/src/Construct/Choices.agda b/src/Construct/Choices.agda index e13ffb99..4ca8d107 100644 --- a/src/Construct/Choices.agda +++ b/src/Construct/Choices.agda @@ -12,13 +12,16 @@ open Eq.≡-Reasoning open import Data.EqIndexedSet as ISet +private variable + ℓ : Level + module NChoice where open import Data.Fin using (Fin) open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥) open import Data.Vec using (Vec; lookup; toList) renaming (map to map-vec) open import Data.Vec.Properties using (lookup-map) - record Syntax (n : ℕ≥ 2) (Q : Set) (A : Set) : Set where + record Syntax (n : ℕ≥ 2) (Q : Set) (A : Set ℓ) : Set ℓ where constructor _⟨_⟩ field dim : Q @@ -28,43 +31,43 @@ module NChoice where Config n Q = Q → Fin (ℕ≥.toℕ n) -- choice-elimination - ⟦_⟧ : ∀ {n : ℕ≥ 2} {A : Set} {Q : Set} → Syntax n Q A → Config n Q → A + ⟦_⟧ : ∀ {n : ℕ≥ 2} {A : Set ℓ} {Q : Set} → Syntax n Q A → Config n Q → A ⟦_⟧ (D ⟨ alternatives ⟩) c = lookup alternatives (c D) - map : ∀ {n : ℕ≥ 2} {Q : Set} {A : Set} {B : Set} + map : ∀ {ℓ₁ ℓ₂} {n : ℕ≥ 2} {Q : Set} {A : Set ℓ₁} {B : Set ℓ₂} → (A → B) → Syntax n Q A → Syntax n Q B map f (D ⟨ alternatives ⟩) = D ⟨ map-vec f alternatives ⟩ -- -- rename - map-dim : ∀ {n : ℕ≥ 2} {Q : Set} {R : Set} {A : Set} + map-dim : ∀ {n : ℕ≥ 2} {Q : Set} {R : Set} {A : Set ℓ} → (Q → R) → Syntax n Q A → Syntax n R A map-dim f (D ⟨ es ⟩) = (f D) ⟨ es ⟩ - map-preserves : ∀ {n : ℕ≥ 2} {Q : Set} {A : Set} {B : Set} + map-preserves : ∀ {ℓ₁ ℓ₂} {n : ℕ≥ 2} {Q : Set} {A : Set ℓ₁} {B : Set ℓ₂} → (f : A → B) → (chc : Syntax n Q A) → (c : Config n Q) → ⟦ map f chc ⟧ c ≡ f (⟦ chc ⟧ c) - map-preserves {n} f (D ⟨ es ⟩) c = + map-preserves {n = n} f (D ⟨ es ⟩) c = begin - ⟦ map {n} f (D ⟨ es ⟩) ⟧ c + ⟦ map {n = n} f (D ⟨ es ⟩) ⟧ c ≡⟨⟩ lookup (map-vec f es) (c D) ≡⟨ lookup-map (c D) f es ⟩ f (lookup es (c D)) ≡⟨⟩ - f (⟦_⟧ {n} (D ⟨ es ⟩) c) -- TODO implicit argument + f (⟦_⟧ {n = n} (D ⟨ es ⟩) c) -- TODO implicit argument ∎ - show : ∀ {n : ℕ≥ 2} {Q : Set} {A : Set} → (Q → String) → (A → String) → Syntax n Q A → String + show : ∀ {n : ℕ≥ 2} {Q : Set} {A : Set ℓ} → (Q → String) → (A → String) → Syntax n Q A → String show show-q show-a (D ⟨ es ⟩) = show-q D <+> "⟨" <+> (intersperse " , " (toList (map-vec show-a es))) <+> "⟩" module 2Choice where - record Syntax (Q : Set) (A : Set) : Set where + record Syntax (Q : Set) (A : Set ℓ) : Set ℓ where constructor _⟨_,_⟩ field dim : Q @@ -75,23 +78,23 @@ module 2Choice where Config Q = Q → Bool -- choice-elimination - ⟦_⟧ : ∀ {A : Set} {Q : Set} → Syntax Q A → Config Q → A + ⟦_⟧ : ∀ {A : Set ℓ} {Q : Set} → Syntax Q A → Config Q → A ⟦_⟧ (D ⟨ l , r ⟩) c = if c D then l else r - map : ∀ {Q : Set} {A : Set} {B : Set} + map : ∀ {ℓ₁ ℓ₂} {Q : Set} {A : Set ℓ₁} {B : Set ℓ₂} → (A → B) → Syntax Q A → Syntax Q B map f (D ⟨ l , r ⟩) = D ⟨ f l , f r ⟩ -- rename - map-dim : ∀ {Q : Set} {R : Set} {A : Set} + map-dim : ∀ {Q : Set} {R : Set} {A : Set ℓ} → (Q → R) → Syntax Q A → Syntax R A map-dim f (D ⟨ l , r ⟩) = (f D) ⟨ l , r ⟩ - map-preserves : ∀ {Q : Set} {A : Set} {B : Set} + map-preserves : ∀ {ℓ₁ ℓ₂} {Q : Set} {A : Set ℓ₁} {B : Set ℓ₂} → (f : A → B) → (chc : Syntax Q A) → (c : Config Q) @@ -107,7 +110,7 @@ module 2Choice where f (⟦ D ⟨ l , r ⟩ ⟧ c) ∎ - show : ∀ {Q : Set} {A : Set} → (Q → String) → (A → String) → Syntax Q A → String + show : ∀ {Q : Set} {A : Set ℓ} → (Q → String) → (A → String) → Syntax Q A → String show show-q show-a (D ⟨ l , r ⟩) = show-q D <+> "⟨" <+> show-a l <+> "," <+> show-a r <+> "⟩" open import Data.Nat using (ℕ) @@ -115,7 +118,7 @@ open import Data.List.NonEmpty using (List⁺; toList) renaming (map to map-list open import Util.List using (find-or-last; map-find-or-last) module Choice where - record Syntax (Q : Set) (A : Set) : Set where + record Syntax (Q : Set) (A : Set ℓ) : Set ℓ where constructor _⟨_⟩ field dim : Q @@ -125,23 +128,23 @@ module Choice where Config Q = Q → ℕ -- choice-elimination - ⟦_⟧ : ∀ {Q : Set} {A : Set} → Syntax Q A → Config Q → A + ⟦_⟧ : ∀ {Q : Set} {A : Set ℓ} → Syntax Q A → Config Q → A ⟦_⟧ (D ⟨ alternatives ⟩) c = find-or-last (c D) alternatives - map : ∀ {Q : Set} {A : Set} {B : Set} + map : ∀ {ℓ₁ ℓ₂} {Q : Set} {A : Set ℓ₁} {B : Set ℓ₂} → (A → B) → Syntax Q A → Syntax Q B map f (dim ⟨ alternatives ⟩) = dim ⟨ map-list⁺ f alternatives ⟩ -- rename - map-dim : ∀ {Q : Set} {R : Set} {A : Set} + map-dim : ∀ {Q : Set} {R : Set} {A : Set ℓ} → (Q → R) → Syntax Q A → Syntax R A map-dim f (dim ⟨ alternatives ⟩) = (f dim) ⟨ alternatives ⟩ - map-preserves : ∀ {Q : Set} {A : Set} {B : Set} + map-preserves : ∀ {ℓ₁ ℓ₂} {Q : Set} {A : Set ℓ₁} {B : Set ℓ₂} → (f : A → B) → (chc : Syntax Q A) → (c : Config Q) -- todo: use ≐ here? @@ -157,7 +160,7 @@ module Choice where f (⟦ D ⟨ as ⟩ ⟧ c) ∎ - show : ∀ {Q : Set} {A : Set} → (Q → String) → (A → String) → Syntax Q A → String + show : ∀ {Q : Set} {A : Set ℓ} → (Q → String) → (A → String) → Syntax Q A → String show show-q show-a (D ⟨ es ⟩) = show-q D <+> "⟨" <+> (intersperse " , " (toList (map-list⁺ show-a es))) <+> "⟩" -- Show how choices can be used as constructors in variability languages. diff --git a/src/Construct/GrulerArtifacts.agda b/src/Construct/GrulerArtifacts.agda index 69da3955..38f9c5ae 100644 --- a/src/Construct/GrulerArtifacts.agda +++ b/src/Construct/GrulerArtifacts.agda @@ -1,5 +1,6 @@ module Construct.GrulerArtifacts where +open import Level using (suc) open import Data.Maybe using (just; nothing) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) @@ -21,26 +22,26 @@ record ParallelComposition {ℓ} (A : Set ℓ) : Set ℓ where module VLLeaf where Syntax : ℂ - Syntax _ A = Leaf (atoms A) + Syntax _ A = Level.Lift _ (Leaf (atoms A)) make-leaf : ∀ {E : 𝔼} → Syntax ∈ₛ E → {A : 𝔸} → atoms A → E A - make-leaf mkLeaf a = cons mkLeaf (leaf a) + make-leaf mkLeaf a = cons mkLeaf (Level.lift (leaf a)) elim-leaf : ∀ {V} → Syntax ∈ₛ V → ∀ {A} → Leaf (atoms A) → V A - elim-leaf leaf∈V l = cons leaf∈V l + elim-leaf leaf∈V l = cons leaf∈V (Level.lift l) Construct : PlainConstruct PSyntax Construct = Syntax pcong Construct _ e _ = e Leaf∈ₛGrulerVariant : Syntax ∈ₛ GrulerVariant - cons Leaf∈ₛGrulerVariant (leaf a) = asset a - snoc Leaf∈ₛGrulerVariant (asset a) = just (leaf a) + cons Leaf∈ₛGrulerVariant (Level.lift (leaf a)) = asset a + snoc Leaf∈ₛGrulerVariant (asset a) = just (Level.lift (leaf a)) snoc Leaf∈ₛGrulerVariant (_ ∥ _) = nothing - id-l Leaf∈ₛGrulerVariant (leaf _) = refl + id-l Leaf∈ₛGrulerVariant (Level.lift (leaf _)) = refl module VLParallelComposition where Syntax : ℂ diff --git a/src/Construct/NestedChoice.agda b/src/Construct/NestedChoice.agda index bac0f0a7..830270f7 100644 --- a/src/Construct/NestedChoice.agda +++ b/src/Construct/NestedChoice.agda @@ -2,20 +2,21 @@ open import Framework.Definitions module Construct.NestedChoice (F : 𝔽) where +open import Level using (suc) open import Data.String using (String) open import Size using (Size; ↑_) open import Construct.Choices -data NestedChoice : Size → Set → Set where +data NestedChoice {ℓ} : Size → Set ℓ → Set (suc ℓ) where value : ∀ {i A} → A → NestedChoice i A choice : ∀ {i A} → 2Choice.Syntax F (NestedChoice i A) → NestedChoice (↑ i) A -⟦_⟧ : ∀ {i A} → NestedChoice i A → 2Choice.Config F → A +⟦_⟧ : ∀ {ℓ i A} → NestedChoice {ℓ} i A → 2Choice.Config F → A ⟦ value v ⟧ c = v ⟦ choice chc ⟧ c = ⟦ 2Choice.⟦ chc ⟧ c ⟧ c -show-nested-choice : ∀ {i A} → (F → String) → (A → String) → NestedChoice i A → String +show-nested-choice : ∀ {ℓ i A} → (F → String) → (A → String) → NestedChoice {ℓ} i A → String show-nested-choice show-q show-carrier ( value v) = show-carrier v show-nested-choice show-q show-carrier (choice c) = 2Choice.show diff --git a/src/Data/EqIndexedSet.agda b/src/Data/EqIndexedSet.agda index 9ea8768d..c8ae3c07 100644 --- a/src/Data/EqIndexedSet.agda +++ b/src/Data/EqIndexedSet.agda @@ -1,4 +1,6 @@ -module Data.EqIndexedSet {A : Set} where +open import Level using (Level) + +module Data.EqIndexedSet {ℓ : Level} {A : Set ℓ} where import Relation.Binary.PropositionalEquality as Eq -open import Data.IndexedSet (Eq.setoid A) as ISet public +open import Data.IndexedSet {ℓ} (Eq.setoid A) as ISet public diff --git a/src/Data/IndexedSet.lagda.md b/src/Data/IndexedSet.lagda.md index f3e2500a..8c5e824d 100644 --- a/src/Data/IndexedSet.lagda.md +++ b/src/Data/IndexedSet.lagda.md @@ -3,14 +3,14 @@ ## Module ```agda -open import Level using (Level; suc; _⊔_) +open import Level using (Level; 0ℓ; suc; _⊔_) open import Relation.Binary as RB using ( Rel; Setoid; Antisym; IsEquivalence) open import Relation.Binary.Indexed.Heterogeneous using ( - IRel; + IREL; Reflexive; Symmetric; Transitive; @@ -40,39 +40,42 @@ module Eq = IsEquivalence isEquivalence ## Definitions ```agda -Index : Set (suc c) -Index = Set c +variable + iℓ jℓ kℓ : Level -IndexedSet : Index → Set c +Index : (iℓ : Level) → Set (suc iℓ) +Index iℓ = Set iℓ + +IndexedSet : Index iℓ → Set (c ⊔ iℓ) IndexedSet I = I → Carrier -- an element is within a subset, if there is an index pointing at that element -_∈_ : ∀ {I} → Carrier → IndexedSet I → Set (c ⊔ ℓ) +_∈_ : ∀ {I : Set iℓ} → Carrier → IndexedSet I → Set (ℓ ⊔ iℓ) a ∈ A = ∃[ i ] (a ≈ A i) -- morphisms -- _⊆_ : ∀ {I J} → IndexedSet I → IndexedSet J → Set ℓ -_⊆_ : IRel IndexedSet (c ⊔ ℓ) -_⊆_ {I} A B = ∀ (i : I) → A i ∈ B +_⊆_ : IREL (IndexedSet {iℓ}) (IndexedSet {jℓ}) (ℓ ⊔ iℓ ⊔ jℓ) +_⊆_ {i₁ = I} A B = ∀ (i : I) → A i ∈ B -_≅_ : IRel IndexedSet (c ⊔ ℓ) +_≅_ : IREL (IndexedSet {iℓ}) (IndexedSet {jℓ}) (ℓ ⊔ iℓ ⊔ jℓ) A ≅ B = (A ⊆ B) × (B ⊆ A) -- Same indices point to same values. -- This definition is the same as _≗_ from the standard-library but generalized to an arbitrary -- underlying equivalence relation _≈_. -_≐_ : ∀ {I} (A B : IndexedSet I) → Set (c ⊔ ℓ) -_≐_ {I} A B = ∀ (i : I) → A i ≈ B i +_≐_ : ∀ {I : Set iℓ} (A B : IndexedSet I) → Set (ℓ ⊔ iℓ) +_≐_ {I = I} A B = ∀ (i : I) → A i ≈ B i -≐→≅ : ∀ {I} {A B : IndexedSet I} → A ≐ B → A ≅ B -- this acts as cong, too +≐→≅ : ∀ {I : Set iℓ} {A B : IndexedSet I} → A ≐ B → A ≅ B -- this acts as cong, too ≐→≅ A≐B = (λ i → (i , A≐B i)) , (λ i → (i , sym (A≐B i))) -≗→≐ : ∀ {I} {A B : IndexedSet I} → A ≗ B → A ≐ B +≗→≐ : ∀ {I : Set iℓ} {A B : IndexedSet I} → A ≗ B → A ≐ B ≗→≐ A≗B i = Eq.reflexive (A≗B i) -≗→≅ : ∀ {I} {A B : IndexedSet I} → A ≗ B → A ≅ B +≗→≅ : ∀ {I : Set iℓ} {A B : IndexedSet I} → A ≗ B → A ≅ B ≗→≅ A≗B = ≐→≅ (≗→≐ A≗B) ``` @@ -82,10 +85,10 @@ _≐_ {I} A B = ∀ (i : I) → A i ≈ B i {-| An indexed set contains only a single element if all indices point to the same element. -} -Singleton : ∀ {I} → IndexedSet I → Set (c ⊔ ℓ) +Singleton : ∀ {I : Set iℓ} → IndexedSet I → Set (c ⊔ ℓ ⊔ iℓ) Singleton A = ∃[ x ] ∀ i → A i ≈ x -irrelevant-index : ∀ {I} {A : IndexedSet I} +irrelevant-index : ∀ {I : Set iℓ} {A : IndexedSet I} → Singleton A → ∀ {i j} → A i ≈ A j irrelevant-index (x , Ai≈x) {i} {j} = Eq.trans (Ai≈x i) (Eq.sym (Ai≈x j)) @@ -94,14 +97,15 @@ irrelevant-index (x , Ai≈x) {i} {j} = Eq.trans (Ai≈x i) (Eq.sym (Ai≈x j)) ## Properties ```agda -⊆-refl : Reflexive IndexedSet _⊆_ +⊆-refl : Reflexive (IndexedSet {iℓ}) _⊆_ ⊆-refl i = i , Eq.refl -- Todo: There is no antsymmetry definition in Relation.Binary.Indexed.Heterogeneous.Definition. Adding that to the standard library would be good and a low hanging fruit. -⊆-antisym : ∀ {I J} → Antisym (_⊆_ {I} {J}) (_⊆_ {J} {I}) (_≅_ {I} {J}) +⊆-antisym : ∀ {I : Set iℓ} {J : Set jℓ} → Antisym (_⊆_ {i₁ = I}) (_⊆_ {i₁ = J}) (_≅_) ⊆-antisym l r = l , r -⊆-trans : Transitive IndexedSet _⊆_ +-- Todo: There are no generalized transitivity, symmetry and antisymmetry definitions which allow different levels in Relation.Binary.Indexed.Heterogeneous.Definition . Adding that to the standard library would be good and a low hanging fruit. +⊆-trans : Transitive (IndexedSet {iℓ}) _⊆_ ⊆-trans A⊆B B⊆C i = -- This proof looks resembles state monad bind >>=. -- interesting... :thinking_face: @@ -109,34 +113,34 @@ irrelevant-index (x , Ai≈x) {i} {j} = Eq.trans (Ai≈x i) (Eq.sym (Ai≈x j)) (k , Bj≈Ck) = B⊆C j in k , Eq.trans Ai≈Bj Bj≈Ck -≅-refl : Reflexive IndexedSet _≅_ +≅-refl : Reflexive (IndexedSet {iℓ}) _≅_ ≅-refl = ⊆-refl , ⊆-refl -≅-sym : Symmetric IndexedSet _≅_ +≅-sym : Symmetric (IndexedSet {iℓ}) _≅_ ≅-sym (l , r) = r , l -≅-trans : Transitive IndexedSet _≅_ +≅-trans : Transitive (IndexedSet {iℓ}) _≅_ ≅-trans (A⊆B , B⊆A) (B⊆C , C⊆B) = ⊆-trans A⊆B B⊆C , ⊆-trans C⊆B B⊆A -≅-IsIndexedEquivalence : IsIndexedEquivalence IndexedSet _≅_ +≅-IsIndexedEquivalence : IsIndexedEquivalence (IndexedSet {iℓ}) _≅_ ≅-IsIndexedEquivalence = record { refl = ≅-refl ; sym = ≅-sym ; trans = ≅-trans } -≐-refl : ∀ {I} → RB.Reflexive (_≐_ {I}) +≐-refl : ∀ {I} → RB.Reflexive (_≐_ {iℓ} {I}) ≐-refl i = refl -≐-sym : ∀ {I} → RB.Symmetric (_≐_ {I}) +≐-sym : ∀ {I} → RB.Symmetric (_≐_ {iℓ} {I}) ≐-sym x≐y i = sym (x≐y i) -≐-trans : ∀ {I} → RB.Transitive (_≐_ {I}) +≐-trans : ∀ {I} → RB.Transitive (_≐_ {iℓ} {I}) ≐-trans x≐y y≐z i = trans (x≐y i) (y≐z i) -≐-IsEquivalence : ∀ {I} → IsEquivalence (_≐_ {I}) +≐-IsEquivalence : ∀ {I} → IsEquivalence (_≐_ {iℓ} {I}) ≐-IsEquivalence = record { refl = ≐-refl ; sym = ≐-sym @@ -147,23 +151,23 @@ irrelevant-index (x , Ai≈x) {i} {j} = Eq.trans (Ai≈x i) (Eq.sym (Ai≈x j)) ## Indexed Sets With Index Translations ```agda -_⊆[_]_ : ∀ {I J} → IndexedSet I → (I → J) → IndexedSet J → Set (c ⊔ ℓ) -_⊆[_]_ {I} A f B = ∀ (i : I) → A i ≈ B (f i) +_⊆[_]_ : ∀ {I : Set iℓ} {J : Set jℓ} → IndexedSet I → (I → J) → IndexedSet J → Set (ℓ ⊔ iℓ) +_⊆[_]_ {I = I} A f B = ∀ (i : I) → A i ≈ B (f i) -_≅[_][_]_ : ∀ {I J} → IndexedSet I → (I → J) → (J → I) → IndexedSet J → Set (c ⊔ ℓ) +_≅[_][_]_ : ∀ {I : Set iℓ} {J : Set jℓ} → IndexedSet I → (I → J) → (J → I) → IndexedSet J → Set (ℓ ⊔ iℓ ⊔ jℓ) A ≅[ f ][ f⁻¹ ] B = (A ⊆[ f ] B) × (B ⊆[ f⁻¹ ] A) ``` ### Relation to Ordinary Indexed Set Operators ```agda -∈[]→∈ : ∀ {I} {A : IndexedSet I} {a : Carrier} {i : I} +∈[]→∈ : ∀ {I : Set iℓ} {A : IndexedSet I} {a : Carrier} {i : I} → a ≈ A i ---------- → a ∈ A ∈[]→∈ {i = i} eq = i , eq -⊆[]→⊆ : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} +⊆[]→⊆ : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} → A ⊆[ f ] B ----------- → A ⊆ B @@ -175,7 +179,7 @@ A ≅[ f ][ f⁻¹ ] B = (A ⊆[ f ] B) × (B ⊆[ f⁻¹ ] A) -- We should isolate that behaviour and report it as a bug. syntax ⊆[]→⊆ e = ⊆-by-index-translation e -≅[]→≅ : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {f⁻¹ : J → I} +≅[]→≅ : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {f⁻¹ : J → I} → A ≅[ f ][ f⁻¹ ] B ----------------- → A ≅ B @@ -184,15 +188,15 @@ syntax ⊆[]→⊆ e = ⊆-by-index-translation e -- verbose name syntax ≅[]→≅ e = ≅-by-index-translation e -≐→≅[] : ∀ {I} {A B : IndexedSet I} → A ≐ B → A ≅[ id ][ id ] B +≐→≅[] : ∀ {I : Set iℓ} {A B : IndexedSet I} → A ≐ B → A ≅[ id ][ id ] B ≐→≅[] {J} {A} {B} A≐B = (λ i → A≐B i ) , (λ i → sym (A≐B i)) -≗→≅[] : ∀ {I} {A B : IndexedSet I} → A ≗ B → A ≅[ id ][ id ] B +≗→≅[] : ∀ {I : Set iℓ} {A B : IndexedSet I} → A ≗ B → A ≅[ id ][ id ] B ≗→≅[] = ≐→≅[] ∘ ≗→≐ -irrelevant-index-⊆ : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} +irrelevant-index-⊆ : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} → (x : Carrier) → (∀ i → A i ≈ x) → (∀ j → B j ≈ x) @@ -202,7 +206,7 @@ irrelevant-index-⊆ _ const-A const-B = λ f i → Eq.trans (const-A i) (Eq.sym (const-B (f i))) -irrelevant-index-≅ : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} +irrelevant-index-≅ : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} → (x : Carrier) → (∀ i → A i ≈ x) → (∀ j → B j ≈ x) @@ -217,10 +221,10 @@ irrelevant-index-≅ x const-A const-B = ### Basic Properties ```agda -⊆[]-refl : ∀ {I} {A : IndexedSet I} → A ⊆[ id ] A +⊆[]-refl : ∀ {I : Set iℓ} {A : IndexedSet I} → A ⊆[ id ] A ⊆[]-refl = λ _ → Eq.refl -⊆[]-antisym : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {f⁻¹ : J → I} +⊆[]-antisym : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {f⁻¹ : J → I} → A ⊆[ f ] B → B ⊆[ f⁻¹ ] A ----------------- @@ -228,7 +232,7 @@ irrelevant-index-≅ x const-A const-B = ⊆[]-antisym A⊆B B⊆A = A⊆B , B⊆A ⊆[]-trans : - ∀ {I J K} {A : IndexedSet I} {B : IndexedSet J} {C : IndexedSet K} + ∀ {I : Set iℓ} {J : Set jℓ} {K : Set kℓ} {A : IndexedSet I} {B : IndexedSet J} {C : IndexedSet K} {f : I → J} {g : J → K} → A ⊆[ f ] B → B ⊆[ g ] C @@ -236,17 +240,17 @@ irrelevant-index-≅ x const-A const-B = → A ⊆[ g ∘ f ] C ⊆[]-trans {f = f} A⊆B B⊆C i = Eq.trans (A⊆B i) (B⊆C (f i)) -≅[]-refl : ∀ {I} {A : IndexedSet I} → A ≅[ id ][ id ] A +≅[]-refl : ∀ {I : Set iℓ} {A : IndexedSet I} → A ≅[ id ][ id ] A ≅[]-refl = ⊆[]-refl , ⊆[]-refl -≅[]-sym : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {f⁻¹ : J → I} +≅[]-sym : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {f⁻¹ : J → I} → A ≅[ f ][ f⁻¹ ] B ----------------- → B ≅[ f⁻¹ ][ f ] A ≅[]-sym (A⊆B , B⊆A) = B⊆A , A⊆B ≅[]-trans : - ∀ {I J K} {A : IndexedSet I} {B : IndexedSet J} {C : IndexedSet K} + ∀ {I : Set iℓ} {J : Set jℓ} {K : Set kℓ} {A : IndexedSet I} {B : IndexedSet J} {C : IndexedSet K} {f : I → J} {f⁻¹ : J → I} {g : J → K} {g⁻¹ : K → J} → A ≅[ f ][ f⁻¹ ] B → B ≅[ g ][ g⁻¹ ] C @@ -256,7 +260,7 @@ irrelevant-index-≅ x const-A const-B = ⊆[]-trans {C = C} A⊆B B⊆C , ⊆[]-trans {C = A} C⊆B B⊆A -⊆→≅ : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} → (f : I → J) → (f⁻¹ : J → I) → f ∘ f⁻¹ ≗ id → A ⊆[ f ] B → A ≅[ f ][ f⁻¹ ] B +⊆→≅ : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} → (f : I → J) → (f⁻¹ : J → I) → f ∘ f⁻¹ ≗ id → A ⊆[ f ] B → A ≅[ f ][ f⁻¹ ] B ⊆→≅ {A = A} {B = B} f f⁻¹ f∘f⁻¹ A⊆B = A⊆B , (λ i → Eq.sym (subst (λ j → A (f⁻¹ i) ≈ B j) (f∘f⁻¹ i) (A⊆B (f⁻¹ i)))) ``` @@ -268,19 +272,19 @@ module ⊆-Reasoning where infixr 2 _⊆⟨⟩_ step-⊆ infix 1 ⊆-begin_ - ⊆-begin_ : ∀{I J} {A : IndexedSet I} {B : IndexedSet J} → A ⊆ B → A ⊆ B + ⊆-begin_ : ∀{I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} → A ⊆ B → A ⊆ B ⊆-begin_ A⊆B = A⊆B - _⊆⟨⟩_ : ∀ {I J} (A : IndexedSet I) {B : IndexedSet J} → A ⊆ B → A ⊆ B + _⊆⟨⟩_ : ∀ {I : Set iℓ} {J : Set 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 : Set iℓ} (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 - _⊆-∎ : ∀ {I} (A : IndexedSet I) → A ⊆ A + _⊆-∎ : ∀ {I : Set iℓ} (A : IndexedSet I) → A ⊆ A _⊆-∎ _ = ⊆-refl syntax step-⊆ A B⊆C A⊆B = A ⊆⟨ A⊆B ⟩ B⊆C @@ -290,13 +294,13 @@ module ≅-Reasoning where 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 + ≅-begin_ : ∀{I J : Set iℓ} {A : IndexedSet I} {B : IndexedSet J} → A ≅ B → A ≅ B ≅-begin_ A≅B = A≅B - _≅⟨⟩_ : ∀ {I J} (A : IndexedSet I) {B : IndexedSet J} → A ≅ B → A ≅ B + _≅⟨⟩_ : ∀ {I J : Set iℓ} (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 : Set iℓ} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} → B ≅ C → A ≅ B → A ≅ C @@ -311,25 +315,25 @@ 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 : Set iℓ} (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-≐-⟩ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} + step-≐-⟩ : ∀ {I J : Set iℓ} (A {B} : IndexedSet I) {C : IndexedSet J} → B ≅ C → A ≐ B → A ≅ C step-≐-⟩ _ B≅C A≐B = ≅-trans (≐→≅ A≐B) B≅C - step-≐-⟨ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} + step-≐-⟨ : ∀ {I J : Set iℓ} (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) - _≅-∎ : ∀ {I} (A : IndexedSet I) → A ≅ A + _≅-∎ : ∀ {I : Set iℓ} (A : IndexedSet I) → A ≅ A _≅-∎ _ = ≅-refl syntax step-≅-⟩ A B≅C A≅B = A ≅⟨ A≅B ⟩ B≅C @@ -343,45 +347,45 @@ module ≅[]-Reasoning where infixr 2 _≅[]⟨⟩_ step-≅[]-⟨ step-≅[]-⟩ step-≐[]-⟨ step-≐[]-⟩ infix 1 ≅[]-begin_ - ≅[]-begin_ : ∀{I J} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {g : J → I} + ≅[]-begin_ : ∀{I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {g : J → I} → A ≅[ f ][ g ] B → A ≅[ f ][ g ] B ≅[]-begin_ A≅B = A≅B - _≅[]⟨⟩_ : ∀ {I J} {f : I → J} {g : J → I} (A : IndexedSet I) {B : IndexedSet J} + _≅[]⟨⟩_ : ∀ {I : Set iℓ} {J : Set jℓ} {f : I → J} {g : J → I} (A : IndexedSet I) {B : IndexedSet J} → A ≅[ f ][ g ] B → A ≅[ f ][ g ] B _ ≅[]⟨⟩ A≅B = A≅B - step-≅[]-⟩ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} + step-≅[]-⟩ : ∀ {I : Set iℓ} {J : Set jℓ} {K : Set 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-≅[]-⟨ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} + step-≅[]-⟨ : ∀ {I : Set iℓ} {J : Set jℓ} {K : Set 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-≐[]-⟩ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} + step-≐[]-⟩ : ∀ {I : Set iℓ} {J : Set 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-≐[]-⟨ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} + step-≐[]-⟨ : ∀ {I : Set iℓ} {J : Set 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) - _≅[]-∎ : ∀ {I} (A : IndexedSet I) + _≅[]-∎ : ∀ {I : Set iℓ} (A : IndexedSet I) → A ≅[ id ][ id ] A _≅[]-∎ _ = ≅[]-refl @@ -397,24 +401,24 @@ module ≅[]-Reasoning where {-| The empty set -} -𝟘 : IndexedSet ⊥ +𝟘 : IndexedSet {0ℓ} ⊥ 𝟘 = λ () {-| The type of singleton sets over a source. -} -𝟙 : Set c -𝟙 = IndexedSet ⊤ +𝟙 : (iℓ : Level) → Set (c ⊔ iℓ) +𝟙 iℓ = IndexedSet {iℓ} ⊤ -- predicate that checks whether a subset is nonempty -- A set is non-empty when there exists at least one index. -nonempty : ∀ {I} → IndexedSet I → Set c +nonempty : ∀ {I : Set iℓ} → IndexedSet I → Set iℓ nonempty {I = I} _ = I --∃[ a ] (a ∈ A) -- We can retrieve an element from a non-empty set. -- This proves that our definition of nonempty indeed -- implies that there is an element in each non-empty set. -get-from-nonempty : ∀ {I} +get-from-nonempty : ∀ {I : Set iℓ} → (A : IndexedSet I) → nonempty A ---------------- @@ -422,31 +426,31 @@ get-from-nonempty : ∀ {I} get-from-nonempty A i = A i -- predicate that checks whether a subset is empty -empty : ∀ {I} → IndexedSet I → Set c +empty : ∀ {I : Set iℓ} → IndexedSet I → Set iℓ empty A = ¬ (nonempty A) 𝟘-is-empty : empty 𝟘 𝟘-is-empty () -𝟘⊆A : ∀ {I} {A : IndexedSet I} +𝟘⊆A : ∀ {I : Set iℓ} {A : IndexedSet I} ----- → 𝟘 ⊆ A 𝟘⊆A = λ () -empty-set⊆𝟘 : ∀ {I} {A : IndexedSet I} +empty-set⊆𝟘 : ∀ {I : Set iℓ} {A : IndexedSet I} → empty A ------- → A ⊆ 𝟘 empty-set⊆𝟘 A-empty i with A-empty i ...| () -all-empty-sets-are-equal : ∀ {I} {A : IndexedSet I} +all-empty-sets-are-equal : ∀ {I : Set iℓ} {A : IndexedSet I} → empty A ------- → A ≅ 𝟘 all-empty-sets-are-equal A-empty = empty-set⊆𝟘 A-empty , 𝟘⊆A -singleton-set-is-nonempty : (A : 𝟙) → nonempty A +singleton-set-is-nonempty : (A : 𝟙 iℓ) → nonempty A singleton-set-is-nonempty _ = tt ``` @@ -457,7 +461,7 @@ singleton-set-is-nonempty _ = tt We can rename the indices of a multiset M to obtain a subset of M. ```agda -re-indexˡ : ∀ {A B : Set c} +re-indexˡ : ∀ {A B : Set iℓ} → (rename : A → B) → (M : IndexedSet B) --------------------- @@ -477,9 +481,9 @@ We do not require that both relations are indeed equivalence relations but only - `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} - {_≈ᵃ_ : Rel A c} -- Equality of renamed indices - {_≈ᵇ_ : Rel B c} -- Equality of original indices +re-indexʳ : ∀ {ℓᵃ ℓᵇ : Level} {A B : Index iℓ} + {_≈ᵃ_ : Rel A ℓᵃ} -- Equality of renamed indices + {_≈ᵇ_ : Rel B ℓᵇ} -- Equality of original indices → (rename : A → B) → (M : IndexedSet B) → Surjective _≈ᵃ_ _≈ᵇ_ rename @@ -488,7 +492,7 @@ re-indexʳ : ∀ {A B : Index} → Congruent _≈ᵇ_ _≈_ M --------------------- → M ⊆ (M ∘ rename) -re-indexʳ {A} {B} {_≈ᵃ_} {_≈ᵇ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent b = +re-indexʳ {A = A} {B} {_≈ᵃ_} {_≈ᵇ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent b = a , same-picks where suitable-a : Σ[ a ∈ A ] ({z : A} → z ≈ᵃ a → rename z ≈ᵇ b) suitable-a = rename-is-surjective b @@ -499,9 +503,9 @@ re-indexʳ {A} {B} {_≈ᵃ_} {_≈ᵇ_} rename M rename-is-surjective ≈ᵃ-re same-picks : M b ≈ M (rename 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 +re-index : ∀ {ℓᵃ ℓᵇ : Level} {A B : Index iℓ} + {_≈ᵃ_ : Rel A ℓᵃ} -- Equality of renamed indices + {_≈ᵇ_ : Rel B ℓᵇ} -- Equality of original indices → (rename : A → B) → (M : IndexedSet B) → Surjective _≈ᵃ_ _≈ᵇ_ rename diff --git a/src/Framework/Construct.agda b/src/Framework/Construct.agda index 7e2d858c..d24441bd 100644 --- a/src/Framework/Construct.agda +++ b/src/Framework/Construct.agda @@ -26,13 +26,13 @@ open _∈ₛ_ public _∉ₛ_ : ℂ → 𝔼 → Set₁ C ∉ₛ E = ¬ (C ∈ₛ E) -_⊆ₛ_ : 𝔼 → 𝔼 → Set₁ +_⊆ₛ_ : 𝔼 → 𝔼 → Set₂ E₁ ⊆ₛ E₂ = ∀ (C : ℂ) → C ∈ₛ E₁ → C ∈ₛ E₂ -_≅ₛ_ : 𝔼 → 𝔼 → Set₁ +_≅ₛ_ : 𝔼 → 𝔼 → Set₂ E₁ ≅ₛ E₂ = E₁ ⊆ₛ E₂ × E₂ ⊆ₛ E₁ -record PlainConstruct : Set₁ where +record PlainConstruct : Set₂ where constructor Plain-⟪_,_⟫ field PSyntax : ℂ @@ -64,7 +64,7 @@ PlainConstruct-Semantics : ∀ {V} → Construct-Semantics Γ (PSyntax P) PlainConstruct-Semantics P make Γ e = cons make ∘ pcong P Γ e -VariationalConstruct-Semantics : 𝕍 → 𝕂 → ℂ → Set₁ +VariationalConstruct-Semantics : 𝕍 → 𝕂 → ℂ → Set₂ VariationalConstruct-Semantics V K C = -- The underlying language, which the construct is part of. ∀ (Γ : VariabilityLanguage V) @@ -78,7 +78,7 @@ VariationalConstruct-Semantics V K C = → (extract : Config Γ → K) → Construct-Semantics Γ C -record VariabilityConstruct (V : 𝕍) : Set₁ where +record VariabilityConstruct (V : 𝕍) : Set₂ where constructor Variational-⟪_,_,_⟫ field -- How to create a constructor... @@ -115,10 +115,10 @@ open _⟦∈⟧ᵥ_ public _⟦∉⟧ᵥ_ : ∀ {V} → VariabilityConstruct V → VariabilityLanguage V → Set₁ C ⟦∉⟧ᵥ E = ¬ (C ⟦∈⟧ᵥ E) -_⟦⊆⟧ᵥ_ : ∀ {V} → VariabilityLanguage V → VariabilityLanguage V → Set₁ +_⟦⊆⟧ᵥ_ : ∀ {V} → VariabilityLanguage V → VariabilityLanguage V → Set₂ E₁ ⟦⊆⟧ᵥ E₂ = ∀ C → C ⟦∈⟧ᵥ E₁ → C ⟦∈⟧ᵥ E₂ -_⟦≅⟧ᵥ_ : ∀ {V} → VariabilityLanguage V → VariabilityLanguage V → Set₁ +_⟦≅⟧ᵥ_ : ∀ {V} → VariabilityLanguage V → VariabilityLanguage V → Set₂ E₁ ⟦≅⟧ᵥ E₂ = E₁ ⟦⊆⟧ᵥ E₂ × E₂ ⟦⊆⟧ᵥ E₁ -- Semantic containment of plain constructs @@ -140,10 +140,10 @@ open _⟦∈⟧ₚ_ public _⟦∉⟧ₚ_ : ∀ {V} → PlainConstruct → VariabilityLanguage V → Set₁ C ⟦∉⟧ₚ E = ¬ (C ⟦∈⟧ₚ E) -_⟦⊆⟧ₚ_ : ∀ {V} → VariabilityLanguage V → VariabilityLanguage V → Set₁ +_⟦⊆⟧ₚ_ : ∀ {V} → VariabilityLanguage V → VariabilityLanguage V → Set₂ E₁ ⟦⊆⟧ₚ E₂ = ∀ C → C ⟦∈⟧ₚ E₁ → C ⟦∈⟧ₚ E₂ -_⟦≅⟧ₚ_ : ∀ {V} → VariabilityLanguage V → VariabilityLanguage V → Set₁ +_⟦≅⟧ₚ_ : ∀ {V} → VariabilityLanguage V → VariabilityLanguage V → Set₂ E₁ ⟦≅⟧ₚ E₂ = E₁ ⟦⊆⟧ₚ E₂ × E₂ ⟦⊆⟧ₚ E₁ ---- Plain constructs can be seen as variational constructs that do nothing upon configuration. --- diff --git a/src/Framework/Definitions.agda b/src/Framework/Definitions.agda index 91129869..fa0173db 100644 --- a/src/Framework/Definitions.agda +++ b/src/Framework/Definitions.agda @@ -28,8 +28,8 @@ A variant should represent atomic data in some way so its parameterized in atomi -} -- 𝕍 : ∀ {ℓ} → Set (suc ℓ) -- 𝕍 {ℓ} = 𝔸 {ℓ} → Set ℓ -𝕍 : Set₁ -𝕍 = 𝔸 → Set +𝕍 : Set₂ +𝕍 = 𝔸 → Set₁ {- Annotation Language. @@ -68,8 +68,8 @@ and hence expressions are parameterized in the type of this atomic data. -} -- 𝔼 : ∀ {ℓ} → Set (suc ℓ) -- 𝔼 {ℓ} = 𝔸 {ℓ} → Set ℓ -𝔼 : Set₁ -𝔼 = 𝔸 → Set +𝔼 : Set₂ +𝔼 = 𝔸 → Set₁ {- Variability Construct. @@ -83,6 +83,5 @@ for variability annotations 𝔽. -} -- ℂ : ∀ {ℓ} → Set (suc ℓ) -- ℂ {ℓ} = 𝔼 {ℓ} → 𝔸 {ℓ} → Set ℓ -ℂ : Set₁ -ℂ = 𝔼 → 𝔸 → Set - +ℂ : Set₂ +ℂ = 𝔼 → 𝔸 → Set₁ diff --git a/src/Framework/Relation/Expression.lagda.md b/src/Framework/Relation/Expression.lagda.md index 9443f958..d5a37059 100644 --- a/src/Framework/Relation/Expression.lagda.md +++ b/src/Framework/Relation/Expression.lagda.md @@ -25,7 +25,7 @@ if the functions they describe are pointwise equal (same output for same inputs) ```agda _⊢_≣₁_ : ∀ (L : VariabilityLanguage V) → (e₁ e₂ : Expression L A) - → Set + → Set₁ L ⊢ e₁ ≣₁ e₂ = ⟦ e₁ ⟧ ≐ ⟦ e₂ ⟧ where ⟦_⟧ = Semantics L @@ -58,7 +58,7 @@ _,_⊢_≤_ : ∀ (L₁ L₂ : VariabilityLanguage V) → Expression L₁ A → Expression L₂ A - → Set + → Set₁ L₁ , L₂ ⊢ e₁ ≤ e₂ = ⟦ e₁ ⟧₁ ⊆ ⟦ e₂ ⟧₂ where ⟦_⟧₁ = Semantics L₁ @@ -69,7 +69,7 @@ _,_⊢_≣_ : ∀ (L₁ L₂ : VariabilityLanguage V) → Expression L₁ A → Expression L₂ A - → Set + → Set₁ L₁ , L₂ ⊢ e₁ ≣ e₂ = ⟦ e₁ ⟧₁ ≅ ⟦ e₂ ⟧₂ where ⟦_⟧₁ = Semantics L₁ diff --git a/src/Framework/Relation/Index.lagda.md b/src/Framework/Relation/Index.lagda.md index 7205ef65..6297404f 100644 --- a/src/Framework/Relation/Index.lagda.md +++ b/src/Framework/Relation/Index.lagda.md @@ -2,7 +2,7 @@ open import Framework.Definitions using (𝕍; 𝔸) module Framework.Relation.Index (V : 𝕍) where -open import Level using (0ℓ) +open import Level using (0ℓ; suc) open import Relation.Binary using (Setoid; IsEquivalence) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl; sym; trans) open import Function using (_∘_; Congruent) @@ -21,7 +21,7 @@ module _ {A : 𝔸} where ∀ (L : 𝕃) → Expression L A → (c₁ c₂ : Config L) - → Set + → Set₁ ⟪ _ , _ , ⟦_⟧ ⟫ ∋ e ⊢ c₁ ≣ⁱ c₂ = ⟦ e ⟧ c₁ ≡ ⟦ e ⟧ c₂ infix 5 _∋_⊢_≣ⁱ_ @@ -44,7 +44,7 @@ module _ {A : 𝔸} where ≣ⁱ-setoid : ∀ (L : 𝕃) → (e : Expression L A) - → Setoid 0ℓ 0ℓ + → Setoid 0ℓ (suc 0ℓ) ≣ⁱ-setoid L e = record { Carrier = Config L ; _≈_ = L ∋ e ⊢_≣ⁱ_ diff --git a/src/Framework/VariabilityLanguage.lagda.md b/src/Framework/VariabilityLanguage.lagda.md index fc40cd64..c792bc4d 100644 --- a/src/Framework/VariabilityLanguage.lagda.md +++ b/src/Framework/VariabilityLanguage.lagda.md @@ -14,7 +14,7 @@ Hence, the semantics is a function that configures an expression 𝔼-Semantics : 𝕍 → 𝕂 → 𝔼 → Set₁ 𝔼-Semantics V K E = ∀ {A : 𝔸} → E A → K → V A -record VariabilityLanguage (V : 𝕍) : Set₁ where +record VariabilityLanguage (V : 𝕍) : Set₂ where constructor ⟪_,_,_⟫ field Expression : 𝔼 diff --git a/src/Framework/VariantMap.agda b/src/Framework/VariantMap.agda index f3cffaf5..68b4ee10 100644 --- a/src/Framework/VariantMap.agda +++ b/src/Framework/VariantMap.agda @@ -9,14 +9,14 @@ open import Level using (0ℓ) open import Relation.Binary using (Setoid) import Relation.Binary.PropositionalEquality as Eq -open import Data.EqIndexedSet {V A} +open import Data.EqIndexedSet {A = V A} {-| Variant maps constitute the semantic domain of variability languages. While we defined variant maps to be indexed sets with an arbitrary finite and non-empty index set, we directly reflect these properties via Fin (suc n) here for convenience. -} -VMap : ℕ → Set +VMap : ℕ → Set₁ VMap n = IndexedSet (Fin (suc n)) -- Utility functions for manipulating variant maps. diff --git a/src/Lang/ADT/Path.agda b/src/Lang/ADT/Path.agda index d22aad6f..444d01b8 100644 --- a/src/Lang/ADT/Path.agda +++ b/src/Lang/ADT/Path.agda @@ -123,7 +123,7 @@ Note: The symmetry between the rules walk-left and walk-right causes many 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 : ADT V F A) → Set where +data _starts-at_ : ∀ {A} → (p : Path) → (e : ADT V F A) → Set₁ where tleaf : ∀ {A} {v : V A} ------------------ → [] starts-at (leaf v) @@ -142,14 +142,14 @@ data _starts-at_ : ∀ {A} → (p : Path) → (e : ADT V F A) → Set where An expression does not contain a feature name if all paths do not contain that feature name. -} -_∉'_ : ∀{A} → F → ADT V F A → Set +_∉'_ : ∀{A} → F → ADT V F 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 : ADT V F A) : Set where +record PathConfig {A} (e : ADT V F A) : Set₁ where constructor _is-valid_ field path : Path @@ -171,7 +171,7 @@ walk (D ⟨ _ , r ⟩) ((.(D ↣ false) ∷ pr) is-valid walk-right t) = walk r An expression a is a sub-expression of b iff all valid paths from a lead to paths from b. -} -_subexprof_ : ∀ {A} → ADT V F A → ADT V F A → Set +_subexprof_ : ∀ {A} → ADT V F A → ADT V F A → Set₁ a subexprof b = ∀ (pa : Path) → pa starts-at a → ∃[ pb ] ((pb starts-at b) × (pb endswith pa)) {- diff --git a/src/Lang/FST.agda b/src/Lang/FST.agda index 9b703100..8002b46a 100644 --- a/src/Lang/FST.agda +++ b/src/Lang/FST.agda @@ -77,20 +77,20 @@ a ≉ b = ¬ (a ≈ b) ≉-sym a b a≉b b≈a = a≉b (≈-sym b a b≈a) infix 15 _∈_ -_∈_ : ∀ {i A} → FST i A → List (FST i A) → Set +_∈_ : ∀ {i A} → FST i A → List (FST i A) → Set₁ x ∈ xs = Any (x ≈_) xs infix 15 _∉_ -_∉_ : ∀ {i A} → FST i A → List (FST i A) → Set +_∉_ : ∀ {i A} → FST i A → List (FST i A) → Set₁ x ∉ xs = All (x ≉_) xs -_⊑_ : ∀ {i A} → (xs ys : List (FST i A)) → Set --\squb= +_⊑_ : ∀ {i A} → (xs ys : List (FST i A)) → Set₁ --\squb= xs ⊑ ys = All (_∈ ys) xs -_⋢_ : ∀ {i A} → (xs ys : List (FST i A)) → Set --\squb=n +_⋢_ : ∀ {i A} → (xs ys : List (FST i A)) → Set₁ --\squb=n xs ⋢ ys = Any (_∉ ys) xs -Disjoint : ∀ {i A} → (xs ys : List (FST i A)) → Set --\squb=n +Disjoint : ∀ {i A} → (xs ys : List (FST i A)) → Set₁ --\squb=n Disjoint xs ys = All (_∉ ys) xs -- identity of proofs @@ -161,7 +161,7 @@ branches : ∀ {A} → List (List (FST ∞ A)) → List (FST ∞ A) branches = concat module Impose (AtomSet : 𝔸) where - FSTA : Size → Set + FSTA : Size → Set₁ FSTA i = FST i AtomSet private @@ -188,14 +188,14 @@ module Impose (AtomSet : 𝔸) where ... | no _ = h ∷ (l ⊙ t) a -< ca >- ⊙ (.a -< cb >- ∷ t) | yes refl = a -< ca ⊕ cb >- ∷ t - Unique : ∀ {i} → List (FSTA i) → Set + Unique : ∀ {i} → List (FSTA i) → Set₁ Unique = AllPairs _≉_ mutual - WellFormed : ∀ {i} → FSTA i → Set + WellFormed : ∀ {i} → FSTA i → Set₁ WellFormed (_ -< cs >-) = AllWellFormed cs - AllWellFormed : ∀ {i} → List (FSTA i) → Set + AllWellFormed : ∀ {i} → List (FSTA i) → Set₁ AllWellFormed cs = Unique cs × All WellFormed cs mutual @@ -277,7 +277,7 @@ module Impose (AtomSet : 𝔸) where ⊕-idˡ rs u-rs = ⊕-strangers [] rs u-rs (disjoint-[]ʳ rs) -- A proof that all FSTs xs are already imposed into another list of FSTs ys. - data _lies-in_ : ∀ {i} → List (FSTA i) → List (FSTA i) → Set where + data _lies-in_ : ∀ {i} → List (FSTA i) → List (FSTA i) → Set₁ where lempty : ∀ {i} {xs : List (FSTA i)} ------------- → [] lies-in xs @@ -295,10 +295,10 @@ module Impose (AtomSet : 𝔸) where ------------------------- → (x ∷ xs) lies-in (y ∷ ys) - _slice-of_ : ∀ {i} → FSTA i → FSTA i → Set + _slice-of_ : ∀ {i} → FSTA i → FSTA i → Set₁ x slice-of y = (x ∷ []) lies-in (y ∷ []) - _slice-within_ : ∀ {i} → FSTA i → List (FSTA i) → Set + _slice-within_ : ∀ {i} → FSTA i → List (FSTA i) → Set₁ x slice-within ys = (x ∷ []) lies-in ys lies-in-refl : ∀ {i} → (xs : List (FSTA i)) → xs lies-in xs @@ -351,7 +351,7 @@ module Impose (AtomSet : 𝔸) where ⊕-idem (x ∷ xs) (y ∷ ys) xs-wf ys-wf = {!!} -- Feature Structure Forest - record FSF : Set where + record FSF : Set₁ where constructor _⊚_ field trees : List (FSTA ∞) @@ -372,14 +372,14 @@ module Impose (AtomSet : 𝔸) where which denote the children of the common root. -} infixr 3 _::_ - record Feature : Set where + record Feature : Set₁ where constructor _::_ field name : Name F impl : FSF open Feature public - record SPL : Set where + record SPL : Set₁ where constructor _◀_ field root : A @@ -408,7 +408,7 @@ module Impose (AtomSet : 𝔸) where ⊛-all : List FSF → FSF ⊛-all = foldr _⊛_ 𝟘 - cong-app₂ : ∀ {A C : Set} {T : A → Set} {x y : A} {tx : T x} {ty : T y} + cong-app₂ : ∀ {ℓ} {A C : Set ℓ} {T : A → Set ℓ} {x y : A} {tx : T x} {ty : T y} → (f : (a : A) → T a → C) → x ≡ y → (∀ (a : A) (t u : T a) → t ≡ u) diff --git a/src/Lang/Gruler.agda b/src/Lang/Gruler.agda index dcbdc67b..692b99b9 100644 --- a/src/Lang/Gruler.agda +++ b/src/Lang/Gruler.agda @@ -3,8 +3,9 @@ module Lang.Gruler (F : 𝔽) where open import Data.Bool using (Bool) open import Data.Maybe using (Maybe; just; nothing) -open import Function using (id) +open import Function using (id; _∘_) open import Size using (Size; ↑_; ∞) +import Level open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) @@ -36,12 +37,12 @@ semantics (GChoice chc) = VL2Choice.Semantics GrulerVariant F GrulerVL id chc gruler-has-leaf : ∀ {i} → VLLeaf.Syntax ∈ₛ Gruler i gruler-has-leaf {i} = record - { cons = GAsset + { cons = GAsset ∘ Level.lower ; snoc = snoc' ; id-l = λ _ → refl } - where snoc' : ∀ {A} → Gruler i A → Maybe (Leaf (atoms A)) - snoc' (GAsset A) = just A + where snoc' : ∀ {A} → Gruler i A → Maybe (VLLeaf.Syntax (Gruler i) A) + snoc' (GAsset A) = just (Level.lift A) snoc' _ = nothing gruler-has-choice : VL2Choice.Syntax F ∈ₛ Gruler ∞ diff --git a/src/Lang/VariantList.lagda.md b/src/Lang/VariantList.lagda.md index 9a07af3d..d3f25893 100644 --- a/src/Lang/VariantList.lagda.md +++ b/src/Lang/VariantList.lagda.md @@ -63,7 +63,7 @@ private -- rules for translating a set of variants to a list of variants infix 3 _⊢_⟶_ -data _⊢_⟶_ : ∀ (n : ℕ) → VMap A n → VariantList A → Set where +data _⊢_⟶_ : ∀ (n : ℕ) → VMap A n → VariantList A → Set₁ where -- a singleton set is translated to a singleton list E-zero : ∀ {A} {V : VMap A zero} ------------------------ diff --git a/src/Main.agda b/src/Main.agda index 46ae4ca5..403b75d0 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -34,7 +34,7 @@ A list of programs that we want to run. Each program is implemented in terms of an Experiment. Each experiment is run on each example from a list of examples (i.e., experiment inputs). -} -experimentsToRun : List (ExperimentSetup 0ℓ) +experimentsToRun : List (ExperimentSetup (suc 0ℓ)) experimentsToRun = -- DEPRECATED: Run some example translations from n-ary to binary choice calculus -- DEPRECATED: (CCC ∞ String , exp-to-binary-and-back , cccex-all) ∷ diff --git a/src/Show/Lines.agda b/src/Show/Lines.agda index c533f96f..15986072 100644 --- a/src/Show/Lines.agda +++ b/src/Show/Lines.agda @@ -6,7 +6,7 @@ open import Data.List as List using (List; _∷_; [_]; concat; splitAt; _∷ʳ_) open import Data.Maybe using (nothing; just) open import Data.String using (String; _++_; _==_; replicate; fromChar; toList; fromList; Alignment; fromAlignment) open import Data.Product as Prod using (_,_; proj₁; map₁) -open import Data.Unit using (⊤; tt) +open import Data.Unit.Polymorphic using (⊤; tt) open import Function using (id; _∘_) open import Algebra using (RawMonoid) @@ -39,24 +39,29 @@ length line = Data.String.length (content line) -- Lines monad. -- It captures a sequence of text lines which we aim to print. -Lines' : Set → Set -Lines' = Writer (List.++-[]-rawMonoid Line) +-- Unfortunately, we need Lines' to be able to handle different levels (e.g. in +-- `Test.Experiments.RoundTrp`). Because of the same level limitation of the +-- writer monad, the level of the actual lines data needs to be lifted +-- accordingly. +Lines' : ∀ {ℓ} → Set ℓ → Set ℓ +Lines' {ℓ} A = Writer (List.++-[]-rawMonoid (Level.Lift ℓ Line)) A Lines : Set -Lines = Lines' (Level.Lift Level.zero ⊤) +Lines = Lines' ⊤ -- Export the composition operator to allow do-notation. open Writer using (functor; applicative; monad) public -open RawMonad {f = 0ℓ} (monad {𝕎 = List.++-[]-rawMonoid Line}) using (_>>_; _>>=_) public +module test {ℓ} = RawMonad {ℓ} (monad {𝕎 = List.++-[]-rawMonoid (Level.Lift ℓ Line)}) +open test using (_>>_; _>>=_) public noLines : Lines -noLines = pure (Level.lift tt) +noLines = pure tt where open RawApplicative applicative -- print a single line single : Line → Lines -single line = tell [ line ] +single line = tell [ Level.lift line ] where open RawMonadWriter Writer.monadWriter @@ -67,15 +72,28 @@ lines lines = sequenceA lines >> noLines open List.TraversableA applicative map-lines : {A : Set} → (List Line → List Line) → Lines' A → Lines' A -map-lines f = writer ∘ map₁ f ∘ runWriter +map-lines f = writer ∘ map₁ (List.map Level.lift ∘ f ∘ List.map Level.lower) ∘ runWriter where open RawMonadWriter Writer.monadWriter map : {A : Set} → (Line → Line) → Lines' A → Lines' A map f = map-lines (List.map f) -raw-lines : Lines → List Line -raw-lines = proj₁ ∘ runWriter +raw-lines : ∀ {ℓ} {A : Set ℓ} → Lines' A → List Line +raw-lines = List.map Level.lower ∘ proj₁ ∘ runWriter + +-- Haskell's `void` function. Only required to get the Level `ℓ` back down to +-- `zero`. +void-level : ∀ {ℓ} {A : Set ℓ} → Lines' A → Lines +void-level lines = tell (List.map Level.lift (raw-lines lines)) + where + open RawMonadWriter Writer.monadWriter + +-- `return` which is able to handle `Set`s of arbitrary levels. +return-level : ∀ {ℓ} {A : Set ℓ} → A → Lines → Lines' A +return-level a lines = writer (List.map Level.lift (raw-lines lines) , a) + where + open RawMonadWriter Writer.monadWriter for-loop : ∀ {ℓ} {A : Set ℓ} → List A → (A → Lines) → Lines for-loop items op = lines (List.map op items) @@ -117,7 +135,7 @@ suffix s = mantle "" s modifyLastLine : (Line → Line) -> Lines → Lines modifyLastLine f ls with List.unsnoc (raw-lines ls) modifyLastLine f ls | nothing = noLines -modifyLastLine f ls | just (init , last) = tell (init ∷ʳ f last) +modifyLastLine f ls | just (init , last) = tell (List.map Level.lift (init ∷ʳ f last)) where open RawMonadWriter Writer.monadWriter diff --git a/src/Test/Examples/CCC.agda b/src/Test/Examples/CCC.agda index 8480c1b5..1b503df0 100644 --- a/src/Test/Examples/CCC.agda +++ b/src/Test/Examples/CCC.agda @@ -17,7 +17,7 @@ open import Lang.All open CCC -- use strings as dimensions open import Test.Example -CCCExample : Set +CCCExample : Set₁ CCCExample = Example (CCC String ∞ (String , String._≟_)) -- some smart constructors diff --git a/src/Test/Examples/OC.agda b/src/Test/Examples/OC.agda index c724ad3c..33aa0ed4 100644 --- a/src/Test/Examples/OC.agda +++ b/src/Test/Examples/OC.agda @@ -12,7 +12,7 @@ open OC open import Test.Example -OCExample : Set +OCExample : Set₁ OCExample = Example (WFOC String ∞ (String , String._≟_)) optex-unary : OCExample diff --git a/src/Test/Experiments/RoundTrip.agda b/src/Test/Experiments/RoundTrip.agda index 9e2ba1bf..82ca2447 100644 --- a/src/Test/Experiments/RoundTrip.agda +++ b/src/Test/Experiments/RoundTrip.agda @@ -49,22 +49,20 @@ CCC→NCC-Exact : (e : CCC.CCC Feature ∞ Artifact) → NCC.NCC ⌈ e ⌉ Featu CCC→NCC-Exact e = CCC-to-NCC.translate ⌈ e ⌉ e (numberOfAlternatives≤⌈_⌉ e) -translate : {E₁ : Set} → {E₂ : E₁ → Set} → (e : E₁) → String → ((e : E₁) → E₂ e) → (E₂ e → Lines) → Lines' (E₂ e) -translate e E₂-name translator show = do +translate : {E₁ : Set₁} → {E₂ : E₁ → Set₁} → (e : E₁) → String → ((e : E₁) → E₂ e) → (E₂ e → Lines) → Lines' (E₂ e) +translate e E₂-name translator show = return-level e' do linebreak [ Center ]> "│" [ Center ]> " │ translate" [ Center ]> "↓" linebreak - let e' = translator e - pretty-e' = show e' [ Center ]> E₂-name overwrite-alignment-with Center (boxed (6 + width pretty-e') "" pretty-e') [ Center ]> "proven to have the same semantics as the previous expression" - pure e' where - open RawApplicative applicative + e' = translator e + pretty-e' = show e' compile : ∀ {VL₁ VL₂ : VariabilityLanguage Variant} → Expression VL₁ Artifact @@ -82,12 +80,13 @@ get round-trip ex@(name ≔ ccc) = do overwrite-alignment-with Center (boxed (6 + width pretty-ccc) "" pretty-ccc) - ncc ← translate ccc "NCC" CCC→NCC-Exact (NCC.Pretty.pretty id) - ncc2 ← compile ncc "NCC" (shrinkTo2Compiler ⌈ ccc ⌉) (NCC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ)) - 2cc ← compile ncc2 "2CC" NCC-2→2CC (2CC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ)) - adt ← compile 2cc "ADT" 2CC→ADT (ADT.pretty (show-rose id) (String.diagonal-ℕ ∘ map₂ Fin.toℕ)) - variantList ← compile adt "VariantList" (ADT→VariantList (decidableEquality-× String._≟_ Fin._≟_)) (VariantList.pretty (show-rose id)) - ccc' ← compile variantList "CCC" (VariantList→CCC "default feature") (CCC.pretty id) + void-level do + ncc ← translate ccc "NCC" CCC→NCC-Exact (NCC.Pretty.pretty id) + ncc2 ← compile ncc "NCC" (shrinkTo2Compiler ⌈ ccc ⌉) (NCC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ)) + 2cc ← compile ncc2 "2CC" NCC-2→2CC (2CC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ)) + adt ← compile 2cc "ADT" 2CC→ADT (ADT.pretty (show-rose id) (String.diagonal-ℕ ∘ map₂ Fin.toℕ)) + variantList ← compile adt "VariantList" (ADT→VariantList (decidableEquality-× String._≟_ Fin._≟_)) (VariantList.pretty (show-rose id)) + do compile variantList "CCC" (VariantList→CCC "default feature") (CCC.pretty id) linebreak diff --git a/src/Test/UnitTest.agda b/src/Test/UnitTest.agda index 07cb4733..5db15edf 100644 --- a/src/Test/UnitTest.agda +++ b/src/Test/UnitTest.agda @@ -23,38 +23,38 @@ open Eq using (refl) public Unit tests are theorems on concrete examples that the Agda type checker can figure out by itself. -} -UnitTest : ∀ {ℓ} (Data : Set ℓ) → Set (suc 0ℓ ⊔ ℓ) -UnitTest Data = Data → Set +UnitTest : ∀ {ℓ₁ ℓ₂} (Data : Set ℓ₂) → Set (suc ℓ₁ ⊔ ℓ₂) +UnitTest {ℓ₁} Data = Data → Set ℓ₁ -ExamplesTest : ∀ {ℓ} (Data : Set ℓ) → Set (suc 0ℓ ⊔ ℓ) -ExamplesTest Data = UnitTest (List (Example Data)) +ExamplesTest : ∀ {ℓ₁ ℓ₂} (Data : Set ℓ₂) → Set (suc ℓ₁ ⊔ ℓ₂) +ExamplesTest {ℓ₁} Data = UnitTest {ℓ₁} (List (Example Data)) -RunTest : ∀ {ℓ} {Data : Set ℓ} - → UnitTest Data +RunTest : ∀ {ℓ₁ ℓ₂} {Data : Set ℓ₂} + → UnitTest {ℓ₁} Data → Data - → Set + → Set ℓ₁ RunTest utest dataset = utest dataset -ForExample : ∀ {ℓ} {Data : Set ℓ} - → UnitTest Data - → UnitTest (Example Data) +ForExample : ∀ {ℓ₁ ℓ₂} {Data : Set ℓ₂} + → UnitTest {ℓ₁} Data + → UnitTest {ℓ₁} (Example Data) ForExample utest (e called _) = utest e -ForAll : ∀ {Data : Set} - → UnitTest Data - → UnitTest (List Data) +ForAll : ∀ {ℓ₁ ℓ₂} {Data : Set ℓ₂} + → UnitTest {ℓ₁} Data + → UnitTest {ℓ₁ ⊔ ℓ₂} (List Data) ForAll utest datasets = All utest datasets -ForAllExamples : ∀ {Data : Set} - → UnitTest Data - → ExamplesTest Data +ForAllExamples : ∀ {ℓ₁ ℓ₂} {Data : Set ℓ₂} + → UnitTest {ℓ₁} Data + → ExamplesTest {ℓ₁ ⊔ ℓ₂} Data ForAllExamples = ForAll ∘ ForExample -- syntactic sugar for ForAllExamples that puts the example list in front -ForAllExamplesIn : ∀ {Data : Set} +ForAllExamplesIn : ∀ {ℓ₁ ℓ₂} {Data : Set ℓ₂} → List (Example Data) - → UnitTest Data - → Set + → UnitTest {ℓ₁} Data + → Set (ℓ₁ ⊔ ℓ₂) ForAllExamplesIn ex utest = ForAllExamples utest ex test-translation : ∀ {V A} diff --git a/src/Translation/Construct/2Choice-to-Choice.agda b/src/Translation/Construct/2Choice-to-Choice.agda index 06f18753..f9103c95 100644 --- a/src/Translation/Construct/2Choice-to-Choice.agda +++ b/src/Translation/Construct/2Choice-to-Choice.agda @@ -79,7 +79,7 @@ default-fnoc-satisfies-contract : ∀ (f : Q) → FnocContract f default-fnoc suc→false (default-fnoc-satisfies-contract f) c cf≡suc rewrite cf≡suc = refl zero→true (default-fnoc-satisfies-contract f) c cf≡zero rewrite cf≡zero = refl -module Translate (S : Setoid 0ℓ 0ℓ) where +module Translate {ℓ} (S : Setoid ℓ ℓ) where open Setoid S module ≈-Eq = IsEquivalence isEquivalence diff --git a/src/Translation/Construct/Choice-to-2Choice.agda b/src/Translation/Construct/Choice-to-2Choice.agda index 1d1c407a..c0bc6bb7 100644 --- a/src/Translation/Construct/Choice-to-2Choice.agda +++ b/src/Translation/Construct/Choice-to-2Choice.agda @@ -102,7 +102,7 @@ record FnocContract (D : Q) (fnoc : 2Config → NConfig) : Set where → fnoc c D ≢ i open FnocContract -module Translate (A : Set) where +module Translate {ℓ} (A : Set ℓ) where show-nested-choice : ∀ {i} → (Q → String) → (A → String) → NestedChoice i A → String show-nested-choice show-q = NestedChoice.show-nested-choice (show-IndexedName show-q) diff --git a/src/Translation/Lang/2CC-to-NCC.agda b/src/Translation/Lang/2CC-to-NCC.agda index 561e8433..ffadc384 100644 --- a/src/Translation/Lang/2CC-to-NCC.agda +++ b/src/Translation/Lang/2CC-to-NCC.agda @@ -83,7 +83,7 @@ module 2Ary where 2CC.⟦ d ⟨ l , r ⟩ ⟧ (fnoc config) ∎ where - lemma : {A : Set} → {a b : A} → Vec.lookup (a ∷ b ∷ []) (config d) ≡ (if fnoc config d then a else b) + lemma : ∀ {ℓ} {A : Set ℓ} {a b : A} → Vec.lookup (a ∷ b ∷ []) (config d) ≡ (if fnoc config d then a else b) lemma with config d ... | zero = refl ... | suc zero = refl @@ -122,7 +122,7 @@ module 2Ary where NCC.⟦ translate (d ⟨ l , r ⟩) ⟧ (conf config) ∎ where - lemma : {A : Set} → {a b : A} → (if config d then a else b) ≡ Vec.lookup (a ∷ b ∷ []) (conf config d) + lemma : ∀ {ℓ} {A : Set ℓ} {a b : A} → (if config d then a else b) ≡ Vec.lookup (a ∷ b ∷ []) (conf config d) lemma with config d ... | true = refl ... | false = refl diff --git a/src/Translation/Lang/ADT/DeadElim.agda b/src/Translation/Lang/ADT/DeadElim.agda index 5f4dbcf2..c3bbc377 100644 --- a/src/Translation/Lang/ADT/DeadElim.agda +++ b/src/Translation/Lang/ADT/DeadElim.agda @@ -31,7 +31,7 @@ A ADT is undead if it does not contain any dead branches. This is the case if any path from the root to a leaf does not contain a feature name twice. -} -Undead : ∀ {A} (e : ADT V F A) → Set +Undead : ∀ {A} (e : ADT V F A) → Set₁ Undead e = ∀ (p : Path) → p starts-at e → Unique p {- @@ -78,7 +78,7 @@ undead-choice : ∀ {A} {D} {l r : ADT V F A} undead-choice u-l u-r D∉l D∉r (.(_ ↣ true ) ∷ p) (walk-left t) = ∉→All-different p (D∉l p t) ∷ (u-l p t) undead-choice u-l u-r D∉l D∉r (.(_ ↣ false) ∷ p) (walk-right t) = ∉→All-different p (D∉r p t) ∷ (u-r p t) -record UndeadADT (A : 𝔸) : Set where +record UndeadADT (A : 𝔸) : Set₁ where constructor _⊚_ -- \oo field node : ADT V F A diff --git a/src/Translation/Lang/CCC-to-NCC.agda b/src/Translation/Lang/CCC-to-NCC.agda index aa4e8518..60c292b7 100644 --- a/src/Translation/Lang/CCC-to-NCC.agda +++ b/src/Translation/Lang/CCC-to-NCC.agda @@ -65,15 +65,15 @@ module Exact where mutual -- A proof that an expression's longest alternative list is at maximum `n`. - data NumberOfAlternatives≤ {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → CCC D i A → Set where + data NumberOfAlternatives≤ {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → CCC D i A → Set₁ where maxArtifact : {i : Size} → {a : atoms A} → {cs : List (CCC D i A)} → NumberOfAlternatives≤-List n {i} cs → NumberOfAlternatives≤ n {↑ i} (a -< cs >-) maxChoice : {i : Size} → {d : D} → {cs : List⁺ (CCC D i A)} → List⁺.length cs ≤ ℕ≥.toℕ n → NumberOfAlternatives≤-List⁺ n {i} cs → NumberOfAlternatives≤ n {↑ i} (d ⟨ cs ⟩) - data NumberOfAlternatives≤-List {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → List (CCC D i A) → Set where + data NumberOfAlternatives≤-List {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → List (CCC D i A) → Set₁ where [] : {i : Size} → NumberOfAlternatives≤-List n {i} [] _∷_ : {i : Size} → {c : CCC D i A} → {cs : List (CCC D i A)} → NumberOfAlternatives≤ n {i} c → NumberOfAlternatives≤-List n {i} cs → NumberOfAlternatives≤-List n {i} (c ∷ cs) - data NumberOfAlternatives≤-List⁺ {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → List⁺ (CCC D i A) → Set where + data NumberOfAlternatives≤-List⁺ {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → List⁺ (CCC D i A) → Set₁ where _∷_ : {i : Size} → {c : CCC D i A} → {cs : List (CCC D i A)} → NumberOfAlternatives≤ n {i} c → NumberOfAlternatives≤-List n {i} cs → NumberOfAlternatives≤-List⁺ n {i} (c ∷ cs) mutual @@ -129,7 +129,7 @@ module Exact where d ⟨ Vec.saturate max≤n (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) ⟩ -- TODO Can probably be generalized - zipWith : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set} + zipWith : ∀ {ℓ} {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set ℓ} → (n : ℕ≥ 2) → ((expr : CCC D i A) → NumberOfAlternatives≤ n expr → Result) → (cs : List (CCC D i A)) @@ -138,16 +138,16 @@ module Exact where zipWith n f [] [] = [] zipWith n f (c ∷ cs) (max-c ∷ max-cs) = f c max-c ∷ zipWith n f cs max-cs - length-zipWith : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set} + length-zipWith : ∀ {ℓ} {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set ℓ} → (n : ℕ≥ 2) → {f : (expr : CCC D i A) → NumberOfAlternatives≤ n expr → Result} → (cs : List (CCC D i A)) → (max-cs : NumberOfAlternatives≤-List n cs) - → List.length (zipWith {i} n f cs max-cs) ≡ List.length cs + → List.length (zipWith {i = i} n f cs max-cs) ≡ List.length cs length-zipWith n [] [] = refl length-zipWith n (c ∷ cs) (max-c ∷ max-cs) = Eq.cong suc (length-zipWith n cs max-cs) - map∘zipWith : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result₁ Result₂ : Set} + map∘zipWith : ∀ {ℓ} {i : Size} {D : 𝔽} {A : 𝔸} {Result₁ Result₂ : Set ℓ} → (n : ℕ≥ 2) → {g : Result₁ → Result₂} → {f : (expr : CCC D i A) → NumberOfAlternatives≤ n expr → Result₁} @@ -157,7 +157,7 @@ module Exact where map∘zipWith n [] [] = refl map∘zipWith n (c ∷ cs) (max-c ∷ max-cs) = Eq.cong₂ _∷_ refl (map∘zipWith n cs max-cs) - zipWith-cong : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set} + zipWith-cong : ∀ {ℓ} {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set ℓ} → (n : ℕ≥ 2) → {f g : (expr : CCC D i A) → NumberOfAlternatives≤ n expr → Result} → ((e : CCC D i A) → (max-e : NumberOfAlternatives≤ n e) → f e max-e ≡ g e max-e) @@ -167,7 +167,7 @@ module Exact where zipWith-cong n f≗g [] [] = refl zipWith-cong n f≗g (c ∷ cs) (max-c ∷ max-cs) = Eq.cong₂ _∷_ (f≗g c max-c) (zipWith-cong n f≗g cs max-cs) - zipWith⇒map : ∀ {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set} + zipWith⇒map : ∀ {ℓ} {i : Size} {D : 𝔽} {A : 𝔸} {Result : Set ℓ} → (n : ℕ≥ 2) → (f : (expr : CCC D i A) → Result) → (cs : List (CCC D i A)) diff --git a/src/Translation/Lang/NCC-to-2CC.agda b/src/Translation/Lang/NCC-to-2CC.agda index acab8086..c2217af3 100644 --- a/src/Translation/Lang/NCC-to-2CC.agda +++ b/src/Translation/Lang/NCC-to-2CC.agda @@ -83,7 +83,7 @@ module 2Ary where NCC.⟦ d ⟨ l ∷ r ∷ [] ⟩ ⟧ (fnoc config) ∎ where - lemma : ∀ {A : Set} {a b : A} → (if config d then a else b) ≡ Vec.lookup (a ∷ b ∷ []) (fnoc config d) + lemma : ∀ {ℓ} {A : Set ℓ} {a b : A} → (if config d then a else b) ≡ Vec.lookup (a ∷ b ∷ []) (fnoc config d) lemma with config d ... | true = refl ... | false = refl @@ -122,7 +122,7 @@ module 2Ary where 2CC.⟦ translate (d ⟨ l ∷ r ∷ [] ⟩) ⟧ (conf config) ∎ where - lemma : {A : Set} → {a b : A} → Vec.lookup (a ∷ b ∷ []) (config d) ≡ (if conf config d then a else b) + lemma : ∀ {ℓ} {A : Set ℓ} → {a b : A} → Vec.lookup (a ∷ b ∷ []) (config d) ≡ (if conf config d then a else b) lemma with config d ... | zero = refl ... | suc zero = refl diff --git a/src/Translation/Lang/OC-to-2CC.lagda.md b/src/Translation/Lang/OC-to-2CC.lagda.md index b1f80617..b144f6e3 100644 --- a/src/Translation/Lang/OC-to-2CC.lagda.md +++ b/src/Translation/Lang/OC-to-2CC.lagda.md @@ -78,7 +78,7 @@ This is in fact working just like "map" does on lists but we need the zipper to The zipper does not store enough information to fully restore a tree from the current focus. This limitation is intended to keep the structure as simple as possible and only as complex as necessary. ```agda -record Zip (work : ℕ) (i : Size) (A : 𝔸) : Set where +record Zip (work : ℕ) (i : Size) (A : 𝔸) : Set₁ where -- In the paper, we write _⦇_≪_⦈ for this constructor. -- However, in Agda, using ⦇ and ⦈ is forbidden. constructor _-<_≪_>- --\T @@ -108,7 +108,7 @@ data _⊢_⟶ₒ_ : → (i : Size) -- We have to make sizes explicit here because otherwise, Agda sometimes infers ∞ which makes termination checking fail. → Zip n i A → 2CC F ∞ A - → Set + → Set₁ infix 3 _⊢_⟶ₒ_ data _⊢_⟶ₒ_ where {-| @@ -170,7 +170,7 @@ data _⟶_ : ∀ {i : Size} {A : 𝔸} → WFOC F i A → 2CC F ∞ A - → Set + → Set₁ infix 4 _⟶_ data _⟶_ where T-root : @@ -216,10 +216,10 @@ Every OC expression is OC→2CCd to at most one 2CC expression. Every OC expression is OC→2CCd to at least one 2CC expression. Since we have already proven determinism, the proof for totality and thus a translation is unique. ```agda -Totalₒ : ∀ {n} {i} {A} → (e : Zip n i A) → Set +Totalₒ : ∀ {n} {i} {A} → (e : Zip n i A) → Set₁ Totalₒ {i = i} e = ∃[ b ] (i ⊢ e ⟶ₒ b) -Total : ∀ {i} {A} → (e : WFOC F i A) → Set +Total : ∀ {i} {A} → (e : WFOC F i A) → Set₁ Total {i} e = ∃[ b ] (e ⟶ b) -- Smart constructor for Totalₒ that does not require naming the expression explicitly. diff --git a/src/Util/List.agda b/src/Util/List.agda index 8c9efae2..825a5c09 100644 --- a/src/Util/List.agda +++ b/src/Util/List.agda @@ -65,7 +65,7 @@ map-find-or-last f (suc i) (x ∷ y ∷ zs) = (find-or-last (suc i) ∘ map⁺ f) (x ∷ y ∷ zs) ∎ -find-or-last⇒lookup : ∀ {A : Set} {i : ℕ} +find-or-last⇒lookup : ∀ {ℓ} {A : Set ℓ} {i : ℕ} → (x : A) → (xs : List A) → find-or-last i (x ∷ xs) ≡ Vec.lookup (x ∷ Vec.fromList xs) (ℕ≥.cappedFin i) @@ -73,7 +73,7 @@ find-or-last⇒lookup {i = i} x [] = refl find-or-last⇒lookup {i = zero} x (y ∷ ys) = refl find-or-last⇒lookup {i = suc i} x (y ∷ ys) = find-or-last⇒lookup y ys -lookup⇒find-or-last : ∀ {A : Set} {n m : ℕ} +lookup⇒find-or-last : ∀ {ℓ} {A : Set ℓ} {n m : ℕ} → (vec : Vec A (suc n)) → Vec.lookup vec (ℕ≥.cappedFin m) ≡ find-or-last m (List⁺.fromVec vec) lookup⇒find-or-last {n = zero} {m = m} (x ∷ []) = refl diff --git a/src/Util/Suffix.agda b/src/Util/Suffix.agda index 956d2e08..4aba647a 100644 --- a/src/Util/Suffix.agda +++ b/src/Util/Suffix.agda @@ -15,7 +15,7 @@ This relation is a partial order because it is - antisymmetric (yet to prove), - and transitive (to prove). -} -data _endswith_ {ℓ} {A : Set ℓ} : List A → List A → Set where +data _endswith_ {ℓ} {A : Set ℓ} : List A → List A → Set ℓ where match : ∀ (p : List A) ------------ → p endswith p -- reflexive diff --git a/src/Util/Vec.agda b/src/Util/Vec.agda index 65bdc7cc..a99ab307 100644 --- a/src/Util/Vec.agda +++ b/src/Util/Vec.agda @@ -11,7 +11,7 @@ import Util.List as List open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -- Duplicates the last element of a vector to increase its length. -saturate : ∀ {A : Set} {n : ℕ≥ 1} {m : ℕ} +saturate : ∀ {ℓ} {A : Set ℓ} {n : ℕ≥ 1} {m : ℕ} → ℕ≥.toℕ n ≤ m → Vec A (ℕ≥.toℕ n) → Vec A m @@ -19,20 +19,20 @@ saturate {n = sucs zero} {m = suc zero} suc-n≤m (x ∷ []) = x ∷ [] saturate {n = sucs zero} {m = suc (suc m)} suc-n≤m (x ∷ []) = x ∷ saturate (s≤s z≤n) (x ∷ []) saturate {n = sucs (suc n)} {m = m} (s≤s suc-n≤m) (x ∷ xs) = x ∷ saturate suc-n≤m xs -saturate-map : ∀ {n : ℕ≥ 1} {m : ℕ} {A B : Set} +saturate-map : ∀ {ℓ} {n : ℕ≥ 1} {m : ℕ} {A B : Set ℓ} → (n≤m : ℕ≥.toℕ n ≤ m) → (f : A → B) → (vec : Vec A (ℕ≥.toℕ n)) → saturate {n = n} n≤m (Vec.map f vec) ≡ Vec.map f (saturate {n = n} n≤m vec) -saturate-map {sucs zero} {suc zero} (s≤s n≤m) f (x ∷ []) = refl -saturate-map {sucs zero} {suc (suc m)} (s≤s n≤m) f (x ∷ []) - rewrite saturate-map {sucs zero} {suc m} (s≤s z≤n) f (x ∷ []) +saturate-map {n = sucs zero} {suc zero} (s≤s n≤m) f (x ∷ []) = refl +saturate-map {n = sucs zero} {suc (suc m)} (s≤s n≤m) f (x ∷ []) + rewrite saturate-map {n = sucs zero} {suc m} (s≤s z≤n) f (x ∷ []) = refl -saturate-map {sucs (suc n)} {m} (s≤s n≤m) f (x ∷ xs) +saturate-map {n = sucs (suc n)} {m} (s≤s n≤m) f (x ∷ xs) rewrite saturate-map n≤m f xs = refl -lookup-saturate : ∀ {A : Set} {n : ℕ≥ 1} {m : ℕ} +lookup-saturate : ∀ {ℓ} {A : Set ℓ} {n : ℕ≥ 1} {m : ℕ} → (n≤m : ℕ≥.toℕ n ≤ m) → (vec : Vec A (ℕ≥.toℕ n)) → (i : Fin m)