diff options
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 545 |
1 files changed, 36 insertions, 509 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 4a564e705e..98dec7930c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1,8 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Printf -open Libobject open Entries open Decl_kinds -open Declare (** - Get types of existentials ; @@ -13,7 +21,6 @@ open Declare open Term open Constr -open Context open Vars open Names open Evd @@ -23,7 +30,7 @@ open Util module NamedDecl = Context.Named.Declaration -let get_fix_exn, stm_get_fix_exn = Hook.make () +open DeclareObl let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) @@ -163,16 +170,16 @@ let evar_dependencies evm oev = else aux deps' in aux (Evar.Set.singleton oev) -let move_after (id, ev, deps as obl) l = +let move_after (id, ev, deps as obl) l = let rec aux restdeps = function - | (id', _, _) as obl' :: tl -> + | (id', _, _) as obl' :: tl -> let restdeps' = Evar.Set.remove id' restdeps in if Evar.Set.is_empty restdeps' then obl' :: obl :: tl else obl' :: aux restdeps' tl | [] -> [obl] in aux (Evar.Set.remove id deps) l - + let sort_dependencies evl = let rec aux l found list = match l with @@ -186,7 +193,7 @@ let sort_dependencies evl = open Environ -let eterm_obligations env name evm fs ?status t ty = +let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) let nc = Environ.named_context env in let nc_len = Context.Named.length nc in @@ -253,10 +260,6 @@ let eterm_obligations env name evm fs ?status t ty = let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in Array.of_list (List.rev evars), (evnames, evmap), t', ty -let hide_obligation () = - Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation") - let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) @@ -276,386 +279,27 @@ type obligation_info = (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array -type 'a obligation_body = - | DefinedObl of 'a - | TermObl of constr - -type obligation = - { obl_name : Id.t; - obl_type : types; - obl_location : Evar_kinds.t Loc.located; - obl_body : pconstant obligation_body option; - obl_status : bool * Evar_kinds.obligation_definition_status; - obl_deps : Int.Set.t; - obl_tac : unit Proofview.tactic option; - } - -type obligations = (obligation array * int) - -type fixpoint_kind = - | IsFixpoint of lident option list - | IsCoFixpoint - -type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - -type program_info_aux = { - prg_name: Id.t; - prg_body: constr; - prg_type: constr; - prg_ctx: UState.t; - prg_univdecl: UState.universe_decl; - prg_obligations: obligations; - prg_deps : Id.t list; - prg_fixkind : fixpoint_kind option ; - prg_implicits : Impargs.manual_implicits; - prg_notations : notations ; - prg_kind : definition_kind; - prg_reduce : constr -> constr; - prg_hook : Lemmas.declaration_hook option; - prg_opaque : bool; - prg_sign: named_context_val; -} - -type program_info = program_info_aux CEphemeron.key - -let get_info x = - try CEphemeron.get x - with CEphemeron.InvalidKey -> - CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker.") - let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) -(* true = hide obligations *) -let get_hide_obligations = - Goptions.declare_bool_option_and_ref - ~depr:false - ~name:"Hiding of Program obligations" - ~key:["Hide";"Obligations"] - ~value:false - - -let get_shrink_obligations = - Goptions.declare_bool_option_and_ref - ~depr:true (* remove in 8.8 *) - ~name:"Shrinking of Program obligations" - ~key:["Shrink";"Obligations"] - ~value:true - let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) -let get_obligation_body expand obl = - match obl.obl_body with - | None -> None - | Some c -> - if expand && snd obl.obl_status == Evar_kinds.Expand then - match c with - | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc) - | TermObl c -> Some c - else (match c with - | DefinedObl pc -> Some (mkConstU pc) - | TermObl c -> Some c) - -let obl_substitution expand obls deps = - Int.Set.fold - (fun x acc -> - let xobl = obls.(x) in - match get_obligation_body expand xobl with - | None -> acc - | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) - deps [] - let subst_deps expand obls deps t = let osubst = obl_substitution expand obls deps in (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) -let rec prod_app t n = - match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (* FIXME *) with - | Prod (_,_,b) -> subst1 n b - | LetIn (_, b, t, b') -> prod_app (subst1 b b') n - | _ -> - user_err ~hdr:"prod_app" - (str"Needed a product, but didn't find one" ++ fnl ()) - - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL - -let replace_appvars subst = - let rec aux c = - let f, l = decompose_app c in - if isVar f then - try - let c' = List.map (Constr.map aux) l in - let (t, b) = Id.List.assoc (destVar f) subst in - mkApp (delayed_force hide_obligation, - [| prod_applist t c'; applistc b c' |]) - with Not_found -> Constr.map aux c - else Constr.map aux c - in Constr.map aux - let subst_deps_obl obls obl = let t' = subst_deps true obls obl.obl_deps obl.obl_type in { obl with obl_type = t' } -module ProgMap = Id.Map - -let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) - -let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] - -let from_prg, program_tcc_summary_tag = - Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" - -let close sec = - if not (ProgMap.is_empty !from_prg) then - let keys = map_keys !from_prg in - user_err ~hdr:"Program" - (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ - prlist_with_sep spc (fun x -> Id.print x) keys ++ - (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ - str "unsolved obligations")) - -let input : program_info ProgMap.t -> obj = - declare_object - { (default_object "Program state") with - cache_function = (fun (na, pi) -> from_prg := pi); - load_function = (fun _ (_, pi) -> from_prg := pi); - discharge_function = (fun _ -> close "section"; None); - classify_function = (fun _ -> close "module"; Dispose) } - open Evd -let progmap_remove prg = - Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) - -let progmap_add n prg = - Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) - -let progmap_replace prg' = - Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) - -let rec intset_to = function - -1 -> Int.Set.empty - | n -> Int.Set.add n (intset_to (pred n)) - -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 - obl_substitution expand obls ints - -let declare_definition prg = - 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 - let uctx = UState.restrict prg.prg_ctx uvars in - let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in - let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in - let () = progmap_remove prg in - let ubinders = UState.universe_binders uctx in - let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in - DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce ubinders prg.prg_implicits ?hook_data - -let rec lam_index n t acc = - match Constr.kind t with - | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> - acc - | Lambda (_, _, b) -> - lam_index n b (succ acc) - | _ -> raise Not_found - -let compute_possible_guardness_evidences n fixbody fixtype = - match n with - | Some { CAst.loc; v = n } -> [lam_index n fixbody 0] - | None -> - (* If recursive argument was not given by user, we try all args. - An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual - fixpoints ?) *) - let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in - let ctx = fst (decompose_prod_n_assum m fixtype) in - List.map_i (fun i _ -> i) 0 ctx - -let mk_proof c = ((c, Univ.ContextSet.empty), Evd.empty_side_effects) - -let declare_mutual_definition l = - let len = List.length l in - let first = List.hd l in - 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 r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) 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, r, 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, fixrs, fixtypes, fiximps = List.split4 defs in - let fixkind = Option.get first.prg_fixkind in - let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in - let rvec = Array.of_list fixrs in - let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in - let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in - let (local,poly,kind) = first.prg_kind in - let fixnames = first.prg_deps in - let opaque = first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in - let indexes, fixdecls = - match fixkind with - | IsFixpoint wfl -> - let possible_indexes = - List.map3 compute_possible_guardness_evidences - wfl fixdefs fixtypes in - let indexes = - Pretyping.search_guard (Global.env()) - possible_indexes fixdecls in - Some indexes, - List.map_i (fun i _ -> - mk_proof (mkFix ((indexes,i),fixdecls))) 0 l - | IsCoFixpoint -> - None, - List.map_i (fun i _ -> - mk_proof (mkCoFix (i,fixdecls))) 0 l - in - (* Declare the recursive definitions *) - let univs = UState.univ_entry ~poly first.prg_ctx in - let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs) - fixnames fixdecls fixtypes fiximps in - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; - Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; - let gr = List.hd kns in - Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; - List.iter progmap_remove l; gr - -let decompose_lam_prod c ty = - let open Context.Rel.Declaration in - let rec aux ctx c ty = - match Constr.kind c, Constr.kind ty with - | LetIn (x, b, t, c), LetIn (x', b', t', ty) - when Constr.equal b b' && Constr.equal t t' -> - let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in - aux ctx' c ty - | _, LetIn (x', b', t', ty) -> - let ctx' = Context.Rel.add (LocalDef (x',b',t')) ctx in - aux ctx' (lift 1 c) ty - | LetIn (x, b, t, c), _ -> - let ctx' = Context.Rel.add (LocalDef (x,b,t)) ctx in - aux ctx' c (lift 1 ty) - | Lambda (x, b, t), Prod (x', b', t') - (* By invariant, must be convertible *) -> - let ctx' = Context.Rel.add (LocalAssum (x,b')) ctx in - aux ctx' t t' - | Cast (c, _, _), _ -> aux ctx c ty - | _, _ -> ctx, c, ty - in aux Context.Rel.empty c ty - -let shrink_body c ty = - let ctx, b, ty = - match ty with - | None -> - let ctx, b = decompose_lam_assum c in - ctx, b, None - | Some ty -> - let ctx, b, ty = decompose_lam_prod c ty in - ctx, b, Some ty - in - let b', ty', n, args = - List.fold_left (fun (b, ty, i, args) decl -> - if noccurn 1 b && Option.cata (noccurn 1) true ty then - subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args - else - let open Context.Rel.Declaration in - let args = if is_local_assum decl then mkRel i :: args else args in - mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty, - succ i, args) - (b, ty, 1, []) ctx - in ctx, b', ty', Array.of_list args - let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) -let it_mkLambda_or_LetIn_or_clean t ctx = - let open Context.Rel.Declaration in - let fold t decl = - if is_local_assum decl then mkLambda_or_LetIn decl t - else - if noccurn 1 t then subst1 mkProp t - else mkLambda_or_LetIn decl t - in - Context.Rel.fold_inside fold ctx ~init:t - -let declare_obligation prg obl body ty uctx = - let body = prg.prg_reduce body in - let ty = Option.map prg.prg_reduce ty in - match obl.obl_status with - | _, Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } - | force, Evar_kinds.Define opaque -> - let opaque = not force && opaque in - let poly = pi2 prg.prg_kind in - let ctx, body, ty, args = - if get_shrink_obligations () && not poly then - shrink_body body ty else [], body, ty, [||] - in - let body = ((body,Univ.ContextSet.empty), Evd.empty_side_effects) in - let ce = - { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; - const_entry_secctx = None; - const_entry_type = ty; - const_entry_universes = uctx; - const_entry_opaque = opaque; - const_entry_inline_code = false; - const_entry_feedback = None; - } in - (* ppedrot: seems legit to have obligations as local *) - let constant = Declare.declare_constant obl.obl_name ~local:ImportNeedQualified - (DefinitionEntry ce,IsProof Property) - in - if not opaque then add_hint (Locality.make_section_locality None) prg constant; - definition_message obl.obl_name; - let body = match uctx with - | Polymorphic_entry (_, uctx) -> - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - | Monomorphic_entry _ -> - Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) - in - true, { obl with obl_body = body } - let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind notations obls impls kind reduce = let obls', b = @@ -671,27 +315,27 @@ let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind | Some b -> Array.mapi (fun i (n, t, l, o, d, tac) -> - { obl_name = n ; obl_body = None; + { obl_name = n ; obl_body = None; obl_location = l; obl_type = t; obl_status = o; obl_deps = d; obl_tac = tac }) obls, b in let ctx = UState.make_flexible_nonalgebraic ctx in - { prg_name = n ; prg_body = b; prg_type = reduce t; + { prg_name = n ; prg_body = b; prg_type = reduce t; prg_ctx = ctx; prg_univdecl = udecl; prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; - prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; + prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; prg_opaque = opaque; prg_sign = sign } 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 snd (CEphemeron.get v).prg_obligations > 0 then incr i) m; !i -exception Found of program_info +exception Found of program_info CEphemeron.key let map_first m = try @@ -702,28 +346,28 @@ let map_first m = with Found x -> x let get_prog name = - let prg_infos = !from_prg in + let prg_infos = get_prg_info_map () in match name with Some n -> - (try get_info (ProgMap.find n prg_infos) + (try CEphemeron.get (ProgMap.find n prg_infos) with Not_found -> raise (NoObligations (Some n))) | None -> (let n = map_cardinal prg_infos in match n with 0 -> raise (NoObligations None) - | 1 -> get_info (map_first prg_infos) + | 1 -> CEphemeron.get (map_first prg_infos) | _ -> let progs = Id.Set.elements (ProgMap.domain prg_infos) in let prog = List.hd progs in let progs = prlist_with_sep pr_comma Id.print progs in - user_err + user_err (str "More than one program with unsolved obligations: " ++ progs ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\"")) let get_any_prog () = - let prg_infos = !from_prg in + let prg_infos = get_prg_info_map () in let n = map_cardinal prg_infos in - if n > 0 then get_info (map_first prg_infos) + if n > 0 then CEphemeron.get (map_first prg_infos) else raise (NoObligations None) let get_prog_err n = @@ -732,42 +376,8 @@ let get_prog_err n = let get_any_prog_err () = try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id) -let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 - let all_programs () = - ProgMap.fold (fun k p l -> p :: l) !from_prg [] - -type progress = - | Remain of int - | Dependent - | Defined of GlobRef.t - -let obligations_message rem = - if rem > 0 then - if Int.equal rem 1 then - Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining") - else - Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining") - else - Flags.if_verbose Feedback.msg_info (str "No more obligations remaining") - -let update_obls prg obls rem = - let prg' = { prg with prg_obligations = (obls, rem) } in - progmap_replace prg'; - obligations_message rem; - if rem > 0 then Remain rem - else ( - match prg'.prg_deps with - | [] -> - let kn = declare_definition prg' in - progmap_remove prg'; - Defined kn - | l -> - let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in - if List.for_all (fun x -> obligations_solved x) progs then - let kn = declare_mutual_definition progs in - Defined kn - else Dependent) + ProgMap.fold (fun k p l -> p :: l) (get_prg_info_map ()) [] let is_defined obls x = not (Option.is_empty obls.(x).obl_body) @@ -778,14 +388,6 @@ let deps_remaining obls deps = else x :: acc) deps [] -let dependencies obls n = - let res = ref Int.Set.empty in - Array.iteri - (fun i obl -> - if not (Int.equal i n) && Int.Set.mem n obl.obl_deps then - res := Int.Set.add i !res) - obls; - !res let goal_kind poly = Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition) @@ -798,12 +400,6 @@ let kind_of_obligation poly o = | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly | _ -> goal_proof_kind poly -let not_transp_msg = - str "Obligation should be transparent but was declared opaque." ++ spc () ++ - str"Use 'Defined' instead." - -let err_not_transp () = pperror not_transp_msg - let rec string_of_list sep f = function [] -> "" | x :: [] -> f x @@ -839,81 +435,12 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_terminator name num guard auto pf = - let open Proof_global in - let open Lemmas in - let term = standard_proof_terminator guard in - match pf with - | Admitted _ -> Internal.apply_terminator term pf - | Proved (opq, id, { entries=[entry]; universes=uctx }, hook ) -> begin - let env = Global.env () in - let ty = entry.Entries.const_entry_type in - let body, eff = Future.force entry.const_entry_body in - let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in - let sigma = Evd.from_ctx uctx in - let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in - Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); - (* Declare the obligation ourselves and drop the hook *) - let prg = get_info (ProgMap.find name !from_prg) in - (* Ensure universes are substituted properly in body and type *) - 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 obl = obls.(num) in - let status = - match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Opaque -> err_not_transp () - | (true, _), Opaque -> err_not_transp () - | (false, _), Opaque -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), Transparent -> - Evar_kinds.Define false - | (_, status), Transparent -> status - in - let obl = { obl with obl_status = false, status } in - let ctx = - if pi2 prg.prg_kind then ctx - else UState.union prg.prg_ctx ctx - in - let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let (defined, obl) = declare_obligation prg obl body ty uctx in - let obls = Array.copy obls in - let () = obls.(num) <- obl in - let prg_ctx = - if pi2 (prg.prg_kind) then (* Polymorphic *) - (* We merge the new universes and constraints of the - polymorphic obligation with the existing ones *) - UState.union prg.prg_ctx ctx - else - (* The first obligation, if defined, - declares the univs of the constant, - each subsequent obligation declares its own additional - universes and constraints if any *) - if defined then UState.make (Global.universes ()) - else ctx - in - let prg = { prg with prg_ctx } in - try - ignore (update_obls prg obls (pred rem)); - if pred rem > 0 then - begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some name) None deps) - end - with e when CErrors.noncritical e -> - let e = CErrors.push e in - pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) - end - | Proved (_, _, _,_ ) -> - CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") - let obligation_hook prg obl num auto ctx' _ _ gr = let obls, rem = prg.prg_obligations in let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in let () = match obl.obl_status with - (true, Evar_kinds.Expand) + (true, Evar_kinds.Expand) | (true, Evar_kinds.Define true) -> if not transparent then err_not_transp () | _ -> () @@ -1049,7 +576,7 @@ and solve_obligations n tac = solve_prg_obligations prg tac and solve_all_obligations tac = - ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg + ProgMap.iter (fun k v -> ignore(solve_prg_obligations (CEphemeron.get v) tac)) (get_prg_info_map ()) and try_solve_obligation n prg tac = let prg = get_prog prg in @@ -1091,9 +618,9 @@ let show_obligations ?(msg=true) n = let progs = match n with | None -> all_programs () | Some n -> - try [ProgMap.find n !from_prg] + try [ProgMap.find n (get_prg_info_map ())] with Not_found -> raise (NoObligations (Some n)) - in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs + in List.iter (fun x -> show_obligations_of_prg ~msg (CEphemeron.get x)) progs let show_term n = let prg = get_prog_err n in @@ -1113,8 +640,8 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); - let cst = declare_definition prg in - Defined cst) + let cst = DeclareObl.declare_definition prg in + Defined cst) else ( let len = Array.length obls in let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in @@ -1140,8 +667,8 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic else let res = auto_solve_obligations (Some x) tactic in match res with - | Defined _ -> - (* If one definition is turned into a constant, + | Defined _ -> + (* If one definition is turned into a constant, the whole block is defined. *) true | _ -> false) false deps @@ -1150,7 +677,7 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic let admit_prog prg = let obls, rem = prg.prg_obligations in let obls = Array.copy obls in - Array.iteri + Array.iteri (fun i x -> match x.obl_body with | None -> |