From 16079a8a21d5d6a9277203fec8ed4b6ed4575f16 Mon Sep 17 00:00:00 2001 From: CAIMEOX <38813005+CAIMEOX@users.noreply.github.com> Date: Fri, 3 Jan 2025 13:36:31 +0800 Subject: [PATCH] fix: counterexample function --- src/lib/feat/enumerate.mbt | 3 +-- src/lib/gen_wbtest.mbt | 17 +++++++++++++++++ src/lib/testable.mbt | 2 +- 3 files changed, 19 insertions(+), 3 deletions(-) diff --git a/src/lib/feat/enumerate.mbt b/src/lib/feat/enumerate.mbt index 87b9dce..6e01d20 100644 --- a/src/lib/feat/enumerate.mbt +++ b/src/lib/feat/enumerate.mbt @@ -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 { diff --git a/src/lib/gen_wbtest.mbt b/src/lib/gen_wbtest.mbt index 21d0fe4..7604a3e 100644 --- a/src/lib/gen_wbtest.mbt +++ b/src/lib/gen_wbtest.mbt @@ -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) @@ -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), diff --git a/src/lib/testable.mbt b/src/lib/testable.mbt index 9737f8e..c62246b 100644 --- a/src/lib/testable.mbt +++ b/src/lib/testable.mbt @@ -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) })._ }) }