From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- printing/printmod.ml | 58 ++++++++++++++++++++++++++++++++++------------------ 1 file changed, 38 insertions(+), 20 deletions(-) (limited to 'printing/printmod.ml') diff --git a/printing/printmod.ml b/printing/printmod.ml index 295d8aaa..1d275c1a 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -72,10 +72,10 @@ let print_params env sigma params = if List.is_empty params then mt () else Printer.pr_rel_context env sigma params ++ brk(1,2) -let print_constructors envpar names types = +let print_constructors envpar sigma names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c) + (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c) (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) @@ -83,7 +83,7 @@ let print_constructors envpar names types = let build_ind_type env mip = Inductive.type_of_inductive env mip -let print_one_inductive env mib ((_,i) as ind) = +let print_one_inductive env sigma mib ((_,i) as ind) = let u = if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes else Univ.Instance.empty in @@ -94,10 +94,15 @@ let print_one_inductive env mib ((_,i) as ind) = let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in + let inst = + if mib.mind_polymorphic then + Printer.pr_universe_instance sigma mib.mind_universes + else mt () + in hov 0 ( - pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ - brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes + pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ + brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) @@ -109,11 +114,13 @@ let print_mutual_inductive env mind mib = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in + let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env mib) inds ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + (print_one_inductive env sigma mib) inds ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -142,6 +149,8 @@ let print_record env mind mib = let cstrtype = hnf_prod_applist env cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in + let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in + let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let keyword = let open Decl_kinds in match mib.mind_finite with @@ -153,16 +162,16 @@ let print_record env mind mib = hov 0 ( Printer.pr_polymorphic mib.mind_polymorphic ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ - print_params env Evd.empty params ++ - str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++ + print_params env sigma params ++ + str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ str ":= " ++ pr_id mip.mind_consnames.(0)) ++ brk(1,2) ++ hv 2 (str "{ " ++ prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ - Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++ - Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then @@ -259,6 +268,11 @@ let print_body is_impl env mp (l,body) = | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> + let u = + if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + else Univ.Instance.empty + in + let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -267,15 +281,17 @@ let print_body is_impl env mp (l,body) = | None -> mt () | Some env -> str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *) - (Typeops.type_of_constant_type env cb.const_type)) ++ + hov 0 (Printer.pr_ltype_env env sigma + (Vars.subst_instance_constr u + (Typeops.type_of_constant_type env cb.const_type))) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l)) + Printer.pr_lconstr_env env sigma + (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx cb.const_universes) + Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes)) | SFBmind mib -> try let env = Option.get env in @@ -315,15 +331,17 @@ let rec print_typ_expr env mp locals mty = let mapp = List.tl lapp in hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++ prlist_with_sep spc (print_modpath locals) mapp ++ str")") - | MEwith(me,WithDef(idl,c))-> + | MEwith(me,WithDef(idl,(c, _)))-> let env' = None in (* TODO: build a proper environment if env <> None *) let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() - ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) - | MEwith(me,WithMod(idl,mp))-> + ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() + ++ Printer.pr_lconstr c) + | MEwith(me,WithMod(idl,mp'))-> let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ - keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) + keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc() + ++ print_modpath locals mp') let print_mod_expr env mp locals = function | MEident mp -> print_modpath locals mp -- cgit v1.2.3