diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 553 |
1 files changed, 330 insertions, 223 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 04337f6b..199aa79c 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -1,34 +1,71 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp open CErrors open Util open Names -open Term +open Constr open Environ open Globnames open Nametab open Evd open Proof_type open Refiner -open Pfedit open Constrextern open Ppconstr open Declarations -let emacs_str s = - if !Flags.print_emacs then s else "" -let delayed_emacs_cmd s = - if !Flags.print_emacs then s () else str "" +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration +module CompactedDecl = Context.Compacted.Declaration + +let enable_unfocused_goal_printing = ref false +let enable_goal_tags_printing = ref false +let enable_goal_names_printing = ref false + +let should_tag() = !enable_goal_tags_printing +let should_unfoc() = !enable_unfocused_goal_printing +let should_gname() = !enable_goal_names_printing + + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "printing of unfocused goal"; + optkey = ["Printing";"Unfocused"]; + optread = (fun () -> !enable_unfocused_goal_printing); + optwrite = (fun b -> enable_unfocused_goal_printing:=b) } + +(* This is set on by proofgeneral proof-tree mode. But may be used for + other purposes *) +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "printing of goal tags"; + optkey = ["Printing";"Goal";"Tags"]; + optread = (fun () -> !enable_goal_tags_printing); + optwrite = (fun b -> enable_goal_tags_printing:=b) } + + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "printing of goal names"; + optkey = ["Printing";"Goal";"Names"]; + optread = (fun () -> !enable_goal_names_printing); + optwrite = (fun b -> enable_goal_names_printing:=b) } -let get_current_context () = - Pfedit.get_current_context () (**********************************************************************) (** Terms *) @@ -41,32 +78,42 @@ let get_current_context () = and only names of goal/section variables and rel names that do _not_ occur in the scope of the binder to be printed are avoided. *) -let pr_constr_core goal_concl_style env sigma t = +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_lconstr_core 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_lconstr_env env = pr_lconstr_core false env -let pr_constr_env env = pr_constr_core false env +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_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 = pr_lconstr_core true env -let pr_constr_goal_style_env env = pr_constr_core true 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 - (* NB do not remove the eta-redexes! Global.env() has side-effects... *) +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 + +(* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lconstr_env env sigma t let pr_constr t = - let (sigma, env) = get_current_context () in + 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_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 *) @@ -74,37 +121,40 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) = let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in pr (Termops.push_rels_assum assums env) sigma c -let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env -let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env +let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env +let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env let pr_constr_under_binders c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_constr_under_binders_env env sigma c let pr_lconstr_under_binders c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lconstr_under_binders_env env sigma c -let pr_type_core goal_concl_style env sigma t = +let pr_etype_core goal_concl_style env sigma t = pr_constr_expr (extern_type goal_concl_style env sigma t) -let pr_ltype_core 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_goal_concl_style_env env = pr_ltype_core true env -let pr_ltype_env env = pr_ltype_core false env -let pr_type_env env = pr_type_core false env +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) let pr_ltype t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_ltype_env env sigma t let pr_type t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_type_env env sigma t +let pr_etype_env env sigma c = pr_etype_core false env sigma c +let pr_letype_env env sigma c = pr_letype_core false env sigma c +let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c + let pr_ljudge_env env sigma j = - (pr_lconstr_env env sigma j.uj_val, pr_lconstr_env env sigma j.uj_type) + (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) let pr_ljudge j = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_ljudge_env env sigma j let pr_lglob_constr_env env c = @@ -113,16 +163,18 @@ let pr_glob_constr_env env c = pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c) let pr_lglob_constr c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lglob_constr_env env c let pr_glob_constr c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_glob_constr_env env c +let pr_closed_glob_n_env env sigma n c = + pr_constr_expr_n n (extern_closed_glob false env sigma c) let pr_closed_glob_env env sigma c = pr_constr_expr (extern_closed_glob false env sigma c) let pr_closed_glob c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_closed_glob_env env sigma c let pr_lconstr_pattern_env env sigma c = @@ -134,16 +186,16 @@ let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t) let pr_lconstr_pattern t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lconstr_pattern_env env sigma t let pr_constr_pattern t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_constr_pattern_env env sigma t let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.set_print_constr - (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t)) + (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 " *)" @@ -182,10 +234,10 @@ let qualid_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 loc vars r + let extern_ref ?loc vars r = + try orig_extern_ref vars r with e when CErrors.noncritical e -> - Libnames.Qualid (loc, qualid_of_global env r) + CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r) in Constrextern.set_extern_reference extern_ref; try @@ -199,17 +251,36 @@ let safe_gen f env sigma c = let safe_pr_lconstr_env = safe_gen pr_lconstr_env let safe_pr_constr_env = safe_gen pr_constr_env let safe_pr_lconstr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in safe_pr_lconstr_env env sigma t let safe_pr_constr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in safe_pr_constr_env env sigma t -let pr_universe_ctx sigma c = +let pr_universe_ctx_set sigma c = + if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c + else + mt() + +let pr_universe_ctx sigma ?variance c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c + (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c + else + mt() + +let pr_constant_universes sigma = function + | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx + | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx + +let pr_cumulativity_info sigma cumi = + if !Detyping.print_universes + && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi else mt() @@ -226,7 +297,7 @@ let pr_puniverses f env (c,u) = else mt ()) let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) -let pr_existential_key = Evd.pr_existential_key +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) @@ -248,31 +319,37 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (**********************************************************************) (* Contexts and declarations *) -let pr_var_decl_skel pr_id env sigma (id,c,typ) = - let pbody = match c with - | None -> (mt ()) - | Some c -> - (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in - let pb = if isCast c then surround pb else pb in - (str" := " ++ pb ++ cut () ) in + +(* Flag for compact display of goals *) + +let get_compact_context,set_compact_context = + let compact_context = ref false in + (fun () -> !compact_context),(fun b -> compact_context := b) + +let pr_compacted_decl env sigma decl = + let ids, pbody, typ = match decl with + | CompactedDecl.LocalAssum (ids, typ) -> + ids, mt (), typ + | CompactedDecl.LocalDef (ids,c,typ) -> + (* Force evaluation *) + let pb = pr_lconstr_env env sigma c in + let pb = if isCast c then surround pb else pb in + ids, (str" := " ++ pb ++ cut ()), typ + in + let pids = prlist_with_sep pr_comma pr_id ids in let pt = pr_ltype_env env sigma typ in let ptyp = (str" : " ++ pt) in - (pr_id id ++ hov 0 (pbody ++ ptyp)) + hov 0 (pids ++ pbody ++ ptyp) -let pr_var_decl env sigma d = - pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d) - -let pr_var_list_decl env sigma (l,c,typ) = - hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) +let pr_named_decl env sigma decl = + decl |> CompactedDecl.of_named_decl |> pr_compacted_decl env sigma let pr_rel_decl env sigma decl = - let open Context.Rel.Declaration in - let na = get_name decl in - let typ = get_type decl in + let na = RelDecl.get_name decl in + let typ = RelDecl.get_type decl in let pbody = match decl with - | LocalAssum _ -> mt () - | LocalDef (_,c,_) -> + | RelDecl.LocalAssum _ -> mt () + | RelDecl.LocalDef (_,c,_) -> (* Force evaluation *) let pb = pr_lconstr_env env sigma c in let pb = if isCast c then surround pb else pb in @@ -289,16 +366,20 @@ let pr_rel_decl env sigma decl = (* Prints a signature, all declarations on the same line if possible *) let pr_named_context_of env sigma = - let make_decl_list env d pps = pr_var_decl env sigma d :: pps in + let make_decl_list env d pps = pr_named_decl env sigma d :: pps in let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) +let pr_var_list_decl env sigma decl = + hov 0 (pr_compacted_decl env sigma decl) + let pr_named_context env sigma ne_context = hv 0 (Context.Named.fold_outside - (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) + (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d) ne_context ~init:(mt ())) let pr_rel_context env sigma rel_context = + let rel_context = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) rel_context in pr_binders (extern_rel_context None env sigma rel_context) let pr_rel_context_of env sigma = @@ -307,9 +388,9 @@ let pr_rel_context_of env sigma = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env sigma = let sign_env = - Context.NamedList.fold + Context.Compacted.fold (fun d pps -> - let pidt = pr_var_list_decl env sigma d in + let pidt = pr_compacted_decl env sigma d in (pps ++ fnl () ++ pidt)) (Termops.compact_named_context (named_context env)) ~init:(mt ()) in @@ -326,39 +407,74 @@ let pr_ne_context_of header env sigma = List.is_empty (Environ.named_context env) then (mt ()) else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ()) -let pr_context_limit n env sigma = - let named_context = Environ.named_context env in - let lgsign = List.length named_context in - if n >= lgsign then - pr_context_unlimited env sigma - else - let k = lgsign-n in - let _,sign_env = - Context.NamedList.fold - (fun d (i,pps) -> - if i < k then - (i+1, (pps ++str ".")) - else - let pidt = pr_var_list_decl env sigma d in - (i+1, (pps ++ fnl () ++ - str (emacs_str "") ++ - pidt))) - (Termops.compact_named_context (Environ.named_context env)) ~init:(0,(mt ())) - in - let db_env = - fold_rel_context - (fun env d pps -> - let pnat = pr_rel_decl env sigma d in - (pps ++ fnl () ++ - str (emacs_str "") ++ - pnat)) - env ~init:(mt ()) - in - (sign_env ++ db_env) +(* Heuristic for horizontalizing hypothesis that the user probably + considers as "variables": An hypothesis H:T where T:S and S<>Prop. *) +let should_compact env sigma typ = + get_compact_context() && + let type_of_typ = Retyping.get_type_of env sigma (EConstr.of_constr typ) in + not (is_Prop (EConstr.to_constr sigma type_of_typ)) + + +(* If option Compact Contexts is set, we pack "simple" hypothesis in a + hov box (with three sapaces as a separator), the global box being a + v box *) +let rec bld_sign_env env sigma ctxt pps = + match ctxt with + | [] -> pps + | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ -> + let pps',ctxt' = bld_sign_env_id env sigma ctxt (mt ()) true in + (* putting simple hyps in a more horizontal flavor *) + bld_sign_env env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps') + | d:: ctxt' -> + let pidt = pr_var_list_decl env sigma d in + let pps' = pps ++ brk (0,0) ++ pidt in + bld_sign_env env sigma ctxt' pps' +and bld_sign_env_id env sigma ctxt pps is_start = + match ctxt with + | [] -> pps,ctxt + | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ -> + let pidt = pr_var_list_decl env sigma d in + let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in + bld_sign_env_id env sigma ctxt' pps' false + | _ -> pps,ctxt + + +(* compact printing an env (variables and de Bruijn). Separator: three + spaces between simple hyps, and newline otherwise *) +let pr_context_limit_compact ?n env sigma = + let ctxt = Termops.compact_named_context (named_context env) in + let lgth = List.length ctxt in + let n_capped = + match n with + | None -> lgth + | Some n when n > lgth -> lgth + | Some n -> n in + let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in + (* a dot line hinting the number of hidden hyps. *) + let hidden_dots = String.make (List.length ctxt_hidden) '.' in + let sign_env = v 0 (str hidden_dots ++ (mt ()) + ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in + let db_env = + fold_rel_context (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d) + env ~init:(mt ()) in + sign_env ++ db_env + +(* The number of printed hypothesis in a goal *) +(* If [None], no limit *) +let print_hyps_limit = ref (None : int option) + +let _ = + let open Goptions in + declare_int_option + { optdepr = false; + optname = "the hypotheses limit"; + optkey = ["Hyps";"Limit"]; + optread = (fun () -> !print_hyps_limit); + optwrite = (fun x -> print_hyps_limit := x) } -let pr_context_of env sigma = match Flags.print_hyps_limit () with - | None -> hv 0 (pr_context_unlimited env sigma) - | Some n -> hv 0 (pr_context_limit n env sigma) +let pr_context_of env sigma = match !print_hyps_limit with + | None -> hv 0 (pr_context_limit_compact env sigma) + | Some n -> hv 0 (pr_context_limit_compact ~n env sigma) (* display goal parts (Proof mode) *) @@ -371,7 +487,7 @@ let pr_predicate pr_elt (b, elts) = if List.is_empty elts then str"none" else pr_elts let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) -let pr_idpred p = pr_predicate Nameops.pr_id (Id.Pred.elements p) +let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p) let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ @@ -379,7 +495,8 @@ let pr_transparent_state (ids, csts) = (* display complete goal *) let default_pr_goal gs = - let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in + 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 = @@ -391,23 +508,25 @@ let default_pr_goal gs = (* display a goal tag *) let pr_goal_tag g = let s = " (ID " ^ Goal.uid g ^ ")" in - str (emacs_str s) - -let display_name = false + str s (* display a goal name *) let pr_goal_name sigma g = - if display_name then str " " ++ Pp.surround (pr_existential_key sigma g) + if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt () +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 ()) + (* display the conclusion of a goal *) let pr_concl n 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 - str (emacs_str "") ++ - str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++ - str " is:" ++ cut () ++ str" " ++ pc + let header = pr_goal_header (int n) sigma g in + header ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) let pr_evgl_sign sigma evi = @@ -417,11 +536,10 @@ let pr_evgl_sign sigma evi = | None -> [], [] | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) in - let open Context.Named.Declaration in - let ids = List.rev_map get_id l in + 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 = @@ -433,7 +551,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 *) @@ -442,15 +560,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 = @@ -464,12 +592,12 @@ let pr_ne_evar_set hd tl sigma l = let pr_selected_subgoal name sigma g = let pg = default_pr_goal { sigma=sigma ; it=g; } in - v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g - ++ str " is:" ++ cut () ++ pg) + let header = pr_goal_header name sigma g in + v 0 (header ++ str " is:" ++ cut () ++ pg) let default_pr_subgoal n sigma = let rec prrec p = function - | [] -> error "No such goal." + | [] -> user_err Pp.(str "No such goal.") | g::rest -> if Int.equal p 1 then pr_selected_subgoal (int n) sigma g @@ -478,7 +606,7 @@ let default_pr_subgoal n sigma = in prrec n -let pr_internal_existential_key ev = str (string_of_existential ev) +let pr_internal_existential_key ev = Evar.print ev let print_evar_constraints gl sigma = let pr_env = @@ -487,15 +615,15 @@ let print_evar_constraints gl sigma = | Some g -> let env = Goal.V82.env sigma g in fun e' -> begin - if Context.Named.equal (named_context env) (named_context e') then - if Context.Rel.equal (rel_context env) (rel_context e') then mt () + if Context.Named.equal Constr.equal (named_context env) (named_context e') then + if Context.Rel.equal Constr.equal (rel_context env) (rel_context e') then mt () else pr_rel_context_of e' sigma ++ str " |-" ++ spc () else pr_context_of e' sigma ++ str " |-" ++ spc () end in let pr_evconstr (pbty,env,t1,t2) = - let t1 = Evarutil.nf_evar sigma t1 - and t2 = Evarutil.nf_evar sigma t2 in + let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1) + and t2 = Evarutil.nf_evar sigma (EConstr.of_constr 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 @@ -503,13 +631,13 @@ let print_evar_constraints gl sigma = problem. MS: we should rather stop depending on anonymous variables, they can be used to indicate independency. Also, this depends on a strategy for naming/renaming *) - Namegen.make_all_name_different env in + Namegen.make_all_name_different env sigma in str" " ++ - hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++ + hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ pr_lconstr_env env sigma t2) + spc () ++ pr_leconstr_env env sigma t2) in let pr_candidate ev evi (candidates,acc) = if Option.has_some evi.evar_candidates then @@ -534,8 +662,7 @@ let should_print_dependent_evars = ref false let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "Printing Dependent Evars Line"; optkey = ["Printing";"Dependent";"Evars";"Line"]; optread = (fun () -> !should_print_dependent_evars); @@ -558,27 +685,24 @@ let print_dependent_evars gl sigma seeds = end i (str ",") end evars (str "") in - fnl () ++ - str "(dependent evars:" ++ evars ++ str ")" ++ fnl () - else - fnl () ++ - str "(dependent evars: (printing disabled) )" ++ fnl () + cut () ++ cut () ++ + str "(dependent evars:" ++ evars ++ str ")" + else mt () in - constraints ++ delayed_emacs_cmd evars + constraints ++ evars () (* 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. *) -(* courtieu: in emacs mode, even less cases where the first goal is printed - in its entirety *) -let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals = +let default_pr_subgoals ?(pr_first=true) + close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals = (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a | b::l -> Pp.int a ++ str"-" ++ print_stack b l in - let print_unfocused l = + let print_unfocused_nums l = match l with | [] -> None | a::l -> Some (str"unfocused: " ++ print_stack a l) @@ -598,7 +722,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals | [] -> Pp.mt () | a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")" in - let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in + let extra = Option.List.flatten [ print_unfocused_nums stack ; print_shelf shelf ] in let print_extra = print_extra_list extra in let focused_if_needed = let needed = not (CList.is_empty extra) && pr_first in @@ -615,8 +739,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals in let print_multiple_goals g l = if pr_first then - default_pr_goal { it = g ; sigma = sigma; } ++ fnl () ++ - pr_rec 2 l + default_pr_goal { it = g ; sigma = sigma; } + ++ (if l=[] then mt () else cut ()) + ++ pr_rec 2 l else pr_rec 1 (g::l) in @@ -629,34 +754,29 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals match goals with | [] -> begin - let exl = Evarutil.non_instantiated sigma in + let exl = Evd.undefined_map sigma in if Evar.Map.is_empty exl then - (str"No more subgoals." - ++ print_dependent_evars None sigma seeds) + (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else - let pei = pr_evars_int sigma 1 exl in - (str "No more subgoals, but there are non-instantiated existential variables:" - ++ fnl () ++ (hov 0 pei) - ++ print_dependent_evars None sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + 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) + ++ print_dependent_evars None sigma seeds + ++ cut () ++ str "You can use Grab Existential Variables.")) end - | [g] when not !Flags.print_emacs && pr_first -> - let pg = default_pr_goal { it = g ; sigma = sigma; } in - v 0 ( - str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra - ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg - ++ print_dependent_evars (Some g) sigma seeds - ) | g1::rest -> let goals = print_multiple_goals g1 rest in let ngoals = List.length rest+1 in v 0 ( - int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ - print_extra ++ - str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1") - ++ pr_goal_tag g1 - ++ pr_goal_name sigma g1 ++ cut () - ++ goals + int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") + ++ print_extra + ++ str (if (should_gname()) then ", subgoal 1" else "") + ++ (if should_tag() then pr_goal_tag g1 else str"") + ++ pr_goal_name sigma g1 ++ cut () ++ goals + ++ (if unfocused=[] then str "" + else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut() + ++ pr_rec (List.length rest + 2) unfocused)) ++ print_dependent_evars (Some g1) sigma seeds ) @@ -665,9 +785,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals type printer_pr = { - pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; - pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; - pr_goal : goal sigma -> std_ppcmds; + 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 = { @@ -687,7 +807,7 @@ let pr_goal x = !printer_pr.pr_goal x (* End abstraction layer *) (**********************************************************************) -let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = +let pr_open_subgoals ~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 @@ -699,66 +819,49 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_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." ++ - (let s = Proof_global.Bullet.suggest p in - if Pp.is_empty s then s else fnl () ++ s) ++ + (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 [] bgoals + pr_subgoals ~pr_first:false (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals end - | _ -> pr_subgoals None sigma seeds shelf stack goals + | _ -> + 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 end -let pr_nth_open_subgoal n = - let pf = get_pftreestate () in - let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in +let pr_nth_open_subgoal ~proof n = + let gls,_,_,_,sigma = Proof.proof proof in pr_subgoal n sigma gls -let pr_goal_by_id id = - let p = Proof_global.give_me_the_proof () in +let pr_goal_by_id ~proof id = try - Proof.in_proof p (fun sigma -> + Proof.in_proof proof (fun sigma -> let g = Evd.evar_key id sigma in pr_selected_subgoal (pr_id id) sigma g) - with Not_found -> error "No such goal." - -let pr_goal_by_uid uid = - let p = Proof_global.give_me_the_proof () in - let g = Goal.get_by_uid uid in - let pr gs = - v 0 (str "goal / evar " ++ str uid ++ str " is:" ++ cut () - ++ pr_goal gs) - in - try - Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;}) - with Not_found -> error "Invalid goal identifier." + with Not_found -> user_err Pp.(str "No such goal.") (* Elementary tactics *) let pr_prim_rule = function - | Cut (b,replace,id,t) -> - if b then - (* TODO: express "replace" *) - (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")") - else - let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in - (str"cut " ++ pr_constr t ++ - str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | Refine c -> - str(if Termops.occur_meta c then "refine " else "exact ") ++ + (** FIXME *) + str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c (* Backwards compatibility *) @@ -770,15 +873,15 @@ let prterm = pr_lconstr It is used primarily by the Print Assumptions command. *) type axiom = - | Constant of constant (* An axiom or a constant. *) + | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *) + | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) | Axiom of axiom * (Label.t * Context.Rel.t * types) list - | Opaque of constant (* An opaque constant. *) - | Transparent of constant + | Opaque of Constant.t (* An opaque constant. *) + | Transparent of Constant.t (* Defines a set of [assumption] *) module OrderedContextObject = @@ -788,11 +891,11 @@ struct let compare_axiom x y = match x,y with | Constant k1 , Constant k2 -> - con_ord k1 k2 + Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> - con_ord k1 k2 + Constant.CanOrd.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 | _ -> -1 @@ -805,16 +908,16 @@ struct | Axiom (k1,_) , Axiom (k2, _) -> compare_axiom k1 k2 | Axiom _ , _ -> -1 | _ , Axiom _ -> 1 - | Opaque k1 , Opaque k2 -> con_ord k1 k2 + | Opaque k1 , Opaque k2 -> Constant.CanOrd.compare k1 k2 | Opaque _ , _ -> -1 | _ , Opaque _ -> 1 - | Transparent k1 , Transparent k2 -> con_ord k1 k2 + | Transparent k1 , Transparent k2 -> Constant.CanOrd.compare k1 k2 end module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) -let pr_assumptionset env s = +let pr_assumptionset env sigma s = if ContextObjectMap.is_empty s && engagement env = PredicativeSet then str "Closed under the global context" @@ -822,15 +925,14 @@ let pr_assumptionset env s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> - let mp,_,lab = repr_con kn in - str (string_of_mp mp) ++ str "." ++ pr_label lab + 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 with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = - let sigma, env = get_current_context () in let env = Environ.push_rel_context rctx env in try str " " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () @@ -857,7 +959,7 @@ let pr_assumptionset env s = let ax = pr_axiom env axiom typ ++ cut() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> - str " used in " ++ pr_label lbl ++ + str " used in " ++ Label.print lbl ++ str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) l in (v, ax :: a, o, tr) @@ -901,6 +1003,11 @@ let pr_assumptionset env s = let xor a b = (a && not b) || (not a && b) +let pr_cumulative poly cum = + if poly then + if cum then str "Cumulative " else str "NonCumulative " + else mt () + let pr_polymorphic b = let print = xor (Flags.is_universe_polymorphism ()) b in if print then @@ -909,4 +1016,4 @@ let pr_polymorphic b = let pr_universe_instance evd ctx = let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}" + str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" |