File: clist.ml

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (60 lines) | stat: -rw-r--r-- 1,612 bytes parent folder | download | duplicates (3)
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
open Utest

let log_out_ch = open_log_out_ch __FILE__

let reference_filter =
  let rec filter f = function
    | [] -> []
    | x :: tl as l ->
      if f x then
        let tl' = filter f tl in
        if tl == tl' then l else x :: tl'
      else filter f tl
  in
  filter

let () =
  let () = Random.self_init () in
  let seed = Random.bits() in
  Printf.fprintf log_out_ch "seed = %d\n" seed;
  Random.init seed

let lists =
  List.init 100 (fun _ ->
      let len = Random.int 100 in
      List.init len (fun _ ->
          let b = Random.bool() in
          let v = Random.bits() in
          b,v))

let t1 = mk_bool_test "clib-clist0"
    "filter produces correct values"
    (List.for_all (fun l ->
         let expected : (bool * int) list = reference_filter fst l in
         let generated = CList.filter fst l in
         expected = generated)
        lists)

let lists' =
  List.init 100 (fun _ ->
      let len = Random.int 100 in
      let keepafter = if len = 0 then 0 else Random.int len in
      let l = List.init len (fun i ->
          let b = i >= keepafter || Random.bool () in
          let v = Random.bits() in
          b, v) in
      keepafter, l)

let t2 = mk_bool_test "clib-clist1"
    "filter correctly preserves physical equality of tails"
    (List.for_all (fun (keepafter,l) ->
         flush log_out_ch;
         let generated = CList.filter fst l in
         let tl = CList.skipn keepafter l in
         let generated_tl = CList.lastn (List.length tl) generated in
         tl == generated_tl)
       lists')

let tests = [ t1; t2 ]

let _ = run_tests __FILE__ log_out_ch tests