diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 61 | ||||
| -rw-r--r-- | printing/printer.mli | 40 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 20 | ||||
| -rw-r--r-- | printing/proof_diffs.mli | 6 |
4 files changed, 58 insertions, 69 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index a85e268306..bb54f587fd 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -76,25 +76,22 @@ let () = 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_econstr_n_core goal_concl_style env sigma n t = - pr_constr_expr_n env sigma n (extern_constr goal_concl_style env sigma t) -let pr_econstr_core goal_concl_style env sigma t = - pr_constr_expr env sigma (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_econstr_n_env ?lax ?inctx ?scope env sigma n t = + pr_constr_expr_n env sigma n (extern_constr ?lax ?inctx ?scope env sigma t) +let pr_econstr_env ?lax ?inctx ?scope env sigma t = + pr_constr_expr env sigma (extern_constr ?lax ?inctx ?scope env sigma t) +let pr_leconstr_env = Proof_diffs.pr_leconstr_env + +let pr_constr_n_env ?lax ?inctx ?scope env sigma n c = + pr_econstr_n_env ?lax ?inctx ?scope env sigma n (EConstr.of_constr c) +let pr_constr_env ?lax ?inctx ?scope env sigma c = + pr_econstr_env ?lax ?inctx ?scope 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 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_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 +let pr_open_lconstr_env ?lax ?inctx ?scope env sigma (_,c) = + pr_leconstr_env ?lax ?inctx ?scope env sigma c +let pr_open_constr_env ?lax ?inctx ?scope env sigma (_,c) = + pr_econstr_env ?lax ?inctx ?scope env sigma 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 *) @@ -106,16 +103,14 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) = 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_etype_core goal_concl_style env sigma t = - pr_constr_expr env sigma (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) +let pr_etype_env ?lax ?goal_concl_style env sigma t = + pr_constr_expr env sigma (extern_type ?lax ?goal_concl_style env sigma t) +let pr_letype_env = Proof_diffs.pr_letype_env -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_type_env ?lax ?goal_concl_style env sigma c = + pr_etype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c) +let pr_ltype_env ?lax ?goal_concl_style env sigma c = + pr_letype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c) let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) @@ -125,10 +120,10 @@ let pr_lglob_constr_env env c = let pr_glob_constr_env env c = pr_constr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c) -let pr_closed_glob_n_env env sigma n c = - pr_constr_expr_n env sigma n (extern_closed_glob false env sigma c) -let pr_closed_glob_env env sigma c = - pr_constr_expr env sigma (extern_closed_glob false env sigma c) +let pr_closed_glob_n_env ?lax ?goal_concl_style ?inctx ?scope env sigma n c = + pr_constr_expr_n env sigma n (extern_closed_glob ?lax ?goal_concl_style ?inctx ?scope env sigma c) +let pr_closed_glob_env ?lax ?goal_concl_style ?inctx ?scope env sigma c = + pr_constr_expr env sigma (extern_closed_glob ?lax ?goal_concl_style ?inctx ?scope env sigma c) let pr_lconstr_pattern_env env sigma c = pr_lconstr_pattern_expr env sigma (extern_constr_pattern (Termops.names_of_rel_context env) sigma c) @@ -141,7 +136,7 @@ let pr_cases_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let () = Termops.Internal.set_print_constr - (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true false env sigma t)) + (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true env sigma t)) let pr_in_comment x = str "(* " ++ x ++ str " *)" @@ -462,7 +457,7 @@ let pr_goal ?(diffs=false) ?og_s g_s = else pr_context_of env sigma ++ cut () ++ str "============================" ++ cut () ++ - pr_goal_concl_style_env env sigma concl + pr_letype_env ~goal_concl_style:true env sigma concl in str " " ++ v 0 goal @@ -489,7 +484,7 @@ let pr_concl n ?(diffs=false) ?og_s sigma g = if diffs then Proof_diffs.diff_concl ?og_s sigma g else - pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) + pr_letype_env ~goal_concl_style:true env sigma (Goal.V82.concl sigma g) in let header = pr_goal_header (int n) sigma g in header ++ str " is:" ++ cut () ++ str" " ++ pc diff --git a/printing/printer.mli b/printing/printer.mli index 87b09ff755..b2d0ea3536 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -15,6 +15,7 @@ open Pattern open Evd open Glob_term open Ltac_pretype +open Notation_term (** These are the entry points for printing terms, context, tac, ... *) @@ -25,45 +26,38 @@ val enable_goal_names_printing : bool ref (** Terms *) -val pr_lconstr_env : env -> evar_map -> constr -> Pp.t -val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t +val pr_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t +val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t -val pr_constr_env : env -> evar_map -> constr -> Pp.t -val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t - -val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t +val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" in case of remaining issues (such as reference not in env). *) -val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t - -val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t +val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t +val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t -val pr_econstr_env : env -> evar_map -> EConstr.t -> Pp.t -val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t +val pr_econstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t +val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t -val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t +val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t -val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t -val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t +val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t +val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t -val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t - -val pr_open_lconstr_env : env -> evar_map -> open_constr -> Pp.t +val pr_open_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t +val pr_open_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t -val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t -val pr_ltype_env : env -> evar_map -> types -> Pp.t - -val pr_type_env : env -> evar_map -> types -> Pp.t +val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t +val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t -val pr_closed_glob_n_env : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t -val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t +val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t +val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> closed_glob_constr -> Pp.t val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 233163d097..dec87f8071 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -245,18 +245,18 @@ let process_goal sigma g : EConstr.t reified_goal = let hyps = List.map to_tuple hyps in { name; ty; hyps; env; sigma };; -let pr_letype_core goal_concl_style env sigma t = - Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_type goal_concl_style env sigma t) +let pr_letype_env ?lax ?goal_concl_style env sigma t = + Ppconstr.pr_lconstr_expr env sigma + (Constrextern.extern_type ?lax ?goal_concl_style env sigma t) let pp_of_type env sigma ty = - pr_letype_core true env sigma ty + pr_letype_env ~goal_concl_style:true env sigma ty -let pr_leconstr_core goal_concl_style env sigma t = - Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr goal_concl_style env sigma t) +let pr_leconstr_env ?lax ?inctx ?scope env sigma t = + Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) -let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) - -let pr_lconstr_env_econstr env sigma c = pr_leconstr_core false env sigma c +let pr_lconstr_env ?lax ?inctx ?scope env sigma c = + pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c) let diff_concl ?og_s nsigma ng = let open Evd in @@ -301,7 +301,7 @@ let goal_info goal sigma = line_idents := idents :: !line_idents; let mid = match body with | Some c -> - let pb = pr_lconstr_env_econstr env sigma c in + let pb = pr_leconstr_env env sigma c in let pb = if EConstr.isCast sigma c then surround pb else pb in str " := " ++ pb | None -> mt() in @@ -556,7 +556,7 @@ let to_constr pf = (* pprf generally has only one element, but it may have more in the derive plugin *) let t = List.hd pprf in let sigma, env = get_proof_context pf in - let x = Constrextern.extern_constr false env sigma t in (* todo: right options?? *) + let x = Constrextern.extern_constr env sigma t in (* todo: right options?? *) x.v diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index a806ab7123..eebdaccd32 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -57,9 +57,9 @@ val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list -val pr_letype_core : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t -val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t -val pr_lconstr_env : env -> evar_map -> constr -> Pp.t +val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t +val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t +val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> env -> evar_map -> constr -> Pp.t (** Computes diffs for a single conclusion *) val diff_concl : ?og_s:Goal.goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t |