reify_in_state, is_ground, is_ground_bool (needed for JGS)

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

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

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

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]
  *)