diff options
| -rw-r--r-- | printing/printer.ml | 84 | ||||
| -rw-r--r-- | printing/printer.mli | 4 | ||||
| -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 |
6 files changed, 105 insertions, 31 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index d51174a42..0386fc652 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -354,8 +354,23 @@ let emacs_print_dependent_evars sigma seeds = (* Print open subgoals. Checks for uninstantiated existential variables *) (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) -let default_pr_subgoals close_cmd sigma seeds = function - | [] -> +let default_pr_subgoals close_cmd sigma seeds stack goals = + let rec print_stack a = function + | [] -> Pp.int a + | b::l -> Pp.int a ++ str"-" ++ print_stack b l + in + let print_unfocused a l = + str"unfocused: " ++ print_stack a l + in + let rec pr_rec n = function + | [] -> (mt ()) + | g::rest -> + let pc = pr_concl n sigma g in + let prest = pr_rec (n+1) rest in + (cut () ++ pc ++ prest) + in + match goals,stack with + | [],_ -> begin match close_cmd with Some cmd -> @@ -363,30 +378,29 @@ let default_pr_subgoals close_cmd sigma seeds = function str ".") | None -> let exl = Evarutil.non_instantiated sigma in - if exl = [] then - (str"No more subgoals." - ++ emacs_print_dependent_evars sigma seeds) - else - let pei = pr_evars_int 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + if exl = [] then + (str"No more subgoals." + ++ emacs_print_dependent_evars sigma seeds) + else + let pei = pr_evars_int 1 exl in + (str "No more subgoals but non-instantiated existential " ++ + str "variables:" ++ fnl () ++ (hov 0 pei) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + str "You can use Grab Existential Variables.") end - | [g] -> + | [g],[] -> + let pg = default_pr_goal { it = g ; sigma = sigma } in + v 0 ( + str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg + ++ emacs_print_dependent_evars sigma seeds + ) + | [g],a::l -> let pg = default_pr_goal { it = g ; sigma = sigma } in v 0 ( - str ("1 "^"subgoal") ++ pr_goal_tag g ++ cut () ++ pg + str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg ++ emacs_print_dependent_evars sigma seeds ) - | g1::rest -> - let rec pr_rec n = function - | [] -> (mt ()) - | g::rest -> - let pc = pr_concl n sigma g in - let prest = pr_rec (n+1) rest in - (cut () ++ pc ++ prest) - in + | g1::rest,[] -> let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in let prest = pr_rec 2 rest in v 0 ( @@ -395,13 +409,23 @@ let default_pr_subgoals close_cmd sigma seeds = function ++ pg1 ++ prest ++ emacs_print_dependent_evars sigma seeds ) + | g1::rest,a::l -> + let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in + let prest = pr_rec 2 rest in + v 0 ( + int(List.length rest+1) ++ str" focused subgoals (" ++ + print_unfocused a l ++ str")" ++ cut () ++ + str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut () + ++ pg1 ++ prest + ++ emacs_print_dependent_evars sigma seeds + ) (**********************************************************************) (* Abstraction layer *) type printer_pr = { - pr_subgoals : string option -> evar_map -> evar list -> goal list -> std_ppcmds; + pr_subgoals : string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; } @@ -424,16 +448,20 @@ let pr_goal x = !printer_pr.pr_goal x (**********************************************************************) let pr_open_subgoals () = + (* spiwack: it shouldn't be the job of the printer to look up stuff + in the [evar_map], I did stuff that way because it was more + straightforward, but seriously, [Proof.proof] should return + [evar_info]-s instead. *) let p = Proof_global.give_me_the_proof () in - let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in + let (goals , stack , sigma ) = Proof.proof p in let seeds = Proof.V82.top_evars p in begin match goals with | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in - begin match bgoals with - | [] -> pr_subgoals None sigma seeds goals - | _ -> str"This subproof is complete, but there are still unfocused goals." ++ fnl () ++ fnl () ++ pr_subgoals None bsigma seeds bgoals - end - | _ -> pr_subgoals None sigma seeds goals + begin match bgoals with + | [] -> pr_subgoals None sigma seeds stack goals + | _ -> str"This subproof is complete, but there are still unfocused goals." ++ fnl () ++ fnl () ++ pr_subgoals None bsigma seeds [] bgoals + end + | _ -> pr_subgoals None sigma seeds stack goals end let pr_nth_open_subgoal n = diff --git a/printing/printer.mli b/printing/printer.mli index 3b9ef8ecc..83155fbc3 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -104,7 +104,7 @@ val pr_transparent_state : transparent_state -> std_ppcmds (** Proofs *) val pr_goal : goal sigma -> std_ppcmds -val pr_subgoals : string option -> evar_map -> evar list -> goal list -> std_ppcmds +val pr_subgoals : string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds val pr_concl : int -> evar_map -> goal -> std_ppcmds @@ -141,7 +141,7 @@ val pr_assumptionset : val pr_goal_by_id : string -> std_ppcmds type printer_pr = { - pr_subgoals : string option -> evar_map -> evar list -> goal list -> std_ppcmds; + pr_subgoals : string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; };; diff --git a/proofs/proof.ml b/proofs/proof.ml index 27a65da4c..ac61c0648 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 e162a2aa0..d0b7e9839 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 fc752cd33..d9c62600d 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 1ae5c4fd2..d29ab4f09 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). |