vlookup

Author: effectfully

Core.agda

@@ -55,8 +55,7 @@ _≅_ : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α} {B : Univ β} -> 
 
 data Desc {i b} {ι : Level i} (I : Type ι) (β : Level b) : Set where
   var : ⟦ I ⟧ -> Desc I β
-  π   : ∀ {a} {α : Level a} .{{_ : a ≤ₘ b}}
-      -> (A : Univ α) -> (⟦ A ⟧ -> Desc I β) -> Desc I β
+  π   : ∀ {a} {α : Level a} .{{_ : a ≤ₘ b}} -> (A : Univ α) -> (⟦ A ⟧ -> Desc I β) -> Desc I β
   _⊛_ : Desc I β -> Desc I β -> Desc I β
 
 ⟦_⟧ᵈ : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι}
@@ -97,15 +96,12 @@ data Univ where
   nat  : Type₀
   enum : ℕ -> Type₀
   univ : ∀ {a} -> (α : Level a) -> Type α
-  σ    : ∀ {a b} {α : Level a} {β : Level b}
-       -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔  β)
-  π    : ∀ {a b} {α : Level a} {β : Level b}
-       -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔₀ β)
+  σ    : ∀ {a b} {α : Level a} {β : Level b} -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔  β)
+  π    : ∀ {a b} {α : Level a} {β : Level b} -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔₀ β)
   desc : ∀ {a i} {ι : Level i} -> Type ι -> (α : Level a) -> Type α
   imu  : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι} -> Desc I α -> ⟦ I ⟧ -> Univ α
 
-⟦_⟧ⁱ : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α}
-     -> (⟦ A ⟧ -> Univ β) -> ⟦ A ⟧ -> Set
+⟦_⟧ⁱ : ∀ {a b} {α : Level a} {β : Level b} {A : Univ α} -> (⟦ A ⟧ -> Univ β) -> ⟦ A ⟧ -> Set
 ⟦ B ⟧ⁱ x = ⟦ B x ⟧
 
 ⟦ bot          ⟧ = ⊥
@@ -243,8 +239,8 @@ mu D = imu D triv
 liftDesc : ∀ {i a b} {ι : Level i} {α : Level a} {β : Level b} {I : Type ι} .{{_ : a ≤ₘ b}}
          -> Desc I α -> Desc I β
 liftDesc                (var i)            = var i
-liftDesc {b = b} {{q₁}} (π {c} {{q₂}} A D) = π
-  {{pright (pcong (c ⊔ₘ_) q₁) (ptrans (pcong (b ⊔ₘ_) q₂) q₁)}} A λ x -> liftDesc (D x)
+liftDesc {b = b} {{q₁}} (π {c} {{q₂}} A D) =
+  π {{pright (pcong (c ⊔ₘ_) q₁) (ptrans (pcong (b ⊔ₘ_) q₂) q₁)}} A λ x -> liftDesc (D x)
 liftDesc                (D ⊛ E)            = liftDesc D ⊛ liftDesc E
 
 var-inj : ∀ {i b} {ι : Level i} {I : Type ι} {β : Level b} {j₁ j₂ : ⟦ I ⟧}

Data/Vec.agda

@@ -1,6 +1,7 @@
 module OTT.Data.Vec where
 
 open import OTT.Main
+open import OTT.Data.Fin
 
 infixr 5 _∷ᵥ_
 
@@ -53,3 +54,15 @@ elimVec : ∀ {n a p} {α : Level a} {π : Level p} {A : Univ α}
         -> (xs : Vec A n)
         -> ⟦ P xs ⟧
 elimVec P f z = elim P (fromTuple (z , λ n x xs -> f x))
+
+vlookupₑ : ∀ {n m a} {α : Level a} {A : Univ α} -> ⟦ n ≅ m ⇒ fin n ⇒ vec A m ⇒ A ⟧
+vlookupₑ         p (fzeroₑ q)       (vconsₑ r x xs)      = x
+vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vconsₑ {m′} r x xs) =
+  vlookupₑ (left (suc n′) {m} {suc m′} (trans (suc n′) {n} {m} q p) r) i xs
+vlookupₑ {n} {m} p (fzeroₑ {n′} q)  (vnilₑ r)            =
+  ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r
+vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vnilₑ r)            =
+  ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r
+
+vlookup : ∀ {n a} {α : Level a} {A : Univ α} -> Fin n -> Vec A n -> ⟦ A ⟧
+vlookup {n} = vlookupₑ (refl n)

Prelude.agda

@@ -45,6 +45,12 @@ tag-inj : ∀ {α β} {A : Set α} {B : A -> Set β} {x} {y₁ y₂ : B x}
         -> tag {B = B} y₁ ≡ tag y₂ -> y₁ ≡ y₂
 tag-inj prefl = prefl
 
+data Match {ι α} {I : Set ι} {i} (A : I -> Set α) (x : A i) : Set (ι ⊔ₘ α) where
+  matched : ∀ {j} -> (x′ : A j) -> [ A ] x ≅ x′ -> Match A x
+
+match : ∀ {ι α} {I : Set ι} {i} -> (A : I -> Set α) -> (x : A i) -> Match A x
+match A x = matched x irefl
+
 data IMatch {ι α β} {I : Set ι} {i} (A : I -> Set α) {x : A i} 
             (B : ∀ {i} -> A i -> Set β) (y : B x) : Set (ι ⊔ₘ α ⊔ₘ β) where
   imatched : ∀ {i} {x : A i} -> (y′ : B x) -> [ A ][ B ] y ≅ y′ -> IMatch A B y