pbt/qcheck/map.ml at main · informatica-unica/pbt · GitHub

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
(**
  Lists are Functors:

  https://wiki.haskell.org/index.php?title=Functor
  https://lean-lang.org/lean4/doc/monads/laws.lean.html#what-are-the-functor-laws
*)

open QCheck

(* ################################################
   Definitions
   ################################################ *)

let rec map (f : 'a -> 'b) (l : 'a list) : 'b list =
  match l with
  | [] -> []
  | x :: xs -> f x :: map f xs

(* ################################################
   Start of tests
   ################################################ *)

(**
  Mapping the identity function over a list preserves the list: [map id l = l]
*)
let test_identity_law map =
  Test.make ~name:"test_identity_law"
  (list small_int) (fun l ->

    map (fun x -> x) l = l

  )

(**
  [map] preserves the composition of functions:
  [map (h . g) x = map h (map g x)]
*)
let test_composition_law map =
  Test.make ~name:"test_composition_law"
  (tup3 (fun1 Observable.int small_int) (fun1 Observable.int small_int) (list small_int)
  )
  (fun (h,g,l) ->
    let h,g = Fn.apply h, Fn.apply g in

    map (Fun.compose h g) l = map h (map g l)

  )

;;

(* ################################################
   Test runner
   ################################################ *)

QCheck_runner.run_tests ~verbose:true
  [
    test_identity_law map;
    test_composition_law map;
  ]