diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 30 | ||||
| -rw-r--r-- | printing/printer.ml | 22 | ||||
| -rw-r--r-- | printing/printer.mli | 8 | ||||
| -rw-r--r-- | printing/printmod.ml | 12 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 2 |
5 files changed, 27 insertions, 47 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index c417ef8a66..797b6faa08 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -86,10 +86,7 @@ let print_ref reduce ref udecl = | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> let mind = Environ.lookup_mind ind env in - begin match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None - | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) - end + mind.Declarations.mind_variance in let inst = if Global.is_polymorphic ref @@ -98,7 +95,7 @@ let print_ref reduce ref udecl = in let priv = None in (* We deliberately don't print private univs in About. *) hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv) + Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) (** Printing implicit arguments *) @@ -193,7 +190,7 @@ let opacity env = | ConstRef cst -> let cb = Environ.lookup_constant cst env in (match cb.const_body with - | Undef _ -> None + | Undef _ | Primitive _ -> None | OpaqueDef _ -> Some FullyOpaque | Def _ -> Some (TransparentMaybeOpacified @@ -267,7 +264,6 @@ let print_name_infos ref = print_ref true ref None; blankline] else [] in - print_polymorphism ref @ print_type_in_type ref @ print_primitive ref @ type_info_for_implicit @ @@ -559,15 +555,15 @@ let print_constant with_values sep sp udecl = let open Univ in let otab = Global.opaque_tables () in match cb.const_body with - | Undef _ | Def _ -> cb.const_universes + | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with - | Monomorphic_const ctx -> - Monomorphic_const (ContextSet.union body_uctxs ctx) - | Polymorphic_const ctx -> + | Monomorphic ctx -> + Monomorphic (ContextSet.union body_uctxs ctx) + | Polymorphic ctx -> assert(ContextSet.is_empty body_uctxs); - Polymorphic_const ctx + Polymorphic ctx in let ctx = UState.of_binders @@ -581,11 +577,11 @@ let print_constant with_values sep sp udecl = str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs + Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs | Some (c, ctx) -> print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ - Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs) + Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs) let gallina_print_constant_with_infos sp udecl = print_constant true " = " sp udecl ++ @@ -725,7 +721,10 @@ let print_full_pure_context env sigma = | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ - pr_lconstr_env env sigma (Mod_subst.force_constr c)) + pr_lconstr_env env sigma (Mod_subst.force_constr c) + | Primitive _ -> + str "Primitive " ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in @@ -838,6 +837,7 @@ let print_about_any ?loc env sigma k udecl = Dumpglob.add_glob ?loc ref; pr_infos_list (print_ref false ref udecl :: blankline :: + print_polymorphism ref @ print_name_infos ref @ (if Pp.ismt rb then [] else [rb]) @ print_opacity ref @ diff --git a/printing/printer.ml b/printing/printer.ml index 3f7837fd6e..bc936975c2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -209,7 +209,7 @@ let pr_universe_ctx sigma ?variance c = else mt() -let pr_abstract_universe_ctx sigma ?variance c ~priv = +let pr_abstract_universe_ctx sigma ?variance ?priv c = let open Univ in let priv = Option.default Univ.ContextSet.empty priv in let has_priv = not (ContextSet.is_empty priv) in @@ -221,23 +221,9 @@ let pr_abstract_universe_ctx sigma ?variance c ~priv = else mt() -let pr_constant_universes sigma ~priv = function - | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx - | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv - -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 (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi)) - else - mt() - -let pr_abstract_cumulativity_info sigma cumi = - if !Detyping.print_universes - && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then - fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi)) - else - mt() +let pr_universes sigma ?variance ?priv = function + | Declarations.Monomorphic ctx -> pr_universe_ctx_set sigma ctx + | Declarations.Polymorphic ctx -> pr_abstract_universe_ctx sigma ?variance ?priv ctx (**********************************************************************) (* Global references *) diff --git a/printing/printer.mli b/printing/printer.mli index 9a06d555e4..4e27268c4d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -86,11 +86,11 @@ val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Const val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> - Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t + ?priv:Univ.ContextSet.t -> Univ.AUContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t -val pr_constant_universes : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t -val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t -val pr_abstract_cumulativity_info : evar_map -> Univ.ACumulativityInfo.t -> Pp.t +val pr_universes : evar_map -> + ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t -> + Declarations.universes -> Pp.t (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 898f231a8b..3438063f76 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -126,10 +126,7 @@ let print_mutual_inductive env mind mib udecl = hov 0 (def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env sigma mib) inds ++ - match mib.mind_universes with - | Monomorphic_ind _ | Polymorphic_ind _ -> str "" - | Cumulative_ind cumi -> - Printer.pr_abstract_cumulativity_info sigma cumi) + Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes) let get_fields = let rec prodec_rec l subst c = @@ -178,10 +175,7 @@ let print_record env mind mib udecl = (fun (id,b,c) -> Id.print id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - match mib.mind_universes with - | Monomorphic_ind _ | Polymorphic_ind _ -> str "" - | Cumulative_ind cumi -> - Printer.pr_abstract_cumulativity_info sigma cumi + Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes ) let pr_mutual_inductive_body env mind mib udecl = @@ -302,7 +296,7 @@ let print_body is_impl extent env mp (l,body) = hov 2 (str ":= " ++ Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ - Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs) + Printer.pr_abstract_universe_ctx sigma ctx ?priv:cb.const_private_poly_univs) | SFBmind mib -> match extent with | WithContents -> diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index c1ea067567..878e9f477b 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -546,7 +546,7 @@ let to_constr p = module GoalMap = Evar.Map -let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma) +let goal_to_evar g sigma = Id.to_string (Termops.evar_suggested_name g sigma) open Goal.Set |