diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 141 |
1 files changed, 124 insertions, 17 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2324e3e9..fe6bf7db 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -72,10 +72,59 @@ let show_node () = could, possibly, be cleaned away. (Feb. 2010) *) () +(* indentation code for Show Script, initially contributed + by D. de Rauglaudre *) + +let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = + (* ng1 : number of goals remaining at the current level (before cmd) + ngl1 : stack of previous levels with their remaining goals + ng : number of goals after the execution of cmd + beginend : special indentation stack for { } *) + let ngprev = List.fold_left (+) ng1 ngl1 in + let new_ngl = + if ng > ngprev then + (* We've branched *) + (ng - ngprev + 1, ng1 - 1 :: ngl1) + else if ng < ngprev then + (* A subgoal have been solved. Let's compute the new current level + by discarding all levels with 0 remaining goals. *) + let _ = assert (ng = ngprev - 1) in + let rec loop = function + | (0, ng2::ngl2) -> loop (ng2,ngl2) + | p -> p + in loop (ng1-1, ngl1) + else + (* Standard case, same goal number as before *) + (ng1, ngl1) + in + (* When a subgoal have been solved, separate this block by an empty line *) + let new_nl = (ng < ngprev) + in + (* Indentation depth *) + let ind = List.length ngl1 + in + (* Some special handling of bullets and { }, to get a nicer display *) + let pred n = max 0 (n-1) in + let ind, nl, new_beginend = match cmd with + | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend + | VernacEndSubproof -> List.hd beginend, false, List.tl beginend + | VernacBullet _ -> pred ind, nl, beginend + | _ -> ind, nl, beginend + in + let pp = + (if nl then fnl () else mt ()) ++ + (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) + in + (new_ngl, new_nl, new_beginend, pp :: ppl) + let show_script () = let prf = Pfedit.get_current_proof_name () in let cmds = Backtrack.get_script prf in - msgnl (Util.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds) + let _,_,_,indented_cmds = + List.fold_left indent_script_item ((1,[]),false,[],[]) cmds + in + let indented_cmds = List.rev (indented_cmds) in + msgnl (v 0 (Util.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) let show_thesis () = msgnl (anomaly "TODO" ) @@ -311,6 +360,11 @@ let smart_global r = Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr; gr +let dump_global r = + try + let gr = Smartlocate.smart_global r in + Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr + with _ -> () (**********) (* Syntax *) @@ -389,8 +443,10 @@ let vernac_end_proof = function let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) - by (Tactics.exact_proof c); - save_named true + let prf = Pfedit.get_current_proof_name () in + by (Tactics.exact_proof c); + save_named true; + Backtrack.mark_unreachable [prf] let vernac_assumption kind l nl= let global = fst kind = Global in @@ -458,9 +514,21 @@ let vernac_cofixpoint l = List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; do_cofixpoint l -let vernac_scheme = Indschemes.do_scheme - -let vernac_combined_scheme = Indschemes.do_combined_scheme +let vernac_scheme l = + if Dumpglob.dump () then + List.iter (fun (lid, s) -> + Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid; + match s with + | InductionScheme (_, r, _) + | CaseScheme (_, r, _) + | EqualityScheme r -> dump_global r) l; + Indschemes.do_scheme l + +let vernac_combined_scheme lid l = + if Dumpglob.dump () then + (Dumpglob.dump_definition lid false "def"; + List.iter (fun lid -> dump_global (Genarg.AN (Ident lid))) l); + Indschemes.do_combined_scheme lid l (**********************) (* Modules *) @@ -1190,6 +1258,7 @@ let vernac_check_may_eval redexp glopt rc = if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> + Tacinterp.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in let redfun = fst (reduction_of_red_expr r_interp) in if !pcoq <> None @@ -1248,8 +1317,10 @@ let vernac_print = function pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) | PrintVisibility s -> pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) - | PrintAbout qid -> msg (print_about qid) - | PrintImplicit qid -> msg (print_impargs qid) + | PrintAbout qid -> + msg (print_about qid) + | PrintImplicit qid -> + dump_global qid; msg (print_impargs qid) | PrintAssumptions (o,r) -> (* Prints all the axioms and section variables used by a term *) let cstr = constr_of_global (smart_global r) in @@ -1340,10 +1411,43 @@ let vernac_back n = with Backtrack.Invalid -> error "Invalid backtrack." let vernac_reset_name id = - try Backtrack.reset_name id; try_print_subgoals () - with Backtrack.Invalid -> error "Invalid Reset." + try + let globalized = + try + let gr = Smartlocate.global_with_alias (Ident id) in + Dumpglob.add_glob (fst id) gr; + true + with _ -> false in + + if not globalized then begin + try begin match Lib.find_opening_node (snd id) with + | Lib.OpenedSection _ -> Dumpglob.dump_reference (fst id) + (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; + (* Might be nice to implement module cases, too.... *) + | _ -> () + end with UserError _ -> () + end; -let vernac_reset_initial () = Backtrack.reset_initial () + if Backtrack.is_active () then + (Backtrack.reset_name id; try_print_subgoals ()) + else + (* When compiling files, Reset is now allowed again + as asked by A. Chlipala. we emulate a simple reset, + that discards all proofs. *) + let lbl = Lib.label_before_name id in + Pfedit.delete_all_proofs (); + Pp.msg_warning (str "Reset command occurred in non-interactive mode."); + Lib.reset_label lbl + with Backtrack.Invalid | Not_found -> error "Invalid Reset." + + +let vernac_reset_initial () = + if Backtrack.is_active () then + Backtrack.reset_initial () + else begin + Pp.msg_warning (str "Reset command occurred in non-interactive mode."); + Lib.reset_label Lib.first_command_label + end (* For compatibility with ProofGeneral: *) @@ -1393,7 +1497,10 @@ let vernac_undoto n = let vernac_focus gln = let p = Proof_global.give_me_the_proof () in let n = match gln with None -> 1 | Some n -> n in - Proof.focus focus_command_cond () n p; print_subgoals () + if n = 0 then + Util.error "Invalid goal number: 0. Goal numbering starts with 1." + else + Proof.focus focus_command_cond () n p; print_subgoals () (* Unfocuses one step in the focus stack. *) let vernac_unfocus () = @@ -1594,11 +1701,11 @@ let interp c = match c with | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, None) -> () - | VernacProof (Some tac, None) -> vernac_set_end_tac tac - | VernacProof (None, Some l) -> vernac_set_used_variables l + | VernacProof (None, None) -> print_subgoals () + | VernacProof (Some tac, None) -> vernac_set_end_tac tac ; print_subgoals () + | VernacProof (None, Some l) -> vernac_set_used_variables l ; print_subgoals () | VernacProof (Some tac, Some l) -> - vernac_set_end_tac tac; vernac_set_used_variables l + vernac_set_end_tac tac; vernac_set_used_variables l ; print_subgoals () | VernacProofMode mn -> Proof_global.set_proof_mode mn (* Toplevel control *) | VernacToplevelControl e -> raise e |