diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 8 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 2 | ||||
| -rw-r--r-- | printing/pputils.ml | 3 | ||||
| -rw-r--r-- | printing/prettyp.ml | 38 | ||||
| -rw-r--r-- | printing/prettyp.mli | 10 | ||||
| -rw-r--r-- | printing/printer.ml | 25 | ||||
| -rw-r--r-- | printing/printer.mli | 30 | ||||
| -rw-r--r-- | printing/printmod.ml | 23 | ||||
| -rw-r--r-- | printing/printmod.mli | 6 |
9 files changed, 73 insertions, 72 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 109a40a037..0f6452de69 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -171,17 +171,17 @@ let tag_var = tag Tag.variable let pr_qualid sp = let (sl, id) = repr_qualid sp in - let id = tag_ref (pr_id id) in + let id = tag_ref (Id.print id) in let sl = match List.rev (DirPath.repr sl) with | [] -> mt () | sl -> - let pr dir = tag_path (pr_id dir) ++ str "." in + let pr dir = tag_path (Id.print dir) ++ str "." in prlist pr sl in sl ++ id - let pr_id = pr_id - let pr_name = pr_name + let pr_id = Id.print + let pr_name = Name.print let pr_qualid = pr_qualid let pr_patvar = pr_id diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index be96cfce50..1320cce9be 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -43,6 +43,8 @@ val pr_sep_com : val pr_id : Id.t -> Pp.t val pr_name : Name.t -> Pp.t +[@@ocaml.deprecated "alias of Names.Name.print"] + val pr_qualid : qualid -> Pp.t val pr_patvar : patvar -> Pp.t diff --git a/printing/pputils.ml b/printing/pputils.ml index 9ef9162aee..3cc7a3e6b9 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -9,7 +9,6 @@ open Util open Pp open Genarg -open Nameops open Misctypes open Locus open Genredexpr @@ -27,7 +26,7 @@ let pr_located pr (loc, x) = let pr_or_var pr = function | ArgArg x -> pr x - | ArgVar (_,s) -> pr_id s + | ArgVar (_,s) -> Names.Id.print s let pr_with_occurrences pr keyword (occs,c) = match occs with diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fdaeded878..acbd2d5d2f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -33,12 +33,12 @@ open Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type object_pr = { - print_inductive : mutual_inductive -> Pp.t; - print_constant_with_infos : constant -> Pp.t; + print_inductive : MutInd.t -> Pp.t; + print_constant_with_infos : Constant.t -> Pp.t; print_section_variable : variable -> Pp.t; - print_syntactic_def : kernel_name -> Pp.t; - print_module : bool -> Names.module_path -> Pp.t; - print_modtype : module_path -> Pp.t; + print_syntactic_def : KerName.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : Context.Named.Declaration.t -> Pp.t; print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; print_context : bool -> int option -> Lib.library_segment -> Pp.t; @@ -94,7 +94,7 @@ let print_ref reduce ref = (********************************) (** Printing implicit arguments *) -let pr_impl_name imp = pr_id (name_of_implicit imp) +let pr_impl_name imp = Id.print (name_of_implicit imp) let print_impargs_by_name max = function | [] -> [] @@ -238,7 +238,7 @@ let print_primitive_record recflag mipv = function | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" | Decl_kinds.BiFinite -> str " with eta conversion" in - [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] + [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] let print_primitive ref = @@ -271,7 +271,7 @@ let print_name_infos ref = let print_id_args_data test pr id l = if List.exists test l then - pr (str "For " ++ pr_id id) l + pr (str "For " ++ Id.print id) l else [] @@ -318,8 +318,8 @@ type locatable = Locatable : 'a locatable_info -> locatable type logical_name = | Term of global_reference | Dir of global_dir_reference - | Syntactic of kernel_name - | ModuleType of module_path + | Syntactic of KerName.t + | ModuleType of ModPath.t | Other : 'a * 'a locatable_info -> logical_name | Undefined of qualid @@ -456,7 +456,7 @@ let print_located_qualid name flags ref = | [] -> let (dir,id) = repr_qualid qid in if DirPath.is_empty dir then - str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id + str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id else str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid | l -> @@ -608,7 +608,7 @@ let gallina_print_syntactic_def kn = hov 2 (hov 4 (str "Notation " ++ pr_qualid qid ++ - prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ + prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++ spc () ++ str ":=") ++ spc () ++ Constrextern.without_specific_symbols @@ -623,14 +623,14 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = constraints *) (try Some(print_named_decl (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> - Some (print_constant with_values sep (constant_of_kn kn)) + Some (print_constant with_values sep (Constant.make1 kn)) | (_,"INDUCTIVE") -> - Some (gallina_print_inductive (mind_of_kn kn)) + Some (gallina_print_inductive (MutInd.make1 kn)) | (_,"MODULE") -> - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in Some (print_module with_values (MPdot (mp,l))) | (_,"MODULE TYPE") -> - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in Some (print_modtype (MPdot (mp,l))) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None @@ -638,7 +638,7 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = | (_,s) -> None let gallina_print_library_entry with_values ent = - let pr_name (sp,_) = pr_id (basename sp) in + let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> gallina_print_leaf_entry with_values (oname,lobj) @@ -750,12 +750,12 @@ let print_full_pure_context () = str "." ++ fnl () ++ fnl () | "MODULE" -> (* TODO: make it reparsable *) - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | "MODULE TYPE" -> (* TODO: make it reparsable *) (* TODO: make it reparsable *) - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _ -> mt () in prec rest ++ pp diff --git a/printing/prettyp.mli b/printing/prettyp.mli index dbd1011593..31fd766ea3 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -80,12 +80,12 @@ val print_located_module : reference -> Pp.t val print_located_other : string -> reference -> Pp.t type object_pr = { - print_inductive : mutual_inductive -> Pp.t; - print_constant_with_infos : constant -> Pp.t; + print_inductive : MutInd.t -> Pp.t; + print_constant_with_infos : Constant.t -> Pp.t; print_section_variable : variable -> Pp.t; - print_syntactic_def : kernel_name -> Pp.t; - print_module : bool -> Names.module_path -> Pp.t; - print_modtype : module_path -> Pp.t; + print_syntactic_def : KerName.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : Context.Named.Declaration.t -> Pp.t; print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; print_context : bool -> int option -> Lib.library_segment -> Pp.t; diff --git a/printing/printer.ml b/printing/printer.ml index 70e96722d6..075b03b7d1 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -11,6 +11,7 @@ open CErrors open Util open Names open Term +open Constr open Environ open Globnames open Nametab @@ -477,7 +478,7 @@ let pr_predicate pr_elt (b, elts) = if List.is_empty elts then str"none" else pr_elts let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) -let pr_idpred p = pr_predicate Nameops.pr_id (Id.Pred.elements p) +let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p) let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ @@ -855,15 +856,15 @@ let prterm = pr_lconstr It is used primarily by the Print Assumptions command. *) type axiom = - | Constant of constant (* An axiom or a constant. *) + | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *) + | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) | Axiom of axiom * (Label.t * Context.Rel.t * types) list - | Opaque of constant (* An opaque constant. *) - | Transparent of constant + | Opaque of Constant.t (* An opaque constant. *) + | Transparent of Constant.t (* Defines a set of [assumption] *) module OrderedContextObject = @@ -873,11 +874,11 @@ struct let compare_axiom x y = match x,y with | Constant k1 , Constant k2 -> - con_ord k1 k2 + Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> - con_ord k1 k2 + Constant.CanOrd.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 | _ -> -1 @@ -890,10 +891,10 @@ struct | Axiom (k1,_) , Axiom (k2, _) -> compare_axiom k1 k2 | Axiom _ , _ -> -1 | _ , Axiom _ -> 1 - | Opaque k1 , Opaque k2 -> con_ord k1 k2 + | Opaque k1 , Opaque k2 -> Constant.CanOrd.compare k1 k2 | Opaque _ , _ -> -1 | _ , Opaque _ -> 1 - | Transparent k1 , Transparent k2 -> con_ord k1 k2 + | Transparent k1 , Transparent k2 -> Constant.CanOrd.compare k1 k2 end module ContextObjectSet = Set.Make (OrderedContextObject) @@ -907,8 +908,8 @@ let pr_assumptionset env s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> - let mp,_,lab = repr_con kn in - str (string_of_mp mp) ++ str "." ++ pr_label lab + let mp,_,lab = Constant.repr3 kn in + str (ModPath.to_string mp) ++ str "." ++ Label.print lab in let safe_pr_ltype typ = try str " : " ++ pr_ltype typ @@ -942,7 +943,7 @@ let pr_assumptionset env s = let ax = pr_axiom env axiom typ ++ cut() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> - str " used in " ++ pr_label lbl ++ + str " used in " ++ Label.print lbl ++ str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) l in (v, ax :: a, o, tr) diff --git a/printing/printer.mli b/printing/printer.mli index f55206f0df..fbba14edea 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -8,7 +8,7 @@ open Names open Globnames -open Term +open Constr open Environ open Pattern open Evd @@ -81,11 +81,11 @@ val pr_closed_glob : closed_glob_constr -> Pp.t val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_lglob_constr_env : env -> glob_constr -> Pp.t -val pr_lglob_constr : glob_constr -> Pp.t +val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_lglob_constr : 'a glob_constr_g -> Pp.t -val pr_glob_constr_env : env -> glob_constr -> Pp.t -val pr_glob_constr : glob_constr -> Pp.t +val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_glob_constr : 'a glob_constr_g -> Pp.t val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t val pr_lconstr_pattern : constr_pattern -> Pp.t @@ -95,22 +95,22 @@ val pr_constr_pattern : constr_pattern -> Pp.t val pr_cases_pattern : cases_pattern -> Pp.t -val pr_sort : evar_map -> sorts -> Pp.t +val pr_sort : evar_map -> Sorts.t -> Pp.t (** Universe constraints *) val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t -val pr_universe_instance : evar_map -> Univ.universe_context -> Pp.t -val pr_universe_ctx : evar_map -> Univ.universe_context -> Pp.t -val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> Pp.t +val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t +val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) val pr_global_env : Id.Set.t -> global_reference -> Pp.t val pr_global : global_reference -> Pp.t -val pr_constant : env -> constant -> Pp.t +val pr_constant : env -> Constant.t -> Pp.t val pr_existential_key : evar_map -> existential_key -> Pp.t val pr_existential : env -> evar_map -> existential -> Pp.t val pr_constructor : env -> constructor -> Pp.t @@ -183,22 +183,22 @@ val prterm : constr -> Pp.t (** = pr_lconstr *) (** Declarations for the "Print Assumption" command *) type axiom = - | Constant of constant (* An axiom or a constant. *) + | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *) + | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) | Axiom of axiom * (Label.t * Context.Rel.t * types) list - | Opaque of constant (* An opaque constant. *) - | Transparent of constant + | Opaque of Constant.t (* An opaque constant. *) + | Transparent of Constant.t module ContextObjectSet : Set.S with type elt = context_object module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet val pr_assumptionset : - env -> Term.types ContextObjectMap.t -> Pp.t + env -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : Id.t -> Pp.t diff --git a/printing/printmod.ml b/printing/printmod.ml index 755e905a70..0abca01602 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -7,12 +7,11 @@ (************************************************************************) open Util -open Term +open Constr open Pp open Names open Environ open Declarations -open Nameops open Globnames open Libnames open Goptions @@ -80,7 +79,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) @@ -107,7 +106,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = 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 @@ -149,7 +148,7 @@ let print_mutual_inductive env mind mib = 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 @@ -189,15 +188,15 @@ let print_record env mind mib = Printer.pr_cumulative (Declareops.inductive_is_polymorphic mib) (Declareops.inductive_is_cumulative mib) ++ - def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ + 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" }" ++ match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> str "" @@ -215,9 +214,9 @@ let pr_mutual_inductive_body env mind mib = (** 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 = @@ -301,7 +300,7 @@ 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 @@ -403,7 +402,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 = diff --git a/printing/printmod.mli b/printing/printmod.mli index 8c3f0149e6..b0bbb21e05 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -11,6 +11,6 @@ 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 -> mutual_inductive -> Declarations.mutual_inductive_body -> Pp.t -val print_module : bool -> module_path -> Pp.t -val print_modtype : module_path -> Pp.t +val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> Pp.t +val print_module : bool -> ModPath.t -> Pp.t +val print_modtype : ModPath.t -> Pp.t |