[program] extend obligation to give back a mapping from obligations to

terms

This is necessary for programs like Equations that call add_definition
and want to later update in their hook some separate datastructures
which refer to the obligations that are defined by Program. We give back
a map from obligation name to a constr defined in the program's universe
state which the hook returns as well. (Obligation names also correspond
to undefined evars in the original terms through
Obligations.eterm_obligations).

Using this, I can avoid ucontext_of_aucontext in Equations, allowing PR
 #8601 to go through.

5 files changed, 45 insertions, 37 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 84ffb84206..f4b0015851 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -149,7 +149,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
 let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype =
   let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
   if program_mode then
-    let hook _ vis gr =
+    let hook _ _ vis gr =
       let cst = match gr with ConstRef kn -> kn | _ -> assert false in
       Impargs.declare_manual_implicits false gr ~enriching:false [imps];
       let pri = intern_info pri in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index cc03473bc6..472411ac3a 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -109,7 +109,7 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
         Obligations.eterm_obligations env ident evd 0 c typ
       in
       let ctx = Evd.evar_universe_context evd in
-      let hook = Obligations.mk_univ_hook (fun _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in
+      let hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in
       ignore(Obligations.add_definition
           ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index fe8ef1f0e0..3d3d825bd0 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -193,7 +193,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       let name = add_suffix recname "_func" in
       (* XXX: Mutating the evar_map in the hook! *)
       (* XXX: Likely the sigma is out of date when the hook is called .... *)
-      let hook sigma _ l gr =
+      let hook sigma _ _ l gr =
         let sigma, h_body = Evarutil.new_global sigma gr in
         let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
@@ -212,7 +212,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       hook, name, typ
     else
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook sigma _ l gr =
+      let hook sigma _ _ l gr =
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5c1384fba7..97ed43c5f4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,10 +20,10 @@ open Pp
 open CErrors
 open Util
 
-type univ_declaration_hook = UState.t -> Decl_kinds.locality -> GlobRef.t -> unit
+type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
 let mk_univ_hook f = f
-let call_univ_hook fix_exn hook uctx l c =
-  try hook uctx l c
+let call_univ_hook fix_exn hook uctx trans l c =
+  try hook uctx trans l c
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
     iraise (fix_exn e)
@@ -415,16 +415,6 @@ let replace_appvars subst =
 	with Not_found -> Constr.map aux c
       else Constr.map aux c
   in Constr.map aux
-       
-let subst_prog expand obls ints prg =
-  let subst = obl_substitution expand obls ints in
-    if get_hide_obligations () then
-      (replace_appvars subst prg.prg_body,
-       replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type))
-    else 
-      let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
-	(Vars.replace_vars subst' prg.prg_body,
-	 Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type))
 
 let subst_deps_obl obls obl =
   let t' = subst_deps true obls obl.obl_deps obl.obl_type in
@@ -471,19 +461,30 @@ let rec intset_to = function
     -1 -> Int.Set.empty
   | n -> Int.Set.add n (intset_to (pred n))
 
-let subst_body expand prg =
+let subst_prog subst prg =
+  if get_hide_obligations () then
+    (replace_appvars subst prg.prg_body,
+     replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type))
+  else
+    let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
+    (Vars.replace_vars subst' prg.prg_body,
+     Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type))
+
+let obligation_substitution expand prg =
   let obls, _ = prg.prg_obligations in
   let ints = intset_to (pred (Array.length obls)) in
-    subst_prog expand obls ints prg
+  obl_substitution expand obls ints
 
 let declare_definition prg =
-  let body, typ = subst_body true prg in
+  let varsubst = obligation_substitution true prg in
+  let body, typ = subst_prog varsubst prg in
   let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
     (UState.subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
   let fix_exn = Hook.get get_fix_exn () in
   let typ = nf typ in
   let body = nf body in
+  let obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in
   let uvars = Univ.LSet.union
       (Vars.universes_of_constr typ)
       (Vars.universes_of_constr body) in
@@ -494,7 +495,7 @@ let declare_definition prg =
   let ubinders = UState.universe_binders uctx in
   DeclareDef.declare_definition prg.prg_name
     prg.prg_kind ce ubinders prg.prg_implicits
-    (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx l r ; ()))
+    (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx obls l r ; ()))
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -522,19 +523,26 @@ let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constant
 let declare_mutual_definition l =
   let len = List.length l in
   let first = List.hd l in
-  let fixdefs, fixtypes, fiximps =
-    List.split3
-      (List.map (fun x -> 
-	let subs, typ = (subst_body true x) in
-        let env = Global.env () in
-        let sigma = Evd.from_ctx x.prg_ctx in
-        let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
-        let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
-        let term = EConstr.to_constr sigma term in
-        let typ = EConstr.to_constr sigma typ in
-	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
+  let defobl x =
+    let oblsubst = obligation_substitution true x in
+    let subs, typ = subst_prog oblsubst x in
+    let env = Global.env () in
+    let sigma = Evd.from_ctx x.prg_ctx in
+    let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
+    let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
+    let term = EConstr.to_constr sigma term in
+    let typ = EConstr.to_constr sigma typ in
+    let def = (x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) in
+    let oblsubst = List.map (fun (id, (_, c)) -> id, c) oblsubst in
+    def, oblsubst
+  in
+  let defs, obls =
+    List.fold_right (fun x (defs, obls) ->
+        let xdef, xobls = defobl x in
+        (xdef :: defs, xobls @ obls)) l ([], [])
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
+  let fixdefs, fixtypes, fiximps = List.split3 defs in
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
@@ -568,7 +576,7 @@ let declare_mutual_definition l =
     List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
-    call_univ_hook fix_exn first.prg_hook first.prg_ctx local gr;
+    call_univ_hook fix_exn first.prg_hook first.prg_ctx obls local gr;
     List.iter progmap_remove l; gr
 
 let decompose_lam_prod c ty =
@@ -1105,7 +1113,7 @@ let show_term n =
 
 let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
                    ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
+    ?(reduce=reduce) ?(hook=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) obls =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let info = Id.print n ++ str " has type-checked" in
   let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in
@@ -1125,7 +1133,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
 
 let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
                            ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
+    ?(hook=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) notations fixkind =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 80294c7a76..57040b3f7c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -14,8 +14,8 @@ open Evd
 open Names
 
 type univ_declaration_hook
-val mk_univ_hook : (UState.t -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook
-val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> Decl_kinds.locality -> GlobRef.t -> unit
+val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook
+val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
 
 (* This is a hack to make it possible for Obligations to craft a Qed
  * behind the scenes.  The fix_exn the Stm attaches to the Future proof