fix: use correct bounds for oneOf and elements (#56)

The index of an array shouldn't go beyond its size-1.

This patch also removes the use of `Array.get!` from `Gen.lean` and uses `Array`
instead of `List` in `elements` because it does size computation and index-based
access in O(1) at runtime.

Further, it sets the `hi` value of the `DefaultRange` instance for `Nat` so that
it's within the `USize` range, for guaranteed memory optimization at runtime.

Author: arthurpaulino

LSpec/SlimCheck/Control/DefaultRange.lean

@@ -48,14 +48,14 @@ instance : Bounded Bool where
 
 instance : DefaultRange Nat where
   lo := 0
-  hi := USize.size
+  hi := USize.size - 1
 
 instance {n : Nat} : Bounded (Fin n.succ) where
   lo := ⟨0, n.succ_pos⟩
   hi := ⟨n, n.lt_succ_self⟩
 
 instance : DefaultRange Int where
-  lo :=  - Int.ofNat (USize.size / 2)
+  lo := - Int.ofNat (USize.size / 2)
   hi := Int.ofNat (USize.size / 2 - 1)
 
 end SlimCheck

LSpec/SlimCheck/Gen.lean

@@ -37,10 +37,6 @@ def chooseAny (α : Type u) [Random α] [DefaultRange α] : Gen α :=
 def choose (α : Type u) [Random α] (lo hi : α) : Gen α :=
   λ _ => randBound α lo hi
 
-/-- Generate a `Nat` example between `x` and `y` (exclusively). -/
-def chooseNatLt (lo hi : Nat) : Gen Nat :=
-  choose Nat (lo.succ) hi
-
 /-- Get access to the size parameter of the `Gen` monad. -/
 def getSize : Gen Nat :=
   return (← read).down
@@ -63,17 +59,22 @@ by the size parameter of `Gen`. -/
 def listOf (x : Gen α) : Gen (List α) :=
   arrayOf x >>= pure ∘ Array.toList
 
-/-- Given a list of example generators, choose one to create an example. -/
+/-- Given an array of example generators, choose one to create an example. -/
 def oneOf [Inhabited α] (xs : Array (Gen α)) : Gen α := do
-  let x ← chooseNatLt 0 xs.size
-  xs.get! x
-
-/-- Given a list of examples, choose one to create an example. -/
-def elements [Inhabited α] (xs : List α) : Gen α := do
-  let x ← chooseNatLt 0 xs.length
-  pure $ xs.get! x
+  let i ← choose Nat 0 (xs.size - 1)
+  if h : i < xs.size then
+    xs.get i h
+  else -- The array is empty
+    pure default
+
+/-- Given an array of examples, choose one. -/
+def elements [Inhabited α] (xs : Array α) : Gen α := do
+  let i ← choose Nat 0 (xs.size - 1)
+  if h : i < xs.size then
+    return xs.get i h
+  else -- The array is empty
+    pure default
 
-open List in
 /-- Generate a random permutation of a given list. -/
 def permutationOf : (xs : List α) → Gen (List α)
 | [] => pure []

LSpec/SlimCheck/Sampleable.lean

@@ -173,7 +173,7 @@ instance Bool.sampleableExt : SampleableExt Bool :=
 /-- This can be specialized into customized `SampleableExt Char` instances.
 The resulting instance has `1 / length` chances of making an unrestricted choice of characters
 and it otherwise chooses a character from `chars` with uniform probabilities.  -/
-def Char.sampleable (length : Nat) (chars : List Char) : SampleableExt Char :=
+def Char.sampleable (length : Nat) (chars : Array Char) : SampleableExt Char :=
     mkSelfContained do
       let x ←  choose Nat 0 length
       if x == 0 then
@@ -183,7 +183,8 @@ def Char.sampleable (length : Nat) (chars : List Char) : SampleableExt Char :=
         elements chars
 
 instance Char.sampleableDefault : SampleableExt Char :=
-  Char.sampleable 3 " 0123abcABC:,;`\\/".toList
+  Char.sampleable 3
+    #[' ', '0', '1', '2', '3', 'a', 'b', 'c', 'A', 'B', 'C', ':', ',', ';', '`', '\\', '/']
 
 instance Prod.sampleableExt {α β : Type u} [SampleableExt α] [SampleableExt β] :
     SampleableExt (α × β) where