From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- parsing/g_vernac.ml4 | 4 +- parsing/lexer.ml4 | 4 +- parsing/ppvernac.ml | 10 +-- parsing/prettyp.ml | 190 ++++++++++++++++++++++++++++++++------------------- parsing/prettyp.mli | 9 +-- parsing/printer.ml | 4 +- 6 files changed, 132 insertions(+), 89 deletions(-) (limited to 'parsing') diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 1f5a6cf9..304640b2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_vernac.ml4 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: g_vernac.ml4 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp @@ -549,7 +549,7 @@ GEXTEND Gram (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; - pos = OPT [ "["; l = LIST0 implicit_name; "]" -> + pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> VernacDeclareImplicits (use_section_locality (),qid,pos) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index cc48c84f..a89594c2 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -10,7 +10,7 @@ (* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with * ast-based camlp4 *) -(*i $Id: lexer.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: lexer.ml4 13521 2010-10-10 21:59:00Z herbelin $ i*) open Pp open Util @@ -147,7 +147,7 @@ let lookup_utf8_tail c cs = | _ -> error_utf8 cs in try classify_unicode unicode, n - with UnsupportedUtf8 -> error_unsupported_unicode_character n cs + with UnsupportedUtf8 -> njunk n cs; error_unsupported_unicode_character n cs let lookup_utf8 cs = match Stream.peek cs with diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index ff35be57..b5e0cc4a 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: ppvernac.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp open Names @@ -847,13 +847,15 @@ let rec pr_vernac = function (pr_locality local ++ str"Notation " ++ pr_lident id ++ prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) - | VernacDeclareImplicits (local,q,None) -> + | VernacDeclareImplicits (local,q,[]) -> hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ pr_smart_global q) - | VernacDeclareImplicits (local,q,Some imps) -> + | VernacDeclareImplicits (local,q,impls) -> hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++ spc() ++ pr_smart_global q ++ spc() ++ - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") + prlist_with_sep spc (fun imps -> + str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") + impls) | VernacReserve bl -> let n = List.length (List.flatten (List.map fst bl)) in hov 2 (str"Implicit Type" ++ diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 9c39e57e..cf83c72a 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id: prettyp.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: prettyp.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp open Util @@ -51,39 +51,25 @@ type object_pr = { let gallina_print_module = print_module let gallina_print_modtype = print_modtype -(*********************) -(** Basic printing *) - -let print_basename sp = pr_global (ConstRef sp) +(**************) +(** Utilities *) let print_closed_sections = ref false -let with_line_skip p = if ismt p then mt() else (fnl () ++ p) +let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) ++ fnl() -(********************************) -(** Printing implicit arguments *) +let with_line_skip l = if l = [] then mt() else fnl() ++ pr_infos_list l -let conjugate_to_be = function [_] -> "is" | _ -> "are" +let blankline = mt() (* add a blank sentence in the list of infos *) -let pr_implicit imp = pr_id (name_of_implicit imp) +let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": " -let print_impl_args_by_name max = function - | [] -> mt () - | impls -> - hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ - prlist_with_sep pr_comma pr_implicit impls ++ spc() ++ - str (conjugate_to_be impls) ++ str" implicit" ++ - (if max then strbrk " and maximally inserted" else mt())) ++ fnl() +let int_or_no n = if n=0 then str "no" else int n -let print_impl_args l = - let imps = List.filter is_status_implicit l in - let maximps = List.filter Impargs.maximal_insertion_of imps in - let nonmaximps = list_subtract imps maximps in - print_impl_args_by_name false nonmaximps ++ - print_impl_args_by_name true maximps +(*******************) +(** Basic printing *) -(*********************) -(** Printing Scopes *) +let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref = let typ = Global.type_of_global ref in @@ -92,16 +78,49 @@ let print_ref reduce ref = 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 () ++ pr_ltype typ) ++ fnl () + hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) -let print_argument_scopes = function - | [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl() - | l when not (List.for_all ((=) None) l) -> - hov 2 (str"Argument scopes are" ++ spc() ++ - str "[" ++ - prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++ - str "]") ++ fnl() - | _ -> mt() +(********************************) +(** Printing implicit arguments *) + +let conjugate_verb_to_be = function [_] -> "is" | _ -> "are" + +let pr_impl_name imp = pr_id (name_of_implicit imp) + +let print_impargs_by_name max = function + | [] -> [] + | impls -> + [hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ + prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++ + str (conjugate_verb_to_be impls) ++ str" implicit" ++ + (if max then strbrk " and maximally inserted" else mt()))] + +let print_one_impargs_list l = + let imps = List.filter is_status_implicit l in + let maximps = List.filter Impargs.maximal_insertion_of imps in + let nonmaximps = list_subtract imps maximps in + print_impargs_by_name false nonmaximps @ + print_impargs_by_name true maximps + +let print_impargs_list prefix l = + let l = extract_impargs_data l in + List.flatten (List.map (fun (cond,imps) -> + match cond with + | None -> + List.map (fun pp -> add_colon prefix ++ pp) + (print_one_impargs_list imps) + | Some (n1,n2) -> + [v 2 (prlist_with_sep cut (fun x -> x) + [(if ismt prefix then str "When" else prefix ++ str ", when") ++ + str " applied to " ++ + (if n1 = n2 then int_or_no n2 else + if n1 = 0 then str "less than " ++ int n2 + else int n1 ++ str " to " ++ int_or_no n2) ++ + str (plural n2 " argument") ++ str ":"; + v 0 (prlist_with_sep cut (fun x -> x) + (if List.exists is_status_implicit imps + then print_one_impargs_list imps + else [str "No implicit arguments"]))])]) l) let need_expansion impl ref = let typ = Global.type_of_global ref in @@ -111,6 +130,33 @@ let need_expansion impl ref = let _,lastimpl = list_chop nprods impl in List.filter is_status_implicit lastimpl <> [] +let print_impargs ref = + let ref = Smartlocate.smart_global ref in + let impl = implicits_of_global ref in + let has_impl = impl <> [] in + (* Need to reduce since implicits are computed with products flattened *) + pr_infos_list + ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref; + blankline ] @ + (if has_impl then print_impargs_list (mt()) impl + else [str "No implicit arguments"])) + +(*********************) +(** Printing Scopes *) + +let print_argument_scopes prefix = function + | [Some sc] -> + [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"] + | l when not (List.for_all ((=) None) l) -> + [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++ + str "[" ++ + prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++ + str "]")] + | _ -> [] + +(*********************) +(** Printing Opacity *) + type opacity = | FullyOpaque | TransparentMaybeOpacified of Conv_oracle.level @@ -128,8 +174,9 @@ let opacity env = function let print_opacity ref = match opacity (Global.env()) ref with - | None -> mt () - | Some s -> pr_global ref ++ str " is " ++ + | None -> [] + | Some s -> + [pr_global ref ++ str " is " ++ str (match s with | FullyOpaque -> "opaque" | TransparentMaybeOpacified Conv_oracle.Opaque -> @@ -139,38 +186,45 @@ let print_opacity ref = | TransparentMaybeOpacified (Conv_oracle.Level n) -> "transparent (with expansion weight "^string_of_int n^")" | TransparentMaybeOpacified Conv_oracle.Expand -> - "transparent (with minimal expansion weight)") ++ fnl() + "transparent (with minimal expansion weight)")] + +(*******************) +(* *) let print_name_infos ref = - let impl = implicits_of_global ref in + let impls = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in - let type_for_implicit = - if need_expansion impl ref then + let type_info_for_implicit = + if need_expansion (select_impargs_size 0 impls) ref then (* Need to reduce since implicits are computed with products flattened *) - str "Expanded type for implicit arguments" ++ fnl () ++ - print_ref true ref ++ fnl() - else mt() in - type_for_implicit ++ print_impl_args impl ++ print_argument_scopes scopes + [str "Expanded type for implicit arguments"; + print_ref true ref; blankline] + else + [] in + type_info_for_implicit @ + print_impargs_list (mt()) impls @ + print_argument_scopes (mt()) scopes let print_id_args_data test pr id l = if List.exists test l then - str"For " ++ pr_id id ++ str": " ++ pr l + pr (str "For " ++ pr_id id) l else - mt() + [] let print_args_data_of_inductive_ids get test pr sp mipv = - prvecti + List.flatten (Array.to_list (Array.mapi (fun i mip -> - print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) ++ - prvecti + print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) @ + List.flatten (Array.to_list (Array.mapi (fun j idc -> print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1)))) - mip.mind_consnames) - mipv + mip.mind_consnames))) + mipv)) let print_inductive_implicit_args = print_args_data_of_inductive_ids - implicits_of_global is_status_implicit print_impl_args + implicits_of_global (fun l -> positions_of_implicits l <> []) + print_impargs_list let print_inductive_argument_scopes = print_args_data_of_inductive_ids @@ -365,7 +419,7 @@ let gallina_print_inductive sp = else pr_mutual_inductive mib.mind_finite names) ++ fnl () ++ with_line_skip - (print_inductive_implicit_args sp mipv ++ + (print_inductive_implicit_args sp mipv @ print_inductive_argument_scopes sp mipv) let print_named_decl id = @@ -666,16 +720,19 @@ let print_opaque_name qid = print_named_decl (id,c,ty) let print_about_any k = - begin match k with + match k with | Term ref -> - print_ref false ref ++ fnl () ++ print_name_infos ref ++ - print_opacity ref + pr_infos_list + ([print_ref false ref; blankline] @ + print_name_infos ref @ + print_opacity ref @ + [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> - print_syntactic_def kn + v 0 ( + print_syntactic_def kn ++ + hov 0 (str "Expands to: " ++ pr_located_qualid k)) ++ fnl() | Dir _ | ModuleType _ | Undefined _ -> - mt () end - ++ - hov 0 (str "Expands to: " ++ pr_located_qualid k) + hov 0 (pr_located_qualid k) ++ fnl() let print_about = function | Genarg.ByNotation (loc,ntn,sc) -> @@ -685,15 +742,6 @@ let print_about = function | Genarg.AN ref -> print_about_any (locate_any_name ref) -let print_impargs ref = - let ref = Smartlocate.smart_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 (need_expansion impl ref) ref ++ fnl() ++ - (if has_impl then print_impl_args impl - else (str "No implicit arguments" ++ fnl ())) - let unfold_head_fconst = let rec unfrec k = match kind_of_term k with | Const cst -> constant_value (Global.env ()) cst @@ -771,7 +819,7 @@ let print_canonical_projections () = open Typeclasses let pr_typeclass env t = - print_ref false t.cl_impl + print_ref false t.cl_impl ++ fnl () let print_typeclasses () = let env = Global.env () in @@ -780,7 +828,7 @@ let print_typeclasses () = let pr_instance env i = (* gallina_print_constant_with_infos i.is_impl *) (* lighter *) - print_ref false (instance_impl i) + print_ref false (instance_impl i) ++ fnl () let print_all_instances () = let env = Global.env () in diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index d7f83b63..5704f54e 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: prettyp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: prettyp.mli 13492 2010-10-04 21:20:01Z herbelin $ i*) (*i*) open Pp @@ -26,7 +26,6 @@ open Genarg val assumptions_for_print : name list -> Termops.names_context val print_closed_sections : bool ref -val print_impl_args : Impargs.implicits_list -> std_ppcmds val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option val print_full_context : unit -> std_ppcmds @@ -46,12 +45,6 @@ val print_opaque_name : reference -> std_ppcmds val print_about : reference or_by_notation -> std_ppcmds val print_impargs : reference or_by_notation -> std_ppcmds -(*i -val print_extracted_name : identifier -> std_ppcmds -val print_extraction : unit -> std_ppcmds -val print_extracted_vars : unit -> std_ppcmds -i*) - (* Pretty-printing functions for classes and coercions *) val print_graph : unit -> std_ppcmds val print_classes : unit -> std_ppcmds diff --git a/parsing/printer.ml b/parsing/printer.ml index c9f27678..cf0050a5 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: printer.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: printer.ml 13390 2010-09-02 08:03:01Z herbelin $ *) open Pp open Util @@ -263,7 +263,7 @@ let pr_predicate pr_elt (b, elts) = else if elts = [] then str"none" else pr_elts -let pr_cpred p = pr_predicate pr_con (Cpred.elements p) +let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p) let pr_transparent_state (ids, csts) = -- cgit v1.2.3