summaryrefslogtreecommitdiff
path: root/proofs/proof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof.ml')
-rw-r--r--proofs/proof.ml482
1 files changed, 482 insertions, 0 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
new file mode 100644
index 00000000..012a4dc1
--- /dev/null
+++ b/proofs/proof.ml
@@ -0,0 +1,482 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* Module defining the last essential tiles of interactive proofs.
+ The features of the Proof module are undoing and focusing.
+ A proof is a mutable object, it contains a proofview, and some information
+ to be able to undo actions, and to unfocus the current view. All three
+ of these being meant to evolve.
+ - Proofview: a proof is primarily the data of the current view.
+ That which is shown to the user (as a remainder, a proofview
+ is mainly the logical state of the proof, together with the
+ currently focused goals).
+ - Focus: a proof has a focus stack: the top of the stack contains
+ the context in which to unfocus the current view to a view focused
+ with the rest of the stack.
+ In addition, this contains, for each of the focus context, a
+ "focus kind" and a "focus condition" (in practice, and for modularity,
+ the focus kind is actually stored inside the condition). To unfocus, one
+ needs to know the focus kind, and the condition (for instance "no condition" or
+ the proof under focused must be complete) must be met.
+ - Undo: since proofviews and focus stacks are immutable objects,
+ it could suffice to hold the previous states, to allow to return to the past.
+ However, we also allow other modules to do actions that can be undone.
+ Therefore the undo stack stores action to be ran to undo.
+*)
+
+open Term
+
+type _focus_kind = int
+type 'a focus_kind = _focus_kind
+type focus_info = Obj.t
+type unfocusable =
+ | Cannot of exn
+ | Loose
+ | Strict
+type _focus_condition =
+ (_focus_kind -> Proofview.proofview -> unfocusable) *
+ (_focus_kind -> bool)
+type 'a focus_condition = _focus_condition
+
+let next_kind = ref 0
+let new_focus_kind () =
+ let r = !next_kind in
+ 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
+let _ = Errors.register_handler begin function
+ | CannotUnfocusThisWay ->
+ Util.error "This proof is focused, but cannot be unfocused this way"
+ | _ -> 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
+
+
+(* Subpart of the type of proofs. It contains the parts of the proof which
+ are under control of the undo mechanism *)
+type proof_state = {
+ (* Current focused proofview *)
+ proofview: Proofview.proofview;
+ (* 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
+}
+
+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 (goals,sigma) = Proofview.proofview p.proofview in
+ (* spiwack: beware, the bottom of the stack is used by [Proof]
+ internally, and should not be exposed. *)
+ let rec map_minus_one f = function
+ | [] -> assert false
+ | [_] -> []
+ | a::l -> f a :: (map_minus_one f l)
+ in
+ let stack =
+ map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack
+ in
+ (goals,stack,sigma)
+
+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)
+
+(* spiwack: for compatibility with <= 8.2 proof engine *)
+let has_unresolved_evar p =
+ Proofview.V82.has_unresolved_evar p.state.proofview
+
+(* Returns the list of partial proofs to initial goals *)
+let partial_proof p =
+ List.map fst (Proofview.return p.state.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 }
+
+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
+ | (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
+ | _ ->
+ 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 }
+
+(* 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
+
+
+(* 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
+
+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)
+ | Loose ->
+ begin try
+ _unfocus pr;
+ push_undo starting_point pr;
+ 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
+ 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)
+
+let is_last_focus kind pr =
+ let ((_,check),_,_) = List.hd pr.state.focus_stack in
+ check kind
+
+let no_focused_goal p =
+ Proofview.finished p.state.proofview
+
+(*** 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 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
+
+exception UnfinishedProof
+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."
+ | _ -> raise Errors.Unhandled
+end
+let return p =
+ if not (is_done p) then
+ raise UnfinishedProof
+ 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 get_proof_info pr =
+ pr.state.intel
+
+let set_proof_info info pr =
+ save pr;
+ pr.state <- { pr.state with intel=info }
+
+
+(*** 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
+
+(*** Commands ***)
+
+let in_proof p k =
+ Proofview.in_proofview p.state.proofview k
+
+
+(*** Compatibility layer with <=v8.2 ***)
+module V82 = struct
+ let subgoals p =
+ Proofview.V82.goals p.state.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
+
+ let top_goal p =
+ let { Evd.it=gls ; sigma=sigma } =
+ Proofview.V82.top_goals p.state.proofview
+ in
+ { Evd.it=List.hd gls ; sigma=sigma }
+
+ let top_evars p =
+ Proofview.V82.top_evars p.state.proofview
+
+ 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
+end
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 03:50:28 +0000