diff options
author | 2017-07-13 15:05:48 +0200 | |
---|---|---|
committer | 2017-07-13 15:05:48 +0200 | |
commit | e3eb17a728d7b6874e67462e8a83fac436441872 (patch) | |
tree | c7932e27be16f4d2c20da8d61c3a61b101be7f70 /printing | |
parent | 9427b99b167842bc4a831def815c4824030d518f (diff) | |
parent | 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 (diff) |
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel
Diffstat (limited to 'printing')
-rw-r--r-- | printing/prettyp.ml | 18 | ||||
-rw-r--r-- | printing/printmod.ml | 15 |
2 files changed, 25 insertions, 8 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 15c0f80b9..ff12737f6 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -78,6 +78,8 @@ let print_ref reduce ref = in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref 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 = Universes.universe_binders_of_global ref in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in @@ -503,13 +505,25 @@ let ungeneralized_type_of_constant_type t = let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then - pr_universe_instance sigma (Declareops.constant_polymorphic_context cb) + let univs = Declareops.constant_polymorphic_context cb in + let inst = Univ.AUContext.instance univs in + let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + pr_universe_instance sigma univs else mt() let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in - let typ = Declareops.type_of_constant cb in + let typ = match cb.const_type with + | RegularArity t as x -> + begin match cb.const_universes with + | Monomorphic_const _ -> x + | Polymorphic_const univs -> + let inst = Univ.AUContext.instance univs in + RegularArity (Vars.subst_instance_constr inst t) + end + | TemplateArity _ as x -> x + in let typ = ungeneralized_type_of_constant_type typ in let univs = let otab = Global.opaque_tables () in diff --git a/printing/printmod.ml b/printing/printmod.ml index 10b791e37..2e0e6d284 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -89,7 +89,7 @@ let build_ind_type env mip = let print_one_inductive env sigma mib ((_,i) as ind) = let u = if Declareops.inductive_is_polymorphic mib then - Declareops.inductive_polymorphic_instance mib + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in @@ -100,7 +100,9 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let envpar = push_rel_context params env in let inst = if Declareops.inductive_is_polymorphic mib then - Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib) + let ctx = Declareops.inductive_polymorphic_context mib in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in + Printer.pr_universe_instance sigma ctx else mt () in hov 0 ( @@ -149,7 +151,7 @@ let get_fields = let print_record env mind mib = let u = if Declareops.inductive_is_polymorphic mib then - Declareops.inductive_polymorphic_instance mib + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) else Univ.Instance.empty in let mip = mib.mind_packets.(0) in @@ -292,11 +294,13 @@ let print_body is_impl env mp (l,body) = | SFBmodule _ -> keyword "Module" ++ spc () ++ name | 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 - Declareops.constant_polymorphic_instance cb + Univ.AUContext.instance ctx else Univ.Instance.empty in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () @@ -316,8 +320,7 @@ let print_body is_impl env mp (l,body) = Printer.pr_lconstr_env env sigma (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx sigma - (Declareops.constant_polymorphic_context cb)) + Printer.pr_universe_ctx sigma ctx) | SFBmind mib -> try let env = Option.get env in |