diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | printing/prettyp.ml | 57 | ||||
| -rw-r--r-- | printing/printer.ml | 2 | ||||
| -rw-r--r-- | printing/printmod.ml | 30 |
4 files changed, 74 insertions, 21 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a15cadfa0b..a68b569cbe 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -105,7 +105,7 @@ open Decl_kinds | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -490,7 +490,7 @@ open Decl_kinds | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,gopt) -> - pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -1132,7 +1132,7 @@ open Decl_kinds | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in let pr_i = match io with None -> mt () - | Some i -> Proof_global.pr_goal_selector i ++ str ": " in + | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index faa69f41e5..827c0e4583 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -70,7 +70,8 @@ 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 = - let typ = Global.type_of_global_unsafe ref in + 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 = EConstr.of_constr typ in let typ = if reduce then @@ -78,6 +79,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 @@ -135,7 +138,7 @@ let print_renames_list prefix l = hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))] let need_expansion impl ref = - let typ = Global.type_of_global_unsafe ref in + let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in let ctx = prod_assum typ in let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && @@ -503,15 +506,48 @@ 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 = Global.universes_of_constant_body cb in + let univs = + let otab = Global.opaque_tables () in + match cb.const_body with + | Undef _ | Def _ -> + begin + match cb.const_universes with + | Monomorphic_const ctx -> ctx + | Polymorphic_const ctx -> + let inst = Univ.AUContext.instance ctx in + Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) + end + | OpaqueDef o -> + let body_uctxs = Opaqueproof.force_constraints otab o in + match cb.const_universes with + | Monomorphic_const ctx -> + let uctxs = Univ.ContextSet.of_context ctx in + Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + | Polymorphic_const ctx -> + assert(Univ.ContextSet.is_empty body_uctxs); + let inst = Univ.AUContext.instance ctx in + Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) + in let ctx = Evd.evar_universe_context_of_binders (Universes.universe_binders_of_global (ConstRef sp)) @@ -525,9 +561,10 @@ let print_constant with_values sep sp = print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ Printer.pr_universe_ctx 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 (val_0,typ) else pr_ltype typ)++ + (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universe_ctx sigma univs) let gallina_print_constant_with_infos sp = @@ -765,9 +802,11 @@ let print_opaque_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> - let open EConstr in - let ty = Universes.unsafe_type_of_global gr in + 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) | VarRef id -> env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl diff --git a/printing/printer.ml b/printing/printer.ml index 2a198d4564..3516788022 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -805,7 +805,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ - (let s = Proof_global.Bullet.suggest p in + (let s = Proof_bullet.suggest p in if Pp.ismt s then s else fnl () ++ s) ++ fnl () in diff --git a/printing/printmod.ml b/printing/printmod.ml index 10b791e37f..5c7dcdc10f 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 ( @@ -108,6 +110,17 @@ 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 subtyp = ACumulativityInfo.subtyp_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, expose subtyp) + let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in @@ -131,7 +144,7 @@ let print_mutual_inductive env mind mib = | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> Printer.pr_cumulativity_info - sigma (Univ.instantiate_cumulativity_info cumi)) + sigma (instantiate_cumulativity_info cumi)) let get_fields = let rec prodec_rec l subst c = @@ -149,7 +162,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 @@ -189,7 +202,7 @@ let print_record env mind mib = | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> Printer.pr_cumulativity_info - sigma (Univ.instantiate_cumulativity_info cumi) + sigma (instantiate_cumulativity_info cumi) ) let pr_mutual_inductive_body env mind mib = @@ -292,11 +305,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 +331,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 |