From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- printing/printer.ml | 217 +++++++++++++++++++++++++++++++--------------------- 1 file changed, 129 insertions(+), 88 deletions(-) (limited to 'printing/printer.ml') 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;; -- cgit v1.2.3