Merge pull request #33 from pmbittner/no-large-indicies-by-level-gene…

…ralization

Get rid of `--large-indicies` using higher levels

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

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,15 +110,15 @@ 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 (ℕ)
 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.

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 : ℂ

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

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