diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 112 |
1 files changed, 82 insertions, 30 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index d76bd1e2b2..5b3ead181f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -82,11 +82,10 @@ let pr_econstr_n_core goal_concl_style env sigma n t = pr_constr_expr_n n (extern_constr goal_concl_style env sigma t) let pr_econstr_core goal_concl_style env sigma t = pr_constr_expr (extern_constr goal_concl_style env sigma t) -let pr_leconstr_core goal_concl_style env sigma t = - pr_lconstr_expr (extern_constr goal_concl_style env sigma t) +let pr_leconstr_core = Proof_diffs.pr_leconstr_core let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c) -let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) +let pr_lconstr_env = Proof_diffs.pr_lconstr_env let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c) let _ = Hook.set Refine.pr_constr pr_constr_env @@ -133,8 +132,7 @@ let pr_lconstr_under_binders c = let pr_etype_core goal_concl_style env sigma t = pr_constr_expr (extern_type goal_concl_style env sigma t) -let pr_letype_core goal_concl_style env sigma t = - pr_lconstr_expr (extern_type goal_concl_style env sigma t) +let pr_letype_core = Proof_diffs.pr_letype_core let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c) let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c) @@ -290,11 +288,13 @@ let pr_cumulativity_info sigma cumi = let pr_global_env = pr_global_env let pr_global = pr_global_env Id.Set.empty -let pr_puniverses f env (c,u) = - f env c ++ - (if !Constrextern.print_universes then - str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" - else mt ()) +let pr_universe_instance evd inst = + str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" + +let pr_puniverses f env sigma (c,u) = + if !Constrextern.print_universes + then f env c ++ pr_universe_instance sigma u + else f env c let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) let pr_existential_key = Termops.pr_existential_key @@ -493,16 +493,23 @@ let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) -(* display complete goal *) -let pr_goal gs = +(* display complete goal + prev_gs has info on the previous proof step for diffs + gs has info on the current proof step + *) +let pr_goal ?(diffs=false) ?prev_gs gs = let g = sig_it gs in let sigma = project gs in let env = Goal.V82.env sigma g in let concl = Goal.V82.concl sigma g in let goal = - pr_context_of env sigma ++ cut () ++ - str "============================" ++ cut () ++ - pr_goal_concl_style_env env sigma concl in + if diffs then + Proof_diffs.diff_goals ?prev_gs (Some gs) + else + pr_context_of env sigma ++ cut () ++ + str "============================" ++ cut () ++ + pr_goal_concl_style_env env sigma concl + in str " " ++ v 0 goal (* display a goal tag *) @@ -695,7 +702,8 @@ let print_dependent_evars gl sigma seeds = (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) -let pr_subgoals ?(pr_first=true) +(* [prev] is the previous proof step, used for diffs *) +let pr_subgoals ?(pr_first=true) ?(diffs=false) ?prev close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals = (** Printing functions for the extra informations. *) let rec print_stack a = function @@ -729,7 +737,7 @@ let pr_subgoals ?(pr_first=true) if needed then str" focused " else str" " (* non-breakable space *) in - (** Main function *) + let rec pr_rec n = function | [] -> (mt ()) | g::rest -> @@ -739,7 +747,14 @@ let pr_subgoals ?(pr_first=true) in let print_multiple_goals g l = if pr_first then - pr_goal { it = g ; sigma = sigma; } + let prev_gs = + match prev with + | Some (prev_goals, prev_sigma) -> + if prev_goals = [] then None + else Some { it = List.hd prev_goals; sigma = prev_sigma} + | None -> None + in + pr_goal ~diffs ?prev_gs { it = g ; sigma = sigma } ++ (if l=[] then mt () else cut ()) ++ pr_rec 2 l else @@ -751,6 +766,8 @@ let pr_subgoals ?(pr_first=true) | Some cmd -> Feedback.msg_info cmd | None -> () in + + (** Main function *) match goals with | [] -> begin @@ -780,7 +797,7 @@ let pr_subgoals ?(pr_first=true) ++ print_dependent_evars (Some g1) sigma seeds ) -let pr_open_subgoals ~proof = +let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?prev_proof proof = (* 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 @@ -803,21 +820,33 @@ let pr_open_subgoals ~proof = fnl () ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf | _ , _, _ -> - let end_cmd = - str "This subproof is complete, but there are some unfocused goals." ++ - (let s = Proof_bullet.suggest p in - if Pp.ismt s then s else fnl () ++ s) ++ - fnl () + let cmd = if quiet then None else + Some + (str "This subproof is complete, but there are some unfocused goals." ++ + (let s = Proof_bullet.suggest p in + if Pp.ismt s then s else fnl () ++ s) ++ + fnl ()) in - pr_subgoals ~pr_first:false (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals + pr_subgoals ~pr_first:false cmd bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals end | _ -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in - pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused + let prev = match prev_proof with + | Some op -> + let (ogoals , _, _, _, _) = Proof.proof op in + let { Evd.it = obgoals; sigma = osigma } = Proof.V82.background_subgoals op in + let obgoals_focused = List.filter (fun x -> List.mem x ogoals) obgoals in + Some (obgoals_focused, osigma) + | None -> None + in + pr_subgoals ~pr_first:true ~diffs ?prev None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused end +let pr_open_subgoals ~proof = + pr_open_subgoals_diff proof + let pr_nth_open_subgoal ~proof n = let gls,_,_,_,sigma = Proof.proof proof in pr_subgoal n sigma gls @@ -852,7 +881,7 @@ type axiom = type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Axiom of axiom * (Label.t * Constr.rel_context * types) list | Opaque of Constant.t (* An opaque constant. *) | Transparent of Constant.t @@ -987,6 +1016,29 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () -let pr_universe_instance evd ctx = - let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" +(* print the proof step, possibly with diffs highlighted, *) +let print_and_diff oldp newp = + match newp with + | None -> () + | Some proof -> + let output = + if Proof_diffs.show_diffs () then + try pr_open_subgoals_diff ~diffs:true ?prev_proof:oldp proof + with Pp_diff.Diff_Failure msg -> begin + (* todo: print the unparsable string (if we know it) *) + Feedback.msg_warning Pp.(str ("Diff failure:" ^ msg ^ "; showing results without diff highlighting" )); + pr_open_subgoals ~proof + end + else + pr_open_subgoals ~proof + in + Feedback.msg_notice output;; + +(* Do diffs on the first goal returning a Pp. *) +let diff_pr_open_subgoals ?(quiet=false) o_proof n_proof = + match n_proof with + | None -> Pp.mt () + | Some proof -> + try pr_open_subgoals_diff ~quiet ~diffs:true ?prev_proof:o_proof proof + with Pp_diff.Diff_Failure _ -> pr_open_subgoals ~proof + (* todo: print the unparsable string (if we know it) *) |