Skip to content

Commit

Permalink
fix: counterexample function
Browse files Browse the repository at this point in the history
  • Loading branch information
CAIMEOX committed Jan 3, 2025
1 parent ded134c commit 16079a8
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 3 deletions.
3 changes: 1 addition & 2 deletions src/lib/feat/enumerate.mbt
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,7 @@ pub fn singleton[T](val : T) -> Enumerate[T] {

///|
pub fn en_index[T](self : Enumerate[T], idx : BigInt) -> T {
let fin = self.parts
loop fin, idx {
loop self.parts, idx {
Nil, _ => abort("index out of bounds")
Cons(f, rest), i =>
if i < f.fCard {
Expand Down
17 changes: 17 additions & 0 deletions src/lib/gen_wbtest.mbt
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,16 @@ test "feat nat" {
)
}

test "feat nat index" {
let x = [0N, 1, 2, 3, 4, 5, 6].map(fn(x) {
(@feat.Enumerable::enumerate() : @feat.Enumerate[Nat]).en_index(x)
})
inspect!(
x,
content="[Zero, Succ(Zero), Succ(Succ(Zero)), Succ(Succ(Succ(Zero))), Succ(Succ(Succ(Succ(Zero)))), Succ(Succ(Succ(Succ(Succ(Zero))))), Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))]",
)
}

///|
enum SingleTree {
Leaf(Bool)
Expand Down Expand Up @@ -76,6 +86,13 @@ test "feat tree" {
)
}

test "index large" {
let eTree : @feat.Enumerate[SingleTree] = @feat.Enumerable::enumerate()
for i = 100000N; i > 0; i = i - 1 {
eTree.en_index(i) |> ignore
}
}

test "nat" {
inspect!(
nat().samples(size=50),
Expand Down
2 changes: 1 addition & 1 deletion src/lib/testable.mbt
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ pub fn forall_shrink[T : Testable, A : Show](
gen.bind(fn(x) {
shrinking(shrinker, x, fn(a : A) {
let s = a.to_string()
counterexample(f(x), s)
counterexample(f(a), s)
})._
})
}
Expand Down

0 comments on commit 16079a8

Please sign in to comment.