-
Notifications
You must be signed in to change notification settings - Fork 0
/
bench.ml
135 lines (120 loc) · 3.44 KB
/
bench.ml
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
open OCanren
open OCanren.Std
(* Appendo decreases on 1st and 3rd arguemnt *)
let rec appendo a b ab =
conde
[
a === nil () &&& (b === ab);
fresh (h t ab') (a === h % t) (h % ab' === ab) (appendo t b ab');
]
let rec reverso_b xs ys =
conde
[
xs === Std.nil () &&& (xs === ys);
fresh (temp h tl)
(xs === List.cons h tl)
(appendo temp (List.cons h (List.nil ())) ys)
(reverso_b tl temp);
]
let rec reverso_f xs ys =
conde
[
xs === Std.nil () &&& (xs === ys);
fresh (h tl temp)
(xs === List.cons h tl)
(reverso_f tl temp)
(appendo temp (List.cons h (List.nil ())) ys);
]
let rec reverso_u xs ys =
conde
[
xs === Std.nil () &&& (xs === ys);
debug_var ys OCanren.reify (function
| [ Var _ ] ->
fresh (temp h tl)
(xs === List.cons h tl)
(reverso_u tl temp)
(appendo temp (List.cons h (List.nil ())) ys)
| [ Value _ ] ->
fresh (temp h tl)
(xs === List.cons h tl)
(appendo temp (List.cons h (List.nil ())) ys)
(reverso_u tl temp)
| _ -> failwith "should not happen");
]
(* appendo before reverso --- backward execution of reverso OK
reverso before appendo --- forward execution of reverso OK
*)
open Tester
let run_exn eta =
run_r
(Std.List.prj_exn OCanren.prj_exn)
(GT.show Std.List.ground (GT.show GT.int))
eta
let _ =
run_exn (-1) qr qrh
(REPR (fun q r -> appendo q r (list ( !! ) [ 1; 2; 3; 4 ])))
let _ =
run_exn (-1) q qh (REPR (fun q -> reverso_b q (list ( !! ) [ 1; 2; 3; 4 ])))
let _ =
run_exn (-1) q qh (REPR (fun q -> reverso_f (list ( !! ) [ 1; 2; 3; 4 ]) q))
let _ =
run_exn (-1) q qh (REPR (fun q -> reverso_u (list ( !! ) [ 1; 2; 3; 4 ]) q));
run_exn (-1) q qh (REPR (fun q -> reverso_u q (list ( !! ) [ 1; 2; 3; 4 ])))
open Benchmark
let all_answers ss = ss |> OCanren.Stream.take |> ignore
let __ () =
let list_of_5 = list ( !! ) [ 1; 2; 3; 4 ] in
let prepare rel lst () =
all_answers
(OCanren.run q (fun q -> rel q lst) (fun rr -> rr#reify OCanren.prj_exn))
in
let samples =
throughputN 5
[
("reverso_b", prepare reverso_b list_of_5, ());
("reverso_f", prepare (Fun.flip reverso_f) list_of_5, ());
]
in
tabulate samples
let () =
let list_of_4 = list ( !! ) [ 1; 2; 3; 4 ] in
let list_of_10 = list ( !! ) (Stdlib.List.init 10 Fun.id) in
let prepare rel lst () =
all_answers
(OCanren.run q (fun q -> rel q lst) (fun rr -> rr#reify OCanren.prj_exn))
in
let delay_in_s = 2 in
let () =
tabulate
@@ throughputN delay_in_s
[
("reverso_b", prepare reverso_b list_of_4, ());
("reverso_u", prepare reverso_u list_of_4, ());
]
in
let () =
tabulate
@@ throughputN delay_in_s
[
("reverso_b", prepare reverso_b list_of_10, ());
("reverso_u", prepare reverso_u list_of_10, ());
]
in
let () =
tabulate
@@ throughputN delay_in_s
[
("reverso_b", prepare (Fun.flip reverso_f) list_of_4, ());
("reverso_u", prepare (Fun.flip reverso_u) list_of_4, ());
]
in
let () =
tabulate
@@ throughputN delay_in_s
[
("reverso_b", prepare (Fun.flip reverso_f) list_of_10, ());
("reverso_u", prepare (Fun.flip reverso_u) list_of_10, ());
]
in
()