From 3e9f0e7eefda1e1df3b5ef33f855f982b660f2ee Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Thu, 24 Jul 2025 19:18:17 +0300
Subject: [PATCH] reify_in_state, is_ground, is_ground_bool (needed for JGS)

Helper functions that are useful when environment variable
OCANREN_NON_ABSTRACT_GOAL is set

Signed-off-by: Kakadu <Kakadu@pm.me>
---
 src/core/Core.ml  | 17 +++++++++++++++++
 src/core/Core.mli |  9 +++++++++
 src/core/Term.ml  |  6 ++++++
 src/core/Term.mli |  2 ++
 4 files changed, 34 insertions(+)

diff --git a/src/core/Core.ml b/src/core/Core.ml
index 9a910a12..aa8903cf 100644
--- a/src/core/Core.ml
+++ b/src/core/Core.ml
@@ -800,3 +800,20 @@ let trace_diseq : goal = fun st ->
   Format.printf "%a\n%!" Disequality.pp (State.constraints st) ;
   success st
 
+IFDEF NON_ABSTRACT_GOAL THEN
+let reify_in_state st reifier x =
+  let env = State.env st in
+  let subst = State.subst st in
+  reifier (State.env st) (Subst.reify env subst x |> Obj.magic)
+
+let is_ground v st cb =
+  let ans = Subst.reify (State.env st) (State.subst st) v in
+  cb (not(Term.is_var ans))
+
+let is_ground_bool
+  : bool ilogic -> State.t -> onvar:(unit->unit) -> on_ground:(bool -> unit) -> unit =
+  fun v st ~onvar ~on_ground ->
+    let ans = Subst.reify (State.env st) (State.subst st) (Obj.magic v) in
+    if (Term.is_var ans) then onvar()
+    else on_ground (Obj.magic ans : bool)
+END
\ No newline at end of file
diff --git a/src/core/Core.mli b/src/core/Core.mli
index 9fb329bd..258822df 100644
--- a/src/core/Core.mli
+++ b/src/core/Core.mli
@@ -330,3 +330,12 @@ end
 val reify_in_empty: ('a, 'b) Reifier.t -> 'a -> 'b
 
 val trace_diseq: goal
+
+IFDEF NON_ABSTRACT_GOAL THEN
+val reify_in_state: State.t -> ('a, 'b) Reifier.t -> 'a -> 'b
+
+val is_ground : 'a ilogic -> State.t -> (bool -> unit) -> unit
+
+val is_ground_bool : bool ilogic -> State.t -> onvar:(unit->unit) -> on_ground:(bool -> unit) -> unit
+
+END
\ No newline at end of file
diff --git a/src/core/Term.ml b/src/core/Term.ml
index e4bb001f..75e0a164 100644
--- a/src/core/Term.ml
+++ b/src/core/Term.ml
@@ -123,6 +123,12 @@ let is_box t =
   t <= Obj.last_non_constant_constructor_tag &&
   t >= Obj.first_non_constant_constructor_tag
 
+let is_var x =
+  let x = Obj.repr x in
+  let tx = Obj.tag x in
+  is_box tx && Var.has_var_structure tx (Obj.size x) x
+;;
+
 let is_int = (=) Obj.int_tag
 let is_str = (=) Obj.string_tag
 let is_dbl = (=) Obj.double_tag
diff --git a/src/core/Term.mli b/src/core/Term.mli
index 5c6a9038..ca3c75c3 100644
--- a/src/core/Term.mli
+++ b/src/core/Term.mli
@@ -81,6 +81,8 @@ val pp : Format.formatter -> t -> unit
 (* [var x] if [x] is logic variable returns it, otherwise returns [None] *)
 val var : 'a -> Var.t option
 
+val is_var: 'a -> bool
+
 (* [map ~fvar ~fval x] map over OCaml's value extended with logic variables;
  *   handles primitive types with the help of [fval] and logic variables with the help of [fvar]
  *)