summaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printer.ml')
-rw-r--r--printing/printer.ml217
1 files changed, 129 insertions, 88 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 199aa79c..b4038e0f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -82,24 +82,23 @@ 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
let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c)
let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c)
-let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c
-let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c
-
let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c
let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c
let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
+let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c
+let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma c
+
(* NB do not remove the eta-redexes! Global.env() has side-effects... *)
let pr_lconstr t =
let (sigma, env) = Pfedit.get_current_context () in
@@ -108,12 +107,12 @@ let pr_constr t =
let (sigma, env) = Pfedit.get_current_context () in
pr_constr_env env sigma t
-let pr_open_lconstr (_,c) = pr_lconstr c
-let pr_open_constr (_,c) = pr_constr c
-
let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c)
let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c)
+let pr_open_lconstr (_,c) = pr_leconstr c
+let pr_open_constr (_,c) = pr_econstr c
+
let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
(* Warning: clashes can occur with variables of same name in env but *)
(* we also need to preserve the actual names of the patterns *)
@@ -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)
@@ -194,7 +192,7 @@ let pr_constr_pattern t =
let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
-let _ = Termops.set_print_constr
+let _ = Termops.Internal.set_print_constr
(fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
@@ -229,15 +227,15 @@ let dirpath_of_global = function
dirpath_of_mp (MutInd.modpath kn)
| VarRef _ -> DirPath.empty
-let qualid_of_global env r =
- Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+let qualid_of_global ?loc env r =
+ Libnames.make_qualid ?loc (dirpath_of_global r) (id_of_global env r)
let safe_gen f env sigma c =
let orig_extern_ref = Constrextern.get_extern_reference () in
let extern_ref ?loc vars r =
try orig_extern_ref vars r
with e when CErrors.noncritical e ->
- CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r)
+ qualid_of_global ?loc env r
in
Constrextern.set_extern_reference extern_ref;
try
@@ -290,17 +288,19 @@ 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 Universes.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
let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev)
-let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind)
-let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr)
+let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (mkConstruct cstr)
let pr_pconstant = pr_puniverses pr_constant
let pr_pinductive = pr_puniverses pr_inductive
@@ -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 default_pr_goal gs =
- let g = sig_it gs in
- let sigma = project gs in
+(* display complete goal
+ og_s has goal+sigma on the previous proof step for diffs
+ g_s has goal+sigma on the current proof step
+ *)
+let pr_goal ?(diffs=false) ?og_s g_s =
+ let g = sig_it g_s in
+ let sigma = project g_s 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_goal ?og_s g sigma
+ 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 *)
@@ -518,13 +525,18 @@ let pr_goal_name sigma g =
let pr_goal_header nme sigma g =
let (g,sigma) = Goal.V82.nf_evar sigma g in
str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
- ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
+ ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
(* display the conclusion of a goal *)
-let pr_concl n sigma g =
+let pr_concl n ?(diffs=false) ?og_s sigma g =
let (g,sigma) = Goal.V82.nf_evar sigma g in
let env = Goal.V82.env sigma g in
- let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
+ let pc =
+ if diffs then
+ Proof_diffs.diff_concl ?og_s sigma g
+ else
+ pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
+ in
let header = pr_goal_header (int n) sigma g in
header ++ str " is:" ++ cut () ++ str" " ++ pc
@@ -541,12 +553,12 @@ let pr_evgl_sign sigma evi =
if List.is_empty ids then mt () else
(str " (" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
in
- let pc = pr_lconstr_env env sigma evi.evar_concl in
+ let pc = pr_leconstr_env env sigma evi.evar_concl in
let candidates =
match evi.evar_body, evi.evar_candidates with
| Evar_empty, Some l ->
spc () ++ str "= {" ++
- prlist_with_sep (fun () -> str "|") (pr_lconstr_env env sigma) l ++ str "}"
+ prlist_with_sep (fun () -> str "|") (pr_leconstr_env env sigma) l ++ str "}"
| _ ->
mt ()
in
@@ -591,11 +603,11 @@ let pr_ne_evar_set hd tl sigma l =
mt ()
let pr_selected_subgoal name sigma g =
- let pg = default_pr_goal { sigma=sigma ; it=g; } in
+ let pg = pr_goal { sigma=sigma ; it=g; } in
let header = pr_goal_header name sigma g in
v 0 (header ++ str " is:" ++ cut () ++ pg)
-let default_pr_subgoal n sigma =
+let pr_subgoal n sigma =
let rec prrec p = function
| [] -> user_err Pp.(str "No such goal.")
| g::rest ->
@@ -622,8 +634,8 @@ let print_evar_constraints gl sigma =
end
in
let pr_evconstr (pbty,env,t1,t2) =
- let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1)
- and t2 = Evarutil.nf_evar sigma (EConstr.of_constr t2) in
+ let t1 = Evarutil.nf_evar sigma t1
+ and t2 = Evarutil.nf_evar sigma t2 in
let env =
(** We currently allow evar instances to refer to anonymous de Bruijn
indices, so we protect the error printing code in this case by giving
@@ -691,12 +703,25 @@ let print_dependent_evars gl sigma seeds =
in
constraints ++ evars ()
+module GoalMap = Evar.Map
+
(* Print open subgoals. Checks for uninstantiated existential variables *)
(* 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 default_pr_subgoals ?(pr_first=true)
+(* [os_map] is derived from the previous proof step, used for diffs *)
+let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals =
+ let diff_goal_map =
+ match os_map with
+ | Some (_, diff_goal_map) -> diff_goal_map
+ | None -> GoalMap.empty
+ in
+
+ let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
+ try GoalMap.find ng diff_goal_map with Not_found -> ng
+ in
+
(** Printing functions for the extra informations. *)
let rec print_stack a = function
| [] -> Pp.int a
@@ -729,17 +754,24 @@ let default_pr_subgoals ?(pr_first=true)
if needed then str" focused "
else str" " (* non-breakable space *)
in
- (** Main function *)
+
+ let get_ogs g =
+ match os_map with
+ | Some (osigma, _) -> Some { it = map_goal_for_diff g; sigma = osigma }
+ | None -> None
+ in
let rec pr_rec n = function
| [] -> (mt ())
| g::rest ->
- let pc = pr_concl n sigma g in
+ let og_s = get_ogs g in
+ let pc = pr_concl n ~diffs ?og_s sigma g in
let prest = pr_rec (n+1) rest in
(cut () ++ pc ++ prest)
in
let print_multiple_goals g l =
if pr_first then
- default_pr_goal { it = g ; sigma = sigma; }
+ let og_s = get_ogs g in
+ pr_goal ~diffs ?og_s { it = g ; sigma = sigma }
++ (if l=[] then mt () else cut ())
++ pr_rec 2 l
else
@@ -751,6 +783,8 @@ let default_pr_subgoals ?(pr_first=true)
| Some cmd -> Feedback.msg_info cmd
| None -> ()
in
+
+ (** Main function *)
match goals with
| [] ->
begin
@@ -780,34 +814,7 @@ let default_pr_subgoals ?(pr_first=true)
++ print_dependent_evars (Some g1) sigma seeds
)
-(**********************************************************************)
-(* Abstraction layer *)
-
-
-type printer_pr = {
- pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t;
- pr_subgoal : int -> evar_map -> goal list -> Pp.t;
- pr_goal : goal sigma -> Pp.t;
-}
-
-let default_printer_pr = {
- pr_subgoals = default_pr_subgoals;
- pr_subgoal = default_pr_subgoal;
- pr_goal = default_pr_goal;
-}
-
-let printer_pr = ref default_printer_pr
-
-let set_printer_pr = (:=) printer_pr
-
-let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x
-let pr_subgoal x = !printer_pr.pr_subgoal x
-let pr_goal x = !printer_pr.pr_goal x
-
-(* End abstraction layer *)
-(**********************************************************************)
-
-let pr_open_subgoals ~proof =
+let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof 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
@@ -830,21 +837,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 os_map = match oproof with
+ | Some op when diffs ->
+ let (_,_,_,_, osigma) = Proof.proof op in
+ let diff_goal_map = Proof_diffs.make_goal_map oproof proof in
+ Some (osigma, diff_goal_map)
+ | _ -> None
+ in
+ pr_subgoals ~pr_first:true ~diffs ?os_map 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
@@ -879,7 +898,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
@@ -925,11 +944,18 @@ let pr_assumptionset env sigma s =
let safe_pr_constant env kn =
try pr_constant env kn
with Not_found ->
+ (* FIXME? *)
let mp,_,lab = Constant.repr3 kn in
str (ModPath.to_string mp) ++ str "." ++ Label.print lab
in
- let safe_pr_ltype typ =
- try str " : " ++ pr_ltype typ
+ let safe_pr_inductive env kn =
+ try pr_inductive env (kn,0)
+ with Not_found ->
+ (* FIXME? *)
+ MutInd.print kn
+ in
+ let safe_pr_ltype env sigma typ =
+ try str " : " ++ pr_ltype_env env sigma typ
with e when CErrors.noncritical e -> mt ()
in
let safe_pr_ltype_relctx (rctx, typ) =
@@ -940,9 +966,9 @@ let pr_assumptionset env sigma s =
let pr_axiom env ax typ =
match ax with
| Constant kn ->
- safe_pr_constant env kn ++ safe_pr_ltype typ
+ safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
| Positive m ->
- hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.")
+ hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.")
| Guarded kn ->
hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
in
@@ -950,7 +976,7 @@ let pr_assumptionset env sigma s =
let (v, a, o, tr) = accu in
match t with
| Variable id ->
- let var = pr_id id ++ str " : " ++ pr_ltype typ in
+ let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in
(var :: v, a, o, tr)
| Axiom (axiom, []) ->
let ax = pr_axiom env axiom typ in
@@ -964,10 +990,10 @@ let pr_assumptionset env sigma s =
l in
(v, ax :: a, o, tr)
| Opaque kn ->
- let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
+ let opq = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
(v, a, opq :: o, tr)
| Transparent kn ->
- let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in
+ let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
(v, a, o, tran :: tr)
in
let (vars, axioms, opaque, trans) =
@@ -1014,6 +1040,21 @@ 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 ?oproof: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) ++ cut()
+ ++ str "Showing results without diff highlighting" );
+ pr_open_subgoals ~proof
+ end
+ else
+ pr_open_subgoals ~proof
+ in
+ Feedback.msg_notice output;;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 23:07:29 +0000