diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 40 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 7 | ||||
| -rw-r--r-- | printing/pputils.ml | 3 | ||||
| -rw-r--r-- | printing/pputils.mli | 3 | ||||
| -rw-r--r-- | printing/prettyp.ml | 20 | ||||
| -rw-r--r-- | printing/prettyp.mli | 21 | ||||
| -rw-r--r-- | printing/printer.ml | 6 |
7 files changed, 46 insertions, 54 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e877b3c63d..e38da45b95 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -15,15 +15,15 @@ open Pp open CAst open Names open Nameops -open Constr open Libnames open Pputils open Ppextend -open Notation_gram +open Glob_term open Constrexpr open Constrexpr_ops +open Notation_gram open Decl_kinds -open Misctypes +open Namegen (*i*) module Tag = @@ -159,7 +159,7 @@ let tag_var = tag Tag.variable let pr_univ_expr = function | Some (x,n) -> - pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) | None -> str"_" let pr_univ l = @@ -180,7 +180,7 @@ let tag_var = tag Tag.variable | GSet -> tag_type (str "Set") | GType UUnknown -> tag_type (str "Type") | GType UAnonymous -> tag_type (str "_") - | GType (UNamed u) -> tag_type (pr_reference u) + | GType (UNamed u) -> tag_type (pr_qualid u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -205,16 +205,16 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | UNamed u -> pr_reference u + | UNamed u -> pr_qualid u | UAnonymous -> tag_type (str "Type") | UUnknown -> tag_type (str "_")) let pr_universe_instance l = pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l - let pr_reference = CAst.with_val (function - | Qualid qid -> pr_qualid qid - | Ident id -> tag_var (pr_id id)) + let pr_reference qid = + if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid) + else pr_qualid qid let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -228,7 +228,7 @@ let tag_var = tag Tag.variable str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type_spc pr = function - | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt () + | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t let pr_lident {loc; v=id} = @@ -242,8 +242,8 @@ let tag_var = tag Tag.variable | x -> pr_ast Name.print x let pr_or_var pr = function - | ArgArg x -> pr x - | ArgVar id -> pr_lident id + | Locus.ArgArg x -> pr x + | Locus.ArgVar id -> pr_lident id let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) @@ -363,7 +363,7 @@ let tag_var = tag Tag.variable end | Default b -> match t with - | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> + | { CAst.v = CHole (_,IntroAnonymous,_) } -> let s = prlist_with_sep spc pr_lname nal in hov 1 (surround_implicit b s) | _ -> @@ -457,7 +457,7 @@ let tag_var = tag Tag.variable let pr_case_type pr po = match po with - | None | Some { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt() + | None | Some { CAst.v = CHole (_,IntroAnonymous,_) } -> mt() | Some p -> spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p) @@ -564,9 +564,9 @@ let tag_var = tag Tag.variable return (p ++ prlist (pr spc (lapp,L)) l2, lapp) else return (p, lproj) - | CAppExpl ((None,{v=Ident var},us),[t]) - | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None]) - when Id.equal var Notation_ops.ldots_var -> + | CAppExpl ((None,qid,us),[t]) + | CApp ((_, {v = CRef(qid,us)}),[t,None]) + when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var -> return ( hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg @@ -592,7 +592,7 @@ let tag_var = tag Tag.variable hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> + | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ @@ -643,9 +643,9 @@ let tag_var = tag Tag.variable lif ) - | CHole (_,Misctypes.IntroIdentifier id,_) -> + | CHole (_,IntroIdentifier id,_) -> return (str "?[" ++ pr_id id ++ str "]", latom) - | CHole (_,Misctypes.IntroFresh id,_) -> + | CHole (_,IntroFresh id,_) -> return (str "?[?" ++ pr_id id ++ str "]", latom) | CHole (_,_,_) -> return (str "_", latom) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 05f48ec79d..bca419c9ac 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -15,14 +15,13 @@ open Libnames open Constrexpr open Names -open Misctypes open Notation_gram val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t -val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t +val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t val pr_lident : lident -> Pp.t val pr_lname : lname -> Pp.t @@ -39,7 +38,7 @@ 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 +val pr_patvar : Pattern.patvar -> Pp.t val pr_glob_level : Glob_term.glob_level -> Pp.t val pr_glob_sort : Glob_term.glob_sort -> Pp.t @@ -48,7 +47,7 @@ val pr_guard_annot : (constr_expr -> Pp.t) -> lident option * recursion_order_expr -> Pp.t -val pr_record_body : (reference * constr_expr) list -> Pp.t +val pr_record_body : (qualid * constr_expr) list -> Pp.t val pr_binders : local_binder_expr list -> Pp.t val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t diff --git a/printing/pputils.ml b/printing/pputils.ml index c14aa318e1..c6b8d50222 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -11,7 +11,6 @@ open Util open Pp open Genarg -open Misctypes open Locus open Genredexpr @@ -122,7 +121,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) -let pr_or_by_notation f = function +let pr_or_by_notation f = let open Constrexpr in function | {CAst.loc; v=AN v} -> f v | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc diff --git a/printing/pputils.mli b/printing/pputils.mli index 6039168f88..5b1969e232 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -9,7 +9,6 @@ (************************************************************************) open Genarg -open Misctypes open Locus open Genredexpr @@ -18,7 +17,7 @@ val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t (** Prints an object surrounded by its commented location *) val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t -val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t +val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t val pr_with_occurrences : ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 895181bc51..5e5d003622 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -26,7 +26,6 @@ open Libobject open Libnames open Globnames open Recordops -open Misctypes open Printer open Printmod open Context.Rel.Declaration @@ -345,8 +344,7 @@ let register_locatable name f = exception ObjFound of logical_name -let locate_any_name ref = - let {v=qid} = qualid_of_reference ref in +let locate_any_name qid = try Term (Nametab.locate qid) with Not_found -> try Syntactic (Nametab.locate_syndef qid) @@ -453,8 +451,7 @@ type locatable_kind = | LocOther of string | LocAny -let print_located_qualid name flags ref = - let {v=qid} = qualid_of_reference ref in +let print_located_qualid name flags qid = let located = match flags with | LocTerm -> locate_term qid | LocModule -> locate_modtype qid @ locate_module qid @@ -788,10 +785,9 @@ let print_full_pure_context env sigma = follows the definition of the inductive type *) (* This is designed to print the contents of an opened section *) -let read_sec_context r = - let qid = qualid_of_reference r in +let read_sec_context qid = let dir = - try Nametab.locate_section qid.v + try Nametab.locate_section qid with Not_found -> user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function @@ -843,12 +839,12 @@ let print_any_name env sigma na udecl = let print_name env sigma na udecl = match na with - | {loc; v=ByNotation (ntn,sc)} -> + | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | {loc; v=AN ref} -> + | {loc; v=Constrexpr.AN ref} -> print_any_name env sigma (locate_any_name ref) udecl let print_opaque_name env sigma qid = @@ -896,11 +892,11 @@ let print_about_any ?loc env sigma k udecl = let print_about env sigma na udecl = match na with - | {loc;v=ByNotation (ntn,sc)} -> + | {loc;v=Constrexpr.ByNotation (ntn,sc)} -> print_about_any ?loc env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | {loc;v=AN ref} -> + | {loc;v=Constrexpr.AN ref} -> print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 50042d6c5b..8dd7296100 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,7 +12,6 @@ open Names open Environ open Reductionops open Libnames -open Misctypes open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -25,20 +24,20 @@ val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node val print_full_context : env -> Evd.evar_map -> Pp.t val print_full_context_typ : env -> Evd.evar_map -> Pp.t val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t -val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t +val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : env -> Evd.evar_map -> reference or_by_notation -> +val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t -val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t -val print_about : env -> Evd.evar_map -> reference or_by_notation -> +val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t +val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t -val print_impargs : reference or_by_notation -> Pp.t +val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) val print_graph : env -> evar_map -> Pp.t @@ -78,10 +77,10 @@ val register_locatable : string -> 'a locatable_info -> unit name describing the kind of objects considered and that is added as a grammar command prefix for vernacular commands Locate. *) -val print_located_qualid : reference -> Pp.t -val print_located_term : reference -> Pp.t -val print_located_module : reference -> Pp.t -val print_located_other : string -> reference -> Pp.t +val print_located_qualid : qualid -> Pp.t +val print_located_term : qualid -> Pp.t +val print_located_module : qualid -> Pp.t +val print_located_other : string -> qualid -> Pp.t type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; diff --git a/printing/printer.ml b/printing/printer.ml index 72030dc9f6..d76bd1e2b2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -229,15 +229,15 @@ let dirpath_of_global = function dirpath_of_mp (MutInd.modpath kn) | VarRef _ -> DirPath.empty -let qualid_of_global env r = - Libnames.make_qualid (dirpath_of_global r) (id_of_global env r) +let qualid_of_global ?loc env r = + Libnames.make_qualid ?loc (dirpath_of_global r) (id_of_global env r) let safe_gen f env sigma c = let orig_extern_ref = Constrextern.get_extern_reference () in let extern_ref ?loc vars r = try orig_extern_ref vars r with e when CErrors.noncritical e -> - CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r) + qualid_of_global ?loc env r in Constrextern.set_extern_reference extern_ref; try |