diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 131 |
1 files changed, 6 insertions, 125 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index acdc302af..1cd343e38 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -884,129 +884,13 @@ let rec top_of_tree pts = if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) +(* Change evars *) +let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} + (* Pretty-printers. *) -open Pp - -let pr_tactic = function - | Tacexpr.TacArg (Tacexpr.Tacexp t) -> - if !Options.v7 then - Pptactic.pr_glob_tactic t (*top tactic from tacinterp*) - else - Pptacticnew.pr_glob_tactic (Global.env()) t - | t -> - if !Options.v7 then - Pptactic.pr_tactic t - else - Pptacticnew.pr_tactic (Global.env()) t - -let pr_rule = function - | Prim r -> hov 0 (pr_prim_rule r) - | Tactic (texp,_) -> hov 0 (pr_tactic texp) - | Change_evars -> - (* This is internal tactic and cannot be replayed at user-level. - Function pr_rule_dot below is used when we want to hide - Change_evars *) - str "Evar change" - -(* Does not print change of evars *) -let pr_rule_dot = function - | Change_evars -> mt () - | r -> pr_rule r ++ str"." - -exception Different - -(* We remove from the var context of env what is already in osign *) -let thin_sign osign sign = - Sign.fold_named_context - (fun (id,c,ty as d) sign -> - try - if Sign.lookup_named id osign = (id,c,ty) then sign - else raise Different - with Not_found | Different -> add_named_decl d sign) - sign ~init:empty_named_context - -let rec print_proof sigma osign pf = - let {evar_hyps=hyps; evar_concl=cl; - evar_body=body} = pf.goal in - let hyps' = thin_sign osign hyps in - match pf.ref with - | None -> - hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) - | Some(r,spfl) -> - hov 0 - (hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++ - spc () ++ str" BY " ++ - hov 0 (pr_rule r) ++ fnl () ++ - str" " ++ - hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl) -) - -let pr_change gl = - (str"Change " ++ Printer.prterm_env (Global.env()) gl.evar_concl ++ str".") - -let rec print_script nochange sigma osign pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - match pf.ref with - | None -> - (if nochange then - (str"<Your Tactic Text here>") - else - pr_change pf.goal) - ++ fnl () - | Some(r,spfl) -> - ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ fnl () ++ - prlist_with_sep pr_fnl - (print_script nochange sigma sign) spfl) - -(* printed by Show Script command *) -let print_treescript nochange sigma _osign pf = - let rec aux top pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - match pf.ref with - | None -> - if nochange then - (str"<Your Tactic Text here>") - else - (pr_change pf.goal) - | Some(r,spfl) -> - (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ - 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) - in hov 0 (aux true pf) - -let rec print_info_script sigma osign pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - match pf.ref with - | None -> (mt ()) - | Some(Change_evars,[spf]) -> - print_info_script sigma osign spf - | Some(r,spfl) -> - (pr_rule r ++ - match spfl with - | [pf1] -> - if pf1.ref = None then - (str "." ++ fnl ()) - else - (str";" ++ brk(1,3) ++ - print_info_script sigma sign pf1) - | _ -> (str"." ++ fnl () ++ - prlist_with_sep pr_fnl - (print_info_script sigma sign) spfl)) - -let format_print_info_script sigma osign pf = - hov 0 (print_info_script sigma osign pf) - -let print_subscript sigma sign pf = - if is_tactic_proof pf then - format_print_info_script sigma sign (subproof_of_proof pf) - else - format_print_info_script sigma sign pf +let pp_info = ref (fun _ _ _ -> assert false) +let set_info_printer f = pp_info := f let tclINFO (tac : tactic) gls = let (sgl,v) as res = tac gls in @@ -1014,11 +898,8 @@ let tclINFO (tac : tactic) gls = let pf = v (List.map leaf (sig_it sgl)) in let sign = (sig_it gls).evar_hyps in msgnl (hov 0 (str" == " ++ - print_subscript (sig_sig gls) sign pf)) + !pp_info (sig_sig gls) sign pf)) with e when catchable_exception e -> msgnl (hov 0 (str "Info failed to apply validation")) end; res - -(* Change evars *) -let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} |