pvec: add Int-indexed helpers (eigentrust pitfall #12)

racket/prologos/lib/prologos/book/PRELUDE

@@ -77,9 +77,12 @@
 ;; Note: pvec-map, pvec-filter, pvec-fold, set-fold, set-filter,
 ;; map-fold-entries, map-filter-entries, map-map-vals are now native
 ;; parser keywords — no need to import from ops modules.
-;; pvec: pvec-any?, pvec-all?, pvec-from-list-fn, pvec-to-list-fn
+;; pvec: pvec-any?, pvec-all?, pvec-from-list-fn, pvec-to-list-fn,
+;;       pvec-nth-int, pvec-length-int, pvec-take-int, pvec-drop-int
 (imports [prologos::core::pvec :refer [pvec-any? pvec-all?
-                                       pvec-from-list-fn pvec-to-list-fn]])
+                                       pvec-from-list-fn pvec-to-list-fn
+                                       pvec-nth-int pvec-length-int
+                                       pvec-take-int pvec-drop-int]])
 ;; map: map-filter-vals, map-keys-list, map-vals-list, map-merge,
 ;;      map-to-entry-list, map-seq, map-from-seq
 (imports [prologos::core::map  :refer [map-filter-vals map-keys-list

racket/prologos/lib/prologos/core/pvec.prologos

@@ -8,7 +8,7 @@ require [prologos::core::collection-traits :refer [Seqable
                                                     Functor]]
 require [prologos::data::lseq          :refer [LSeq]]
 require [prologos::data::lseq-ops      :refer [list-to-lseq lseq-to-list]]
-require [prologos::data::list           :refer [List nil cons zip-with]]
+require [prologos::data::list           :refer [List nil cons zip-with nth-int take-int drop-int]]
 require [prologos::data::option        :refer [Option some none]]
 require [prologos::data::nat            :refer [lt?]]
 
@@ -146,3 +146,50 @@ spec pvec-zip-with {A B C : Type} [A -> B -> C] [PVec A] [PVec B] -> [PVec C]
   :doc "Combine two PVecs element-wise with a function; truncates to shorter."
 defn pvec-zip-with [f xs ys]
   pvec-from-list [zip-with f [pvec-to-list xs] [pvec-to-list ys]]
+
+;; ========================================
+;; Int-Indexed Operations
+;; ========================================
+;; Mirrors the nth-int / length-int / take-int / drop-int quartet on List
+;; (see prologos::data::list). Use these when your algorithm carries Int
+;; counters (e.g. a budget compared via int-le) and you'd otherwise have
+;; to maintain a parallel Nat counter just to index a PVec.
+;;
+;; Negative indices are treated as out-of-range / clamped-to-zero per the
+;; List convention — they never panic. Out-of-bounds reads return none.
+;;
+;; Implementation note: these helpers route through pvec-to-list / List's
+;; existing Int-indexed helpers, then back via pvec-from-list when needed.
+;; This bridges the Int↔Nat gap exactly the way the List versions handle
+;; it (pure recursion, no Int→Nat conversion primitive). The cost is
+;; O(n) for take-int/drop-int (matching the List counterparts) and O(n)
+;; for nth-int (also matching List nth-int). pvec-length-int is O(log32 n)
+;; — it composes pvec-length (O(log32 n)) with from-nat (O(1) on Nat
+;; literals).
+
+;; pvec-length-int : PVec A -> Int
+;; Number of elements as Int (for computational contexts). Mirrors List length-int.
+spec pvec-length-int {A : Type} [PVec A] -> Int
+defn pvec-length-int [v]
+  from-nat [pvec-length v]
+
+;; pvec-nth-int : PVec A -> Int -> Option A
+;; Element at Int index (0-based). Negative indices return none;
+;; out-of-bounds indices return none. Mirrors List nth-int.
+spec pvec-nth-int {A : Type} [PVec A] Int -> [Option A]
+defn pvec-nth-int [v i]
+  nth-int i [pvec-to-list v]
+
+;; pvec-take-int : Int -> PVec A -> PVec A
+;; Take first n elements. Non-positive n returns the empty pvec; n larger
+;; than the length returns the whole pvec. Mirrors List take-int.
+spec pvec-take-int {A : Type} Int [PVec A] -> [PVec A]
+defn pvec-take-int [n v]
+  pvec-from-list [take-int n [pvec-to-list v]]
+
+;; pvec-drop-int : Int -> PVec A -> PVec A
+;; Drop first n elements. Non-positive n returns the pvec unchanged; n
+;; larger than the length returns the empty pvec. Mirrors List drop-int.
+spec pvec-drop-int {A : Type} Int [PVec A] -> [PVec A]
+defn pvec-drop-int [n v]
+  pvec-from-list [drop-int n [pvec-to-list v]]

racket/prologos/namespace.rkt

@@ -511,9 +511,12 @@
     ;; Note: pvec-map, pvec-filter, pvec-fold, set-fold, set-filter,
     ;; map-fold-entries, map-filter-entries, map-map-vals are now native
     ;; parser keywords — no need to import from ops modules.
-    ;; pvec: pvec-any?, pvec-all?, pvec-from-list-fn, pvec-to-list-fn
+    ;; pvec: pvec-any?, pvec-all?, pvec-from-list-fn, pvec-to-list-fn,
+    ;;       pvec-nth-int, pvec-length-int, pvec-take-int, pvec-drop-int
     (imports [prologos::core::pvec :refer [pvec-any? pvec-all?
-                                           pvec-from-list-fn pvec-to-list-fn]])
+                                           pvec-from-list-fn pvec-to-list-fn
+                                           pvec-nth-int pvec-length-int
+                                           pvec-take-int pvec-drop-int]])
     ;; map: map-filter-vals, map-keys-list, map-vals-list, map-merge,
     ;;      map-to-entry-list, map-seq, map-from-seq
     (imports [prologos::core::map  :refer [map-filter-vals map-keys-list

racket/prologos/tests/test-pvec-int-helpers.rkt

@@ -0,0 +1,123 @@
+#lang racket/base
+
+;;;
+;;; Tests for PVec Int-indexed helpers (eigentrust pitfalls doc #12)
+;;;
+;;; Covers the pvec-nth-int / pvec-length-int / pvec-take-int /
+;;; pvec-drop-int quartet that mirrors the List Int-indexed helpers.
+;;; See racket/prologos/lib/prologos/core/pvec.prologos for the
+;;; implementation.
+;;;
+;;; All test cases use Int indices/lengths so an algorithm written
+;;; against a budget compared via int-le doesn't have to maintain a
+;;; parallel Nat counter just to index a PVec.
+;;;
+
+(require racket/string
+         rackunit
+         "test-support.rkt")
+
+(define (run s) (run-ns-last s))
+
+;; ========================================
+;; pvec-length-int : PVec A → Int
+;; ========================================
+
+(test-case "pvec-length-int: empty pvec returns 0"
+  (let ([result (run "(ns pvec-int-len-1)\n(eval (pvec-length-int (pvec-empty Nat)))")])
+    (check-true (string-contains? result "0 : Int"))))
+
+(test-case "pvec-length-int: singleton returns 1"
+  (let ([result (run "(ns pvec-int-len-2)\n(eval (pvec-length-int (pvec-push (pvec-empty Nat) zero)))")])
+    (check-true (string-contains? result "1 : Int"))))
+
+(test-case "pvec-length-int: two elements returns 2"
+  (let ([result (run "(ns pvec-int-len-3)\n(eval (pvec-length-int (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero))))")])
+    (check-true (string-contains? result "2 : Int"))))
+
+;; ========================================
+;; pvec-nth-int : PVec A → Int → Option A
+;; ========================================
+
+(test-case "pvec-nth-int: index 0 of singleton"
+  ;; vec [zero], index 0 → some 0N
+  (let ([result (run "(ns pvec-int-nth-1)\n(eval (pvec-nth-int (pvec-push (pvec-empty Nat) zero) 0))")])
+    (check-true (string-contains? result "0N"))))
+
+(test-case "pvec-nth-int: index 1 of two-element vec"
+  ;; vec [zero, suc zero], index 1 → some 1N
+  (let ([result (run "(ns pvec-int-nth-2)\n(eval (pvec-nth-int (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero)) 1))")])
+    (check-true (string-contains? result "1N"))))
+
+(test-case "pvec-nth-int: last index of three-element vec"
+  ;; vec [zero, suc zero, suc (suc zero)], index 2 → some 2N
+  (let ([result (run "(ns pvec-int-nth-3)\n(eval (pvec-nth-int (pvec-push (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero)) (suc (suc zero))) 2))")])
+    (check-true (string-contains? result "2N"))))
+
+(test-case "pvec-nth-int: negative index returns none (mirrors List nth-int)"
+  ;; vec [zero], index -1 → none
+  (let ([result (run "(ns pvec-int-nth-4)\n(eval (pvec-nth-int (pvec-push (pvec-empty Nat) zero) (int-neg 1)))")])
+    (check-true (string-contains? result "none"))))
+
+(test-case "pvec-nth-int: out-of-bounds index returns none"
+  ;; vec [zero], index 5 → none
+  (let ([result (run "(ns pvec-int-nth-5)\n(eval (pvec-nth-int (pvec-push (pvec-empty Nat) zero) 5))")])
+    (check-true (string-contains? result "none"))))
+
+(test-case "pvec-nth-int: empty pvec at index 0 returns none"
+  (let ([result (run "(ns pvec-int-nth-6)\n(eval (pvec-nth-int (pvec-empty Nat) 0))")])
+    (check-true (string-contains? result "none"))))
+
+;; ========================================
+;; pvec-take-int : Int → PVec A → PVec A
+;; ========================================
+
+(test-case "pvec-take-int: take 1 from two-element vec yields length 1"
+  ;; take 1 from [zero, suc zero] → length 1
+  (let ([result (run "(ns pvec-int-take-1)\n(eval (pvec-length-int (pvec-take-int 1 (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero)))))")])
+    (check-true (string-contains? result "1 : Int"))))
+
+(test-case "pvec-take-int: take 0 yields empty vec"
+  (let ([result (run "(ns pvec-int-take-2)\n(eval (pvec-length-int (pvec-take-int 0 (pvec-push (pvec-empty Nat) zero))))")])
+    (check-true (string-contains? result "0 : Int"))))
+
+(test-case "pvec-take-int: take negative yields empty vec (mirrors List take-int)"
+  (let ([result (run "(ns pvec-int-take-3)\n(eval (pvec-length-int (pvec-take-int (int-neg 5) (pvec-push (pvec-empty Nat) zero))))")])
+    (check-true (string-contains? result "0 : Int"))))
+
+(test-case "pvec-take-int: take more than length yields whole vec"
+  ;; take 100 from a 2-element vec → length 2
+  (let ([result (run "(ns pvec-int-take-4)\n(eval (pvec-length-int (pvec-take-int 100 (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero)))))")])
+    (check-true (string-contains? result "2 : Int"))))
+
+;; ========================================
+;; pvec-drop-int : Int → PVec A → PVec A
+;; ========================================
+
+(test-case "pvec-drop-int: drop 1 from two-element vec yields length 1"
+  ;; drop 1 from [zero, suc zero] → length 1
+  (let ([result (run "(ns pvec-int-drop-1)\n(eval (pvec-length-int (pvec-drop-int 1 (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero)))))")])
+    (check-true (string-contains? result "1 : Int"))))
+
+(test-case "pvec-drop-int: drop 0 returns vec unchanged"
+  (let ([result (run "(ns pvec-int-drop-2)\n(eval (pvec-length-int (pvec-drop-int 0 (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero)))))")])
+    (check-true (string-contains? result "2 : Int"))))
+
+(test-case "pvec-drop-int: drop negative returns vec unchanged (mirrors List drop-int)"
+  (let ([result (run "(ns pvec-int-drop-3)\n(eval (pvec-length-int (pvec-drop-int (int-neg 5) (pvec-push (pvec-empty Nat) zero))))")])
+    (check-true (string-contains? result "1 : Int"))))
+
+(test-case "pvec-drop-int: drop more than length yields empty vec"
+  (let ([result (run "(ns pvec-int-drop-4)\n(eval (pvec-length-int (pvec-drop-int 100 (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero)))))")])
+    (check-true (string-contains? result "0 : Int"))))
+
+;; ========================================
+;; Round-trip property: take + drop reconstruct length
+;; ========================================
+
+(test-case "pvec-take-int + pvec-drop-int: lengths sum to original"
+  ;; |take 1 v| + |drop 1 v| = |v| for a 3-element vec
+  (let ([take-len (run "(ns pvec-int-rt-1)\n(eval (pvec-length-int (pvec-take-int 1 (pvec-push (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero)) (suc (suc zero))))))")]
+        [drop-len (run "(ns pvec-int-rt-2)\n(eval (pvec-length-int (pvec-drop-int 1 (pvec-push (pvec-push (pvec-push (pvec-empty Nat) zero) (suc zero)) (suc (suc zero))))))")])
+    (check-true (string-contains? take-len "1 : Int"))
+    (check-true (string-contains? drop-len "2 : Int"))))