diff options
| -rw-r--r-- | printing/ppconstr.ml | 21 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 1 | ||||
| -rw-r--r-- | printing/printer.ml | 6 | ||||
| -rw-r--r-- | printing/printer.mli | 5 |
4 files changed, 26 insertions, 7 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 4d7a71631..109a40a03 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -742,29 +742,36 @@ let tag_var = tag Tag.variable let rec fix rf x = rf (fix rf) x let pr = fix modular_constr_pr mt + let pr prec = function + (* A toplevel printer hack mimicking parsing, incidentally meaning + that we cannot use [pr] correctly anymore in a recursive loop + if the current expr is followed by other exprs which would be + interpreted as arguments *) + | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us + | c -> pr prec c + let transf env c = if !Flags.beautify_file then let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in Constrextern.extern_glob_constr (Termops.vars_of_env env) r else c - let pr prec c = pr prec (transf (Global.env()) c) + let pr_expr prec c = pr prec (transf (Global.env()) c) - let pr_simpleconstr = function - | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us - | c -> pr lsimpleconstr c + let pr_simpleconstr = pr_expr lsimpleconstr let default_term_pr = { pr_constr_expr = pr_simpleconstr; - pr_lconstr_expr = pr ltop; + pr_lconstr_expr = pr_expr ltop; pr_constr_pattern_expr = pr_simpleconstr; - pr_lconstr_pattern_expr = pr ltop + pr_lconstr_pattern_expr = pr_expr ltop } let term_pr = ref default_term_pr let set_term_pr = (:=) term_pr + let pr_constr_expr_n n c = pr_expr n c let pr_constr_expr c = !term_pr.pr_constr_expr c let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c @@ -774,5 +781,5 @@ let tag_var = tag Tag.variable let pr_record_body = pr_record_body_gen pr - let pr_binders = pr_undelimited_binders spc (pr ltop) + let pr_binders = pr_undelimited_binders spc (pr_expr ltop) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 34cccfc2d..be96cfce5 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -60,6 +60,7 @@ val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t val pr_constr_expr : constr_expr -> Pp.t val pr_lconstr_expr : constr_expr -> Pp.t val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t +val pr_constr_expr_n : tolerability -> constr_expr -> Pp.t type term_pr = { pr_constr_expr : constr_expr -> Pp.t; diff --git a/printing/printer.ml b/printing/printer.ml index 28b10c781..c6650ea3b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -79,11 +79,14 @@ 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 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_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 @@ -94,6 +97,7 @@ let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (ECons 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 @@ -166,6 +170,8 @@ let pr_glob_constr c = let (sigma, env) = 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 = diff --git a/printing/printer.mli b/printing/printer.mli index ba849bee6..658ea6060 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -33,6 +33,8 @@ val pr_constr_env : env -> evar_map -> constr -> Pp.t val pr_constr : constr -> Pp.t val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t +val pr_constr_n_env : env -> evar_map -> Notation_term.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). *) @@ -48,6 +50,8 @@ val pr_econstr : EConstr.t -> Pp.t val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr : EConstr.t -> Pp.t +val pr_econstr_n_env : env -> evar_map -> Notation_term.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 @@ -70,6 +74,7 @@ val pr_ltype : types -> Pp.t val pr_type_env : env -> evar_map -> types -> Pp.t val pr_type : types -> Pp.t +val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t val pr_closed_glob : closed_glob_constr -> Pp.t |