feat: Use partial indexing operation for Lists

Co-authored-by: Reed Mullanix <reedmullanix@gmail.com>

Author: 4e554c4c

1lab.agda-lib

@@ -3,7 +3,6 @@ include:
   src
   wip
   _build
-  .
 flags:
   --cubical
   --no-load-primitives

src/Data/List/Base.lagda.md

@@ -9,13 +9,16 @@ open import Data.Maybe.Base
 open import Data.Bool.Base
 open import Data.Dec.Base
 open import Data.Fin.Base
+open import Data.Irr
 
 open import Meta.Traversable
 open import Meta.Foldable
 open import Meta.Append
 open import Meta.Idiom
 open import Meta.Bind
 open import Meta.Alt
+
+import Data.Nat.Base as Nat
 ```
 -->
 
@@ -338,10 +341,22 @@ lookup x ((k , v) ∷ xs) with x ≡? k
 ... | yes _ = just v
 ... | no  _ = lookup x xs
 
+_!?_ : List A → Nat → Maybe A
+[] !? n = nothing
+(x ∷ xs) !? zero = just x
+(x ∷ xs) !? suc n = xs !? n
+
+-- Make sure that all of the actual computation is guarded behind irrelevance to make this zero cost
+!?-just : ∀ (xs : List A) (n : Nat) → .(n Nat.< length xs) → is-just (xs !? n)
+!?-just {A = a} xs n n<xs = erase (worker xs n n<xs)
+  where
+    worker : ∀ (xs : List A) (n : Nat) → n Nat.< length xs → is-true (is-just? (xs !? n))
+    worker (x ∷ xs) zero n<xs = tt
+    worker (x ∷ xs) (suc n) n<xs = worker xs n (Nat.≤-peel n<xs)
+
 _!_ : (l : List A) → Fin (length l) → A
-(x ∷ xs) ! n with fin-view n
-... | zero  = x
-... | suc i = xs ! i
+xs ! (fin n ⦃ forget pf ⦄) = from-just! $ !?-just xs n pf
+
 
 tabulate : ∀ {n} (f : Fin n → A) → List A
 tabulate {n = zero}  f = []

src/Data/List/Sigma.agda

@@ -42,19 +42,19 @@ module _ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} where
     member-pair-inv x (y ∷ ys) a b (there it)   = ap there (member-pair-inv x ys a b it)
 
     rem₀
-      : ∀ {x a} (ys : ∀ a → List (B a)) (b : B a) (p : a ≡ᵢ x) ix .{q} .{q'}
-      → (Id-over B (symᵢ p) (ys x ! fin ix ⦃ forget q ⦄) b) ≃ (ys a ! fin ix ⦃ forget q' ⦄ ≡ᵢ b)
+      : ∀ {x a} (ys : ∀ a → List (B a)) (b : B a) (p : a ≡ᵢ x) ix {q : Irr (ix Nat.< length (ys x))} {q' : Irr (ix Nat.< length (ys a))}
+      → (Id-over B (symᵢ p) (ys x ! fin ix ⦃ q ⦄) b) ≃ (ys a ! fin ix ⦃ q' ⦄ ≡ᵢ b)
     rem₀ {x = x} {a} ys b p ix {q} {q'} = Jᵢ'
-      (λ a x p → ∀ b .q .q' → Id-over B (symᵢ p) (ys x ! fin ix ⦃ forget q ⦄) b ≃ (ys a ! fin ix ⦃ forget q' ⦄ ≡ᵢ b))
+      (λ a x p → ∀ b q q' → Id-over B (symᵢ p) (ys x ! fin ix ⦃ q ⦄) b ≃ (ys a ! fin ix ⦃ q' ⦄ ≡ᵢ b))
       (λ b q q' → id , id-equiv)
       p b q q'
 
     rem₁ : ∀ {x a} (ys : ∀ a → List (B a)) (b : B _) (p : a ≡ᵢ x) → fibre' (ys x) p b → fibreᵢ (ys a !_) b
-    rem₁ {x = x} {a} ys b p (fin ix ⦃ forget q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.to (rem₀ ys b p ix) r where
+    rem₁ {x = x} {a} ys b p (fin ix ⦃ forget q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.to (rem₀ ys b p ix {forget q} {q'}) r where
       q' = forget (transport (λ i → suc ix Nat.≤ length (ys (Id≃path.to p (~ i)))) q)
 
     rem₂ : ∀ {x a} (ys : ∀ a → List (B a)) (b : B _) (p : a ≡ᵢ x) → fibreᵢ (ys a !_) b → fibre' (ys x) p b
-    rem₂ {x = x} {a} ys b p (fin ix ⦃ forget q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.from (rem₀ ys b p ix) r where
+    rem₂ {x = x} {a} ys b p (fin ix ⦃ forget q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.from (rem₀ ys b p ix {q'} {forget q}) r where
       q' = forget (transport (λ i → suc ix Nat.≤ length (ys (Id≃path.to p i))) q)
 
   sigma-member : ∀ {a b xs ys} → a ∈ₗ xs → b ∈ₗ ys a → (a , b) ∈ₗ sigma xs ys

src/Data/Maybe/Base.lagda.md

@@ -4,6 +4,7 @@ open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type
 
+open import Data.Bool.Base
 open import Data.Dec.Base
 
 open import Meta.Traversable
@@ -83,19 +84,27 @@ from-just def nothing = def
 
 <!--
 ```agda
-is-just : Maybe A → Type
-is-just (just _) = ⊤
-is-just nothing = ⊥
+is-just? : Maybe A → Bool
+is-just? nothing = false
+is-just? (just _) = true
 
-is-nothing : Maybe A → Type
-is-nothing (just _) = ⊥
-is-nothing nothing = ⊤
+record is-just (m : Maybe A) : Type where
+  constructor erase
+  field
+    .witness : is-true (is-just? m)
 
-nothing≠just : {x : A} → ¬ (nothing ≡ just x)
-nothing≠just p = subst is-nothing p tt
+
+from-just! : ∀ {x} → is-just x → A
+from-just! {x = just x} _ = x
 
 just≠nothing : {x : A} → ¬ (just x ≡ nothing)
-just≠nothing p = subst is-just p tt
+just≠nothing p = subst is-just' p tt  where
+  is-just' : Maybe A → Type
+  is-just' (just _) = ⊤
+  is-just' nothing = ⊥
+
+nothing≠just : {x : A} → ¬ (nothing ≡ just x)
+nothing≠just p = just≠nothing (sym p)
 
 just-inj : ∀ {x y : A} → just x ≡ just y → x ≡ y
 just-inj {x = x} = ap (from-just x)
@@ -106,6 +115,7 @@ instance
   Discrete-Maybe .decide (just x) nothing  = no just≠nothing
   Discrete-Maybe .decide nothing (just x)  = no nothing≠just
   Discrete-Maybe .decide nothing nothing   = yes refl
+
 ```
 -->
 

src/Data/Vec/Base.lagda.md

@@ -4,9 +4,11 @@ open import 1Lab.Path
 open import 1Lab.Type
 
 open import Data.Product.NAry
+open import Data.Maybe.Base
 open import Data.List.Base hiding (head ; tail ; lookup) renaming (tabulate to tabulateℓ ; _++_ to _++ℓ_)
 open import Data.Fin.Base
-open import Data.Nat.Base
+open import Data.Nat.Base as Nat
+open import Data.Id.Base
 
 open import Meta.Idiom
 
@@ -59,6 +61,13 @@ instance
 length-uncons : ∀ {xs n x} → Length {A = A} (x ∷ xs) (suc n) → Length xs n
 length-uncons (suc l) = l
 
+has-lengthᵢ : ∀ {xs : List A} {n : Nat} → Irr (Length xs n) → length xs ≡ᵢ n
+has-lengthᵢ {xs = []} {n = zero} len = reflᵢ
+has-lengthᵢ {xs = x ∷ xs} {n = suc n} len = apᵢ suc $ has-lengthᵢ $ length-uncons <$> len
+
+has-length : ∀ {xs : List A} {n : Nat} → Irr (Length xs n) → length xs ≡ n
+has-length l = Id≃path.to $ has-lengthᵢ l
+
 record Vec {ℓ} (A : Type ℓ) (n : Nat) : Type ℓ where
   constructor vec
   field
@@ -89,9 +98,8 @@ tail : Vec A (suc n) → Vec A n
 tail v with (x ∷ xs) ← vec-view v = xs
 
 lookup : Vec A n → Fin n → A
-lookup xs n with fin-view n
-... | zero  = head xs
-... | suc i = lookup (tail xs) i
+lookup (vec xs ⦃ forget len ⦄) (fin n ⦃ forget n<xs ⦄) =
+  from-just! $ !?-just xs n $ᵢ ≤-trans n<xs $ subst (Nat._≤ length xs) (has-length $ forget len) Nat.x≤x
 
 instance
   From-prod-Vec : From-product A (Vec A)