From a8f8da7b98f1f43e18e7e16c00fcd0d514353f88 Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Sun, 26 Feb 2023 12:22:34 +0300
Subject: [PATCH 01/11] [wc] ppx_wildcard

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 ppx/wildcard/dune            |   8 +++
 ppx/wildcard/ppx_wildcard.ml | 123 +++++++++++++++++++++++++++++++++++
 2 files changed, 131 insertions(+)
 create mode 100644 ppx/wildcard/dune
 create mode 100644 ppx/wildcard/ppx_wildcard.ml

diff --git a/ppx/wildcard/dune b/ppx/wildcard/dune
new file mode 100644
index 000000000..25f60b4f1
--- /dev/null
+++ b/ppx/wildcard/dune
@@ -0,0 +1,8 @@
+(library
+ (name ppx_wildcard)
+ (public_name OCanren-ppx.ppx_wildcard)
+ (kind ppx_rewriter)
+ (libraries base ppxlib)
+ (modules ppx_wildcard)
+ (preprocess
+  (pps ppxlib.metaquot)))
diff --git a/ppx/wildcard/ppx_wildcard.ml b/ppx/wildcard/ppx_wildcard.ml
new file mode 100644
index 000000000..720fc2212
--- /dev/null
+++ b/ppx/wildcard/ppx_wildcard.ml
@@ -0,0 +1,123 @@
+(*
+ * OCanren. PPX syntax extensions.
+ * Copyright (C) 2015-2023
+ * Dmitri Boulytchev, Dmitry Kosarev, Alexey Syomin, Evgeny Moiseenko
+ * St.Petersburg State University, JetBrains Research
+ *
+ * This software is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Library General Public
+ * License version 2, as published by the Free Software Foundation.
+ *
+ * This software is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+ *
+ * See the GNU Library General Public License version 2 for more details
+ * (enclosed in the file COPYING).
+ *)
+
+(** This extension performs expansion of wildcards in:
+
+  {ul {- Unification
+         {[ (q === __ % __) ]} to {[ Fresh.two (fun __1 __2 -> q === __1 % __2) ]}
+      }
+      {- Disequality
+          {[ (q =/= Std.List.cons __ __) ]}
+             to
+          {[ wc (fun __1 -> wc (fun __2 -> q =/= Std.List.cons __1 __2)) ]}
+      }
+  }
+ *)
+
+open Ppxlib
+open Ppxlib.Ast_helper
+
+let name_of_loc loc =
+  (* Format.printf "name_of_loc: %a\n%!" Location.print loc; *)
+  let start = loc.Location.loc_start in
+  (* let mangled_fname =
+    String.map start.pos_fname ~f:(function
+        | '.' -> '_'
+        | c -> c)
+  in *)
+  let mangled_fname = start.pos_fname in
+  Printf.sprintf "__%s_c%d" mangled_fname Lexing.(start.pos_cnum - start.pos_bol)
+;;
+
+let wildcard_extractor expr =
+  let folder =
+    object
+      inherit [_] Ppxlib.Ast_traverse.fold_map as super
+
+      method! expression e acc =
+        (* Format.printf "wildcard_extractor: %a\n%!" Pprintast.expression e; *)
+        let open Ppxlib.Ast_pattern in
+        let loc = e.pexp_loc in
+        let on_OK =
+          let open Ppxlib.Ast_builder.Default in
+          pexp_ident ~loc (Located.mk ~loc (Lident (name_of_loc e.pexp_loc)))
+        in
+        parse
+          (pexp_ident (lident (string "__")))
+          loc
+          e
+          (on_OK, e.pexp_loc :: acc)
+          ~on_error:(fun () -> super#expression e acc)
+    end
+  in
+  folder#expression expr []
+;;
+
+type kind =
+  | Unif
+  | Diseq
+
+let mapper =
+  object
+    inherit Ast_traverse.map as super
+
+    method! expression e =
+      (* Format.printf "%a\n%!" Pprintast.expression  e; *)
+      let loc = e.pexp_loc in
+      let pat =
+        let open Ppxlib.Ast_pattern in
+        pexp_apply
+          (pexp_ident (lident (string "===")))
+          ((nolabel ** __) ^:: (nolabel ** __) ^:: nil)
+        |> map2 ~f:(fun a b -> Unif, a, b)
+        ||| (pexp_apply
+               (pexp_ident (lident (string "=/=")))
+               ((nolabel ** __) ^:: (nolabel ** __) ^:: nil)
+            |> map2 ~f:(fun a b -> Diseq, a, b))
+      in
+      let on_unif (kind, l, r) =
+        let l, accl = wildcard_extractor l in
+        let r, accr = wildcard_extractor r in
+        let f acc loc =
+          let open Ppxlib.Ast_builder.Default in
+          let name = name_of_loc loc in
+          let name_expr = pexp_constant ~loc (Pconst_string (name, loc, None)) in
+          let pat = ppat_var ~loc (Located.mk ~loc name) in
+          let nameless = true in
+          let make_wc, make_fresh =
+            if nameless
+            then [%expr wc], [%expr call_fresh]
+            else [%expr named_wc [%e name_expr]], [%expr named_fresh [%e name_expr]]
+          in
+          match kind with
+          | Diseq -> [%expr [%e make_wc] (fun [%p pat] -> [%e acc])]
+          | Unif -> [%expr [%e make_fresh] (fun [%p pat] -> [%e acc])]
+        in
+        let init =
+          match kind with
+          | Unif -> [%expr [%e l] === [%e r]]
+          | Diseq -> [%expr [%e l] =/= [%e r]]
+        in
+        let ans1 = ListLabels.fold_left ~f ~init accr in
+        ListLabels.fold_left ~f ~init:ans1 accl
+      in
+      Ppxlib.Ast_pattern.parse pat loc e on_unif ~on_error:(fun () -> super#expression e)
+  end
+;;
+
+let () = Ppxlib.Driver.register_transformation ~impl:mapper#structure "ppx_wildcard"

From 8c0ebacf9a222c70f177d68c23a3b95949f69f17 Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Sun, 26 Feb 2023 12:23:35 +0300
Subject: [PATCH 02/11] [wc] Wildcards in =/= implementation

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 src/core/Core.ml        |  7 ++++++
 src/core/Core.mli       |  2 ++
 src/core/Disequality.ml | 50 ++++++++++++++++++++++++-----------------
 src/core/Env.ml         |  8 +++++++
 src/core/Env.mli        |  6 +++++
 src/core/Subst.ml       | 35 ++++++++++++++++++++++++-----
 src/core/Term.ml        |  4 ++++
 src/core/Term.mli       |  4 ++++
 8 files changed, 89 insertions(+), 27 deletions(-)

diff --git a/src/core/Core.ml b/src/core/Core.ml
index c17e5a5e4..9a910a127 100644
--- a/src/core/Core.ml
+++ b/src/core/Core.ml
@@ -279,6 +279,7 @@ module State =
     let prunes {prunes} = prunes
 
     let fresh {env; scope} = Env.fresh ~scope env
+    let wc { env; scope } = Env.wc ~scope env
 
     let new_scope st = {st with scope = Term.Var.new_scope ()}
 
@@ -499,6 +500,12 @@ let call_fresh f st =
   let x = State.fresh st in
   f x st
 
+let wc f st =
+  let x = State.wc st in
+  f x st
+;;
+
+
 module Fresh =
   struct
     let succ prev f = call_fresh (fun x -> prev (f x))
diff --git a/src/core/Core.mli b/src/core/Core.mli
index 06fbc2fe9..9fb329bd7 100644
--- a/src/core/Core.mli
+++ b/src/core/Core.mli
@@ -42,6 +42,8 @@ type goal = State.t Stream.t goal'
     parameter. See also {!module-Fresh} to create variables in numbers. *)
 val call_fresh : ('a ilogic -> goal) -> goal
 
+val wc : ('a ilogic -> goal) -> goal
+
 (** [x === y] creates a goal, which performs a unification of [x] and [y] *)
 val (===) : 'a ilogic -> 'a ilogic -> goal
 
diff --git a/src/core/Disequality.ml b/src/core/Disequality.ml
index 013404a5b..b752f7017 100644
--- a/src/core/Disequality.ml
+++ b/src/core/Disequality.ml
@@ -16,9 +16,6 @@
  * (enclosed in the file COPYING).
  *)
 
-(* to avoid clash with Std.List (i.e. logic list) *)
-module List = Stdlib.List
-
 let log fmt =
   if false
   then Format.kasprintf (Format.printf "%s\n%!") fmt
@@ -158,8 +155,14 @@ module Disjunct :
     let refine env subst x y =
       match Subst.unify env subst x y with
       | None              -> Fulfiled
-      | Some ([], _)      -> Violated
-      | Some (prefix, _)  -> Refined prefix
+      | Some (prefix, _)  ->
+        let cond = fun {Subst.Binding.var; term} ->
+          if Term.Var.is_wildcard var || (Env.is_wc env term)
+            then false else true
+        in
+        match Stdlib.List.filter cond prefix with
+        | [] -> Violated
+        | prefix -> Refined prefix
 
     let make env subst x y =
       match refine env subst x y with
@@ -167,8 +170,7 @@ module Disjunct :
       | Fulfiled      -> raise Disequality_fulfilled
       | Violated      -> raise Disequality_violated
 
-    let rec recheck env subst (t: t): t  =
-      (* log "Disjunct.recheck: %a" pp t; *)
+    let rec recheck : Env.t -> Subst.t ->  t -> t = fun env subst t ->
       let var, term = Term.VarMap.max_binding t in
       (* log "       max bind index =  %d" var.Term.Var.index; *)
       let unchecked = Term.VarMap.remove var t in
@@ -298,17 +300,23 @@ module Conjunct :
     let make env subst x y =
       let id = !next_id in
       next_id := !next_id + 1;
-      M.singleton id @@ Disjunct.make env subst x y
+      M.singleton id (Disjunct.make env subst x y)
+
+    let split : t -> t Term.VarMap.t =
+      (* TODO(Kakadu): rewriter *)
+      let group_by : ('a -> Term.Var.t) -> 'a M.t -> 'a M.t Term.VarMap.t
+        = fun (* *) extract mapa ->
+          M.fold (fun k v acc ->
+            let new_key = extract v in
+            let upd = function
+              | Some old -> Some (M.add k v old)
+              | None      -> Some (M.singleton k v)
+            in
+            Term.VarMap.update new_key upd acc
+            ) mapa Term.VarMap.empty
+      in
+      group_by Disjunct.samplevar
 
-    let split t =
-      M.fold (fun id disj acc ->
-        let var = Disjunct.samplevar disj in
-        let upd = function
-        | Some conj -> Some (M.add id disj conj)
-        | None      -> Some (M.singleton id disj)
-        in
-        Term.VarMap.update var upd acc
-      ) t Term.VarMap.empty
 
     let recheck env subst t =
       (* log "Conjunct.recheck. %a" pp t; *)
@@ -396,11 +404,11 @@ module Conjunct :
              * then extended answers are [(x =/= 1) /\ (y =/= 2)] and [(x =/= 1) /\ (y =/= 2) /\ (z =/= 3)],
              * but the second one is subsumed by the first one and can be thrown away
              *)
-            if List.exists (fun {var; term} -> Answer.mem env answ var term) bs then
+            if Stdlib.List.exists (fun {var; term} -> Answer.mem env answ var term) bs then
               [answ]
             else
-              List.map (fun {var; term} -> Answer.add env answ var term) bs
-          ) |> List.concat
+              Stdlib.List.map (fun {var; term} -> Answer.add env answ var term) bs
+          ) |> Stdlib.List.concat
       ) t [Answer.empty]
 
   end
@@ -430,7 +438,7 @@ let add env subst cstore x y =
     Some (update env subst (Conjunct.make env subst x y) cstore)
   with
     | Disequality_fulfilled -> Some cstore
-    | Disequality_violated  -> None
+    | Disequality_violated -> None
 
 let recheck env subst cstore bs =
   let helper var cstore : t =
diff --git a/src/core/Env.ml b/src/core/Env.ml
index 6405faeb9..5455b72eb 100644
--- a/src/core/Env.ml
+++ b/src/core/Env.ml
@@ -34,6 +34,8 @@ let fresh ~scope e =
   e.next <- 1 + e.next;
   Obj.magic v
 
+let wc ~scope e = Obj.magic (Term.Var.make_wc ~env:e.anchor ~scope)
+
 let check env v = (v.Term.Var.env = env.anchor)
 
 let check_exn env v =
@@ -44,6 +46,12 @@ let var env x =
   | (Some v) as res -> check_exn env v ; res
   | None            -> None
 
+let is_wc env x =
+  match Term.var x with
+  | None -> false
+  | Some v -> check_exn env v; Term.Var.is_wildcard v
+
+
 let freevars env x =
   Term.fold (Term.repr x) ~init:Term.VarSet.empty
     ~fvar:(fun acc v -> Term.VarSet.add v acc)
diff --git a/src/core/Env.mli b/src/core/Env.mli
index fe849a02d..a1833f24a 100644
--- a/src/core/Env.mli
+++ b/src/core/Env.mli
@@ -40,6 +40,8 @@ val fresh : scope:Term.Var.scope -> t -> 'a
 
 val check : t -> Term.Var.t -> bool
 
+val wc : scope:Term.Var.scope -> t -> 'a
+
 val check_exn : t -> Term.Var.t -> unit
 
 (* See [Term.var] *)
@@ -47,6 +49,10 @@ val var : t -> 'a -> Term.Var.t option
 
 val freevars : t -> 'a -> Term.VarSet.t
 
+val is_wc        : t -> 'a -> bool
+
+(* val var           : t -> 'a -> Term.Var.t option *)
+
 val is_open : t -> 'a -> bool
 
 val equal : t -> t -> bool
diff --git a/src/core/Subst.ml b/src/core/Subst.ml
index b7a6da7c4..deda7e344 100644
--- a/src/core/Subst.ml
+++ b/src/core/Subst.ml
@@ -71,17 +71,18 @@ let pp ppf s =
   Term.VarMap.iter (fun x t -> fprintf ppf "%a |- %a; " Term.pp (Term.repr x) Term.pp t) s ;
   fprintf ppf "|subst}"
 
-type lterm = Var of Term.Var.t | Value of Term.t
+type lterm = Var of Term.Var.t | Value of Term.t | WC of Term.Var.t
 
 let walk env subst =
 
   (* walk var *)
   let rec walkv v =
     let () = IFDEF STATS THEN walk_incr () ELSE () END in
-    Env.check_exn env v ;
-
-    match v.Term.Var.subst with
-    | Some term -> walkt term
+    Env.check_exn env v;
+    if Term.Var.is_wildcard v
+    then WC v
+    else match v.Term.Var.subst with
+    | Some term -> walkt (Obj.magic term)
     | None ->
         try walkt (Term.VarMap.find v subst)
         with Not_found -> Var v
@@ -91,6 +92,7 @@ let walk env subst =
     let () = IFDEF STATS THEN walk_incr () ELSE () END in
 
     match Env.var env t with
+    | Some v when Term.Var.is_wildcard v -> WC v
     | Some v -> walkv v
     | None   -> Value t
   in
@@ -102,6 +104,7 @@ let map ~fvar ~fval env subst x =
   let rec deepfvar v =
     Env.check_exn env v;
     match walk env subst v with
+    | WC v
     | Var v   -> fvar v
     | Value x -> Term.map x ~fval ~fvar:deepfvar
   in
@@ -112,11 +115,23 @@ let iter ~fvar ~fval env subst x =
   let rec deepfvar v =
     Env.check_exn env v;
     match walk env subst v with
+    | WC v
     | Var v   -> fvar v
     | Value x -> Term.iter x ~fval ~fvar:deepfvar
   in
   Term.iter x ~fval ~fvar:deepfvar
 
+(* same as [Term.fold] but performs [walk] on the road *)
+let fold ~fvar ~fval ~init env subst x =
+  let rec deepfvar acc v =
+    Env.check_exn env v;
+    match walk env subst v with
+    | WC v
+    | Var v   -> fvar acc v
+    | Value x -> Term.fold x ~fval ~fvar:deepfvar ~init:acc
+  in
+  Term.fold x ~init ~fval ~fvar:deepfvar
+
 exception Occurs_check
 
 let rec occurs env subst var term = iter env subst term ~fval:(fun _ -> ())
@@ -151,6 +166,11 @@ let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
   let rec helper x y acc = Term.fold2 x y ~init:acc
     ~fvar:begin fun ((_, subst) as acc) x y ->
       match walk env subst x, walk env subst y with
+      | WC _, WC _ ->
+        (* TODO(Kakadu): explain why we return substitution as is *)
+        acc
+      | Var z, WC v | WC v, Var z -> extend (Obj.magic v) (Obj.repr z) acc
+      | Value z, WC v | WC v, Value z -> extend (Obj.magic v) (Obj.repr z) acc
       | Var x, Var y ->
         if Term.Var.equal x y then acc
         else extend x (Term.repr y) acc
@@ -163,11 +183,14 @@ let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
       else raise Unification_failed
     end
     ~fk:begin fun ((_, subst) as acc) l v y ->
-      if subsume && l = Term.R
+      if Term.Var.is_wildcard v
+      then acc
+      else if subsume && l = Term.R
       then raise Unification_failed
       else match walk env subst v with
       | Var v   -> extend v y acc
       | Value x -> helper x y acc
+      | WC _ -> failwith "Wildcards should not appear in unifications"
     end
   in
 
diff --git a/src/core/Term.ml b/src/core/Term.ml
index 2d8ed6d6b..e4bb001f5 100644
--- a/src/core/Term.ml
+++ b/src/core/Term.ml
@@ -61,6 +61,10 @@ module Var =
       scope;
     }
 
+    let is_wildcard { index } = index = -42
+
+    let make_wc ~env ~scope = make ~env ~scope (-42)
+
     let dummy =
       let env   = 0 in
       let scope = 0 in
diff --git a/src/core/Term.mli b/src/core/Term.mli
index f70c1b6fd..5c6a9038e 100644
--- a/src/core/Term.mli
+++ b/src/core/Term.mli
@@ -53,6 +53,10 @@ module Var :
     val hash : t -> int
 
     val describe : Format.formatter -> t -> unit
+
+    val is_wildcard : t -> bool
+
+    val make_wc : env:env -> scope:scope -> t
   end
 
 module VarSet : Set.S with type elt = Var.t

From f5ea0718e42fcef5f9ea2e50883e89e8f115af2e Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Thu, 9 Oct 2025 23:04:30 +0300
Subject: [PATCH 03/11] [wc] Wildcards in =/= tests

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 test_wc/.ocamlformat |   2 +
 test_wc/debug_var.ml |  35 +++++
 test_wc/debug_var.t  |   0
 test_wc/dune         |  40 +++++
 test_wc/main.ml      | 289 ++++++++++++++++++++++++++++++++++++
 test_wc/main.t       | 122 ++++++++++++++++
 test_wc/match.ml     | 341 +++++++++++++++++++++++++++++++++++++++++++
 test_wc/peano.ml     |  38 +++++
 test_wc/peano.t      |  17 +++
 9 files changed, 884 insertions(+)
 create mode 100644 test_wc/.ocamlformat
 create mode 100644 test_wc/debug_var.ml
 create mode 100644 test_wc/debug_var.t
 create mode 100644 test_wc/dune
 create mode 100644 test_wc/main.ml
 create mode 100644 test_wc/main.t
 create mode 100644 test_wc/match.ml
 create mode 100644 test_wc/peano.ml
 create mode 100644 test_wc/peano.t

diff --git a/test_wc/.ocamlformat b/test_wc/.ocamlformat
new file mode 100644
index 000000000..e0fad4ee4
--- /dev/null
+++ b/test_wc/.ocamlformat
@@ -0,0 +1,2 @@
+profile=janestreet
+max-indent = 2
diff --git a/test_wc/debug_var.ml b/test_wc/debug_var.ml
new file mode 100644
index 000000000..8b8d2671b
--- /dev/null
+++ b/test_wc/debug_var.ml
@@ -0,0 +1,35 @@
+open OCanren
+open OCanren.Std
+open Tester
+
+let show_int = GT.show GT.int
+let show_intl = GT.show logic (GT.show GT.int)
+let run_int eta = run_r OCanren.reify (GT.show logic @@ GT.show GT.int) eta
+let show_pairl = GT.show Pair.logic show_intl show_intl
+let run_pair eta = run_r (Pair.reify reify reify) show_pairl eta
+
+let trace_int q =
+  debug_var q (Fun.flip OCanren.reify) (fun xs ->
+    Stdlib.List.iter (fun x -> print_endline @@ show_intl x) xs;
+    success)
+;;
+
+let trace_pair (q : (_, _) Pair.groundi) =
+  debug_var
+    q
+    (Fun.flip @@ Pair.reify reify reify)
+    (fun xs ->
+      Stdlib.List.iter (fun x -> print_endline @@ show_pairl x) xs;
+      success)
+;;
+
+let _ = [%tester run_int (-1) (fun q -> trace_int q)]
+let __ _ = [%tester run_int (-1) (fun q -> q === !!1 &&& trace_int q)]
+let _ = [%tester run_int (-1) (fun q -> q =/= !!1 &&& trace_int q)]
+let _ = [%tester run_pair (-1) (fun q -> q =/= Std.pair !!1 !!2 &&& trace_pair q)]
+
+let _ =
+  [%tester
+    run_pair (-1) (fun q ->
+      fresh (x y) (q =/= Std.pair x y) (x =/= !!1) (y =/= !!2) (trace_pair q))]
+;;
diff --git a/test_wc/debug_var.t b/test_wc/debug_var.t
new file mode 100644
index 000000000..e69de29bb
diff --git a/test_wc/dune b/test_wc/dune
new file mode 100644
index 000000000..3a0056a9a
--- /dev/null
+++ b/test_wc/dune
@@ -0,0 +1,40 @@
+(env
+ (_
+  (flags
+   (:standard -rectypes))))
+
+(executables
+ (names main debug_var peano)
+ (modules main debug_var peano)
+ (preprocess
+  (pps
+   ppx_expect
+   OCanren-ppx.ppx_wildcard
+   OCanren-ppx.ppx_repr
+   OCanren-ppx.ppx_fresh
+   OCanren-ppx.ppx_tester
+   OCanren-ppx.ppx_distrib
+   GT.ppx_all))
+ (libraries OCanren OCanren.tester))
+
+(library
+ (name match)
+ (modules match)
+ (libraries OCanren OCanren.tester)
+ (preprocess
+  (pps
+   ppx_expect
+   OCanren-ppx.ppx_wildcard
+   OCanren-ppx.ppx_repr
+   OCanren-ppx.ppx_fresh
+   OCanren-ppx.ppx_tester
+   GT.ppx_all))
+ (inline_tests))
+
+(cram
+ (deps
+  ./main.exe
+  ./debug_var.exe
+  ./peano.exe
+  ;
+  ))
diff --git a/test_wc/main.ml b/test_wc/main.ml
new file mode 100644
index 000000000..e8113f896
--- /dev/null
+++ b/test_wc/main.ml
@@ -0,0 +1,289 @@
+open OCanren
+open OCanren.Std
+open Tester
+
+let show_int = GT.show GT.int
+let show_intl = GT.show logic (GT.show GT.int)
+let show_bool = GT.show GT.bool
+let show_booll = GT.show logic (GT.show GT.bool)
+let run_bool eta = run_r OCanren.reify (GT.show logic @@ GT.show GT.bool) eta
+let run_int eta = run_r OCanren.reify (GT.show logic @@ GT.show GT.int) eta
+
+let run_pair eta =
+  run_r
+    (Pair.reify OCanren.reify OCanren.reify)
+    (GT.show Pair.logic show_intl show_intl)
+    eta
+;;
+
+let run_pair_bool eta =
+  run_r
+    (Pair.reify OCanren.reify OCanren.reify)
+    (GT.show Pair.logic show_booll show_booll)
+    eta
+;;
+
+let run_pair_int eta =
+  run_r
+    (Pair.reify OCanren.reify OCanren.reify)
+    ([%show: (GT.int OCanren.logic, GT.int OCanren.logic) Std.Pair.logic] ())
+    eta
+;;
+
+let run_list eta = run_r (List.reify OCanren.reify) (GT.show Std.List.logic show_intl) eta
+let triple a b c = pair a (pair b c)
+
+let run_triple eta =
+  run_r
+    (Pair.reify OCanren.reify (Pair.reify OCanren.reify OCanren.reify))
+    (GT.show Pair.logic show_intl (GT.show Pair.logic show_intl show_intl))
+    eta
+;;
+
+let run_exn eta = run_r OCanren.prj_exn show_int eta
+
+let __ _ =
+  run_exn (-1) q qh (REPR (fun _ -> fresh (x y) (x === y) (x =/= y)));
+  run_exn (-1) q qh (REPR (fun _ -> fresh (x y) (x =/= y) (x === y)));
+  exit 1
+;;
+
+let _ = [%tester run_int (-1) (fun q -> q === __)]
+let _ = [%tester run_int (-1) (fun q -> q =/= __)]
+let _ = [%tester run_int (-1) (fun _ -> __ =/= __)]
+let _ = [%tester run_int (-1) (fun _ -> !!5 =/= __)]
+let _ = [%tester run_pair (-1) (fun _ -> pair !!2 __ =/= pair __ !!2)]
+(* let _ = exit 0 *)
+
+let _ =
+  [%tester run_pair (-1) (fun q -> fresh () (q =/= pair __ !!1) (q === pair !!1 __))]
+;;
+
+(* ***************************** *)
+let _ = [%tester run_pair (-1) (fun _ -> pair !!1 __ === pair __ !!1)]
+let _ = [%tester run_pair (-1) (fun q -> q === pair __ !!1 &&& (q === pair !!1 __))]
+let _ = [%tester run_pair (-1) (fun _ -> pair !!1 __ =/= pair __ !!1)]
+let _ = [%tester run_pair (-1) (fun _ -> pair !!1 __ =/= pair !!2 __)]
+let _ = [%tester run_int (-1) (fun q -> triple q !!2 __ =/= triple !!1 __ !!2)]
+let _ = [%tester run_int (-1) (fun q r -> pair q r =/= pair !!1 __)]
+let _ = [%tester run_int (-1) (fun q -> pair q !!1 =/= pair !!1 __)]
+
+let _ =
+  [%tester
+    run_pair (-1) (fun q ->
+      fresh
+        (a b)
+        (q === pair a b)
+        (* (debug_var a OCanren.reify (fun _ ->
+               let () = OCanren.set_diseq_logging true in
+               success)) *)
+        (q =/= pair !!1 __)
+        (q === pair __ !!1))]
+;;
+
+(* let () = OCanren.set_diseq_logging false *)
+
+let _ =
+  [%tester
+    run_pair (-1) (fun q ->
+      fresh (a b) (q =/= pair !!1 __) (* (q =/= pair __ !!1)  *) (q === pair a b))]
+;;
+
+let _ =
+  [%tester run_pair (-1) (fun q -> fresh () (q =/= pair !!1 __) (q =/= pair __ !!1))]
+;;
+
+let _ =
+  [%tester
+    run_pair (-1) (fun q ->
+      fresh (a b) (q =/= pair !!1 __) (q === pair __ !!1) (q === pair a b))]
+;;
+
+let _ =
+  [%tester run_list (-1) (fun q -> fresh () (q === !!1 % (!!2 % __)) (q === __ % __))]
+;;
+
+let _ =
+  [%tester run_list (-1) (fun q -> fresh (a b) (q === !!1 % (!!2 % __)) (q === a % b))]
+;;
+
+let _ =
+  [%tester
+    run_list (-1) (fun q -> fresh () (q === __ % __) (q === !<(!!1)) (q === !<(!!2)))]
+;;
+
+let _ = [%tester run_int (-1) (fun q -> q === !!1 &&& (__ =/= !!1 % __))]
+let _ = [%tester run_int (-1) (fun q -> fresh (a b) (q === !!1) (a =/= !!1 % b))]
+let _ = [%tester run_int (-1) (fun q -> fresh a (q === !!1) (a =/= !!1 % a))]
+
+let rec non_membero x xs =
+  let open OCanren.Std in
+  fresh
+    ()
+    (xs =/= List.cons x __)
+    (conde
+       [ fresh (h tl) (xs === List.cons h tl) (non_membero x tl); xs === List.nil () ])
+;;
+
+let _ =
+  [%tester run_int (-1) (fun _ -> non_membero !!0 (Std.list ( !! ) [ 1; 2; 3 ]))];
+  [%tester run_int (-1) (fun _ -> non_membero !!0 (Std.list ( !! ) []))];
+  [%tester run_int (-1) (fun _ -> non_membero !!0 (Std.list ( !! ) [ 0 ]))];
+  ()
+;;
+
+let _ = [%tester run_list (-1) (fun q -> q =/= __ % __ &&& (q =/= List.nil ()))]
+
+(*      fresh () (q =/= pair true_ __) (q === pair __ true_) *)
+let _ =
+  [%tester
+    run_pair_bool (-1) (fun q -> q =/= Std.pair !!true __ &&& (q === Std.pair __ !!true))]
+;;
+
+let _ = [%tester run_pair_bool (-1) (fun _ -> __ =/= Std.pair __ !!true)]
+
+let _ =
+  [%tester
+    run_pair_bool (-1) (fun q ->
+      fresh () (q === Std.pair !!false !!true) (q =/= Std.pair !!true __))]
+;;
+
+let __ _ =
+  [%tester
+    run_pair_bool (-1) (fun _ ->
+      fresh () (Std.pair !!false !!true =/= Std.pair !!true __))]
+;;
+
+let _ =
+  [%tester
+    run_pair_bool (-1) (fun q ->
+      fresh () (q =/= Std.pair !!true __) (q === Std.pair !!false !!true))]
+;;
+
+let __ _ =
+  [%tester
+    run_list (-1) (fun _ -> fresh (x y) (!![ x; !!1 ] =/= !![ !!2; y ]) (x === !!2))]
+;;
+
+let _ =
+  [%tester
+    run_list (-1) (fun _ ->
+      fresh
+        (x y)
+        (* TODO: document that using logic lists is not strongly required *)
+        (!![ x; !!1 ] =/= !![ !!2; y ])
+        (* trace_diseq_constraints *)
+        (y === !!1)
+        success)]
+;;
+
+(* let () = OCanren.set_diseq_logging false *)
+
+let _ =
+  [%tester
+    run_pair_int (-1) (fun q ->
+      fresh
+        (x y)
+        (Std.pair x !!1 =/= Std.pair !!2 y)
+        (x === !!2)
+        (* (debug_var x OCanren.reify (fun _ ->
+               let () = OCanren.set_diseq_logging true in
+               trace_diseq_constraints)) *)
+        (y === !!9)
+        (Std.pair x y === q))]
+;;
+
+(* let () = OCanren.set_diseq_logging false *)
+
+let _ =
+  [%tester
+    run_pair (-1) (fun q ->
+      fresh (a b) (q === pair a b) (q =/= pair !!1 __) (* trace_diseq_constraints *))]
+;;
+
+let _ =
+  [%tester
+    run_pair (-1) (fun q ->
+      fresh
+        (a b)
+        (q === pair a b)
+        (q =/= pair !!1 __)
+        (* trace_diseq_constraints *)
+        (q === pair __ !!1))]
+;;
+
+(* let () = OCanren.set_diseq_logging false *)
+
+let _ =
+  [%tester
+    run_pair (-1) (fun q ->
+      fresh (a b) (q === pair a b) (q =/= pair __ __) (* trace_diseq_constraints *))]
+;;
+
+module Expr = struct
+  type ('tag, 'args) t = Econstr of 'tag * 'args [@@deriving gt ~options:{ gmap; show }]
+  type ground = (GT.string, ground Std.List.ground) t
+  (* [@@deriving gt ~options:{ show }] *)
+
+  type logic = (GT.string OCanren.logic, logic Std.List.logic) t OCanren.logic
+  [@@deriving gt ~options:{ show }]
+
+  let make t xs = inj (Econstr (t, xs))
+
+  let fmapt fa fb subj =
+    let open Env.Monad in
+    Env.Monad.return (GT.gmap t) <*> fa <*> fb <*> subj
+  ;;
+
+  type injected = (string ilogic, injected Std.List.injected) t OCanren.ilogic
+
+  let (reify : (_, logic) Reifier.t) =
+    let open Env.Monad in
+    Reifier.fix (fun self ->
+      OCanren.reify
+      <..> chain
+             (Reifier.zed
+                (Reifier.rework ~fv:(fmapt OCanren.reify (Std.List.reify self)))))
+  ;;
+end
+
+let run_expr eta = run_r Expr.reify (GT.show Expr.logic) eta
+
+let _ =
+  [%tester
+    run_expr (-1) (fun q ->
+      fresh (a b c) (q === Expr.make !!"triple" (a % (b %< c))) (q =/= Expr.make __ __)
+      (* trace_diseq_constraints *))]
+;;
+
+module _ = struct
+  module Op = struct
+    [%%ocanren_inject
+    type nonrec t = LE [@@deriving gt ~options:{ show; fmt; gmap }]
+    type nonrec ground = t]
+  end
+
+  [%%ocanren_inject
+  type nonrec ('self, 'binop, 'term) t =
+    | True
+    | Not of 'self
+    | Op of 'binop * 'term * 'term
+    | Var of 'term
+  [@@deriving gt ~options:{ show; fmt; gmap }]
+
+  type ground = (ground, Op.ground, GT.string) t]
+
+  let run_t eta = Tester.run_r reify (GT.show logic) eta
+  let le a b = !!(Op (!!Op.LE, a, b))
+  let _ = var !!""
+
+  let _ =
+    [%tester
+      run_t (-1) (fun _ ->
+        fresh
+          www
+          (Std.pair (le !!"one" !!"x") (le !!"one" !!"x")
+          =/= Std.pair (le __ www) (le __ www))
+        (* gives an answer, bvecause it simplifies to www=/= "x" *))]
+  ;;
+end
diff --git a/test_wc/main.t b/test_wc/main.t
new file mode 100644
index 000000000..7cda37b0d
--- /dev/null
+++ b/test_wc/main.t
@@ -0,0 +1,122 @@
+  $ ./main.exe
+  fun q -> q === __, all answers {
+  q=_.11;
+  }
+  fun q -> q =/= __, all answers {
+  }
+  fun _ -> __ =/= __, all answers {
+  }
+  fun _ -> (!! 5) =/= __, all answers {
+  }
+  fun _ -> (pair (!! 2) __) =/= (pair __ (!! 2)), all answers {
+  }
+  fun q -> fresh () (q =/= (pair __ (!! 1))) (q === (pair (!! 1) __)), all answers {
+  q=(1, _.11 [=/= 1]);
+  }
+  fun _ -> (pair (!! 1) __) === (pair __ (!! 1)), all answers {
+  q=_.10;
+  }
+  fun q -> (q === (pair __ (!! 1))) &&& (q === (pair (!! 1) __)), all answers {
+  q=(1, 1);
+  }
+  fun _ -> (pair (!! 1) __) =/= (pair __ (!! 1)), all answers {
+  }
+  fun _ -> (pair (!! 1) __) =/= (pair (!! 2) __), all answers {
+  q=_.10;
+  }
+  fun q -> (triple q (!! 2) __) =/= (triple (!! 1) __ (!! 2)), all answers {
+  q=_.10 [=/= 1];
+  }
+  fun q -> fun r -> (pair q r) =/= (pair (!! 1) __), all answers {
+  q=_.10 [=/= 1]; r=_.11;
+  }
+  fun q -> (pair q (!! 1)) =/= (pair (!! 1) __), all answers {
+  q=_.10 [=/= 1];
+  }
+  fun q ->
+    fresh (a b) (q === (pair a b)) (q =/= (pair (!! 1) __))
+      (q === (pair __ (!! 1))), all answers {
+  q=(_.13 [=/= 1], 1);
+  }
+  fun q -> fresh (a b) (q =/= (pair (!! 1) __)) (q === (pair a b)), all answers {
+  q=(_.11 [=/= 1], _.12);
+  }
+  fun q -> fresh () (q =/= (pair (!! 1) __)) (q =/= (pair __ (!! 1))), all answers {
+  q=_.10 [=/= (1, _.-42)];
+  }
+  fun q ->
+    fresh (a b) (q =/= (pair (!! 1) __)) (q === (pair __ (!! 1)))
+      (q === (pair a b)), all answers {
+  q=(_.11 [=/= 1], 1);
+  }
+  fun q -> fresh () (q === ((!! 1) % ((!! 2) % __))) (q === (__ % __)), all answers {
+  q=[1; 2 | _.11];
+  }
+  fun q -> fresh (a b) (q === ((!! 1) % ((!! 2) % __))) (q === (a % b)), all answers {
+  q=[1; 2 | _.13];
+  }
+  fun q -> fresh () (q === (__ % __)) (q === (!< (!! 1))) (q === (!< (!! 2))), all answers {
+  }
+  fun q -> (q === (!! 1)) &&& (__ =/= ((!! 1) % __)), all answers {
+  }
+  fun q -> fresh (a b) (q === (!! 1)) (a =/= ((!! 1) % b)), all answers {
+  q=1;
+  }
+  fun q -> fresh a (q === (!! 1)) (a =/= ((!! 1) % a)), all answers {
+  q=1;
+  }
+  fun _ -> non_membero (!! 0) (Std.list (!!) [1; 2; 3]), all answers {
+  q=_.10;
+  }
+  fun _ -> non_membero (!! 0) (Std.list (!!) []), all answers {
+  q=_.10;
+  }
+  fun _ -> non_membero (!! 0) (Std.list (!!) [0]), all answers {
+  }
+  fun q -> (q =/= (__ % __)) &&& (q =/= (List.nil ())), all answers {
+  q=_.10 [=/= [_.-42 | _.-42]; =/= []];
+  }
+  fun q -> (q =/= (Std.pair (!! true) __)) &&& (q === (Std.pair __ (!! true))), all answers {
+  q=(_.11 [=/= true], true);
+  }
+  fun _ -> __ =/= (Std.pair __ (!! true)), all answers {
+  }
+  fun q ->
+    fresh () (q === (Std.pair (!! false) (!! true)))
+      (q =/= (Std.pair (!! true) __)), all answers {
+  q=(false, true);
+  }
+  fun q ->
+    fresh () (q =/= (Std.pair (!! true) __))
+      (q === (Std.pair (!! false) (!! true))), all answers {
+  q=(false, true);
+  }
+  fun _ ->
+    fresh (x y) ((!! [x; !! 1]) =/= (!! [!! 2; y])) (y === (!! 1)) success, all answers {
+  q=_.10;
+  }
+  fun q ->
+    fresh (x y) ((Std.pair x (!! 1)) =/= (Std.pair (!! 2) y)) (x === (!! 2))
+      (y === (!! 9)) ((Std.pair x y) === q), all answers {
+  q=(2, 9);
+  }
+  fun q -> fresh (a b) (q === (pair a b)) (q =/= (pair (!! 1) __)), all answers {
+  q=(_.11 [=/= 1], _.12);
+  }
+  fun q ->
+    fresh (a b) (q === (pair a b)) (q =/= (pair (!! 1) __))
+      (q === (pair __ (!! 1))), all answers {
+  q=(_.13 [=/= 1], 1);
+  }
+  fun q -> fresh (a b) (q === (pair a b)) (q =/= (pair __ __)), all answers {
+  }
+  fun q ->
+    fresh (a b c) (q === (Expr.make (!! "triple") (a % (b %< c))))
+      (q =/= (Expr.make __ __)), all answers {
+  }
+  fun _ ->
+    fresh www
+      ((Std.pair (le (!! "one") (!! "x")) (le (!! "one") (!! "x"))) =/=
+         (Std.pair (le __ www) (le __ www))), all answers {
+  q=_.10;
+  }
diff --git a/test_wc/match.ml b/test_wc/match.ml
new file mode 100644
index 000000000..08df7fd2b
--- /dev/null
+++ b/test_wc/match.ml
@@ -0,0 +1,341 @@
+open OCanren
+open Tester
+open OCanren.Std
+
+let bool_dom l = conde [ l === !!false; l === !!true ]
+let run_int eta = run_r OCanren.reify ([%show: GT.int logic] ()) eta
+
+module _ = struct
+  let source = {|
+    match ... with
+    | t,_ -> 1
+    | _,_ -> 2
+  |}
+
+  let%expect_test " " =
+    Printf.printf "Pseudecode:\n%s\n" source;
+    [%expect
+      {|
+      Pseudecode:
+
+          match ... with
+          | t,_ -> 1
+          | _,_ -> 2 |}]
+  ;;
+
+  let run_m eta =
+    run_r
+      (Pair.reify (Pair.reify OCanren.reify OCanren.reify) OCanren.reify)
+      ([%show:
+         ((GT.bool logic, GT.bool logic) Std.Pair.logic, GT.int logic) Std.Pair.logic]
+         ())
+      eta
+  ;;
+
+  let test ?(explicit = true) rel =
+    [%tester
+      run_m (-1) (fun q ->
+        fresh
+          (scru rhs)
+          (q === pair scru rhs)
+          (rel scru rhs)
+          (fresh
+             (l r)
+             (scru === Std.pair l r)
+             (if explicit then bool_dom l &&& bool_dom r else success)))]
+  ;;
+
+  let naive_rel q rez =
+    conde
+      [ fresh () (q === Std.pair !!true __) (rez === !!1)
+      ; fresh temp (q =/= Std.pair !!true temp) (rez === !!2)
+      ]
+  ;;
+
+  let%expect_test "Without disequalities at all" =
+    let xxx q rez =
+      conde
+        [ fresh () (q === Std.pair !!true __) (rez === !!1)
+        ; fresh (l r) (q === Std.pair l r) (rez === !!2)
+        ]
+    in
+    test ~explicit:false xxx;
+    [%expect
+      {|
+      fun q ->
+        fresh (scru rhs) (q === (pair scru rhs)) (rel scru rhs)
+          (fresh (l r) (scru === (Std.pair l r))
+             (if explicit then (bool_dom l) &&& (bool_dom r) else success)), all answers {
+      q=((true, _.17), 1);
+      q=((_.18, _.19), 2);
+      } |}];
+    test ~explicit:true xxx;
+    [%expect
+      {|
+      fun q ->
+        fresh (scru rhs) (q === (pair scru rhs)) (rel scru rhs)
+          (fresh (l r) (scru === (Std.pair l r))
+             (if explicit then (bool_dom l) &&& (bool_dom r) else success)), all answers {
+      q=((true, false), 1);
+      q=((true, true), 1);
+      q=((false, false), 2);
+      q=((true, false), 2);
+      q=((false, true), 2);
+      q=((true, true), 2);
+      } |}]
+  ;;
+
+  let%expect_test " " =
+    print_endline "Naive with diseq constraints (6 answers instead of 4): ";
+    test ~explicit:false naive_rel;
+    [%expect
+      {|
+      Naive with diseq constraints (6 answers instead of 4):
+      fun q ->
+        fresh (scru rhs) (q === (pair scru rhs)) (rel scru rhs)
+          (fresh (l r) (scru === (Std.pair l r))
+             (if explicit then (bool_dom l) &&& (bool_dom r) else success)), all answers {
+      q=((true, _.16), 1);
+      q=((_.17, _.18 [=/= _.13]), 2);
+      q=((_.17 [=/= true], _.18), 2);
+      } |}]
+  ;;
+
+  let smart_rel q rez =
+    conde
+      [ fresh () (q === Std.pair !!true __) (rez === !!1)
+      ; fresh () (q =/= Std.pair !!true __) (rez === !!2)
+      ]
+  ;;
+
+  let%expect_test " " =
+    print_endline "With wildcards (explicit domain):";
+    test smart_rel;
+    [%expect
+      {|
+      With wildcards (explicit domain):
+      fun q ->
+        fresh (scru rhs) (q === (pair scru rhs)) (rel scru rhs)
+          (fresh (l r) (scru === (Std.pair l r))
+             (if explicit then (bool_dom l) &&& (bool_dom r) else success)), all answers {
+      q=((true, false), 1);
+      q=((false, false), 2);
+      q=((true, true), 1);
+      q=((false, true), 2);
+      } |}];
+    print_endline "With wildcards (no domain):";
+    test ~explicit:false smart_rel;
+    [%expect
+      {|
+      With wildcards (no domain):
+      fun q ->
+        fresh (scru rhs) (q === (pair scru rhs)) (rel scru rhs)
+          (fresh (l r) (scru === (Std.pair l r))
+             (if explicit then (bool_dom l) &&& (bool_dom r) else success)), all answers {
+      q=((true, _.15), 1);
+      q=((_.16 [=/= true], _.17), 2);
+      } |}]
+  ;;
+end
+
+module _ = struct
+  let source =
+    {|
+    match ... with
+    | _,f,t -> 1
+    | f,t,_ -> 2
+    | _,_,f -> 3
+    | _,_,t -> 4
+  |}
+  ;;
+
+  let%expect_test " " =
+    Printf.printf "*******\n\nLonger example for Luc's Maranget paper\n";
+    Printf.printf "Pseudecode:\n%s\n" source;
+    [%expect
+      {|
+      *******
+
+      Longer example for Luc's Maranget paper
+      Pseudecode:
+
+          match ... with
+          | _,f,t -> 1
+          | f,t,_ -> 2
+          | _,_,f -> 3
+          | _,_,t -> 4 |}]
+  ;;
+
+  let run_m eta =
+    run_r
+      (Pair.reify (Triple.reify OCanren.reify OCanren.reify OCanren.reify) OCanren.reify)
+      ([%show:
+         ( (GT.bool logic, GT.bool logic, GT.bool logic) Std.Triple.logic
+         , GT.int logic )
+         Std.Pair.logic]
+         ())
+      eta
+  ;;
+
+  let test ?(explicit = true) rel =
+    [%tester
+      run_m (-1) (fun q ->
+        fresh
+          (scru rhs l m r)
+          (q === pair scru rhs)
+          (rel scru rhs)
+          (scru === Std.triple l m r)
+          (if explicit then bool_dom l &&& bool_dom m &&& bool_dom r else success))]
+  ;;
+
+  let smart_rel q rez =
+    let _T = !!true in
+    let _F = !!false in
+    let w = Std.triple in
+    conde
+      [ fresh () (rez === !!1) (q === w __ _F _T)
+      ; fresh () (rez === !!2) (q === w _F _T __) (q =/= w __ _F _T)
+      ; fresh () (rez === !!3) (q === w __ __ _F) (q =/= w __ _F _T) (q =/= w _F _T __)
+      ; fresh
+          ()
+          (rez === !!4)
+          (q =/= w __ _F _T)
+          (q =/= w _F _T __)
+          (q =/= w __ __ _F)
+          (q === w __ __ _T)
+      ]
+  ;;
+
+  let%expect_test " " =
+    print_endline "With wildcards (explicit domain): ";
+    test smart_rel;
+    [%expect
+      {|
+      With wildcards (explicit domain):
+      fun q ->
+        fresh (scru rhs l m r) (q === (pair scru rhs)) (rel scru rhs)
+          (scru === (Std.triple l m r))
+          (if explicit
+           then ((bool_dom l) &&& (bool_dom m)) &&& (bool_dom r)
+           else success), all answers {
+      q=((false, false, true), 1);
+      q=((true, false, true), 1);
+      q=((false, true, false), 2);
+      q=((false, true, true), 2);
+      q=((true, true, true), 4);
+      q=((false, false, false), 3);
+      q=((true, false, false), 3);
+      q=((true, true, false), 3);
+      } |}];
+    print_endline "With wildcards (no explicit domain): ";
+    test ~explicit:false smart_rel;
+    [%expect
+      {|
+      With wildcards (no explicit domain):
+      fun q ->
+        fresh (scru rhs l m r) (q === (pair scru rhs)) (rel scru rhs)
+          (scru === (Std.triple l m r))
+          (if explicit
+           then ((bool_dom l) &&& (bool_dom m)) &&& (bool_dom r)
+           else success), all answers {
+      q=((_.13, false, true), 1);
+      q=((false, true, _.15), 2);
+      q=((_.13, _.14 [=/= true], false), 3);
+      q=((_.13, _.14 [=/= false; =/= true], true), 4);
+      q=((_.13 [=/= false], _.14, false), 3);
+      q=((_.13 [=/= false], _.14 [=/= false], true), 4);
+      } |}]
+  ;;
+
+  let naive_rel q rez =
+    let _T = !!true in
+    let _F = !!false in
+    let w = Std.triple in
+    conde
+      [ fresh () (rez === !!1) (q === w __ _F _T)
+      ; fresh x (rez === !!2) (q === w _F _T __) (q =/= w x _F _T)
+      ; fresh (x z) (rez === !!3) (q === w __ __ _F) (q =/= w x _F _T) (q =/= w _F _T z)
+      ; fresh
+          (x y z x2 y2)
+          (rez === !!4)
+          (q =/= w x _F _T)
+          (q =/= w _F _T z)
+          (q =/= w x y _F)
+          (q === w x2 y2 _T)
+      ]
+  ;;
+
+  let%expect_test " " =
+    test ~explicit:false naive_rel;
+    [%expect
+      {|
+      fun q ->
+        fresh (scru rhs l m r) (q === (pair scru rhs)) (rel scru rhs)
+          (scru === (Std.triple l m r))
+          (if explicit
+           then ((bool_dom l) &&& (bool_dom m)) &&& (bool_dom r)
+           else success), all answers {
+      q=((_.13, false, true), 1);
+      q=((false, true, _.15), 2);
+      q=((_.13, _.14, false), 3);
+      q=((_.13, _.14 [=/= false], true), 4);
+      q=((_.13 [=/= _.21], _.14, true), 4);
+      } |}]
+  ;;
+
+  let%expect_test " " =
+    [%tester
+      run_int (-1) (fun rhs -> fresh s (s === Std.triple !!true __ __) (smart_rel s rhs))];
+    [%expect
+      {|
+      fun rhs -> fresh s (s === (Std.triple (!! true) __ __)) (smart_rel s rhs), all answers {
+      q=1;
+      q=3;
+      q=4;
+      } |}]
+  ;;
+
+  let hack q rez =
+    let _T = !!true in
+    let _F = !!false in
+    let w = Std.triple in
+    conde
+      [ failure
+        (* ; fresh () (rez === !!1) (q === w __ _F _T) *)
+        (* ; fresh () (rez === !!2) (q === w _F _T __) (q =/= w __ _F _T) *)
+        (* ; fresh () (rez === !!3) (q === w __ __ _F) (q =/= w __ _F _T) (q =/= w _F _T __) *)
+      ; fresh
+          ()
+          (rez === !!4)
+          (* (q === w __ __ __) *)
+          (q =/= w __ _F _T)
+          (q =/= w _F _T __)
+          (q =/= w __ __ _F)
+          (debug_var !!1 (Fun.flip OCanren.reify) (fun _ ->
+             (* OCanren.set_diseq_logging true; *)
+             success))
+          (q === w __ __ _T)
+      ]
+  ;;
+
+  let%expect_test " " =
+    [%tester
+      run_m (-1) (fun q ->
+        fresh
+          (scru rhs (* l m r*))
+          (q === pair scru rhs)
+          (* (scru === Std.triple l m r) *)
+          (hack scru rhs)
+          (* (bool_dom l) *)
+          (* (bool_dom m) *)
+          (* (bool_dom r) *)
+          (* trace_diseq_constraints *)
+          success)];
+    [%expect
+      {|
+      fun q -> fresh (scru rhs) (q === (pair scru rhs)) (hack scru rhs) success, all answers {
+      q=((_.13, _.14 [=/= false; =/= true], true), 4);
+      q=((_.13 [=/= false], _.14 [=/= false], true), 4);
+      } |}]
+  ;;
+end
diff --git a/test_wc/peano.ml b/test_wc/peano.ml
new file mode 100644
index 000000000..9d8877845
--- /dev/null
+++ b/test_wc/peano.ml
@@ -0,0 +1,38 @@
+(* Wildcard variables allows us to express "a peano number that is less than a constant" *)
+
+open OCanren
+open Tester
+
+let run_nat eta = run_r Std.Nat.reify (GT.show Std.Nat.logic) eta
+
+let of_int =
+  let rec helper acc n = if n > 0 then helper (Std.Nat.succ acc) (n - 1) else acc in
+  helper Std.Nat.zero
+;;
+
+(* q >= 2 *)
+let _ =
+  let open Std.Nat in
+  [%tester run_nat (-1) (fun q -> fresh v (q === succ (succ v)))]
+;;
+
+(* q <= 3 *)
+let le3 q =
+  let open Std.Nat in
+  q =/= succ (succ (succ __))
+;;
+
+(* 2 <= 3 *)
+let _ = [%tester run_nat (-1) (fun q -> fresh () (le3 q) (q === of_int 2))]
+
+(* 3 <= 3 *)
+let _ = [%tester run_nat (-1) (fun q -> fresh () (le3 q) (q === of_int 3))]
+
+(* 1 <= 3 *)
+let _ = [%tester run_nat (-1) (fun q -> fresh () (le3 q) (q === of_int 1))]
+
+(* 0 <= 3 *)
+let _ = [%tester run_nat (-1) (fun q -> fresh () (le3 q) (q === of_int 0))]
+
+(* not 4 <= 3 *)
+let _ = [%tester run_nat (-1) (fun q -> fresh () (le3 q) (q === of_int 4))]
diff --git a/test_wc/peano.t b/test_wc/peano.t
new file mode 100644
index 000000000..e60971d1f
--- /dev/null
+++ b/test_wc/peano.t
@@ -0,0 +1,17 @@
+  $ ./peano.exe
+  fun q -> fresh v (q === (succ (succ v))), all answers {
+  q=S (S (_.11));
+  }
+  fun q -> fresh () (le3 q) (q === (of_int 2)), all answers {
+  q=S (S (O));
+  }
+  fun q -> fresh () (le3 q) (q === (of_int 3)), all answers {
+  }
+  fun q -> fresh () (le3 q) (q === (of_int 1)), all answers {
+  q=S (O);
+  }
+  fun q -> fresh () (le3 q) (q === (of_int 0)), all answers {
+  q=O;
+  }
+  fun q -> fresh () (le3 q) (q === (of_int 4)), all answers {
+  }

From 9caa82f91d2f85aced9877cc6b4f78898aaffa7d Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Wed, 26 Apr 2023 16:07:23 +0300
Subject: [PATCH 04/11] update tests for nonrecursive fully abstract types

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 regression_ppx/dune                           |  31 ++++-
 regression_ppx/test015.t                      | 113 ++++++++++++------
 regression_ppx/test015mutual.ml               |   7 ++
 regression_ppx/test016.t                      |  36 ++++++
 .../{test015diseq.ml => test016diseq.ml}      |   0
 test_wc/debug_var.ml                          |  11 +-
 test_wc/dune                                  |   4 +-
 test_wc/match.ml                              |   6 +-
 8 files changed, 155 insertions(+), 53 deletions(-)
 create mode 100644 regression_ppx/test015mutual.ml
 create mode 100644 regression_ppx/test016.t
 rename regression_ppx/{test015diseq.ml => test016diseq.ml} (100%)

diff --git a/regression_ppx/dune b/regression_ppx/dune
index f702628f5..a26e35f5c 100644
--- a/regression_ppx/dune
+++ b/regression_ppx/dune
@@ -175,17 +175,27 @@
  (libraries OCanren OCanren.tester))
 
 (executables
- (names test015diseq)
- (modules test015diseq)
+ (names test015mutual)
+ (modules test015mutual)
+ (package OCanren)
+ (public_names -)
+ (preprocess
+  (pps OCanren-ppx.ppx_distrib GT.ppx_all -- -new-typenames -pretty))
+ (libraries OCanren OCanren.tester))
+
+(executables
+ (names test016diseq)
+ (modules test016diseq)
  (package OCanren)
  (public_names -)
  (preprocess
   (pps
+   OCanren-ppx.ppx_distrib
    OCanren-ppx.ppx_fresh
-   OCanren-ppx.ppx_deriving_reify
-   GT.ppx_all
    OCanren-ppx.ppx_repr
+   GT.ppx_all
    --
+   -new-typenames
    -pretty))
  (libraries OCanren OCanren.tester))
 
@@ -331,5 +341,14 @@
  (deps
   (package OCanren-ppx)
   %{project_root}/ppx/pp_ocanren_all.exe
-  test015diseq.ml
-  test015diseq.exe))
+  test015mutual.ml
+  test015mutual.exe))
+
+(cram
+ (package OCanren)
+ (applies_to test016)
+ (deps
+  (package OCanren-ppx)
+  %{project_root}/ppx/pp_ocanren_all.exe
+  test016diseq.ml
+  test016diseq.exe))
diff --git a/regression_ppx/test015.t b/regression_ppx/test015.t
index 3f690473d..637ee122e 100644
--- a/regression_ppx/test015.t
+++ b/regression_ppx/test015.t
@@ -1,35 +1,78 @@
-  $ ./test015diseq.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];
-  }
+
+  $ ./test015mutual.exe
+  test015
+
+  $ ../ppx/pp_ocanren_all.exe test015mutual.ml -pretty -new-typenames
+  let () = print_endline "test015"
+  module _ =
+    struct
+      include
+        struct
+          type nonrec 'a0 targ_fuly =
+            | Type of 'a0 [@@deriving gt ~options:{ show; gmap }]
+          type nonrec 'a0 jtype_fuly =
+            | Array of 'a0 [@@deriving gt ~options:{ show; gmap }]
+          type targ = jtype targ_fuly
+          and jtype = targ jtype_fuly[@@deriving gt ~options:{ show; gmap }]
+          type targ_logic = jtype_logic targ_fuly OCanren.logic
+          and jtype_logic = targ_logic jtype_fuly OCanren.logic[@@deriving
+                                                                 gt
+                                                                   ~options:
+                                                                   { show; gmap
+                                                                   }]
+          type targ_injected = jtype_injected targ_fuly OCanren.ilogic
+          and jtype_injected = targ_injected jtype_fuly OCanren.ilogic
+          let targ_fmapt f__005_ subj__006_ =
+            let open OCanren.Env.Monad in
+              ((OCanren.Env.Monad.return (GT.gmap targ_fuly)) <*> f__005_) <*>
+                subj__006_
+          let jtype_fmapt f__002_ subj__003_ =
+            let open OCanren.Env.Monad in
+              ((OCanren.Env.Monad.return (GT.gmap jtype_fuly)) <*> f__002_) <*>
+                subj__003_
+          include
+            struct
+              let rec __jtype fa0 =
+                let open OCanren.Env.Monad in
+                  OCanren.Reifier.fix
+                    (fun _ -> OCanren.prj_exn <..> (chain (jtype_fmapt fa0)))
+              and __targ fa0 =
+                let open OCanren.Env.Monad in
+                  OCanren.Reifier.fix
+                    (fun _ -> OCanren.prj_exn <..> (chain (targ_fmapt fa0)))
+              let fix =
+                let rec jtype_prj_exn eta = (__jtype targ_prj_exn) eta
+                and targ_prj_exn eta = (__targ jtype_prj_exn) eta in
+                (jtype_prj_exn, targ_prj_exn)
+              let jtype_prj_exn eta = let (f, _) = fix in f eta
+              let targ_prj_exn eta = let (_, f) = fix in f eta
+            end
+          include
+            struct
+              let rec __jtype fa0 =
+                let open OCanren.Env.Monad in
+                  OCanren.Reifier.fix
+                    (fun _ ->
+                       OCanren.reify <..>
+                         (chain
+                            (OCanren.Reifier.zed
+                               (OCanren.Reifier.rework ~fv:(jtype_fmapt fa0)))))
+              and __targ fa0 =
+                let open OCanren.Env.Monad in
+                  OCanren.Reifier.fix
+                    (fun _ ->
+                       OCanren.reify <..>
+                         (chain
+                            (OCanren.Reifier.zed
+                               (OCanren.Reifier.rework ~fv:(targ_fmapt fa0)))))
+              let fix =
+                let rec jtype_reify eta = (__jtype targ_reify) eta
+                and targ_reify eta = (__targ jtype_reify) eta in
+                (jtype_reify, targ_reify)
+              let jtype_reify eta = let (f, _) = fix in f eta
+              let targ_reify eta = let (_, f) = fix in f eta
+            end
+        end
+    end
+  $ ./test015mutual.exe
+  test015
diff --git a/regression_ppx/test015mutual.ml b/regression_ppx/test015mutual.ml
new file mode 100644
index 000000000..c8b8a372c
--- /dev/null
+++ b/regression_ppx/test015mutual.ml
@@ -0,0 +1,7 @@
+let () = print_endline "test015"
+
+module _ = struct
+  [%%ocanren_inject
+  type targ = Type of jtype
+  and jtype = Array of targ [@@deriving gt ~options:{ show; gmap }]]
+end
diff --git a/regression_ppx/test016.t b/regression_ppx/test016.t
new file mode 100644
index 000000000..20a4a9546
--- /dev/null
+++ b/regression_ppx/test016.t
@@ -0,0 +1,36 @@
+
+  $ ./test016diseq.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/test015diseq.ml b/regression_ppx/test016diseq.ml
similarity index 100%
rename from regression_ppx/test015diseq.ml
rename to regression_ppx/test016diseq.ml
diff --git a/test_wc/debug_var.ml b/test_wc/debug_var.ml
index 8b8d2671b..9f96c4160 100644
--- a/test_wc/debug_var.ml
+++ b/test_wc/debug_var.ml
@@ -9,18 +9,15 @@ let show_pairl = GT.show Pair.logic show_intl show_intl
 let run_pair eta = run_r (Pair.reify reify reify) show_pairl eta
 
 let trace_int q =
-  debug_var q (Fun.flip OCanren.reify) (fun xs ->
+  debug_var q OCanren.reify (fun xs ->
     Stdlib.List.iter (fun x -> print_endline @@ show_intl x) xs;
     success)
 ;;
 
 let trace_pair (q : (_, _) Pair.groundi) =
-  debug_var
-    q
-    (Fun.flip @@ Pair.reify reify reify)
-    (fun xs ->
-      Stdlib.List.iter (fun x -> print_endline @@ show_pairl x) xs;
-      success)
+  debug_var q (Pair.reify reify reify) (fun xs ->
+    Stdlib.List.iter (fun x -> print_endline @@ show_pairl x) xs;
+    success)
 ;;
 
 let _ = [%tester run_int (-1) (fun q -> trace_int q)]
diff --git a/test_wc/dune b/test_wc/dune
index 3a0056a9a..58e2891fc 100644
--- a/test_wc/dune
+++ b/test_wc/dune
@@ -8,7 +8,7 @@
  (modules main debug_var peano)
  (preprocess
   (pps
-   ppx_expect
+   ppx_expect_nobase
    OCanren-ppx.ppx_wildcard
    OCanren-ppx.ppx_repr
    OCanren-ppx.ppx_fresh
@@ -23,7 +23,7 @@
  (libraries OCanren OCanren.tester)
  (preprocess
   (pps
-   ppx_expect
+   ppx_expect_nobase
    OCanren-ppx.ppx_wildcard
    OCanren-ppx.ppx_repr
    OCanren-ppx.ppx_fresh
diff --git a/test_wc/match.ml b/test_wc/match.ml
index 08df7fd2b..0e7a5d7ff 100644
--- a/test_wc/match.ml
+++ b/test_wc/match.ml
@@ -171,8 +171,8 @@ module _ = struct
       (Pair.reify (Triple.reify OCanren.reify OCanren.reify OCanren.reify) OCanren.reify)
       ([%show:
          ( (GT.bool logic, GT.bool logic, GT.bool logic) Std.Triple.logic
-         , GT.int logic )
-         Std.Pair.logic]
+           , GT.int logic )
+           Std.Pair.logic]
          ())
       eta
   ;;
@@ -311,7 +311,7 @@ module _ = struct
           (q =/= w __ _F _T)
           (q =/= w _F _T __)
           (q =/= w __ __ _F)
-          (debug_var !!1 (Fun.flip OCanren.reify) (fun _ ->
+          (debug_var !!1 OCanren.reify (fun _ ->
              (* OCanren.set_diseq_logging true; *)
              success))
           (q === w __ __ _T)

From 5fb9303b98eac37905bfae8add9d24281f108bec Mon Sep 17 00:00:00 2001
From: Peter Lozov <not_kill@gmail.ru>
Date: Thu, 22 Jun 2023 04:21:17 +0300
Subject: [PATCH 05/11] Magic fix for disequality simplify exception.

---
 src/core/Subst.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/core/Subst.ml b/src/core/Subst.ml
index deda7e344..c80848283 100644
--- a/src/core/Subst.ml
+++ b/src/core/Subst.ml
@@ -172,8 +172,10 @@ let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
       | Var z, WC v | WC v, Var z -> extend (Obj.magic v) (Obj.repr z) acc
       | Value z, WC v | WC v, Value z -> extend (Obj.magic v) (Obj.repr z) acc
       | Var x, Var y ->
-        if Term.Var.equal x y then acc
-        else extend x (Term.repr y) acc
+          let cmp = Term.Var.compare x y in
+          if cmp < 0 then extend x (Term.repr y) acc
+          else if cmp > 0 then extend y (Term.repr x) acc
+          else acc
       | Var x, Value y -> extend x y acc
       | Value x, Var y -> extend y x acc
       | Value x, Value y  -> helper x y acc

From bbd083b93bd7501d05318d761b33577a266bac96 Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Thu, 20 Mar 2025 09:27:22 +0300
Subject: [PATCH 06/11] Apply OCamlformat 0.26.1

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 ppx/distrib/ppx_distrib_expander.ml | 62 ++++++++++++++---------------
 regression_ppx/dune                 |  2 +-
 test_wc/main.ml                     | 12 +++---
 test_wc/match.ml                    | 24 +++++------
 4 files changed, 50 insertions(+), 50 deletions(-)

diff --git a/ppx/distrib/ppx_distrib_expander.ml b/ppx/distrib/ppx_distrib_expander.ml
index 62e6d171d..76db250ae 100644
--- a/ppx/distrib/ppx_distrib_expander.ml
+++ b/ppx/distrib/ppx_distrib_expander.ml
@@ -787,36 +787,36 @@ let process_main ~loc rec_ (base_tdecl, tdecl) =
 ;;
 *)
 (* let prepare_reifiers (rs : Reifier_info.t list) =
-     let names = [] (* type params of original decl *) in
-     let mk_arg_reifier s = sprintf "r%s" s in
-     let add_args tdecl rhs =
-       let loc = tdecl.ptype_loc in
-       Exp.funs ~loc rhs (List.map ~f:mk_arg_reifier names)
-     in
-     match rs with
-     | [] -> []
-     | [ h ] ->
-         let loc = h.Reifier_info.decl.ptype_loc in
-         let pat = ppat_var ~loc (Located.mk ~loc h.Reifier_info.name) in
-         [ value_binding ~loc ~pat ~expr:(add_args h.Reifier_info.decl h.Reifier_info.body) ]
-     | rs ->
-         let mutual_names = List.map rs ~f:(fun { Reifier_info.decl } -> decl.ptype_name.txt) in
-         let mutual_args ~loc e =
-           pexp_fun
-             ~loc
-             nolabel
-             None
-             (ppat_tuple
+        let names = [] (* type params of original decl *) in
+        let mk_arg_reifier s = sprintf "r%s" s in
+        let add_args tdecl rhs =
+          let loc = tdecl.ptype_loc in
+          Exp.funs ~loc rhs (List.map ~f:mk_arg_reifier names)
+        in
+        match rs with
+        | [] -> []
+        | [ h ] ->
+            let loc = h.Reifier_info.decl.ptype_loc in
+            let pat = ppat_var ~loc (Located.mk ~loc h.Reifier_info.name) in
+            [ value_binding ~loc ~pat ~expr:(add_args h.Reifier_info.decl h.Reifier_info.body) ]
+        | rs ->
+            let mutual_names = List.map rs ~f:(fun { Reifier_info.decl } -> decl.ptype_name.txt) in
+            let mutual_args ~loc e =
+              pexp_fun
                 ~loc
-                (List.map mutual_names ~f:(fun name -> ppat_var ~loc (Located.mk ~loc name))))
-             e
-         in
-         List.concat
-           [ List.map rs ~f:(fun { Reifier_info.name; decl; body } ->
-                 let loc = decl.ptype_loc in
-                 let pat = ppat_var ~loc (Located.mk ~loc name) in
-                 value_binding ~loc ~pat ~expr:(mutual_args ~loc @@ add_args decl body))
-           ; List.concat_map rs ~f:(fun _ -> [])
-           ]
-   ;;
+                nolabel
+                None
+                (ppat_tuple
+                   ~loc
+                   (List.map mutual_names ~f:(fun name -> ppat_var ~loc (Located.mk ~loc name))))
+                e
+            in
+            List.concat
+              [ List.map rs ~f:(fun { Reifier_info.name; decl; body } ->
+                    let loc = decl.ptype_loc in
+                    let pat = ppat_var ~loc (Located.mk ~loc name) in
+                    value_binding ~loc ~pat ~expr:(mutual_args ~loc @@ add_args decl body))
+              ; List.concat_map rs ~f:(fun _ -> [])
+              ]
+      ;;
 *)
diff --git a/regression_ppx/dune b/regression_ppx/dune
index a26e35f5c..797e0d8af 100644
--- a/regression_ppx/dune
+++ b/regression_ppx/dune
@@ -136,7 +136,7 @@
  (public_names -)
  (flags
   (:standard
-   ;-dsource
+   -dsource
    ;
    ))
  (preprocess
diff --git a/test_wc/main.ml b/test_wc/main.ml
index e8113f896..d62632504 100644
--- a/test_wc/main.ml
+++ b/test_wc/main.ml
@@ -75,8 +75,8 @@ let _ =
         (a b)
         (q === pair a b)
         (* (debug_var a OCanren.reify (fun _ ->
-               let () = OCanren.set_diseq_logging true in
-               success)) *)
+           let () = OCanren.set_diseq_logging true in
+           success)) *)
         (q =/= pair !!1 __)
         (q === pair __ !!1))]
 ;;
@@ -86,7 +86,7 @@ let _ =
 let _ =
   [%tester
     run_pair (-1) (fun q ->
-      fresh (a b) (q =/= pair !!1 __) (* (q =/= pair __ !!1)  *) (q === pair a b))]
+      fresh (a b) (q =/= pair !!1 __) (* (q =/= pair __ !!1) *) (q === pair a b))]
 ;;
 
 let _ =
@@ -187,8 +187,8 @@ let _ =
         (Std.pair x !!1 =/= Std.pair !!2 y)
         (x === !!2)
         (* (debug_var x OCanren.reify (fun _ ->
-               let () = OCanren.set_diseq_logging true in
-               trace_diseq_constraints)) *)
+           let () = OCanren.set_diseq_logging true in
+           trace_diseq_constraints)) *)
         (y === !!9)
         (Std.pair x y === q))]
 ;;
@@ -283,7 +283,7 @@ module _ = struct
         fresh
           www
           (Std.pair (le !!"one" !!"x") (le !!"one" !!"x")
-          =/= Std.pair (le __ www) (le __ www))
+           =/= Std.pair (le __ www) (le __ www))
         (* gives an answer, bvecause it simplifies to www=/= "x" *))]
   ;;
 end
diff --git a/test_wc/match.ml b/test_wc/match.ml
index 0e7a5d7ff..2807ad86b 100644
--- a/test_wc/match.ml
+++ b/test_wc/match.ml
@@ -96,8 +96,8 @@ module _ = struct
           (fresh (l r) (scru === (Std.pair l r))
              (if explicit then (bool_dom l) &&& (bool_dom r) else success)), all answers {
       q=((true, _.16), 1);
-      q=((_.17, _.18 [=/= _.13]), 2);
       q=((_.17 [=/= true], _.18), 2);
+      q=((_.17, _.18), 2);
       } |}]
   ;;
 
@@ -238,12 +238,12 @@ module _ = struct
           (if explicit
            then ((bool_dom l) &&& (bool_dom m)) &&& (bool_dom r)
            else success), all answers {
-      q=((_.13, false, true), 1);
-      q=((false, true, _.15), 2);
-      q=((_.13, _.14 [=/= true], false), 3);
-      q=((_.13, _.14 [=/= false; =/= true], true), 4);
-      q=((_.13 [=/= false], _.14, false), 3);
-      q=((_.13 [=/= false], _.14 [=/= false], true), 4);
+      q=((_.16, false, true), 1);
+      q=((false, true, _.17), 2);
+      q=((_.18, _.19 [=/= true], false), 3);
+      q=((_.20, _.21 [=/= false; =/= true], true), 4);
+      q=((_.18 [=/= false], _.19, false), 3);
+      q=((_.20 [=/= false], _.21 [=/= false], true), 4);
       } |}]
   ;;
 
@@ -275,11 +275,11 @@ module _ = struct
           (if explicit
            then ((bool_dom l) &&& (bool_dom m)) &&& (bool_dom r)
            else success), all answers {
-      q=((_.13, false, true), 1);
-      q=((false, true, _.15), 2);
-      q=((_.13, _.14, false), 3);
-      q=((_.13, _.14 [=/= false], true), 4);
-      q=((_.13 [=/= _.21], _.14, true), 4);
+      q=((_.17, false, true), 1);
+      q=((false, true, _.20), 2);
+      q=((_.26, _.27, false), 3);
+      q=((_.24, _.25 [=/= false], true), 4);
+      q=((_.24, _.25, true), 4);
       } |}]
   ;;
 

From 0976966645b3f23f96751616c0ecc43587880b0b Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Thu, 20 Mar 2025 09:27:34 +0300
Subject: [PATCH 07/11] Promote tests

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 regression/test002.t     |  6 +++---
 regression/test005.t     |  8 ++++----
 regression/test006.t     |  4 ++--
 regression/test011.t     |  4 ++--
 regression/test014.t     | 18 +++++++++---------
 regression_ppx/test016.t |  8 ++++----
 test_wc/main.t           |  2 +-
 7 files changed, 25 insertions(+), 25 deletions(-)

diff --git a/regression/test002.t b/regression/test002.t
index c3abc17ab..99ef14d02 100644
--- a/regression/test002.t
+++ b/regression/test002.t
@@ -1,7 +1,7 @@
   $ ./test002sort.exe
-  [O; O; _.138]
-  [O; O; _.136 [=/= O]]
-  [O; O; _.153 [=/= O]]
+  [O; O; _.140]
+  [O; O; _.140 [=/= O]]
+  [O; O; _.157 [=/= 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
index 85d225fd7..dbb8b0a52 100644
--- 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 (_.18, _.18);
+  q=Arr (_.21, _.21);
   }
   fun q -> infero (abs varF (abs varX (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (Arr (_.30, _.26), Arr (_.30, _.26));
+  q=Arr (Arr (_.54, _.26), Arr (_.54, _.26));
   }
   fun q -> infero (abs varX (abs varF (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (_.30, Arr (Arr (_.30, _.26), _.26));
+  q=Arr (_.64, Arr (Arr (_.64, _.26), _.26));
   }
   fun q -> infero q (arr (p varX) (p varX)), 1 answer {
-  q=Abs (_.29, V (_.29));
+  q=Abs (_.30, V (_.30));
   }
diff --git a/regression/test006.t b/regression/test006.t
index f56d607c5..1d0e4012a 100644
--- 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 (_.44, V (_.44));
+  q=Abs (_.59, V (_.59));
   }
   fun q r -> evalo (app r q) (v varX), 1 answer {
-  q=V ("x"); r=Abs (_.54, V (_.54));
+  q=V ("x"); r=Abs (_.68, V (_.68));
   }
   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
index a4a7a1533..43190636f 100644
--- 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 [=/= _.11]];
+  q=[_.11 [=/= _.12]; _.12];
   }
   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 [=/= _.11]; 2];
+  q=[_.12; 2];
   }
   fun q -> distincto (!2 % (!3 %< q)), all answers {
   q=_.35 [=/= 2; =/= 3];
diff --git a/regression/test014.t b/regression/test014.t
index c1f784a21..8c5cbfb05 100644
--- 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=[_.28; _.33 | _.34]; s=[0; _.28; _.33 | _.34];
-  q=[0; 0; 1]; r=[_.69; _.76 | _.77]; s=[0; 0; _.69; _.76 | _.77];
+  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=[1; _.102 | _.103]; r=[0; 1]; s=[0; 1; _.102 | _.103];
-  q=[0; 0; 0; 1]; r=[_.149; _.164 | _.165]; s=[0; 0; 0; _.149; _.164 | _.165];
+  q=[0; 0; 0; 1]; r=[_.207; _.164 | _.165]; s=[0; 0; 0; _.207; _.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=[_.314; _.343 | _.344]; s=[0; 0; 0; 0; _.314; _.343 | _.344];
+  q=[0; 0; 0; 0; 1]; r=[_.437; _.343 | _.344]; s=[0; 0; 0; 0; _.437; _.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=[_.656; _.713 | _.714]; s=[0; 0; 0; 0; 0; _.656; _.713 | _.714];
+  q=[0; 0; 0; 0; 0; 1]; r=[_.904; _.713 | _.714]; s=[0; 0; 0; 0; 0; _.904; _.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=[_.1360; _.1493 | _.1494]; s=[0; 0; 0; 0; 0; 0; _.1360; _.1493 | _.1494];
+  q=[0; 0; 0; 0; 0; 0; 1]; r=[_.1860; _.1493 | _.1494]; s=[0; 0; 0; 0; 0; 0; _.1860; _.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; _.225; 1]; r=[0; 1; _.225; 1];
+  q=[1; _.653; 1]; r=[0; 1; _.653; 1];
   q=[0; 0; 1]; r=[0; 0; 0; 1];
   q=[0; 1; 1]; r=[0; 0; 1; 1];
-  q=[1; _.247; _.408; 1]; r=[0; 1; _.247; _.408; 1];
-  q=[0; 1; _.408; 1]; r=[0; 0; 1; _.408; 1];
+  q=[1; _.1001; _.408; 1]; r=[0; 1; _.1001; _.408; 1];
+  q=[0; 1; _.1243; 1]; r=[0; 0; 1; _.1243; 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/test016.t b/regression_ppx/test016.t
index 20a4a9546..fa2e69432 100644
--- a/regression_ppx/test016.t
+++ b/regression_ppx/test016.t
@@ -8,16 +8,16 @@
   
   11: { 0: [|  11 =/= boxed 0 <_.12, _.13> |] }
   
-  15: { 0: [|  14 =/= _.12,  15 =/= _.13 |] }
+  13: { 0: [|  12 =/= _.14,  13 =/= _.15 |] }
   
    hd2 === 1
-  15: { 0: [|  14 =/= _.12,  15 =/= _.13 |] }
+  13: { 0: [|  12 =/= _.14,  13 =/= _.15 |] }
   
    tl2 === []
-  13: { 0: [|  12 =/= int<1>,  13 =/= int<0> |] }
+  13: { 0: [|  12 =/= _.14,  13 =/= _.15 |] }
   
   47
-  13: { 0: [|  12 =/= int<1>,  13 =/= int<0> |] }
+  13: { 0: [|  12 =/= _.14,  13 =/= _.15 |] }
   
   }
   fun _ ->
diff --git a/test_wc/main.t b/test_wc/main.t
index 7cda37b0d..c20ed44b1 100644
--- a/test_wc/main.t
+++ b/test_wc/main.t
@@ -47,7 +47,7 @@
   fun q ->
     fresh (a b) (q =/= (pair (!! 1) __)) (q === (pair __ (!! 1)))
       (q === (pair a b)), all answers {
-  q=(_.11 [=/= 1], 1);
+  q=(_.13 [=/= 1], 1);
   }
   fun q -> fresh () (q === ((!! 1) % ((!! 2) % __))) (q === (__ % __)), all answers {
   q=[1; 2 | _.11];

From 06e48e670ed5d95838c1e884268dcd661ba6cf44 Mon Sep 17 00:00:00 2001
From: "Dmitrii.Kosarev a.k.a. Kakadu" <Kakadu@pm.me>
Date: Tue, 17 Dec 2024 18:00:22 +0300
Subject: [PATCH 08/11] [chore] Promote tests

Signed-off-by: Dmitrii.Kosarev a.k.a. Kakadu <Kakadu@pm.me>
---
 test_wc/match.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/test_wc/match.ml b/test_wc/match.ml
index 2807ad86b..cac89ab3a 100644
--- a/test_wc/match.ml
+++ b/test_wc/match.ml
@@ -45,13 +45,6 @@ module _ = struct
              (if explicit then bool_dom l &&& bool_dom r else success)))]
   ;;
 
-  let naive_rel q rez =
-    conde
-      [ fresh () (q === Std.pair !!true __) (rez === !!1)
-      ; fresh temp (q =/= Std.pair !!true temp) (rez === !!2)
-      ]
-  ;;
-
   let%expect_test "Without disequalities at all" =
     let xxx q rez =
       conde
@@ -85,6 +78,13 @@ module _ = struct
       } |}]
   ;;
 
+  let naive_rel q rez =
+    conde
+      [ fresh () (q === Std.pair !!true __) (rez === !!1)
+      ; fresh temp (q =/= Std.pair !!true temp) (rez === !!2)
+      ]
+  ;;
+
   let%expect_test " " =
     print_endline "Naive with diseq constraints (6 answers instead of 4): ";
     test ~explicit:false naive_rel;

From fa9fc9b4fec4a64ce6cffdbe20624153541b8164 Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Mon, 3 Mar 2025 18:37:06 +0300
Subject: [PATCH 09/11] Demo where __ =/= term with __ inside

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 test_wc/peano.ml | 3 +++
 test_wc/peano.t  | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/test_wc/peano.ml b/test_wc/peano.ml
index 9d8877845..b6e81b1ed 100644
--- a/test_wc/peano.ml
+++ b/test_wc/peano.ml
@@ -36,3 +36,6 @@ let _ = [%tester run_nat (-1) (fun q -> fresh () (le3 q) (q === of_int 0))]
 
 (* not 4 <= 3 *)
 let _ = [%tester run_nat (-1) (fun q -> fresh () (le3 q) (q === of_int 4))]
+
+(* Questionable case *)
+let _ = [%tester run_nat (-1) (fun q -> __ =/= Std.Nat.(succ (succ __)))]
diff --git a/test_wc/peano.t b/test_wc/peano.t
index e60971d1f..d15510ba1 100644
--- a/test_wc/peano.t
+++ b/test_wc/peano.t
@@ -15,3 +15,5 @@
   }
   fun q -> fresh () (le3 q) (q === (of_int 4)), all answers {
   }
+  fun q -> __ =/= (let open Std.Nat in succ (succ __)), all answers {
+  }

From 06c1beb366fa48df5cf72b1d6fdc989de856e820 Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Tue, 4 Mar 2025 12:07:32 +0300
Subject: [PATCH 10/11] A few wildcard tests

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 test_wc/peano.ml | 5 ++++-
 test_wc/peano.t  | 4 +++-
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/test_wc/peano.ml b/test_wc/peano.ml
index b6e81b1ed..68bf7a147 100644
--- a/test_wc/peano.ml
+++ b/test_wc/peano.ml
@@ -38,4 +38,7 @@ let _ = [%tester run_nat (-1) (fun q -> fresh () (le3 q) (q === of_int 0))]
 let _ = [%tester run_nat (-1) (fun q -> fresh () (le3 q) (q === of_int 4))]
 
 (* Questionable case *)
-let _ = [%tester run_nat (-1) (fun q -> __ =/= Std.Nat.(succ (succ __)))]
+let _ = [%tester run_nat (-1) (fun _ -> __ =/= Std.Nat.(succ (succ __)))]
+
+(* Obvious case *)
+let _ = [%tester run_nat (-1) (fun _ -> __ =/= Std.Nat.(succ (succ zero)))]
diff --git a/test_wc/peano.t b/test_wc/peano.t
index d15510ba1..954f13eb8 100644
--- a/test_wc/peano.t
+++ b/test_wc/peano.t
@@ -15,5 +15,7 @@
   }
   fun q -> fresh () (le3 q) (q === (of_int 4)), all answers {
   }
-  fun q -> __ =/= (let open Std.Nat in succ (succ __)), all answers {
+  fun _ -> __ =/= (let open Std.Nat in succ (succ __)), all answers {
+  }
+  fun _ -> __ =/= (let open Std.Nat in succ (succ zero)), all answers {
   }

From 98e15bb13bc443afb0dc844679315f90ac645914 Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Wed, 19 Mar 2025 21:46:07 +0300
Subject: [PATCH 11/11] tests: Disable -dsource in regression_ppx

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 regression_ppx/dune | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/regression_ppx/dune b/regression_ppx/dune
index 797e0d8af..e2cc4b47c 100644
--- a/regression_ppx/dune
+++ b/regression_ppx/dune
@@ -134,11 +134,6 @@
  (modules test012mutual)
  (package OCanren)
  (public_names -)
- (flags
-  (:standard
-   -dsource
-   ;
-   ))
  (preprocess
   (pps OCanren-ppx.ppx_distrib GT.ppx_all -- -new-typenames -pretty))
  (libraries OCanren OCanren.tester))