diff options
-rw-r--r-- | contrib/interface/xlate.ml | 3 | ||||
-rw-r--r-- | parsing/g_basevernac.ml4 | 3 | ||||
-rw-r--r-- | parsing/prettyp.ml | 51 | ||||
-rw-r--r-- | parsing/prettyp.mli | 1 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 1 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 1 | ||||
-rw-r--r-- | translate/ppvernacnew.ml | 1 |
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 -> |