diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 16 | ||||
| -rw-r--r-- | proofs/proof.mli | 9 | ||||
| -rw-r--r-- | proofs/proofview.ml | 5 | ||||
| -rw-r--r-- | proofs/proofview.mli | 18 |
4 files changed, 47 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 27a65da4c7..ac61c06483 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -149,12 +149,26 @@ type proof = { (* current proof_state *) (*** 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. + doesn't hide any goal. Unfocusing is handled in {!return}. *) let is_done p = Proofview.finished p.state.proofview && diff --git a/proofs/proof.mli b/proofs/proof.mli index e162a2aa0d..d0b7e9839d 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -34,6 +34,15 @@ open Term (* Type of a proof. *) type proof +(* Returns a stylised view of a proof for use by, for instance, + ide-s. *) +(* spiwack: the type of [proof] will change as we push more refined + functions to ide-s. This would be better than spawning a new nearly + identical function everytime. Hence the generic name. *) +(* In this version: returns the focused goals, a representation of the + focus stack (the number of goals at each level) and the underlying + evar_map *) +val proof : proof -> Goal.goal list * int list * Evd.evar_map (*** General proof functions ***) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index fc752cd336..d9c62600d4 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -27,6 +27,9 @@ type proofview = { comb : Goal.goal list } +let proofview p = + p.comb , p.solution + (* Initialises a proofview, the argument is a list of environement, conclusion types, and optional names, creating that many initial goals. *) let init = @@ -94,6 +97,8 @@ let list_goto = order) *) type focus_context = Goal.goal list * Goal.goal list +let focus_context (l,r) = List.length l + List.length r + (* This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 1ae5c4fd2d..d29ab4f090 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -24,6 +24,16 @@ open Term type proofview + +(* Returns a stylised view of a proofview for use by, for instance, + ide-s. *) +(* spiwack: the type of [proofview] will change as we push more + refined functions to ide-s. This would be better than spawning a + new nearly identical function everytime. Hence the generic name. *) +(* In this version: returns the list of focused goals together with + the [evar_map] context. *) +val proofview : proofview -> Goal.goal list * Evd.evar_map + (* Initialises a proofview, the argument is a list of environement, conclusion types, creating that many initial goals. *) val init : (Environ.env * Term.types) list -> proofview @@ -46,6 +56,14 @@ exception IndexOutOfRange (* Type of the object which allow to unfocus a view.*) type focus_context +(* Returns a stylised view of a focus_context for use by, for + instance, ide-s. *) +(* spiwack: the type of [focus_context] will change as we push more + refined functions to ide-s. This would be better than spawning a + new nearly identical function everytime. Hence the generic name. *) +(* In this version: returns the number of goals that are held *) +val focus_context : focus_context -> int + (* [focus i j] focuses a proofview on the goals from index [i] to index [j] (inclusive). (i.e. goals number [i] to [j] become the only goals of the returned proofview). |