diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 58 | ||||
| -rw-r--r-- | printing/printer.ml | 21 | ||||
| -rw-r--r-- | printing/printer.mli | 5 | ||||
| -rw-r--r-- | printing/printmod.ml | 55 |
4 files changed, 47 insertions, 92 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9ed985195f..66f748454d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -71,17 +71,17 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref udecl = - let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in - let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in + let typ, univs = Global.type_of_global_in_context (Global.env ()) ref in + let inst = Univ.make_abstract_instance univs in + let bl = UnivNames.universe_binders_with_opt_names ref udecl in + let sigma = Evd.from_ctx (UState.of_binders bl) in let typ = EConstr.of_constr typ in let typ = if reduce then let env = Global.env () in - let sigma = Evd.from_env env in let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in - let univs = Global.universes_of_global ref in let variance = match ref with | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> @@ -91,19 +91,14 @@ let print_ref reduce ref udecl = | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) end in - let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in let env = Global.env () in - let bl = UnivNames.universe_binders_with_opt_names ref - (Array.to_list (Univ.Instance.to_array inst)) udecl in - let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = if Global.is_polymorphic ref - then Printer.pr_universe_instance sigma (Univ.UContext.instance univs) + then Printer.pr_universe_instance sigma inst else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_universe_ctx sigma ?variance univs) + Printer.pr_abstract_universe_ctx sigma ?variance univs) (********************************) (** Printing implicit arguments *) @@ -552,48 +547,31 @@ let print_typed_body env evd (val_0,typ) = let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then let univs = Declareops.constant_polymorphic_context cb in - let inst = Univ.AUContext.instance univs in + let inst = Univ.make_abstract_instance univs in pr_universe_instance sigma inst else mt() let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in - let typ = - match cb.const_universes with - | Monomorphic_const _ -> cb.const_type - | Polymorphic_const univs -> - let inst = Univ.AUContext.instance univs in - Vars.subst_instance_constr inst cb.const_type - in - let univs, ulist = - let open Entries in + let typ = cb.const_type in + let univs = let open Univ in let otab = Global.opaque_tables () in match cb.const_body with - | Undef _ | Def _ -> - begin - match cb.const_universes with - | Monomorphic_const ctx -> Monomorphic_const_entry ctx, [] - | Polymorphic_const ctx -> - let inst = AUContext.instance ctx in - Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)), - Array.to_list (Instance.to_array inst) - end + | Undef _ | Def _ -> cb.const_universes | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with | Monomorphic_const ctx -> - Monomorphic_const_entry (ContextSet.union body_uctxs ctx), [] + Monomorphic_const (ContextSet.union body_uctxs ctx) | Polymorphic_const ctx -> assert(ContextSet.is_empty body_uctxs); - let inst = AUContext.instance ctx in - Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)), - Array.to_list (Instance.to_array inst) + Polymorphic_const ctx in let ctx = UState.of_binders - (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl) + (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in @@ -605,7 +583,6 @@ let print_constant with_values sep sp udecl = str" ]" ++ Printer.pr_constant_universes sigma univs | Some (c, ctx) -> - let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in 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) @@ -712,11 +689,6 @@ let print_eval x = !object_pr.print_eval x (**** Printing declarations and judgments *) (**** Abstract layer *****) -let print_typed_value x = - let env = Global.env () in - let sigma = Evd.from_env env in - print_typed_value_in_env env sigma x - let print_judgment env sigma {uj_val=trm;uj_type=typ} = print_typed_value_in_env env sigma (trm, typ) @@ -852,11 +824,9 @@ let print_opaque_name env sigma qid = print_inductive sp None | ConstructRef cstr as gr -> let ty, ctx = Global.type_of_global_in_context env gr in - let inst = Univ.AUContext.instance ctx in - let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in let open EConstr in - print_typed_value (mkConstruct cstr, ty) + print_typed_value_in_env env sigma (mkConstruct cstr, ty) | VarRef id -> env |> lookup_named id |> print_named_decl env sigma diff --git a/printing/printer.ml b/printing/printer.ml index 5ca330d377..6cd4daa374 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -192,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 " *)" @@ -270,9 +270,16 @@ let pr_universe_ctx sigma ?variance c = else mt() +let pr_abstract_universe_ctx sigma ?variance c = + if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c + else + mt() + let pr_constant_universes sigma = function - | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx - | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx + | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx + | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx let pr_cumulativity_info sigma cumi = if !Detyping.print_universes @@ -282,6 +289,14 @@ let pr_cumulativity_info 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 (fun uii -> v 0 + (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + else + mt() + (**********************************************************************) (* Global references *) diff --git a/printing/printer.mli b/printing/printer.mli index 518c5b930b..96db7091a6 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -123,9 +123,12 @@ val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t 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 -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t -val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t +val pr_constant_universes : evar_map -> 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 (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index e2d9850bf8..1fc308ac99 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -90,9 +90,7 @@ let build_ind_type env mip = Inductive.type_of_inductive env mip let print_one_inductive env sigma mib ((_,i) as ind) = - let u = if Declareops.inductive_is_polymorphic mib then - Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) - else Univ.Instance.empty in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in @@ -111,16 +109,6 @@ let print_one_inductive env sigma mib ((_,i) as ind) = str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes -let instantiate_cumulativity_info cumi = - let open Univ in - let univs = ACumulativityInfo.univ_context cumi in - let expose ctx = - let inst = AUContext.instance ctx in - let cst = AUContext.instantiate inst ctx in - UContext.make (inst, cst) - in - CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi) - let print_mutual_inductive env mind mib udecl = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in @@ -131,14 +119,7 @@ let print_mutual_inductive env mind mib udecl = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in - let univs = - let open Univ in - if Declareops.inductive_is_polymorphic mib then - Array.to_list (Instance.to_array - (AUContext.instance (Declareops.inductive_polymorphic_context mib))) - else [] - in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative @@ -150,8 +131,7 @@ let print_mutual_inductive env mind mib udecl = match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> - Printer.pr_cumulativity_info - sigma (instantiate_cumulativity_info cumi)) + Printer.pr_abstract_cumulativity_info sigma cumi) let get_fields = let rec prodec_rec l subst c = @@ -167,11 +147,7 @@ let get_fields = prodec_rec [] [] let print_record env mind mib udecl = - let u = - if Declareops.inductive_is_polymorphic mib then - Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) - else Univ.Instance.empty - in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in @@ -181,8 +157,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 (IndRef (mind,0)) - (Array.to_list (Univ.Instance.to_array u)) udecl in + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in @@ -210,8 +185,7 @@ let print_record env mind mib udecl = match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> - Printer.pr_cumulativity_info - sigma (instantiate_cumulativity_info cumi) + Printer.pr_abstract_cumulativity_info sigma cumi ) let pr_mutual_inductive_body env mind mib udecl = @@ -315,12 +289,6 @@ let print_body is_impl env mp (l,body) = | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> let ctx = Declareops.constant_polymorphic_context cb in - let u = - if Declareops.constant_is_polymorphic cb then - Univ.AUContext.instance ctx - else Univ.Instance.empty - in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -328,18 +296,17 @@ let print_body is_impl env mp (l,body) = (match env with | None -> mt () | Some env -> + let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in + let sigma = Evd.from_ctx (UState.of_binders bl) in str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env (Evd.from_env env) - (Vars.subst_instance_constr u - cb.const_type)) ++ + hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env (Evd.from_env env) - (Vars.subst_instance_constr u (Mod_subst.force_constr l))) + Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx (Evd.from_env env) ctx) + Printer.pr_abstract_universe_ctx sigma ctx) | SFBmind mib -> try let env = Option.get env in |