1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
import "dotenv/config";
import Prando from 'prando';
import { Gen, property } from "./property";
let genint: Gen<number> = (rng: Prando) =>
(size: number) =>
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);
return (size: number) => {
let result = [];
for (let i = 0; i < size; i++) {
result.push(g(size));
}
return result;
};
};
}
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 = [];
let tail = arr.slice(1);
let keep1 = arr.slice();
keep1.splice(1, 1);
result.push(tail,keep1);
if (arr.length >3) {
let half = Math.floor(arr.length / 2);
let copy = arr.slice();
let secondHalf = copy.slice(half);
result.push(secondHalf);
}
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() {
let rng = new Prando(Math.random() * 1000);
let reverse_append_result = prop_reverse_with_two_lists(rng, 10);
let reverse_reverse_result = prop_reverse_is_self_inverse(rng, 10);
console.log('result: ' + JSON.stringify(reverse_append_result));
console.log('result: ' + JSON.stringify(reverse_reverse_result));
}
main();
|
