diff options
Diffstat (limited to 'parsing/tactic_printer.ml')
| -rw-r--r-- | parsing/tactic_printer.ml | 67 |
1 files changed, 31 insertions, 36 deletions
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 1fef688c..c5b77774 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactic_printer.ml 9593 2007-02-05 13:58:52Z corbinea $ *) +(* $Id: tactic_printer.ml 11146 2008-06-19 08:26:38Z corbinea $ *) open Pp open Util @@ -34,7 +34,7 @@ let pr_rule = function | Nested(cmpd,_) -> begin match cmpd with - Tactic (texp,_) -> hov 0 (pr_tactic texp) + | Tactic (texp,_) -> hov 0 (pr_tactic texp) | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr) end | Daimon -> str "<Daimon>" @@ -46,10 +46,20 @@ let uses_default_tac = function (* Does not print change of evars *) let pr_rule_dot = function - | Prim Change_evars -> mt () + | Prim Change_evars ->str "PC: ch_evars" ++ mt () + (* PC: this might be redundant *) | r -> pr_rule r ++ if uses_default_tac r then str "..." else str"." +let pr_rule_dot_fnl = function + | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_) + | TacMutualCofix (true,_,_))),_),_) -> + (* Very big hack to not display hidden tactics in "Theorem with" *) + (* (would not scale!) *) + mt () + | Prim Change_evars -> mt () + | r -> pr_rule_dot r ++ fnl () + exception Different (* We remove from the var context of env what is already in osign *) @@ -88,40 +98,39 @@ let rec print_decl_script tac_printer nochange sigma pf = else pr_change pf.goal) ++ fnl () - | Some (Daimon,[]) -> mt () - | Some (Prim Change_evars,[next]) -> - (* ignore evar changes *) - print_decl_script tac_printer nochange sigma next + | Some (Daimon,[]) -> str "(* Some proof has been skipped here *)" + | Some (Prim Change_evars,[subpf]) -> + print_decl_script tac_printer nochange sigma subpf | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) -> begin match instr.instr,subprfs with Pescape,[{ref=Some(_,subsubprfs)}] -> hov 7 - (pr_rule_dot rule ++ fnl () ++ + (pr_rule_dot_fnl rule ++ prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++ if opened then mt () else str "return." | Pclaim _,[body;cont] -> hov 2 - (pr_rule_dot rule ++ fnl () ++ + (pr_rule_dot_fnl rule ++ print_decl_script tac_printer nochange sigma body) ++ fnl () ++ if opened then mt () else str "end claim." ++ fnl () ++ print_decl_script tac_printer nochange sigma cont | Pfocus _,[body;cont] -> hov 2 - (pr_rule_dot rule ++ fnl () ++ + (pr_rule_dot_fnl rule ++ print_decl_script tac_printer nochange sigma body) ++ fnl () ++ if opened then mt () else str "end focus." ++ fnl () ++ print_decl_script tac_printer nochange sigma cont | (Psuppose _ |Pcase (_,_,_)),[body;cont] -> hov 2 - (pr_rule_dot rule ++ fnl () ++ + (pr_rule_dot_fnl rule ++ print_decl_script tac_printer nochange sigma body) ++ fnl () ++ print_decl_script tac_printer nochange sigma cont | _,[next] -> - pr_rule_dot rule ++ fnl () ++ + pr_rule_dot_fnl rule ++ print_decl_script tac_printer nochange sigma next | _,[] -> pr_rule_dot rule @@ -156,30 +165,28 @@ let rec print_script nochange sigma pf = (print_script nochange sigma) spfl ) | Some(rule,spfl) -> ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot rule ++ fnl () ++ + pr_rule_dot_fnl rule ++ prlist_with_sep pr_fnl (print_script nochange sigma) spfl ) (* printed by Show Script command *) let print_treescript nochange sigma pf = - let rec aux top pf = + let rec aux pf = match pf.ref with | None -> if nochange then - if pf.goal.evar_extra=None then - (str"<Your Tactic Text here>") - else (str"<Your Proof Text here>") - else - (pr_change pf.goal) + if pf.goal.evar_extra=None then str"<Your Tactic Text here>" + else str"<Your Proof Text here>" + else pr_change pf.goal | Some(Decl_proof opened,script) -> assert (List.length script = 1); begin - if nochange then (mt ()) else (pr_change pf.goal ++ fnl ()) + if nochange then mt () else pr_change pf.goal ++ fnl () end ++ hov 0 begin str "proof." ++ fnl () ++ - print_decl_script (aux false) + print_decl_script aux nochange sigma (List.hd script) end ++ fnl () ++ begin @@ -190,22 +197,10 @@ let print_treescript nochange sigma pf = prlist_with_sep pr_fnl (print_script nochange sigma) spfl ) | Some(r,spfl) -> + let indent = if List.length spfl >= 2 then 1 else 0 in (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ - begin - if List.length spfl > 1 then - fnl () ++ - str " " ++ hov 0 (aux false (List.hd spfl)) ++ fnl () ++ - hov 0 (prlist_with_sep fnl (aux false) (List.tl spfl)) - else - match spfl with - | [] -> mt () - | [spf] -> fnl () ++ - (if top then mt () else str " ") ++ aux top spf - | _ -> fnl () ++ str " " ++ - hov 0 (prlist_with_sep fnl (aux false) spfl) - end - in hov 0 (aux true pf) + hv indent (pr_rule_dot_fnl r ++ prlist_with_sep mt aux spfl) + in hov 0 (aux pf) let rec print_info_script sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in |