diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 35 | ||||
| -rw-r--r-- | printing/printer.mli | 12 | ||||
| -rw-r--r-- | printing/printing.mllib | 1 | ||||
| -rw-r--r-- | printing/printmod.ml | 458 | ||||
| -rw-r--r-- | printing/printmod.mli | 26 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 4 |
6 files changed, 47 insertions, 489 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 2ad9e268c2..96213b3b8b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -16,7 +16,6 @@ open Constr open Context open Environ open Evd -open Refiner open Constrextern open Ppconstr open Declarations @@ -173,6 +172,38 @@ let safe_gen f env sigma c = let safe_pr_lconstr_env = safe_gen pr_lconstr_env let safe_pr_constr_env = safe_gen pr_constr_env +let u_ident = Id.of_string "u" + +let universe_binders_with_opt_names orig names = + let orig = Univ.AUContext.names orig in + let orig = Array.to_list orig in + let udecl = match names with + | None -> orig + | Some udecl -> + try + List.map2 (fun orig {CAst.v = na} -> + match na with + | Anonymous -> orig + | Name id -> Name id) orig udecl + with Invalid_argument _ -> + let len = List.length orig in + CErrors.user_err ~hdr:"universe_binders_with_opt_names" + Pp.(str "Universe instance should have length " ++ int len) + in + let fold_named i ubind = function + | Name id -> Id.Map.add id (Univ.Level.var i) ubind + | Anonymous -> ubind + in + let ubind = List.fold_left_i fold_named 0 UnivNames.empty_binders udecl in + let fold_anons i (u_ident, ubind) = function + | Name _ -> u_ident, ubind + | Anonymous -> + let id = Namegen.next_ident_away_from u_ident (fun id -> Id.Map.mem id ubind) in + (id, Id.Map.add id (Univ.Level.var i) ubind) + in + let (_, ubind) = List.fold_left_i fold_anons 0 (u_ident, ubind) udecl in + ubind + let pr_universe_ctx_set sigma c = if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) @@ -421,7 +452,7 @@ let pr_transparent_state ts = *) let pr_goal ?(diffs=false) ?og_s g_s = let g = sig_it g_s in - let sigma = project g_s in + let sigma = Tacmach.project g_s in let env = Goal.V82.env sigma g in let concl = Goal.V82.concl sigma g in let goal = diff --git a/printing/printer.mli b/printing/printer.mli index 8c633b5e79..8805819890 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -132,6 +132,18 @@ val pr_universes : evar_map -> ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t -> Declarations.universes -> Pp.t +(** [universe_binders_with_opt_names ref l] + + If [l] is [Some univs] return the universe binders naming the + bound levels of [ref] by [univs] (generating names for Anonymous). + May error if the lengths mismatch. + + Otherwise return the bound universe names registered for [ref]. + + Inefficient on large contexts due to name generation. *) +val universe_binders_with_opt_names : Univ.AUContext.t -> + UnivNames.univ_name_list option -> UnivNames.universe_binders + (** Printing global references using names as short as possible *) val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t diff --git a/printing/printing.mllib b/printing/printing.mllib index 5b5b6590a4..39e160706b 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -3,4 +3,3 @@ Pputils Ppconstr Proof_diffs Printer -Printmod diff --git a/printing/printmod.ml b/printing/printmod.ml deleted file mode 100644 index eec2fe86ac..0000000000 --- a/printing/printmod.ml +++ /dev/null @@ -1,458 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * 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 Constr -open Context -open Pp -open Names -open Environ -open Declarations -open Libnames -open Goptions - -(** Note: there is currently two modes for printing modules. - - The "short" one, that just prints the names of the fields. - - The "rich" one, that also tries to print the types of the fields. - The short version used to be the default behavior, but now we print - types by default. The following option allows changing this. -*) - -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 - -type short = OnlyNames | WithContents - -let short = ref false - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Short";"Module";"Printing"]; - optread = (fun () -> !short) ; - optwrite = ((:=) short) } - -(** Each time we have to print a non-globally visible structure, - we place its elements in a fake fresh namespace. *) - -let mk_fake_top = - let r = ref 0 in - fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r)) - -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 = - let dir = DirPath.make [id] in - if not (Nametab.exists_dir dir) then - id - else - get_id (Id.Set.add id l) (Namegen.next_ident_away id l) - in - let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in - get_id avoid id - -(** Inductive declarations *) - -open Reduction - -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 sigma names types = - let pc = - prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (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) - -let build_ind_type mip = - Inductive.type_of_inductive mip - -let print_one_inductive env sigma mib ((_,i) as ind) = - 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 - let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((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_assum env nparamdecls c args) cstrtypes in - let envpar = push_rel_context params env in - let inst = - if Declareops.inductive_is_polymorphic mib then - Printer.pr_universe_instance sigma u - else mt () - in - hov 0 ( - 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 udecl = - let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) - in - let keyword = - let open Declarations in - match mib.mind_finite with - | Finite -> "Inductive" - | BiFinite -> "Variant" - | CoFinite -> "CoInductive" - in - let bl = UnivNames.universe_binders_with_opt_names - (Declareops.inductive_polymorphic_context mib) udecl - in - let sigma = Evd.from_ctx (UState.of_binders bl) in - hov 0 (def keyword ++ spc () ++ - prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env sigma mib) inds ++ - Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes) - -let get_fields = - let rec prodec_rec l subst c = - match kind c with - | Prod (na,t,c) -> - let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in - prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c - | LetIn (na,b,_,c) -> - let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in - prodec_rec ((id,false,Vars.substl subst b)::l) (mkVar id::subst) c - | _ -> List.rev l - in - prodec_rec [] [] - -let print_record env mind mib udecl = - 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 - let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in - let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) 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 = UnivNames.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib) - udecl - in - let sigma = Evd.from_ctx (UState.of_binders bl) in - let keyword = - let open Declarations in - match mib.mind_finite with - | BiFinite -> "Record" - | Finite -> "Inductive" - | CoFinite -> "CoInductive" - in - hov 0 ( - hov 0 ( - 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 ":= " ++ Id.print mip.mind_consnames.(0)) ++ - brk(1,2) ++ - hv 2 (str "{ " ++ - prlist_with_sep (fun () -> str ";" ++ brk(2,0)) - (fun (id,b,c) -> - Id.print id ++ str (if b then " : " else " := ") ++ - Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes - ) - -let pr_mutual_inductive_body env mind mib udecl = - if mib.mind_record != NotRecord && not !Flags.raw_print then - print_record env mind mib udecl - else - print_mutual_inductive env mind mib udecl - -(** Modpaths *) - -let rec print_local_modpath locals = function - | MPbound mbid -> Id.print (Util.List.assoc_f MBId.equal mbid locals) - | MPdot(mp,l) -> - print_local_modpath locals mp ++ str "." ++ Label.print l - | MPfile _ -> raise Not_found - -let print_modpath locals mp = - try (* must be with let because streams are lazy! *) - let qid = Nametab.shortest_qualid_of_module mp in - pr_qualid qid - with - | Not_found -> print_local_modpath locals mp - -let print_kn locals kn = - try - let qid = Nametab.shortest_qualid_of_modtype kn in - pr_qualid qid - with - Not_found -> - try - print_local_modpath locals kn - with - Not_found -> print_modpath locals kn - -let nametab_register_dir obj_mp = - let id = mk_fake_top () in - let obj_dir = DirPath.make [id] in - Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; })) - -(** Nota: the [global_reference] we register in the nametab below - might differ from internal ones, since we cannot recreate here - the canonical part of constant and inductive names, but only - the user names. This works nonetheless since we search now - [Nametab.the_globrevtab] modulo user name. *) - -let nametab_register_body mp dir (l,body) = - let push id ref = - Nametab.push (Nametab.Until (1+List.length (DirPath.repr dir))) - (make_path dir id) ref - in - match body with - | SFBmodule _ -> () (* TODO *) - | SFBmodtype _ -> () (* TODO *) - | SFBconst _ -> - push (Label.to_id l) (GlobRef.ConstRef (Constant.make2 mp l)) - | SFBmind mib -> - let mind = MutInd.make2 mp l in - Array.iteri - (fun i mip -> - push mip.mind_typename (GlobRef.IndRef (mind,i)); - Array.iteri (fun j id -> push id (GlobRef.ConstructRef ((mind,i),j+1))) - mip.mind_consnames) - mib.mind_packets - -type mod_ops = - { import_module : export:bool -> ModPath.t -> unit - ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit - } - -let nametab_register_module_body ~mod_ops mp struc = - (* If [mp] is a globally visible module, we simply import it *) - try mod_ops.import_module ~export:false mp - with Not_found -> - (* Otherwise we try to emulate an import by playing with nametab *) - nametab_register_dir mp; - List.iter (nametab_register_body mp DirPath.empty) struc - -let get_typ_expr_alg mtb = match mtb.mod_type_alg with - | Some (NoFunctor me) -> me - | _ -> raise Not_found - -let nametab_register_modparam ~mod_ops mbid mtb = - let id = MBId.to_id mbid in - match mtb.mod_type with - | MoreFunctor _ -> id (* functorial param : nothing to register *) - | NoFunctor struc -> - (* We first try to use the algebraic type expression if any, - via a Declaremods function that converts back to module entries *) - try - let () = mod_ops.process_module_binding mbid (get_typ_expr_alg mtb) in - id - with e when CErrors.noncritical e -> - (* Otherwise, we try to play with the nametab ourselves *) - let mp = MPbound mbid in - let check id = Nametab.exists_dir (DirPath.make [id]) in - let id = Namegen.next_ident_away_from id check in - let dir = DirPath.make [id] in - nametab_register_dir mp; - List.iter (nametab_register_body mp dir) struc; - id - -let print_body is_impl extent env mp (l,body) = - 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 - (match cb.const_body with - | Def _ -> def "Definition" ++ spc () - | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () - | _ -> def "Parameter" ++ spc ()) ++ name ++ - (match extent with - | OnlyNames -> mt () - | WithContents -> - let bl = UnivNames.universe_binders_with_opt_names ctx None in - let sigma = Evd.from_ctx (UState.of_binders bl) in - str " :" ++ spc () ++ - 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 sigma (Mod_subst.force_constr l)) - | _ -> mt ()) ++ str "." ++ - Printer.pr_abstract_universe_ctx sigma ctx) - | SFBmind mib -> - match extent with - | WithContents -> - pr_mutual_inductive_body env (MutInd.make2 mp l) mib None - | OnlyNames -> - let keyword = - let open Declarations in - match mib.mind_finite with - | Finite -> def "Inductive" - | BiFinite -> def "Variant" - | CoFinite -> def "CoInductive" - in - keyword ++ spc () ++ name) - -let print_struct is_impl extent env mp struc = - prlist_with_sep spc (print_body is_impl extent env mp) struc - -let print_structure ~mod_ops is_type extent env mp locals struc = - let env' = Modops.add_structure mp struc Mod_subst.empty_delta_resolver env in - nametab_register_module_body ~mod_ops mp struc; - let kwd = if is_type then "Sig" else "Struct" in - hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++ - brk (1,-2) ++ keyword "End") - -let rec flatten_app mexpr l = match mexpr with - | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l) - | MEident mp -> mp::l - | MEwith _ -> assert false - -let rec print_typ_expr extent env mp locals mty = - match mty with - | MEident kn -> print_kn locals kn - | MEapply _ -> - let lapp = flatten_app mty [] in - let fapp = List.hd lapp in - 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, _)))-> - let s = String.concat "." (List.map Id.to_string idl) in - let body = match extent with - | WithContents -> - let sigma = Evd.from_env env in - spc() ++ str ":=" ++ spc() ++ Printer.pr_lconstr_env env sigma c - | OnlyNames -> - mt() in - hov 2 (print_typ_expr extent env mp locals me ++ spc() ++ str "with" ++ spc() - ++ def "Definition"++ spc() ++ str s ++ body) - | MEwith(me,WithMod(idl,mp'))-> - let s = String.concat "." (List.map Id.to_string idl) in - let body = match extent with - | WithContents -> - spc() ++ str ":="++ spc() ++ print_modpath locals mp' - | OnlyNames -> mt () in - hov 2 (print_typ_expr extent env mp locals me ++ spc() ++ str "with" ++ spc() ++ - keyword "Module"++ spc() ++ str s ++ body) - -let print_mod_expr env mp locals = function - | MEident mp -> print_modpath locals mp - | MEapply _ as me -> - let lapp = flatten_app me [] in - hov 3 - (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")") - | MEwith _ -> assert false (* No 'with' syntax for modules *) - -let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function - | NoFunctor me -> fatom ~mod_ops is_type extent env mp locals me - | MoreFunctor (mbid,mtb1,me2) -> - let id = nametab_register_modparam ~mod_ops mbid mtb1 in - let mp1 = MPbound mbid in - let pr_mtb1 = fty ~mod_ops extent env mp1 locals mtb1 in - let env' = Modops.add_module_type mp1 mtb1 env in - let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in - let kwd = if is_type then "Funsig" else "Functor" in - hov 2 - (keyword kwd ++ spc () ++ - str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ - spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2) - -let rec print_expression ~mod_ops x = - print_functor ~mod_ops - print_modtype - (fun ~mod_ops -> function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x - -and print_signature ~mod_ops x = - print_functor ~mod_ops print_modtype print_structure x - -and print_modtype ~mod_ops extent env mp locals mtb = match mtb.mod_type_alg with - | Some me -> print_expression ~mod_ops true extent env mp locals me - | None -> print_signature ~mod_ops true extent env mp locals mtb.mod_type - -let rec printable_body dir = - let dir = pop_dirpath dir in - DirPath.is_empty dir || - try - let open Nametab.GlobDirRef in - match Nametab.locate_dir (qualid_of_dirpath dir) with - DirOpenModtype _ -> false - | DirModule _ | DirOpenModule _ -> printable_body dir - | _ -> true - with - Not_found -> true - -(** Since we might play with nametab above, we should reset to prior - state after the printing *) - -let print_expression' ~mod_ops is_type extent env mp me = - States.with_state_protection - (fun e -> print_expression ~mod_ops is_type extent env mp [] e) me - -let print_signature' ~mod_ops is_type extent env mp me = - States.with_state_protection - (fun e -> print_signature ~mod_ops is_type extent env mp [] e) me - -let unsafe_print_module ~mod_ops extent env mp with_body mb = - let name = print_modpath [] mp in - let pr_equals = spc () ++ str ":= " in - let body = match with_body, mb.mod_expr with - | false, _ - | true, Abstract -> mt() - | _, Algebraic me -> pr_equals ++ print_expression' ~mod_ops false extent env mp me - | _, Struct sign -> pr_equals ++ print_signature' ~mod_ops false extent env mp sign - | _, FullStruct -> pr_equals ++ print_signature' ~mod_ops false extent env mp mb.mod_type - in - let modtype = match mb.mod_expr, mb.mod_type_alg with - | FullStruct, _ -> mt () - | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' ~mod_ops true extent env mp ty - | _, _ -> brk (1,1) ++ str": " ++ print_signature' ~mod_ops true extent env mp mb.mod_type - in - hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body) - -exception ShortPrinting - -let print_module ~mod_ops with_body mp = - let me = Global.lookup_module mp in - try - if !short then raise ShortPrinting; - unsafe_print_module ~mod_ops WithContents - (Global.env ()) mp with_body me ++ fnl () - with e when CErrors.noncritical e -> - unsafe_print_module ~mod_ops OnlyNames - (Global.env ()) mp with_body me ++ fnl () - -let print_modtype ~mod_ops kn = - let mtb = Global.lookup_modtype kn in - let name = print_kn [] kn in - hv 1 - (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++ - try - if !short then raise ShortPrinting; - print_signature' ~mod_ops true WithContents - (Global.env ()) kn mtb.mod_type - with e when CErrors.noncritical e -> - print_signature' ~mod_ops true OnlyNames - (Global.env ()) kn mtb.mod_type) diff --git a/printing/printmod.mli b/printing/printmod.mli deleted file mode 100644 index c7f056063b..0000000000 --- a/printing/printmod.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * 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 Names - -(** false iff the module is an element of an open module type *) -val printable_body : DirPath.t -> bool - -val pr_mutual_inductive_body : Environ.env -> - MutInd.t -> Declarations.mutual_inductive_body -> - UnivNames.univ_name_list option -> Pp.t - -type mod_ops = - { import_module : export:bool -> ModPath.t -> unit - ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit - } - -val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t -val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index c78cc96a83..43f70dfecc 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -335,7 +335,7 @@ let unwrap g_s = match g_s with | Some g_s -> let goal = Evd.sig_it g_s in - let sigma = Refiner.project g_s in + let sigma = Tacmach.project g_s in goal_info goal sigma | None -> ([], CString.Map.empty, Pp.mt ()) @@ -545,7 +545,7 @@ let match_goals ot nt = let get_proof_context (p : Proof.t) = let Proof.{goals; sigma} = Proof.data p in - sigma, Refiner.pf_env { Evd.it = List.(hd goals); sigma } + sigma, Tacmach.pf_env { Evd.it = List.(hd goals); sigma } let to_constr pf = let open CAst in |