From 75b7729d204c7bae280d859bb233750f7c4b543e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 18 Feb 2018 19:08:04 +0100 Subject: Adding mention of shelved/given-up status in "Show Existentials". Also changed the API of pr_subgoals now using labels. Also removed a trailing space in printing existentials. --- printing/printer.ml | 44 +++++++++++++++++++++++++++----------------- printing/printer.mli | 8 ++++---- 2 files changed, 31 insertions(+), 21 deletions(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index d720bc2f8..c38a73d7d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -537,7 +537,7 @@ let pr_evgl_sign sigma evi = let ids = List.rev_map NamedDecl.get_id l in let warn = if List.is_empty ids then mt () else - (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") + (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 candidates = @@ -549,7 +549,7 @@ let pr_evgl_sign sigma evi = mt () in hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ - candidates ++ spc () ++ warn) + candidates ++ warn) (* Print an existential variable *) @@ -558,15 +558,25 @@ let pr_evar sigma (evk, evi) = hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl) (* Print an enumerated list of existential variables *) -let rec pr_evars_int_hd head sigma i = function +let rec pr_evars_int_hd pr sigma i = function | [] -> mt () | (evk,evi)::rest -> - (hov 0 (head i ++ pr_evar sigma (evk,evi))) ++ - (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd head sigma (i+1) rest) - -let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ int i ++ str " =" ++ spc ()) sigma i (Evar.Map.bindings evs) - -let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs) + (hov 0 (pr i evk evi)) ++ + (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest) + +let pr_evars_int sigma ~shelf ~givenup i evs = + let pr_status i = + if List.mem i shelf then str " (shelved)" + else if List.mem i givenup then str " (given up)" + else mt () in + pr_evars_int_hd + (fun i evk evi -> + str "Existential " ++ int i ++ str " =" ++ + spc () ++ pr_evar sigma (evk,evi) ++ pr_status evk) + sigma i (Evar.Map.bindings evs) + +let pr_evars sigma evs = + pr_evars_int_hd (fun i evk evi -> pr_evar sigma (evk,evi)) sigma 1 (Evar.Map.bindings evs) (* Display a list of evars given by their name, with a prefix *) let pr_ne_evar_set hd tl sigma l = @@ -684,7 +694,7 @@ let print_dependent_evars gl sigma seeds = (* 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) - close_cmd sigma seeds shelf stack unfocused goals = + close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals = (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a @@ -746,7 +756,7 @@ let default_pr_subgoals ?(pr_first=true) if Evar.Map.is_empty exl then (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else - let pei = pr_evars_int sigma 1 exl in + let pei = pr_evars_int sigma ~shelf ~givenup:[] 1 exl in v 0 ((str "No more subgoals," ++ str " but there are non-instantiated existential variables:" ++ cut () ++ (hov 0 pei) @@ -773,7 +783,7 @@ let default_pr_subgoals ?(pr_first=true) type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + 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; } @@ -807,16 +817,16 @@ let pr_open_subgoals ~proof = begin match goals with | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in begin match bgoals,shelf,given_up with - | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals + | [] , [] , [] -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals | [] , [] , _ -> Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up + ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> Feedback.msg_info (str "All the remaining goals are on the shelf."); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf + ++ 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." ++ @@ -824,13 +834,13 @@ let pr_open_subgoals ~proof = if Pp.ismt s then s else fnl () ++ s) ++ fnl () in - pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals + pr_subgoals ~pr_first:false (Some end_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 [] unfocused_if_needed bgoals_focused + pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused end let pr_nth_open_subgoal ~proof n = diff --git a/printing/printer.mli b/printing/printer.mli index a3427920a..9b26d4c84 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -181,8 +181,7 @@ val pr_goal : goal sigma -> Pp.t focused goals unless the conrresponding option [enable_unfocused_goal_printing] is set. [seeds] is for printing dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list - -> goal list -> goal list -> Pp.t +val 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 val pr_subgoal : int -> evar_map -> goal list -> Pp.t val pr_concl : int -> evar_map -> goal -> Pp.t @@ -190,7 +189,7 @@ val pr_concl : int -> evar_map -> goal -> Pp.t val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t -val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars_int : evar_map -> shelf:goal list -> givenup:goal list -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t @@ -223,7 +222,8 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + 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; } -- cgit v1.2.3