diff --git a/tests/list/.gitignore b/tests/list/.gitignore new file mode 100644 index 0000000..dd4ff93 --- /dev/null +++ b/tests/list/.gitignore @@ -0,0 +1,2 @@ +/list_test.ml +/list_test_unnesting.ml diff --git a/tests/list/dune b/tests/list/dune index 428c272..8658c89 100644 --- a/tests/list/dune +++ b/tests/list/dune @@ -10,12 +10,29 @@ (:peano %{project_root}/std/.Peano.objs/byte/peano.cmi) (:exec %{project_root}/src/noCanren.exe) (:input list_test.ml2mk.ml)) + (mode + (promote (until-clean))) (action (run sh -c "%{exec} -w -8 %{input} -rectypes -o %{targets} | ocamlformat --enable-outside-detected-project --impl -"))) +(rule + (targets list_test_unnesting.ml) + (deps + (:list %{project_root}/std/.List.objs/byte/list.cmi) + (:peano %{project_root}/std/.Peano.objs/byte/peano.cmi) + (:exec %{project_root}/src/noCanren.exe) + (:input unnesting.ml2mk.ml)) + (mode + (promote (until-clean))) + (action + (run + sh + -c + "%{exec} -unnesting-mode -without-activate-tactics -w -8 %{input} -rectypes -o %{targets} "))) + (executable (name list_test_run) (libraries GT OCanren OCanren.tester Peano List) @@ -27,5 +44,18 @@ OCanren-ppx.ppx_distrib GT.ppx_all))) +(executable + (name list_test_run2) + (libraries GT OCanren OCanren.tester Peano List) + (modules list_test_run2 list_test_unnesting) + (flags + (:standard -open OCanren.Std)) + (preprocess + (pps + OCanren-ppx.ppx_repr + OCanren-ppx.ppx_fresh + OCanren-ppx.ppx_distrib + GT.ppx_all))) + (cram - (deps ./list_test_run.exe)) + (deps ./list_test_run.exe ./list_test_run2.exe)) diff --git a/tests/list/list_test.t b/tests/list/list_test.t index 4a6a2d2..f7712c3 100644 --- a/tests/list/list_test.t +++ b/tests/list/list_test.t @@ -1,3 +1,4 @@ + $ ./list_test_run2.exe $ ./list_test_run.exe lenght, all answers { q=5; diff --git a/tests/list/list_test_run2.ml b/tests/list/list_test_run2.ml new file mode 100644 index 0000000..8fe7958 --- /dev/null +++ b/tests/list/list_test_run2.ml @@ -0,0 +1,15 @@ +open OCanren +open OCanren.Std +open Tester +open List_test_unnesting + +let () = + let injected : int ilogic Std.List.injected = OCanren.Std.list ( !! ) [ 1 ] in + let _ = + OCanren.(run q) + (list_map (fun x q17 -> x === q17) injected) + (fun rr -> rr#reify (Std.List.reify OCanren.reify)) + |> OCanren.Stream.hd + in + () +;; diff --git a/tests/list/unnesting.ml2mk.ml b/tests/list/unnesting.ml2mk.ml new file mode 100644 index 0000000..8cd1134 --- /dev/null +++ b/tests/list/unnesting.ml2mk.ml @@ -0,0 +1,11 @@ +open List +open Peano + +let list_map f xs = + let rec helper xs = + match xs with + | [] -> [] + | x :: xs -> f x :: helper xs + in + helper xs +;;