aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml3
-rw-r--r--parsing/g_basevernac.ml43
-rw-r--r--parsing/prettyp.ml51
-rw-r--r--parsing/prettyp.mli1
-rw-r--r--toplevel/vernacentries.ml1
-rw-r--r--toplevel/vernacexpr.ml1
-rw-r--r--translate/ppvernacnew.ml1
7 files changed, 38 insertions, 23 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6b4b82e39..5e0bc4d9f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1474,7 +1474,8 @@ let xlate_vernac =
| PrintScopes -> xlate_error "TODO: Print Scopes"
| PrintScope _ -> xlate_error "TODO: Print Scope"
| PrintVisibility _ -> xlate_error "TODO: Print Visibility"
- | PrintAbout _ -> xlate_error "TODO: Print About")
+ | PrintAbout _ -> xlate_error "TODO: Print About"
+ | _ -> xlate_error "TODO: Print")
| VernacBeginSection id ->
CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
| VernacEndSegment id -> CT_section_end (xlate_ident id)
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 27675758f..da16be9b5 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -194,7 +194,8 @@ GEXTEND Gram
| IDENT "HintDb"; s = IDENT -> PrintHintDbName s
| IDENT "Scopes" -> PrintScopes
| IDENT "Scope"; s = IDENT -> PrintScope s
- | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s ] ]
+ | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
+ | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]
;
locatable:
[ [ qid = global -> LocateTerm qid
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index ff6411a40..8c1ff3211 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -76,7 +76,10 @@ let print_argument_scopes = function
let print_name_infos ref =
let impl = implicits_of_global ref in
let scopes = Symbols.find_arguments_scope ref in
- (if impl<>[] or not (List.for_all ((=) None) scopes) then fnl() else mt())
+ (if (List.filter is_status_implicit impl<>[])
+ or not (List.for_all ((=) None) scopes)
+ then fnl()
+ else mt())
++ print_impl_args impl ++ print_argument_scopes scopes
let print_id_args_data test pr id l =
@@ -295,8 +298,10 @@ let print_constant with_values sep sp =
| _ ->
print_basename sp ++ str sep ++ cut () ++
(if with_values then print_typed_body (val_0,typ) else prtype typ) ++
- fnl ()) ++
- print_name_infos (ConstRef sp)
+ fnl ())
+
+let print_constant_with_infos sp =
+ print_constant true " = " sp ++ print_name_infos (ConstRef sp)
let print_inductive sp = (print_mutual sp)
@@ -410,7 +415,7 @@ let print_eval red_fun env {uj_val=trm;uj_type=typ} =
let print_name ref =
match locate_any_name ref with
- | Term (ConstRef sp) -> print_constant true " = " sp
+ | Term (ConstRef sp) -> print_constant_with_infos sp
| Term (IndRef (sp,_)) -> print_inductive sp
| Term (ConstructRef ((sp,_),_)) -> print_inductive sp
| Term (VarRef sp) -> print_section_variable sp
@@ -450,7 +455,7 @@ let print_opaque_name qid =
| ConstRef cst ->
let cb = Global.lookup_constant cst in
if cb.const_body <> None then
- print_constant true " = " cst
+ print_constant_with_infos cst
else
error "not a defined constant"
| IndRef (sp,_) ->
@@ -462,30 +467,34 @@ let print_opaque_name qid =
let (_,c,ty) = lookup_named id env in
print_named_decl (id,c,ty)
+let print_ref reduce ref =
+ let typ = Global.type_of_global ref in
+ let typ =
+ if reduce then
+ let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
+ in it_mkProd_or_LetIn ccl ctx
+ else typ in
+ hov 0 (pr_global ref ++ str " :" ++ spc () ++ prtype typ) ++ fnl ()
+
let print_about ref =
let sigma = Evd.empty in
- let env = Global.env () in
let k = locate_any_name ref in
begin match k with
- | Term (ConstRef sp as ref) ->
- print_constant false " : " sp
- | Term (IndRef ind as ref) ->
- let ty = Inductive.type_of_inductive env ind in
- print_typed_value (mkInd ind, ty) ++
- print_name_infos ref
- | Term (ConstructRef cstr as ref) ->
- let ty = Inductive.type_of_constructor env cstr in
- print_typed_value (mkConstruct cstr, ty) ++
- print_name_infos ref
- | Term (VarRef sp as ref) ->
- print_named_decl (get_variable sp) ++
- print_name_infos ref
- | Syntactic kn ->
- print_syntactic_def " = " kn
+ | Term ref -> print_ref false ref ++ print_name_infos ref
+ | Syntactic kn -> print_syntactic_def " = " kn
| Dir _ | ModuleType _ | Undefined _ -> mt () end
++
hov 0 (str "Expands to: " ++ pr_located_qualid k)
+let print_impargs ref =
+ let ref = Nametab.global ref in
+ let impl = implicits_of_global ref in
+ let has_impl = List.filter is_status_implicit impl <> [] in
+ (* Need to reduce since implicits are computed with products flattened *)
+ print_ref true ref ++ fnl() ++
+ (if has_impl then print_impl_args impl
+ else (str "No implicit arguments" ++ fnl ()))
+
let print_local_context () =
let env = Lib.contents_after None in
let rec print_var_rec = function
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 769688493..d58d7808d 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -44,6 +44,7 @@ val print_name : reference -> std_ppcmds
val print_opaque_name : reference -> std_ppcmds
val print_local_context : unit -> std_ppcmds
val print_about : reference -> std_ppcmds
+val print_impargs : reference -> std_ppcmds
(*i
val print_extracted_name : identifier -> std_ppcmds
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 94bdb1a08..67da01408 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -879,6 +879,7 @@ let vernac_print = function
| PrintVisibility s ->
pp (Symbols.pr_visibility (Constrextern.without_symbols pr_rawterm) s)
| PrintAbout qid -> msgnl (print_about qid)
+ | PrintImplicit qid -> msg (print_impargs qid)
let global_module r =
let (loc,qid) = qualid_of_reference r in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e720245b7..76d16862a 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -55,6 +55,7 @@ type printable =
| PrintScope of string
| PrintVisibility of string option
| PrintAbout of reference
+ | PrintImplicit of reference
type search_about_item =
| SearchRef of reference
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 9e6aa0fe0..ae51a552b 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1020,6 +1020,7 @@ let rec pr_vernac = function
| PrintScope s -> str"Print Scope" ++ spc() ++ str s
| PrintVisibility s -> str"Print Visibility" ++ pr_opt str s
| PrintAbout qid -> str"About" ++ spc() ++ pr_reference qid
+ | PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_reference qid
in pr_printable p
| VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern
| VernacLocate loc ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-07 22:46:39 +0000