From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- proofs/proof.ml | 69 +++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 48 insertions(+), 21 deletions(-) (limited to 'proofs/proof.ml') diff --git a/proofs/proof.ml b/proofs/proof.ml index 5c963d53..51e0a1d6 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - CErrors.error "This proof is focused, but cannot be unfocused this way" + CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way") | NoSuchGoals (i,j) when Int.equal i j -> - CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").") + CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> - CErrors.errorlabstrm "Focus" Pp.( + CErrors.user_err ~hdr:"Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) - | FullyUnfocused -> CErrors.error "The proof is not focused" + | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") | _ -> raise CErrors.Unhandled end @@ -98,7 +100,7 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k) (* Subpart of the type of proofs. It contains the parts of the proof which are under control of the undo mechanism *) -type proof = { +type t = { (* Current focused proofview *) proofview: Proofview.proofview; (* Entry for the proofview *) @@ -112,9 +114,11 @@ type proof = { (* List of goals that have been given up *) given_up : Goal.goal list; (* The initial universe context (for the statement) *) - initial_euctx : Evd.evar_universe_context + initial_euctx : UState.t } +type proof = t + (*** General proof functions ***) let proof p = @@ -163,6 +167,7 @@ let map_structured_proof pfts process_goal: 'a pre_goals = let rec unroll_focus pv = function | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk | [] -> pv + (* spiwack: a proof is considered completed even if its still focused, if the focus doesn't hide any goal. Unfocusing is handled in {!return}. *) @@ -301,10 +306,10 @@ exception HasShelvedGoals exception HasGivenUpGoals exception HasUnresolvedEvar let _ = CErrors.register_handler begin function - | UnfinishedProof -> CErrors.error "Some goals have not been solved." - | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf." - | HasGivenUpGoals -> CErrors.error "Some goals have been given up." - | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated." + | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.") + | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.") + | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.") + | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.") | _ -> raise CErrors.Unhandled end @@ -342,7 +347,11 @@ let run_tactic env tac pr = Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) - let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in + let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in + let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in + (* Check that retrieved given up is empty *) + if not (List.is_empty retrieved_given_up) then + CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved @@ -372,13 +381,31 @@ let in_proof p k = k (Proofview.return p.proofview) let unshelve p = { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] } +let pr_proof p = + let p = map_structured_proof p (fun _sigma g -> g) in + Pp.( + let pr_goal_list = prlist_with_sep spc Goal.pr_goal in + let rec aux acc = function + | [] -> acc + | (before,after)::stack -> + aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++ + pr_goal_list after) stack in + str "[" ++ str "focus structure: " ++ + aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++ + str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++ + str "given up: " ++ pr_goal_list p.given_up_goals ++ + str "]" + ) + (*** Compatibility layer with <=v8.2 ***) module V82 = struct let subgoals p = - Proofview.V82.goals p.proofview + let it, sigma = Proofview.proofview p.proofview in + Evd.{ it; sigma } let background_subgoals p = - Proofview.V82.goals (unroll_focus p.proofview p.focus_stack) + let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in + Evd.{ it; sigma } let top_goal p = let { Evd.it=gls ; sigma=sigma; } = @@ -404,15 +431,15 @@ module V82 = struct let evl = Evarutil.non_instantiated sigma in let evl = Evar.Map.bindings evl in if (n <= 0) then - CErrors.error "incorrect existential variable index" + CErrors.user_err Pp.(str "incorrect existential variable index") else if CList.length evl < n then - CErrors.error "not so many uninstantiated existential variables" + CErrors.user_err Pp.(str "not so many uninstantiated existential variables") else CList.nth evl (n-1) in let env = Evd.evar_filtered_env evi in - let rawc = Constrintern.intern_constr env com in - let ltac_vars = Pretyping.empty_lvar in + let rawc = Constrintern.intern_constr env sigma com in + let ltac_vars = Glob_ops.empty_lvar in let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in Proofview.Unsafe.tclEVARS sigma end in -- cgit v1.2.3