diff options
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 206 |
1 files changed, 120 insertions, 86 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index dfa66d43..e076c10f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -1,18 +1,19 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util -open Term +open Constr open Pp open Names open Environ open Declarations -open Nameops open Globnames open Libnames open Goptions @@ -26,12 +27,23 @@ open Goptions the "short" mode or (Some env) in the "rich" one. *) +module Tag = +struct + + let definition = "module.definition" + let keyword = "module.keyword" + +end + +let tag t s = Pp.tag t s +let tag_definition s = tag Tag.definition s +let tag_keyword s = tag Tag.keyword s + let short = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "short module printing"; optkey = ["Short";"Module";"Printing"]; optread = (fun () -> !short) ; @@ -44,14 +56,8 @@ let mk_fake_top = let r = ref 0 in fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r)) -module Make (Taggers : sig - val tag_definition : std_ppcmds -> std_ppcmds - val tag_keyword : std_ppcmds -> std_ppcmds -end) = -struct - -let def s = Taggers.tag_definition (str s) -let keyword s = Taggers.tag_keyword (str s) +let def s = tag_definition (str s) +let keyword s = tag_keyword (str s) let get_new_id locals id = let rec get_id l id = @@ -59,9 +65,10 @@ let get_new_id locals id = if not (Nametab.exists_module dir) then id else - get_id (id::l) (Namegen.next_ident_away id l) + get_id (Id.Set.add id l) (Namegen.next_ident_away id l) in - get_id (List.map snd locals) id + let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in + get_id avoid id (** Inductive declarations *) @@ -74,7 +81,7 @@ let print_params env sigma params = 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 sigma c) + (fun (id,c) -> Id.print 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,47 +90,74 @@ 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 mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + let u = if Declareops.inductive_is_polymorphic mib then + 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 - let args = Context.Rel.to_extended_list 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let nparamdecls = Context.Rel.length params in + let args = Context.Rel.to_extended_list mkRel 0 params in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in 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 cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls 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 + if Declareops.inductive_is_polymorphic mib then + 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 ( - pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ + Id.print 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 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 let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> "Inductive" | 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 sigma mib) inds ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + 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 = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs 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 + (Declareops.inductive_is_polymorphic mib) + (Declareops.inductive_is_cumulative mib) ++ + 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_cumulativity_info + sigma (instantiate_cumulativity_info cumi)) let get_fields = let rec prodec_rec l subst c = - match kind_of_term c with + match kind c with | Prod (na,t,c) -> let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c @@ -134,24 +168,26 @@ let get_fields = in prodec_rec [] [] -let print_record env mind mib = +let print_record env mind mib udecl = let u = - if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + if Declareops.inductive_is_polymorphic mib then + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) else Univ.Instance.empty in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = Context.Rel.to_extended_list 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let nparamdecls = Context.Rel.length params in + let args = Context.Rel.to_extended_list mkRel 0 params in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in - let cstrtype = hnf_prod_applist env cstrtypes.(0) args in + 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 = Universes.universe_binders_of_global (IndRef (mind,0)) in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) + (Array.to_list (Univ.Instance.to_array u)) udecl in + let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | BiFinite -> "Record" | Finite -> "Inductive" @@ -159,31 +195,39 @@ let print_record env mind mib = in hov 0 ( hov 0 ( - Printer.pr_polymorphic mib.mind_polymorphic ++ - def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ + Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ + Printer.pr_cumulative + (Declareops.inductive_is_polymorphic mib) + (Declareops.inductive_is_cumulative mib) ++ + def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ - str ":= " ++ pr_id mip.mind_consnames.(0)) ++ + str ":= " ++ Id.print 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 " := ") ++ + Id.print id ++ str (if b then " : " else " := ") ++ 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 = + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> str "" + | Cumulative_ind cumi -> + Printer.pr_cumulativity_info + sigma (instantiate_cumulativity_info cumi) + ) + +let pr_mutual_inductive_body env mind mib udecl = if mib.mind_record <> None && not !Flags.raw_print then - print_record env mind mib + print_record env mind mib udecl else - print_mutual_inductive env mind mib + print_mutual_inductive env mind mib udecl (** Modpaths *) let rec print_local_modpath locals = function - | MPbound mbid -> pr_id (Util.List.assoc_f MBId.equal mbid locals) + | MPbound mbid -> Id.print (Util.List.assoc_f MBId.equal mbid locals) | MPdot(mp,l) -> - print_local_modpath locals mp ++ str "." ++ pr_lab l + print_local_modpath locals mp ++ str "." ++ Label.print l | MPfile _ -> raise Not_found let print_modpath locals mp = @@ -204,10 +248,10 @@ let print_kn locals kn = with Not_found -> print_modpath locals kn -let nametab_register_dir mp = +let nametab_register_dir obj_mp = let id = mk_fake_top () in - let dir = DirPath.make [id] in - Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty))) + let obj_dir = DirPath.make [id] in + Nametab.push_dir (Nametab.Until 1) obj_dir (DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here @@ -267,15 +311,18 @@ let nametab_register_modparam mbid mtb = id let print_body is_impl env mp (l,body) = - let name = pr_label l in + let name = Label.print l in hov 2 (match body with | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> + let ctx = Declareops.constant_polymorphic_context cb in let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + 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 let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () @@ -287,7 +334,7 @@ let print_body is_impl env mp (l,body) = str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma (Vars.subst_instance_constr u - (Typeops.type_of_constant_type env cb.const_type))) ++ + cb.const_type)) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ @@ -295,14 +342,14 @@ 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 (Univ.instantiate_univ_context cb.const_universes)) + Printer.pr_universe_ctx sigma ctx) | SFBmind mib -> try let env = Option.get env in - pr_mutual_inductive_body env (MutInd.make2 mp l) mib + pr_mutual_inductive_body env (MutInd.make2 mp l) mib None with e when CErrors.noncritical e -> let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> def "Inductive" | BiFinite -> def "Variant" @@ -338,9 +385,12 @@ let rec print_typ_expr env mp locals mty = | 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 + (* XXX: What should env and sigma be here? *) + let env = Global.env () in + let sigma = Evd.empty in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() - ++ Printer.pr_lconstr c) + ++ Printer.pr_lconstr_env env sigma 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() ++ @@ -366,7 +416,7 @@ let rec print_functor fty fatom is_type env mp locals = function let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ - str "(" ++ pr_id id ++ str ":" ++ pr_mtb1 ++ str ")" ++ + str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ spc() ++ print_functor fty fatom is_type env' mp locals' me2) let rec print_expression x = @@ -397,11 +447,11 @@ let rec printable_body dir = let print_expression' is_type env mp me = States.with_state_protection - (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me + (fun e -> print_expression is_type env mp [] e) me let print_signature' is_type env mp me = States.with_state_protection - (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me + (fun e -> print_signature is_type env mp [] e) me let unsafe_print_module env mp with_body mb = let name = print_modpath [] mp in @@ -441,20 +491,4 @@ let print_modtype kn = with e when CErrors.noncritical e -> print_signature' true None kn mtb.mod_type)) -end - -module Tag = -struct - let definition = - let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in - Ppstyle.make ~style ["module"; "definition"] - let keyword = - let style = Terminal.make ~bold:true () in - Ppstyle.make ~style ["module"; "keyword"] -end -include Make(struct - let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s - let tag_definition s = tag Tag.definition s - let tag_keyword s = tag Tag.keyword s -end) |