diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 32 | ||||
| -rw-r--r-- | printing/printer.mli | 12 | ||||
| -rw-r--r-- | printing/printmod.ml | 6 |
3 files changed, 47 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 2ad9e268c2..b0a4c8b738 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -173,6 +173,38 @@ 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 u_ident = Id.of_string "u" + +let universe_binders_with_opt_names orig names = + let orig = Univ.AUContext.names orig in + let orig = Array.to_list orig in + let udecl = match names with + | None -> orig + | Some udecl -> + try + List.map2 (fun orig {CAst.v = na} -> + match na with + | Anonymous -> orig + | Name id -> Name id) orig udecl + with Invalid_argument _ -> + let len = List.length orig in + CErrors.user_err ~hdr:"universe_binders_with_opt_names" + Pp.(str "Universe instance should have length " ++ int len) + in + let fold_named i ubind = function + | Name id -> Id.Map.add id (Univ.Level.var i) ubind + | Anonymous -> ubind + in + let ubind = List.fold_left_i fold_named 0 UnivNames.empty_binders udecl in + let fold_anons i (u_ident, ubind) = function + | Name _ -> u_ident, ubind + | Anonymous -> + let id = Namegen.next_ident_away_from u_ident (fun id -> Id.Map.mem id ubind) in + (id, Id.Map.add id (Univ.Level.var i) ubind) + in + let (_, ubind) = List.fold_left_i fold_anons 0 (u_ident, ubind) udecl in + ubind + let pr_universe_ctx_set sigma c = if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) diff --git a/printing/printer.mli b/printing/printer.mli index 8c633b5e79..8805819890 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -132,6 +132,18 @@ val pr_universes : evar_map -> ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t -> Declarations.universes -> Pp.t +(** [universe_binders_with_opt_names ref l] + + If [l] is [Some univs] return the universe binders naming the + bound levels of [ref] by [univs] (generating names for Anonymous). + May error if the lengths mismatch. + + Otherwise return the bound universe names registered for [ref]. + + Inefficient on large contexts due to name generation. *) +val universe_binders_with_opt_names : Univ.AUContext.t -> + UnivNames.univ_name_list option -> UnivNames.universe_binders + (** Printing global references using names as short as possible *) val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t diff --git a/printing/printmod.ml b/printing/printmod.ml index eec2fe86ac..9beac17546 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -118,7 +118,7 @@ let print_mutual_inductive env mind mib udecl = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in - let bl = UnivNames.universe_binders_with_opt_names + let bl = Printer.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in @@ -151,7 +151,7 @@ let print_record env mind mib udecl = let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in - let bl = UnivNames.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib) + let bl = Printer.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in @@ -290,7 +290,7 @@ let print_body is_impl extent env mp (l,body) = (match extent with | OnlyNames -> mt () | WithContents -> - let bl = UnivNames.universe_binders_with_opt_names ctx None in + let bl = Printer.universe_binders_with_opt_names ctx None in let sigma = Evd.from_ctx (UState.of_binders bl) in str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ |