[obligations] Step towards more structured handling of remaining obligations.

There is a lot of check overhead in the code, we will try to provide a
more convenient API for manipulation of remaining obligations.

4 files changed, 30 insertions, 22 deletions

diff --git a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
index c87c3f7f0f..6928925e54 100644
--- a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
+++ b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
@@ -6,4 +6,7 @@ if [ "$CI_PULL_REQUEST" = "11731" ] || [ "$CI_BRANCH" = "proof+more_naming_unif"
     rewriter_CI_REF=proof+more_naming_unif
     rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
 
+    elpi_CI_REF=proof+more_naming_unif
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
 fi
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index f12ae0804a..626dcd5d34 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -33,7 +33,9 @@ module Obligation = struct
 
 end
 
-type obligations = Obligation.t array * int
+type obligations =
+  { obls : Obligation.t array
+  ; remaining : int }
 
 type fixpoint_kind =
   | IsFixpoint of lident option list
@@ -88,7 +90,7 @@ module ProgramDecl = struct
     ; prg_type = reduce t
     ; prg_ctx = ctx
     ; prg_univdecl = udecl
-    ; prg_obligations = (obls', Array.length obls')
+    ; prg_obligations = { obls = obls' ; remaining = Array.length obls' }
     ; prg_deps = deps
     ; prg_fixkind = fixkind
     ; prg_notations = notations
@@ -287,7 +289,7 @@ let progmap_add n prg =
 let progmap_replace prg' =
   Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
 
-let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0
+let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0
 
 let obligations_message rem =
   if rem > 0 then
@@ -327,7 +329,7 @@ let rec intset_to = function
   | n -> Int.Set.add n (intset_to (pred n))
 
 let obligation_substitution expand prg =
-  let obls, _ = prg.prg_obligations in
+  let obls = prg.prg_obligations.obls in
   let ints = intset_to (pred (Array.length obls)) in
   obl_substitution expand obls ints
 
@@ -503,7 +505,8 @@ let declare_mutual_definition l =
   dref
 
 let update_obls prg obls rem =
-  let prg' = {prg with prg_obligations = (obls, rem)} in
+  let prg_obligations = { obls; remaining = rem } in
+  let prg' = {prg with prg_obligations} in
   progmap_replace prg';
   obligations_message rem;
   if rem > 0 then Remain rem
@@ -564,7 +567,7 @@ let obligation_terminator entries uctx { name; num; auto } =
     let body = EConstr.to_constr sigma (EConstr.of_constr body) in
     let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
     let ctx = Evd.evar_universe_context sigma in
-    let obls, rem = prg.prg_obligations in
+    let { obls; remaining=rem } = prg.prg_obligations in
     let obl = obls.(num) in
     let status =
       match obl.obl_status, entry.Declare.proof_entry_opaque with
@@ -606,7 +609,7 @@ let obligation_terminator entries uctx { name; num; auto } =
 (* Similar to the terminator but for interactive paths, as the
    terminator is only called in interactive proof mode *)
 let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } =
-  let obls, rem = prg.prg_obligations in
+  let { obls; remaining=rem } = prg.prg_obligations in
   let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in
   let transparent = evaluable_constant cst (Global.env ()) in
   let () = match obl.obl_status with
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index c2bd0595fa..4e20c7c192 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -29,7 +29,9 @@ module Obligation : sig
 
 end
 
-type obligations = Obligation.t array * int
+type obligations =
+  { obls : Obligation.t array
+  ; remaining : int }
 
 type fixpoint_kind =
   | IsFixpoint of lident option list
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a9d43e851d..f449cb02f1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -297,7 +297,7 @@ open Evd
 let map_cardinal m =
   let i = ref 0 in
   ProgMap.iter (fun _ v ->
-      if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m;
+      if (CEphemeron.get v).prg_obligations.remaining > 0 then incr i) m;
   !i
 
 exception Found of ProgramDecl.t CEphemeron.key
@@ -305,8 +305,8 @@ exception Found of ProgramDecl.t CEphemeron.key
 let map_first m =
   try
     ProgMap.iter (fun _ v ->
-                  if snd (CEphemeron.get v).prg_obligations > 0 then
-                    raise (Found v)) m;
+        if (CEphemeron.get v).prg_obligations.remaining > 0 then
+          raise (Found v)) m;
     assert(false)
   with Found x -> x
 
@@ -395,7 +395,7 @@ let solve_by_tac ?loc name evi t poly uctx =
 
 let rec solve_obligation prg num tac =
   let user_num = succ num in
-  let obls, rem = prg.prg_obligations in
+  let { obls; remaining=rem } = prg.prg_obligations in
   let obl = obls.(num) in
   let remaining = deps_remaining obls obl.obl_deps in
   let () =
@@ -423,7 +423,7 @@ let rec solve_obligation prg num tac =
 and obligation (user_num, name, typ) tac =
   let num = pred user_num in
   let prg = get_prog_err name in
-  let obls, rem = prg.prg_obligations in
+  let { obls; remaining } = prg.prg_obligations in
     if num >= 0 && num < Array.length obls then
       let obl = obls.(num) in
         match obl.obl_body with
@@ -468,8 +468,8 @@ and solve_obligation_by_tac prg obls i tac =
       else None
 
 and solve_prg_obligations prg ?oblset tac =
-  let obls, rem = prg.prg_obligations in
-  let rem = ref rem in
+  let { obls; remaining } = prg.prg_obligations in
+  let rem = ref remaining in
   let obls' = Array.copy obls in
   let set = ref Int.Set.empty in
   let p = match oblset with
@@ -501,10 +501,10 @@ and solve_all_obligations tac =
 
 and try_solve_obligation n prg tac =
   let prg = get_prog prg in
-  let obls, rem = prg.prg_obligations in
+  let {obls; remaining } = prg.prg_obligations in
   let obls' = Array.copy obls in
     match solve_obligation_by_tac prg obls' n tac with
-    | Some prg' -> ignore(update_obls prg' obls' (pred rem))
+    | Some prg' -> ignore(update_obls prg' obls' (pred remaining))
     | None -> ()
 
 and try_solve_obligations n tac =
@@ -517,9 +517,9 @@ and auto_solve_obligations n ?oblset tac : progress =
 open Pp
 let show_obligations_of_prg ?(msg=true) prg =
   let n = prg.prg_name in
-  let obls, rem = prg.prg_obligations in
+  let {obls; remaining} = prg.prg_obligations in
   let showed = ref 5 in
-    if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: ");
+    if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: ");
     Array.iteri (fun i x ->
                    match x.obl_body with
                    | None ->
@@ -557,7 +557,7 @@ let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl)
     ?(reduce=reduce) ?hook ?(opaque = false) obls =
   let info = Id.print name ++ str " has type-checked" in
   let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in
-  let obls,_ = prg.prg_obligations in
+  let {obls;_} = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
     let cst = DeclareObl.declare_definition prg in
@@ -594,7 +594,7 @@ let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic
     in ()
 
 let admit_prog prg =
-  let obls, rem = prg.prg_obligations in
+  let {obls; remaining} = prg.prg_obligations in
   let obls = Array.copy obls in
     Array.iteri
       (fun i x ->
@@ -631,7 +631,7 @@ let next_obligation n tac =
   | None -> get_any_prog_err ()
   | Some _ -> get_prog_err n
   in
-  let obls, rem = prg.prg_obligations in
+  let {obls; remaining} = prg.prg_obligations in
   let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
   let i = match Array.findi is_open obls with
   | Some i -> i