Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions ppx/tester/ppx_tester.ml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(*
* OCanren. PPX syntax extensions.
* Copyright (C) 2016-2024
* Copyright (C) 2016-2026
* Dmitrii Kosarev aka Kakadu
* St.Petersburg State University, JetBrains Research
*)
Expand All @@ -11,13 +11,13 @@

Expands

{[ let __ _ = [%tester runR OCanren.reify show_int show_intl (fun q -> q === !!1)] ]}
{[ let __ _ = [%tester run_r OCanren.reify show_intl 1 (fun q -> q === !!1)] ]}

to

{[
let __ _ =
runR OCanren.reify show_int show_intl q qh
run_r OCanren.reify show_intl 1 q qh
("<string repr of goal>", (fun q -> q === (!! 1)))
]}

Expand Down
90 changes: 90 additions & 0 deletions samples/bench_reverso.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@
(* SPDX-License-Identifier: LGPL-2.1-or-later *)
(*
* OCanren. PPX syntax extensions.
* Copyright (C) 2016-2026
* Dmitrii Kosarev aka Kakadu
* St.Petersburg State University, JetBrains Research
*)

(* In this demo we benhmark default reverso in a lucky direction
against debug_var reverso, which works in any direction.
For longer lists, performance difference could be neglected
*)

open OCanren

let rec appendo xs ys zs =
let open OCanren.Std in
conde
[
xs === Std.nil () &&& (ys === zs);
fresh (h tl tmp) (xs === h % tl) (zs === h % tmp) (appendo tl ys tmp);
]

let rec reverso xs rez =
let open OCanren.Std in
conde
[
xs === nil () &&& (xs === rez);
(* Good order for forward execution *)
fresh (h tl tmp) (xs === h % tl) (reverso tl tmp) (appendo tmp !<h rez);
]

let rec reverso_hacky xs rez =
let open OCanren.Std in
conde
[
xs === nil () &&& (xs === rez);
debug_var xs [%reify: GT.int OCanren.Std.List.ground] (function
| [ Var _ ] ->
fresh (h tl tmp)
(xs === h % tl)
(appendo tmp !<h rez) (reverso_hacky tl tmp)
| _ ->
fresh (h tl tmp)
(xs === h % tl)
(reverso_hacky tl tmp) (appendo tmp !<h rez));
]

let () =
let open OCanren.Std in
let open Tester in
[%tester
run_r [%reify: GT.int OCanren.Std.List.ground]
([%show: GT.int OCanren.logic OCanren.Std.List.logic] ())
(-1)
(fun q -> reverso (OCanren.Std.list OCanren.inj [ 1; 2; 3 ]) q)]

let () =
let open OCanren.Std in
let open Tester in
[%tester
run_r [%reify: GT.int OCanren.Std.List.ground]
([%show: GT.int OCanren.logic OCanren.Std.List.logic] ())
(-1)
(fun q -> reverso_hacky q (OCanren.Std.list OCanren.inj [ 1; 2; 3 ]))]

let make_list n : _ ilogic =
assert (n > 0);
let rec helper acc n =
if n <= 0 then acc else helper (Std.List.cons !!1 acc) (n - 1)
in
helper (Std.nil ()) n

let () =
let xs700 = make_list 500 in
let test rel () =
let s =
run q
(fun v -> rel xs700 v)
(fun rr -> rr#reify [%reify: GT.int OCanren.Std.List.ground])
in
let answers = OCanren.Stream.take s in
assert (List.length answers = 1)
in
let open Benchmark in
let res =
throughputN ~style:Nil ~repeat:2 2
[ ("default", test reverso, ()); ("debug_var", test reverso_hacky, ()) ]
in
tabulate res
26 changes: 24 additions & 2 deletions samples/dune
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,23 @@
(file %{project_root}/camlp5/pp5+ocanren+dump.exe)
(file %{project_root}/camlp5/pp5+gt+plugins+ocanren+logger+dump.exe)
(file %{project_root}/camlp5/pp5+ocanren+o.exe))
(libraries GT OCanren benchmark))
(libraries GT OCanren))

(executable
(name bench_reverso)
(modules bench_reverso)
(preprocess
(pps
OCanren-ppx.ppx_tester
OCanren-ppx.ppx_fresh
OCanren-ppx.ppx_deriving_reify
GT.ppx_all))
(preprocessor_deps
(file %{project_root}/ppx/pp_distrib_gt_reify.exe)
(file %{project_root}/camlp5/pp5+ocanren+dump.exe)
(file %{project_root}/camlp5/pp5+gt+plugins+ocanren+logger+dump.exe)
(file %{project_root}/camlp5/pp5+ocanren+o.exe))
(libraries GT OCanren OCanren.tester benchmark))

(executable
(name JeepProblem)
Expand All @@ -70,7 +86,13 @@

(alias
(name all)
(deps tree.exe sorting.exe WGC.exe JeepProblem.exe len.exe))
(deps
tree.exe
sorting.exe
WGC.exe
JeepProblem.exe
len.exe
bench_reverso.exe))

(cram
(deps
Expand Down