diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 440 |
1 files changed, 257 insertions, 183 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 314789ce..29d74573 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -13,21 +13,16 @@ open Declare *) open Term -open Context open Vars open Names open Evd open Pp -open Errors +open CErrors open Util let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) -let trace s = - if !Flags.debug then msg_debug s - else () - let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) @@ -44,21 +39,19 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: named_context; - ev_status: Evar_kinds.obligation_definition_status; + ev_hyps: Context.Named.t; + ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; ev_typ: types; ev_tac: unit Proofview.tactic option; ev_deps: Int.Set.t } -(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *) -let evar_tactic = Store.field () - (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) -let subst_evar_constr evs n idf t = +let subst_evar_constr evs n idf t = + let open Context.Named.Declaration in let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in let evar_info id = List.assoc_f Evar.equal id evs in @@ -82,9 +75,9 @@ let subst_evar_constr evs n idf t = let args = let rec aux hyps args acc = match hyps, args with - ((_, None, _) :: tlh), (c :: tla) -> + (LocalAssum _ :: tlh), (c :: tla) -> aux tlh tla ((substrec (depth, fixrels) c) :: acc) - | ((_, Some _, _) :: tlh), (_ :: tla) -> + | (LocalDef _ :: tlh), (_ :: tla) -> aux tlh tla acc | [], [] -> acc | _, _ -> acc (*failwith "subst_evars: invalid argument"*) @@ -120,22 +113,23 @@ let subst_vars acc n t = Changes evars and hypothesis references to variable references. *) let etype_of_evar evs hyps concl = + let open Context.Named.Declaration in let rec aux acc n = function - (id, copt, t) :: tl -> - let t', s, trans = subst_evar_constr evs n mkVar t in + decl :: tl -> + let t', s, trans = subst_evar_constr evs n mkVar (get_type decl) in let t'' = subst_vars acc 0 t' in - let rest, s', trans' = aux (id :: acc) (succ n) tl in + let rest, s', trans' = aux (get_id decl :: acc) (succ n) tl in let s' = Int.Set.union s s' in let trans' = Id.Set.union trans trans' in - (match copt with - Some c -> + (match decl with + | LocalDef (id,c,_) -> let c', s'', trans'' = subst_evar_constr evs n mkVar c in let c' = subst_vars acc 0 c' in - mkNamedProd_or_LetIn (id, Some c', t'') rest, + mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, Int.Set.union s'' s', Id.Set.union trans'' trans' - | None -> - mkNamedProd_or_LetIn (id, None, t'') rest, s', trans') + | LocalAssum (id,_) -> + mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') | [] -> let t', s, trans = subst_evar_constr evs n mkVar concl in subst_vars acc 0 t', s, trans @@ -194,7 +188,7 @@ open Environ 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_context_length nc in + let nc_len = Context.Named.length nc in let evm = Evarutil.nf_evar_map_undefined evm in let evl = Evarutil.non_instantiated evm in let evl = Evar.Map.bindings evl in @@ -221,25 +215,21 @@ let eterm_obligations env name evm fs ?status t ty = | None -> evtyp, hyps, 0 in let loc, k = evar_source id evm in - let status = match k with Evar_kinds.QuestionMark o -> Some o | _ -> status in - let status, chop = match status with - | Some (Evar_kinds.Define true as stat) -> - if not (Int.equal chop fs) then Evar_kinds.Define false, None - else stat, Some chop - | Some s -> s, None - | None -> Evar_kinds.Define true, None - in - let tac = match Store.get ev.evar_extra evar_tactic with - | Some t -> - if Dyn.has_tag t "tactic" then - Some (Tacinterp.interp - (Tacinterp.globTacticIn (Tacinterp.tactic_out t))) - else None - | None -> None + let status = match k with + | Evar_kinds.QuestionMark o -> o + | _ -> match status with + | Some o -> o + | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ())) + in + let force_status, status, chop = match status with + | Evar_kinds.Define true as stat -> + if not (Int.equal chop fs) then true, Evar_kinds.Define false, None + else false, stat, Some chop + | s -> false, s, None in let info = { ev_name = (n, nstr); - ev_hyps = hyps; ev_status = status; ev_chop = chop; - ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac } + ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop; + ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None } in (id, info) :: l) evn [] in @@ -249,14 +239,14 @@ let eterm_obligations env name evm fs ?status t ty = let ty, _, _ = subst_evar_constr evts 0 mkVar ty in let evars = List.map (fun (ev, info) -> - let { ev_name = (_, name); ev_status = status; + let { ev_name = (_, name); ev_status = force_status, status; ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info in - let status = match status with + let force_status, status = match status with | Evar_kinds.Define true when Id.Set.mem name transparent -> - Evar_kinds.Define false - | _ -> status - in name, typ, src, status, deps, tac) evts + true, Evar_kinds.Define false + | _ -> force_status, status + in name, typ, src, (force_status, status), deps, tac) evts in let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in let evmap f c = pi1 (subst_evar_constr evts 0 f c) in @@ -268,21 +258,22 @@ let safe_init_constant md name () = Coqlib.gen_constant "Obligations" md name let hide_obligation = safe_init_constant tactics_module "obligation" -let pperror cmd = Errors.errorlabstrm "Program" cmd +let pperror cmd = CErrors.errorlabstrm "Program" cmd let error s = pperror (str s) let reduce c = - Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c + Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c exception NoObligations of Id.t option let explain_no_obligations = function - Some ident -> str "No obligations for program " ++ str (Id.to_string ident) + Some ident -> str "No obligations for program " ++ Id.print ident | None -> str "No obligations remaining" type obligation_info = (Names.Id.t * Term.types * Evar_kinds.t Loc.located * - Evar_kinds.obligation_definition_status * Int.Set.t * unit Proofview.tactic option) array + (bool * Evar_kinds.obligation_definition_status) + * Int.Set.t * unit Proofview.tactic option) array type 'a obligation_body = | DefinedObl of 'a @@ -293,7 +284,7 @@ type obligation = obl_type : types; obl_location : Evar_kinds.t Loc.located; obl_body : constant obligation_body option; - obl_status : Evar_kinds.obligation_definition_status; + obl_status : bool * Evar_kinds.obligation_definition_status; obl_deps : Int.Set.t; obl_tac : unit Proofview.tactic option; } @@ -311,6 +302,7 @@ type program_info_aux = { prg_body: constr; prg_type: constr; prg_ctx: Evd.evar_universe_context; + prg_pl: Id.t Loc.located list option; prg_obligations: obligations; prg_deps : Id.t list; prg_fixkind : fixpoint_kind option ; @@ -323,34 +315,16 @@ type program_info_aux = { prg_sign: named_context_val; } -type program_info = program_info_aux Ephemeron.key +type program_info = program_info_aux CEphemeron.key let get_info x = - try Ephemeron.get x - with Ephemeron.InvalidKey -> - Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker") + 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 (set_default_tactic, get_default_tactic, print_default_tactic) = - Tactic_option.declare_tactic_option "Program tactic" - -(* true = All transparent, false = Opaque if possible *) -let proofs_transparency = ref true - -let set_proofs_transparency = (:=) proofs_transparency -let get_proofs_transparency () = !proofs_transparency - -open Goptions - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "transparency of Program obligations"; - optkey = ["Transparent";"Obligations"]; - optread = get_proofs_transparency; - optwrite = set_proofs_transparency; } +let default_tactic = ref (Proofview.tclUNIT ()) (* true = hide obligations *) let hide_obligations = ref false @@ -358,6 +332,7 @@ let hide_obligations = ref false let set_hide_obligations = (:=) hide_obligations let get_hide_obligations () = !hide_obligations +open Goptions let _ = declare_bool_option { optsync = true; @@ -367,7 +342,7 @@ let _ = optread = get_hide_obligations; optwrite = set_hide_obligations; } -let shrink_obligations = ref false +let shrink_obligations = ref true let set_shrink_obligations = (:=) shrink_obligations let get_shrink_obligations () = !shrink_obligations @@ -375,7 +350,7 @@ let get_shrink_obligations () = !shrink_obligations let _ = declare_bool_option { optsync = true; - optdepr = false; + optdepr = true; optname = "Shrinking of Program obligations"; optkey = ["Shrink";"Obligations"]; optread = get_shrink_obligations; @@ -383,36 +358,35 @@ let _ = let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type -let get_body obl = +let get_body obl = match obl.obl_body with - | None -> assert false + | None -> None | Some (DefinedObl c) -> let ctx = Environ.constant_context (Global.env ()) c in let pc = (c, Univ.UContext.instance ctx) in - DefinedObl pc - | Some (TermObl c) -> - TermObl c + Some (DefinedObl pc) + | Some (TermObl c) -> + Some (TermObl c) let get_obligation_body expand obl = - let c = get_body obl in - let c' = - if expand && obl.obl_status == Evar_kinds.Expand then - (match c with - | DefinedObl pc -> constant_value_in (Global.env ()) pc - | TermObl c -> c) - else (match c with - | DefinedObl pc -> mkConstU pc - | TermObl c -> c) - in c' + match get_body obl 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 - let oblb = - try get_obligation_body expand xobl - with e when Errors.noncritical e -> assert false - in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) + 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 = @@ -458,9 +432,9 @@ 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 = Map.Make(Id) +module ProgMap = Id.Map -let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m) +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 [] @@ -510,15 +484,21 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Stm.get_fix_exn () in + let pl, ctx = + Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in - progmap_remove prg; + let () = progmap_remove prg in + let cst = !declare_definition_ref prg.prg_name - prg.prg_kind ce prg.prg_implicits - (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) + prg.prg_kind ce prg.prg_implicits + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) + in + Universes.register_universe_binders cst pl; + cst open Pp @@ -539,7 +519,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) - let m = nb_prod fixtype in + let m = Termops.nb_prod fixtype in let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx @@ -571,7 +551,8 @@ let declare_mutual_definition l = List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in let indexes = - Pretyping.search_guard Loc.ghost (Global.env()) + Pretyping.search_guard + Loc.ghost (Global.env()) possible_indexes fixdecls in Some indexes, List.map_i (fun i _ -> @@ -594,15 +575,49 @@ let declare_mutual_definition l = Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx; List.iter progmap_remove l; kn -let shrink_body c = - let ctx, b = decompose_lam c in - let b', n, args = - List.fold_left (fun (b, i, args) (n,t) -> - if noccurn 1 b then - subst1 mkProp b, succ i, args - else mkLambda (n,t,b), succ i, mkRel i :: args) - (b, 1, []) ctx - in List.map (fun (c,t) -> (c,None,t)) ctx, b', Array.of_list args +let decompose_lam_prod c ty = + let open Context.Rel.Declaration in + let rec aux ctx c ty = + match kind_of_term c, kind_of_term ty with + | LetIn (x, b, t, c), LetIn (x', b', t', ty) + when eq_constr b b' && eq_constr 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 open Context.Rel.Declaration in + 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 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] @@ -613,46 +628,47 @@ 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) } - | Evar_kinds.Define opaque -> - let opaque = if get_proofs_transparency () then false else opaque in + | _, 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, args = + let ctx, body, ty, args = if get_shrink_obligations () && not poly then - shrink_body body else [], body, [||] + shrink_body body ty else [], body, ty, [||] in let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in - let ce = + let ce = { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; - const_entry_type = if List.is_empty ctx then ty else None; + const_entry_type = ty; const_entry_polymorphic = poly; 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 *) + (** ppedrot: seems legit to have obligations as local *) let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in if not opaque then add_hint false prg constant; definition_message obl.obl_name; true, { obl with obl_body = - if poly then + if poly then Some (DefinedObl constant) else Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) } -let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls impls kind reduce hook = - let obls', b = +let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind + notations obls impls kind reduce hook = + let obls', b = match b with | None -> assert(Int.equal (Array.length obls) 0); let n = Nameops.add_suffix n "_obligation" in [| { obl_name = n; obl_body = None; obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t; - obl_status = Evar_kinds.Expand; obl_deps = Int.Set.empty; + obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty; obl_tac = None } |], mkVar n | Some b -> @@ -664,7 +680,7 @@ let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls obls, b in { prg_name = n ; prg_body = b; prg_type = reduce t; - prg_ctx = ctx; + prg_ctx = ctx; prg_pl = pl; prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; @@ -674,7 +690,7 @@ let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls let map_cardinal m = let i = ref 0 in ProgMap.iter (fun _ v -> - if snd (Ephemeron.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 @@ -682,7 +698,7 @@ exception Found of program_info let map_first m = try ProgMap.iter (fun _ v -> - if snd (Ephemeron.get v).prg_obligations > 0 then + if snd (CEphemeron.get v).prg_obligations > 0 then raise (Found v)) m; assert(false) with Found x -> x @@ -698,11 +714,13 @@ let get_prog name = match n with 0 -> raise (NoObligations None) | 1 -> get_info (map_first prg_infos) - | _ -> - error ("More than one program with unsolved obligations: "^ - String.concat ", " - (List.map string_of_id - (ProgMap.fold (fun k _ s -> k::s) 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 Nameops.pr_id progs in + errorlabstrm "" + (str "More than one program with unsolved obligations: " ++ progs + ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\"")) let get_any_prog () = let prg_infos = !from_prg in @@ -729,11 +747,11 @@ type progress = let obligations_message rem = if rem > 0 then if Int.equal rem 1 then - Flags.if_verbose msg_info (int rem ++ str " obligation remaining") + Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining") else - Flags.if_verbose msg_info (int rem ++ str " obligations remaining") + Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining") else - Flags.if_verbose msg_info (str "No more obligations remaining") + 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 @@ -807,14 +825,64 @@ let solve_by_tac name evi t poly ctx = Inductiveops.control_only_guard (Global.env ()) (fst body); (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' +let obligation_terminator name num guard hook auto pf = + let open Proof_global in + let term = Lemmas.universe_proof_terminator guard hook in + match pf with + | Admitted _ -> apply_terminator term pf + | Proved (opq, id, proof) -> + if not !shrink_obligations then apply_terminator term pf + else + let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in + let env = Global.env () in + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let ty = entry.Entries.const_entry_type in + let (body, cstr), eff = Future.force entry.Entries.const_entry_body in + assert(Safe_typing.empty_private_constants = eff); + let sigma = Evd.from_ctx (fst uctx) in + let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in + Inductiveops.control_only_guard (Global.env ()) body; + (** Declare the obligation ourselves and drop the hook *) + let prg = get_info (ProgMap.find name !from_prg) in + let ctx = Evd.evar_universe_context sigma in + let prg = { prg with prg_ctx = ctx } in + let obls, rem = prg.prg_obligations in + let obl = obls.(num) in + let status = + match obl.obl_status, opq with + | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp () + | (true, _), Vernacexpr.Opaque _ -> err_not_transp () + | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false + | (_, status), Vernacexpr.Transparent -> status + in + let obl = { obl with obl_status = false, status } in + let uctx = Evd.evar_context_universe_context ctx in + let (_, obl) = declare_obligation prg obl body ty uctx in + let obls = Array.copy obls in + let _ = obls.(num) <- obl 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)) + let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in let cst = match gr with ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in let () = match obl.obl_status with - | Evar_kinds.Expand -> if not transparent then err_not_transp () - | Evar_kinds.Define op -> if not op && not transparent then err_not_transp () - in + (true, Evar_kinds.Expand) + | (true, Evar_kinds.Define true) -> + if not transparent then err_not_transp () + | _ -> () +in let obl = { obl with obl_body = Some (DefinedObl cst) } in let () = if transparent then add_hint true prg cst in let obls = Array.copy obls in @@ -832,9 +900,9 @@ let obligation_hook prg obl num auto ctx' _ gr = let prg = { prg with prg_ctx = ctx' } in let () = try ignore (update_obls prg obls (pred rem)) - with e when Errors.noncritical e -> - let e = Errors.push e in - pperror (Errors.iprint (Cerrors.process_vernac_interp_error e)) + with e when CErrors.noncritical e -> + let e = CErrors.push e in + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) in if pred rem > 0 then begin let deps = dependencies obls num in @@ -855,15 +923,16 @@ let rec solve_obligation prg num tac = ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); in let obl = subst_deps_obl obls obl in - let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in + let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in + let terminator guard hook = + Proof_global.make_terminator + (obligation_terminator prg.prg_name num guard hook auto) in let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in - let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type hook in - let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in - let _ = Pfedit.by (snd (get_default_tactic ())) in + let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in + let _ = Pfedit.by !default_tactic in Option.iter (fun tac -> Pfedit.set_end_tac tac) tac and obligation (user_num, name, typ) tac = @@ -881,7 +950,7 @@ and obligation (user_num, name, typ) tac = and solve_obligation_by_tac prg obls i tac = let obl = obls.(i) in match obl.obl_body with - | Some _ -> false + | Some _ -> None | None -> try if List.is_empty (deps_remaining obls obl.obl_deps) then @@ -892,32 +961,32 @@ and solve_obligation_by_tac prg obls i tac = | None -> match obl.obl_tac with | Some t -> t - | None -> snd (get_default_tactic ()) + | None -> !default_tactic in - let evd = Evd.from_ctx !prg.prg_ctx in + let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in - let t, ty, ctx = - solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 !prg.prg_kind) (Evd.evar_universe_context evd) + let t, ty, ctx = + solve_by_tac obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) in let uctx = Evd.evar_context_universe_context ctx in - let () = prg := {!prg with prg_ctx = ctx} in - let def, obl' = declare_obligation !prg obl t ty uctx in + let prg = {prg with prg_ctx = ctx} in + let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; - if def && not (pi2 !prg.prg_kind) then ( + if def && not (pi2 prg.prg_kind) then ( (* Declare the term constraints with the first obligation only *) let evd = Evd.from_env (Global.env ()) in let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in let ctx' = Evd.evar_universe_context evd in - prg := {!prg with prg_ctx = ctx'}); - true - else false - with e when Errors.noncritical e -> - let (e, _) = Errors.push e in + Some {prg with prg_ctx = ctx'}) + else Some prg + else None + with e when CErrors.noncritical e -> + let (e, _) = CErrors.push e in match e with | Refiner.FailError (_, s) -> user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) - | e -> false + | e -> None (* FIXME really ? *) and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in @@ -929,16 +998,20 @@ and solve_prg_obligations prg ?oblset tac = | Some s -> set := s; (fun i -> Int.Set.mem i !set) in - let prg = ref prg in + let prgref = ref prg in let _ = Array.iteri (fun i x -> - if p i && solve_obligation_by_tac prg obls' i tac then - let deps = dependencies obls i in - (set := Int.Set.union !set deps; - decr rem)) + if p i then + match solve_obligation_by_tac !prgref obls' i tac with + | None -> () + | Some prg' -> + prgref := prg'; + let deps = dependencies obls i in + (set := Int.Set.union !set deps; + decr rem)) obls' in - update_obls !prg obls' !rem + update_obls !prgref obls' !rem and solve_obligations n tac = let prg = get_prog_err n in @@ -951,15 +1024,15 @@ and try_solve_obligation n prg tac = let prg = get_prog prg in let obls, rem = prg.prg_obligations in let obls' = Array.copy obls in - let prgref = ref prg in - if solve_obligation_by_tac prgref obls' n tac then - ignore(update_obls !prgref obls' (pred rem)); + match solve_obligation_by_tac prg obls' n tac with + | Some prg' -> ignore(update_obls prg' obls' (pred rem)) + | None -> () and try_solve_obligations n tac = try ignore (solve_obligations n tac) with NoObligations _ -> () and auto_solve_obligations n ?oblset tac : progress = - Flags.if_verbose msg_info (str "Solving obligations automatically..."); + Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically..."); try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent open Pp @@ -967,14 +1040,15 @@ let show_obligations_of_prg ?(msg=true) prg = let n = prg.prg_name in let obls, rem = prg.prg_obligations in let showed = ref 5 in - if msg then msg_info (int rem ++ str " obligation(s) remaining: "); + if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: "); Array.iteri (fun i x -> match x.obl_body with | None -> if !showed > 0 then ( - decr showed; - msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ - str "of" ++ spc() ++ str (Id.to_string n) ++ str ":" ++ spc () ++ + decr showed; + let x = subst_deps_obl obls x in + Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ + str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++ hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++ str "." ++ fnl ()))) | Some _ -> ()) @@ -991,38 +1065,38 @@ let show_obligations ?(msg=true) n = let show_term n = let prg = get_prog_err n in let n = prg.prg_name in - (str (Id.to_string n) ++ spc () ++ str":" ++ spc () ++ + (Id.print n ++ spc () ++ str":" ++ spc () ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body) -let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic +let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = let sign = Decls.initialize_named_context_for_proof () in - let info = str (Id.to_string n) ++ str " has type-checked" in - let prg = init_prog_info sign ~opaque n term t ctx [] None [] obls implicits kind reduce hook in + let info = Id.print n ++ str " has type-checked" in + let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( - Flags.if_verbose msg_info (info ++ str "."); + Flags.if_verbose Feedback.msg_info (info ++ str "."); let cst = declare_definition prg in Defined cst) else ( let len = Array.length obls in - let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in - progmap_add n (Ephemeron.create prg); + let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in + progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) +let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = let sign = Decls.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> - let prg = init_prog_info sign ~opaque n (Some b) t ctx deps (Some fixkind) + let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind) notations obls imps kind reduce hook - in progmap_add n (Ephemeron.create prg)) l; + in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> if finished then finished |