[micromega/zify] expose more API for plugin users

4 files changed, 31 insertions, 2 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 542b99075d..a8f88df079 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -12,7 +12,7 @@
 (*                                                                      *)
 (* ** Toplevel definition of tactics **                                 *)
 (*                                                                      *)
-(* - Modules M, Mc, Env, Cache, CacheZ                                  *)
+(* - Modules Mc, Env, Cache, CacheZ                                  *)
 (*                                                                      *)
 (*  Frédéric Besson (Irisa/Inria) 2006-2019                             *)
 (*                                                                      *)
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index f59d65085a..bd47ccae8b 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -534,7 +534,7 @@ type ('a, 'b) hitkind =
 
 let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) =
   let n, r = Vect.decomp_cst v in
-  let fn = frac_num n in
+  let fn = frac_num (Q.abs n) in
   if fn =/ Q.zero then Forget (* The solution is integral *)
   else
     (* The cut construction is from:
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 917961fdcd..d1403558ad 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -1070,6 +1070,28 @@ let pp_trans_expr env evd e res =
     Feedback.msg_debug Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res);
   res
 
+let declared_term env evd hd args =
+  let match_operator (t, d) =
+    let decomp t i =
+      let n = Array.length args in
+      let t' = EConstr.mkApp (hd, Array.sub args 0 (n - i)) in
+      if is_convertible env evd t' t then Some (t, Array.sub args (n - i) i)
+      else None
+    in
+    match t with
+    | OtherTerm t -> ( match d with InjTyp _ -> None | _ -> Some (t, args) )
+    | Application t -> (
+      match d with
+      | CstOp _ -> decomp t 0
+      | UnOp _ -> decomp t 1
+      | BinOp _ -> decomp t 2
+      | BinRel _ -> decomp t 2
+      | PropOp _ -> decomp t 2
+      | PropUnOp _ -> decomp t 1
+      | _ -> None )
+  in
+  find_option match_operator (HConstr.find_all hd !table)
+
 let rec trans_expr env evd e =
   let inj = e.inj in
   let e = e.constr in
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
index 537e652fd0..555bb4c7fb 100644
--- a/plugins/micromega/zify.mli
+++ b/plugins/micromega/zify.mli
@@ -31,3 +31,10 @@ val iter_specs : unit Proofview.tactic
 val assert_inj : EConstr.constr -> unit Proofview.tactic
 val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic
 val elim_let : unit Proofview.tactic
+
+val declared_term :
+     Environ.env
+  -> Evd.evar_map
+  -> EConstr.t
+  -> EConstr.t array
+  -> EConstr.constr * EConstr.t array