From 064e80689c7d7126a504400d8c4e962b6b334bac Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud.bailly@iohk.io>
Date: Sat, 25 Jan 2025 22:36:19 +0100
Subject: Added some 'interesting' properties about lists

These are the classical properties from Claessen and Hughes' paper.
Shrinking is too expensive as it is so need to prune recursion tree.
---
 pbt/ts/src/index.ts    | 70 +++++++++++++++++++++++++++++++++++++++++++++-----
 pbt/ts/src/property.ts | 40 +++++++++++++++++++----------
 2 files changed, 91 insertions(+), 19 deletions(-)

diff --git a/pbt/ts/src/index.ts b/pbt/ts/src/index.ts
index 46454f0..474b656 100644
--- a/pbt/ts/src/index.ts
+++ b/pbt/ts/src/index.ts
@@ -1,12 +1,19 @@
 import "dotenv/config";
 import Prando from 'prando';
-import { Gen } from "./property";
+import { Gen, property } from "./property";
 
 let genint: Gen<number> = (rng: Prando) =>
   (size: number) =>
-  rng.nextInt(-size, size);
+    rng.nextInt(-size, size);
 
 
+function arrayEquals<A>(a: A[], b: A[]): boolean {
+  return Array.isArray(a) &&
+    Array.isArray(b) &&
+    a.length === b.length &&
+    a.every((val, index) => val === b[index]);
+}
+
 function genlist<A>(gen: Gen<A>): Gen<A[]> {
   return (rng: Prando) => {
     let g = gen(rng);
@@ -20,13 +27,64 @@ function genlist<A>(gen: Gen<A>): Gen<A[]> {
   };
 }
 
-function generate<A>(gen: Gen<A>): A {
-  let rng = new Prando(Math.random() * 1000);
-  return gen(rng)(100);
+function reverse<A>(arr: A[]): A[] {
+  let result = [];
+  for (let i = arr.length - 1; i >= 0; i--) {
+    result.push(arr[i]);
+  }
+  return result;
+}
+
+function reverse_is_self_inverse(arr: number[]): boolean {
+  return arrayEquals(reverse(reverse(arr)), arr);
+}
+
+function shrinklist<A>(arr: A[]): A[][] {
+  let result = [];
+  for (let i = 0; i < arr.length; i++) {
+    let copy = arr.slice();
+    copy.splice(i, 1);
+    result.push(copy);
+  }
+  return result;
+}
+
+function gen2lists<A>(gen: Gen<A>): Gen<[A[], A[]]> {
+  return (rng: Prando) => {
+    let gl = genlist(gen)(rng);
+    return (size: number) => {
+      return [gl(size), gl(size)]
+    };
+  };
+}
+
+function reverse_with_two_lists<A>(arrs: [A[], A[]]): boolean {
+  return arrayEquals(reverse(arrs[0].concat(arrs[1])),
+    reverse(arrs[0]).concat(reverse(arrs[1])));
 }
 
+function shrink2lists<A>([l1, l2]: [A[], A[]]): [A[], A[]][] {
+  let result: [A[], A[]][] = [];
+  let s1 = shrinklist(l1);
+  let s2 = shrinklist(l2);
+  for (let i = 0; i < s1.length; i++) {
+    let j = s2.length - i -1;
+    let news2 = j >= 0 ? s2[j] : [];
+    result.push([s1[i], news2]);
+  }
+  return result;
+}
+
+let prop_reverse_with_two_lists =
+  property<[number[], number[]]>(reverse_with_two_lists, gen2lists(genint), shrink2lists);
+
+let prop_reverse_is_self_inverse =
+  property(reverse_is_self_inverse, genlist(genint), shrinklist);
+
 async function main() {
-  console.log('list: ' + generate(genlist(genint)));
+  let rng = new Prando(Math.random() * 1000);
+  let result = prop_reverse_with_two_lists(rng, 10);
+  console.log('result: ' + JSON.stringify(result));
 }
 
 main();
diff --git a/pbt/ts/src/property.ts b/pbt/ts/src/property.ts
index e8d3a21..40e32c5 100644
--- a/pbt/ts/src/property.ts
+++ b/pbt/ts/src/property.ts
@@ -13,7 +13,10 @@ type Predicate<A> = (a: A) => boolean;
 
 export type Gen<A> = (rng: Prando) => ((size: number) => A);
 
-type Shrinker<A> = (a: A) => [A];
+type Shrinker<A> = (a: A) => A[];
+
+type Property<A> = (rng: Prando,
+                    size: number) =>  TestResult<A>;
 
 const MAX_SUCCESS = 100;
 
@@ -26,6 +29,7 @@ function findMinimalCounterExample<A>(x: A,
   let shrinks = depth;
   for (let y of xs) {
     if (!predicate(y)) {
+      console.log("Shrinking with " + y);
       let shrink = findMinimalCounterExample(y, predicate, shrinker, depth + 1);
       if (shrink.shrinks > depth) {
         counterexample = shrink.counterexample;
@@ -36,18 +40,28 @@ function findMinimalCounterExample<A>(x: A,
   return { counterexample, shrinks };
 }
 
-export function property<A>(rng: Prando,
-  size: number,
+
+export function generate<A>(gen: Gen<A>): A {
+  let rng = new Prando(Math.random() * 1000);
+  return gen(rng)(100);
+}
+
+export function property<A>(
   predicate: Predicate<A>,
   generator: Gen<A>,
-  shrinker: Shrinker<A>): TestResult<A> {
-  let gen = generator(rng);
-  for (let i = 0; i < MAX_SUCCESS; i++) {
-    let x = gen(size);
-    if (!predicate(x)) {
-      let counterexample = findMinimalCounterExample(x, predicate, shrinker);
-      return { result: 'Falsified', counterexample };
-    }
-  }
-  return { result: 'OK', counterexample: null };
+  shrinker: Shrinker<A>): Property<A> {
+  return (rng: Prando,
+          size: number) => {
+            let gen = generator(rng);
+            let i = 0;
+            for (; i < MAX_SUCCESS; i++) {
+              let x = gen(size);
+              if (!predicate(x)) {
+                let counterexample = findMinimalCounterExample(x, predicate, shrinker);
+                return { result: 'Falsified', tests: i, counterexample };
+              }
+              size++;
+            }
+            return { result: 'OK', tests: i, counterexample: null };
+          };
 }
-- 
cgit v1.2.3