Promote tests for issue #173

Signed-off-by: Dmitrii.Kosarev a.k.a. Kakadu <[email protected]>
PLTools · Jan 12, 2025 · aafc2e3 · aafc2e3
1 parent dc4ab0e
commit aafc2e3
Show file tree

Hide file tree

Showing 7 changed files with 89 additions and 21 deletions.
diff --git a/regression/test002.t b/regression/test002.t
@@ -1,7 +1,7 @@
   $ ./test002sort.exe
-  [O; O; _.140]
-  [O; O; _.140 [=/= O]]
-  [O; O; _.157 [=/= O]]
+  [O; O; _.138]
+  [O; O; _.136 [=/= O]]
+  [O; O; _.153 [=/= O]]
   [O; S (O); S (_.497)]
   [O; S (O); S (_.516 [=/= O])]
   [O; S (O); S (_.110)]

diff --git a/regression/test005.t b/regression/test005.t
@@ -19,14 +19,14 @@
   q=[("x", V ("y")) | _.13];
   }
   fun q -> infero (abs varX (v varX)) q, 1 answer {
-  q=Arr (_.21, _.21);
+  q=Arr (_.18, _.18);
   }
   fun q -> infero (abs varF (abs varX (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (Arr (_.54, _.26), Arr (_.54, _.26));
+  q=Arr (Arr (_.30, _.26), Arr (_.30, _.26));
   }
   fun q -> infero (abs varX (abs varF (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (_.64, Arr (Arr (_.64, _.26), _.26));
+  q=Arr (_.30, Arr (Arr (_.30, _.26), _.26));
   }
   fun q -> infero q (arr (p varX) (p varX)), 1 answer {
-  q=Abs (_.30, V (_.30));
+  q=Abs (_.29, V (_.29));
   }
diff --git a/regression/test006.t b/regression/test006.t
@@ -24,10 +24,10 @@
   q=V ("x");
   }
   fun q -> evalo (app q (v varX)) (v varX), 1 answer {
-  q=Abs (_.59, V (_.59));
+  q=Abs (_.44, V (_.44));
   }
   fun q r -> evalo (app r q) (v varX), 1 answer {
-  q=V ("x"); r=Abs (_.68, V (_.68));
+  q=V ("x"); r=Abs (_.54, V (_.54));
   }
   fun q r s -> a_la_quine q r s, 2 answers {
   q=Abs (_.668, V (_.668)); r=Abs (_.668, V (_.668)); s=Abs (_.668, V (_.668));

diff --git a/regression/test011.t b/regression/test011.t
@@ -174,7 +174,7 @@
   fun q ->
     OCanren.Fresh.two
       (fun x y -> delay (fun () -> conj (!![x; y] === q) (y =/= x))), all answers {
-  q=[_.11 [=/= _.12]; _.12];
+  q=[_.11; _.12 [=/= _.11]];
   }
   fun q ->
     OCanren.Fresh.two
@@ -247,7 +247,7 @@
   fun x ->
     OCanren.Fresh.two
       (fun y z -> delay (fun () -> conj (x =/= !![y; !2]) (x === !![z; !2]))), all answers {
-  q=[_.12; 2];
+  q=[_.12 [=/= _.11]; 2];
   }
   fun q -> distincto (!2 % (!3 %< q)), all answers {
   q=_.35 [=/= 2; =/= 3];

diff --git a/regression/test014.t b/regression/test014.t
@@ -28,18 +28,18 @@
   q=[_.13 | _.14]; r=[]; s=[];
   q=[1]; r=[_.15 | _.16]; s=[_.15 | _.16];
   q=[_.17; _.18 | _.19]; r=[1]; s=[_.17; _.18 | _.19];
-  q=[0; 1]; r=[_.43; _.33 | _.34]; s=[0; _.43; _.33 | _.34];
-  q=[0; 0; 1]; r=[_.97; _.76 | _.77]; s=[0; 0; _.97; _.76 | _.77];
+  q=[0; 1]; r=[_.28; _.33 | _.34]; s=[0; _.28; _.33 | _.34];
+  q=[0; 0; 1]; r=[_.69; _.76 | _.77]; s=[0; 0; _.69; _.76 | _.77];
   q=[1; _.102 | _.103]; r=[0; 1]; s=[0; 1; _.102 | _.103];
-  q=[0; 0; 0; 1]; r=[_.207; _.164 | _.165]; s=[0; 0; 0; _.207; _.164 | _.165];
+  q=[0; 0; 0; 1]; r=[_.149; _.164 | _.165]; s=[0; 0; 0; _.149; _.164 | _.165];
   q=[1; _.192 | _.193]; r=[0; 0; 1]; s=[0; 0; 1; _.192 | _.193];
   q=[0; 1; _.218 | _.219]; r=[0; 1]; s=[0; 0; 1; _.218 | _.219];
-  q=[0; 0; 0; 0; 1]; r=[_.437; _.343 | _.344]; s=[0; 0; 0; 0; _.437; _.343 | _.344];
+  q=[0; 0; 0; 0; 1]; r=[_.314; _.343 | _.344]; s=[0; 0; 0; 0; _.314; _.343 | _.344];
   q=[1; _.375 | _.376]; r=[0; 0; 0; 1]; s=[0; 0; 0; 1; _.375 | _.376];
   q=[0; 1; _.401 | _.402]; r=[0; 0; 1]; s=[0; 0; 0; 1; _.401 | _.402];
   q=[0; 0; 1; _.459 | _.460]; r=[0; 1]; s=[0; 0; 0; 1; _.459 | _.460];
   q=[1; 1]; r=[1; 1]; s=[1; 0; 0; 1];
-  q=[0; 0; 0; 0; 0; 1]; r=[_.904; _.713 | _.714]; s=[0; 0; 0; 0; 0; _.904; _.713 | _.714];
+  q=[0; 0; 0; 0; 0; 1]; r=[_.656; _.713 | _.714]; s=[0; 0; 0; 0; 0; _.656; _.713 | _.714];
   q=[1; _.745 | _.746]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.745 | _.746];
   q=[0; 1; _.778 | _.779]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.778 | _.779];
   q=[0; 0; 1; _.834 | _.835]; r=[0; 0; 1]; s=[0; 0; 0; 0; 1; _.834 | _.835];
@@ -48,7 +48,7 @@
   q=[0; 1; 1]; r=[1; 1]; s=[0; 1; 0; 0; 1];
   q=[1; 1]; r=[1; 1; 1]; s=[1; 0; 1; 0; 1];
   q=[1; 1]; r=[0; 1; 1]; s=[0; 1; 0; 0; 1];
-  q=[0; 0; 0; 0; 0; 0; 1]; r=[_.1860; _.1493 | _.1494]; s=[0; 0; 0; 0; 0; 0; _.1860; _.1493 | _.1494];
+  q=[0; 0; 0; 0; 0; 0; 1]; r=[_.1360; _.1493 | _.1494]; s=[0; 0; 0; 0; 0; 0; _.1360; _.1493 | _.1494];
   q=[1; _.1523 | _.1524]; r=[0; 0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1523 | _.1524];
   q=[0; 1; _.1553 | _.1554]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1553 | _.1554];
   q=[0; 0; 1; _.1607 | _.1608]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1607 | _.1608];
@@ -64,11 +64,11 @@
   q=[1]; r=[0; 1];
   q=[0; 1]; r=[0; 0; 1];
   q=[1; 1]; r=[0; 1; 1];
-  q=[1; _.653; 1]; r=[0; 1; _.653; 1];
+  q=[1; _.225; 1]; r=[0; 1; _.225; 1];
   q=[0; 0; 1]; r=[0; 0; 0; 1];
   q=[0; 1; 1]; r=[0; 0; 1; 1];
-  q=[1; _.1001; _.408; 1]; r=[0; 1; _.1001; _.408; 1];
-  q=[0; 1; _.1243; 1]; r=[0; 0; 1; _.1243; 1];
+  q=[1; _.247; _.408; 1]; r=[0; 1; _.247; _.408; 1];
+  q=[0; 1; _.408; 1]; r=[0; 0; 1; _.408; 1];
   q=[0; 0; 0; 1]; r=[0; 0; 0; 0; 1];
   }
   fun q r -> lelo q r, 15 answers {

diff --git a/regression_ppx/test014.t b/regression_ppx/test014.t
@@ -1,3 +1,35 @@
   $ ./test014diseq.exe
   rel, 1 answer {
+  hd1 = _.12
+  hd2 = _.14
+  tl2 = _.15
+  10: { 0: [|  10 =/= _.11 |] }
+  
+  11: { 0: [|  11 =/= boxed 0 <_.12, _.13> |] }
+  
+  15: { 0: [|  14 =/= _.12,  15 =/= _.13 |] }
+  
+   hd2 === 1
+  15: { 0: [|  14 =/= _.12,  15 =/= _.13 |] }
+  
+   tl2 === []
+  13: { 0: [|  12 =/= int<1>,  13 =/= int<0> |] }
+  
+  47
+  13: { 0: [|  12 =/= int<1>,  13 =/= int<0> |] }
+  
+  }
+  fun _ ->
+    fresh x
+      ((Std.list Fun.id [!< x; !< x]) =/=
+         (Std.list Fun.id [!< (!! 1); !< (!! 2)])), 1 answer {
+  q=_.10;
+  }
+  fun q ->
+    fresh (x y) (trace_index "x" x) (trace_index "y" y) ((x % y) === q)
+      ((x % y) =/= (Std.list Fun.id [!! 1; x]))
+      (y === (Std.list Fun.id [!! 2])) success, 1 answer {
+  x = _.11
+  y = _.12
+  q=[_.11; 2];
   }
diff --git a/regression_ppx/test014diseq.ml b/regression_ppx/test014diseq.ml
@@ -32,14 +32,17 @@ let rel list1 =
     (trace_index "hd2" hd2)
     (trace_index "tl2" tl2)
     (list1 =/= list2)
+    trace_diseq
     (list1 === hd1 % tl1)
+    trace_diseq
     (list2 === hd2 % tl2)
     trace_diseq
     (trace " hd2 === 1")
     (hd2 === !!1)
     trace_diseq
-    (trace " tl2 === []") (* bad behaviour starts now *)
+    (trace " tl2 === []")
     (tl2 === nil ())
+    trace_diseq
     (hd1 === !!1)
     (debug_line __LINE__)
     trace_diseq
@@ -49,3 +52,36 @@ let rel list1 =
 
 (* let () = [%tester run_r [%show GT.int GT.list] (Std.List.reify reify) 1 (fun q -> rel q)] *)
 let () = run_r (Std.List.reify reify) ([%show: GT.int logic Std.List.logic] ()) 1 q qh (REPR rel)
+
+let () =
+  let open Std in
+  run_r
+    (Std.List.reify reify)
+    ([%show: GT.int logic Std.List.logic] ())
+    1
+    q
+    qh
+    (REPR (fun _ -> fresh x (Std.list Fun.id [ !<x; !<x ] =/= Std.list Fun.id [ !<(!!1); !<(!!2) ])))
+;;
+
+let () =
+  let open OCanren.Std in
+  run_r
+    (Std.List.reify reify)
+    ([%show: GT.int logic Std.List.logic] ())
+    1
+    q
+    qh
+    (REPR
+       (fun q ->
+         fresh
+           (x y)
+           (trace_index "x" x)
+           (trace_index "y" y)
+           (x % y === q)
+           (x % y =/= Std.list Fun.id [ !!1; x ])
+           (* trace_diseq *)
+           (y === Std.list Fun.id [ !!2 ])
+           (* trace_diseq *)
+           success))
+;;