From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/proof.ml | 507 +++++++++++++++++++++++--------------------------------- 1 file changed, 206 insertions(+), 301 deletions(-) (limited to 'proofs/proof.ml') diff --git a/proofs/proof.ml b/proofs/proof.ml index bd185b99..828f9fa7 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -1,16 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Proofview.proofview -> unfocusable) * - (_focus_kind -> bool) +type _focus_condition = + | CondNo of bool * _focus_kind + | CondDone of bool * _focus_kind + | CondEndStack of _focus_kind (* loose_end is false here *) type 'a focus_condition = _focus_condition let next_kind = ref 0 @@ -49,107 +51,71 @@ let new_focus_kind () = incr next_kind; r -(* Auxiliary function to define conditions. *) -let check kind1 kind2 = kind1=kind2 - (* To be authorized to unfocus one must meet the condition prescribed by the action which focused.*) (* spiwack: we could consider having a list of authorized focus_kind instead of just one, if anyone needs it *) -(* [no_cond] only checks that the unfocusing command uses the right - [focus_kind]. *) - -module Cond = struct - (* first attempt at an algebra of condition *) - (* semantics: - - [Cannot] means that the condition is not met - - [Strict] that the condition is met - - [Loose] that the condition is not quite met - but authorises to unfocus provided a condition - of a previous focus on the stack is (strictly) - met. [Loose] focuses are those, like bullets, - which do not have a closing command and - are hence closed by unfocusing actions unrelated - to their focus_kind. - *) - let bool e b = - if b then fun _ _ -> Strict - else fun _ _ -> Cannot e - let loose c k p = match c k p with - | Cannot _ -> Loose - | c -> c - let cloose l c = - if l then loose c - else c - let (&&&) c1 c2 k p= - match c1 k p , c2 k p with - | Cannot e , _ - | _ , Cannot e -> Cannot e - | Strict, Strict -> Strict - | _ , _ -> Loose - let kind e k0 k p = bool e (k0=k) k p - let pdone e k p = bool e (Proofview.finished p) k p -end - -(* Unfocus command. - Fails if the proof is not focused. *) exception CannotUnfocusThisWay + +(* Cannot focus on non-existing subgoals *) +exception NoSuchGoals of int * int + + +exception FullyUnfocused + let _ = Errors.register_handler begin function | CannotUnfocusThisWay -> - Util.error "This proof is focused, but cannot be unfocused this way" + Errors.error "This proof is focused, but cannot be unfocused this way" + | NoSuchGoals (i,j) when Int.equal i j -> + Errors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").") + | NoSuchGoals (i,j) -> + Errors.errorlabstrm "Focus" Pp.( + str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." + ) + | FullyUnfocused -> Errors.error "The proof is not focused" | _ -> raise Errors.Unhandled end -open Cond -let no_cond_gen e ~loose_end k0 = - cloose loose_end (kind e k0) -let no_cond_gen e ?(loose_end=false) k = no_cond_gen e ~loose_end k , check k -let no_cond ?loose_end = no_cond_gen CannotUnfocusThisWay ?loose_end -(* [done_cond] checks that the unfocusing command uses the right [focus_kind] - and that the focused proofview is complete. *) -let done_cond_gen e ~loose_end k0 = - (cloose loose_end (kind e k0)) &&& pdone e -let done_cond_gen e ?(loose_end=false) k = done_cond_gen e ~loose_end k , check k -let done_cond ?loose_end = done_cond_gen CannotUnfocusThisWay ?loose_end - +let check_cond_kind c k = + let kind_of_cond = function + | CondNo (_,k) | CondDone(_,k) | CondEndStack k -> k in + Int.equal (kind_of_cond c) k + +let test_cond c k1 pw = + match c with + | CondNo(_, k) when Int.equal k k1 -> Strict + | CondNo(true, _) -> Loose + | CondNo(false, _) -> Cannot NotThisWay + | CondDone(_, k) when Int.equal k k1 && Proofview.finished pw -> Strict + | CondDone(true, _) -> Loose + | CondDone(false, _) -> Cannot NotThisWay + | CondEndStack k when Int.equal k k1 -> Strict + | CondEndStack _ -> Cannot AlreadyNoFocus + +let no_cond ?(loose_end=false) k = CondNo (loose_end, k) +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_state = { +type proof = { (* Current focused proofview *) proofview: Proofview.proofview; + (* Entry for the proofview *) + entry : Proofview.entry; (* History of the focusings, provides information on how to unfocus the proof and the extra information stored while focusing. The list is empty when the proof is fully unfocused. *) focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list; - (* Extra information which can be freely used to create new behaviours. *) - intel: Store.t + (* List of goals that have been shelved. *) + shelf : Goal.goal list; + (* List of goals that have been given up *) + given_up : Goal.goal list; } -type proof_info = { - mutable endline_tactic : unit Proofview.tactic ; - mutable section_vars : Sign.section_context option; - initial_conclusions : Term.types list -} - -type undo_action = - | State of proof_state - | Effect of (unit -> unit) - -type proof = { (* current proof_state *) - mutable state : proof_state; - (* The undo stack *) - mutable undo_stack : undo_action list; - (* secondary undo stacks used for transactions *) - mutable transactions : undo_action list list; - info : proof_info - } - - (*** General proof functions ***) -let proof { state = p } = +let proof p = let (goals,sigma) = Proofview.proofview p.proofview in (* spiwack: beware, the bottom of the stack is used by [Proof] internally, and should not be exposed. *) @@ -161,322 +127,261 @@ let proof { state = p } = let stack = map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack in - (goals,stack,sigma) + let shelf = p.shelf in + let given_up = p.given_up in + (goals,stack,shelf,given_up,sigma) + +type 'a pre_goals = { + fg_goals : 'a list; + (** List of the focussed goals *) + bg_goals : ('a list * 'a list) list; + (** Zipper representing the unfocussed background goals *) + shelved_goals : 'a list; + (** List of the goals on the shelf. *) + given_up_goals : 'a list; + (** List of the goals that have been given up *) +} + +let map_structured_proof pfts process_goal: 'a pre_goals = + let (goals, zipper, shelf, given_up, sigma) = proof pfts in + let fg = List.map (process_goal sigma) goals in + let map_zip (lg, rg) = + let lg = List.map (process_goal sigma) lg in + let rg = List.map (process_goal sigma) rg in + (lg, rg) + in + let bg = List.map map_zip zipper in + let shelf = List.map (process_goal sigma) shelf in + let given_up = List.map (process_goal sigma) given_up in + { fg_goals = fg; + bg_goals = bg; + shelved_goals = shelf; + given_up_goals = given_up; } 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}. *) let is_done p = - Proofview.finished p.state.proofview && - Proofview.finished (unroll_focus p.state.proofview p.state.focus_stack) + Proofview.finished p.proofview && + Proofview.finished (unroll_focus p.proofview p.focus_stack) (* spiwack: for compatibility with <= 8.2 proof engine *) let has_unresolved_evar p = - Proofview.V82.has_unresolved_evar p.state.proofview + Proofview.V82.has_unresolved_evar p.proofview (* Returns the list of partial proofs to initial goals *) -let partial_proof p = - List.map fst (Proofview.return p.state.proofview) - - +let partial_proof p = Proofview.partial_proof p.entry p.proofview (*** The following functions implement the basic internal mechanisms of proofs, they are not meant to be exported in the .mli ***) (* An auxiliary function to push a {!focus_context} on the focus stack. *) let push_focus cond inf context pr = - pr.state <- { pr.state with focus_stack = (cond,inf,context)::pr.state.focus_stack } + { pr with focus_stack = (cond,inf,context)::pr.focus_stack } -exception FullyUnfocused -let _ = Errors.register_handler begin function - | FullyUnfocused -> Util.error "The proof is not focused" - | _ -> raise Errors.Unhandled -end (* An auxiliary function to read the kind of the next focusing step *) let cond_of_focus pr = - match pr.state.focus_stack with + match pr.focus_stack with | (cond,_,_)::_ -> cond | _ -> raise FullyUnfocused (* An auxiliary function to pop and read the last {!Proofview.focus_context} on the focus stack. *) let pop_focus pr = - match pr.state.focus_stack with - | focus::other_focuses -> - pr.state <- { pr.state with focus_stack = other_focuses }; focus - | _ -> + match pr.focus_stack with + | focus::other_focuses -> + { pr with focus_stack = other_focuses }, focus + | _ -> raise FullyUnfocused -(* Auxiliary function to push a [proof_state] onto the undo stack. *) -let push_undo save pr = - match pr.transactions with - | [] -> pr.undo_stack <- save::pr.undo_stack - | stack::trans' -> pr.transactions <- (save::stack)::trans' - -(* Auxiliary function to pop and read a [save_state] from the undo stack. *) -exception EmptyUndoStack -let _ = Errors.register_handler begin function - | EmptyUndoStack -> Util.error "Cannot undo: no more undo information" - | _ -> raise Errors.Unhandled -end -let pop_undo pr = - match pr.transactions , pr.undo_stack with - | [] , state::stack -> pr.undo_stack <- stack; state - | (state::stack)::trans', _ -> pr.transactions <- stack::trans'; state - | _ -> raise EmptyUndoStack - - (* This function focuses the proof [pr] between indices [i] and [j] *) let _focus cond inf i j pr = - let (focused,context) = Proofview.focus i j pr.state.proofview in - push_focus cond inf context pr; - pr.state <- { pr.state with proofview = focused } + let focused, context = Proofview.focus i j pr.proofview in + let pr = push_focus cond inf context pr in + { pr with proofview = focused } (* This function unfocuses the proof [pr], it raises [FullyUnfocused], if the proof is already fully unfocused. This function does not care about the condition of the current focus. *) let _unfocus pr = - let (_,_,fc) = pop_focus pr in - pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview } - - -let set_used_variables l p = - p.info.section_vars <- Some l - -let get_used_variables p = p.info.section_vars - -(*** Endline tactic ***) - -(* spiwack this is an information about the UI, it might be a good idea to move - it to the Proof_global module *) - -(* Sets the tactic to be used when a tactic line is closed with [...] *) -let set_endline_tactic tac p = - p.info.endline_tactic <- tac - -let with_end_tac pr tac = - Proofview.tclTHEN tac pr.info.endline_tactic - -(*** The following functions define the safety mechanism of the - proof system, they may be unsafe if not used carefully. There is - currently no reason to export them in the .mli ***) - -(* This functions saves the current state into a [proof_state]. *) -let save_state { state = ps } = State ps - -(* This function stores the current proof state in the undo stack. *) -let save pr = - push_undo (save_state pr) pr - -(* This function restores a state, presumably from the top of the undo stack. *) -let restore_state save pr = - match save with - | State save -> pr.state <- save - | Effect undo -> undo () - -(* Interpretes the Undo command. *) -let undo pr = - (* On a single line, since the effects commute *) - restore_state (pop_undo pr) pr - -(* Adds an undo effect to the undo stack. Use it with care, errors here might result - in inconsistent states. *) -let add_undo effect pr = - push_undo (Effect effect) pr - - - -(*** Transactions ***) - -let init_transaction pr = - pr.transactions <- []::pr.transactions - -let commit_stack pr stack = - let push s = push_undo s pr in - List.iter push (List.rev stack) - -(* Invariant: [commit] should be called only when a transaction - is open. It closes the current transaction. *) -let commit pr = - match pr.transactions with - | stack::trans' -> - pr.transactions <- trans'; - commit_stack pr stack - | [] -> assert false - -(* Invariant: [rollback] should be called only when a transaction - is open. It closes the current transaction. *) -let rec rollback pr = - try - undo pr; - rollback pr - with EmptyUndoStack -> - match pr.transactions with - | []::trans' -> pr.transactions <- trans' - | _ -> assert false - - -let transaction pr t = - init_transaction pr; - try t (); commit pr - with reraise -> rollback pr; raise reraise - + let pr, (_,_,fc) = pop_focus pr in + { pr with proofview = Proofview.unfocus fc pr.proofview } (* Focus command (focuses on the [i]th subgoal) *) (* spiwack: there could also, easily be a focus-on-a-range tactic, is there a need for it? *) let focus cond inf i pr = - save pr; - _focus cond (Obj.repr inf) i i pr + try _focus cond (Obj.repr inf) i i pr + with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i)) let rec unfocus kind pr () = - let starting_point = save_state pr in let cond = cond_of_focus pr in - match fst cond kind pr.state.proofview with - | Cannot e -> raise e - | Strict -> - (_unfocus pr; - push_undo starting_point pr) + match test_cond cond kind pr.proofview with + | Cannot NotThisWay -> raise CannotUnfocusThisWay + | Cannot AlreadyNoFocus -> raise FullyUnfocused + | Strict -> + let pr = _unfocus pr in + pr | Loose -> begin try - _unfocus pr; - push_undo starting_point pr; + let pr = _unfocus pr in unfocus kind pr () with FullyUnfocused -> raise CannotUnfocusThisWay end -let unfocus kind pr = - transaction pr (unfocus kind pr) - exception NoSuchFocus (* no handler: should not be allowed to reach toplevel. *) let rec get_in_focus_stack kind stack = match stack with - | ((_,check),inf,_)::stack -> - if check kind then inf + | (cond,inf,_)::stack -> + if check_cond_kind cond kind then inf else get_in_focus_stack kind stack | [] -> raise NoSuchFocus let get_at_focus kind pr = - Obj.magic (get_in_focus_stack kind pr.state.focus_stack) + Obj.magic (get_in_focus_stack kind pr.focus_stack) let is_last_focus kind pr = - let ((_,check),_,_) = List.hd pr.state.focus_stack in - check kind + let (cond,_,_) = List.hd pr.focus_stack in + check_cond_kind cond kind let no_focused_goal p = - Proofview.finished p.state.proofview + Proofview.finished p.proofview + +let rec maximal_unfocus k p = + if no_focused_goal p then + try maximal_unfocus k (unfocus k p ()) + with FullyUnfocused | CannotUnfocusThisWay -> p + else p (*** Proof Creation/Termination ***) (* [end_of_stack] is unfocused by return to close every loose focus. *) let end_of_stack_kind = new_focus_kind () -let end_of_stack = done_cond_gen FullyUnfocused end_of_stack_kind +let end_of_stack = CondEndStack end_of_stack_kind let unfocused = is_last_focus end_of_stack_kind -let start goals = - let pr = - { state = { proofview = Proofview.init goals ; - focus_stack = [] ; - intel = Store.empty} ; - undo_stack = [] ; - transactions = [] ; - info = { endline_tactic = Proofview.tclUNIT (); - initial_conclusions = List.map snd goals; - section_vars = None } - } - in - _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr; - pr +let start sigma goals = + let entry, proofview = Proofview.init sigma goals in + let pr = { + proofview; + entry; + focus_stack = [] ; + shelf = [] ; + given_up = [] } in + _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr +let dependent_start goals = + let entry, proofview = Proofview.dependent_init goals in + let pr = { + proofview; + entry; + focus_stack = [] ; + shelf = [] ; + given_up = [] } in + let number_of_goals = List.length (Proofview.initial_goals pr.entry) in + _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr exception UnfinishedProof +exception HasShelvedGoals +exception HasGivenUpGoals exception HasUnresolvedEvar let _ = Errors.register_handler begin function - | UnfinishedProof -> Util.error "Some goals have not been solved." - | HasUnresolvedEvar -> Util.error "Some existential variables are uninstantiated." + | UnfinishedProof -> Errors.error "Some goals have not been solved." + | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf." + | HasGivenUpGoals -> Errors.error "Some goals have been given up." + | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated." | _ -> raise Errors.Unhandled end + let return p = if not (is_done p) then raise UnfinishedProof - else if has_unresolved_evar p then + else if not (CList.is_empty (p.shelf)) then + raise HasShelvedGoals + else if not (CList.is_empty (p.given_up)) then + raise HasGivenUpGoals + else if has_unresolved_evar p then (* spiwack: for compatibility with <= 8.3 proof engine *) raise HasUnresolvedEvar else - unfocus end_of_stack_kind p; - Proofview.return p.state.proofview - -(*** Function manipulation proof extra informations ***) + let p = unfocus end_of_stack_kind p () in + Proofview.return p.proofview -let get_proof_info pr = - pr.state.intel +let initial_goals p = Proofview.initial_goals p.entry -let set_proof_info info pr = - save pr; - pr.state <- { pr.state with intel=info } +let compact p = + let entry, proofview = Proofview.compact p.entry p.proofview in + { p with proofview; entry } +(*** Function manipulation proof extra informations ***) (*** Tactics ***) let run_tactic env tac pr = - let starting_point = save_state pr in - let sp = pr.state.proofview in - try - let tacticced_proofview = Proofview.apply env tac sp in - pr.state <- { pr.state with proofview = tacticced_proofview }; - push_undo starting_point pr - with reraise -> - restore_state starting_point pr; - raise reraise + let sp = pr.proofview in + let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) = + Proofview.apply env tac sp + in + let sigma = Proofview.return tacticced_proofview in + (* Already solved goals are not to be counted as shelved. Nor are + they to be marked as unresolvable. *) + let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in + let retrieved = undef (List.rev (Evd.future_goals sigma)) in + let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in + let proofview = + List.fold_left + Proofview.Unsafe.mark_as_goal + tacticced_proofview + retrieved + in + let given_up = pr.given_up@give_up in + let proofview = Proofview.Unsafe.reset_future_goals proofview in + { pr with proofview ; shelf ; given_up },(status,info_trace) (*** Commands ***) -let in_proof p k = - Proofview.in_proofview p.state.proofview k +let in_proof p k = k (Proofview.return p.proofview) +(* Remove all the goals from the shelf and adds them at the end of the + focused goals. *) +let unshelve p = + { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] } (*** Compatibility layer with <=v8.2 ***) module V82 = struct let subgoals p = - Proofview.V82.goals p.state.proofview + Proofview.V82.goals p.proofview let background_subgoals p = - Proofview.V82.goals (unroll_focus p.state.proofview p.state.focus_stack) - - let get_initial_conclusions p = - p.info.initial_conclusions - - let depth p = List.length p.undo_stack + Proofview.V82.goals (unroll_focus p.proofview p.focus_stack) - let top_goal p = - let { Evd.it=gls ; sigma=sigma } = - Proofview.V82.top_goals p.state.proofview + let top_goal p = + let { Evd.it=gls ; sigma=sigma; } = + Proofview.V82.top_goals p.entry p.proofview in - { Evd.it=List.hd gls ; sigma=sigma } + { Evd.it=List.hd gls ; sigma=sigma; } let top_evars p = - Proofview.V82.top_evars p.state.proofview + Proofview.V82.top_evars p.entry let grab_evars p = if not (is_done p) then raise UnfinishedProof else - save p; - p.state <- { p.state with proofview = Proofview.V82.grab p.state.proofview } - - - let instantiate_evar n com pr = - let starting_point = save_state pr in - let sp = pr.state.proofview in - try - let new_proofview = Proofview.V82.instantiate_evar n com sp in - pr.state <- { pr.state with proofview = new_proofview }; - push_undo starting_point pr - with reraise -> - restore_state starting_point pr; - raise reraise + { p with proofview = Proofview.V82.grab p.proofview } + + + let instantiate_evar n com pr = + let sp = pr.proofview in + let proofview = Proofview.V82.instantiate_evar n com sp in + let shelf = + List.filter begin fun g -> + Evd.is_undefined (Proofview.return proofview) g + end pr.shelf + in + { pr with proofview ; shelf } + end -- cgit v1.2.3